TPTP Axioms


AGT001+0.ax AGT001+1.ax AGT001+2.ax ALG001-0.ax ALG002+0.ax ALG003^0.ax ANA001-0.ax
ANA002-0.ax ANA003-0.ax BIO001+0.ax BOO001-0.ax BOO002-0.ax BOO003-0.ax BOO004-0.ax
CAT001-0.ax CAT002-0.ax CAT003-0.ax CAT004-0.ax COL001-0.ax COL002-0.ax COL002-1.ax
COM001+0.ax COM001+1.ax CSR001+0.ax CSR001+1.ax CSR001+2.ax CSR001+3.ax CSR002+0.ax
CSR002+1.ax CSR002+2.ax CSR002+3.ax CSR002+4.ax CSR002+5.ax CSR003+0.ax CSR003+1.ax
CSR003+2.ax CSR003+3.ax CSR003+4.ax CSR003+5.ax CSR004+0.ax CSR005^0.ax DAT001=0.ax
DAT002=0.ax DAT002=1.ax DAT003=0.ax DAT004=0.ax DAT005=0.ax DAT006=0.ax FLD001-0.ax
FLD002-0.ax GEO001-0.ax GEO001-1.ax GEO002-0.ax GEO002-1.ax GEO002-2.ax GEO002-3.ax
GEO003-0.ax GEO004+0.ax GEO004-0.ax GEO004+1.ax GEO004-1.ax GEO004+2.ax GEO004-2.ax
GEO004+3.ax GEO004-3.ax GEO005-0.ax GEO006+0.ax GEO006+1.ax GEO006+2.ax GEO006+3.ax
GEO006+4.ax GEO006+5.ax GEO006+6.ax GEO007+0.ax GEO007+1.ax GEO008+0.ax GEO009+0.ax
GRA001+0.ax GRP001-0.ax GRP002-0.ax GRP003+0.ax GRP003-0.ax GRP003-1.ax GRP003-2.ax
GRP004+0.ax GRP004-0.ax GRP004-1.ax GRP004-2.ax GRP005-0.ax GRP006-0.ax GRP007+0.ax
GRP008-0.ax GRP008-1.ax HAL001+0.ax HEN001-0.ax HEN002-0.ax HEN003-0.ax HWC001-0.ax
HWC002-0.ax HWV001-0.ax HWV001-1.ax HWV001-2.ax HWV002-0.ax HWV002-1.ax HWV002-2.ax
HWV003-0.ax HWV004-0.ax KLE001+0.ax KLE001+1.ax KLE001+2.ax KLE001+3.ax KLE001+4.ax
KLE001+5.ax KLE001+6.ax KLE001+7.ax KLE002+0.ax KLE003+0.ax KLE004+0.ax KRS001+0.ax
KRS001+1.ax LAT001-0.ax LAT001-1.ax LAT001-2.ax LAT001-3.ax LAT001-4.ax LAT002-0.ax
LAT003-0.ax LAT004-0.ax LAT005-0.ax LAT006-0.ax LAT006-1.ax LAT006-2.ax LCL001-0.ax
LCL001-1.ax LCL001-2.ax LCL002-0.ax LCL002-1.ax LCL003-0.ax LCL004-0.ax LCL004-1.ax
LCL004-2.ax LCL005-0.ax LCL006+0.ax LCL006+1.ax LCL006+2.ax LCL006+3.ax LCL006+4.ax
LCL006+5.ax LCL007+0.ax LCL007+1.ax LCL007+2.ax LCL007+3.ax LCL007+4.ax LCL007+5.ax
LCL007+6.ax LCL008^0.ax LCL009^0.ax LCL010^0.ax LCL011^0.ax LCL012^0.ax LCL013^0.ax
LCL013^1.ax LCL013^2.ax LCL013^3.ax LCL013^4.ax LCL013^5.ax LCL013^6.ax LCL014^0.ax
LCL015^0.ax LCL015^1.ax LCL016^0.ax LCL016^1.ax LCL017^0.ax LDA001-0.ax MED001+0.ax
MED001+1.ax MED002+0.ax MGT001+0.ax MGT001-0.ax MSC001-0.ax MSC001-1.ax MSC001-2.ax
NLP001+0.ax NUM001-0.ax NUM001-1.ax NUM001-2.ax NUM002-0.ax NUM003-0.ax NUM004-0.ax
NUM005+0.ax NUM005+1.ax NUM005+2.ax NUM006^0.ax PHI001^0.ax PLA001-0.ax PLA001-1.ax
PLA002+0.ax PRD001+0.ax PUZ001-0.ax PUZ002-0.ax PUZ003-0.ax PUZ004-0.ax PUZ005+0.ax
PUZ005-0.ax PUZ006+0.ax QUA001^0.ax QUA001^1.ax REL001+0.ax REL001-0.ax REL001+1.ax
REL001-1.ax RNG001-0.ax RNG002-0.ax RNG003-0.ax RNG004-0.ax RNG005-0.ax ROB001-0.ax
ROB001-1.ax SET001-0.ax SET001-1.ax SET001-2.ax SET001-3.ax SET002-0.ax SET003-0.ax
SET004-0.ax SET004-1.ax SET005+0.ax SET006+0.ax SET006+1.ax SET006+2.ax SET006+3.ax
SET006+4.ax SET007 SET008^0.ax SET008^1.ax SET008^2.ax SET009^0.ax SWB001+0.ax
SWB002+0.ax SWB003+0.ax SWB003+1.ax SWC001+0.ax SWC001-0.ax SWV001-0.ax SWV002-0.ax
SWV003+0.ax SWV004-0.ax SWV005-0.ax SWV005-1.ax SWV005-2.ax SWV005-3.ax SWV005-4.ax
SWV005-5.ax SWV005-6.ax SWV005-7.ax SWV006-0.ax SWV006-1.ax SWV006-2.ax SWV006-3.ax
SWV007+0.ax SWV007+1.ax SWV007+2.ax SWV007+3.ax SWV007+4.ax SWV008^0.ax SWV008^1.ax
SWV008^2.ax SWV009+0.ax SWV010^0.ax SWV011+0.ax SWV012+0.ax SWV013-0.ax SYN000+0.ax
SYN000-0.ax SYN000^0.ax SYN000_0.ax SYN001-0.ax SYN002+0.ax TOP001-0.ax