PB'05 competition: run trace

Some explanations

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

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

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        455068 kB
Buffers:         33856 kB
Cached:         523620 kB
SwapCached:        532 kB
Active:          53044 kB
Inactive:       506836 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        454816 kB
SwapTotal:     2097136 kB
SwapFree:      2096016 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5636 kB
Slab:            14032 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-27 05:56:59 (client local time) WITH STATUS 152 IN 1229.87 SECONDS
stats: 23085 7 1229.87 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 58245 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: (none)
c   -- Clauses(.)/Splits(s): .....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   58245   116490 |   19415       0        0     nan |  0.000 % |
c ==============================================================================
c [1mFound solution: -29[0m
c ---[   0]---> Sorter-cost:44290     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  103674   223173 |   34558       0        0     nan |  0.000 % |
c |       100 |  103217   222224 |   38013      74      640     8.6 |  0.795 % |
c |       250 |  102277   220190 |   41815     178     1328     7.5 |  2.556 % |
c |       475 |  101299   218072 |   45996     363     3330     9.2 |  4.391 % |
c |       812 |   99047   213116 |   50596     601     6292    10.5 |  8.826 % |
c ==============================================================================
c [1mFound solution: -33[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      1154 |   97981   210998 |   32660     842     9717    11.5 |  8.826 % |
c |      1254 |   97456   209833 |   35926     908    10864    12.0 | 12.242 % |
c |      1404 |   96930   208673 |   39518    1038    12408    12.0 | 13.257 % |
c |      1630 |   96171   206966 |   43470    1223    14347    11.7 | 14.977 % |
c |      1967 |   94090   202274 |   47817    1458    16260    11.2 | 18.956 % |
c |      2473 |   92212   198058 |   52599    1787    19115    10.7 | 22.689 % |
c |      3232 |   88553   189636 |   57859    2356    25138    10.7 | 30.105 % |
c |      4372 |   84300   179875 |   63645    3005    31878    10.6 | 38.823 % |
c |      6081 |   80620   171309 |   70009    4307    46466    10.8 | 46.451 % |
c |      8643 |   75017   158019 |   77010    6013    68321    11.4 | 58.474 % |
c ==============================================================================
c [1mFound solution: -34[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |      9837 |   73511   154433 |   24503    6917    84271    12.2 | 58.474 % |
c |      9937 |   73160   153606 |   26953    6916    84599    12.2 | 62.459 % |
c |     10087 |   73060   153368 |   29648    6999    85824    12.3 | 62.676 % |
c |     10312 |   72828   152824 |   32613    7170    89136    12.4 | 63.163 % |
c |     10649 |   72659   152439 |   35874    7471    94516    12.7 | 63.509 % |
c |     11155 |   72503   152068 |   39462    7865   103845    13.2 | 63.970 % |
c |     11914 |   71669   150067 |   43408    8396   115466    13.8 | 65.675 % |
c |     13055 |   71037   148549 |   47749    9401   141983    15.1 | 67.046 % |
c |     14763 |   70222   146623 |   52524   10862   187323    17.2 | 68.772 % |
c ==============================================================================
c [1mFound solution: -35[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     15084 |   70261   146790 |   23420   11142   194649    17.5 | 68.772 % |
c |     15184 |   70145   146515 |   25762   11226   196318    17.5 | 69.049 % |
c |     15334 |   70122   146458 |   28338   11375   199287    17.5 | 69.100 % |
c |     15559 |   70122   146458 |   31172   11600   219368    18.9 | 69.100 % |
c |     15896 |   70114   146440 |   34289   11935   226983    19.0 | 69.116 % |
c |     16402 |   69855   145806 |   37718   12327   241011    19.6 | 69.697 % |
c |     17161 |   69457   144856 |   41489   12860   269839    21.0 | 70.553 % |
c |     18300 |   68230   141868 |   45638   13498   300688    22.3 | 73.307 % |
c ==============================================================================
c [1mFound solution: -36[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19394 |   67923   141108 |   22641   14427   343281    23.8 | 73.307 % |
c |     19495 |   67908   141073 |   24905   14526   347004    23.9 | 74.024 % |
c ==============================================================================
c [1mFound solution: -37[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     19613 |   67925   141145 |   22641   14641   351375    24.0 | 74.024 % |
c |     19713 |   67839   140937 |   24905   14731   356033    24.2 | 74.212 % |
c |     19863 |   67762   140750 |   27395   14851   358518    24.1 | 74.384 % |
c |     20088 |   67631   140425 |   30135   14979   363163    24.2 | 74.687 % |
c |     20425 |   67626   140412 |   33148   15243   374131    24.5 | 74.700 % |
c |     20932 |   67626   140412 |   36463   15750   434642    27.6 | 74.700 % |
c |     21692 |   67432   139937 |   40109   16429   458771    27.9 | 75.130 % |
c |     22831 |   67112   139167 |   44120   17411   506808    29.1 | 75.822 % |
c |     24539 |   67069   139072 |   48532   19055   591866    31.1 | 75.899 % |
c |     27101 |   66891   138638 |   53386   21563   774079    35.9 | 76.294 % |
c |     30945 |   66792   138391 |   58724   25311  1005599    39.7 | 76.527 % |
c ==============================================================================
c [1mFound solution: -38[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     35844 |   66669   138025 |   22223   30022  1470073    49.0 | 76.527 % |
c |     35945 |   66544   137727 |   24445   30030  1471559    49.0 | 77.089 % |
c |     36097 |   66544   137727 |   26889   30182  1483627    49.2 | 77.089 % |
c |     36322 |   66328   137202 |   29578   30294  1489137    49.2 | 77.568 % |
c |     36659 |   66286   137102 |   32536   30598  1502725    49.1 | 77.657 % |
c |     37165 |   66286   137102 |   35790   31104  1531065    49.2 | 77.657 % |
c |     37924 |   66236   136980 |   39369   31838  1579318    49.6 | 77.772 % |
c |     39063 |   66198   136896 |   43306   32931  1663184    50.5 | 77.845 % |
c |     40771 |   66094   136643 |   47636   34450  1773571    51.5 | 78.081 % |
c ==============================================================================
c [1mFound solution: -39[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     43229 |   66119   136738 |   22039   36846  2044619    55.5 | 78.081 % |
c |     43330 |   66082   136649 |   24242   36918  2046357    55.4 | 78.194 % |
c |     43480 |   66082   136649 |   26667   37068  2055234    55.4 | 78.194 % |
c |     43705 |   66061   136598 |   29333   37197  2068198    55.6 | 78.241 % |
c |     44042 |   66061   136598 |   32267   37534  2088672    55.6 | 78.241 % |
c |     44548 |   65988   136417 |   35494   37789  2109858    55.8 | 78.407 % |
c |     45307 |   65967   136364 |   39043   38528  2171262    56.4 | 78.457 % |
c |     46446 |   65967   136364 |   42947   39667  2284055    57.6 | 78.457 % |
c |     48155 |   65911   136232 |   47242   41326  2437988    59.0 | 78.578 % |
c |     50717 |   65911   136232 |   51966   43888  2766324    63.0 | 78.578 % |
c |     54561 |   65908   136225 |   57163   47731  3237086    67.8 | 78.584 % |
c ==============================================================================
c [1mFound solution: -40[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     56290 |   65823   135998 |   21941   48563  3297518    67.9 | 78.584 % |
c |     56390 |   65712   135748 |   24135   19988  1396674    69.9 | 78.983 % |
c |     56540 |   65712   135748 |   26548   20138  1404187    69.7 | 78.983 % |
c |     56765 |   65650   135596 |   29203   20338  1414088    69.5 | 79.126 % |
c |     57103 |   65650   135596 |   32123   20676  1442270    69.8 | 79.126 % |
c |     57610 |   65650   135596 |   35336   21183  1470803    69.4 | 79.126 % |
c |     58369 |   65650   135596 |   38869   21942  1512854    68.9 | 79.126 % |
c |     59509 |   65650   135596 |   42756   23082  1617718    70.1 | 79.126 % |
c |     61219 |   65650   135596 |   47032   24792  1814999    73.2 | 79.126 % |
c |     63781 |   65446   135086 |   51735   27327  2124510    77.7 | 79.590 % |
c |     67625 |   65344   134832 |   56909   31081  2420985    77.9 | 79.825 % |
c |     73391 |   65273   134642 |   62600   36808  2997370    81.4 | 80.003 % |
c ==============================================================================
c [1mFound solution: -41[0m
c ---[   0]---> Sorter-cost:    0     Base:
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |     78259 |   65233   134560 |   21744   41665  3434394    82.4 | 80.003 % |
c |     78359 |   65233   134560 |   23918   41765  3440374    82.4 | 80.114 % |
c |     78509 |   65194   134462 |   26310   41909  3446929    82.2 | 80.209 % |
c |     78735 |   65194   134462 |   28941   42135  3468085    82.3 | 80.209 % |
c |     79072 |   65194   134462 |   31835   42472  3491885    82.2 | 80.209 % |
c |     79578 |   65194   134462 |   35018   42978  3533426    82.2 | 80.209 % |
c |     80337 |   65194   134462 |   38520   43737  3606744    82.5 | 80.209 % |
c |     81476 |   65186   134442 |   42372   44835  3720600    83.0 | 80.228 % |
c |     83184 |   65186   134442 |   46610   46543  3854293    82.8 | 80.228 % |
c |     85747 |   65146   134350 |   51271   49094  4064252    82.8 | 80.307 % |
c |     89591 |   65137   134329 |   56398   52931  4435673    83.8 | 80.326 % |
c |     95358 |   65137   134329 |   62038   58698  5204836    88.7 | 80.326 % |
c |    104009 |   65137   134329 |   68241   67349  6225461    92.4 | 80.326 % |
c |    116985 |   65033   134076 |   75066   80299  7880223    98.1 | 80.561 % |
c |    136446 |   64945   133856 |   82572   99663 10505945   105.4 | 80.761 % |
c |    165638 |   64651   133139 |   90830   37553  3984323   106.1 | 81.418 % |
c |    209427 |   64398   132524 |   99913   81184  8603031   106.0 | 81.986 % |
c |    275112 |   64354   132420 |  109904   41677  3387232    81.3 | 82.081 % |
/oldhome/oroussel/solvers/minisat+_script: line 9: 27370 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.91 0.97 0.91 2/54 27366
Raw data (stat): 27366 (runsolver) R 27365 5562 5561 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 853693139 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0005 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0016 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.0019 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0027 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0034 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0028 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.71 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 27370
Raw data (stat): 27366 (minisat+_script) S 27365 5562 5561 0 -1 0 275 239 0 0 0 0 0 0 20 0 1 0 853693139 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.71
CPU time (s): 1229.87
CPU user time (s): 1229.16
CPU system time (s): 0.705892
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####