public static Keyword tryManufactureSkolemProof(ControlFrame frame) {
    { Proposition proposition = frame.proposition;
      NamedDescription description = Logic.getDescription(((Surrogate)(proposition.operator)));
      Cons argumentvalues = Stella.NIL;

      if ((!Logic.testPropertyP(description, Logic.SGT_PL_KERNEL_KB_TOTAL)) ||
          frame.reversePolarityP) {
        return (Logic.KWD_FAILURE);
      }
      { Stella_Object arg = null;
        Vector vector000 = proposition.arguments;
        int index000 = 0;
        int length000 = vector000.length();

        for (;index000 < length000; index000 = index000 + 1) {
          arg = (vector000.theArray)[index000];
          argumentvalues = Cons.cons(Logic.argumentBoundTo(arg), argumentvalues);
        }
      }
      { boolean testValue000 = false;

        if (argumentvalues.value != null) {
          testValue000 = true;
        }
        else {
          { boolean foundP000 = false;

            { Stella_Object value = null;
              Cons iter000 = argumentvalues.rest;

              loop001 : for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
                value = iter000.value;
                if (value == null) {
                  foundP000 = true;
                  break loop001;
                }
              }
            }
            testValue000 = foundP000;
          }
        }
        if (testValue000) {
          return (Logic.KWD_FAILURE);
        }
      }
      { Cons inputvalues = argumentvalues.rest.reverse();
        Proposition definingproposition = Logic.findOrCreateFunctionProposition(((Surrogate)(proposition.operator)), inputvalues);

        PatternVariable.bindVariableToValueP(((PatternVariable)((proposition.arguments.theArray)[(proposition.arguments.length() - 1)])), (definingproposition.arguments.theArray)[(definingproposition.arguments.length() - 1)], true);
        return (Logic.KWD_FINAL_SUCCESS);
      }
    }
  }