fof(axiom1, axiom, (? [T] : (nontime(X) => present(X,T)))).
fof(axiom2, axiom, (phtxt(X,T) => ! [T1] : (present(X,T1) => phtxt(X,T1)))).
fof(axiom3, axiom, (txt(X,T) => ! [T1] : (present(X,T1) => txt(X,T1)))).
fof(definition4, axiom, (pt(X,Y,T) <=> (ppt(X,Y,T) | (X = Y & (present(X,T) & present(Y,T)))))).
fof(definition5, axiom, (overlap(X,Y,T) <=> ? [Z] : (pt(Z,X,T) & pt(Z,Y,T)))).
fof(definition6, axiom, (sumpt(X, Y,Z,T) <=> ((pt(Y,X,T) & pt(Z,X,T)) & ! [V] : (pt(V,X,T) => (overlap(V,Y,T) | overlap(V,Z,T)))))).
fof(axiom7, axiom, (ppt(X,Y,T) => (present(X,T) & present(Y,T)))).
fof(axiom8, axiom, (~ppt(X,X,T))).
fof(axiom9, axiom, ((ppt(X,Y,T) & ppt(Y,Z,T)) => ppt(X,Z,T))).
fof(axiom10, axiom, (ppt(X,Y,T) => ? [Z] : (ppt(Z,Y,T) & ~overlap(X,Z,T)))).
fof(axiom11, axiom, ((present(X,T) & present(Y,T)) => ? [Z] : sumpt(Z, X,Y,T))).
fof(axiom12, axiom, ((reg(S) & time(T)) => occ(S, S, T))).
fof(axiom13, axiom, (occ(S, R, T) => (present(S,T) & present(R,T)))).
fof(axiom14, axiom, (((ppt(R1, R2, T) & reg(R2)) & time(T)) => occ(R1,R1,T))).
fof(axiom15, axiom, ((ppt(X, Y, T) & occ(Y, R1, T)) => ? [R2] : (ppt(R2, R1, T) & occ(X, R2, T)))).
fof(axiom16, axiom, (phtxt(X,T) => ? [T1] : (time(T1) & ~present(X,T1)))).
fof(definition17, axiom, (phppt(X,Y,T) <=> ((ppt(X,Y,T) & phtxt(X,T)) & phtxt(Y,T)))).
fof(definition18, axiom, (phpt(X,Y,T) <=> ((pt(X,Y,T) & phtxt(X,T)) & phtxt(Y,T)))).
fof(definition19, axiom, (phoverlap(X,Y,T) <=> ? [Z] : (phpt(Z,X,T) & phpt(Z,Y,T)))).
fof(definition20, axiom, (phsumpt(X, Y,Z,T) <=> ((phpt(Y,X,T) & phpt(Z,X,T)) & ! [V] : (phpt(V,X,T) => (phoverlap(V,Y,T) | phoverlap(V,Z,T)))))).
fof(definition21, axiom, (compphtxt(X,T) <=> (phtxt(X,T) & ~(? [Y] : phppt(X,Y,T))))).
fof(axiom22, axiom, (phppt(X,Y,T) => ~(? [T1] : phppt(Y,X,T1)))).
fof(axiom23, axiom, ((phtxt(X,T) & phtxt(Y,T)) => (~phpt(X,Y,T) => ? [Z] : (phpt(Z,X,T) & ~(phoverlap(Z,Y,T)))))).
fof(axiom24, axiom, (phtxt(X,T) => ? [Z] : (~(phtxt(Z,T)) & pt(Z,X,T)))).
fof(axiom25, axiom, (phppt(X,Y,T) => ? [Z] : (phppt(X,Z,T) & ~(? [V] : (phppt(X,V,T) & phppt(V,Z,T)))))).
fof(axiom26, axiom, (phppt(X,Y,T) => ? [Z] : (phppt(Z,Y,T) & ~(? [V] : (phppt(Z,V,T) & phppt(V,Y,T)))))).
fof(axiom27, axiom, (phtxt(X,T) => (! [Y] : phpt(Y,X,T) => ? [Z] : (phpt(Z,Y,T) & ! [V] : ~(phppt(V,Z,T)))))).
fof(axiom28, axiom, (phtxt(X,T) => ? [R] : occ(X, R, T))).
fof(axiom29, axiom, ((occ(X, R, T) & occ(Y, R, T)) => ((phtxt(X,T) & phtxt(Y,T)) => X=Y))).
fof(axiom30, axiom, (phtxtprec(X,Y,T) => (phtxt(X,T) & phtxt(Y,T)))).
fof(axiom31, axiom, (~phtxtprec(X,X,T))).
fof(axiom32, axiom, ((phtxtprec(X,Y,T) & phtxtprec(Y,Z,T)) => phtxtprec(X,Z,T))).
fof(axiom33, axiom, (phtxtprec(X,Y,T) => ? [Z] : (phtxtprec(X,Z,T) & ~(? [V] : (phtxtprec(X,V,T) & phtxtprec(V,Z,T)))))).
fof(axiom34, axiom, (phtxtprec(X,Y,T) => ? [Z] : (phtxtprec(Z,Y,T) & ~(? [V] : (phtxtprec(Z,V,T) & phtxtprec(V,Y,T)))))).
fof(axiom35, axiom, (phtxtprec(X,Y,T) => ~(? [T1] : (phpt(X,Y,T1) | phpt(Y,X,T1))))).
fof(axiom36, axiom, (phtxtprec(X,Y,T) => ! [Z] : (phpt(Z,X,T) => phtxtprec(Z,Y,T)))).
fof(axiom37, axiom, (phtxtprec(X,Y,T) => ! [Z] : (phpt(Z,Y,T) => phtxtprec(X,Z,T)))).
fof(axiom38a, axiom, (phtxtprec(X,Y,T) => ? [Z] : ((compphtxt(Z,T) & phpt(X,Z,T)) & phpt(Y,Z,T)))).
fof(axiom38b, axiom, (phtxtprec(X,Y,T) => ! [Z1, Z1] : ((((compphtxt(Z1,T) & phpt(X,Z1,T)) & phpt(Y,Z1,T)) & ((compphtxt(Z2,T) & phpt(X,Z2,T)) & phpt(Y,Z2,T))) => Z1=Z2))).
fof(axiom39, axiom, (phtxt(X,T) => ? [Y] : (phpt(Y,X,T) & ! [Z] : (phpt(Z,X,T) => ~(phtxtprec(Z,Y,T)))))).
fof(axiom40, axiom, (phtxt(X,T) => ? [Y] : (phpt(Y,X,T) & ! [Z] : (phpt(Z,X,T) => ~(phtxtprec(Y,Z,T)))))).
fof(axiom41, axiom, ((phtxtprec(X,Y,T) & ~(? [Z] : (phtxtprec(X,Z,T) & phtxtprec(Z,Y,T)))) => ? [Z] : phsumpt(Z, X,Y,T))).
fof(axiom42, axiom, (phtxtprec(X,Y,T) => ((occ(X, R1, T) & occ(Y, R2, T)) => ~overlap(R1, R2, T)))).
fof(axiom45, axiom, (phrep(X, Y, T) => phtxt(X,T))).
fof(axiom46, axiom, (? [Y] : phrep(X, Y, T) => ! [T1] : (present(X, T1) => ? [Y] : phrep(X, Y, T1)) )).
fof(axiom47, axiom, (phtxtequiv(X,T,Y,T1) => (phtxt(X,T) & phtxt(Y,T1)))).
fof(axiom48, axiom, (phtxtequiv(X,T,Y,T1) => (present(X,T) & present(Y,T1)))).
fof(axiom49, axiom, (phtxt(X,T) => phtxtequiv(X,T,X,T))).
fof(axiom50, axiom, (phtxtequiv(X,T,Y,T1) => phtxtequiv(Y,T1,X,T))).
fof(axiom51, axiom, ((phtxtequiv(X,T1,Y,T2) & phtxtequiv(Y,T2,Z,T3)) => phtxtequiv(X,T1,Z,T3))).
fof(axiom52, axiom, (ppt(X,Y,T) => ~phtxtequiv(X,T,Y,T))).
fof(axiom53, axiom, ((phtxtequiv(X1,T,X2,T) & phppt(Y1,X1,T)) => ? [Y2] : (phtxtequiv(Y1,T,Y2,T) & ppt(Y2,X2,T)))).
fof(axiom54, axiom, ((phtxtequiv(X1,T,X2,T) & phppt(X1,Y1,T)) => ? [Y2] : (phtxtequiv(Y1,T,Y2,T) & ppt(X2,Y2,T)))).
fof(axiom55, axiom, (phtxtequiv(X1,T1,X2,T2) =>  (phrep(X1, Y, T1) <=> phrep(X2, Y, T2)))).
fof(axiom56, axiom, (txtdep(X,Y) => ((? [T] : txt(X,T)) & (? [T] : phtxt(Y,T))))).
fof(axiom57a, axiom, (phtxt(X,T) => ? [Y] : (txt(Y,T) & txtdep(Y,X)))).
fof(axiom57b, axiom, (phtxt(X,T) => ! [Y1, Y2] : (((txt(Y1,T) & txtdep(Y1,X)) & (txt(Y2,T) & txtdep(Y2,X))) => Y1=Y2))).
fof(axiom58, axiom, (txt(X,T) => ? [Y] : (phtxt(Y,T) & txtdep(X,Y)))).
fof(axiom59, axiom, ((txtdep(X,Y1) & txtdep(X,Y2)) => ! [T1,T2] : ((present(Y1,T1) & present(Y2,T2)) =>  phtxtequiv(Y1,T1, Y2,T2)))).
fof(axiom60, axiom, (txtdep(X,Y) => ! [T] : (present(X,T) => ? [Z,T1] : phtxtequiv(Z,T,Y,T1)))).
fof(axiom61, axiom, (txtdep(X,Y) => ! [T] : (present(Y,T) => present(X,T)))).
fof(axiom62, axiom, (phtxtequiv(Y1,T1, Y2,T2) => ! [Z] :(txtdep(Z,Y1) <=> txtdep(Z,Y2)))).
fof(axiom63, axiom, ((txtdep(X1,Y1) & txtdep(X2,Y2)) => (ppt(X1,X2,T) <=> ppt(Y1,Y2,T)))).
fof(axiom64, axiom, ((txtdep(X1,Y1) & txtdep(X2,Y2)) => (phtxtprec(X1,X2,T) <=> phtxtprec(Y1,Y2,T)))).
fof(axiom65, axiom, ((txt(X,T) & ppt(Z,X,T)) => txt(Z,T))).
fof(axiom66, axiom, (~ (? [X] : (phtxt(X,T) & txt(X,T))))).
fof(axiom68, axiom, (txtppt(X,Y,T) <=> ? [X1, Y1] : ((txtdep(X,X1) & txtdep(Y,Y1)) & ppt(X1, Y1, T)))).
fof(axiomLXX, axiom, (txtpt(X,Y,T) <=> ? [X1, Y1] : ((txtdep(X,X1) & txtdep(Y,Y1)) & pt(X1, Y1, T)))).
fof(axiomLXXI, axiom, (txtoverlap(X,Y,T) <=> ? [X1, Y1] : ((txtdep(X,X1) & txtdep(Y,Y1)) & phoverlap(X1, Y1, T)))).
fof(axiomLXXII, axiom, (txtprec(X,Y,T) <=> ? [X1, Y1] : ((txtdep(X,X1) & txtdep(Y,Y1)) & phtxtprec(X1, Y1, T)))).
fof(axiomLXXIII, axiom, (txtrep(X,Y,T) <=> ? [X1] : (txtdep(X,X1) & phrep(X1, Y, T)))).
fof(axiomLXXIV, axiom, (txtsumpt(X,Y,Z,T) <=> ? [X1, Y1, Z1] : (((txtdep(X,X1) & txtdep(Y,Y1)) &  txtdep(Z,Z1))  & phsumpt(X1, Y1,Z1,T)))).
fof(axiomLXXV, axiom, (comptxt(X,T) <=> ? [X1] : (txtdep(X,X1) & compphtxt(X1, T)))).
fof(axiomC, axiom, (phtxt(X,T) => (obj(X) & time(T)))).
fof(axiomCI, axiom, (txt(X,T) =>  (obj(X) & time(T)))).
fof(axiomCII, axiom, (txtdep(X,Y) => (obj(X) & obj(Y)))).
fof(axiomCIII, axiom, (present(X,T) => (nontime(X) & time(T)))).
fof(axiomCIV, axiom, (occ(S, R, T) => (nontime(S) & (reg(R) & time(T))))).
fof(axiomCV, axiom, (ppt(X,Y,T) => (nontime(X) & (nontime(Y) & time(T))))).
fof(axiomCVI, axiom, (phtxtprec(X,Y,T) => (obj(X) & (obj(Y) & time(T))))).
fof(axiomCVII, axiom, (phtxtequiv(X,T1,Y,T2) => (obj(X) & (obj(Y) & (time(T1) & time(T2)))))).
fof(axiomCVIII, axiom, (phrep(X, Y, T) => (obj(X) & (obj(Y) & time(T))))).
fof(axiomCIX, axiom, ((obj(X) | reg(X)) => nontime(X))).
fof(axiomCX, axiom, (time(T) => ~nontime(T))).
fof(axiomCXI, axiom, (obj(X) => ~reg(X))).