P73
      & P162 & P2577
      & P363 & 
     (a0 = "NOTBOTH" & 
     a0 = "MZERO2" & a0 = "ATIMES"
      & a0 = "RZERO" & 
     a0 = "RTIMES" & a0 = "EQUALITY"
      & a0 = "CTIMES" & 
     a0 = "ITIMES" & a0 = "RTIMES"
      & a0 = "RTIMES" & 
     a0 = "INV" & a0 = "ATIMES"
      & a0 = "ATIMES" & 
     a0 = "CTIMES" & a0 = "ATIMES"
      & a0 = "ATIMES" & 
     a0 = "TRANS" & a0 = "TIMESPOS"
      & a0 = "THREEPOS" & 
     a0 = "POSINV" & a0 = "MTIMES"
      & a0 = "CTIMES" & 
     a0 = "LIKETERMS1" & a0 = "IPLUSa"
      & a0 = "MINUS" & 
     a0 = "APLUS" & a0 = "APLUS"
      & a0 = "MPLUS" & 
     a0 = "MINUS" & a0 = "MPLUS"
      & a0 = "TRANS" & 
     a0 = "ORDERLEMMA1" & a0 = "FOIL"
      & a0 = "NOTBOTH" & 
     a0 = "MZERO2" & a0 = "ATIMES"
      & a0 = "RZERO" & 
     a0 = "RTIMES" & a0 = "RTIMES"
      & a0 = "RSUP" & 
     a0 = "EQUALITY" & a0 = "MZERO2"
      & a0 = "TRANS" & 
     a0 = "TIMESPOS" & a0 = "THREEPOS"
      & a0 = "POSINV" & 
     a0 = "MTIMES" & a0 = "CTIMES"
      & a0 = "RTIMES" & 
     a0 = "ITIMES" & a0 = "INV"
      & a0 = "ATIMES" & 
     a0 = "ATIMES" & a0 = "CTIMES"
      & a0 = "ATIMES" & 
     a0 = "ATIMES" & a0 = "TRANS"
      & a0 = "TIMESPOS" & 
     a0 = "THREEPOS" & a0 = "POSINV"
      & a0 = "MTIMES" & 
     a0 = "CTIMES" & a0 = "LIKETERMS1"
      & a0 = "IPLUSa" & 
     a0 = "MINUS" & a0 = "APLUS"
      & a0 = "APLUS" & 
     a0 = "MPLUS" & a0 = "MINUS"
      & a0 = "MPLUS" & 
     a0 = "ORDERLEMMA1" & a0 = "FOIL"
      & a0 = "RTIMES" & 
     a0 = "EQUALITY" & a0 = "TRANS"
      & a0 = "TRANS" & 
     a0 = "NOTBOTH" & a0 = "NOTBOTH3"
      & a0 = "TRI" & 
     a0 = "TRANS" & a0 = "TRANS"
      & a0 = "TRANS" & 
     a0 = "SquareOrder1" & a0 = "IPLUSb"
      & a0 = "MPLUS" & 
     a0 = "BDED" & a0 = "BDED"
      & a0 = "TRANS" & 
     a0 = "SOMETHINGBIGGER"
      & a0 = "TRANS" & 
     a0 = "SQPOS" & a0 = "SquareOrder2"
      & a0 = "TRANS" & 
     a0 = "SqLemma" & a0 = "SUP2"
      & a0 = "RTIMES" & 
     a0 = "EQUALITY" & a0 = "TRI"
      & a0 = "LIKETERMS1" & 
     a0 = "LIKETERMS1" & a0 = "DIST2"
      & a0 = "CTIMES" & 
     a0 = "ITIMES" & a0 = "TIMESPOS"
      & a0 = "TIMESPOS" & 
     a0 = "CTIMES" & a0 = "MZERO2"
      & a0 = "MTIMES" & 
     a0 = "THREEPOS" & a0 = "THREEPOS"
      & a0 = "RONE" & 
     a0 = "RONE" & a0 = "APLUS"
      & a0 = "TRANS" & 
     a0 = "IPLUSb" & a0 = "MPLUS"
      & a0 = "TRANS" & 
     a0 = "IPLUSb" & a0 = "MPLUS"
      & a0 = "ZEROLESSONE" & 
     a0 = "ORDERLEMMA1"
      & a0 = "ORDERLEMMA1" & 
     a0 = "CTIMES" & a0 = "MPLUS"
      & a0 = "MTIMES" & 
     a0 = "HALFTWO" & a0 = "HALFTWO"
      & a0 = "NOTBOTH3" & 
     a0 = "TWOPOS" & a0 = "INV"
      & a0 = "CTIMES" & 
     a0 = "SupLemma" & a0 = "SupLemma"
      & a0 = "RONE" & 
     a0 = "ITIMES" & a0 = "ZEROLESSONE"
      & a0 = "HALFPOS" & 
     a0 = "HalfLess" & a0 = "CTIMES"
      & a0 = "ATIMES" & 
     a0 = "CTIMES" & a0 = "ATIMES"
      & a0 = "CTIMES" & 
     a0 = "TRANS" & a0 = "MTIMES"
      & a0 = "TRANS" & 
     a0 = "MTIMES" & a0 = "CTIMES"
      & a0 = "ITIMES" & 
     a0 = "MTIMES" & a0 = "MHALFPOS"
      & a0 = "RHALF" & 
     a0 = "RONE" & a0 = "ZEROLESSONE"
      & a0 = "RONE" & 
     a0 = "IPLUSb" & a0 = "MPLUS"
      & a0 = "ZEROLESSONE" & 
     a0 = "TRANS" & a0 = "HalfLess"
      & a0 = "NOTBOTH3" & 
     a0 = "TWOPOS" & a0 = "INV"
      & a0 = "HALFPOS" & 
     a0 = "MTIMES" & a0 = "ITIMES"
      & a0 = "MHALFPOS" & 
     a0 = "RONE" & a0 = "EQUALITY"
      & a0 = "TRI" & 
     a0 = "FOIL" & a0 = "FOIL"
      & a0 = "RTIMES" & 
     a0 = "ITIMES" & a0 = "CTIMES"
      & a0 = "DIST2" & 
     a0 = "DIST" & a0 = "CTIMES"
      & a0 = "DIST2" & 
     a0 = "DIST" & a0 = "APLUS"
      & a0 = "APLUS" & 
     a0 = "EPSLEMMA" & a0 = "EPSLEMMA"
      & a0 = "NOTBOTH" & 
     a0 = "HalfLess" & a0 = "NOTBOTH3"
      & a0 = "HalfLess" & 
     a0 = "TRANS" & a0 = "HalfLess"
      & a0 = "RTIMES" & 
     a0 = "HalfLess" & a0 = "EQUALITY"
      & a0 = "HalfLess" & 
     a0 = "MHALFPOS" & a0 = "RTIMES"
      & a0 = "TRANS" & 
     a0 = "HalfLess" & a0 = "MHALFPOS"
      & a0 = "RTIMES" & 
     a0 = "RZERO" & a0 = "EQUALITY"
      & a0 = "SqLemma" & 
     a0 = "SqLemma" & a0 = "RONE"
      & a0 = "TRANS" & 
     a0 = "CTIMES" & a0 = "TRANS"
      & a0 = "MTIMES" & 
     a0 = "SOMETHINGBIGGER"
      & a0 = "CTIMES" & 
     a0 = "ITIMES" & a0 = "MTIMES"
      & a0 = "IPLUSb" & 
     a0 = "MPLUS" & a0 = "RONE"
      & a0 = "RONE" & 
     a0 = "NOTBOTH3" & a0 = "TWOPOS"
      & a0 = "CTIMES" & 
     a0 = "INV" & a0 = "RTIMES"
      & a0 = "SquareOrder2" & 
     a0 = "SquareOrder2"
      & a0 = "NOTBOTH" & 
     a0 = "SquareOrder1" & a0 = "IRR"
      & a0 = "SubLemma" & 
     a0 = "SubLemma" & a0 = "CTIMES"
      & a0 = "CTIMES" & 
     a0 = "SubLemma" & a0 = "SubLemma"
      & a0 = "TRI" & 
     a0 = "TRANS" & a0 = "CTIMES"
      & a0 = "MTIMES" & 
     a0 = "MTIMES" & a0 = "SQPOS"
      & a0 = "SQPOS" & 
     a0 = "MZERO2" & a0 = "MTIMES"
      & a0 = "HalfLess" & 
     a0 = "HalfLess" & a0 = "MHALFPOS"
      & a0 = "RTIMES" & 
     a0 = "CTIMES" & a0 = "ITIMES"
      & a0 = "TWOHALVES" & 
     a0 = "DIST2" & a0 = "CPLUS"
      & a0 = "IPLUSa" & 
     a0 = "MPLUS" & a0 = "MHALFPOS"
      & a0 = "MHALFPOS" & 
     a0 = "CTIMES" & a0 = "MZERO2"
      & a0 = "HALFPOS" & 
     a0 = "MTIMES" & a0 = "TWOHALVES"
      & a0 = "TWOHALVES" & 
     a0 = "NOTBOTH3" & a0 = "TWOPOS"
      & a0 = "INV" & 
     a0 = "CTIMES" & a0 = "DIST"
      & a0 = "RHALF" & 
     a0 = "ITIMES" & a0 = "HALFPOS"
      & a0 = "HALFPOS" & 
     a0 = "POSINV" & a0 = "TWOPOS"
      & a0 = "TWOPOS" & 
     a0 = "TWOPOS"
      & a0 = "TRANS" & 
     a0 = "SOMETHINGBIGGER"
      & a0 = "MPLUS" & 
     a0 = "ZEROLESSONE" & a0 = "RHALF"
      & a0 = "RHALF" & 
     a0 = "RINV"
      & a0 = "RTWO" & a0 = "RTWO"
      & a0 = "RPLUS" & 
     a0 = "SOMETHINGBIGGER"
      & a0 = "SOMETHINGBIGGER" & 
     a0 = "RPLUS" & a0 = "LESSTYPEa"
      & a0 = "CPLUS" & 
     a0 = "IPLUSa" & a0 = "CPLUS"
      & a0 = "MPLUS" & 
     a0 = "ZEROLESSONE"
      & a0 = "SUP2" & 
     a0 = "SomethingLess"
      & a0 = "SomethingLess" & 
     a0 = "LESSTYPEa" & a0 = "CPLUS"
      & a0 = "CPLUS" & 
     a0 = "MINUS" & a0 = "APLUS"
      & a0 = "CPLUS" & 
     a0 = "MPLUS" & a0 = "ZEROLESSONE"
      & a0 = "POSINV" & 
     a0 = "POSINV" & a0 = "IRR"
      & a0 = "ZEROLESSONE" & 
     a0 = "MZERO" & a0 = "RINV"
      & a0 = "RZERO" & 
     a0 = "EQUALITY" & a0 = "NOTBOTH3"
      & a0 = "INV" & 
     a0 = "NOTBOTH" & a0 = "ZEROLESSONE"
      & a0 = "MZERO2" & 
     a0 = "CTIMES" & a0 = "NOTBOTH3"
      & a0 = "INV" & 
     a0 = "MTIMES" & a0 = "TRI"
      & a0 = "MPLUSCONV" & 
     a0 = "MPLUSCONV" & a0 = "LESSTYPEa"
      & a0 = "MINUS" & 
     a0 = "MINUS" & a0 = "APLUS"
      & a0 = "APLUS" & 
     a0 = "MPLUS"
      & a0 = "TYPECONVERT" & 
     a0 = "TYPECONVERT" & a0 = "RTIMES"
      & a0 = "RTIMES" & 
     a0 = "IRR" & a0 = "IPLUSa"
      & a0 = "MZERO2" & 
     a0 = "ITIMES" & a0 = "DIST2"
      & a0 = "ZEROLESSONE" & 
     a0 = "MTIMES" & a0 = "MPLUS"
      & a0 = "RTIMES" & 
     a0 = "RTIMES" & a0 = "IRR"
      & a0 = "IPLUSa" & 
     a0 = "MZERO2" & a0 = "ITIMES"
      & a0 = "DIST2" & 
     a0 = "ZEROLESSONE" & a0 = "MTIMES"
      & a0 = "RTIMES" & 
     a0 = "RPLUS" & a0 = "IPLUSa"
      & a0 = "IPLUSa" & 
     a0 = "TRI" & a0 = "DIST2"
      & a0 = "DIST2" & 
     a0 = "CTIMES" & a0 = "CTIMES"
      & a0 = "DIST" & 
     a0 = "CTIMES" & a0 = "RETRACT"
      & a0 = "RETRACT" & 
     a0 = "RPLUS" & a0 = "IPLUSa"
      & a0 = "LESSTYPEa" & 
     a0 = "LESSTYPEa"
      & a0 = "LESSTYPE" & 
     a0 = "LESSTYPE" & a0 = "LESSTYPE"
      & a0 = "NOTBOTH" & 
     a0 = "MPLUS"
      & a0 = "IRR" & a0 = "TRI"
      & a0 = "THE" & 
     a0 = "THE" & a0 = "AN"
      & a0 = "COORDONE" & 
     a0 = "COORDONE" & a0 = "COORDONE"
      & a0 = "COORDONE" & 
     a0 = "COORDONE" & a0 = "SCLEMMA2"
      & a0 = "SCLEMMA3" & 
     a0 = "SCLEMMA1" & a0 = "CoupleEq"
      & a0 = "CoupleEq" & 
     a0 = "SCLEMMA3" & a0 = "SCLEMMA3"
      & a0 = "SCLEMMA2" & 
     a0 = "SCLEMMA1"
      & a0 = "CoupleComm" & 
     a0 = "CoupleComm"
      & a0 = "SCLEMMA1" & 
     a0 = "SCLEMMA1" & a0 = "SCLEMMA2"
      & a0 = "SCLEMMA2" & 
     a0 = "CoupleEq" & a0 = "CoupleEq"
      & a0 = "KPAIR" & 
     a0 = "KPAIR" & a0 = "PROJ2"
      & a0 = "PROJ2" & 
     a0 = "PROJ1" & a0 = "PROJ1"
      & a0 = "PROJ2" & 
     a0 = "PROJ2" & a0 = "PROJ1"
      & a0 = "PROJ1" & 
     a0 = "Symmetric"
      & a0 = "Symmetric" & 
     a0 = "Symmetric" & a0 = "RPLUS"
      & a0 = "RZERO" & 
     a0 = "NatReal" & a0 = "NatReal"
      & a0 = "RPLUS" & 
     a0 = "RZERO" & a0 = "NatClosed"
      & a0 = "NatClosed" & 
     a0 = "ZeroNat"
      & a0 = "ZeroNat" & 
     a0 = "SquareOrder"
      & a0 = "SquareOrder" & 
     a0 = "NOTBOTH" & a0 = "SquareOrder1"
      & a0 = "IRR" & 
     a0 = "SubLemma" & a0 = "SubLemma"
      & a0 = "CTIMES" & 
     a0 = "CTIMES" & a0 = "SubLemma"
      & a0 = "SubLemma" & 
     a0 = "TRI"
      & a0 = "SquareOrder1" & 
     a0 = "SquareOrder1" & a0 = "TRANS"
      & a0 = "CTIMES" & 
     a0 = "MTIMES" & a0 = "MTIMES"
      & a0 = "SubLemma" & 
     a0 = "SubLemma" & a0 = "RTIMES"
      & a0 = "CTIMES" & 
     a0 = "IPLUS" & a0 = "MZERO"
      & a0 = "DIST" & 
     a0 = "CTIMES" & a0 = "DIST"
      & a0 = "ZEROLESSONE" & 
     a0 = "ZEROLESSONE"
      & a0 = "REALONE" & 
     a0 = "NONTRIV" & a0 = "REALONE"
      & a0 = "ITIMES" & 
     a0 = "SQUARENONNEG"
      & a0 = "NOTBOTH3" & 
     a0 = "NOTBOTH3"
      & a0 = "NOTBOTH2" & 
     a0 = "EqualSymm"
      & a0 = "NOTBOTH2" & 
     a0 = "NOTBOTH2" & a0 = "IRR"
      & a0 = "MPLUS" & 
     a0 = "NOTBOTH" & a0 = "NOTBOTH"
      & a0 = "IRR" & 
     a0 = "TRANS" & a0 = "REALONE"
      & a0 = "REALONE" & 
     a0 = "RTIMES" & a0 = "EqualSymm"
      & a0 = "NONTRIV" & 
     a0 = "INV" & a0 = "EqualSymm"
      & a0 = "EqualSymm" & 
     a0 = "MZERO2" & a0 = "MZERO2"
      & a0 = "MZERO" & 
     a0 = "CTIMES"
      & a0 = "SQUARENONNEG" & 
     a0 = "SQUARENONNEG" & a0 = "CTIMES"
      & a0 = "MZERO" & 
     a0 = "MTIMES" & a0 = "CTIMES"
      & a0 = "MZERO" & 
     a0 = "MTIMESNEG" & a0 = "RZERO"
      & a0 = "MZERO" & 
     a0 = "EQUALITY" & a0 = "TRI"
      & a0 = "MTIMESNEG" & 
     a0 = "MTIMESNEG"
      & a0 = "TIMESDOUBNEG" & 
     a0 = "TIMESDOUBNEG"
      & a0 = "MTIMES" & 
     a0 = "MINUSLESS"
      & a0 = "NEGINEQ" & 
     a0 = "TIMESDOUBNEG"
      & a0 = "TIMESDOUBNEG" & 
     a0 = "RTIMES" & a0 = "DOUBLENEG"
      & a0 = "CTIMES" & 
     a0 = "NEGCOMM" & a0 = "CTIMES"
      & a0 = "NEGCOMM" & 
     a0 = "DOUBLENEG" & a0 = "DOUBLENEG"
      & a0 = "UINV" & 
     a0 = "CPLUS" & a0 = "MINUS"
      & a0 = "NEGCOMM" & 
     a0 = "NEGCOMM" & a0 = "MZERO"
      & a0 = "MINUS" & 
     a0 = "DIST" & a0 = "RTIMES"
      & a0 = "UINV" & 
     a0 = "MZERO" & a0 = "MINUS"
      & a0 = "DIST" & 
     a0 = "NEGINEQ" & a0 = "NEGINEQ"
      & a0 = "MPLUS" & 
     a0 = "RMINUS" & a0 = "IPLUSa"
      & a0 = "CPLUS" & 
     a0 = "MINUS" & a0 = "EQUALITY"
      & a0 = "EQUALITY" & 
     a0 = "IPLUS" & a0 = "IPLUS"
      & a0 = "MINUSLESS" & 
     a0 = "MINUSLESS" & a0 = "MINUS"
      & a0 = "APLUS" & 
     a0 = "CPLUS" & a0 = "CPLUS"
      & a0 = "MINUS2" & 
     a0 = "APLUS" & a0 = "MP"
      & a0 = "MPLUS0" & 
     a0 = "MPLUS" & a0 = "RMINUS"
      & a0 = "RMINUS" & 
     a0 = "IPLUSb" & a0 = "MINUS"
      & a0 = "APLUS" & 
     a0 = "CPLUS" & a0 = "IPLUSb"
      & a0 = "MINUS" & 
     a0 = "APLUS" & a0 = "MPLUS"
      & a0 = "MINUS2" & 
     a0 = "MINUS2" & a0 = "MINUS"
      & a0 = "CPLUS" & 
     a0 = "IPLUSb" & a0 = "IPLUSb"
      & a0 = "RZERO" & 
     a0 = "MP" & a0 = "NULLADD"
      & a0 = "CPLUS" & 
     a0 = "UINV" & a0 = "UINV"
      & a0 = "UNIQUEINV" & 
     a0 = "UNIQUEINV" & a0 = "UNIQUEINV"
      & a0 = "IPLUS" & 
     a0 = "MINUS" & a0 = "APLUS"
      & a0 = "RMINUS" & 
     a0 = "IPLUS" & a0 = "CPLUS"
      & a0 = "TRIV" & 
     a0 = "CPLUS" & a0 = "MZERO"
      & a0 = "MZERO" & 
     a0 = "RZERO" & a0 = "IPLUS"
      & a0 = "DIST" & 
     a0 = "RTIMES" & a0 = "RTIMES"
      & a0 = "MP" & 
     a0 = "NULLADD" & a0 = "RZERO"
      & a0 = "RZERO" & 
     a0 = "RPLUS"
      & a0 = "MINUS" & a0 = "MP"
      & a0 = "MP" & 
     a0 = "IPLUSa" & a0 = "IPLUSa"
      & a0 = "APLUS" & 
     a0 = "CPLUS" & a0 = "MINUS"
      & a0 = "TRIV" & 
     a0 = "TRIV" & a0 = "TRIV"
      & a0 = "IPLUSa" & 
     a0 = "IPLUSa" & a0 = "IPLUS"
      & a0 = "NULLADD" & 
     a0 = "NULLADD" & a0 = "IPLUS"
      & a0 = "IPLUS" & 
     a0 = "APLUS" & a0 = "CPLUS"
      & a0 = "MINUS" & 
     a0 = "SUP2" & a0 = "SUP1"
      & a0 = "MTIMES" & 
     a0 = "MPLUS" & a0 = "MPLUS"
      & a0 = "MPLUS0" & 
     a0 = "MPLUS0"
      & a0 = "TRANS" & a0 = "TRI"
      & a0 = "IRR" & 
     a0 = "NONTRIV" & a0 = "INV"
      & a0 = "MINUS" & 
     a0 = "ITIMES" & a0 = "IPLUS"
      & a0 = "DIST" & 
     a0 = "ATIMES" & a0 = "APLUS"
      & a0 = "CTIMES" & 
     a0 = "CPLUS" & a0 = "RSUP"
      & a0 = "RINV" & 
     a0 = "RMINUS" & a0 = "RTIMES"
      & a0 = "RPLUS" & 
     a0 = "AN" & P0) & P0 & P0
\