The Mizar-TPTP
Semantic Presentation

`abcmiz_0`	`abian`	`absvalue`	`aff_1`	`aff_2`	`aff_3`	`aff_4`	`afinsq_1`	`afproj`	`afvect01`	`afvect0`	`alg_1`
`algseq_1`	`algspec1`	`algstr_1`	`algstr_2`	`algstr_3`	`ali2`	`altcat_1`	`altcat_2`	`altcat_3`	`altcat_4`	`ami_1`	`ami_2`
`ami_3`	`ami_4`	`ami_5`	`ami_6`	`ami_7`	`amistd_1`	`amistd_2`	`amistd_3`	`analmetr`	`analoaf`	`analort`	`anproj_1`
`anproj_2`	`arithm`	`armstrng`	`arytm_0`	`arytm_1`	`arytm_2`	`arytm_3`	`asympt_0`	`asympt_1`	`autalg_1`	`autgroup`	`axioms`
`bagorder`	`bhsp_1`	`bhsp_2`	`bhsp_3`	`bhsp_4`	`bhsp_5`	`bhsp_6`	`bhsp_7`	`bilinear`	`binari_2`	`binari_3`	`binari_4`
`binari_5`	`binari_6`	`binarith`	`binom`	`binop_1`	`binop_2`	`bintree1`	`bintree2`	`birkhoff`	`boolealg`	`boole`	`boolmark`
`borsuk_1`	`borsuk_2`	`borsuk_3`	`borsuk_4`	`borsuk_5`	`borsuk_6`	`brouwer`	`bvfunc10`	`bvfunc11`	`bvfunc13`	`bvfunc14`	`bvfunc_1`
`bvfunc23`	`bvfunc24`	`bvfunc25`	`bvfunc26`	`bvfunc_2`	`bvfunc_3`	`bvfunc_4`	`bvfunc_5`	`bvfunc_6`	`bvfunc_7`	`bvfunc_8`	`bvfunc_9`
`calcul_1`	`calcul_2`	`cantor_1`	`card_1`	`card_2`	`card_3`	`card_4`	`card_5`	`card_fil`	`card_fin`	`card_lar`	`cat_1`
`cat_2`	`cat_3`	`cat_4`	`cat_5`	`catalan1`	`catalg_1`	`cfcont_1`	`cfuncdom`	`cfunct_1`	`chain_1`	`circcmb2`	`circcmb3`
`circcomb`	`circled1`	`circtrm1`	`circuit1`	`circuit2`	`classes1`	`classes2`	`clopban1`	`clopban2`	`clopban3`	`clopban4`	`closure1`
`closure2`	`closure3`	`clvect_1`	`clvect_2`	`clvect_3`	`cohsp_1`	`coh_sp`	`collsp`	`commacat`	`complex1`	`complex2`	`complfld`
`complsp1`	`complsp2`	`comptrig`	`compts_1`	`comput_1`	`comseq_1`	`comseq_2`	`comseq_3`	`conaffm`	`conlat_1`	`conlat_2`	`conmetr1`
`conmetr`	`connsp_1`	`connsp_2`	`connsp_3`	`convex1`	`convex2`	`convex3`	`convfun1`	`cqc_lang`	`cqc_sim1`	`cqc_the1`	`cqc_the2`
`cqc_the3`	`csspace2`	`csspace3`	`csspace4`	`csspace`	`decomp_1`	`dickson`	`diraf`	`dirort`	`domain_1`	`dtconstr`	`dynkin`
`endalg`	`ens_1`	`enumset1`	`eqrel_1`	`equation`	`e_siec`	`euclid_2`	`euclid_3`	`euclid_4`	`euclid_5`	`euclid`	`euclidlp`
`euclmetr`	`euler_1`	`euler_2`	`extens_1`	`extreal1`	`extreal2`	`facirc_1`	`facirc_2`	`fcont_1`	`fcont_2`	`fcont_3`	`fdiff_1`
`fdiff_2`	`fdiff_3`	`fdiff_4`	`fdiff_5`	`fdiff_6`	`ff_siec`	`fib_fusc`	`fib_num2`	`fib_num3`	`fib_num`	`filerec1`	`filter_0`
`filter_1`	`filter_2`	`finseq_1`	`finseq_2`	`finseq_3`	`finseq_4`	`finseq_5`	`finseq_6`	`finseq_7`	`finseq_8`	`finseqop`	`finset_1`
`finsop_1`	`finsub_1`	`fintopo2`	`fintopo3`	`fintopo4`	`fintopo5`	`fin_topo`	`fraenkel`	`frechet2`	`frechet`	`freealg`	`fscirc_1`
`fscirc_2`	`fsm_1`	`fsm_2`	`funcop_1`	`funcsdom`	`funct_1`	`funct_2`	`funct_3`	`funct_4`	`funct_5`	`funct_6`	`funct_7`
`functor0`	`functor1`	`functor2`	`functor3`	`fuzzy_1`	`fuzzy_2`	`fuzzy_3`	`fuzzy_4`	`fvsum_1`	`gate_1`	`gate_2`	`gate_3`
`gate_4`	`gate_5`	`gcd_1`	`genealg1`	`geomtrap`	`glib_000`	`glib_001`	`glib_002`	`glib_003`	`glib_004`	`glib_005`	`goboard1`
`goboard2`	`goboard3`	`goboard4`	`goboard5`	`goboard6`	`goboard7`	`goboard8`	`goboard9`	`gobrd10`	`gobrd11`	`gobrd12`	`gobrd13`
`gobrd14`	`goedelcp`	`graph_1`	`graph_2`	`graph_3`	`graph_4`	`graph_5`	`graphsp`	`grcat_1`	`gr_cy_1`	`gr_cy_2`	`grfunc_1`
`groeb_1`	`groeb_2`	`groeb_3`	`group_1`	`group_2`	`group_3`	`group_4`	`group_5`	`group_6`	`group_7`	`group_8`	`grsolv_1`
`hahnban1`	`hahnban`	`hallmar1`	`hausdorf`	`heine`	`henmodel`	`hermitan`	`hessenbe`	`heyting1`	`heyting2`	`heyting3`	`hidden`
`hilbasis`	`hilbert1`	`hilbert2`	`hilbert3`	`holder_1`	`homothet`	`idea_1`	`ideal_1`	`incproj`	`incsp_1`	`index_1`	`instalg1`
`int_1`	`int_2`	`int_3`	`integra1`	`integra2`	`integra3`	`integra4`	`integra5`	`intpro_1`	`irrat_1`	`isocat_1`	`isocat_2`
`isomichi`	`jct_misc`	`jgraph_1`	`jgraph_2`	`jgraph_3`	`jgraph_4`	`jgraph_5`	`jgraph_6`	`jgraph_7`	`jgraph_8`	`jordan10`	`jordan11`
`jordan12`	`jordan13`	`jordan14`	`jordan15`	`jordan16`	`jordan17`	`jordan18`	`jordan19`	`jordan1a`	`jordan1b`	`jordan1c`	`jordan1d`
`jordan1e`	`jordan1f`	`jordan1g`	`jordan1h`	`jordan1`	`jordan1i`	`jordan1j`	`jordan1k`	`jordan20`	`jordan21`	`jordan22`	`jordan23`
`jordan24`	`jordan2b`	`jordan2c`	`jordan3`	`jordan4`	`jordan5a`	`jordan5b`	`jordan5c`	`jordan5d`	`jordan6`	`jordan7`	`jordan8`
`jordan9`	`jordan_a`	`jordan`	`knaster`	`kurato_1`	`kurato_2`	`lang1`	`latsubgr`	`latsum_1`	`lattice2`	`lattice3`	`lattice4`
`lattice5`	`lattice6`	`lattice7`	`lattice8`	`lattices`	`lfuzzy_0`	`lfuzzy_1`	`l_hospit`	`limfunc1`	`limfunc2`	`limfunc3`	`limfunc4`
`lmod_5`	`lmod_6`	`lmod_7`	`lopban_1`	`lopban_2`	`lopban_3`	`lopban_4`	`lopclset`	`lp_space`	`lukasi_1`	`margrel1`	`mathmorp`
`matrix_1`	`matrix_2`	`matrix_3`	`matrix_4`	`matrix_5`	`matrixc1`	`matrlin`	`mboolean`	`mcart_1`	`mcart_2`	`mcart_3`	`mcart_4`
`mcart_5`	`mcart_6`	`measure1`	`measure2`	`measure3`	`measure4`	`measure5`	`measure6`	`measure7`	`membered`	`mesfunc1`	`mesfunc2`
`mesfunc3`	`mesfunc4`	`metric_1`	`metric_2`	`metric_3`	`metric_4`	`metric_6`	`midsp_1`	`midsp_2`	`midsp_3`	`mod_1`	`mod_2`
`mod_3`	`mod_4`	`modal_1`	`modcat_1`	`monoid_0`	`monoid_1`	`msafree1`	`msafree2`	`msafree3`	`msafree`	`msalimit`	`msaterm`
`msinst_1`	`msscyc_1`	`msscyc_2`	`mssubfam`	`mssublat`	`msualg_1`	`msualg_2`	`msualg_3`	`msualg_4`	`msualg_5`	`msualg_6`	`msualg_7`
`msualg_8`	`msualg_9`	`msuhom_1`	`multop_1`	`nagata_1`	`nagata_2`	`nat_1`	`nat_2`	`nat_3`	`nat_lat`	`nattra_1`	`ncfcont1`
`ncfcont2`	`ndiff_1`	`ndiff_2`	`neckla_2`	`neckla_3`	`necklace`	`net_1`	`newton`	`nfcont_1`	`nfcont_2`	`normform`	`normsp_1`
`numbers`	`numerals`	`openlatt`	`oposet_1`	`oppcat_1`	`orders_1`	`orders_2`	`orders_3`	`orders_4`	`ordinal1`	`ordinal2`	`ordinal3`
`ordinal4`	`o_ring_1`	`o_ring_2`	`o_ring_3`	`ortsp_1`	`osafree`	`osalg_1`	`osalg_2`	`osalg_3`	`osalg_4`	`papdesaf`	`pardepap`
`parsp_1`	`parsp_2`	`partfun1`	`partfun2`	`partfun3`	`partit1`	`partit_2`	`pasch`	`pboole`	`pcomps_1`	`pcomps_2`	`pencil_1`
`pencil_2`	`pencil_3`	`pencil_4`	`pepin`	`petri`	`pnproc_1`	`polyalg1`	`polyeq_1`	`polyeq_2`	`polyeq_3`	`polyeq_4`	`polynom1`
`polynom2`	`polynom3`	`polynom4`	`polynom5`	`polynom6`	`polynom7`	`polyred`	`power`	`pralg_1`	`pralg_2`	`pralg_3`	`pre_circ`
`pre_ff`	`prelamb`	`prepower`	`pre_topc`	`prgcor_1`	`prgcor_2`	`prob_1`	`prob_2`	`prob_3`	`prob_4`	`procal_1`	`projdes1`
`projpl_1`	`projred1`	`projred2`	`prvect_1`	`pscomp_1`	`pua2mss1`	`pythtrip`	`pzfmisc1`	`qc_lang1`	`qc_lang2`	`qc_lang3`	`qc_lang4`
`qmax_1`	`quantal1`	`quin_1`	`quofield`	`radix_1`	`radix_2`	`radix_3`	`radix_4`	`radix_5`	`radix_6`	`rat_1`	`rcomp_1`
`rcomp_2`	`rcomp_3`	`real_1`	`real_2`	`real`	`real_lat`	`realset1`	`realset2`	`realset3`	`rearran1`	`recdef_1`	`recdef_2`
`relat_1`	`relat_2`	`reloc`	`relset_1`	`relset_2`	`revrot_1`	`rewrite1`	`rfinseq2`	`rfinseq`	`rfunct_1`	`rfunct_2`	`rfunct_3`
`rfunct_4`	`rinfsup1`	`ringcat1`	`rlsub_1`	`rlsub_2`	`rltopsp1`	`rlvect_1`	`rlvect_2`	`rlvect_3`	`rlvect_4`	`rlvect_5`	`rmod_2`
`rmod_3`	`rmod_4`	`rmod_5`	`robbins1`	`robbins2`	`robbins3`	`rolle`	`roughs_1`	`rpr_1`	`rsspace2`	`rsspace3`	`rsspace4`
`rsspace`	`rusub_1`	`rusub_2`	`rusub_3`	`rusub_4`	`rusub_5`	`rvsum_1`	`scheme1`	`schems_1`	`scm_1`	`scmbsort`	`scm_comp`
`scmfsa10`	`scmfsa_1`	`scmfsa_2`	`scmfsa_3`	`scmfsa_4`	`scmfsa_5`	`scmfsa6a`	`scmfsa6b`	`scmfsa6c`	`scmfsa7b`	`scmfsa_7`	`scmfsa8a`
`scmfsa8b`	`scmfsa8c`	`scmfsa9a`	`scmfsa_9`	`scm_halt`	`scmisort`	`scmpds_1`	`scmpds_2`	`scmpds_3`	`scmpds_4`	`scmpds_5`	`scmpds_6`
`scmpds_7`	`scmpds_8`	`scmpds_9`	`scmp_gcd`	`scmring1`	`scmring2`	`scmring3`	`scmring4`	`scpinvar`	`scpisort`	`scpqsort`	`semi_af1`
`seq_1`	`seq_2`	`seq_4`	`seqfunc`	`seqm_3`	`series_1`	`series_2`	`series_3`	`series_4`	`series_5`	`setfam_1`	`setlim_1`
`setlim_2`	`setwiseo`	`setwop_2`	`sfmastr1`	`sfmastr2`	`sfmastr3`	`sf_mastr`	`sgraph1`	`sheffer1`	`sheffer2`	`sin_cos2`	`sin_cos3`
`sin_cos4`	`sin_cos5`	`sin_cos6`	`sin_cos7`	`sin_cos8`	`sin_cos`	`sppol_1`	`sppol_2`	`sprect_1`	`sprect_2`	`sprect_3`	`sprect_4`
`sprect_5`	`square_1`	`stirl2_1`	`struct_0`	`sublemma`	`sub_metr`	`subset_1`	`subset`	`substlat`	`substut1`	`substut2`	`supinf_1`
`supinf_2`	`symsp_1`	`sysrel`	`t_0topsp`	`t_1topsp`	`tarski`	`taxonom1`	`taxonom2`	`taylor_1`	`taylor_2`	`tbsp_1`	`tdgroup`
`tdlat_1`	`tdlat_2`	`tdlat_3`	`termord`	`tex_1`	`tex_2`	`tex_3`	`tex_4`	`tietze`	`tmap_1`	`toler_1`	`topalg_1`
`topalg_2`	`topalg_3`	`topalg_4`	`topalg_5`	`topgen_1`	`topgen_2`	`topgen_3`	`topgen_4`	`topgen_5`	`topgrp_1`	`topmetr2`	`topmetr3`
`topmetr`	`topreal1`	`topreal2`	`topreal3`	`topreal4`	`topreal5`	`topreal6`	`topreal7`	`topreal8`	`topreal9`	`topreala`	`toprealb`
`toprns_1`	`tops_1`	`tops_2`	`tops_3`	`transgeo`	`translac`	`treal_1`	`trees_1`	`trees_2`	`trees_3`	`trees_4`	`trees_9`
`trees_a`	`triang_1`	`tsep_1`	`tsep_2`	`tsp_1`	`tsp_2`	`turing_1`	`twoscomp`	`unialg_1`	`unialg_2`	`unialg_3`	`uniform1`
`uniroots`	`uproots`	`urysohn1`	`urysohn2`	`urysohn3`	`valuat_1`	`vectmetr`	`vectsp10`	`vectsp_1`	`vectsp_2`	`vectsp_3`	`vectsp_4`
`vectsp_5`	`vectsp_6`	`vectsp_7`	`vectsp_8`	`vectsp_9`	`vfunct_1`	`vfunct_2`	`waybel_0`	`waybel10`	`waybel11`	`waybel12`	`waybel13`
`waybel14`	`waybel15`	`waybel16`	`waybel17`	`waybel18`	`waybel19`	`waybel_1`	`waybel20`	`waybel21`	`waybel22`	`waybel23`	`waybel24`
`waybel25`	`waybel26`	`waybel27`	`waybel28`	`waybel29`	`waybel_2`	`waybel30`	`waybel31`	`waybel32`	`waybel33`	`waybel34`	`waybel35`
`waybel_3`	`waybel_4`	`waybel_5`	`waybel_6`	`waybel_7`	`waybel_8`	`waybel_9`	`weddwitt`	`weierstr`	`wellfnd1`	`wellord1`	`wellord2`
`wellset1`	`wsierp_1`	`xboole_0`	`xboole_1`	`xcmplx_0`	`xcmplx_1`	`xreal_0`	`xreal_1`	`yellow_0`	`yellow10`	`yellow11`	`yellow12`
`yellow13`	`yellow14`	`yellow15`	`yellow16`	`yellow17`	`yellow18`	`yellow19`	`yellow_1`	`yellow20`	`yellow21`	`yellow_2`	`yellow_3`
`yellow_4`	`yellow_5`	`yellow_6`	`yellow_7`	`yellow_8`	`yellow_9`	`yoneda_1`	`zf_colla`	`zf_fund1`	`zf_fund2`	`zf_lang1`	`zf_lang`
`zfmisc_1`	`zfmodel1`	`zfmodel2`	`zf_model`	`zfrefle1`	`zf_refle`

The Mizar-TPTP Semantic Presentation

The Mizar-TPTP
Semantic Presentation