public static String operatorToString(Stella_Object operator) {
    if (operator == null) {
      return ("NULL");
    }
    { Surrogate testValue000 = Stella_Object.safePrimaryType(operator);

      if (Surrogate.subtypeOfSurrogateP(testValue000)) {
        { Surrogate operator000 = ((Surrogate)(operator));

          { String printname = Logic.stringifiedSurrogate(operator000);

            if ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_AND) ||
                ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_OR) ||
                 ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_NOT) ||
                  ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_FAIL) ||
                   ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_FORALL) ||
                    ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_EXISTS) ||
                     ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_KAPPA) ||
                      ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_SUBSET_OF) ||
                       ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_SETOF) ||
                        ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_LISTOF) ||
                         ((operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_BAGOF) ||
                          ((operator000 == OntosaurusUtil.SGT_STELLA_TRUE) ||
                           (operator000 == OntosaurusUtil.SGT_STELLA_FALSE))))))))))))) {
              if (OntosaurusUtil.$DOWNCASE_STANDARD_KIF_OPERATORSp$) {
                printname = Native.stringDowncase(printname);
              }
            }
            else if (operator000 == OntosaurusUtil.SGT_PL_KERNEL_KB_EQUIVALENT) {
              printname = "=";
            }
            else {
            }
            return (printname);
          }
        }
      }
      else if (Surrogate.subtypeOfSymbolP(testValue000)) {
        { Symbol operator000 = ((Symbol)(operator));

          return (Logic.maybeDowncase(operator000.symbolName));
        }
      }
      else {
        { OutputStringStream stream000 = OutputStringStream.newOutputStringStream();

          stream000.nativeStream.print("`" + testValue000 + "' is not a valid case option");
          throw ((StellaException)(StellaException.newStellaException(stream000.theStringReader()).fillInStackTrace()));
        }
      }
    }
  }