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/frb50-23-opb/normalized-frb50-23-5.opb
MD5SUM	54f6acf3ab92bda8abb11350f74de20e
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-37
Optimality of the best value was proved	NO
Number of terms in the objective function	1150
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	1150
Number of bits of the sum of numbers in the objective function	11
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	1150
Number of bits of the biggest sum of numbers	11
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.08
Number of variables	1150
Total number of constraints	80035
Number of constraints which are clauses	80035
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 6383

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc17 THE 2005-04-14 04:47:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4850 boxname=wulflinc17 idbench=338 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  54f6acf3ab92bda8abb11350f74de20e  /oldhome/oroussel/tmp/wulflinc17/normalized-frb50-23-5.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc17/normalized-frb50-23-5.opb /oldhome/oroussel/tmp/wulflinc17/normalized-frb50-23-5.opb
IDLAUNCH: 4850
/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:        813320 kB
Buffers:         36400 kB
Cached:         149652 kB
SwapCached:       2376 kB
Active:          61868 kB
Inactive:       129532 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        813068 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              44 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            24168 kB
Committed_AS:    63740 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:07:53 (client local time) WITH STATUS 10 IN 1200.3 SECONDS
stats: 4850 7 1200.3 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 80035 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ...................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   80035   160070 |   26678       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:63046     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  216507   479341 |   72169       0        0     nan |  0.000 % |
c |       100 |  216109   478437 |   79385      89      482     5.4 |  0.253 % |
c |       250 |  214483   474731 |   87324     183      830     4.5 |  1.276 % |
c |       475 |  213200   471802 |   96056     378    10844    28.7 |  2.094 % |
c |       812 |  208836   461835 |  105662     650    14469    22.3 |  4.869 % |
c |      1318 |  205701   454627 |  116228    1089    16983    15.6 |  6.961 % |
c |      2077 |  199516   440379 |  127851    1744    25891    14.8 | 11.147 % |
c |      3216 |  186888   411223 |  140636    2599    32865    12.6 | 19.821 % |
c |      4924 |  167463   366223 |  154700    3601    41433    11.5 | 33.395 % |
c |      7486 |  146314   316658 |  170170    5222    59361    11.4 | 48.526 % |
c |     11332 |  122260   260396 |  187187    7055   106701    15.1 | 66.093 % |
c |     17098 |  108188   227416 |  205906   10417   159050    15.3 | 76.489 % |
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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18784 |  105222   220461 |   35074   11602   179143    15.4 | 76.489 % |
c |     18884 |  103847   217238 |   38581   11534   178729    15.5 | 79.734 % |
c |     19037 |  103516   216463 |   42439   11607   179378    15.5 | 79.985 % |
c |     19263 |  103208   215742 |   46683   11686   181682    15.5 | 80.215 % |
c |     19602 |  103188   215696 |   51351   12010   187227    15.6 | 80.228 % |
c |     20108 |  102447   213939 |   56487   12339   190553    15.4 | 80.803 % |
c |     20867 |  101567   211876 |   62135   12756   198408    15.6 | 81.454 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     21180 |  101699   212217 |   33899   13069   201561    15.4 | 81.454 % |
c |     21280 |  101649   212098 |   37288   13151   202608    15.4 | 81.464 % |
c |     21430 |  101154   210938 |   41017   13152   201744    15.3 | 81.817 % |
c |     21655 |  101130   210881 |   45119   13340   205845    15.4 | 81.837 % |
c |     21992 |  100751   209969 |   49631   13533   209468    15.5 | 82.152 % |
c |     22498 |  100363   209055 |   54594   13793   216881    15.7 | 82.450 % |
c |     23257 |   99853   207851 |   60054   14168   223719    15.8 | 82.842 % |
c |     24396 |   99363   206688 |   66059   14947   236846    15.8 | 83.227 % |
c |     26104 |   98344   204309 |   72665   16133   286787    17.8 | 83.980 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27116 |   97798   203012 |   32599   16548   299953    18.1 | 83.980 % |
c |     27216 |   97672   202720 |   35858   16518   298831    18.1 | 84.496 % |
c |     27367 |   97223   201668 |   39444   16416   298552    18.2 | 84.831 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27507 |   97289   201838 |   32429   16556   301080    18.2 | 84.831 % |
c |     27607 |   97209   201648 |   35671   16573   301566    18.2 | 84.868 % |
c |     27757 |   97201   201629 |   39239   16714   304854    18.2 | 84.874 % |
c |     27984 |   97118   201434 |   43162   16845   309029    18.3 | 84.939 % |
c |     28321 |   96790   200654 |   47479   16998   314195    18.5 | 85.208 % |
c |     28827 |   96784   200640 |   52227   17496   331626    19.0 | 85.213 % |
c |     29586 |   96770   200608 |   57449   18243   353799    19.4 | 85.221 % |
c |     30726 |   96262   199411 |   63194   18610   374765    20.1 | 85.610 % |
c |     32434 |   95739   198178 |   69514   19814   424743    21.4 | 86.011 % |
c |     34997 |   95638   197945 |   76465   22234   605603    27.2 | 86.080 % |
c ==============================================================================
c [1mFound solution: -42[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     38374 |   94773   195880 |   31591   24574   735028    29.9 | 86.080 % |
c |     38474 |   94652   195595 |   34750   24639   736267    29.9 | 86.839 % |
c |     38624 |   94652   195595 |   38225   24789   745760    30.1 | 86.839 % |
c |     38849 |   94652   195595 |   42047   25014   757011    30.3 | 86.839 % |
c |     39186 |   94652   195595 |   46252   25351   772206    30.5 | 86.839 % |
c |     39692 |   94652   195595 |   50877   25857   824446    31.9 | 86.839 % |
c |     40451 |   94652   195595 |   55965   26616   878175    33.0 | 86.839 % |
c |     41590 |   94479   195182 |   61561   27584   975083    35.3 | 86.982 % |
c |     43298 |   94471   195163 |   67718   29288  1079848    36.9 | 86.988 % |
c |     45862 |   94255   194653 |   74489   31140  1227091    39.4 | 87.158 % |
c |     49706 |   94147   194398 |   81938   34937  1606697    46.0 | 87.245 % |
c |     55472 |   93554   193021 |   90132   40290  2171046    53.9 | 87.670 % |
c ==============================================================================
c [1mFound solution: -43[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     62272 |   93627   193204 |   31209   47090  2963097    62.9 | 87.670 % |
c |     62372 |   93522   192957 |   34329   47116  2964652    62.9 | 87.730 % |
c |     62522 |   93522   192957 |   37762   47266  2974226    62.9 | 87.730 % |
c |     62747 |   93522   192957 |   41539   47491  2989349    62.9 | 87.730 % |
c |     63085 |   93522   192957 |   45693   47829  3021859    63.2 | 87.730 % |
c |     63591 |   93447   192785 |   50262   48266  3055835    63.3 | 87.780 % |
c |     64351 |   93447   192785 |   55288   49026  3118705    63.6 | 87.780 % |
c |     65490 |   93047   191836 |   60817   49558  3187050    64.3 | 88.107 % |
c |     67198 |   93047   191836 |   66899   51266  3352054    65.4 | 88.107 % |
c |     69760 |   93033   191802 |   73589   53826  3648285    67.8 | 88.120 % |
c |     73604 |   92942   191586 |   80948   57324  3962210    69.1 | 88.195 % |
c |     79370 |   92942   191586 |   89042   63090  4596363    72.9 | 88.195 % |
c |     88020 |   92769   191176 |   97947   71186  6032750    84.7 | 88.335 % |
c |    100994 |   92769   191176 |  107741   84160  7874850    93.6 | 88.335 % |
c ==============================================================================
c [1mFound solution: -44[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    103820 |   92715   191041 |   30905   86662  8131164    93.8 | 88.335 % |
c |    103921 |   92715   191041 |   33995   20004  1850980    92.5 | 88.374 % |
c |    104071 |   92709   191027 |   37395   20151  1860656    92.3 | 88.378 % |
c |    104296 |   92695   190994 |   41134   20369  1873688    92.0 | 88.389 % |
c |    104633 |   92685   190971 |   45248   20703  1906598    92.1 | 88.396 % |
c |    105140 |   92685   190971 |   49772   21210  1972341    93.0 | 88.396 % |
c |    105899 |   92566   190694 |   54750   21935  2004077    91.4 | 88.480 % |
c |    107039 |   92562   190685 |   60225   23071  2118377    91.8 | 88.482 % |
c |    108747 |   92353   190189 |   66247   24653  2254214    91.4 | 88.650 % |
c |    111309 |   92339   190155 |   72872   27210  2480642    91.2 | 88.662 % |
c |    115153 |   92331   190136 |   80159   31051  2894852    93.2 | 88.669 % |
c |    120919 |   92331   190136 |   88175   36817  3579853    97.2 | 88.669 % |
c |    129569 |   92331   190136 |   96993   45467  4674293   102.8 | 88.669 % |
c |    142543 |   92331   190136 |  106692   58441  6361638   108.9 | 88.669 % |
c ==============================================================================
c [1mFound solution: -45[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    161971 |   92345   190174 |   30781   77812  9847048   126.5 | 88.669 % |
c |    162074 |   92345   190174 |   33859   18370  2550798   138.9 | 88.667 % |
c |    162224 |   92329   190136 |   37245   18519  2554629   137.9 | 88.680 % |
c |    162449 |   92323   190122 |   40969   18740  2557007   136.4 | 88.684 % |
c |    162787 |   92287   190037 |   45066   19064  2574618   135.1 | 88.712 % |
c |    163293 |   92235   189913 |   49573   19557  2590933   132.5 | 88.755 % |
c |    164052 |   92235   189913 |   54530   20316  2628690   129.4 | 88.755 % |
c |    165191 |   92235   189913 |   59983   21455  2720865   126.8 | 88.755 % |
c |    166899 |   92156   189723 |   65981   23145  2818919   121.8 | 88.816 % |
c |    169463 |   92142   189690 |   72579   25704  3033735   118.0 | 88.826 % |
c |    173308 |   92016   189393 |   79837   29414  3400502   115.6 | 88.923 % |
c |    179074 |   92002   189360 |   87821   35174  3854576   109.6 | 88.934 % |
c |    187723 |   91996   189346 |   96603   43821  4632924   105.7 | 88.938 % |
c |    200697 |   91986   189323 |  106264   56792  6146274   108.2 | 88.945 % |
c |    220160 |   91986   189323 |  116890   76255  8052895   105.6 | 88.945 % |
c ==============================================================================
c [1mFound solution: -46[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    232484 |   91939   189185 |   30646   88565  9647230   108.9 | 88.945 % |
c |    232585 |   91939   189185 |   33710   21350  1679600    78.7 | 88.975 % |
c |    232735 |   91931   189166 |   37081   21499  1686977    78.5 | 88.982 % |
c |    232960 |   91931   189166 |   40789   21724  1699874    78.2 | 88.982 % |
c |    233300 |   91931   189166 |   44868   22064  1732205    78.5 | 88.982 % |
c |    233806 |   91931   189166 |   49355   22570  1766884    78.3 | 88.982 % |
c |    234566 |   91931   189166 |   54291   23330  1839066    78.8 | 88.982 % |
c |    235705 |   91931   189166 |   59720   24469  1918659    78.4 | 88.982 % |
c |    237413 |   91931   189166 |   65692   26177  2023895    77.3 | 88.982 % |
c |    239975 |   91931   189166 |   72261   28739  2241886    78.0 | 88.982 % |
c |    243820 |   91931   189166 |   79487   32584  2646636    81.2 | 88.982 % |
c |    249586 |   91909   189113 |   87436   38344  3255301    84.9 | 89.001 % |
c |    258235 |   91909   189113 |   96180   46993  4018908    85.5 | 89.001 % |
c |    271209 |   91909   189113 |  105798   59967  5110703    85.2 | 89.001 % |
c |    290670 |   91839   188951 |  116378   79420  7012404    88.3 | 89.050 % |
c |    319863 |   91839   188951 |  128015  108613  9254896    85.2 | 89.050 % |
c |    363653 |   91839   188951 |  140817  152403 13548725    88.9 | 89.050 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C1150 -C1149 -C1148 -C1147 -C1146 -C1145 -C1144 -C1143 -C1142 -C1141 -C1140 -C1139 -C1138 -C1137 -C1136 -C1135 -C1134 -C1133 -C1132 C1131 -C1130 -C1129 -C1128 -C1127 -C1126 -C1125 -C1124 -C1123 C1122 -C1121 -C1120 -C1119 -C1118 -C1117 -C1116 -C1115 -C1114 -C1113 -C1112 -C1111 -C1110 -C1109 -C1108 -C1107 -C1106 -C1105 -C1104 -C1103 -C1102 -C1101 -C1100 -C1099 -C1098 -C1097 -C1096 -C1095 -C1094 -C1093 -C1092 -C1091 -C1090 -C1089 -C1088 C1087 -C1086 -C1085 -C1084 -C1083 -C1082 -C1081 -C1080 -C1079 -C1078 -C1077 -C1076 -C1075 -C1074 -C1073 -C1072 -C1071 -C1070 C1069 -C1068 -C1067 -C1066 -C1065 -C1064 -C1063 -C1062 -C1061 -C1060 -C1059 -C1058 -C1057 C1056 -C1055 -C1054 -C1053 -C1052 -C1051 -C1050 -C1049 -C1048 -C1047 -C1046 -C1045 -C1044 -C1043 -C1042 -C1041 -C1040 -C1039 -C1038 -C1037 -C1036 -C1035 -C1034 -C1033 -C1032 -C1031 -C1030 -C1029 C1028 -C1027 -C1026 -C1025 -C1024 -C1023 -C1022 -C1021 -C1020 -C1019 -C1018 -C1017 -C1016 -C1015 -C1014 -C1013 -C1012 -C1011 -C1010 -C1009 -C1008 -C1007 -C1006 -C1005 C1004 -C1003 -C1002 -C1001 -C1000 -C999 -C998 -C997 -C996 -C995 -C994 -C993 -C992 -C991 -C990 -C989 -C988 -C987 -C986 -C985 -C984 -C983 -C982 -C981 -C980 -C979 -C978 -C977 -C976 -C975 C974 -C973 -C972 -C971 -C970 -C969 -C968 -C967 -C966 -C965 -C964 -C963 -C962 -C961 -C960 -C959 -C958 -C957 -C956 -C955 -C954 -C953 C952 -C951 -C950 -C949 -C948 -C947 -C946 -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 -C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 C901 -C900 -C899 -C898 -C897 -C896 C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 -C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 -C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 -C849 -C848 C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 -C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 -C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 C760 -C759 -C758 -C757 -C756 -C755 -C754 -C753 -C752 -C751 C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 -C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 C685 -C684 -C683 -C682 -C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 C660 -C659 -C658 -C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 -C642 -C641 -C640 -C639 -C638 -C637 C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 -C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 -C577 C576 C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C4#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/55 29429
Raw data (stat): 29429 (runsolver) R 29428 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481836234 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.0006 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5259 0 0 0 985 13 0 0 25 0 1 0 481836234 24330240 5237 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5940 5237 603 41 0 5899 0
vsize: 23760
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5269 0 0 0 1984 14 0 0 25 0 1 0 481836234 24330240 5247 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5940 5247 603 41 0 5899 0
vsize: 23760
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5274 0 0 0 2985 14 0 0 25 0 1 0 481836234 24330240 5252 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5940 5252 603 41 0 5899 0
vsize: 23760
[startup+40.001 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5276 0 0 0 3983 14 0 0 25 0 1 0 481836234 24330240 5254 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5940 5254 603 41 0 5899 0
vsize: 23760
[startup+50.0005 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5281 0 0 0 4984 14 0 0 25 0 1 0 481836234 24494080 5259 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5980 5259 603 41 0 5939 0
vsize: 23920
[startup+60.0004 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5282 0 0 0 5984 14 0 0 25 0 1 0 481836234 24494080 5260 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5980 5260 603 41 0 5939 0
vsize: 23920
[startup+70.001 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5286 0 0 0 6983 15 0 0 25 0 1 0 481836234 24494080 5264 4294967295 134512640 134672761 3221224560 3221223752 134556585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5980 5264 603 41 0 5939 0
vsize: 23920
[startup+80.0013 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5319 0 0 0 7983 15 0 0 25 0 1 0 481836234 24625152 5297 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6012 5297 603 41 0 5971 0
vsize: 24048
[startup+90.0013 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5345 0 0 0 8983 15 0 0 25 0 1 0 481836234 24760320 5323 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6045 5323 603 41 0 6004 0
vsize: 24180
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5643 0 0 0 9983 16 0 0 25 0 1 0 481836234 26726400 5621 4294967295 134512640 134672761 3221224560 3221223732 134556658 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6525 5621 603 41 0 6484 0
vsize: 26100
[startup+110.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5663 0 0 0 10982 16 0 0 25 0 1 0 481836234 26968064 5641 4294967295 134512640 134672761 3221224560 3221223728 134560842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6584 5641 603 41 0 6543 0
vsize: 26336
[startup+120.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 5922 0 0 0 11982 17 0 0 25 0 1 0 481836234 27910144 5900 4294967295 134512640 134672761 3221224560 3221223696 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6814 5900 603 41 0 6773 0
vsize: 27256
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 6290 0 0 0 12981 18 0 0 25 0 1 0 481836234 29499392 6268 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7202 6268 603 41 0 7161 0
vsize: 28808
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 6800 0 0 0 13980 19 0 0 25 0 1 0 481836234 31506432 6778 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7692 6778 603 41 0 7651 0
vsize: 30768
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 7384 0 0 0 14978 21 0 0 25 0 1 0 481836234 34045952 7362 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8312 7362 603 41 0 8271 0
vsize: 33248
[startup+160.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29429
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 7905 0 0 0 15976 23 0 0 25 0 1 0 481836234 36061184 7883 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8804 7883 603 41 0 8763 0
vsize: 35216
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 8482 0 0 0 16974 25 0 0 25 0 1 0 481836234 38445056 8460 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9386 8460 603 41 0 9345 0
vsize: 37544
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 8784 0 0 0 17974 26 0 0 25 0 1 0 481836234 39694336 8762 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9691 8762 603 41 0 9650 0
vsize: 38764
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 9218 0 0 0 18972 28 0 0 25 0 1 0 481836234 41435136 9196 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10116 9196 603 41 0 10075 0
vsize: 40464
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 9571 0 0 0 19971 29 0 0 25 0 1 0 481836234 42909696 9549 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10476 9549 603 41 0 10435 0
vsize: 41904
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 9991 0 0 0 20970 30 0 0 25 0 1 0 481836234 44654592 9969 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10902 9969 603 41 0 10861 0
vsize: 43608
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 10408 0 0 0 21968 32 0 0 25 0 1 0 481836234 46260224 10386 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11294 10386 603 41 0 11253 0
vsize: 45176
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 10954 0 0 0 22967 34 0 0 25 0 1 0 481836234 48787456 10932 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11911 10932 603 41 0 11870 0
vsize: 47644
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 11488 0 0 0 23966 35 0 0 25 0 1 0 481836234 50925568 11466 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12433 11466 603 41 0 12392 0
vsize: 49732
[startup+250.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 11902 0 0 0 24964 37 0 0 25 0 1 0 481836234 52662272 11880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12857 11880 603 41 0 12816 0
vsize: 51428
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 12310 0 0 0 25963 38 0 0 25 0 1 0 481836234 54272000 12288 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13250 12288 603 41 0 13209 0
vsize: 53000
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 12710 0 0 0 26962 39 0 0 25 0 1 0 481836234 55865344 12688 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13639 12688 603 41 0 13598 0
vsize: 54556
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 13125 0 0 0 27961 41 0 0 25 0 1 0 481836234 57581568 13103 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14058 13103 603 41 0 14017 0
vsize: 56232
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 13532 0 0 0 28961 41 0 0 25 0 1 0 481836234 59301888 13510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14478 13510 603 41 0 14437 0
vsize: 57912
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 13866 0 0 0 29960 42 0 0 25 0 1 0 481836234 60641280 13844 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14805 13844 603 41 0 14764 0
vsize: 59220
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 30959 43 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+320.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 31959 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+330.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 32959 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223664 134560381 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 33959 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 34959 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+360.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 35960 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 36960 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223664 134560318 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 37960 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 38960 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 39960 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 40961 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+420.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 41961 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+430.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14076 0 0 0 42961 44 0 0 25 0 1 0 481836234 61431808 14054 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14998 14054 603 41 0 14957 0
vsize: 59992
[startup+440.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 14598 0 0 0 43960 45 0 0 25 0 1 0 481836234 63586304 14576 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15524 14576 603 41 0 15483 0
vsize: 62096
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15078 0 0 0 44960 46 0 0 25 0 1 0 481836234 65585152 15056 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16012 15056 603 41 0 15971 0
vsize: 64048
[startup+460.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29431
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15565 0 0 0 45959 47 0 0 25 0 1 0 481836234 67588096 15543 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16501 15543 603 41 0 16460 0
vsize: 66004
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 46958 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 47959 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 48959 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 49959 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+510.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 50959 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 51959 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223664 134560169 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 52959 47 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 53959 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 54959 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 55959 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 56959 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 57959 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 58960 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 59960 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 60960 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 61960 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223744 134558841 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 62960 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 63960 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15948 0 0 0 64961 48 0 0 25 0 1 0 481836234 69099520 15926 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15926 603 41 0 16829 0
vsize: 67480
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 65961 48 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 66961 48 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 67961 48 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 68961 48 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 69961 48 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223664 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 70962 48 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 71962 49 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29433
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 72962 49 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+740.087 s]
Raw data (loadavg): 1.15 1.00 0.92 3/58 29475
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 73967 50 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+750.087 s]
Raw data (loadavg): 1.20 1.02 0.93 2/55 29487
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 74963 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+760.088 s]
Raw data (loadavg): 1.17 1.02 0.93 2/55 29487
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 75963 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+770.087 s]
Raw data (loadavg): 1.14 1.02 0.93 2/55 29489
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 76963 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+780.088 s]
Raw data (loadavg): 1.12 1.02 0.93 2/55 29489
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 77963 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+790.088 s]
Raw data (loadavg): 1.10 1.02 0.93 2/55 29489
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 78964 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+800.088 s]
Raw data (loadavg): 1.08 1.01 0.93 2/55 29489
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 79964 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223560 1075349746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+810.088 s]
Raw data (loadavg): 1.07 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 80964 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+820.087 s]
Raw data (loadavg): 1.06 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 81964 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+830.088 s]
Raw data (loadavg): 1.05 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 82964 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+840.088 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15950 0 0 0 83964 55 0 0 25 0 1 0 481836234 69099520 15928 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15928 603 41 0 16829 0
vsize: 67480
[startup+850.087 s]
Raw data (loadavg): 1.04 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15951 0 0 0 84964 55 0 0 25 0 1 0 481836234 69099520 15929 4294967295 134512640 134672761 3221224560 3221223664 134560158 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15929 603 41 0 16829 0
vsize: 67480
[startup+860.088 s]
Raw data (loadavg): 1.03 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15953 0 0 0 85965 55 0 0 25 0 1 0 481836234 69099520 15931 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15931 603 41 0 16829 0
vsize: 67480
[startup+870.087 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15956 0 0 0 86965 55 0 0 25 0 1 0 481836234 69099520 15934 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15934 603 41 0 16829 0
vsize: 67480
[startup+880.088 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15959 0 0 0 87965 55 0 0 25 0 1 0 481836234 69099520 15937 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15937 603 41 0 16829 0
vsize: 67480
[startup+890.088 s]
Raw data (loadavg): 1.02 1.01 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15961 0 0 0 88965 55 0 0 25 0 1 0 481836234 69099520 15939 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15939 603 41 0 16829 0
vsize: 67480
[startup+900.088 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15964 0 0 0 89965 55 0 0 25 0 1 0 481836234 69099520 15942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15942 603 41 0 16829 0
vsize: 67480
[startup+910.089 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15966 0 0 0 90966 55 0 0 25 0 1 0 481836234 69099520 15944 4294967295 134512640 134672761 3221224560 3221223728 134560845 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15944 603 41 0 16829 0
vsize: 67480
[startup+920.089 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 15969 0 0 0 91966 55 0 0 25 0 1 0 481836234 69099520 15947 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15947 603 41 0 16829 0
vsize: 67480
[startup+930.09 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 16005 0 0 0 92965 55 0 0 25 0 1 0 481836234 69234688 15983 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16903 15983 603 41 0 16862 0
vsize: 67612
[startup+940.091 s]
Raw data (loadavg): 1.01 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 16241 0 0 0 93965 56 0 0 25 0 1 0 481836234 70299648 16219 4294967295 134512640 134672761 3221224560 3221223664 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17163 16219 603 41 0 17122 0
vsize: 68652
[startup+950.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 16502 0 0 0 94965 56 0 0 25 0 1 0 481836234 71372800 16480 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17425 16480 603 41 0 17384 0
vsize: 69700
[startup+960.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 16729 0 0 0 95964 57 0 0 25 0 1 0 481836234 72298496 16707 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17651 16707 603 41 0 17610 0
vsize: 70604
[startup+970.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 16945 0 0 0 96964 58 0 0 25 0 1 0 481836234 73093120 16923 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17845 16923 603 41 0 17804 0
vsize: 71380
[startup+980.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 17153 0 0 0 97963 59 0 0 25 0 1 0 481836234 74018816 17131 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18071 17131 603 41 0 18030 0
vsize: 72284
[startup+990.091 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 17358 0 0 0 98963 59 0 0 25 0 1 0 481836234 74821632 17336 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18267 17336 603 41 0 18226 0
vsize: 73068
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 17561 0 0 0 99962 60 0 0 25 0 1 0 481836234 75616256 17539 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18461 17539 603 41 0 18420 0
vsize: 73844
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 17751 0 0 0 100962 60 0 0 25 0 1 0 481836234 76402688 17729 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18653 17729 603 41 0 18612 0
vsize: 74612
[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 17959 0 0 0 101961 61 0 0 25 0 1 0 481836234 77197312 17937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18847 17937 603 41 0 18806 0
vsize: 75388
[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 18195 0 0 0 102961 61 0 0 25 0 1 0 481836234 78647296 18173 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19201 18173 603 41 0 19160 0
vsize: 76804
[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 18421 0 0 0 103961 62 0 0 25 0 1 0 481836234 79572992 18399 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19427 18399 603 41 0 19386 0
vsize: 77708
[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 18684 0 0 0 104960 63 0 0 25 0 1 0 481836234 80637952 18662 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19687 18662 603 41 0 19646 0
vsize: 78748
[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29491
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 18932 0 0 0 105960 63 0 0 25 0 1 0 481836234 81698816 18910 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19946 18910 603 41 0 19905 0
vsize: 79784
[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29493
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 19144 0 0 0 106959 64 0 0 25 0 1 0 481836234 82501632 19122 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20142 19122 603 41 0 20101 0
vsize: 80568
[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 19336 0 0 0 107959 64 0 0 25 0 1 0 481836234 83296256 19314 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20336 19314 603 41 0 20295 0
vsize: 81344
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 19516 0 0 0 108959 65 0 0 25 0 1 0 481836234 84090880 19494 4294967295 134512640 134672761 3221224560 3221223728 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20530 19494 603 41 0 20489 0
vsize: 82120
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 19680 0 0 0 109958 66 0 0 25 0 1 0 481836234 84754432 19658 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20692 19658 603 41 0 20651 0
vsize: 82768
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 19868 0 0 0 110958 66 0 0 25 0 1 0 481836234 85557248 19846 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20888 19846 603 41 0 20847 0
vsize: 83552
[startup+1120.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 20085 0 0 0 111958 67 0 0 25 0 1 0 481836234 86487040 20063 4294967295 134512640 134672761 3221224560 3221223696 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21115 20063 603 41 0 21074 0
vsize: 84460
[startup+1130.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 20314 0 0 0 112957 67 0 0 25 0 1 0 481836234 87416832 20292 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21342 20292 603 41 0 21301 0
vsize: 85368
[startup+1140.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 20522 0 0 0 113956 68 0 0 25 0 1 0 481836234 88223744 20500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21539 20500 603 41 0 21498 0
vsize: 86156
[startup+1150.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 20723 0 0 0 114955 69 0 0 25 0 1 0 481836234 89026560 20701 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21735 20701 603 41 0 21694 0
vsize: 86940
[startup+1160.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 20932 0 0 0 115954 70 0 0 25 0 1 0 481836234 89956352 20910 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21962 20910 603 41 0 21921 0
vsize: 87848
[startup+1170.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 21132 0 0 0 116954 71 0 0 25 0 1 0 481836234 90750976 21110 4294967295 134512640 134672761 3221224560 3221223760 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22156 21110 603 41 0 22115 0
vsize: 88624
[startup+1180.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 21358 0 0 0 117953 71 0 0 25 0 1 0 481836234 91684864 21336 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22384 21336 603 41 0 22343 0
vsize: 89536
[startup+1190.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 21582 0 0 0 118953 72 0 0 25 0 1 0 481836234 92483584 21560 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22579 21560 603 41 0 22538 0
vsize: 90316
[startup+1200.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/55 29495
Raw data (stat): 29429 (minisat+) R 29428 20838 20837 0 -1 0 21801 0 0 0 119953 72 0 0 25 0 1 0 481836234 93421568 21779 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22808 21779 603 41 0 22767 0
vsize: 91232
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 1.00 1.00 0.93 1/55 29495
Raw data (stat): 29429 (minisat+) Z 29428 20838 20837 0 -1 12 21804 0 0 0 119953 76 0 0 25 0 1 0 481836234 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.3
CPU user time (s): 1199.53
CPU system time (s): 0.769882
CPU usage (%): 100.014
Max. virtual memory (Kb): 91232
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####