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-5.opb
MD5SUM	7850e0b228f4ef5ee038a9c3595683ab
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	58579
Number of constraints which are clauses	58579
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 5250

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-04-13 22:56:38 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3717 boxname=wulflinc4 idbench=333 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  7850e0b228f4ef5ee038a9c3595683ab  /oldhome/oroussel/tmp/wulflinc4/normalized-frb45-21-5.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc4/normalized-frb45-21-5.opb /oldhome/oroussel/tmp/wulflinc4/normalized-frb45-21-5.opb
IDLAUNCH: 3717
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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	: 890.88

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        907488 kB
Buffers:         34728 kB
Cached:          72576 kB
SwapCached:          0 kB
Active:          54008 kB
Inactive:        56160 kB
HighTotal:      131008 kB
HighFree:        54656 kB
LowTotal:       903652 kB
LowFree:        852832 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11444 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-13 23:16:40 (client local time) WITH STATUS 10 IN 1200.24 SECONDS
stats: 3717 7 1200.24 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58579 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 |   58579   117158 |   19526       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1869   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71493   163298 |   23831       0        0     nan |  0.000 % |
c |       100 |   71493   163298 |   26214     100      783     7.8 |  0.074 % |
c |       250 |   71466   163205 |   28835     236     2267     9.6 |  0.180 % |
c |       475 |   71439   163112 |   31719     451     5319    11.8 |  0.285 % |
c |       813 |   71421   163050 |   34890     785     8876    11.3 |  0.357 % |
c |      1319 |   71361   162844 |   38380    1275    14155    11.1 |  0.607 % |
c |      2079 |   71310   162669 |   42218    2020    23562    11.7 |  0.821 % |
c |      3218 |   71123   162024 |   46439    3106    42751    13.8 |  1.641 % |
c |      4926 |   70701   160580 |   51083    4704    71827    15.3 |  3.532 % |
c |      7488 |   69856   157673 |   56192    7023   116766    16.6 |  7.991 % |
c |     11332 |   68840   154167 |   61811   10339   223852    21.7 | 13.557 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 34   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14466 |   67964   151140 |   22654   12991   378752    29.2 | 13.557 % |
c |     14566 |   67931   151023 |   24919   13071   380846    29.1 | 19.180 % |
c |     14716 |   67889   150877 |   27411   13206   383860    29.1 | 19.465 % |
c |     14941 |   67700   150224 |   30152   13321   389729    29.3 | 20.606 % |
c |     15278 |   67627   149971 |   33167   13587   400955    29.5 | 21.034 % |
c |     15784 |   67500   149526 |   36484   14036   419304    29.9 | 21.925 % |
c |     16543 |   67319   148895 |   40132   14714   459281    31.2 | 23.173 % |
c |     17682 |   67204   148496 |   44146   15771   542300    34.4 | 23.957 % |
c |     19390 |   66746   146896 |   48560   17197   618162    35.9 | 27.132 % |
c |     21952 |   66617   146449 |   53416   19579   735834    37.6 | 27.988 % |
c |     25796 |   66587   146347 |   58758   23281  1331984    57.2 | 28.128 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     27975 |   66460   145905 |   22153   25333  1434849    56.6 | 28.128 % |
c |     28078 |   66441   145838 |   24368   12766   885083    69.3 | 29.154 % |
c |     28228 |   66441   145838 |   26805   12916   890705    69.0 | 29.154 % |
c |     28453 |   66441   145838 |   29485   13141   897090    68.3 | 29.152 % |
c |     28790 |   66441   145838 |   32434   13478   923024    68.5 | 29.152 % |
c |     29296 |   66432   145807 |   35677   13981   942770    67.4 | 29.187 % |
c |     30055 |   66345   145506 |   39245   14675   981619    66.9 | 29.724 % |
c |     31195 |   66256   145197 |   43169   15764  1036366    65.7 | 30.330 % |
c |     32904 |   66188   144965 |   47486   17420  1158552    66.5 | 30.793 % |
c |     35466 |   66147   144820 |   52235   19945  1342554    67.3 | 31.076 % |
c |     39311 |   66124   144737 |   57459   23785  1961080    82.5 | 31.290 % |
c |     45078 |   66124   144737 |   63205   29552  2909536    98.5 | 31.293 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 36   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     48483 |   66029   144411 |   22009   32887  3130406    95.2 | 31.293 % |
c |     48583 |   66023   144391 |   24209   15385  1607142   104.5 | 32.134 % |
c |     48733 |   65966   144188 |   26630   15526  1611952   103.8 | 32.597 % |
c |     48958 |   65966   144188 |   29293   15751  1621800   103.0 | 32.599 % |
c |     49297 |   65966   144188 |   32223   16090  1639515   101.9 | 32.597 % |
c |     49803 |   65966   144188 |   35445   16596  1659957   100.0 | 32.597 % |
c |     50563 |   65957   144157 |   38990   17346  1730858    99.8 | 32.635 % |
c |     51703 |   65885   143899 |   42889   18440  1781585    96.6 | 33.167 % |
c |     53411 |   65876   143868 |   47178   20137  1941581    96.4 | 33.205 % |
c |     55973 |   65855   143793 |   51896   22695  2120780    93.4 | 33.383 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 37   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     57390 |   65812   143648 |   21937   24078  2212705    91.9 | 33.383 % |
c |     57491 |   65812   143648 |   24130   12140   633424    52.2 | 33.689 % |
c |     57641 |   65812   143648 |   26543   12290   643714    52.4 | 33.692 % |
c |     57866 |   65812   143648 |   29198   12515   650601    52.0 | 33.691 % |
c |     58203 |   65812   143648 |   32117   12852   676169    52.6 | 33.689 % |
c |     58709 |   65812   143648 |   35329   13358   697519    52.2 | 33.690 % |
c |     59468 |   65782   143540 |   38862   14089   739892    52.5 | 33.869 % |
c |     60610 |   65782   143540 |   42749   15231   844153    55.4 | 33.869 % |
c |     62318 |   65764   143478 |   47023   16915   917388    54.2 | 33.939 % |
c |     64881 |   65743   143403 |   51726   19475  1125867    57.8 | 34.117 % |
c |     68725 |   65743   143403 |   56898   23319  1556441    66.7 | 34.117 % |
c |     74491 |   65743   143403 |   62588   29085  2129648    73.2 | 34.117 % |
c |     83141 |   65729   143353 |   68847   37715  2663458    70.6 | 34.190 % |
c |     96115 |   65729   143353 |   75732   50689  4524473    89.3 | 34.188 % |
c |    115576 |   65675   143161 |   83305   70120  6071336    86.6 | 34.689 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 38   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    127181 |   65670   143149 |   21890   81716  7132900    87.3 | 34.689 % |
c |    127281 |   65670   143149 |   24079   17363  1188120    68.4 | 34.747 % |
c |    127432 |   65670   143149 |   26486   17514  1199567    68.5 | 34.748 % |
c |    127657 |   65630   143011 |   29135   17728  1202086    67.8 | 34.995 % |
c |    127995 |   65630   143011 |   32049   18066  1219508    67.5 | 34.997 % |
c |    128503 |   65630   143011 |   35254   18574  1233432    66.4 | 34.996 % |
c |    129262 |   65630   143011 |   38779   19333  1282443    66.3 | 34.995 % |
c |    130401 |   65630   143011 |   42657   20472  1352836    66.1 | 34.995 % |
c |    132111 |   65614   142957 |   46923   22174  1470176    66.3 | 35.137 % |
c |    134673 |   65614   142957 |   51615   24736  1641021    66.3 | 35.137 % |
c |    138517 |   65614   142957 |   56777   28580  1961237    68.6 | 35.139 % |
c |    144283 |   65614   142957 |   62454   34346  2701123    78.6 | 35.137 % |
c |    152932 |   65592   142879 |   68700   42968  3224087    75.0 | 35.279 % |
c |    165908 |   65567   142792 |   75570   55935  4717560    84.3 | 35.457 % |
c |    185369 |   65567   142792 |   83127   75396  6222560    82.5 | 35.460 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 39   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    205519 |   65562   142777 |   21854   28126  2376584    84.5 | 35.460 % |
c |    205619 |   65562   142777 |   24039   14163  1194421    84.3 | 35.516 % |
c |    205770 |   65562   142777 |   26443   14314  1196367    83.6 | 35.516 % |
c |    205995 |   65553   142746 |   29087   14532  1200161    82.6 | 35.552 % |
c |    206335 |   65553   142746 |   31996   14872  1216803    81.8 | 35.552 % |
c |    206842 |   65553   142746 |   35196   15379  1238228    80.5 | 35.552 % |
c |    207601 |   65553   142746 |   38715   16138  1312285    81.3 | 35.552 % |
c |    208740 |   65553   142746 |   42587   17277  1386715    80.3 | 35.552 % |
c |    210449 |   65553   142746 |   46845   18986  1473624    77.6 | 35.552 % |
c |    213011 |   65553   142746 |   51530   21548  1589589    73.8 | 35.552 % |
c |    216856 |   65553   142746 |   56683   25393  1915010    75.4 | 35.552 % |
c |    222622 |   65553   142746 |   62352   31159  2432965    78.1 | 35.552 % |
c |    231271 |   65553   142746 |   68587   39808  3284858    82.5 | 35.552 % |
c |    244246 |   65553   142746 |   75445   52783  4986519    94.5 | 35.552 % |
c |    263707 |   65553   142746 |   82990   72244  7050290    97.6 | 35.552 % |
c |    292899 |   65553   142746 |   91289   33537  2691713    80.3 | 35.554 % |
c |    336688 |   65553   142746 |  100418   77326  6370922    82.4 | 35.552 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 40   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    377826 |   65556   142760 |   21852   32830  3209384    97.8 | 35.552 % |
c |    377927 |   65556   142760 |   24037   15708  1367144    87.0 | 35.577 % |
c |    378077 |   65556   142760 |   26440   15858  1374799    86.7 | 35.575 % |
c |    378302 |   65556   142760 |   29085   16083  1381157    85.9 | 35.575 % |
c |    378639 |   65556   142760 |   31993   16420  1402997    85.4 | 35.577 % |
c |    379145 |   65556   142760 |   35192   16926  1419863    83.9 | 35.575 % |
c |    379904 |   65556   142760 |   38712   17685  1447082    81.8 | 35.575 % |
c |    381045 |   65556   142760 |   42583   18826  1487174    79.0 | 35.575 % |
c |    382754 |   65550   142740 |   46841   20523  1597802    77.9 | 35.610 % |
c |    385317 |   65550   142740 |   51525   23086  1837672    79.6 | 35.612 % |
c |    389161 |   65550   142740 |   56678   26930  2062525    76.6 | 35.610 % |
c |    394928 |   65550   142740 |   62346   32697  2710559    82.9 | 35.612 % |
c |    403577 |   65550   142740 |   68580   41346  3596597    87.0 | 35.610 % |
c |    416552 |   65550   142740 |   75439   54321  4910274    90.4 | 35.610 % |
c |    436014 |   65544   142720 |   82982   73782  6523525    88.4 | 35.646 % |
c |    465207 |   65544   142720 |   91281   35324  1883420    53.3 | 35.648 % |
c |    508996 |   65538   142700 |  100409   79108  6108979    77.2 | 35.681 % |
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.91 0.95 0.90 2/54 9922
Raw data (stat): 9922 (runsolver) R 9921 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 421496197 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 2919 0 0 0 990 8 0 0 25 0 1 0 421496197 13672448 2897 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3338 2897 603 41 0 3297 0
vsize: 13352
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 2919 0 0 0 1990 8 0 0 25 0 1 0 421496197 13672448 2897 4294967295 134512640 134672761 3221224560 3221223664 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3338 2897 603 41 0 3297 0
vsize: 13352
[startup+30.0022 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 2919 0 0 0 2989 8 0 0 25 0 1 0 421496197 13672448 2897 4294967295 134512640 134672761 3221224560 3221223560 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3338 2897 603 41 0 3297 0
vsize: 13352
[startup+40.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 3208 0 0 0 3988 9 0 0 25 0 1 0 421496197 14884864 3186 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3634 3186 603 41 0 3593 0
vsize: 14536
[startup+50.0023 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 4413 0 0 0 4984 13 0 0 25 0 1 0 421496197 19861504 4391 4294967295 134512640 134672761 3221224560 3221223684 134566018 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4849 4391 603 41 0 4808 0
vsize: 19396
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 4827 0 0 0 5983 14 0 0 25 0 1 0 421496197 21598208 4805 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5273 4805 603 41 0 5232 0
vsize: 21092
[startup+70.0033 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 4827 0 0 0 6983 15 0 0 25 0 1 0 421496197 21598208 4805 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5273 4805 603 41 0 5232 0
vsize: 21092
[startup+80.0028 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 4827 0 0 0 7983 15 0 0 25 0 1 0 421496197 21598208 4805 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5273 4805 603 41 0 5232 0
vsize: 21092
[startup+90.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 4828 0 0 0 8983 15 0 0 25 0 1 0 421496197 21598208 4806 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5273 4806 603 41 0 5232 0
vsize: 21092
[startup+100.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 4909 0 0 0 9983 15 0 0 25 0 1 0 421496197 21999616 4887 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5371 4887 603 41 0 5330 0
vsize: 21484
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 5611 0 0 0 10981 17 0 0 25 0 1 0 421496197 24817664 5589 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6059 5589 603 41 0 6018 0
vsize: 24236
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 6297 0 0 0 11979 19 0 0 25 0 1 0 421496197 27639808 6275 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6748 6275 603 41 0 6707 0
vsize: 26992
[startup+130.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 6677 0 0 0 12979 19 0 0 25 0 1 0 421496197 29118464 6655 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7109 6655 603 41 0 7068 0
vsize: 28436
[startup+140.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 7005 0 0 0 13978 20 0 0 25 0 1 0 421496197 30466048 6983 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7438 6983 603 41 0 7397 0
vsize: 29752
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 7312 0 0 0 14977 21 0 0 25 0 1 0 421496197 31797248 7290 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7763 7290 603 41 0 7722 0
vsize: 31052
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 7679 0 0 0 15977 22 0 0 25 0 1 0 421496197 33525760 7657 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8185 7657 603 41 0 8144 0
vsize: 32740
[startup+170.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 8055 0 0 0 16975 24 0 0 25 0 1 0 421496197 34992128 8033 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8543 8033 603 41 0 8502 0
vsize: 34172
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 8426 0 0 0 17974 25 0 0 25 0 1 0 421496197 36462592 8404 4294967295 134512640 134672761 3221224560 3221223696 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8902 8404 603 41 0 8861 0
vsize: 35608
[startup+190.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 8786 0 0 0 18973 27 0 0 25 0 1 0 421496197 37933056 8764 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9261 8764 603 41 0 9220 0
vsize: 37044
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 9922
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9190 0 0 0 19972 28 0 0 25 0 1 0 421496197 39661568 9168 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9683 9168 603 41 0 9642 0
vsize: 38732
[startup+210.04 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 9966
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9312 0 0 0 20975 28 0 0 25 0 1 0 421496197 40062976 9290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9290 603 41 0 9740 0
vsize: 39124
[startup+220.041 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9312 0 0 0 21975 28 0 0 25 0 1 0 421496197 40062976 9290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9290 603 41 0 9740 0
vsize: 39124
[startup+230.041 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9312 0 0 0 22975 28 0 0 25 0 1 0 421496197 40062976 9290 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9290 603 41 0 9740 0
vsize: 39124
[startup+240.041 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9312 0 0 0 23975 28 0 0 25 0 1 0 421496197 40062976 9290 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9290 603 41 0 9740 0
vsize: 39124
[startup+250.041 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9312 0 0 0 24975 28 0 0 25 0 1 0 421496197 40062976 9290 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9290 603 41 0 9740 0
vsize: 39124
[startup+260.042 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 25976 28 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+270.043 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 26976 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+280.042 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 9975
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 27976 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+290.043 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 28976 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+300.043 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 29976 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+310.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 30976 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+320.043 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 31976 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+330.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9313 0 0 0 32977 29 0 0 25 0 1 0 421496197 40062976 9291 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9291 603 41 0 9740 0
vsize: 39124
[startup+340.044 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9314 0 0 0 33977 29 0 0 25 0 1 0 421496197 40062976 9292 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9781 9292 603 41 0 9740 0
vsize: 39124
[startup+350.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 34976 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134561533 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+360.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 35977 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+370.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 36977 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+380.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 37977 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+390.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 38977 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+400.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 39977 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+410.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 40977 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+420.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 41978 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+430.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 42978 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+440.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9510 0 0 0 43978 29 0 0 25 0 1 0 421496197 40853504 9488 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9488 603 41 0 9933 0
vsize: 39896
[startup+450.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9511 0 0 0 44978 29 0 0 25 0 1 0 421496197 40853504 9489 4294967295 134512640 134672761 3221224560 3221223760 134557842 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9489 603 41 0 9933 0
vsize: 39896
[startup+460.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9511 0 0 0 45978 29 0 0 25 0 1 0 421496197 40853504 9489 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9974 9489 603 41 0 9933 0
vsize: 39896
[startup+470.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9589 0 0 0 46978 30 0 0 25 0 1 0 421496197 41259008 9567 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10073 9567 603 41 0 10032 0
vsize: 40292
[startup+480.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 9857 0 0 0 47978 31 0 0 25 0 1 0 421496197 42328064 9835 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10334 9835 603 41 0 10293 0
vsize: 41336
[startup+490.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10080 0 0 0 48977 32 0 0 25 0 1 0 421496197 43257856 10058 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10561 10058 603 41 0 10520 0
vsize: 42244
[startup+500.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10326 0 0 0 49976 33 0 0 25 0 1 0 421496197 44318720 10304 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10820 10304 603 41 0 10779 0
vsize: 43280
[startup+510.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 50976 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+520.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 51976 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+530.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 52976 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+540.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 53976 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+550.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 54976 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+560.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 55976 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+570.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9977
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 56977 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+580.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 57977 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+590.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 58977 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+600.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 59977 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+610.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10486 0 0 0 60977 33 0 0 25 0 1 0 421496197 44974080 10464 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10464 603 41 0 10939 0
vsize: 43920
[startup+620.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10491 0 0 0 61977 33 0 0 25 0 1 0 421496197 44974080 10469 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10469 603 41 0 10939 0
vsize: 43920
[startup+630.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10492 0 0 0 62978 33 0 0 25 0 1 0 421496197 44974080 10470 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10470 603 41 0 10939 0
vsize: 43920
[startup+640.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10493 0 0 0 63978 33 0 0 25 0 1 0 421496197 44974080 10471 4294967295 134512640 134672761 3221224560 3221223664 134560347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10471 603 41 0 10939 0
vsize: 43920
[startup+650.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10493 0 0 0 64978 33 0 0 25 0 1 0 421496197 44974080 10471 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10471 603 41 0 10939 0
vsize: 43920
[startup+660.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10493 0 0 0 65978 33 0 0 25 0 1 0 421496197 44974080 10471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10980 10471 603 41 0 10939 0
vsize: 43920
[startup+670.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10493 0 0 0 66978 33 0 0 25 0 1 0 421496197 44974080 10471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10471 603 41 0 10939 0
vsize: 43920
[startup+680.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10493 0 0 0 67978 33 0 0 25 0 1 0 421496197 44974080 10471 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10471 603 41 0 10939 0
vsize: 43920
[startup+690.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10494 0 0 0 68978 33 0 0 25 0 1 0 421496197 44974080 10472 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10980 10472 603 41 0 10939 0
vsize: 43920
[startup+700.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 10723 0 0 0 69978 34 0 0 25 0 1 0 421496197 45903872 10701 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11207 10701 603 41 0 11166 0
vsize: 44828
[startup+710.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 11033 0 0 0 70977 35 0 0 25 0 1 0 421496197 47108096 11011 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11501 11011 603 41 0 11460 0
vsize: 46004
[startup+720.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 11342 0 0 0 71977 35 0 0 25 0 1 0 421496197 48435200 11320 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11825 11320 603 41 0 11784 0
vsize: 47300
[startup+730.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 11683 0 0 0 72976 36 0 0 25 0 1 0 421496197 49766400 11661 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12150 11661 603 41 0 12109 0
vsize: 48600
[startup+740.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 73975 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223664 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+750.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 74976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+760.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 75976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+770.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 76976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+780.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 77976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+790.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 78976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+800.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 79976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+810.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 80976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+820.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 81976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+830.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 82976 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+840.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 83977 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+850.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 84977 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+860.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 85977 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+870.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 86977 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+880.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 87977 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134559675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+890.062 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 88978 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+900.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 89978 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+910.063 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 90978 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+920.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 91978 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223664 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+930.064 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 92978 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+940.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 93979 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+950.065 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 94979 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+960.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 95979 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+970.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 96979 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+980.066 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 97979 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+990.067 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 98980 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 99980 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 100980 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 101980 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 102980 37 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1040.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 103980 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1050.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 104980 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1060.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 105980 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1070.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 106981 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1080.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 107981 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 108981 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 109981 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 110982 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12040 0 0 0 111982 38 0 0 25 0 1 0 421496197 51228672 12018 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12018 603 41 0 12466 0
vsize: 50028
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 112982 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223664 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 113982 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 114982 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 115982 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 116983 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 117983 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 118983 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 9979
Raw data (stat): 9922 (minisat+) R 9921 5897 5896 0 -1 0 12041 0 0 0 119983 38 0 0 25 0 1 0 421496197 51228672 12019 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12507 12019 603 41 0 12466 0
vsize: 50028
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 9979
Raw data (stat): 9922 (minisat+) Z 9921 5897 5896 0 -1 12 12044 0 0 0 119983 40 0 0 25 0 1 0 421496197 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.1
CPU time (s): 1200.24
CPU user time (s): 1199.84
CPU system time (s): 0.404938
CPU usage (%): 100.012
Max. virtual memory (Kb): 50028
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####