translation set mm -- set mdl processed theory set constants 308 axiom

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
================================
translation: set.mm --> set.mdl
================================
processed:
theory set
constants - 308
axiomatic - 659
provable - 9679
axioms - 49
theorems - 9676
definitions - 300
rules - 309
super - 1
ruleTheorems - 3
from set.mm in in 11.74 seconds seconds
memory allocation summary:
--------------------------
total memory: 6912 kb (7077888) = 100 %
used memory: 6737 kb (6898835) = 97.4702 %
free memory: 174 kb (179053) = 2.52975 %
active memory: 6695 kb (6856403) = 96.8707 %
disposed memory information:
----------------------------
wasted memory: 28 kb (29646) = 0.418854 %
disposed mem.: 12 kb (12786) = 0.180647 %
fragmentation: 9 of: 16384 = 0.0549316 %
memory usage summary:
---------------------
total volume: 6695 kb (6856403) = 100 %
assertions volume: 3766 kb (3857394) = 56.2597 %
names volume: 1619 kb (1658558) = 24.1899 %
parser volume: 1309 kb (1340451) = 19.5504 %
Memory balance (must be 0):
----------------------------
delta: 0 = 6856403 (active) - 6856403 (used)
================================
DONE
================================
================================
translation: set.mdl --> set.mm
================================
processed:
constants - 308
rules - 309
supers - 1
theories - 1
types - 3
axioms - 349
theorems - 9676
from set.mdl in in 30.72 seconds seconds
memory allocation summary:
--------------------------
total memory: 99328 kb (101711872) = 100 %
used memory: 61171 kb (62639552) = 61.5853 %
free memory: 38156 kb (39072320) = 38.4147 %
active memory: 61103 kb (62569891) = 61.5168 %
disposed memory information:
----------------------------
wasted memory: 68 kb (69653) = 0.0684807 %
disposed mem.: 0 kb (8) = 7.86536e-06 %
fragmentation: 1 of: 16384 = 0.00610352 %
memory usage summary:
---------------------
total volume: 61103 kb (62569891) = 100 %
assertions: 59666 kb (61098718) = 97.6488 %
names: 1132 kb (1159825) = 1.85365 %
parser volume: 304 kb (311348) = 0.4976 %
Memory balance (must be 0):
----------------------------
delta: 0 = 62569891 (active) - 62569891 (used)
================================
DONE
================================
================================
cheking of set-out.mm
================================
processed:
theory set-out
constants - 308
axiomatic - 659
provable - 9676
axioms - 49
theorems - 9676
definitions - 300
rules - 309
super - 1
ruleTheorems - 0
from set-out.mm in in 6.33 seconds seconds
memory allocation summary:
--------------------------
total memory: 6912 kb (7077888) = 100 %
used memory: 6830 kb (6993990) = 98.8146 %
free memory: 81 kb (83898) = 1.18535 %
active memory: 6829 kb (6993190) = 98.8033 %
disposed memory information:
----------------------------
wasted memory: 0 kb (800) = 0.0113028 %
disposed mem.: 0 kb (0) = 0 %
fragmentation: 0 of: 16384 = 0 %
memory usage summary:
---------------------
total volume: 6829 kb (6993190) = 100 %
assertions volume: 4325 kb (4429214) = 63.3361 %
names volume: 1544 kb (1582030) = 22.6224 %
parser volume: 958 kb (981946) = 14.0415 %
Memory balance (must be 0):
----------------------------
delta: 0 = 6993190 (active) - 6993190 (used)
================================
DONE
================================