PB'05 competition: run trace

Some explanations

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

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

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        855028 kB
Buffers:         31652 kB
Cached:         104368 kB
SwapCached:        524 kB
Active:          47076 kB
Inactive:        92360 kB
HighTotal:      131008 kB
HighFree:        22932 kB
LowTotal:       903652 kB
LowFree:        832096 kB
SwapTotal:     2097892 kB
SwapFree:      2097368 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            34524 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 23:16:20 (client local time) WITH STATUS 10 IN 1200.19 SECONDS
stats: 3716 7 1200.19 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58549 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   58549   117098 |   19516       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -33[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 1869   maxlim: 33   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   71463   163238 |   23821       0        0     nan |  0.000 % |
c |       100 |   71454   163207 |   26203      97      675     7.0 |  0.108 % |
c |       250 |   71454   163207 |   28823     247     1599     6.5 |  0.109 % |
c |       475 |   71418   163083 |   31705     461     3614     7.8 |  0.250 % |
c |       812 |   71409   163052 |   34876     796     7523     9.5 |  0.285 % |
c |      1319 |   71409   163052 |   38363    1303    11822     9.1 |  0.285 % |
c |      2079 |   71328   162773 |   42200    2039    19036     9.3 |  0.607 % |
c |      3219 |   71103   162002 |   46420    3119    38889    12.5 |  1.570 % |
c |      4927 |   70825   161050 |   51062    4749    65320    13.8 |  2.818 % |
c |      7489 |   69919   157932 |   56168    7013   118112    16.8 |  7.389 % |
c |     11333 |   68135   151784 |   61785   10032   201611    20.1 | 17.555 % |
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 |     12011 |   67847   150789 |   22615   10602   223223    21.1 | 17.555 % |
c |     12111 |   67779   150557 |   24876   10575   224651    21.2 | 19.750 % |
c |     12262 |   67779   150557 |   27364   10726   236778    22.1 | 19.753 % |
c |     12487 |   67728   150378 |   30100   10898   244496    22.4 | 20.036 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Adder-cost: 0   maxlim: 35   bits: 7/6
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     12732 |   67720   150353 |   22573   11140   256128    23.0 | 20.036 % |
c |     12832 |   67636   150061 |   24830   11159   257202    23.0 | 20.672 % |
c |     12982 |   67636   150061 |   27313   11309   266796    23.6 | 20.670 % |
c |     13207 |   67429   149336 |   30044   11413   271125    23.8 | 22.131 % |
c |     13544 |   67367   149118 |   33049   11718   283411    24.2 | 22.632 % |
c |     14050 |   67080   148117 |   36354   12040   294018    24.4 | 24.590 % |
c |     14809 |   67012   147881 |   39989   12739   331217    26.0 | 25.018 % |
c |     15948 |   66985   147790 |   43988   13846   401042    29.0 | 25.160 % |
c |     17657 |   66967   147730 |   48387   15507   471401    30.4 | 25.267 % |
c |     20220 |   66653   146632 |   53225   17729   570041    32.2 | 27.515 % |
c |     24064 |   66543   146254 |   58548   21435   936087    43.7 | 28.261 % |
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 |     27529 |   66525   146197 |   22175   24859  1439504    57.9 | 28.261 % |
c |     27629 |   66433   145875 |   24392   12487   987949    79.1 | 28.999 % |
c |     27779 |   66406   145782 |   26831   12605   992450    78.7 | 29.179 % |
c |     28005 |   66118   144768 |   29514   12782   998738    78.1 | 31.457 % |
c |     28342 |   66118   144768 |   32466   13119  1016029    77.4 | 31.460 % |
c |     28848 |   66101   144709 |   35713   13607  1032392    75.9 | 31.564 % |
c |     29608 |   66095   144689 |   39284   14356  1084717    75.6 | 31.602 % |
c |     30748 |   66089   144669 |   43212   15483  1147682    74.1 | 31.635 % |
c |     32457 |   66080   144638 |   47534   17179  1219132    71.0 | 31.671 % |
c |     35019 |   66030   144462 |   52287   19662  1402993    71.4 | 31.991 % |
c |     38863 |   66030   144462 |   57516   23506  1810659    77.0 | 31.991 % |
c |     44629 |   66021   144431 |   63267   29259  2502706    85.5 | 32.027 % |
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 |     51735 |   65988   144324 |   21996   36328  3303870    90.9 | 32.027 % |
c |     51835 |   65988   144324 |   24195   15172  1431226    94.3 | 32.302 % |
c |     51985 |   65988   144324 |   26615   15322  1438757    93.9 | 32.301 % |
c |     52210 |   65970   144262 |   29276   15543  1450110    93.3 | 32.375 % |
c |     52549 |   65964   144242 |   32204   15877  1463000    92.1 | 32.407 % |
c |     53055 |   65964   144242 |   35424   16383  1491959    91.1 | 32.407 % |
c |     53814 |   65955   144211 |   38967   17139  1536367    89.6 | 32.443 % |
c |     54954 |   65942   144164 |   42863   18277  1609450    88.1 | 32.552 % |
c |     56662 |   65942   144164 |   47150   19985  1738287    87.0 | 32.550 % |
c |     59224 |   65885   143963 |   51865   22535  1885678    83.7 | 32.977 % |
c |     63070 |   65885   143963 |   57051   26381  2206303    83.6 | 32.977 % |
c |     68837 |   65849   143839 |   62757   32117  3031345    94.4 | 33.193 % |
c |     77486 |   65822   143744 |   69032   40763  4060879    99.6 | 33.405 % |
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 |     86531 |   65823   143752 |   21941   49808  5202209   104.4 | 33.405 % |
c |     86631 |   65823   143752 |   24135   15509  1428619    92.1 | 33.428 % |
c |     86782 |   65814   143721 |   26548   15653  1437113    91.8 | 33.466 % |
c |     87007 |   65763   143544 |   29203   15872  1444457    91.0 | 33.891 % |
c |     87344 |   65763   143544 |   32123   16209  1474314    91.0 | 33.891 % |
c |     87852 |   65763   143544 |   35336   16717  1500135    89.7 | 33.893 % |
c |     88612 |   65734   143441 |   38869   17470  1567883    89.7 | 34.140 % |
c |     89752 |   65734   143441 |   42756   18610  1634844    87.8 | 34.140 % |
c |     91461 |   65734   143441 |   47032   20319  1779020    87.6 | 34.140 % |
c |     94024 |   65734   143441 |   51735   22882  2027264    88.6 | 34.142 % |
c |     97868 |   65648   143141 |   56909   26650  2372176    89.0 | 34.817 % |
c |    103636 |   65648   143141 |   62600   32418  3025438    93.3 | 34.818 % |
c |    112286 |   65648   143141 |   68860   41068  4498258   109.5 | 34.819 % |
c |    125260 |   65648   143141 |   75746   54042  6105108   113.0 | 34.819 % |
c |    144721 |   65648   143141 |   83320   73503  8451514   115.0 | 34.817 % |
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 |    163265 |   65649   143146 |   21883   22977  1987278    86.5 | 34.817 % |
c |    163365 |   65649   143146 |   24071   11589   917311    79.2 | 34.842 % |
c |    163515 |   65649   143146 |   26478   11739   920093    78.4 | 34.840 % |
c |    163740 |   65649   143146 |   29126   11964   929463    77.7 | 34.841 % |
c |    164077 |   65638   143107 |   32038   12295   938526    76.3 | 34.911 % |
c |    164583 |   65638   143107 |   35242   12801   960745    75.1 | 34.911 % |
c |    165345 |   65638   143107 |   38767   13563  1012435    74.6 | 34.911 % |
c |    166484 |   65638   143107 |   42643   14702  1078247    73.3 | 34.911 % |
c |    168192 |   65606   142995 |   46908   16379  1223020    74.7 | 35.056 % |
c |    170755 |   65606   142995 |   51598   18942  1474585    77.8 | 35.053 % |
c |    174600 |   65606   142995 |   56758   22787  1966026    86.3 | 35.053 % |
c |    180366 |   65606   142995 |   62434   28553  2443623    85.6 | 35.055 % |
c |    189015 |   65580   142905 |   68678   37185  3463056    93.1 | 35.198 % |
c |    201991 |   65580   142905 |   75546   50161  4641997    92.5 | 35.198 % |
c |    221453 |   65580   142905 |   83100   69623  5827411    83.7 | 35.196 % |
c |    250646 |   65580   142905 |   91410   30085  2727070    90.6 | 35.198 % |
c |    294436 |   65495   142606 |  100551   73859  7931078   107.4 | 35.872 % |
c |    360120 |   65483   142566 |  110606   52789  6445163   122.1 | 35.945 % |
c |    458648 |   65452   142457 |  121667   55555  7885092   141.9 | 36.123 % |
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 -C26#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 29712
Raw data (stat): 29712 (runsolver) R 29711 26298 26297 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479717493 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.99956 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 2906 0 0 0 988 9 0 0 25 0 1 0 479717493 13668352 2884 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3337 2884 603 41 0 3296 0
vsize: 13348
[startup+20.0003 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 2906 0 0 0 1989 9 0 0 25 0 1 0 479717493 13668352 2884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3337 2884 603 41 0 3296 0
vsize: 13348
[startup+30.0015 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 3010 0 0 0 2988 10 0 0 25 0 1 0 479717493 14065664 2988 4294967295 134512640 134672761 3221224560 3221223728 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3434 2988 603 41 0 3393 0
vsize: 13736
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 3276 0 0 0 3987 11 0 0 25 0 1 0 479717493 15130624 3254 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3694 3254 603 41 0 3653 0
vsize: 14776
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 4220 0 0 0 4983 15 0 0 25 0 1 0 479717493 19034112 4198 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4647 4198 603 41 0 4606 0
vsize: 18588
[startup+60.0025 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 4982 0 0 0 5981 17 0 0 25 0 1 0 479717493 22253568 4960 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5433 4960 603 41 0 5392 0
vsize: 21732
[startup+70.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 5016 0 0 0 6981 17 0 0 25 0 1 0 479717493 22384640 4994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4994 603 41 0 5424 0
vsize: 21860
[startup+80.0027 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 5016 0 0 0 7981 17 0 0 25 0 1 0 479717493 22384640 4994 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4994 603 41 0 5424 0
vsize: 21860
[startup+90.0034 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 5522 0 0 0 8980 18 0 0 25 0 1 0 479717493 24535040 5500 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5990 5500 603 41 0 5949 0
vsize: 23960
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 6080 0 0 0 9978 21 0 0 25 0 1 0 479717493 26681344 6058 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6514 6058 603 41 0 6473 0
vsize: 26056
[startup+110.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 6722 0 0 0 10977 22 0 0 25 0 1 0 479717493 29360128 6700 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7168 6700 603 41 0 7127 0
vsize: 28672
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7094 0 0 0 11976 24 0 0 25 0 1 0 479717493 30830592 7072 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7527 7072 603 41 0 7486 0
vsize: 30108
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7094 0 0 0 12976 24 0 0 25 0 1 0 479717493 30830592 7072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7527 7072 603 41 0 7486 0
vsize: 30108
[startup+140.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7094 0 0 0 13976 24 0 0 25 0 1 0 479717493 30830592 7072 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7527 7072 603 41 0 7486 0
vsize: 30108
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7094 0 0 0 14976 24 0 0 25 0 1 0 479717493 30830592 7072 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7527 7072 603 41 0 7486 0
vsize: 30108
[startup+160.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7095 0 0 0 15976 24 0 0 25 0 1 0 479717493 30830592 7073 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7527 7073 603 41 0 7486 0
vsize: 30108
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7353 0 0 0 16975 25 0 0 25 0 1 0 479717493 31903744 7331 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7789 7331 603 41 0 7748 0
vsize: 31156
[startup+180.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 7979 0 0 0 17974 27 0 0 25 0 1 0 479717493 34451456 7957 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8411 7957 603 41 0 8370 0
vsize: 33644
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 8451 0 0 0 18973 28 0 0 25 0 1 0 479717493 36339712 8429 4294967295 134512640 134672761 3221224560 3221223728 134564457 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8872 8429 603 41 0 8831 0
vsize: 35488
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 8916 0 0 0 19972 29 0 0 25 0 1 0 479717493 38354944 8894 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9364 8894 603 41 0 9323 0
vsize: 37456
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 9386 0 0 0 20970 31 0 0 25 0 1 0 479717493 40235008 9364 4294967295 134512640 134672761 3221224560 3221223708 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9823 9364 603 41 0 9782 0
vsize: 39292
[startup+220.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 29712
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 9927 0 0 0 21969 32 0 0 25 0 1 0 479717493 42647552 9905 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10412 9905 603 41 0 10371 0
vsize: 41648
[startup+230.004 s]
Raw data (loadavg): 1.07 0.99 0.91 3/57 29753
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 10407 0 0 0 22966 35 0 0 25 0 1 0 479717493 44658688 10385 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10903 10385 603 41 0 10862 0
vsize: 43612
[startup+240.005 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 10784 0 0 0 23965 37 0 0 25 0 1 0 479717493 46125056 10762 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11261 10762 603 41 0 11220 0
vsize: 45044
[startup+250.006 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11113 0 0 0 24963 39 0 0 25 0 1 0 479717493 47452160 11091 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11585 11091 603 41 0 11544 0
vsize: 46340
[startup+260.006 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11435 0 0 0 25962 40 0 0 25 0 1 0 479717493 48787456 11413 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11911 11413 603 41 0 11870 0
vsize: 47644
[startup+270.006 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11708 0 0 0 26962 40 0 0 25 0 1 0 479717493 49856512 11686 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12172 11686 603 41 0 12131 0
vsize: 48688
[startup+280.007 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 27962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+290.008 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 28961 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+300.007 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 29765
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 29962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+310.007 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 30962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+320.007 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 31962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+330.007 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 32962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+340.008 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 33962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+350.008 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 34962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+360.007 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 35962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+370.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 36962 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+380.007 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 37963 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+390.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 38963 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+400.008 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 39963 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+410.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11833 0 0 0 40963 41 0 0 25 0 1 0 479717493 50388992 11811 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11811 603 41 0 12261 0
vsize: 49208
[startup+420.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 41963 41 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+430.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 42963 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+440.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 43963 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+450.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 44964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+460.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 45964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+470.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 46964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223744 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+480.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 47964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+490.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 48964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+500.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 49964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+510.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 50964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+520.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 51965 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+530.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 52965 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+540.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 53965 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+550.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 54965 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+560.006 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 55965 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+570.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 56965 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+580.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 57964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+590.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29767
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 58964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+600.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 11834 0 0 0 59964 42 0 0 25 0 1 0 479717493 50388992 11812 4294967295 134512640 134672761 3221224560 3221223664 134560477 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12302 11812 603 41 0 12261 0
vsize: 49208
[startup+610.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 12143 0 0 0 60964 43 0 0 25 0 1 0 479717493 51748864 12121 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12634 12121 603 41 0 12593 0
vsize: 50536
[startup+620.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 12523 0 0 0 61963 44 0 0 25 0 1 0 479717493 53219328 12501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12993 12501 603 41 0 12952 0
vsize: 51972
[startup+630.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 12806 0 0 0 62962 45 0 0 25 0 1 0 479717493 54427648 12784 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13288 12784 603 41 0 13247 0
vsize: 53152
[startup+640.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13197 0 0 0 63960 47 0 0 25 0 1 0 479717493 56037376 13175 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13681 13175 603 41 0 13640 0
vsize: 54724
[startup+650.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13584 0 0 0 64959 48 0 0 25 0 1 0 479717493 57507840 13562 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14040 13562 603 41 0 13999 0
vsize: 56160
[startup+660.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 65958 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221222396 134565911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+670.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 66958 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+680.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 67958 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+690.007 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 68958 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+700.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 69959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+710.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 70959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+720.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 71959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223700 134560629 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+730.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 72959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+740.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 73959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223720 134561240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+750.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 74959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+760.008 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 75959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+770.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 76959 50 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+780.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 77959 51 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223712 134541817 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+790.009 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 78959 51 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+800.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 79959 51 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+810.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13988 0 0 0 80958 52 0 0 25 0 1 0 479717493 59248640 13966 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13966 603 41 0 14424 0
vsize: 57860
[startup+820.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13989 0 0 0 81958 52 0 0 25 0 1 0 479717493 59248640 13967 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13967 603 41 0 14424 0
vsize: 57860
[startup+830.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 13989 0 0 0 82958 52 0 0 25 0 1 0 479717493 59248640 13967 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14465 13967 603 41 0 14424 0
vsize: 57860
[startup+840.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 14090 0 0 0 83957 53 0 0 25 0 1 0 479717493 59654144 14068 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14564 14068 603 41 0 14523 0
vsize: 58256
[startup+850.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 14469 0 0 0 84957 54 0 0 25 0 1 0 479717493 61132800 14447 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14925 14447 603 41 0 14884 0
vsize: 59700
[startup+860.011 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 14841 0 0 0 85956 55 0 0 25 0 1 0 479717493 62730240 14819 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15315 14819 603 41 0 15274 0
vsize: 61260
[startup+870.012 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 15203 0 0 0 86954 56 0 0 25 0 1 0 479717493 64204800 15181 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15675 15181 603 41 0 15634 0
vsize: 62700
[startup+880.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 15577 0 0 0 87953 57 0 0 25 0 1 0 479717493 65687552 15555 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16037 15555 603 41 0 15996 0
vsize: 64148
[startup+890.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 15957 0 0 0 88952 59 0 0 25 0 1 0 479717493 67297280 15935 4294967295 134512640 134672761 3221224560 3221223728 134559068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16430 15935 603 41 0 16389 0
vsize: 65720
[startup+900.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 16231 0 0 0 89951 60 0 0 25 0 1 0 479717493 68374528 16209 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16693 16209 603 41 0 16652 0
vsize: 66772
[startup+910.013 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 16476 0 0 0 90950 61 0 0 25 0 1 0 479717493 69476352 16454 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16962 16454 603 41 0 16921 0
vsize: 67848
[startup+920.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 16691 0 0 0 91950 62 0 0 25 0 1 0 479717493 70283264 16669 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17159 16669 603 41 0 17118 0
vsize: 68636
[startup+930.015 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 16944 0 0 0 92948 63 0 0 25 0 1 0 479717493 71352320 16922 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17420 16922 603 41 0 17379 0
vsize: 69680
[startup+940.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17196 0 0 0 93948 64 0 0 25 0 1 0 479717493 72286208 17174 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17648 17174 603 41 0 17607 0
vsize: 70592
[startup+950.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17446 0 0 0 94946 65 0 0 25 0 1 0 479717493 73359360 17424 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17910 17424 603 41 0 17869 0
vsize: 71640
[startup+960.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17694 0 0 0 95946 66 0 0 25 0 1 0 479717493 74293248 17672 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18138 17672 603 41 0 18097 0
vsize: 72552
[startup+970.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 96945 67 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134561264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+980.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 97945 67 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+990.014 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 98945 68 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1000.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 99944 68 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1010.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 100944 68 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1020.01 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 101944 68 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 102944 69 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 103944 69 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17835 0 0 0 104944 69 0 0 25 0 1 0 479717493 74964992 17813 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17813 603 41 0 18261 0
vsize: 73208
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 105944 69 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 106944 70 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 107944 70 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 108944 70 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 109943 70 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 110943 70 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 111943 71 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 112943 71 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 113943 71 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 114943 71 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 115943 72 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 116942 72 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 117943 72 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 118943 72 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.92 2/54 29769
Raw data (stat): 29712 (minisat+) R 29711 26298 26297 0 -1 0 17836 0 0 0 119942 73 0 0 25 0 1 0 479717493 74964992 17814 4294967295 134512640 134672761 3221224560 3221223744 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18302 17814 603 41 0 18261 0
vsize: 73208
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.92 1/54 29769
Raw data (stat): 29712 (minisat+) Z 29711 26298 26297 0 -1 12 17839 0 0 0 119942 76 0 0 25 0 1 0 479717493 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.06
CPU time (s): 1200.19
CPU user time (s): 1199.43
CPU system time (s): 0.764883
CPU usage (%): 100.011
Max. virtual memory (Kb): 73208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####