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-3.opb
MD5SUM	b3a3f977e810fc2043ea057a8d94a7d8
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	-34
Optimality of the best value was proved	NO
Number of terms in the objective function	945
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	945
Number of bits of the sum of numbers in the objective function	10
Biggest number in a constraint	1
Number of bits of the biggest number in a constraint	1
Biggest sum of numbers in a constraint	945
Number of bits of the biggest sum of numbers	10
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.07
Number of variables	945
Total number of constraints	58245
Number of constraints which are clauses	58245
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 5248

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898540 kB
Buffers:         33524 kB
Cached:          67692 kB
SwapCached:         36 kB
Active:          47272 kB
Inactive:        56864 kB
HighTotal:      131008 kB
HighFree:        59472 kB
LowTotal:       903652 kB
LowFree:        839068 kB
SwapTotal:     2097892 kB
SwapFree:      2097856 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            26336 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:15:29 (client local time) WITH STATUS 10 IN 1200.16 SECONDS
stats: 3715 7 1200.16 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58245 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 |   58245   116490 |   19415       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1856   maxlim: 29   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   70928   161846 |   23642       0        0     nan |  0.000 % |
c |       100 |   70901   161753 |   26006      91      680     7.5 |  0.252 % |
c |       251 |   70892   161722 |   28606     240     1963     8.2 |  0.288 % |
c |       476 |   70874   161660 |   31467     461     5229    11.3 |  0.360 % |
c |       813 |   70838   161536 |   34614     789     9149    11.6 |  0.504 % |
c |      1319 |   70814   161454 |   38075    1291    15661    12.1 |  0.614 % |
c ==============================================================================
c [1mFound solution: -30[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1970 |   70821   161483 |   23607    1942    27269    14.0 |  0.614 % |
c |      2070 |   70821   161483 |   25967    2042    27843    13.6 |  0.648 % |
c |      2220 |   70812   161452 |   28564    2190    29307    13.4 |  0.686 % |
c |      2445 |   70794   161390 |   31420    2411    31405    13.0 |  0.758 % |
c |      2783 |   70734   161184 |   34563    2736    36318    13.3 |  1.008 % |
c |      3289 |   70707   161091 |   38019    3236    43747    13.5 |  1.116 % |
c |      4048 |   70618   160784 |   41821    3961    52644    13.3 |  1.511 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 31   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      4918 |   70517   160429 |   23505    4794    68011    14.2 |  1.511 % |
c |      5018 |   70491   160339 |   25855    4887    71154    14.6 |  2.087 % |
c |      5168 |   70491   160339 |   28441    5037    73442    14.6 |  2.087 % |
c |      5393 |   70447   160187 |   31285    5252    76775    14.6 |  2.305 % |
c ==============================================================================
c [1mFound solution: -32[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 41   maxlim: 32   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      5415 |   70691   161048 |   23563    5274    77456    14.7 |  2.305 % |
c |      5515 |   70649   160904 |   25919    5365    78848    14.7 |  2.527 % |
c |      5666 |   70640   160873 |   28511    5505    81444    14.8 |  2.565 % |
c |      5891 |   70563   160608 |   31362    5695    84349    14.8 |  2.918 % |
c |      6228 |   70405   160068 |   34498    5986    89984    15.0 |  3.665 % |
c |      6734 |   70339   159846 |   37948    6471   101347    15.7 |  4.021 % |
c |      7493 |   70127   159120 |   41743    7142   117358    16.4 |  4.982 % |
c |      8632 |   69916   158393 |   45917    8208   141398    17.2 |  6.050 % |
c |     10341 |   69490   156927 |   50509    9768   188069    19.3 |  8.259 % |
c |     12903 |   69002   155251 |   55560   12205   381231    31.2 | 10.925 % |
c |     16748 |   67741   150886 |   61116   15545   549382    35.3 | 18.683 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19625 |   67189   148972 |   22396   17966   656669    36.6 | 18.683 % |
c |     19726 |   67133   148780 |   24635   17938   657528    36.7 | 22.415 % |
c |     19876 |   67058   148519 |   27099   18059   660999    36.6 | 22.946 % |
c |     20101 |   67058   148519 |   29809   18284   670164    36.7 | 22.946 % |
c |     20439 |   67020   148385 |   32789   18609   681711    36.6 | 23.233 % |
c |     20945 |   66836   147751 |   36068   18785   692605    36.9 | 24.297 % |
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 |     21425 |   66775   147543 |   22258   19214   727105    37.8 | 24.297 % |
c |     21525 |   66744   147436 |   24483   19296   731633    37.9 | 24.931 % |
c |     21676 |   66733   147397 |   26932   19406   737828    38.0 | 25.000 % |
c |     21901 |   66733   147397 |   29625   19631   753571    38.4 | 25.002 % |
c |     22238 |   66678   147208 |   32587   19865   766069    38.6 | 25.320 % |
c |     22744 |   66645   147095 |   35846   20259   797771    39.4 | 25.462 % |
c |     23503 |   66565   146815 |   39431   20954   848059    40.5 | 26.031 % |
c |     24644 |   66565   146815 |   43374   22095   928818    42.0 | 26.031 % |
c |     26355 |   66460   146458 |   47711   23678  1040667    44.0 | 26.743 % |
c |     28918 |   66307   145923 |   52483   26088  1210830    46.4 | 27.774 % |
c |     32762 |   66191   145515 |   57731   29888  1584436    53.0 | 28.701 % |
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 |     36593 |   66193   145529 |   22064   33719  2052930    60.9 | 28.701 % |
c |     36693 |   66193   145529 |   24270   15561  1113016    71.5 | 28.749 % |
c |     36844 |   66193   145529 |   26697   15712  1126520    71.7 | 28.751 % |
c |     37069 |   66193   145529 |   29367   15937  1139850    71.5 | 28.749 % |
c |     37406 |   66193   145529 |   32303   16274  1156240    71.0 | 28.752 % |
c |     37912 |   66125   145289 |   35534   16738  1186761    70.9 | 29.249 % |
c |     38673 |   66073   145111 |   39087   17461  1215106    69.6 | 29.569 % |
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 |     39718 |   66063   145079 |   22021   18488  1315488    71.2 | 29.569 % |
c |     39818 |   66063   145079 |   24223   18588  1317854    70.9 | 29.663 % |
c |     39969 |   66020   144926 |   26645   18670  1322840    70.9 | 29.982 % |
c |     40194 |   65890   144472 |   29309   18873  1333687    70.7 | 30.906 % |
c |     40531 |   65890   144472 |   32240   19210  1351085    70.3 | 30.906 % |
c |     41037 |   65796   144138 |   35465   19647  1374729    70.0 | 31.545 % |
c |     41799 |   65751   143977 |   39011   20390  1434093    70.3 | 31.903 % |
c |     42938 |   65596   143432 |   42912   21477  1508061    70.2 | 33.040 % |
c |     44646 |   65587   143401 |   47203   23169  1609194    69.5 | 33.073 % |
c |     47208 |   65587   143401 |   51924   25731  1971945    76.6 | 33.075 % |
c |     51053 |   65558   143296 |   57116   29507  2280769    77.3 | 33.288 % |
c |     56819 |   65558   143296 |   62828   35273  3075521    87.2 | 33.288 % |
c |     65468 |   65479   143017 |   69111   43869  4078245    93.0 | 33.927 % |
c |     78443 |   65426   142826 |   76022   56832  5588515    98.3 | 34.387 % |
c |     97904 |   65363   142615 |   83624   76187  8172274   107.3 | 34.849 % |
c |    127096 |   65363   142615 |   91987   36257  5030661   138.8 | 34.851 % |
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 |    159266 |   65359   142605 |   21786   68425 11254129   164.5 | 34.851 % |
c |    159367 |   65359   142605 |   23964   16130  2281264   141.4 | 34.895 % |
c |    159518 |   65321   142475 |   26361   16275  2283559   140.3 | 35.108 % |
c |    159743 |   65301   142405 |   28997   16492  2288407   138.8 | 35.215 % |
c |    160080 |   65301   142405 |   31896   16829  2302276   136.8 | 35.215 % |
c |    160586 |   65301   142405 |   35086   17335  2320172   133.8 | 35.215 % |
c |    161348 |   65301   142405 |   38595   18097  2352449   130.0 | 35.215 % |
c |    162487 |   65290   142366 |   42454   19215  2392320   124.5 | 35.286 % |
c |    164195 |   65290   142366 |   46700   20923  2484784   118.8 | 35.288 % |
c |    166758 |   65290   142366 |   51370   23486  2648614   112.8 | 35.286 % |
c |    170602 |   65290   142366 |   56507   27330  2929665   107.2 | 35.288 % |
c |    176368 |   65237   142177 |   62158   33071  3218415    97.3 | 35.676 % |
c |    185017 |   65237   142177 |   68373   41720  4200666   100.7 | 35.678 % |
c |    197992 |   65237   142177 |   75211   54695  5508019   100.7 | 35.676 % |
c |    217454 |   65220   142118 |   82732   74132  7066168    95.3 | 35.783 % |
c |    246646 |   65220   142118 |   91005   35759  3313448    92.7 | 35.785 % |
c |    290435 |   65220   142118 |  100106   79548  9302390   116.9 | 35.785 % |
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 |    330177 |   65221   142123 |   21740   34332  3878612   113.0 | 35.785 % |
c |    330278 |   65221   142123 |   23914   17164  1634871    95.2 | 35.807 % |
c |    330428 |   65221   142123 |   26305   17314  1637651    94.6 | 35.806 % |
c |    330653 |   65221   142123 |   28935   17539  1642554    93.7 | 35.806 % |
c |    330990 |   65221   142123 |   31829   17876  1658719    92.8 | 35.806 % |
c |    331496 |   65168   141940 |   35012   18377  1678775    91.4 | 36.231 % |
c |    332255 |   65168   141940 |   38513   19136  1722215    90.0 | 36.233 % |
c |    333394 |   65168   141940 |   42365   20275  1816218    89.6 | 36.231 % |
c |    335102 |   65168   141940 |   46601   21983  1976978    89.9 | 36.231 % |
c |    337665 |   65168   141940 |   51261   24546  2195280    89.4 | 36.231 % |
c |    341510 |   65168   141940 |   56387   28391  2500793    88.1 | 36.231 % |
c |    347277 |   65168   141940 |   62026   34158  3240167    94.9 | 36.231 % |
c |    355926 |   65168   141940 |   68229   42807  4299169   100.4 | 36.233 % |
c |    368901 |   65168   141940 |   75052   55782  5762096   103.3 | 36.231 % |
c |    388362 |   65168   141940 |   82557   75243  8158679   108.4 | 36.233 % |
c |    417554 |   65168   141940 |   90813   36459  4557610   125.0 | 36.231 % |
c |    461343 |   65153   141889 |   99894   80233 10287868   128.2 | 36.304 % |
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.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (runsolver) R 30918 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479723858 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99935 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 2898 0 0 0 988 9 0 0 25 0 1 0 479723858 13631488 2876 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3328 2876 603 41 0 3287 0
vsize: 13312
[startup+20 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 2898 0 0 0 1988 10 0 0 25 0 1 0 479723858 13631488 2876 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3328 2876 603 41 0 3287 0
vsize: 13312
[startup+29.9996 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 2898 0 0 0 2987 10 0 0 25 0 1 0 479723858 13631488 2876 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3328 2876 603 41 0 3287 0
vsize: 13312
[startup+40.0001 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 3412 0 0 0 3985 12 0 0 25 0 1 0 479723858 15785984 3390 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3854 3390 603 41 0 3813 0
vsize: 15416
[startup+50.0005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 3687 0 0 0 4985 13 0 0 25 0 1 0 479723858 16990208 3665 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4148 3665 603 41 0 4107 0
vsize: 16592
[startup+60.0004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 3987 0 0 0 5984 14 0 0 25 0 1 0 479723858 18194432 3965 4294967295 134512640 134672761 3221224560 3221223664 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4442 3965 603 41 0 4401 0
vsize: 17768
[startup+70.0012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 5038 0 0 0 6980 18 0 0 25 0 1 0 479723858 22495232 5016 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5492 5016 603 41 0 5451 0
vsize: 21968
[startup+80.0018 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 5769 0 0 0 7976 21 0 0 25 0 1 0 479723858 25452544 5747 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6214 5747 603 41 0 6173 0
vsize: 24856
[startup+90.0025 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 6416 0 0 0 8973 24 0 0 25 0 1 0 479723858 28147712 6394 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6872 6394 603 41 0 6831 0
vsize: 27488
[startup+100.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 6961 0 0 0 9972 25 0 0 25 0 1 0 479723858 30294016 6939 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7396 6939 603 41 0 7355 0
vsize: 29584
[startup+110.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 7590 0 0 0 10970 27 0 0 25 0 1 0 479723858 32845824 7568 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8019 7568 603 41 0 7978 0
vsize: 32076
[startup+120.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 8063 0 0 0 11968 29 0 0 25 0 1 0 479723858 34738176 8041 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8481 8041 603 41 0 8440 0
vsize: 33924
[startup+130.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 8521 0 0 0 12967 30 0 0 25 0 1 0 479723858 36614144 8499 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8939 8499 603 41 0 8898 0
vsize: 35756
[startup+140.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 9049 0 0 0 13966 32 0 0 25 0 1 0 479723858 39022592 9027 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9527 9027 603 41 0 9486 0
vsize: 38108
[startup+150.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 9579 0 0 0 14965 33 0 0 25 0 1 0 479723858 41172992 9557 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10052 9557 603 41 0 10011 0
vsize: 40208
[startup+160.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 10120 0 0 0 15964 34 0 0 25 0 1 0 479723858 43438080 10098 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10605 10098 603 41 0 10564 0
vsize: 42420
[startup+170.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 10610 0 0 0 16962 36 0 0 25 0 1 0 479723858 45449216 10588 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11096 10588 603 41 0 11055 0
vsize: 44384
[startup+180.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11038 0 0 0 17961 37 0 0 25 0 1 0 479723858 47194112 11016 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11522 11016 603 41 0 11481 0
vsize: 46088
[startup+190.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11493 0 0 0 18961 38 0 0 25 0 1 0 479723858 49061888 11471 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11978 11471 603 41 0 11937 0
vsize: 47912
[startup+200.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11599 0 0 0 19960 39 0 0 25 0 1 0 479723858 49459200 11577 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11577 603 41 0 12034 0
vsize: 48300
[startup+210.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 20960 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+220.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 21961 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+230.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 22961 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+240.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 23961 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+250.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 24961 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+260.002 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 25961 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+270.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 30919
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 26961 39 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+280.003 s]
Raw data (loadavg): 0.99 0.98 0.92 3/57 30955
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 27956 43 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+290.003 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 11600 0 0 0 28956 43 0 0 25 0 1 0 479723858 49459200 11578 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12075 11578 603 41 0 12034 0
vsize: 48300
[startup+300.004 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 12010 0 0 0 29956 44 0 0 25 0 1 0 479723858 51208192 11988 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12502 11988 603 41 0 12461 0
vsize: 50008
[startup+310.003 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 12616 0 0 0 30954 46 0 0 25 0 1 0 479723858 53620736 12594 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13091 12594 603 41 0 13050 0
vsize: 52364
[startup+320.005 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13072 0 0 0 31953 47 0 0 25 0 1 0 479723858 55508992 13050 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13552 13051 603 41 0 13511 0
vsize: 54208
[startup+330.005 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 32951 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223728 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+340.005 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 33951 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223760 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+350.006 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30972
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 34952 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223664 134560243 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+360.005 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 35952 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223728 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+370.006 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 36952 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+380.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 37952 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+390.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13522 0 0 0 38952 49 0 0 25 0 1 0 479723858 57356288 13500 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13500 603 41 0 13962 0
vsize: 56012
[startup+400.006 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 39953 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+410.005 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 40953 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+420.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 41953 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+430.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 42953 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+440.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 43953 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+450.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 44953 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+460.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 45954 49 0 0 25 0 1 0 479723858 57356288 13501 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14003 13501 603 41 0 13962 0
vsize: 56012
[startup+470.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 46954 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+480.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 47954 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+490.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 48954 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+500.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 49954 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+510.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 50954 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+520.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 51955 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+530.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 52955 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+540.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 53955 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+550.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 54955 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+560.005 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 55955 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+570.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 56956 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+580.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 57956 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+590.006 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 58956 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+600.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 59956 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+610.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 60956 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+620.007 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30974
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 61957 49 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223744 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+630.008 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 62956 50 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+640.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 63956 50 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+650.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13523 0 0 0 64955 51 0 0 25 0 1 0 479723858 57344000 13501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13501 603 41 0 13959 0
vsize: 56000
[startup+660.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13526 0 0 0 65955 51 0 0 25 0 1 0 479723858 57344000 13504 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13504 603 41 0 13959 0
vsize: 56000
[startup+670.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13529 0 0 0 66955 51 0 0 25 0 1 0 479723858 57344000 13507 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13507 603 41 0 13959 0
vsize: 56000
[startup+680.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13531 0 0 0 67954 52 0 0 25 0 1 0 479723858 57344000 13509 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14000 13509 603 41 0 13959 0
vsize: 56000
[startup+690.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 13770 0 0 0 68953 53 0 0 25 0 1 0 479723858 58286080 13748 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14230 13748 603 41 0 14189 0
vsize: 56920
[startup+700.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14038 0 0 0 69952 54 0 0 25 0 1 0 479723858 59355136 14016 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14491 14016 603 41 0 14450 0
vsize: 57964
[startup+710.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14336 0 0 0 70951 56 0 0 25 0 1 0 479723858 60686336 14314 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14816 14314 603 41 0 14775 0
vsize: 59264
[startup+720.009 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14624 0 0 0 71950 57 0 0 25 0 1 0 479723858 61755392 14602 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15077 14602 603 41 0 15036 0
vsize: 60308
[startup+730.01 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 72949 58 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223664 134559869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+740.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 73949 58 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+750.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 74949 58 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+760.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 75949 58 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+770.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 76948 59 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+780.011 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 77948 59 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+790.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 78948 60 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+800.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 79947 60 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+810.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 80947 60 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+820.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 81947 61 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223664 134555076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 82946 61 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+840.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 83946 61 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+850.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 84946 62 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+860.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 85946 62 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+870.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 86945 63 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+880.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 87945 63 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+890.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 88945 63 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+900.013 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 89945 64 0 0 25 0 1 0 479723858 62152704 14683 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15174 14683 603 41 0 15133 0
vsize: 60696
[startup+910.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 90944 64 0 0 25 0 1 0 479723858 62111744 14683 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14683 603 41 0 15123 0
vsize: 60656
[startup+920.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 91944 65 0 0 25 0 1 0 479723858 62111744 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14683 603 41 0 15123 0
vsize: 60656
[startup+930.014 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14705 0 0 0 92944 65 0 0 25 0 1 0 479723858 62111744 14683 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14683 603 41 0 15123 0
vsize: 60656
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 93943 66 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+950.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 94943 66 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+960.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 95943 66 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+970.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 96942 67 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+980.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 97942 67 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+990.017 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 98942 67 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 99942 67 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 100942 68 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 101942 68 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 102941 68 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 103941 69 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 104941 69 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 105940 70 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 106940 70 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 107940 70 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 108940 71 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14706 0 0 0 109940 71 0 0 25 0 1 0 479723858 62111744 14684 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15164 14684 603 41 0 15123 0
vsize: 60656
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 14758 0 0 0 110939 71 0 0 25 0 1 0 479723858 62382080 14736 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15230 14736 603 41 0 15189 0
vsize: 60920
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15049 0 0 0 111938 73 0 0 25 0 1 0 479723858 63586304 15027 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15524 15027 603 41 0 15483 0
vsize: 62096
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15333 0 0 0 112937 74 0 0 25 0 1 0 479723858 64659456 15311 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15786 15311 603 41 0 15745 0
vsize: 63144
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15596 0 0 0 113936 75 0 0 25 0 1 0 479723858 65863680 15574 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16080 15574 603 41 0 16039 0
vsize: 64320
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15853 0 0 0 114935 76 0 0 25 0 1 0 479723858 66793472 15831 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16307 15831 603 41 0 16266 0
vsize: 65228
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15877 0 0 0 115934 77 0 0 25 0 1 0 479723858 66928640 15855 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16340 15855 603 41 0 16299 0
vsize: 65360
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15877 0 0 0 116934 77 0 0 25 0 1 0 479723858 66928640 15855 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16340 15855 603 41 0 16299 0
vsize: 65360
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15877 0 0 0 117934 77 0 0 25 0 1 0 479723858 66928640 15855 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16340 15855 603 41 0 16299 0
vsize: 65360
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15879 0 0 0 118934 77 0 0 25 0 1 0 479723858 66928640 15857 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16340 15857 603 41 0 16299 0
vsize: 65360
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 30976
Raw data (stat): 30919 (minisat+) R 30918 28099 28098 0 -1 0 15879 0 0 0 119934 77 0 0 25 0 1 0 479723858 66928640 15857 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16340 15857 603 41 0 16299 0
vsize: 65360
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 30976
Raw data (stat): 30919 (minisat+) Z 30918 28099 28098 0 -1 12 15882 0 0 0 119934 81 0 0 25 0 1 0 479723858 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.06
CPU time (s): 1200.16
CPU user time (s): 1199.35
CPU system time (s): 0.810876
CPU usage (%): 100.008
Max. virtual memory (Kb): 65360
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####