public static void printDescriptionsAsKifRule(Description head, Description tail, Proposition rule, boolean reversepolarityP) {
    { OutputStream stream = ((OutputStream)(Logic.$PRINTLOGICALFORMSTREAM$.get()));
      boolean forwardarrowP = ((BooleanWrapper)(KeyValueList.dynamicSlotValue(rule.dynamicSlots, Logic.SYM_LOGIC_FORWARD_ONLYp, Stella.FALSE_WRAPPER))).wrapperValue &&
          (!reversepolarityP);
      boolean reverseargumentsP = forwardarrowP ||
          reversepolarityP;
      int currentindentcounter = ((Integer)(Logic.$INDENTCOUNTER$.get())).intValue();
      Surrogate operatorprefix = Proposition.chooseImplicationOperator(rule, forwardarrowP);
      int operatorprefixindent = 2 + (operatorprefix.symbolName).length();
      boolean mapheadvariablesP = Description.namedDescriptionP(head);
      Vector ruleVariables = ((Vector)(KeyValueList.dynamicSlotValue(rule.dynamicSlots, Logic.SYM_LOGIC_IO_VARIABLES, null)));
      KeyValueMap headvariablemapping = null;
      KeyValueMap tailvariablemapping = null;

      if (head.deletedP() ||
          tail.deletedP()) {
        stream.nativeStream.print("(=> <DeLeTeD ArGuMeNt(S)>)");
        return;
      }
      if (reverseargumentsP) {
        { Description temp = head;

          head = tail;
          tail = temp;
        }
        mapheadvariablesP = !mapheadvariablesP;
      }
      if (ruleVariables != null) {
        headvariablemapping = ((KeyValueMap)(Logic.createSkolemMappingTable(head.ioVariables, ruleVariables)));
        tailvariablemapping = ((KeyValueMap)(Logic.createSkolemMappingTable(tail.ioVariables, ruleVariables)));
      }
      else if (mapheadvariablesP) {
        ruleVariables = tail.ioVariables;
        headvariablemapping = ((KeyValueMap)(Logic.createSkolemMappingTable(head.ioVariables, ruleVariables)));
      }
      else {
        ruleVariables = head.ioVariables;
        tailvariablemapping = ((KeyValueMap)(Logic.createSkolemMappingTable(tail.ioVariables, ruleVariables)));
      }
      { Object old$Indentcounter$000 = Logic.$INDENTCOUNTER$.get();

        try {
          Native.setIntSpecial(Logic.$INDENTCOUNTER$, currentindentcounter);
          stream.nativeStream.print("(" + Logic.stringifiedSurrogate(Logic.SGT_PL_KERNEL_KB_FORALL) + " ");
          Logic.printKifQuantifiedVariables(ruleVariables, false);
          stream.nativeStream.println();
          Logic.increaseIndent(Stella.NULL_INTEGER);
          Logic.printIndent(stream, Stella.NULL_INTEGER);
          stream.nativeStream.print("(" + Logic.stringifiedSurrogate(operatorprefix) + " ");
          Logic.increaseIndent(operatorprefixindent);
          { Object old$Skolemnamemappingtable$000 = Logic.$SKOLEMNAMEMAPPINGTABLE$.get();

            try {
              Native.setSpecial(Logic.$SKOLEMNAMEMAPPINGTABLE$, headvariablemapping);
              Description.printKifDescriptionProposition(head, reversepolarityP);

            } finally {
              Logic.$SKOLEMNAMEMAPPINGTABLE$.set(old$Skolemnamemappingtable$000);
            }
          }
          stream.nativeStream.println();
          Logic.printIndent(stream, Stella.NULL_INTEGER);
          { Object old$Skolemnamemappingtable$001 = Logic.$SKOLEMNAMEMAPPINGTABLE$.get();

            try {
              Native.setSpecial(Logic.$SKOLEMNAMEMAPPINGTABLE$, tailvariablemapping);
              Description.printKifDescriptionProposition(tail, reversepolarityP);

            } finally {
              Logic.$SKOLEMNAMEMAPPINGTABLE$.set(old$Skolemnamemappingtable$001);
            }
          }
          stream.nativeStream.print("))");
          Logic.decreaseIndent(operatorprefixindent);
          Logic.decreaseIndent(Stella.NULL_INTEGER);

        } finally {
          Logic.$INDENTCOUNTER$.set(old$Indentcounter$000);
        }
      }
    }
  }