Mock Version: 2.15
Mock Version: 2.15
Mock Version: 2.15
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'], chrootPath='/var/lib/mock/f40-build-794381-139514/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x3f94976c10>timeout=432000uid=991gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False)
Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bs --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'} and shell False
Building target platforms: riscv64
Building for target riscv64
setting SOURCE_DATE_EPOCH=1706140800
Wrote: /builddir/build/SRPMS/metamath-0.198-7.fc40.src.rpm
Child return code was: 0
ENTER ['do_with_status'](['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'], chrootPath='/var/lib/mock/f40-build-794381-139514/root'env={'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'}shell=Falselogger=<mockbuild.trace_decorator.getLog object at 0x3f94976c10>timeout=432000uid=991gid=135user='mockbuild'nspawn_args=[]unshare_net=TrueprintOutput=False)
Executing command: ['bash', '--login', '-c', '/usr/bin/rpmbuild -bb --target riscv64 --nodeps /builddir/build/SPECS/metamath.spec'] with env {'TERM': 'vt100', 'SHELL': '/bin/bash', 'HOME': '/builddir', 'HOSTNAME': 'mock', 'PATH': '/usr/bin:/bin:/usr/sbin:/sbin', 'PROMPT_COMMAND': 'printf "\\033]0;<mock-chroot>\\007"', 'PS1': '<mock-chroot> \\s-\\v\\$ ', 'LANG': 'C.UTF-8'} and shell False
Building target platforms: riscv64
Building for target riscv64
setting SOURCE_DATE_EPOCH=1706140800
Executing(%prep): /bin/sh -e /var/tmp/rpm-tmp.P3W1DC
+ umask 022
+ cd /builddir/build/BUILD
+ cd /builddir/build/BUILD
+ rm -rf metamath
+ /usr/lib/rpm/rpmuncompress -x /builddir/build/SOURCES/metamath.tar.bz2
+ STATUS=0
+ '[' 0 -ne 0 ']'
+ cd metamath
+ rm -rf /builddir/build/BUILD/metamath-SPECPARTS
+ /usr/bin/mkdir -p /builddir/build/BUILD/metamath-SPECPARTS
+ /usr/bin/chmod -Rf a+rX,u+w,g-w,o-w .
+ cp -p /builddir/build/SOURCES/metamath.tex .
+ touch special-settings.sty
+ rm metamath.exe
+ sed -i '/Try to optimize/,/^$/d' configure.ac
+ autoreconf -fi
configure.ac:13: installing './compile'
configure.ac:26: installing './config.guess'
configure.ac:26: installing './config.sub'
configure.ac:9: installing './install-sh'
configure.ac:9: installing './missing'
Makefile.am: installing './depcomp'
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%build): /bin/sh -e /var/tmp/rpm-tmp.v2gDhf
+ umask 022
+ cd /builddir/build/BUILD
+ CFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CFLAGS
+ CXXFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CXXFLAGS
+ FFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FFLAGS
+ FCFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed   -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes '
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd metamath
+ CFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CFLAGS
+ CXXFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CXXFLAGS
+ FFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FFLAGS
+ FCFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed   -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes '
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ '[' x '!=' x ']'
+ '[' 1 = 1 ']'
+++ dirname ./configure
++ find . -name config.guess -o -name config.sub
+ for i in $(find $(dirname ./configure) -name config.guess -o -name config.sub)
++ basename ./config.sub
+ '[' -f /usr/lib/rpm/redhat/config.sub ']'
+ /usr/bin/rm -f ./config.sub
++ basename ./config.sub
+ /usr/bin/cp -fv /usr/lib/rpm/redhat/config.sub ./config.sub
'/usr/lib/rpm/redhat/config.sub' -> './config.sub'
+ for i in $(find $(dirname ./configure) -name config.guess -o -name config.sub)
++ basename ./config.guess
+ '[' -f /usr/lib/rpm/redhat/config.guess ']'
+ /usr/bin/rm -f ./config.guess
++ basename ./config.guess
+ /usr/bin/cp -fv /usr/lib/rpm/redhat/config.guess ./config.guess
'/usr/lib/rpm/redhat/config.guess' -> './config.guess'
+ '[' 1 = 1 ']'
+ '[' x '!=' 'x-Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-hardened-ld' ']'
++ find . -name ltmain.sh
++ grep -q runstatedir=DIR ./configure
++ echo --runstatedir=/run
+ ./configure --build=riscv64-redhat-linux-gnu --host=riscv64-redhat-linux-gnu --program-prefix= --disable-dependency-tracking --prefix=/usr --exec-prefix=/usr --bindir=/usr/bin --sbindir=/usr/sbin --sysconfdir=/etc --datadir=/usr/share --includedir=/usr/include --libdir=/usr/lib64 --libexecdir=/usr/libexec --localstatedir=/var --runstatedir=/run --sharedstatedir=/var/lib --mandir=/usr/share/man --infodir=/usr/share/info 'CFLAGS=-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv'
checking for a BSD-compatible install... /usr/bin/install -c
checking whether build environment is sane... yes
checking for a race-free mkdir -p... /usr/bin/mkdir -p
checking for gawk... gawk
checking whether make sets $(MAKE)... yes
checking whether make supports nested variables... yes
checking for riscv64-redhat-linux-gnu-gcc... gcc
checking whether the C compiler works... yes
checking for C compiler default output file name... a.out
checking for suffix of executables... 
checking whether we are cross compiling... no
checking for suffix of object files... o
checking whether the compiler supports GNU C... yes
checking whether gcc accepts -g... yes
checking for gcc option to enable C11 features... none needed
checking whether gcc understands -c and -o together... yes
checking whether make supports the include directive... yes (GNU style)
checking dependency style of gcc... none
checking for stdio.h... yes
checking for stdlib.h... yes
checking for string.h... yes
checking for inttypes.h... yes
checking for stdint.h... yes
checking for strings.h... yes
checking for sys/stat.h... yes
checking for sys/types.h... yes
checking for unistd.h... yes
checking for limits.h... yes
checking for stdlib.h... (cached) yes
checking for string.h... (cached) yes
checking for _Bool... yes
checking for stdbool.h that conforms to C99... yes
checking for size_t... yes
checking build system type... riscv64-redhat-linux-gnu
checking host system type... riscv64-redhat-linux-gnu
checking for GNU libc compatible malloc... yes
checking for GNU libc compatible realloc... yes
checking for strchr... yes
checking for strcspn... yes
checking for strstr... yes
checking for gcc warning flags... yes
checking for 'inline' support... yes
CFLAGS=-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra
checking that generated files are newer than configure... done
configure: creating ./config.status
config.status: creating Makefile
config.status: creating config.h
config.status: executing depfiles commands
+ /usr/bin/make -O -j4 V=1 VERBOSE=1
/usr/bin/make  all-am
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmcmdl.o mmcmdl.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmhlpa.o mmhlpa.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmdata.o mmdata.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
mmdata.c: In function ‘getContrib’:
mmdata.c:3579:45: warning: comparison is always false due to limited range of data type [-Wtype-limits]
 3579 |         (vstring)(reviseDateList[stmtNum])) == -1) {
      |                                             ^~
mmdata.c:3584:46: warning: comparison is always false due to limited range of data type [-Wtype-limits]
 3584 |         (vstring)(shortenDateList[stmtNum])) == -1) {
      |                                              ^~
mmdata.c:3830:51: warning: comparison is always true due to limited range of data type [-Wtype-limits]
 3830 |          && compareDates(contribDate, reviseDate) != -1)
      |                                                   ^~
mmdata.c:3832:52: warning: comparison is always true due to limited range of data type [-Wtype-limits]
 3832 |          && compareDates(contribDate, shortenDate) != -1))) {
      |                                                    ^~
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mminou.o mminou.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmmaci.o mmmaci.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmhlpb.o mmhlpb.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmcmds.o mmcmds.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
mmcmds.c: In function ‘verifyMarkup’:
mmcmds.c:5841:46: warning: comparison is always false due to limited range of data type [-Wtype-limits]
 5841 |       if (compareDates(mostRecentDate, str1) == -1) {
      |                                              ^~
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmpfas.o mmpfas.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmutil.o mmutil.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmunif.o mmunif.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmveri.o mmveri.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmvstr.o mmvstr.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmword.o mmword.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmpars.o mmpars.c
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o metamath.o metamath.c
metamath.c: In function ‘command’:
metamath.c:1141:15: warning: ignoring return value of ‘system’ declared with attribute ‘warn_unused_result’ [-Wunused-result]
 1141 |         (void)system(str1);
      |               ^~~~~~~~~~~~
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DHAVE_CONFIG_H -I.    -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra -c -o mmwtex.o mmwtex.c
mmwtex.c: In function ‘printTexComment’:
mmwtex.c:2170:18: warning: comparison is always false due to limited range of data type [-Wtype-limits]
 2170 |         if (mode == -1) { /* Math mode */
      |                  ^~
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
gcc -DINLINE=inline -O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer  -DINLINE=inline -fwrapv -Wall -Wextra  -Wl,-z,relro -Wl,--as-needed   -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes  -o metamath metamath.o mmcmdl.o mmcmds.o mmdata.o mmhlpa.o mmhlpb.o mminou.o mmmaci.o mmpars.o mmpfas.o mmunif.o mmutil.o mmveri.o mmvstr.o mmword.o mmwtex.o   
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
+ touch metamath.ind
+ pdflatex metamath
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2022-11-01> patch level 1
L3 programming layer <2023-02-22>
LaTeX Info: Writing file `./realref.sty'.
LaTeX Info: Writing file `./metamath.bib'.
(/usr/share/texlive/texmf-dist/tex/latex/base/book.cls
Document Class: book 2022/07/02 v1.4n Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
(/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty)
(/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty)
(/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty)
(/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty)
(/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)
(/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty
(/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty)
(/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty
(/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def)))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
No file metamath.aux.
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/var/lib/texm
f/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
No file metamath.toc.
[3] [4] [5] [6]
LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page vii undefined o
n input line 1118.
LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page vii undefined on 
input line 1123.
[7] [8]
LaTeX Warning: Citation `Barrow' on page ix undefined on input line 1220.
[9]
LaTeX Warning: Citation `Davis' on page x undefined on input line 1245.
[10] [11] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd) [12{/usr/sh
are/texlive/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}] [13]
[14]
Chapter 1.
LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1428.
[1]
LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1521.
[2] [3]
LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1588.
[4]
LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1625.
LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1631.
[5]
LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1663.
[6] [7]
LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1783.
[8] [9] [10] [11]
LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1998.
[12] [13]
LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2072.
LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2080.
LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2089.
LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2111.
[14]
LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2140.
LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2156.
LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2164.
LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2169.
[15]
LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2220.
[16]
LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2254.
LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2254.
LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2256.
LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2258.
LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2275.
LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2288.
LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2288.
[17]
LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2302.
LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2322.
[18] [19]
LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2417.
LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2442.
[20]
LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2477.
LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2489.
[21]
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2523.
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2530.
LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2546.
LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2549.
[22]
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2562.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2566.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2577.
LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2587.
LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2591.
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2593.
LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2604.
LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2605.
[23]
LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2634.
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 2663.
[24]
LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26
79.
LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2688.
LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2698.
LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2703.
LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2713.
[25]
LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2755.
[26]
LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2783.
LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2792.
LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2800.
LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2831.
[27] [28]
LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 
2910.
LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2932.
[29] [30] [31] [32]
LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3143.
LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3144.
LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3152.
LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3164.
LaTeX Warning: Citation `PM' on page 33 undefined on input line 3172.
[33]
LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3193.
LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3193.
LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3194.
LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3194.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3202.
LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3214.
LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3245.
LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3245.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3260.
LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3262.
[34]
LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3277.
[35] [36]
Chapter 2.
[37]
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3376.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3379.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3380.
[38] [39]
LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3516.
LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3517.
[40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54]
[55] [56] [57] [58]
Chapter 3.
LaTeX Warning: Citation `Barrow' on page 59 undefined on input line 4512.
[59] [60] [61]
LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4724.
[62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739
[]\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut
ed to Jan []ukasiewicz
[63] [64]
Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmsy/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
LaTeX Warning: Citation `Tarski1965' on page 65 undefined on input line 4919.
[65]
LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4932.
LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4973.
[66]
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5001.
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5018.
LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5037.
[67] [68] [69] [70]
Overfull \hbox (17.90143pt too wide) in paragraph at lines 5320--5320
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarsk
i's
Overfull \hbox (26.88689pt too wide) in paragraph at lines 5400--5400
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxil
iary 
[71] [72] [73]
LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5722.
LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5723.
LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5724.
LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5724.
[74] [75] [76]
LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5986.
LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5988.
LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5989.
[77] [78] [79] [80] [81] [82]
Package amsmath Warning: Foreign command \atop;
(amsmath)                \frac or \genfrac should be used instead
(amsmath)                 on input line 6661.
[83] [84] [85]
LaTeX Warning: Citation `PM' on page 86 undefined on input line 6946.
[86] [87] [88]
Overfull \hbox (2.4539pt too wide) in paragraph at lines 7289--7289
[]\OT1/cmr/bx/n/12 (-20) The Ax-ioms for Real and Com-plex Num-bers Them-
[89] [90] [91]
LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7649.
[92] [93]
LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7789.
[94] [95] [96] [97]
LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8056.
[98]
LaTeX Warning: Citation `CarneiroND' on page 99 undefined on input line 8093.
LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8109.
[99]
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Ration-
Underfull \hbox (badness 5203) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmtt/m/n/10 pm2.65da
Package longtable Warning: Column widths have changed
(longtable)                in table 3.4 on input line 8218.
[100] [101]
Overfull \hbox (1.91838pt too wide) in paragraph at lines 8313--8313
[]\OT1/cmtt/m/n/10 The source has 155711 statements; 2254 are $a and 32250 are 
$p.[] 
LaTeX Warning: Citation `Enderton' on page 102 undefined on input line 8338.
[102] [103] [104]
LaTeX Warning: Citation `Hamilton' on page 105 undefined on input line 8477.
[105] [106] [107] [108] [109] [110]
Chapter 4.
LaTeX Warning: Citation `Russell2' on page 111 undefined on input line 8768.
[111]
LaTeX Warning: Citation `deMillo' on page 112 undefined on input line 8820.
[112] [113] [114] [115] [116] [117] [118]
LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined
(Font)              using `TS1/cmtt/m/n' instead
(Font)              for symbol `textdollar' on input line 9416.
[119] [120] [121] [122] [123] [124]
LaTeX Warning: Citation `Nemeti' on page 125 undefined on input line 9769.
LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9770.
LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9777.
[125] [126] [127] [128] [129] [130] [131]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10257.
[132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143]
[144] [145] [146] [147] [148] [149]
LaTeX Warning: Citation `Behnke' on page 150 undefined on input line 11675.
[150]
LaTeX Warning: Citation `Nemesszeghy' on page 151 undefined on input line 11686
.
LaTeX Warning: Citation `Lejewski' on page 151 undefined on input line 11702.
LaTeX Warning: Citation `Goodstein' on page 151 undefined on input line 11780.
LaTeX Warning: Citation `Robinsont' on page 151 undefined on input line 11789.
[151]
LaTeX Warning: Citation `Quine' on page 152 undefined on input line 11824.
[152] [153] [154]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023
[]\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif
ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases
[155] [156]
Chapter 5.
[157] [158] [159] [160] [161] [162] [163] [164] [165]
Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10
 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m
/n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1
0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth
[166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177]
[178] [179] [180] [181] [182]
Appendix A.
LaTeX Warning: Hyper reference `df-bi' on page 183 undefined on input line 1387
4.
Underfull \hbox (badness 3780) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
LaTeX Warning: Hyper reference `df-or' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-3or' on page 183 undefined on input line 138
74.
LaTeX Warning: Hyper reference `df-an' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-3an' on page 183 undefined on input line 138
74.
LaTeX Warning: Hyper reference `df-ex' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-sb' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-eu' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-clab' on page 183 undefined on input line 13
874.
LaTeX Warning: Hyper reference `df-cleq' on page 183 undefined on input line 13
874.
LaTeX Warning: Hyper reference `df-clel' on page 183 undefined on input line 13
874.
LaTeX Warning: Hyper reference `df-v' on page 183 undefined on input line 13874
.
LaTeX Warning: Hyper reference `df-ss' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-un' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-in' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-dif' on page 183 undefined on input line 138
74.
LaTeX Warning: Hyper reference `df-nul' on page 183 undefined on input line 138
74.
LaTeX Warning: Hyper reference `df-pw' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-op' on page 183 undefined on input line 1387
4.
LaTeX Warning: Hyper reference `df-fv' on page 183 undefined on input line 1387
4.
Underfull \hbox (badness 4266) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
Package longtable Warning: Column widths have changed
(longtable)                in table A.1 on input line 13874.
[183] [184] [185] [186]
Appendix B.
[187] [188]
Appendix C.
LaTeX Warning: Citation `Campbell' on page 189 undefined on input line 14141.
LaTeX Warning: Citation `Munkres' on page 189 undefined on input line 14155.
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14172.
[189] [190] [191]
LaTeX Warning: Citation `Nemeti' on page 192 undefined on input line 14359.
[192] [193] [194]
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14580.
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14581.
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg)
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14635.
[195] [196] [197]
LaTeX Warning: Citation `Hamilton' on page 198 undefined on input line 14805.
LaTeX Warning: Citation `Tarski1965' on page 198 undefined on input line 14812.
[198]
LaTeX Warning: Citation `Kalish' on page 199 undefined on input line 14872.
LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14885.
LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14896.
[199] [200] [201]
LaTeX Warning: Citation `Takeuti' on page 202 undefined on input line 15136.
LaTeX Warning: Citation `Quine' on page 202 undefined on input line 15137.
[202] [203] [204] [205] [206]
Appendix D.
[207] [208]
LaTeX Warning: Citation `Hofstadter' on page 209 undefined on input line 15417.
[209] [210]
Appendix E.
[211] [212] [213] [214]
No file metamath.bbl.
(./metamath.ind)
Package longtable Warning: Table widths have changed. Rerun LaTeX.
(./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
LaTeX Warning: There were undefined references.
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
Package rerunfilecheck Warning: File `metamath.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.
 )
(see the transcript file for additional information)
pdfTeX warning (dest): name{page.\\page@num.exampleref\040} has been referenced
 but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.frameconvert\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.tcomment\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.htmlout\040} has been referenced bu
t does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.framelist\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.redeclaration\040} has been referen
ced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.spec1chars\040} has been referenced
 but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.mathcomments\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.tut1\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.ax1\040} has been referenced but do
es not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfbr\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfopr\040} has been referenced but 
does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.effectivelybound\040} has been refe
renced but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.expandom\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfom\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dfclel\040} has been referenced but
 does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.dollardollar\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.zeroproof\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.treeproof\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.includef\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.demo0\040} has been referenced but 
does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.demoproof\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.nodd\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.envision\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.languagespec\040} has been referenc
ed but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.using\040} has been referenced but 
does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.spec\040} has been referenced but d
oes not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.poincare\040} has been referenced b
ut does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.namespace\040} has been referenced 
but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.categoryth\040} has been referenced
 but does not exist, replaced by a fixed one
pdfTeX warning (dest): name{page.\\page@num.bourbaki\040} has been referenced b
ut does not exist, replaced by a fixed one
</usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/
share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-
dist/fonts/type1/public/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/
fonts/type1/public/amsfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/amsfonts/cm/cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmmi6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmmi7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/
cmmi8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></us
r/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/
texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/
texmf-dist/fonts/type1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/cm/cmsy7.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmsy8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmti10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb><
/usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/s
hare/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/te
xlive/texmf-dist/fonts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texli
ve/texmf-dist/fonts/type1/public/amsfonts/symbols/msam10.pfb></usr/share/texliv
e/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive
/texmf-dist/fonts/type1/public/amsfonts/symbols/msbm7.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/cm-super/sfrm1000.pfb></usr/share/texlive/texmf-dist/font
s/type1/public/cm-super/sftt0800.pfb></usr/share/texlive/texmf-dist/fonts/type1
/public/cm-super/sftt1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public
/cm-super/sftt1200.pfb>
Output written on metamath.pdf (228 pages, 1072702 bytes).
Transcript written on metamath.log.
+ pdflatex metamath
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2022-11-01> patch level 1
L3 programming layer <2023-02-22>
LaTeX Info: File `realref.sty' already exists on the system.
            Not generating it from this source.
LaTeX Info: File `metamath.bib' already exists on the system.
            Not generating it from this source.
(/usr/share/texlive/texmf-dist/tex/latex/base/book.cls
Document Class: book 2022/07/02 v1.4n Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
(/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty)
(/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty)
(/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty)
(/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty)
(/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)
(/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty
(/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty)
(/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty
(/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def)))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/var/lib/texm
f/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd)
[4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 108.
[5{/usr/share/texlive/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}]
[6]) [7] [8] [9] [10]
LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page xi undefined on
 input line 1118.
LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page xi undefined on i
nput line 1123.
[11] [12]
LaTeX Warning: Citation `Barrow' on page xiii undefined on input line 1220.
[13]
LaTeX Warning: Citation `Davis' on page xiv undefined on input line 1245.
[14] [15] [16] [17] [18]
Chapter 1.
LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1428.
[1]
LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1521.
[2] [3]
LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1588.
[4]
LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1625.
LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1631.
[5]
LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1663.
[6] [7]
LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1783.
[8] [9] [10] [11]
LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1998.
[12] [13]
LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2072.
LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2080.
LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2089.
LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2111.
[14]
LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2140.
LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2156.
LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2164.
LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2169.
[15]
LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2220.
[16]
LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2254.
LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2254.
LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2256.
LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2258.
LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2275.
LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2288.
LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2288.
[17]
LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2302.
LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2322.
[18] [19]
LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2417.
LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2442.
[20]
LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2477.
LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2489.
[21]
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2523.
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2530.
LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2546.
LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2549.
[22]
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2562.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2566.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2577.
LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2587.
LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2591.
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2593.
LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2604.
LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2605.
[23]
LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2634.
[24]
LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26
79.
LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2688.
LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2698.
LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2703.
LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2713.
[25]
LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2755.
[26]
LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2783.
LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2792.
LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2800.
LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2831.
[27] [28]
LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 
2910.
LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2932.
[29] [30] [31] [32]
LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3143.
LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3144.
LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3152.
LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3164.
LaTeX Warning: Citation `PM' on page 33 undefined on input line 3172.
[33]
LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3193.
LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3193.
LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3194.
LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3194.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3202.
LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3214.
LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3245.
LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3245.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3260.
LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3262.
[34]
LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3277.
[35] [36]
Chapter 2.
[37]
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3376.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3379.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3380.
[38] [39]
LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3516.
LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3517.
[40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54]
[55] [56] [57] [58]
Chapter 3.
LaTeX Warning: Citation `Barrow' on page 59 undefined on input line 4512.
[59] [60] [61]
LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4724.
[62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739
[]\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut
ed to Jan []ukasiewicz
[63] [64]
Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmtt/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
LaTeX Warning: Citation `Tarski1965' on page 65 undefined on input line 4919.
[65]
LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4932.
LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4973.
[66]
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5001.
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5018.
LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5037.
[67] [68] [69] [70]
Overfull \hbox (17.90143pt too wide) in paragraph at lines 5320--5320
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarsk
i's
Overfull \hbox (26.88689pt too wide) in paragraph at lines 5400--5400
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxil
iary 
[71] [72] [73]
LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5722.
LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5723.
LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5724.
LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5724.
[74] [75] [76]
LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5986.
LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5988.
LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5989.
[77] [78] [79] [80] [81] [82]
Package amsmath Warning: Foreign command \atop;
(amsmath)                \frac or \genfrac should be used instead
(amsmath)                 on input line 6661.
[83] [84] [85]
LaTeX Warning: Citation `PM' on page 86 undefined on input line 6946.
[86] [87] [88]
Overfull \hbox (2.4539pt too wide) in paragraph at lines 7289--7289
[]\OT1/cmr/bx/n/12 (-20) The Ax-ioms for Real and Com-plex Num-bers Them-
[89] [90] [91]
LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7649.
[92] [93]
LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7789.
[94] [95] [96] [97]
LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8056.
[98]
LaTeX Warning: Citation `CarneiroND' on page 99 undefined on input line 8093.
LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8109.
[99]
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Ration-
Underfull \hbox (badness 5203) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmtt/m/n/10 pm2.65da
[100] [101]
Overfull \hbox (1.91838pt too wide) in paragraph at lines 8313--8313
[]\OT1/cmtt/m/n/10 The source has 155711 statements; 2254 are $a and 32250 are 
$p.[] 
[102]
LaTeX Warning: Citation `Enderton' on page 103 undefined on input line 8338.
[103] [104]
LaTeX Warning: Citation `Hamilton' on page 105 undefined on input line 8477.
[105] [106] [107] [108] [109] [110]
Chapter 4.
LaTeX Warning: Citation `Russell2' on page 111 undefined on input line 8768.
[111]
LaTeX Warning: Citation `deMillo' on page 112 undefined on input line 8820.
[112] [113] [114] [115] [116] [117] [118]
LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined
(Font)              using `TS1/cmtt/m/n' instead
(Font)              for symbol `textdollar' on input line 9416.
[119] [120] [121] [122] [123] [124]
LaTeX Warning: Citation `Nemeti' on page 125 undefined on input line 9769.
LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9770.
LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9777.
[125] [126] [127] [128] [129] [130] [131]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10257.
[132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143]
[144] [145] [146] [147] [148] [149]
LaTeX Warning: Citation `Behnke' on page 150 undefined on input line 11675.
[150]
LaTeX Warning: Citation `Nemesszeghy' on page 151 undefined on input line 11686
.
LaTeX Warning: Citation `Lejewski' on page 151 undefined on input line 11702.
LaTeX Warning: Citation `Goodstein' on page 151 undefined on input line 11780.
LaTeX Warning: Citation `Robinsont' on page 151 undefined on input line 11789.
[151]
LaTeX Warning: Citation `Quine' on page 152 undefined on input line 11824.
[152] [153] [154]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023
[]\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif
ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases
[155] [156]
Chapter 5.
[157] [158] [159] [160] [161] [162] [163] [164] [165]
Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10
 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m
/n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1
0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth
[166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177]
[178] [179] [180] [181] [182]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[183] [184] [185] [186]
Appendix B.
[187] [188]
Appendix C.
LaTeX Warning: Citation `Campbell' on page 189 undefined on input line 14141.
LaTeX Warning: Citation `Munkres' on page 189 undefined on input line 14155.
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14172.
[189] [190] [191]
LaTeX Warning: Citation `Nemeti' on page 192 undefined on input line 14359.
[192] [193] [194]
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14580.
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14581.
[195] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg)
LaTeX Warning: Citation `Tarski1965' on page 196 undefined on input line 14635.
[196] [197]
LaTeX Warning: Citation `Hamilton' on page 198 undefined on input line 14805.
LaTeX Warning: Citation `Tarski1965' on page 198 undefined on input line 14812.
[198]
LaTeX Warning: Citation `Kalish' on page 199 undefined on input line 14872.
LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14885.
LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14896.
[199] [200] [201]
LaTeX Warning: Citation `Takeuti' on page 202 undefined on input line 15136.
LaTeX Warning: Citation `Quine' on page 202 undefined on input line 15137.
[202] [203] [204] [205] [206]
Appendix D.
[207] [208]
LaTeX Warning: Citation `Hofstadter' on page 209 undefined on input line 15417.
[209] [210]
Appendix E.
[211] [212] [213] [214]
No file metamath.bbl.
(./metamath.ind) (./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
LaTeX Warning: There were undefined references.
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
itt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texli
ve/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/
fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-su
per/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sft
t0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1000.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.pfb>
Output written on metamath.pdf (232 pages, 1098050 bytes).
Transcript written on metamath.log.
+ bibtex metamath
This is BibTeX, Version 0.99d (TeX Live 2023)
The top-level auxiliary file: metamath.aux
The style file: plain.bst
Database file #1: metamath.bib
Warning--empty journal in CarneiroND
Warning--empty journal in Knill
Warning--empty publisher in Clemente
Warning--empty journal in Schmidt
Warning--empty journal in Wiedijk-revisited
(There were 5 warnings)
+ makeindex metamath.idx
This is makeindex, version 2.17 [TeX Live 2023] (kpathsea + Thai support).
Scanning input file metamath.idx.....done (1591 entries accepted, 0 rejected).
Sorting entries................done (18500 comparisons).
Generating output file metamath.ind.....done (930 lines written, 0 warnings).
Output written in metamath.ind.
Transcript written in metamath.ilg.
+ pdflatex metamath
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2022-11-01> patch level 1
L3 programming layer <2023-02-22>
LaTeX Info: File `realref.sty' already exists on the system.
            Not generating it from this source.
LaTeX Info: File `metamath.bib' already exists on the system.
            Not generating it from this source.
(/usr/share/texlive/texmf-dist/tex/latex/base/book.cls
Document Class: book 2022/07/02 v1.4n Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
(/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty)
(/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty)
(/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty)
(/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty)
(/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)
(/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty
(/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty)
(/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty
(/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def)))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/var/lib/texm
f/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd)
[4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 108.
[5{/usr/share/texlive/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}]
[6]) [7] [8] [9] [10]
LaTeX Warning: Citation `DBLP:journals/corr/Carneiro14' on page xi undefined on
 input line 1118.
LaTeX Warning: Citation `DBLP:journals/corr/Whalen16' on page xi undefined on i
nput line 1123.
[11] [12]
LaTeX Warning: Citation `Barrow' on page xiii undefined on input line 1220.
[13]
LaTeX Warning: Citation `Davis' on page xiv undefined on input line 1245.
[14] [15] [16] [17] [18]
Chapter 1.
LaTeX Warning: Citation `Davis' on page 1 undefined on input line 1428.
[1]
LaTeX Warning: Citation `Munkres' on page 2 undefined on input line 1521.
[2] [3]
LaTeX Warning: Citation `Whitehead' on page 4 undefined on input line 1588.
[4]
LaTeX Warning: Citation `Landau' on page 5 undefined on input line 1625.
LaTeX Warning: Citation `Guillen' on page 5 undefined on input line 1631.
[5]
LaTeX Warning: Citation `Rucker' on page 6 undefined on input line 1663.
[6] [7]
LaTeX Warning: Citation `Solow' on page 8 undefined on input line 1783.
[8] [9] [10] [11]
LaTeX Warning: Citation `Davis' on page 12 undefined on input line 1998.
[12] [13]
LaTeX Warning: Citation `Edwards' on page 14 undefined on input line 2072.
LaTeX Warning: Citation `Davis' on page 14 undefined on input line 2080.
LaTeX Warning: Citation `Wang' on page 14 undefined on input line 2089.
LaTeX Warning: Citation `deMillo' on page 14 undefined on input line 2111.
[14]
LaTeX Warning: Citation `Mathias' on page 15 undefined on input line 2140.
LaTeX Warning: Citation `Moore' on page 15 undefined on input line 2156.
LaTeX Warning: Citation `Russell' on page 15 undefined on input line 2164.
LaTeX Warning: Citation `Davis' on page 15 undefined on input line 2169.
[15]
LaTeX Warning: Citation `deMillo' on page 16 undefined on input line 2220.
[16]
LaTeX Warning: Citation `Anderson' on page 17 undefined on input line 2254.
LaTeX Warning: Citation `MegillBunder' on page 17 undefined on input line 2254.
LaTeX Warning: Citation `Boolos' on page 17 undefined on input line 2256.
LaTeX Warning: Citation `Pavicic' on page 17 undefined on input line 2258.
LaTeX Warning: Citation `Tymoczko' on page 17 undefined on input line 2275.
LaTeX Warning: Citation `Enderton' on page 17 undefined on input line 2288.
LaTeX Warning: Citation `Curry' on page 17 undefined on input line 2288.
[17]
LaTeX Warning: Citation `Kline' on page 18 undefined on input line 2302.
LaTeX Warning: Citation `Klinel' on page 18 undefined on input line 2322.
[18] [19]
LaTeX Warning: Citation `Harrison' on page 20 undefined on input line 2417.
LaTeX Warning: Citation `Albers' on page 20 undefined on input line 2442.
[20]
LaTeX Warning: Citation `Tymoczko' on page 21 undefined on input line 2477.
LaTeX Warning: Citation `Swart' on page 21 undefined on input line 2489.
[21]
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2523.
LaTeX Warning: Citation `deMillo' on page 22 undefined on input line 2530.
LaTeX Warning: Citation `Stark' on page 22 undefined on input line 2546.
LaTeX Warning: Citation `Kramer' on page 22 undefined on input line 2549.
[22]
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2562.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2566.
LaTeX Warning: Citation `Enderton' on page 23 undefined on input line 2577.
LaTeX Warning: Citation `Courant' on page 23 undefined on input line 2587.
LaTeX Warning: Citation `Swart' on page 23 undefined on input line 2591.
LaTeX Warning: Citation `Davis' on page 23 undefined on input line 2593.
LaTeX Warning: Citation `PetersonI' on page 23 undefined on input line 2604.
LaTeX Warning: Citation `Szpiro' on page 23 undefined on input line 2605.
[23]
LaTeX Warning: Citation `Wolfram' on page 24 undefined on input line 2634.
[24]
LaTeX Warning: Citation `Harrison-thesis' on page 25 undefined on input line 26
79.
LaTeX Warning: Citation `Tarski' on page 25 undefined on input line 2688.
LaTeX Warning: Citation `Chou' on page 25 undefined on input line 2698.
LaTeX Warning: Citation `Penrose' on page 25 undefined on input line 2703.
LaTeX Warning: Citation `Robinson' on page 25 undefined on input line 2713.
[25]
LaTeX Warning: Citation `Wos' on page 26 undefined on input line 2755.
[26]
LaTeX Warning: Citation `Wos' on page 27 undefined on input line 2783.
LaTeX Warning: Citation `Megill' on page 27 undefined on input line 2792.
LaTeX Warning: Citation `Bledsoe' on page 27 undefined on input line 2800.
LaTeX Warning: Citation `Harrison' on page 27 undefined on input line 2831.
[27] [28]
LaTeX Warning: Citation `Wiedijk-revisited' on page 29 undefined on input line 
2910.
LaTeX Warning: Citation `Knill' on page 29 undefined on input line 2932.
[29] [30] [31] [32]
LaTeX Warning: Citation `Kline' on page 33 undefined on input line 3143.
LaTeX Warning: Citation `Behnke' on page 33 undefined on input line 3144.
LaTeX Warning: Citation `Shoenfield' on page 33 undefined on input line 3152.
LaTeX Warning: Citation `Davis' on page 33 undefined on input line 3164.
LaTeX Warning: Citation `PM' on page 33 undefined on input line 3172.
[33]
LaTeX Warning: Citation `Hindley' on page 34 undefined on input line 3193.
LaTeX Warning: Citation `Kalman' on page 34 undefined on input line 3193.
LaTeX Warning: Citation `Meredith' on page 34 undefined on input line 3194.
LaTeX Warning: Citation `Peterson' on page 34 undefined on input line 3194.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3202.
LaTeX Warning: Citation `Robinson' on page 34 undefined on input line 3214.
LaTeX Warning: Citation `Herrlich' on page 34 undefined on input line 3245.
LaTeX Warning: Citation `Blass' on page 34 undefined on input line 3245.
LaTeX Warning: Citation `Megill' on page 34 undefined on input line 3260.
LaTeX Warning: Citation `Monks' on page 34 undefined on input line 3262.
[34]
LaTeX Warning: Citation `Leblanc' on page 35 undefined on input line 3277.
[35] [36]
Chapter 2.
[37]
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3376.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3379.
LaTeX Warning: Citation `Mendelson' on page 38 undefined on input line 3380.
[38] [39]
LaTeX Warning: Citation `Rucker' on page 40 undefined on input line 3516.
LaTeX Warning: Citation `Hofstadter' on page 40 undefined on input line 3517.
[40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51] [52] [53] [54]
[55] [56] [57] [58]
Chapter 3.
LaTeX Warning: Citation `Barrow' on page 59 undefined on input line 4512.
[59] [60] [61]
LaTeX Warning: Citation `CAMeredith' on page 62 undefined on input line 4724.
[62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739
[]\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut
ed to Jan []ukasiewicz
[63] [64]
Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmtt/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
LaTeX Warning: Citation `Tarski1965' on page 65 undefined on input line 4919.
[65]
LaTeX Warning: Citation `Tarski1965' on page 66 undefined on input line 4932.
LaTeX Warning: Citation `Megill' on page 66 undefined on input line 4973.
[66]
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5001.
LaTeX Warning: Citation `Megill' on page 67 undefined on input line 5018.
LaTeX Warning: Citation `Hamilton' on page 67 undefined on input line 5037.
[67] [68] [69] [70]
Overfull \hbox (17.90143pt too wide) in paragraph at lines 5320--5320
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarsk
i's
Overfull \hbox (26.88689pt too wide) in paragraph at lines 5400--5400
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxil
iary 
[71] [72] [73]
LaTeX Warning: Citation `Takeuti' on page 74 undefined on input line 5722.
LaTeX Warning: Citation `Quine' on page 74 undefined on input line 5723.
LaTeX Warning: Citation `Bell' on page 74 undefined on input line 5724.
LaTeX Warning: Citation `Enderton' on page 74 undefined on input line 5724.
[74] [75] [76]
LaTeX Warning: Citation `Levy' on page 77 undefined on input line 5986.
LaTeX Warning: Citation `Quine' on page 77 undefined on input line 5988.
LaTeX Warning: Citation `Takeuti' on page 77 undefined on input line 5989.
[77] [78] [79] [80] [81] [82]
Package amsmath Warning: Foreign command \atop;
(amsmath)                \frac or \genfrac should be used instead
(amsmath)                 on input line 6661.
[83] [84] [85]
LaTeX Warning: Citation `PM' on page 86 undefined on input line 6946.
[86] [87] [88]
Overfull \hbox (2.4539pt too wide) in paragraph at lines 7289--7289
[]\OT1/cmr/bx/n/12 (-20) The Ax-ioms for Real and Com-plex Num-bers Them-
[89] [90] [91]
LaTeX Warning: Citation `Schmidt' on page 92 undefined on input line 7649.
[92] [93]
LaTeX Warning: Citation `Margaris' on page 94 undefined on input line 7789.
[94] [95] [96] [97]
LaTeX Warning: Citation `Indrzejczak' on page 98 undefined on input line 8056.
[98]
LaTeX Warning: Citation `CarneiroND' on page 99 undefined on input line 8093.
LaTeX Warning: Citation `Clemente' on page 99 undefined on input line 8109.
[99]
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Ration-
Underfull \hbox (badness 5203) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmtt/m/n/10 pm2.65da
[100] [101]
Overfull \hbox (1.91838pt too wide) in paragraph at lines 8313--8313
[]\OT1/cmtt/m/n/10 The source has 155711 statements; 2254 are $a and 32250 are 
$p.[] 
[102]
LaTeX Warning: Citation `Enderton' on page 103 undefined on input line 8338.
[103] [104]
LaTeX Warning: Citation `Hamilton' on page 105 undefined on input line 8477.
[105] [106] [107] [108] [109] [110]
Chapter 4.
LaTeX Warning: Citation `Russell2' on page 111 undefined on input line 8768.
[111]
LaTeX Warning: Citation `deMillo' on page 112 undefined on input line 8820.
[112] [113] [114] [115] [116] [117] [118]
LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined
(Font)              using `TS1/cmtt/m/n' instead
(Font)              for symbol `textdollar' on input line 9416.
[119] [120] [121] [122] [123] [124]
LaTeX Warning: Citation `Nemeti' on page 125 undefined on input line 9769.
LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9770.
LaTeX Warning: Citation `Megill' on page 125 undefined on input line 9777.
[125] [126] [127] [128] [129] [130] [131]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10257.
[132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143]
[144] [145] [146] [147] [148] [149]
LaTeX Warning: Citation `Behnke' on page 150 undefined on input line 11675.
[150]
LaTeX Warning: Citation `Nemesszeghy' on page 151 undefined on input line 11686
.
LaTeX Warning: Citation `Lejewski' on page 151 undefined on input line 11702.
LaTeX Warning: Citation `Goodstein' on page 151 undefined on input line 11780.
LaTeX Warning: Citation `Robinsont' on page 151 undefined on input line 11789.
[151]
LaTeX Warning: Citation `Quine' on page 152 undefined on input line 11824.
[152] [153] [154]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023
[]\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif
ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases
[155] [156]
Chapter 5.
[157] [158] [159] [160] [161] [162] [163] [164] [165]
Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10
 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m
/n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1
0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth
[166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177]
[178] [179] [180] [181] [182]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[183] [184] [185] [186]
Appendix B.
[187] [188]
Appendix C.
LaTeX Warning: Citation `Campbell' on page 189 undefined on input line 14141.
LaTeX Warning: Citation `Munkres' on page 189 undefined on input line 14155.
LaTeX Warning: Citation `Tarski1965' on page 189 undefined on input line 14172.
[189] [190] [191]
LaTeX Warning: Citation `Nemeti' on page 192 undefined on input line 14359.
[192] [193] [194]
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14580.
LaTeX Warning: Citation `Tarski1965' on page 195 undefined on input line 14581.
[195] (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg)
LaTeX Warning: Citation `Tarski1965' on page 196 undefined on input line 14635.
[196] [197]
LaTeX Warning: Citation `Hamilton' on page 198 undefined on input line 14805.
LaTeX Warning: Citation `Tarski1965' on page 198 undefined on input line 14812.
[198]
LaTeX Warning: Citation `Kalish' on page 199 undefined on input line 14872.
LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14885.
LaTeX Warning: Citation `Megill' on page 199 undefined on input line 14896.
[199] [200] [201]
LaTeX Warning: Citation `Takeuti' on page 202 undefined on input line 15136.
LaTeX Warning: Citation `Quine' on page 202 undefined on input line 15137.
[202] [203] [204] [205] [206]
Appendix D.
[207] [208]
LaTeX Warning: Citation `Hofstadter' on page 209 undefined on input line 15417.
[209] [210]
Appendix E.
[211] [212] [213] [214] (./metamath.bbl [215] [216] [217] [218] [219]) [220]
(./metamath.ind [221] [222] [223] [224] [225] [226] [227] [228] [229])
(./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
LaTeX Warning: There were undefined references.
LaTeX Warning: Label(s) may have changed. Rerun to get cross-references right.
Package rerunfilecheck Warning: File `metamath.out' has changed.
(rerunfilecheck)                Rerun to get outlines right
(rerunfilecheck)                or use package `bookmark'.
 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmbx8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/ams
fonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts
/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cm
itt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi10.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/share/texli
ve/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texmf-dist/
fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publ
ic/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfo
nts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm
/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy6
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></usr/sha
re/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/texlive/te
xmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/texmf-di
st/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/p
ublic/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pu
blic/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-su
per/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sft
t0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1000.p
fb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.pfb>
Output written on metamath.pdf (247 pages, 1179993 bytes).
Transcript written on metamath.log.
+ pdflatex metamath
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2022-11-01> patch level 1
L3 programming layer <2023-02-22>
LaTeX Info: File `realref.sty' already exists on the system.
            Not generating it from this source.
LaTeX Info: File `metamath.bib' already exists on the system.
            Not generating it from this source.
(/usr/share/texlive/texmf-dist/tex/latex/base/book.cls
Document Class: book 2022/07/02 v1.4n Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
(/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty)
(/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty)
(/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty)
(/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty)
(/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)
(/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty
(/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty)
(/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty
(/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def)))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/var/lib/texm
f/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd)
[4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 108.
[5{/usr/share/texlive/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}]
[6]) [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18]
Chapter 1.
[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]
Chapter 2.
[37] [38] [39] [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51]
[52] [53] [54] [55] [56] [57] [58]
Chapter 3.
[59] [60] [61] [62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739
[]\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut
ed to Jan []ukasiewicz
[63] [64]
Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmtt/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
[65] [66] [67] [68] [69] [70]
Overfull \hbox (17.90143pt too wide) in paragraph at lines 5320--5320
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarsk
i's
Overfull \hbox (26.88689pt too wide) in paragraph at lines 5400--5400
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxil
iary 
[71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82]
Package amsmath Warning: Foreign command \atop;
(amsmath)                \frac or \genfrac should be used instead
(amsmath)                 on input line 6661.
[83] [84] [85] [86] [87] [88]
Overfull \hbox (2.4539pt too wide) in paragraph at lines 7289--7289
[]\OT1/cmr/bx/n/12 (-20) The Ax-ioms for Real and Com-plex Num-bers Them-
[89] [90] [91] [92] [93] [94] [95] [96] [97] [98] [99]
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Ration-
Underfull \hbox (badness 5203) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmtt/m/n/10 pm2.65da
[100] [101]
Overfull \hbox (1.91838pt too wide) in paragraph at lines 8313--8313
[]\OT1/cmtt/m/n/10 The source has 155711 statements; 2254 are $a and 32250 are 
$p.[] 
[102] [103] [104] [105] [106] [107] [108] [109] [110]
Chapter 4.
[111] [112] [113] [114] [115] [116] [117] [118]
LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined
(Font)              using `TS1/cmtt/m/n' instead
(Font)              for symbol `textdollar' on input line 9416.
[119] [120] [121] [122] [123] [124] [125] [126] [127] [128] [129] [130]
[131]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10257.
[132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143]
[144] [145] [146] [147] [148] [149] [150] [151] [152] [153] [154]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023
[]\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif
ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases
[155] [156]
Chapter 5.
[157] [158] [159] [160] [161] [162] [163] [164] [165]
Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10
 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m
/n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1
0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth
[166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177]
[178] [179] [180] [181] [182]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[183] [184] [185] [186]
Appendix B.
[187] [188]
Appendix C.
[189] [190] [191] [192] [193] [194] [195]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) [196] [197]
[198] [199] [200] [201] [202] [203] [204] [205] [206]
Appendix D.
[207] [208] [209] [210]
Appendix E.
[211] [212] [213] [214] (./metamath.bbl [215] [216] [217] [218] [219]) [220]
(./metamath.ind [221] [222] [223] [224] [225] [226] [227] [228] [229])
(./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/
cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texli
ve/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
m/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/cm-super/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-su
per/sftt0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sft
t1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.p
fb>
Output written on metamath.pdf (247 pages, 1176827 bytes).
Transcript written on metamath.log.
+ pdflatex metamath
This is pdfTeX, Version 3.141592653-2.6-1.40.25 (TeX Live 2023) (preloaded format=pdflatex)
 restricted \write18 enabled.
entering extended mode
(./metamath.tex
LaTeX2e <2022-11-01> patch level 1
L3 programming layer <2023-02-22>
LaTeX Info: File `realref.sty' already exists on the system.
            Not generating it from this source.
LaTeX Info: File `metamath.bib' already exists on the system.
            Not generating it from this source.
(/usr/share/texlive/texmf-dist/tex/latex/base/book.cls
Document Class: book 2022/07/02 v1.4n Standard LaTeX document class
(/usr/share/texlive/texmf-dist/tex/latex/base/leqno.clo)
(/usr/share/texlive/texmf-dist/tex/latex/base/bk10.clo))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hyperref.sty
(/usr/share/texlive/texmf-dist/tex/generic/ltxcmds/ltxcmds.sty)
(/usr/share/texlive/texmf-dist/tex/generic/iftex/iftex.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdftexcmds/pdftexcmds.sty
(/usr/share/texlive/texmf-dist/tex/generic/infwarerr/infwarerr.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/keyval.sty)
(/usr/share/texlive/texmf-dist/tex/latex/kvsetkeys/kvsetkeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/kvdefinekeys/kvdefinekeys.sty)
(/usr/share/texlive/texmf-dist/tex/generic/pdfescape/pdfescape.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hycolor/hycolor.sty)
(/usr/share/texlive/texmf-dist/tex/latex/letltxmacro/letltxmacro.sty)
(/usr/share/texlive/texmf-dist/tex/latex/auxhook/auxhook.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/nameref.sty
(/usr/share/texlive/texmf-dist/tex/latex/refcount/refcount.sty)
(/usr/share/texlive/texmf-dist/tex/generic/gettitlestring/gettitlestring.sty
(/usr/share/texlive/texmf-dist/tex/latex/kvoptions/kvoptions.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/pd1enc.def)
(/usr/share/texlive/texmf-dist/tex/generic/intcalc/intcalc.sty)
(/usr/share/texlive/texmf-dist/tex/generic/etexcmds/etexcmds.sty)
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/puenc.def)
(/usr/share/texlive/texmf-dist/tex/latex/url/url.sty)
(/usr/share/texlive/texmf-dist/tex/generic/bitset/bitset.sty
(/usr/share/texlive/texmf-dist/tex/generic/bigintcalc/bigintcalc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/base/atbegshi-ltx.sty))
(/usr/share/texlive/texmf-dist/tex/latex/hyperref/hpdftex.def
(/usr/share/texlive/texmf-dist/tex/latex/base/atveryend-ltx.sty)
(/usr/share/texlive/texmf-dist/tex/latex/rerunfilecheck/rerunfilecheck.sty
(/usr/share/texlive/texmf-dist/tex/generic/uniquecounter/uniquecounter.sty)))
(/usr/share/texlive/texmf-dist/tex/latex/needspace/needspace.sty)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/breqn.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3kernel/expl3.sty
(/usr/share/texlive/texmf-dist/tex/latex/l3backend/l3backend-pdftex.def))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsmath.sty
For additional information on amsmath, use the `?' option.
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amstext.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsgen.sty))
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsbsy.sty)
(/usr/share/texlive/texmf-dist/tex/latex/amsmath/amsopn.sty))
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphicx.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/graphics.sty
(/usr/share/texlive/texmf-dist/tex/latex/graphics/trig.sty)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-cfg/graphics.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/graphics-def/pdftex.def)))
(/usr/share/texlive/texmf-dist/tex/latex/breqn/flexisym.sty
(/usr/share/texlive/texmf-dist/tex/latex/breqn/cmbase.sym)
(/usr/share/texlive/texmf-dist/tex/latex/breqn/mathstyle.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/calc.sty))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.sty
(/usr/share/texlive/texmf-dist/tex/latex/etoolbox/etoolbox.sty)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype-pdftex.def)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/microtype.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/makecell/makecell.sty
(/usr/share/texlive/texmf-dist/tex/latex/tools/array.sty))
(/usr/share/texlive/texmf-dist/tex/latex/tools/longtable.sty)
(/usr/share/texlive/texmf-dist/tex/latex/tabu/tabu.sty
(/usr/share/texlive/texmf-dist/tex/latex/varwidth/varwidth.sty)) (./realref.sty
) (/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amssymb.sty
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/amsfonts.sty))
(/usr/share/texlive/texmf-dist/tex/latex/anysize/anysize.sty
document style option `anysize' loaded
Michael Salzenberg, Thomas Esser, Dirk Hillbrecht
Version 1.0, Aug 13, 1994
) (./special-settings.sty)
Writing index file metamath.idx
(./metamath.aux) (./metamath.out) (./metamath.out)
(/usr/share/texlive/texmf-dist/tex/context/base/mkii/supp-pdf.mkii
[Loading MPS to PDF converter (version 2006.09.02).]
) (/usr/share/texlive/texmf-dist/tex/latex/epstopdf-pkg/epstopdf-base.sty
(/usr/share/texlive/texmf-dist/tex/latex/latexconfig/epstopdf-sys.cfg))
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-cmr.cfg) [1{/var/lib/texm
f/fonts/map/pdftex/updmap/pdftex.map}]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsa.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msa.cfg)
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/umsb.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-msb.cfg) [2]
(./metamath.toc [3] (/usr/share/texlive/texmf-dist/tex/latex/base/ts1cmtt.fd)
[4]
LaTeX Font Warning: Font shape `OMS/cmtt/m/n' undefined
(Font)              using `OMS/cmsy/m/n' instead
(Font)              for symbol `textbraceleft' on input line 108.
[5{/usr/share/texlive/texmf-dist/fonts/enc/dvips/cm-super/cm-super-ts1.enc}]
[6]) [7] [8] [9] [10] [11] [12] [13] [14] [15] [16] [17] [18]
Chapter 1.
[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]
Chapter 2.
[37] [38] [39] [40] [41] [42] [43] [44] [45] [46] [47] [48] [49] [50] [51]
[52] [53] [54] [55] [56] [57] [58]
Chapter 3.
[59] [60] [61] [62]
Overfull \hbox (5.00305pt too wide) in paragraph at lines 4735--4739
[]\OT1/cmr/m/n/10 (-20) These three ax-ioms are widely used. They are at-tribut
ed to Jan []ukasiewicz
[63] [64]
Overfull \hbox (0.69049pt too wide) in paragraph at lines 4868--4873
\OT1/cmr/m/n/10 (-20) theorem, then $\OMS/cmtt/m/n/10 8\OML/cmm/m/it/10 x '$ \O
T1/cmr/m/n/10 (-20) is also a theorem[]. This is called the rule of ``generaliz
ation.''[]
[65] [66] [67] [68] [69] [70]
Overfull \hbox (17.90143pt too wide) in paragraph at lines 5320--5320
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Tarsk
i's
Overfull \hbox (26.88689pt too wide) in paragraph at lines 5400--5400
[]\OT1/cmr/bx/n/12 (-20) Axioms of Pred-i-cate Cal-cu-lus with Equality---Auxil
iary 
[71] [72] [73] [74] [75] [76] [77] [78] [79] [80] [81] [82]
Package amsmath Warning: Foreign command \atop;
(amsmath)                \frac or \genfrac should be used instead
(amsmath)                 on input line 6661.
[83] [84] [85] [86] [87] [88]
Overfull \hbox (2.4539pt too wide) in paragraph at lines 7289--7289
[]\OT1/cmr/bx/n/12 (-20) The Ax-ioms for Real and Com-plex Num-bers Them-
[89] [90] [91] [92] [93] [94] [95] [96] [97] [98] [99]
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND Ex-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Trans-
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) ND
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
\OT1/cmr/bx/n/10 (+20) Ration-
Underfull \hbox (badness 5203) in paragraph at lines 8177--8177
[]\OT1/cmr/bx/n/10 (+20) MPE Ra-
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 2478) in paragraph at lines 8177--8177
[]\TS1/cmr/m/n/10 (+20) $\OT1/cmr/m/n/10 (+20) e; \OT1/cmtt/m/n/10 adantr
Underfull \hbox (badness 10000) in paragraph at lines 8177--8177
[]\OT1/cmtt/m/n/10 pm2.65da
[100] [101]
Overfull \hbox (1.91838pt too wide) in paragraph at lines 8313--8313
[]\OT1/cmtt/m/n/10 The source has 155711 statements; 2254 are $a and 32250 are 
$p.[] 
[102] [103] [104] [105] [106] [107] [108] [109] [110]
Chapter 4.
[111] [112] [113] [114] [115] [116] [117] [118]
LaTeX Font Warning: Font shape `TS1/cmtt/bx/n' undefined
(Font)              using `TS1/cmtt/m/n' instead
(Font)              for symbol `textdollar' on input line 9416.
[119] [120] [121] [122] [123] [124] [125] [126] [127] [128] [129] [130]
[131]
LaTeX Font Warning: Font shape `OMS/cmtt/bx/n' undefined
(Font)              using `OMS/cmtt/m/n' instead
(Font)              for symbol `textbraceleft' on input line 10257.
[132] [133] [134] [135] [136] [137] [138] [139] [140] [141] [142] [143]
[144] [145] [146] [147] [148] [149] [150] [151] [152] [153] [154]
Overfull \hbox (1.59137pt too wide) in paragraph at lines 12015--12023
[]\OT1/cmr/m/n/10 (-20) Second, we run a def-i-ni-tion sound-ness check spe-cif
ic to \OT1/cmtt/m/n/10 set.mm \OT1/cmr/m/n/10 (-20) or databases
[155] [156]
Chapter 5.
[157] [158] [159] [160] [161] [162] [163] [164] [165]
Overfull \hbox (11.18817pt too wide) in paragraph at lines 12675--12677
\OT1/cmr/m/n/10 (-20) Syntax: \OT1/cmtt/m/n/10 show trace_back \OT1/cmr/m/it/10
 (-20) label-match \OT1/cmr/m/n/10 (-20) [\OT1/cmtt/m/n/10 /essential\OT1/cmr/m
/n/10 (-20) ] [\OT1/cmtt/m/n/10 /axioms\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/1
0 /tree\OT1/cmr/m/n/10 (-20) ] [\OT1/cmtt/m/n/10 /depth
[166] [167] [168] [169] [170] [171] [172] [173] [174] [175] [176] [177]
[178] [179] [180] [181] [182]
Appendix A.
Underfull \hbox (badness 3780) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Biconditional (aka is-equals for
Underfull \hbox (badness 4266) in paragraph at lines 13874--13874
[]\OT1/cmr/m/n/10 (+20) Complex num-ber mul-ti-pli-ca-tion;
[183] [184] [185] [186]
Appendix B.
[187] [188]
Appendix C.
[189] [190] [191] [192] [193] [194] [195]
(/usr/share/texlive/texmf-dist/tex/latex/amsfonts/ueuf.fd)
(/usr/share/texlive/texmf-dist/tex/latex/microtype/mt-euf.cfg) [196] [197]
[198] [199] [200] [201] [202] [203] [204] [205] [206]
Appendix D.
[207] [208] [209] [210]
Appendix E.
[211] [212] [213] [214] (./metamath.bbl [215] [216] [217] [218] [219]) [220]
(./metamath.ind [221] [222] [223] [224] [225] [226] [227] [228] [229])
(./metamath.aux)
LaTeX Font Warning: Some font shapes were not available, defaults substituted.
 )
(see the transcript file for additional information)</usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmbx10.pfb></usr/share/texlive/texmf-dist/fo
nts/type1/public/amsfonts/cm/cmbx12.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/cm/cmbx7.pfb></usr/share/texlive/texmf-dist/fonts/type1/pub
lic/amsfonts/cm/cmcsc10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/a
msfonts/cm/cmex10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfont
s/cm/cmitt10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/
cmmi10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi6.
pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi7.pfb></u
sr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmmi8.pfb></usr/shar
e/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmr10.pfb></usr/share/texli
ve/texmf-dist/fonts/type1/public/amsfonts/cm/cmr12.pfb></usr/share/texlive/texm
f-dist/fonts/type1/public/amsfonts/cm/cmr6.pfb></usr/share/texlive/texmf-dist/f
onts/type1/public/amsfonts/cm/cmr7.pfb></usr/share/texlive/texmf-dist/fonts/typ
e1/public/amsfonts/cm/cmr8.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/amsfonts/cm/cmsl10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsf
onts/cm/cmsy10.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/c
m/cmsy6.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy7
.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmsy8.pfb></
usr/share/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti10.pfb></usr/sh
are/texlive/texmf-dist/fonts/type1/public/amsfonts/cm/cmti8.pfb></usr/share/tex
live/texmf-dist/fonts/type1/public/amsfonts/cm/cmtt10.pfb></usr/share/texlive/t
exmf-dist/fonts/type1/public/amsfonts/cm/cmtt12.pfb></usr/share/texlive/texmf-d
ist/fonts/type1/public/amsfonts/cm/cmtt8.pfb></usr/share/texlive/texmf-dist/fon
ts/type1/public/amsfonts/euler/eufm10.pfb></usr/share/texlive/texmf-dist/fonts/
type1/public/amsfonts/symbols/msam10.pfb></usr/share/texlive/texmf-dist/fonts/t
ype1/public/amsfonts/symbols/msbm10.pfb></usr/share/texlive/texmf-dist/fonts/ty
pe1/public/amsfonts/symbols/msbm7.pfb></usr/share/texlive/texmf-dist/fonts/type
1/public/cm-super/sfbx1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/publi
c/cm-super/sfrm1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-su
per/sftt0800.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sft
t1000.pfb></usr/share/texlive/texmf-dist/fonts/type1/public/cm-super/sftt1200.p
fb>
Output written on metamath.pdf (247 pages, 1176827 bytes).
Transcript written on metamath.log.
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%install): /bin/sh -e /var/tmp/rpm-tmp.r3kPFz
+ umask 022
+ cd /builddir/build/BUILD
+ '[' /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64 '!=' / ']'
+ rm -rf /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64
++ dirname /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64
+ mkdir -p /builddir/build/BUILDROOT
+ mkdir /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64
+ CFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CFLAGS
+ CXXFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CXXFLAGS
+ FFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FFLAGS
+ FCFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed   -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes '
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd metamath
+ /usr/bin/make install DESTDIR=/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64 'INSTALL=/usr/bin/install -p'
make[1]: Entering directory '/builddir/build/BUILD/metamath'
 /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/bin'
  /usr/bin/install -p metamath '/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/bin'
 /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/metamath'
 /usr/bin/install -p -m 644 big-unifier.mm demo0.mm miu.mm peano.mm ql.mm set.mm '/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/metamath'
 /usr/bin/mkdir -p '/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/man/man1'
 /usr/bin/install -p -m 644 metamath.1 '/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/man/man1'
make[1]: Leaving directory '/builddir/build/BUILD/metamath'
+ cp -p big-unifier.mm demo0.mm hol.mm iset.mm miu.mm nf.mm peano.mm ql.mm set.mm /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/metamath
+ mkdir -p /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/doc/metamath
+ cp -p metamath.pdf /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/doc/metamath
+ /usr/bin/find-debuginfo -j4 --strict-build-id -m -i --build-id-seed 0.198-7.fc40 --unique-debug-suffix -0.198-7.fc40.riscv64 --unique-debug-src-base metamath-0.198-7.fc40.riscv64 --run-dwz --dwz-low-mem-die-limit 10000000 --dwz-max-die-limit 50000000 -S debugsourcefiles.list /builddir/build/BUILD/metamath
find-debuginfo: starting
Extracting debug info from 1 files
DWARF-compressing 1 files
sepdebugcrcfix: Updated 1 CRC32s, 0 CRC32s did match.
Creating .debug symlinks for symlinks to ELF files
Copying sources found by 'debugedit -l' to /usr/src/debug/metamath-0.198-7.fc40.riscv64
3819 blocks
find-debuginfo: done
+ /usr/lib/rpm/check-buildroot
+ /usr/lib/rpm/redhat/brp-ldconfig
+ /usr/lib/rpm/brp-compress
+ /usr/lib/rpm/redhat/brp-strip-lto /usr/bin/strip
+ /usr/lib/rpm/brp-strip-static-archive /usr/bin/strip
+ /usr/lib/rpm/check-rpaths
+ /usr/lib/rpm/redhat/brp-mangle-shebangs
+ /usr/lib/rpm/brp-remove-la-files
+ env /usr/lib/rpm/redhat/brp-python-bytecompile '' 1 0 -j4
+ /usr/lib/rpm/redhat/brp-python-hardlink
Executing(%check): /bin/sh -e /var/tmp/rpm-tmp.cWRmpX
+ umask 022
+ cd /builddir/build/BUILD
+ CFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CFLAGS
+ CXXFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Werror=format-security -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer '
+ export CXXFLAGS
+ FFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FFLAGS
+ FCFLAGS='-O2  -fexceptions -g -grecord-gcc-switches -pipe -Wall -Wp,-U_FORTIFY_SOURCE,-D_FORTIFY_SOURCE=3 -Wp,-D_GLIBCXX_ASSERTIONS -specs=/usr/lib/rpm/redhat/redhat-hardened-cc1 -fstack-protector-strong -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -fasynchronous-unwind-tables -fno-omit-frame-pointer -I/usr/lib64/gfortran/modules '
+ export FCFLAGS
+ VALAFLAGS=-g
+ export VALAFLAGS
+ RUSTFLAGS='-Copt-level=3 -Cdebuginfo=2 -Ccodegen-units=1 -Cstrip=none -Cforce-frame-pointers=yes -Clink-arg=-specs=/usr/lib/rpm/redhat/redhat-package-notes'
+ export RUSTFLAGS
+ LDFLAGS='-Wl,-z,relro -Wl,--as-needed   -Wl,-z,now -specs=/usr/lib/rpm/redhat/redhat-hardened-ld-errors -specs=/usr/lib/rpm/redhat/redhat-hardened-ld -specs=/usr/lib/rpm/redhat/redhat-annobin-cc1  -Wl,--build-id=sha1 -specs=/usr/lib/rpm/redhat/redhat-package-notes '
+ export LDFLAGS
+ LT_SYS_LIBRARY_PATH=/usr/lib64:
+ export LT_SYS_LIBRARY_PATH
+ CC=gcc
+ export CC
+ CXX=g++
+ export CXX
+ cd metamath
+ for fil in *.mm
+ run_verify big-unifier.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "big-unifier.mm"... 21721 bytes
21721 bytes were read into the source buffer.
The source has 29 statements; 4 are $a and 2 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.07 s.
MM> + for fil in *.mm
+ run_verify demo0.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "demo0.mm"... 1364 bytes
1364 bytes were read into the source buffer.
The source has 19 statements; 7 are $a and 1 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.00 s.
MM> + for fil in *.mm
+ run_verify hol.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "hol.mm"... 87294 bytes
87294 bytes were read into the source buffer.
The source has 936 statements; 71 are $a and 138 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.05 s.
MM> + for fil in *.mm
+ run_verify iset.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "iset.mm"... 4653282 bytes
4653282 bytes were read into the source buffer.
The source has 31955 statements; 468 are $a and 9097 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 3.49 s.
MM> + for fil in *.mm
+ run_verify miu.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "miu.mm"... 4660 bytes
4660 bytes were read into the source buffer.
The source has 27 statements; 10 are $a and 1 are $p.
SET EMPTY_SUBSTITUTION was turned ON (allowed) for this database.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.00 s.
MM> + for fil in *.mm
+ run_verify nf.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "nf.mm"... 2977364 bytes
2977364 bytes were read into the source buffer.
The source has 24967 statements; 363 are $a and 5966 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 2.17 s.
MM> + for fil in *.mm
+ run_verify peano.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "peano.mm"... 27968 bytes
27968 bytes were read into the source buffer.
The source has 120 statements; 48 are $a and 0 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.00 s.
MM> + for fil in *.mm
+ run_verify ql.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "ql.mm"... 572529 bytes
572529 bytes were read into the source buffer.
The source has 2768 statements; 77 are $a and 1138 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 0.52 s.
MM> + for fil in *.mm
+ run_verify set.mm
+ ./metamath
Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> Reading source file "set.mm"... 43203944 bytes
43203944 bytes were read into the source buffer.
The source has 201862 statements; 2709 are $a and 39597 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> Continuous scrolling is now in effect.
MM> 0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 47.68 s.
MM> + RPM_EC=0
++ jobs -p
+ exit 0
Processing files: metamath-0.198-7.fc40.riscv64
Executing(%doc): /bin/sh -e /var/tmp/rpm-tmp.BVwzt7
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ DOCDIR=/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/doc/metamath
+ export LC_ALL=
+ LC_ALL=
+ export DOCDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/doc/metamath
+ cp -pr /builddir/build/BUILD/metamath/README.TXT /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/doc/metamath
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.VtzuMZ
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/licenses/metamath
+ export LC_ALL=
+ LC_ALL=
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/licenses/metamath
+ cp -pr /builddir/build/BUILD/metamath/LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/licenses/metamath
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: metamath = 0.198-7.fc40 metamath(riscv-64) = 0.198-7.fc40
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Requires: ld-linux-riscv64-lp64d.so.1()(64bit) ld-linux-riscv64-lp64d.so.1(GLIBC_2.27)(64bit) libc.so.6()(64bit) libc.so.6(GLIBC_2.27)(64bit) libc.so.6(GLIBC_2.34)(64bit) rtld(GNU_HASH)
Suggests: rlwrap
Processing files: metamath-theories-0.198-7.fc40.noarch
Provides: metamath-theories = 0.198-7.fc40
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: metamath-doc-0.198-7.fc40.noarch
Executing(%license): /bin/sh -e /var/tmp/rpm-tmp.Hha0PU
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ LICENSEDIR=/builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/licenses/metamath-doc
+ export LC_ALL=
+ LC_ALL=
+ export LICENSEDIR
+ /usr/bin/mkdir -p /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/licenses/metamath-doc
+ cp -pr /builddir/build/BUILD/metamath/LICENSE.TXT /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64/usr/share/licenses/metamath-doc
+ RPM_EC=0
++ jobs -p
+ exit 0
Provides: metamath-doc = 0.198-7.fc40
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: metamath-debugsource-0.198-7.fc40.riscv64
Provides: metamath-debugsource = 0.198-7.fc40 metamath-debugsource(riscv-64) = 0.198-7.fc40
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Processing files: metamath-debuginfo-0.198-7.fc40.riscv64
Provides: debuginfo(build-id) = 91200cde8c71c17e5b97f4faef36b488c2e470c2 metamath-debuginfo = 0.198-7.fc40 metamath-debuginfo(riscv-64) = 0.198-7.fc40
Requires(rpmlib): rpmlib(CompressedFileNames) <= 3.0.4-1 rpmlib(FileDigests) <= 4.6.0-1 rpmlib(PayloadFilesHavePrefix) <= 4.0-1
Recommends: metamath-debugsource(riscv-64) = 0.198-7.fc40
Checking for unpackaged file(s): /usr/lib/rpm/check-files /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64
Wrote: /builddir/build/RPMS/metamath-doc-0.198-7.fc40.noarch.rpm
Wrote: /builddir/build/RPMS/metamath-0.198-7.fc40.riscv64.rpm
Wrote: /builddir/build/RPMS/metamath-debuginfo-0.198-7.fc40.riscv64.rpm
Wrote: /builddir/build/RPMS/metamath-debugsource-0.198-7.fc40.riscv64.rpm
Wrote: /builddir/build/RPMS/metamath-theories-0.198-7.fc40.noarch.rpm
Executing(%clean): /bin/sh -e /var/tmp/rpm-tmp.xxQbqp
+ umask 022
+ cd /builddir/build/BUILD
+ cd metamath
+ /usr/bin/rm -rf /builddir/build/BUILDROOT/metamath-0.198-7.fc40.riscv64
+ RPM_EC=0
++ jobs -p
+ exit 0
Executing(rmbuild): /bin/sh -e /var/tmp/rpm-tmp.Wna6Qs
+ umask 022
+ cd /builddir/build/BUILD
+ rm -rf /builddir/build/BUILD/metamath-SPECPARTS
+ rm -rf metamath metamath.gemspec
+ RPM_EC=0
++ jobs -p
+ exit 0
Child return code was: 0