public static Cons loomSatisfiesToKif(Cons tree, Cons implicitvariables) {
    { Stella_Object iovariables = tree.rest.value;
      Stella_Object body = tree.rest.rest.value;
      Cons substitution = Stella.NIL;

      if (!Stella_Object.consP(iovariables)) {
        iovariables = Cons.consList(Cons.cons(iovariables, Stella.NIL));
      }
      { Stella_Object v1 = null;
        Cons iter000 = ((Cons)(iovariables));
        Symbol v2 = null;
        Cons iter001 = implicitvariables;

        for (;(!(iter000 == Stella.NIL)) &&
                  (!(iter001 == Stella.NIL)); iter000 = iter000.rest, iter001 = iter001.rest) {
          v1 = iter000.value;
          v2 = ((Symbol)(iter001.value));
          substitution = Cons.cons(v2, substitution);
          substitution = Cons.cons(v1, substitution);
        }
      }
      Logic.substituteVariablesInTree(((Cons)(body)), substitution);
      return (((Cons)(body)));
    }
  }