PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034724 kB
MemFree:        701964 kB
Buffers:         35228 kB
Cached:         185512 kB
SwapCached:       1212 kB
Active:         147936 kB
Inactive:       153208 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        701708 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25716 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:11:48 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 4465 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 59186 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): ..................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   59186   118372 |   19728       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  104775   225435 |   34925       0        0     nan |  0.000 % |
c |       100 |  104524   224914 |   38417      85     1066    12.5 |  0.436 % |
c |       250 |  103672   223098 |   42259     189     2294    12.1 |  2.065 % |
c |       475 |  102383   220255 |   46485     345     4840    14.0 |  4.529 % |
c |       812 |  100937   217141 |   51133     586     7419    12.7 |  7.149 % |
c |      1318 |   98182   211016 |   56247     955    12123    12.7 | 12.554 % |
c |      2077 |   95016   203912 |   61871    1479    18940    12.8 | 18.868 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      2281 |   94270   202263 |   31423    1638    21254    13.0 | 18.868 % |
c |      2381 |   93557   200642 |   34565    1705    22268    13.1 | 21.898 % |
c |      2531 |   92946   199272 |   38021    1827    23369    12.8 | 23.109 % |
c |      2756 |   91830   196738 |   41824    1986    25232    12.7 | 25.365 % |
c |      3093 |   90546   193828 |   46006    2258    28068    12.4 | 27.941 % |
c |      3599 |   89135   190554 |   50607    2662    32253    12.1 | 30.930 % |
c |      4358 |   86431   184320 |   55667    3235    39718    12.3 | 36.339 % |
c |      5497 |   82098   174321 |   61234    4060    50083    12.3 | 45.224 % |
c |      7205 |   78759   166500 |   67357    5274    69800    13.2 | 52.309 % |
c |      9767 |   74447   156240 |   74093    7257   115053    15.9 | 61.626 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     11855 |   72901   152602 |   24300    9007   171237    19.0 | 61.626 % |
c |     11956 |   72669   152047 |   26730    9026   173881    19.3 | 65.703 % |
c |     12106 |   72511   151662 |   29403    9103   175319    19.3 | 66.054 % |
c |     12332 |   71960   150355 |   32343    9214   178574    19.4 | 67.232 % |
c |     12669 |   71960   150355 |   35577    9551   186891    19.6 | 67.232 % |
c |     13175 |   71822   150026 |   39135   10017   198100    19.8 | 67.634 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     13651 |   71767   149867 |   23922   10477   227070    21.7 | 67.634 % |
c |     13751 |   71635   149552 |   26314   10560   229754    21.8 | 67.952 % |
c |     13901 |   71495   149231 |   28945   10689   232692    21.8 | 68.240 % |
c |     14126 |   71495   149231 |   31840   10914   240590    22.0 | 68.240 % |
c |     14464 |   71301   148771 |   35024   11166   247387    22.2 | 68.658 % |
c |     14970 |   71096   148283 |   38526   11598   264285    22.8 | 69.105 % |
c |     15729 |   70692   147312 |   42379   12216   294929    24.1 | 70.005 % |
c |     16868 |   70606   147101 |   46617   13307   355598    26.7 | 70.197 % |
c |     18576 |   70013   145662 |   51278   14834   442373    29.8 | 71.487 % |
c |     21138 |   69860   145296 |   56406   17357   580759    33.5 | 71.822 % |
c |     24982 |   69186   143692 |   62047   21008   882895    42.0 | 73.271 % |
c |     30748 |   68669   142440 |   68252   26564  1266965    47.7 | 74.405 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     36888 |   68477   142002 |   22825   32538  2350890    72.3 | 74.405 % |
c |     36989 |   68477   142002 |   25107   32639  2355889    72.2 | 74.863 % |
c |     37139 |   68477   142002 |   27618   32789  2364920    72.1 | 74.863 % |
c |     37364 |   68390   141794 |   30380   32976  2374435    72.0 | 75.048 % |
c |     37701 |   68208   141353 |   33418   33252  2387786    71.8 | 75.447 % |
c |     38207 |   68191   141312 |   36759   33737  2410028    71.4 | 75.485 % |
c |     38966 |   68191   141312 |   40435   34496  2508782    72.7 | 75.485 % |
c |     40105 |   67643   139988 |   44479   35447  2584380    72.9 | 76.710 % |
c |     41813 |   67533   139718 |   48927   36998  2681268    72.5 | 76.965 % |
c |     44377 |   67408   139415 |   53820   39481  2933313    74.3 | 77.249 % |
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 |     46463 |   67399   139347 |   22466   41488  3173600    76.5 | 77.249 % |
c |     46563 |   67366   139264 |   24712   41579  3178985    76.5 | 77.355 % |
c |     46714 |   67366   139264 |   27183   41730  3188195    76.4 | 77.355 % |
c |     46939 |   67366   139264 |   29902   41955  3203516    76.4 | 77.355 % |
c |     47277 |   67152   138734 |   32892   42197  3212016    76.1 | 77.856 % |
c |     47783 |   67024   138429 |   36181   42593  3256759    76.5 | 78.130 % |
c |     48542 |   66893   138094 |   39799   43247  3317085    76.7 | 78.440 % |
c |     49681 |   66773   137806 |   43779   44272  3468329    78.3 | 78.708 % |
c |     51389 |   66773   137806 |   48157   45980  3665783    79.7 | 78.708 % |
c |     53951 |   66773   137806 |   52973   48542  3874270    79.8 | 78.708 % |
c |     57795 |   66703   137642 |   58271   52249  4403144    84.3 | 78.858 % |
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 |     60959 |   66746   137780 |   22248   55413  4808677    86.8 | 78.858 % |
c |     61059 |   66746   137780 |   24472   19970  1491252    74.7 | 78.843 % |
c |     61209 |   66696   137659 |   26920   20112  1501421    74.7 | 78.955 % |
c |     61434 |   66655   137558 |   29612   20326  1508405    74.2 | 79.050 % |
c |     61772 |   66655   137558 |   32573   20664  1548997    75.0 | 79.050 % |
c |     62278 |   66641   137528 |   35830   21164  1579134    74.6 | 79.075 % |
c |     63038 |   66483   137145 |   39413   21877  1624906    74.3 | 79.428 % |
c |     64178 |   66436   137033 |   43355   23009  1706960    74.2 | 79.533 % |
c |     65886 |   66394   136940 |   47690   24715  1877964    76.0 | 79.612 % |
c |     68448 |   66394   136940 |   52459   27277  2138187    78.4 | 79.612 % |
c |     72292 |   66188   136448 |   57705   31053  2536364    81.7 | 80.060 % |
c |     78058 |   65990   135958 |   63476   36773  3108332    84.5 | 80.515 % |
c |     86708 |   65668   135177 |   69823   45315  4027181    88.9 | 81.214 % |
c |     99682 |   65663   135166 |   76806   58283  5489233    94.2 | 81.223 % |
c |    119143 |   65625   135078 |   84486   77730  8037334   103.4 | 81.303 % |
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 |    133656 |   65574   134927 |   21858   91840  9604872   104.6 | 81.303 % |
c |    133756 |   65574   134927 |   24043   23083  1518038    65.8 | 81.425 % |
c |    133906 |   65574   134927 |   26448   23233  1526900    65.7 | 81.425 % |
c |    134131 |   65574   134927 |   29092   23458  1544148    65.8 | 81.425 % |
c |    134468 |   65574   134927 |   32002   23795  1579065    66.4 | 81.425 % |
c |    134975 |   65574   134927 |   35202   24302  1634412    67.3 | 81.425 % |
c |    135734 |   65574   134927 |   38722   25061  1715989    68.5 | 81.425 % |
c |    136873 |   65574   134927 |   42595   26200  1819780    69.5 | 81.425 % |
c |    138581 |   65538   134839 |   46854   27898  1949053    69.9 | 81.507 % |
c |    141143 |   65538   134839 |   51540   30460  2313155    75.9 | 81.507 % |
c |    144987 |   65523   134802 |   56694   34301  2805082    81.8 | 81.542 % |
c |    150753 |   65475   134677 |   62363   40058  3378991    84.4 | 81.663 % |
c |    159402 |   65475   134677 |   68599   48707  4419954    90.7 | 81.663 % |
c |    172376 |   65475   134677 |   75459   61681  6333551   102.7 | 81.663 % |
c |    191837 |   65421   134551 |   83005   81127  9152518   112.8 | 81.778 % |
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 |    219923 |   65394   134505 |   21798  109183 12991111   119.0 | 81.778 % |
c |    220023 |   65338   134375 |   23977   22717  1789048    78.8 | 81.963 % |
c |    220174 |   65333   134362 |   26375   22867  1792281    78.4 | 81.976 % |
c |    220399 |   65333   134362 |   29013   23092  1806748    78.2 | 81.976 % |
c |    220736 |   65333   134362 |   31914   23429  1824678    77.9 | 81.976 % |
c |    221242 |   65333   134362 |   35105   23935  1866744    78.0 | 81.976 % |
c |    222002 |   65293   134272 |   38616   24652  1951243    79.2 | 82.055 % |
c |    223141 |   65286   134253 |   42478   25787  2104469    81.6 | 82.074 % |
c |    224849 |   65180   133992 |   46725   27472  2289235    83.3 | 82.319 % |
c |    227411 |   65176   133982 |   51398   30033  2573728    85.7 | 82.328 % |
c |    231255 |   65155   133933 |   56538   33873  3074425    90.8 | 82.373 % |
c |    237023 |   65155   133933 |   62192   39641  3661660    92.4 | 82.373 % |
c |    245672 |   65067   133711 |   68411   48265  4631228    96.0 | 82.585 % |
c |    258647 |   65059   133691 |   75252   61219  6278193   102.6 | 82.604 % |
c |    278108 |   65021   133594 |   82777   80669  8915752   110.5 | 82.696 % |
c |    307300 |   64872   133243 |   91055   25592  1556180    60.8 | 83.017 % |
c |    351089 |   64793   133051 |  100161   69306  6528778    94.2 | 83.195 % |
c 
c *** TERMINATED ***
s SATISFIABLE
v -C945 -C944 -C943 -C942 -C941 -C940 -C939 -C938 -C937 -C936 -C935 -C934 C933 -C932 -C931 -C930 -C929 -C928 -C927 -C926 -C925 -C924 -C923 -C922 -C921 -C920 -C919 -C918 -C917 -C916 -C915 -C914 -C913 -C912 -C911 C910 -C909 -C908 -C907 -C906 -C905 -C904 -C903 -C902 -C901 -C900 -C899 -C898 -C897 -C896 -C895 -C894 -C893 -C892 -C891 -C890 -C889 -C888 -C887 -C886 -C885 -C884 C883 -C882 -C881 -C880 -C879 -C878 -C877 -C876 -C875 -C874 -C873 C872 -C871 -C870 -C869 -C868 -C867 -C866 -C865 -C864 -C863 -C862 -C861 -C860 -C859 -C858 -C857 -C856 -C855 -C854 -C853 -C852 -C851 -C850 C849 -C848 -C847 -C846 -C845 -C844 -C843 -C842 -C841 -C840 -C839 -C838 -C837 -C836 -C835 -C834 -C833 -C832 -C831 -C830 -C829 -C828 -C827 -C826 -C825 -C824 -C823 -C822 -C821 -C820 -C819 -C818 -C817 -C816 -C815 -C814 -C813 -C812 -C811 -C810 -C809 -C808 -C807 -C806 -C805 -C804 -C803 C802 -C801 -C800 -C799 -C798 -C797 -C796 -C795 -C794 -C793 -C792 -C791 -C790 -C789 -C788 -C787 -C786 -C785 -C784 -C783 C782 -C781 -C780 -C779 -C778 -C777 -C776 -C775 -C774 -C773 -C772 -C771 -C770 -C769 -C768 -C767 -C766 -C765 -C764 -C763 -C762 -C761 -C760 -C759 C758 -C757 C756 -C755 -C754 -C753 -C752 -C751 -C750 -C749 -C748 -C747 -C746 -C745 -C744 -C743 -C742 -C741 -C740 -C739 -C738 -C737 -C736 -C735 -C734 -C733 -C732 -C731 -C730 -C729 -C728 -C727 -C726 -C725 -C724 -C723 -C722 -C721 -C720 C719 -C718 -C717 -C716 -C715 -C714 -C713 -C712 -C711 -C710 -C709 C708 -C707 -C706 -C705 -C704 -C703 -C702 -C701 -C700 -C699 -C698 -C697 -C696 -C695 -C694 -C693 -C692 -C691 -C690 -C689 -C688 -C687 -C686 -C685 -C684 -C683 -C682 C681 -C680 -C679 -C678 -C677 -C676 -C675 -C674 -C673 -C672 -C671 -C670 -C669 -C668 -C667 -C666 -C665 -C664 -C663 -C662 -C661 -C660 -C659 -C658 C657 -C656 -C655 -C654 -C653 -C652 -C651 -C650 -C649 -C648 -C647 -C646 -C645 -C644 -C643 C642 -C641 -C640 -C639 -C638 -C637 -C636 -C635 -C634 -C633 -C632 -C631 -C630 -C629 C628 -C627 -C626 -C625 -C624 -C623 -C622 -C621 -C620 -C619 -C618 -C617 -C616 -C615 -C614 -C613 -C612 -C611 -C610 -C609 -C608 -C607 -C606 -C605 C604 -C603 -C602 -C601 -C600 -C599 -C598 -C597 -C596 -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 -C582 -C581 -C580 -C579 -C578 C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 -C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 -C542 C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 -C494 -C493 -C492 -C491 -C490 C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 -C479 -C478 -C477 -C476 C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 -C454 C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 -C433 -C432 -C431 -C430 -C429 -C428 -C427 C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 -C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 C380 -C379 C378 -C377 -C376 -C375 -C374 -C373 -C372 -C371 -C370 -C369 -C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 -C356 -C355 -C354 C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 C301 -C300 -C299 -C298 -C297 -C296 -C295 -C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 -C275 C274 -C273 -C272 -C271 C270 -C269 -C268 -C267 -C266 -C265 #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.84 0.94 0.91 2/53 14450
Raw data (stat): 14450 (runsolver) R 14449 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481127786 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.94 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 3620 0 0 0 989 9 0 0 25 0 1 0 481127786 16437248 3598 4294967295 134512640 134672761 3221224560 3221223776 134561979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4013 3598 603 41 0 3972 0
vsize: 16052
[startup+20.0022 s]
Raw data (loadavg): 0.89 0.94 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 3716 0 0 0 1988 10 0 0 25 0 1 0 481127786 17170432 3694 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4192 3694 603 41 0 4151 0
vsize: 16768
[startup+30.0028 s]
Raw data (loadavg): 0.90 0.94 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 3716 0 0 0 2987 10 0 0 25 0 1 0 481127786 17170432 3694 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4192 3694 603 41 0 4151 0
vsize: 16768
[startup+40.0036 s]
Raw data (loadavg): 0.92 0.94 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 3716 0 0 0 3987 10 0 0 25 0 1 0 481127786 17170432 3694 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4192 3694 603 41 0 4151 0
vsize: 16768
[startup+50.0046 s]
Raw data (loadavg): 0.93 0.94 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 3829 0 0 0 4987 10 0 0 25 0 1 0 481127786 17608704 3807 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4299 3807 603 41 0 4258 0
vsize: 17196
[startup+60.0051 s]
Raw data (loadavg): 0.94 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 4164 0 0 0 5985 12 0 0 25 0 1 0 481127786 18956288 4142 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4628 4142 603 41 0 4587 0
vsize: 18512
[startup+70.0059 s]
Raw data (loadavg): 0.95 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 4715 0 0 0 6984 13 0 0 25 0 1 0 481127786 21352448 4693 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5213 4693 603 41 0 5172 0
vsize: 20852
[startup+80.0066 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 5176 0 0 0 7982 15 0 0 25 0 1 0 481127786 23236608 5154 4294967295 134512640 134672761 3221224560 3221223664 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5673 5154 603 41 0 5632 0
vsize: 22692
[startup+90.0074 s]
Raw data (loadavg): 0.96 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 6093 0 0 0 8979 18 0 0 25 0 1 0 481127786 26865664 6071 4294967295 134512640 134672761 3221224560 3221223664 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6559 6071 603 41 0 6518 0
vsize: 26236
[startup+100.008 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 6413 0 0 0 9979 19 0 0 25 0 1 0 481127786 28303360 6391 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6910 6391 603 41 0 6869 0
vsize: 27640
[startup+110.009 s]
Raw data (loadavg): 0.97 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 6718 0 0 0 10976 21 0 0 25 0 1 0 481127786 29511680 6696 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7205 6696 603 41 0 7164 0
vsize: 28820
[startup+120.01 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 7180 0 0 0 11975 22 0 0 25 0 1 0 481127786 31510528 7158 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7693 7158 603 41 0 7652 0
vsize: 30772
[startup+130.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 7532 0 0 0 12975 23 0 0 25 0 1 0 481127786 32849920 7510 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8020 7510 603 41 0 7979 0
vsize: 32080
[startup+140.011 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 7948 0 0 0 13973 24 0 0 25 0 1 0 481127786 34590720 7926 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8445 7926 603 41 0 8404 0
vsize: 33780
[startup+150.012 s]
Raw data (loadavg): 0.98 0.95 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8493 0 0 0 14972 26 0 0 25 0 1 0 481127786 36732928 8471 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8968 8471 603 41 0 8927 0
vsize: 35872
[startup+160.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 15971 27 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+170.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 16971 27 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+180.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 17970 28 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+190.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 18970 28 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223744 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+200.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 19969 29 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+210.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 20969 29 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+220.018 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 21970 29 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223664 134555091 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+230.019 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 8902 0 0 0 22970 29 0 0 25 0 1 0 481127786 38461440 8880 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9390 8880 603 41 0 9349 0
vsize: 37560
[startup+240.02 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 9132 0 0 0 23970 29 0 0 25 0 1 0 481127786 39391232 9110 4294967295 134512640 134672761 3221224560 3221223728 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9617 9110 603 41 0 9576 0
vsize: 38468
[startup+250.021 s]
Raw data (loadavg): 0.99 0.96 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 9516 0 0 0 24969 30 0 0 25 0 1 0 481127786 41009152 9494 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10012 9494 603 41 0 9971 0
vsize: 40048
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 9875 0 0 0 25968 31 0 0 25 0 1 0 481127786 42475520 9853 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10370 9853 603 41 0 10329 0
vsize: 41480
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 10278 0 0 0 26967 32 0 0 25 0 1 0 481127786 44089344 10256 4294967295 134512640 134672761 3221224560 3221223728 134561018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10764 10256 603 41 0 10723 0
vsize: 43056
[startup+280.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 10688 0 0 0 27967 33 0 0 25 0 1 0 481127786 45948928 10666 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11218 10666 603 41 0 11177 0
vsize: 44872
[startup+290.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 11215 0 0 0 28966 34 0 0 25 0 1 0 481127786 48087040 11193 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11740 11193 603 41 0 11699 0
vsize: 46960
[startup+300.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 11618 0 0 0 29965 35 0 0 25 0 1 0 481127786 49836032 11596 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12167 11596 603 41 0 12126 0
vsize: 48668
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 12043 0 0 0 30963 37 0 0 25 0 1 0 481127786 51445760 12021 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12560 12021 603 41 0 12519 0
vsize: 50240
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 12464 0 0 0 31963 38 0 0 25 0 1 0 481127786 53202944 12442 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12989 12442 603 41 0 12948 0
vsize: 51956
[startup+330.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 12816 0 0 0 32961 39 0 0 25 0 1 0 481127786 54677504 12794 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13349 12794 603 41 0 13308 0
vsize: 53396
[startup+340.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 13154 0 0 0 33960 41 0 0 25 0 1 0 481127786 56012800 13132 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13675 13132 603 41 0 13634 0
vsize: 54700
[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 13415 0 0 0 34959 42 0 0 25 0 1 0 481127786 57081856 13393 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13936 13393 603 41 0 13895 0
vsize: 55744
[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 13722 0 0 0 35959 42 0 0 25 0 1 0 481127786 58286080 13700 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13700 603 41 0 14189 0
vsize: 56920
[startup+370.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14055 0 0 0 36958 44 0 0 25 0 1 0 481127786 59760640 14033 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14590 14033 603 41 0 14549 0
vsize: 58360
[startup+380.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 37958 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+390.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 38957 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+400.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 39957 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+410.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 40957 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223664 134560303 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+420.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 41958 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+430.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 42958 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 43958 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+450.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 44958 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+460.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 45959 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+470.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 46959 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+480.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 47958 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+490.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/53 14450
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 48959 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+500.044 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 14484
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 49959 44 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+510.045 s]
Raw data (loadavg): 1.07 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 50957 46 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+520.045 s]
Raw data (loadavg): 1.06 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 51957 46 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+530.046 s]
Raw data (loadavg): 1.05 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 52957 46 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+540.047 s]
Raw data (loadavg): 1.04 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 53957 46 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223664 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+550.048 s]
Raw data (loadavg): 1.03 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 54958 46 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+560.049 s]
Raw data (loadavg): 1.03 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14222 0 0 0 55957 46 0 0 25 0 1 0 481127786 60387328 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14743 14200 603 41 0 14702 0
vsize: 58972
[startup+570.05 s]
Raw data (loadavg): 1.02 0.99 0.92 2/53 14503
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14566 0 0 0 56955 47 0 0 25 0 1 0 481127786 61726720 14544 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15070 14544 603 41 0 15029 0
vsize: 60280
[startup+580.051 s]
Raw data (loadavg): 1.02 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 14898 0 0 0 57954 48 0 0 25 0 1 0 481127786 63205376 14876 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15431 14876 603 41 0 15390 0
vsize: 61724
[startup+590.053 s]
Raw data (loadavg): 1.02 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 15246 0 0 0 58954 49 0 0 25 0 1 0 481127786 64536576 15224 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15756 15224 603 41 0 15715 0
vsize: 63024
[startup+600.053 s]
Raw data (loadavg): 1.01 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 15618 0 0 0 59953 50 0 0 25 0 1 0 481127786 66146304 15596 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16149 15596 603 41 0 16108 0
vsize: 64596
[startup+610.054 s]
Raw data (loadavg): 1.01 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 15995 0 0 0 60953 51 0 0 25 0 1 0 481127786 67629056 15973 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16511 15973 603 41 0 16470 0
vsize: 66044
[startup+620.055 s]
Raw data (loadavg): 1.01 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 16228 0 0 0 61952 52 0 0 25 0 1 0 481127786 68567040 16206 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16740 16206 603 41 0 16699 0
vsize: 66960
[startup+630.056 s]
Raw data (loadavg): 1.01 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 16480 0 0 0 62951 53 0 0 25 0 1 0 481127786 69648384 16458 4294967295 134512640 134672761 3221224560 3221223616 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17004 16458 603 41 0 16963 0
vsize: 68016
[startup+640.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 16776 0 0 0 63950 54 0 0 25 0 1 0 481127786 70856704 16754 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17299 16754 603 41 0 17258 0
vsize: 69196
[startup+650.057 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17116 0 0 0 64950 54 0 0 25 0 1 0 481127786 72179712 17094 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17622 17094 603 41 0 17581 0
vsize: 70488
[startup+660.058 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17431 0 0 0 65949 55 0 0 25 0 1 0 481127786 73510912 17409 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17947 17409 603 41 0 17906 0
vsize: 71788
[startup+670.06 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17742 0 0 0 66949 56 0 0 25 0 1 0 481127786 74842112 17720 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18272 17720 603 41 0 18231 0
vsize: 73088
[startup+680.061 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 67947 57 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+690.062 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 68947 57 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+700.063 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 69947 57 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134564457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+710.064 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 70948 57 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+720.065 s]
Raw data (loadavg): 1.00 0.99 0.92 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 71948 57 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+730.065 s]
Raw data (loadavg): 1.08 1.00 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 72948 57 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+740.066 s]
Raw data (loadavg): 1.14 1.02 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 73948 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+750.067 s]
Raw data (loadavg): 1.12 1.02 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 74948 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+760.068 s]
Raw data (loadavg): 1.10 1.02 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 75948 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+770.068 s]
Raw data (loadavg): 1.08 1.02 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 76949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223664 134560139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+780.069 s]
Raw data (loadavg): 1.07 1.02 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 77949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223696 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+790.071 s]
Raw data (loadavg): 1.06 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 78949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+800.072 s]
Raw data (loadavg): 1.05 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 79949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+810.072 s]
Raw data (loadavg): 1.04 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 80949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+820.073 s]
Raw data (loadavg): 1.04 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 81949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+830.074 s]
Raw data (loadavg): 1.03 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 82949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+840.075 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 83949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+850.076 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 84949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+860.077 s]
Raw data (loadavg): 1.02 1.01 0.93 2/53 14505
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 85950 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+870.078 s]
Raw data (loadavg): 1.01 1.01 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 86949 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+880.079 s]
Raw data (loadavg): 1.01 1.01 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 87950 58 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+890.079 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 88950 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+900.079 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 89950 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+910.08 s]
Raw data (loadavg): 1.01 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 90950 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+920.081 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 91950 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223696 134560590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+930.082 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 92950 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+940.081 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 93951 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+950.082 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 94951 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+960.083 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 95951 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+970.085 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17873 0 0 0 96951 59 0 0 25 0 1 0 481127786 75243520 17851 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17851 603 41 0 18329 0
vsize: 73480
[startup+980.085 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17874 0 0 0 97952 59 0 0 25 0 1 0 481127786 75243520 17852 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17852 603 41 0 18329 0
vsize: 73480
[startup+990.086 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17875 0 0 0 98952 59 0 0 25 0 1 0 481127786 75243520 17853 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17853 603 41 0 18329 0
vsize: 73480
[startup+1000.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 99951 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1010.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 100952 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1020.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 101952 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1030.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 102952 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1040.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 103952 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1050.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 104952 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1060.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 105953 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1070.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 106953 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1080.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 107953 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1090.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 108953 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1100.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 109953 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1110.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 110954 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560979 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1120.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 111954 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1130.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 112953 59 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1140.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 113953 60 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1150.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 114953 60 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1160.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 115954 60 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1170.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 116954 60 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1180.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 117954 60 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1190.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17876 0 0 0 118954 60 0 0 25 0 1 0 481127786 75243520 17854 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17854 603 41 0 18329 0
vsize: 73480
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 2/53 14507
Raw data (stat): 14450 (minisat+) R 14449 7987 7986 0 -1 0 17877 0 0 0 119955 60 0 0 25 0 1 0 481127786 75243520 17855 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18370 17855 603 41 0 18329 0
vsize: 73480
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 1.00 1.00 0.93 1/53 14507
Raw data (stat): 14450 (minisat+) Z 14449 7987 7986 0 -1 12 17880 0 0 0 119955 63 0 0 24 0 1 0 481127786 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.15
CPU time (s): 1200.19
CPU user time (s): 1199.55
CPU system time (s): 0.636903
CPU usage (%): 100.003
Max. virtual memory (Kb): 73480
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####