public static Keyword tryEquivalenceProof(ControlFrame frame) {
    { Vector arguments = frame.proposition.arguments;
      Stella_Object firstarg = (arguments.theArray)[0];
      Stella_Object firstvalue = Logic.argumentBoundTo(firstarg);
      Stella_Object secondarg = (arguments.theArray)[1];
      Stella_Object secondvalue = Logic.argumentBoundTo(secondarg);
      boolean successP = false;

      if (frame.reversePolarityP) {
        if ((firstvalue == null) ||
            (secondvalue == null)) {
          return (Logic.KWD_FAILURE);
        }
        else if (Logic.skolemP(firstvalue) ||
            Logic.skolemP(secondvalue)) {
          return (Logic.KWD_FAILURE);
        }
        else if (Stella_Object.eqlP(firstvalue, secondvalue)) {
          ControlFrame.setFrameTruthValue(frame, Logic.FALSE_TRUTH_VALUE);
          return (Logic.KWD_TERMINAL_FAILURE);
        }
        else {
          ControlFrame.setFrameTruthValue(frame, Logic.TRUE_TRUTH_VALUE);
          return (Logic.KWD_FINAL_SUCCESS);
        }
      }
      if (firstvalue != null) {
        if (secondvalue != null) {
          successP = Stella_Object.eqlP(firstvalue, secondvalue);
        }
        else {
          successP = PatternVariable.bindVariableToValueP(((PatternVariable)(secondarg)), firstvalue, true);
        }
      }
      else {
        if (secondvalue != null) {
          successP = PatternVariable.bindVariableToValueP(((PatternVariable)(firstarg)), secondvalue, true);
        }
        else {
          successP = false;
        }
      }
      return ((successP ? Logic.KWD_FINAL_SUCCESS : Logic.KWD_FAILURE));
    }
  }