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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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:        895916 kB
Buffers:         36552 kB
Cached:          80168 kB
SwapCached:       2144 kB
Active:          65472 kB
Inactive:        56200 kB
HighTotal:      131008 kB
HighFree:        46984 kB
LowTotal:       903652 kB
LowFree:        848932 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11520 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 03:12:49 (client local time) WITH STATUS 10 IN 1200.22 SECONDS
stats: 4466 7 1200.22 10
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58624 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 |   58624   117248 |   19541       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -31[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  104213   224311 |   34737       0        0     nan |  0.000 % |
c |       100 |  103753   223355 |   38210      63      352     5.6 |  0.799 % |
c |       250 |  103075   221899 |   42031     184     1699     9.2 |  2.046 % |
c |       475 |  101685   218869 |   46234     359     3428     9.5 |  4.676 % |
c |       813 |   99941   215027 |   50858     624     5935     9.5 |  8.041 % |
c ==============================================================================
c [1mFound solution: -34[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1145 |   98367   211607 |   32789     875     9453    10.8 |  8.041 % |
c |      1246 |   97670   210062 |   36067     936    10041    10.7 | 12.509 % |
c |      1396 |   97202   209006 |   39674    1031    10925    10.6 | 13.452 % |
c |      1621 |   95987   206277 |   43642    1161    12048    10.4 | 15.877 % |
c |      1958 |   94801   203593 |   48006    1411    15086    10.7 | 18.255 % |
c |      2464 |   92142   197582 |   52807    1692    17509    10.3 | 23.612 % |
c |      3223 |   89622   191786 |   58087    2260    23288    10.3 | 28.835 % |
c |      4362 |   85515   182365 |   63896    3094    31899    10.3 | 37.082 % |
c |      6070 |   81641   173405 |   70286    4400    47324    10.8 | 45.054 % |
c |      8632 |   76140   160465 |   77314    6222    77175    12.4 | 56.811 % |
c |     12476 |   71881   150330 |   85046    9255   155440    16.8 | 66.013 % |
c ==============================================================================
c [1mFound solution: -35[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     14307 |   70810   147891 |   23603   10753   201061    18.7 | 66.013 % |
c |     14407 |   70765   147784 |   25963   10841   202522    18.7 | 68.509 % |
c |     14557 |   70765   147784 |   28559   10991   207402    18.9 | 68.509 % |
c |     14783 |   70691   147602 |   31415   11185   216078    19.3 | 68.675 % |
c |     15120 |   70586   147358 |   34557   11507   227319    19.8 | 68.886 % |
c |     15626 |   70348   146787 |   38012   11951   241938    20.2 | 69.400 % |
c |     16385 |   70089   146154 |   41814   12648   271863    21.5 | 69.975 % |
c ==============================================================================
c [1mFound solution: -36[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     16815 |   69891   145672 |   23297   13020   282802    21.7 | 69.975 % |
c |     16915 |   69891   145672 |   25626   13120   284893    21.7 | 70.395 % |
c |     17065 |   69891   145672 |   28189   13270   286399    21.6 | 70.395 % |
c |     17290 |   69827   145517 |   31008   13475   295467    21.9 | 70.532 % |
c |     17627 |   69734   145292 |   34109   13799   310942    22.5 | 70.743 % |
c |     18133 |   69371   144409 |   37520   14192   322561    22.7 | 71.538 % |
c ==============================================================================
c [1mFound solution: -37[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     18277 |   69362   144430 |   23120   14335   325818    22.7 | 71.538 % |
c |     18377 |   69362   144430 |   25432   14435   332585    23.0 | 71.584 % |
c |     18527 |   69277   144233 |   27975   14556   347362    23.9 | 71.763 % |
c |     18752 |   69277   144233 |   30772   14781   367844    24.9 | 71.763 % |
c |     19089 |   69030   143626 |   33849   14950   374080    25.0 | 72.327 % |
c |     19596 |   68741   142905 |   37234   15398   392392    25.5 | 73.016 % |
c |     20355 |   68660   142718 |   40958   16081   432831    26.9 | 73.185 % |
c |     21494 |   68513   142365 |   45054   17165   509426    29.7 | 73.511 % |
c |     23202 |   68154   141510 |   49559   18653   641562    34.4 | 74.298 % |
c ==============================================================================
c [1mFound solution: -38[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     23824 |   67852   140729 |   22617   19046   663777    34.9 | 74.298 % |
c |     23924 |   67766   140515 |   24878   19123   665280    34.8 | 75.183 % |
c |     24074 |   67714   140393 |   27366   19252   669804    34.8 | 75.292 % |
c |     24299 |   67714   140393 |   30103   19477   677322    34.8 | 75.292 % |
c |     24636 |   67714   140393 |   33113   19814   696585    35.2 | 75.292 % |
c |     25142 |   67678   140303 |   36424   20309   716491    35.3 | 75.375 % |
c |     25902 |   67425   139703 |   40067   20929   797034    38.1 | 75.917 % |
c |     27042 |   67212   139192 |   44074   21947   872312    39.7 | 76.383 % |
c |     28750 |   67142   139014 |   48481   23609  1034815    43.8 | 76.548 % |
c |     31312 |   67092   138893 |   53329   26102  1245314    47.7 | 76.657 % |
c |     35156 |   66477   137377 |   58662   29648  1507713    50.9 | 78.057 % |
c |     40922 |   66357   137092 |   64528   35234  2003265    56.9 | 78.315 % |
c |     49572 |   66165   136632 |   70981   43618  2849495    65.3 | 78.733 % |
c ==============================================================================
c [1mFound solution: -39[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     53102 |   66131   136585 |   22043   46964  3239093    69.0 | 78.733 % |
c |     53203 |   66092   136494 |   24247   19870  1267667    63.8 | 78.977 % |
c |     53353 |   66092   136494 |   26672   20020  1277625    63.8 | 78.977 % |
c |     53578 |   66092   136494 |   29339   20245  1297647    64.1 | 78.977 % |
c |     53917 |   66083   136473 |   32273   20580  1329003    64.6 | 78.996 % |
c |     54424 |   66083   136473 |   35500   21087  1371465    65.0 | 78.996 % |
c |     55183 |   66081   136469 |   39050   21844  1449488    66.4 | 78.999 % |
c |     56322 |   66081   136469 |   42955   22983  1576964    68.6 | 78.999 % |
c |     58030 |   66081   136469 |   47251   24691  1727745    70.0 | 78.999 % |
c |     60592 |   65903   136032 |   51976   27218  1994366    73.3 | 79.390 % |
c |     64436 |   65748   135667 |   57173   31008  2368011    76.4 | 79.714 % |
c |     70202 |   65748   135667 |   62891   36774  3054028    83.0 | 79.714 % |
c |     78851 |   65630   135370 |   69180   45415  4281369    94.3 | 79.987 % |
c |     91825 |   65630   135370 |   76098   58389  6085540   104.2 | 79.987 % |
c ==============================================================================
c [1mFound solution: -40[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     97446 |   65617   135317 |   21872   63942  6734885   105.3 | 79.987 % |
c |     97546 |   65521   135083 |   24059   19913  1776166    89.2 | 80.240 % |
c |     97696 |   65511   135059 |   26465   20062  1785837    89.0 | 80.262 % |
c |     97921 |   65485   134999 |   29111   20286  1798820    88.7 | 80.316 % |
c |     98258 |   65485   134999 |   32022   20623  1818617    88.2 | 80.316 % |
c |     98765 |   65485   134999 |   35225   21130  1863451    88.2 | 80.316 % |
c |     99525 |   65485   134999 |   38747   21890  1943719    88.8 | 80.316 % |
c |    100667 |   65432   134870 |   42622   23023  2052223    89.1 | 80.433 % |
c |    102376 |   65237   134387 |   46884   24634  2215179    89.9 | 80.881 % |
c |    104938 |   65233   134377 |   51573   27193  2439838    89.7 | 80.891 % |
c |    108784 |   65114   134084 |   56730   31017  2904470    93.6 | 81.164 % |
c |    114550 |   64872   133502 |   62403   36617  3619951    98.9 | 81.689 % |
c |    123199 |   64872   133502 |   68643   45266  4649642   102.7 | 81.689 % |
c |    136175 |   64810   133346 |   75508   58227  6774965   116.4 | 81.838 % |
c ==============================================================================
c [1mFound solution: -41[0m
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): (none)
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |    150026 |   64829   133402 |   21609   72073  8627626   119.7 | 81.838 % |
c |    150126 |   64829   133402 |   23769   20486  1739332    84.9 | 81.817 % |
c |    150276 |   64829   133402 |   26146   20636  1744519    84.5 | 81.817 % |
c |    150501 |   64829   133402 |   28761   20861  1763472    84.5 | 81.817 % |
c |    150839 |   64720   133135 |   31637   21184  1776192    83.8 | 82.068 % |
c |    151345 |   64720   133135 |   34801   21690  1809498    83.4 | 82.068 % |
c |    152104 |   64667   133003 |   38281   22431  1868161    83.3 | 82.192 % |
c |    153244 |   64576   132788 |   42109   23332  1921393    82.4 | 82.385 % |
c |    154952 |   64519   132644 |   46320   25032  2128460    85.0 | 82.515 % |
c |    157514 |   64514   132633 |   50952   27592  2413144    87.5 | 82.525 % |
c |    161359 |   64514   132633 |   56048   31437  2830357    90.0 | 82.525 % |
c |    167125 |   64508   132619 |   61652   37198  3592888    96.6 | 82.538 % |
c |    175774 |   64484   132559 |   67818   45837  4744404   103.5 | 82.595 % |
c |    188750 |   64443   132458 |   74600   58799  6135883   104.4 | 82.690 % |
c |    208211 |   64435   132438 |   82060   78258  8346917   106.7 | 82.709 % |
c |    237404 |   64428   132421 |   90266  107448 11304159   105.2 | 82.725 % |
c |    281193 |   64313   132144 |   99292   56003  5085663    90.8 | 82.979 % |
c |    346877 |   64154   131750 |  109222  121446 12746175   105.0 | 83.347 % |
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.84 0.94 0.90 2/54 3935
Raw data (stat): 3935 (runsolver) R 3934 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422914135 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 3613 0 0 0 989 9 0 0 25 0 1 0 422914135 16498688 3591 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4028 3591 603 41 0 3987 0
vsize: 16112
[startup+20.0013 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 3701 0 0 0 1988 9 0 0 25 0 1 0 422914135 17096704 3679 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4174 3679 603 41 0 4133 0
vsize: 16696
[startup+30.0025 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 3701 0 0 0 2987 9 0 0 25 0 1 0 422914135 17096704 3679 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4174 3679 603 41 0 4133 0
vsize: 16696
[startup+40.0023 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 3706 0 0 0 3987 9 0 0 25 0 1 0 422914135 17096704 3684 4294967295 134512640 134672761 3221224560 3221223684 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4174 3684 603 41 0 4133 0
vsize: 16696
[startup+50.0025 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 3802 0 0 0 4987 10 0 0 25 0 1 0 422914135 17502208 3780 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4273 3780 603 41 0 4232 0
vsize: 17092
[startup+60.003 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 4052 0 0 0 5986 11 0 0 25 0 1 0 422914135 18558976 4030 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4531 4030 603 41 0 4490 0
vsize: 18124
[startup+70.003 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 4453 0 0 0 6984 13 0 0 25 0 1 0 422914135 20226048 4431 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4938 4431 603 41 0 4897 0
vsize: 19752
[startup+80.004 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 5038 0 0 0 7982 14 0 0 25 0 1 0 422914135 22634496 5016 4294967295 134512640 134672761 3221224560 3221223712 1074743821 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5526 5016 603 41 0 5485 0
vsize: 22104
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 5450 0 0 0 8981 16 0 0 25 0 1 0 422914135 24244224 5428 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5919 5428 603 41 0 5878 0
vsize: 23676
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 5965 0 0 0 9979 18 0 0 25 0 1 0 422914135 26525696 5943 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6476 5943 603 41 0 6435 0
vsize: 25904
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 6455 0 0 0 10977 20 0 0 25 0 1 0 422914135 28532736 6433 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6966 6433 603 41 0 6925 0
vsize: 27864
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 6963 0 0 0 11976 21 0 0 25 0 1 0 422914135 30547968 6941 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7458 6941 603 41 0 7417 0
vsize: 29832
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 7261 0 0 0 12975 22 0 0 25 0 1 0 422914135 31748096 7239 4294967295 134512640 134672761 3221224560 3221223744 134559038 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7751 7239 603 41 0 7710 0
vsize: 31004
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 7261 0 0 0 13975 23 0 0 25 0 1 0 422914135 31748096 7239 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7751 7239 603 41 0 7710 0
vsize: 31004
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 7261 0 0 0 14975 23 0 0 25 0 1 0 422914135 31748096 7239 4294967295 134512640 134672761 3221224560 3221223704 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7751 7239 603 41 0 7710 0
vsize: 31004
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 7262 0 0 0 15975 23 0 0 25 0 1 0 422914135 31748096 7240 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7751 7240 603 41 0 7710 0
vsize: 31004
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 7609 0 0 0 16974 24 0 0 25 0 1 0 422914135 33222656 7587 4294967295 134512640 134672761 3221224560 3221223664 134559847 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8111 7587 603 41 0 8070 0
vsize: 32444
[startup+180.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 8201 0 0 0 17972 27 0 0 25 0 1 0 422914135 35631104 8179 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8699 8179 603 41 0 8658 0
vsize: 34796
[startup+190.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 8722 0 0 0 18970 29 0 0 25 0 1 0 422914135 37781504 8700 4294967295 134512640 134672761 3221224560 3221223728 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9224 8700 603 41 0 9183 0
vsize: 36896
[startup+200.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 9213 0 0 0 19968 30 0 0 25 0 1 0 422914135 39788544 9191 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9714 9191 603 41 0 9673 0
vsize: 38856
[startup+210.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 9759 0 0 0 20967 32 0 0 25 0 1 0 422914135 41922560 9737 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10235 9737 603 41 0 10194 0
vsize: 40940
[startup+220.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 10190 0 0 0 21966 33 0 0 25 0 1 0 422914135 43659264 10168 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10659 10168 603 41 0 10618 0
vsize: 42636
[startup+230.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 10586 0 0 0 22963 36 0 0 25 0 1 0 422914135 45395968 10564 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11083 10564 603 41 0 11042 0
vsize: 44332
[startup+240.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 10971 0 0 0 23963 36 0 0 25 0 1 0 422914135 46862336 10949 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11441 10949 603 41 0 11400 0
vsize: 45764
[startup+250.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 24963 36 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+260.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 25963 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223744 134558856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+270.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 26963 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 27963 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 28964 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 29964 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223708 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 30964 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 31964 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 32964 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11019 0 0 0 33965 37 0 0 25 0 1 0 422914135 47104000 10997 4294967295 134512640 134672761 3221224560 3221223720 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11500 10997 603 41 0 11459 0
vsize: 46000
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11343 0 0 0 34964 38 0 0 25 0 1 0 422914135 48451584 11321 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11829 11321 603 41 0 11788 0
vsize: 47316
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 11844 0 0 0 35962 39 0 0 25 0 1 0 422914135 50450432 11822 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12317 11822 603 41 0 12276 0
vsize: 49268
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 12249 0 0 0 36961 41 0 0 25 0 1 0 422914135 52441088 12227 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12803 12227 603 41 0 12762 0
vsize: 51212
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 12626 0 0 0 37961 41 0 0 25 0 1 0 422914135 53903360 12604 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13160 12604 603 41 0 13119 0
vsize: 52640
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 12984 0 0 0 38960 42 0 0 25 0 1 0 422914135 55373824 12962 4294967295 134512640 134672761 3221224560 3221223728 134561406 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13519 12962 603 41 0 13478 0
vsize: 54076
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 39960 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 40960 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 41960 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3935
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 42960 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134561021 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+440.037 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 3973
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 43962 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+450.038 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 3988
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 44962 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223744 134558761 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+460.038 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 3988
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 45962 43 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+470.039 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 3988
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 46962 44 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223664 134560065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+480.039 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 3988
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 47962 44 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+490.039 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3988
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 48962 44 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+500.04 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 3988
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 49962 45 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+510.041 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13068 0 0 0 50962 45 0 0 25 0 1 0 422914135 55726080 13046 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13046 603 41 0 13564 0
vsize: 54420
[startup+520.041 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13069 0 0 0 51961 46 0 0 25 0 1 0 422914135 55726080 13047 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13047 603 41 0 13564 0
vsize: 54420
[startup+530.042 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13069 0 0 0 52961 46 0 0 25 0 1 0 422914135 55726080 13047 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13047 603 41 0 13564 0
vsize: 54420
[startup+540.042 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13069 0 0 0 53961 46 0 0 25 0 1 0 422914135 55726080 13047 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13047 603 41 0 13564 0
vsize: 54420
[startup+550.042 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13072 0 0 0 54961 47 0 0 25 0 1 0 422914135 55726080 13050 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13050 603 41 0 13564 0
vsize: 54420
[startup+560.043 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13074 0 0 0 55961 47 0 0 25 0 1 0 422914135 55726080 13052 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13605 13052 603 41 0 13564 0
vsize: 54420
[startup+570.043 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13176 0 0 0 56961 47 0 0 25 0 1 0 422914135 56131584 13154 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13704 13154 603 41 0 13663 0
vsize: 54816
[startup+580.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13467 0 0 0 57960 48 0 0 25 0 1 0 422914135 57323520 13445 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13995 13445 603 41 0 13954 0
vsize: 55980
[startup+590.044 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 13746 0 0 0 58959 49 0 0 25 0 1 0 422914135 58384384 13724 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14254 13724 603 41 0 14213 0
vsize: 57016
[startup+600.045 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 14017 0 0 0 59958 51 0 0 25 0 1 0 422914135 59588608 13995 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14548 13995 603 41 0 14507 0
vsize: 58192
[startup+610.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 14295 0 0 0 60957 52 0 0 25 0 1 0 422914135 60657664 14273 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14809 14273 603 41 0 14768 0
vsize: 59236
[startup+620.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 14569 0 0 0 61956 53 0 0 25 0 1 0 422914135 61853696 14547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15101 14547 603 41 0 15060 0
vsize: 60404
[startup+630.046 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 14813 0 0 0 62956 53 0 0 25 0 1 0 422914135 62787584 14791 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15329 14791 603 41 0 15288 0
vsize: 61316
[startup+640.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 15016 0 0 0 63955 54 0 0 25 0 1 0 422914135 63586304 14994 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15524 14994 603 41 0 15483 0
vsize: 62096
[startup+650.047 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 15241 0 0 0 64954 56 0 0 25 0 1 0 422914135 64528384 15219 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15754 15219 603 41 0 15713 0
vsize: 63016
[startup+660.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 15441 0 0 0 65953 57 0 0 25 0 1 0 422914135 65318912 15419 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15947 15419 603 41 0 15906 0
vsize: 63788
[startup+670.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 15650 0 0 0 66952 58 0 0 25 0 1 0 422914135 66248704 15628 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16174 15628 603 41 0 16133 0
vsize: 64696
[startup+680.048 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 15850 0 0 0 67952 58 0 0 25 0 1 0 422914135 67043328 15828 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16368 15828 603 41 0 16327 0
vsize: 65472
[startup+690.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 16047 0 0 0 68952 59 0 0 25 0 1 0 422914135 67850240 16025 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16565 16025 603 41 0 16524 0
vsize: 66260
[startup+700.049 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 16235 0 0 0 69951 60 0 0 25 0 1 0 422914135 68513792 16213 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16727 16213 603 41 0 16686 0
vsize: 66908
[startup+710.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 16448 0 0 0 70950 60 0 0 25 0 1 0 422914135 69447680 16426 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16955 16426 603 41 0 16914 0
vsize: 67820
[startup+720.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 16680 0 0 0 71950 61 0 0 25 0 1 0 422914135 70385664 16658 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17184 16658 603 41 0 17143 0
vsize: 68736
[startup+730.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 16918 0 0 0 72949 61 0 0 25 0 1 0 422914135 71323648 16896 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17413 16896 603 41 0 17372 0
vsize: 69652
[startup+740.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17144 0 0 0 73949 62 0 0 25 0 1 0 422914135 72261632 17122 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17642 17122 603 41 0 17601 0
vsize: 70568
[startup+750.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 74948 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+760.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 75948 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+770.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 76949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+780.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 77949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+790.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3990
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 78949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+800.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 79949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223760 134557830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+810.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 80949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+820.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 81950 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+830.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 82950 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+840.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 83949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+850.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 84949 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+860.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 85950 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223664 134560237 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+870.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17316 0 0 0 86950 63 0 0 25 0 1 0 422914135 72925184 17294 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17294 603 41 0 17763 0
vsize: 71216
[startup+880.056 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17317 0 0 0 87950 63 0 0 25 0 1 0 422914135 72925184 17295 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17295 603 41 0 17763 0
vsize: 71216
[startup+890.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17317 0 0 0 88950 63 0 0 25 0 1 0 422914135 72925184 17295 4294967295 134512640 134672761 3221224560 3221223744 134558836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17295 603 41 0 17763 0
vsize: 71216
[startup+900.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17317 0 0 0 89950 63 0 0 25 0 1 0 422914135 72925184 17295 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17295 603 41 0 17763 0
vsize: 71216
[startup+910.057 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17317 0 0 0 90951 63 0 0 25 0 1 0 422914135 72925184 17295 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17295 603 41 0 17763 0
vsize: 71216
[startup+920.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17317 0 0 0 91951 63 0 0 25 0 1 0 422914135 72925184 17295 4294967295 134512640 134672761 3221224560 3221223712 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17295 603 41 0 17763 0
vsize: 71216
[startup+930.058 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 92951 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+940.059 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 93951 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+950.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 94951 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+960.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 95952 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+970.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 96952 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+980.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 97952 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+990.061 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 98952 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1000.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 99952 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1010.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 100953 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1020.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 101953 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1030.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 102953 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1040.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 103953 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1050.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 104954 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1060.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 105954 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1070.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17318 0 0 0 106954 63 0 0 25 0 1 0 422914135 72925184 17296 4294967295 134512640 134672761 3221224560 3221223708 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17804 17296 603 41 0 17763 0
vsize: 71216
[startup+1080.06 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17514 0 0 0 107954 63 0 0 25 0 1 0 422914135 73723904 17492 4294967295 134512640 134672761 3221224560 3221223696 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17999 17492 603 41 0 17958 0
vsize: 71996
[startup+1090.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17744 0 0 0 108953 64 0 0 25 0 1 0 422914135 74661888 17722 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18228 17722 603 41 0 18187 0
vsize: 72912
[startup+1100.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 17933 0 0 0 109953 64 0 0 25 0 1 0 422914135 75460608 17911 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18423 17911 603 41 0 18382 0
vsize: 73692
[startup+1110.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 18174 0 0 0 110951 65 0 0 25 0 1 0 422914135 76423168 18152 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18658 18152 603 41 0 18617 0
vsize: 74632
[startup+1120.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 18430 0 0 0 111949 67 0 0 25 0 1 0 422914135 77492224 18408 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18919 18408 603 41 0 18878 0
vsize: 75676
[startup+1130.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 18639 0 0 0 112948 68 0 0 25 0 1 0 422914135 78430208 18617 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19148 18617 603 41 0 19107 0
vsize: 76592
[startup+1140.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 18870 0 0 0 113948 68 0 0 25 0 1 0 422914135 79360000 18848 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19375 18848 603 41 0 19334 0
vsize: 77500
[startup+1150.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 19083 0 0 0 114948 69 0 0 25 0 1 0 422914135 80162816 19061 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19571 19061 603 41 0 19530 0
vsize: 78284
[startup+1160.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 19289 0 0 0 115947 69 0 0 25 0 1 0 422914135 81620992 19267 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19927 19267 603 41 0 19886 0
vsize: 79708
[startup+1170.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 19531 0 0 0 116947 70 0 0 25 0 1 0 422914135 82563072 19509 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20157 19509 603 41 0 20116 0
vsize: 80628
[startup+1180.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 19798 0 0 0 117947 70 0 0 25 0 1 0 422914135 83623936 19776 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20416 19776 603 41 0 20375 0
vsize: 81664
[startup+1190.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 20022 0 0 0 118947 71 0 0 25 0 1 0 422914135 84566016 20000 4294967295 134512640 134672761 3221224560 3221221804 134566359 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20000 603 41 0 20605 0
vsize: 82584
[startup+1200.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 3992
Raw data (stat): 3935 (minisat+) R 3934 29151 29150 0 -1 0 20022 0 0 0 119947 71 0 0 25 0 1 0 422914135 84566016 20000 4294967295 134512640 134672761 3221224560 3221223664 134559838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20646 20000 603 41 0 20605 0
vsize: 82584
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 3992
Raw data (stat): 3935 (minisat+) Z 3934 29151 29150 0 -1 12 20025 0 0 0 119947 75 0 0 25 0 1 0 422914135 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 10
Real time (s): 1200.11
CPU time (s): 1200.22
CPU user time (s): 1199.47
CPU system time (s): 0.750885
CPU usage (%): 100.009
Max. virtual memory (Kb): 82584
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####