public static Keyword refutationDisjointSpecialist(ControlFrame frame, Keyword lastmove) {
    { Proposition proposition = frame.proposition;
      Stella_Object arg1 = Logic.argumentBoundTo((proposition.arguments.theArray)[0]);
      Stella_Object arg2 = Logic.argumentBoundTo((proposition.arguments.theArray)[1]);

      lastmove = lastmove;
      if ((arg1 == null) ||
          ((arg2 == null) ||
           ((!Stella_Object.isaP(arg1, Logic.SGT_LOGIC_DESCRIPTION)) ||
            ((!Stella_Object.isaP(arg2, Logic.SGT_LOGIC_DESCRIPTION)) ||
             (proposition.arguments.length() > 2))))) {
        return (Logic.KWD_TERMINAL_FAILURE);
      }
      Logic.pushMonotonicWorld();
      Logic.initializeInferenceWorld(((World)(((Context)(Stella.$CONTEXT$.get())))));
      try {
        { LogicObject skolem = Logic.createHypothesizedInstance("refutation-disjoint");

          { Description c = null;
            Cons iter000 = ((Cons)(Cons.consList(Cons.cons(arg1, Cons.cons(arg2, Stella.NIL)))));

            for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
              c = ((Description)(iter000.value));
              Logic.assertMemberOfProposition(skolem, c);
            }
          }
          Logic.elaborateInstance(skolem);
        }
      } catch (Clash e000) {
        Stella.popWorld();
        return (Logic.KWD_FINAL_SUCCESS);
      }
      Stella.popWorld();
      return (Logic.KWD_FAILURE);
    }
  }