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 CML001+0.ax CML001+100.ax CML001+101.ax
CML001+102.ax CML001+103.ax CML001+104.ax CML001+105.ax CML001+106.ax CML001+107.ax CML001+108.ax
CML001+109.ax CML001+10.ax CML001+110.ax CML001+111.ax CML001+112.ax CML001+113.ax CML001+114.ax
CML001+115.ax CML001+116.ax CML001+117.ax CML001+118.ax CML001+119.ax CML001+11.ax CML001+120.ax
CML001+121.ax CML001+122.ax CML001+123.ax CML001+124.ax CML001+125.ax CML001+126.ax CML001+127.ax
CML001+128.ax CML001+129.ax CML001+12.ax CML001+130.ax CML001+131.ax CML001+132.ax CML001+133.ax
CML001+134.ax CML001+135.ax CML001+136.ax CML001+137.ax CML001+138.ax CML001+139.ax CML001+13.ax
CML001+140.ax CML001+141.ax CML001+142.ax CML001+143.ax CML001+144.ax CML001+145.ax CML001+146.ax
CML001+147.ax CML001+148.ax CML001+149.ax CML001+14.ax CML001+150.ax CML001+151.ax CML001+152.ax
CML001+153.ax CML001+154.ax CML001+155.ax CML001+156.ax CML001+157.ax CML001+158.ax CML001+159.ax
CML001+15.ax CML001+160.ax CML001+161.ax CML001+162.ax CML001+163.ax CML001+164.ax CML001+165.ax
CML001+166.ax CML001+167.ax CML001+168.ax CML001+169.ax CML001+16.ax CML001+170.ax CML001+171.ax
CML001+172.ax CML001+173.ax CML001+174.ax CML001+175.ax CML001+176.ax CML001+177.ax CML001+178.ax
CML001+179.ax CML001+17.ax CML001+180.ax CML001+181.ax CML001+182.ax CML001+183.ax CML001+184.ax
CML001+185.ax CML001+186.ax CML001+187.ax CML001+188.ax CML001+189.ax CML001+18.ax CML001+190.ax
CML001+191.ax CML001+192.ax CML001+193.ax CML001+194.ax CML001+195.ax CML001+196.ax CML001+197.ax
CML001+198.ax CML001+199.ax CML001+19.ax CML001+1.ax CML001+200.ax CML001+201.ax CML001+202.ax
CML001+203.ax CML001+204.ax CML001+205.ax CML001+206.ax CML001+207.ax CML001+208.ax CML001+209.ax
CML001+20.ax CML001+210.ax CML001+211.ax CML001+212.ax CML001+213.ax CML001+214.ax CML001+215.ax
CML001+216.ax CML001+217.ax CML001+218.ax CML001+219.ax CML001+21.ax CML001+220.ax CML001+221.ax
CML001+222.ax CML001+223.ax CML001+224.ax CML001+225.ax CML001+226.ax CML001+227.ax CML001+228.ax
CML001+229.ax CML001+22.ax CML001+230.ax CML001+231.ax CML001+232.ax CML001+233.ax CML001+234.ax
CML001+235.ax CML001+236.ax CML001+237.ax CML001+238.ax CML001+239.ax CML001+23.ax CML001+240.ax
CML001+241.ax CML001+242.ax CML001+243.ax CML001+244.ax CML001+245.ax CML001+246.ax CML001+247.ax
CML001+248.ax CML001+249.ax CML001+24.ax CML001+250.ax CML001+251.ax CML001+252.ax CML001+253.ax
CML001+254.ax CML001+255.ax CML001+256.ax CML001+257.ax CML001+258.ax CML001+259.ax CML001+25.ax
CML001+260.ax CML001+261.ax CML001+262.ax CML001+263.ax CML001+264.ax CML001+265.ax CML001+266.ax
CML001+267.ax CML001+268.ax CML001+269.ax CML001+26.ax CML001+270.ax CML001+271.ax CML001+272.ax
CML001+273.ax CML001+274.ax CML001+275.ax CML001+276.ax CML001+277.ax CML001+278.ax CML001+279.ax
CML001+27.ax CML001+280.ax CML001+281.ax CML001+282.ax CML001+283.ax CML001+284.ax CML001+285.ax
CML001+286.ax CML001+287.ax CML001+288.ax CML001+289.ax CML001+28.ax CML001+290.ax CML001+291.ax
CML001+292.ax CML001+293.ax CML001+294.ax CML001+295.ax CML001+296.ax CML001+297.ax CML001+298.ax
CML001+299.ax CML001+29.ax CML001+2.ax CML001+300.ax CML001+301.ax CML001+302.ax CML001+303.ax
CML001+304.ax CML001+305.ax CML001+306.ax CML001+307.ax CML001+308.ax CML001+309.ax CML001+30.ax
CML001+310.ax CML001+311.ax CML001+312.ax CML001+313.ax CML001+314.ax CML001+315.ax CML001+316.ax
CML001+317.ax CML001+318.ax CML001+319.ax CML001+31.ax CML001+320.ax CML001+321.ax CML001+322.ax
CML001+323.ax CML001+324.ax CML001+325.ax CML001+326.ax CML001+327.ax CML001+328.ax CML001+329.ax
CML001+32.ax CML001+330.ax CML001+331.ax CML001+332.ax CML001+333.ax CML001+334.ax CML001+335.ax
CML001+336.ax CML001+337.ax CML001+338.ax CML001+339.ax CML001+33.ax CML001+34.ax CML001+35.ax
CML001+36.ax CML001+37.ax CML001+38.ax CML001+39.ax CML001+3.ax CML001+40.ax CML001+41.ax
CML001+42.ax CML001+43.ax CML001+44.ax CML001+45.ax CML001+46.ax CML001+47.ax CML001+48.ax
CML001+49.ax CML001+4.ax CML001+50.ax CML001+51.ax CML001+52.ax CML001+53.ax CML001+54.ax
CML001+55.ax CML001+56.ax CML001+57.ax CML001+58.ax CML001+59.ax CML001+5.ax CML001+60.ax
CML001+61.ax CML001+62.ax CML001+63.ax CML001+64.ax CML001+65.ax CML001+66.ax CML001+67.ax
CML001+68.ax CML001+69.ax CML001+6.ax CML001+70.ax CML001+71.ax CML001+72.ax CML001+73.ax
CML001+74.ax CML001+75.ax CML001+76.ax CML001+77.ax CML001+78.ax CML001+79.ax CML001+7.ax
CML001+80.ax CML001+81.ax CML001+82.ax CML001+83.ax CML001+84.ax CML001+85.ax CML001+86.ax
CML001+87.ax CML001+88.ax CML001+89.ax CML001+8.ax CML001+90.ax CML001+91.ax CML001+92.ax
CML001+93.ax CML001+94.ax CML001+95.ax CML001+96.ax CML001+97.ax CML001+98.ax CML001+99.ax
CML001+9.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 GEO010+0.ax GEO010+1.ax GEO011+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 MAT001^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