public static Cons removeRedundantClauses(Cons clauses) {
    { Cons result = Stella.NIL;
      HashTable trueTable = HashTable.newHashTable();
      HashTable notTable = HashTable.newHashTable();
      List entries = null;
      List sharedVariables = List.newList();
      List knownVariables = List.newList();
      Symbol operator = null;
      boolean subsumedP = false;
      List operators = List.newList();

      { Cons clause = null;
        Cons iter000 = ((Cons)(Stella_Object.copyConsTree(clauses)));

        for (;!(iter000 == Stella.NIL); iter000 = iter000.rest) {
          clause = ((Cons)(iter000.value));
          if (clause.value == Logic.SYM_STELLA_NOT) {
            {
              operator = ((Symbol)(((Cons)(clause.rest.value)).value));
              operators.insertNew(operator);
              entries = ((List)(notTable.lookup(operator)));
              if (entries == null) {
                entries = List.newList();
              }
              entries.push(((Cons)(clause.rest.value)));
              notTable.insertAt(operator, entries);
            }
          }
          else {
            {
              operator = ((Symbol)(clause.value));
              operators.insertNew(operator);
              entries = ((List)(trueTable.lookup(operator)));
              if (entries == null) {
                entries = List.newList();
              }
              entries.push(clause);
              trueTable.insertAt(operator, entries);
            }
          }
          { Symbol v = null;
            Cons iter001 = Logic.getVariablesFromConsPropositions(Cons.consList(Cons.cons(clause, Stella.NIL))).theConsList;

            for (;!(iter001 == Stella.NIL); iter001 = iter001.rest) {
              v = ((Symbol)(iter001.value));
              if (knownVariables.memberP(v)) {
                sharedVariables.insertNew(v);
              }
              else {
                knownVariables.push(v);
              }
            }
          }
        }
      }
      { Symbol operator000 = null;
        Cons iter002 = operators.theConsList;

        for (;!(iter002 == Stella.NIL); iter002 = iter002.rest) {
          operator000 = ((Symbol)(iter002.value));
          entries = ((List)(trueTable.lookup(operator000)));
          if (entries != null) {
            { Cons clause1 = null;
              Cons iter003 = entries.theConsList;

              for (;!(iter003 == Stella.NIL); iter003 = iter003.rest) {
                clause1 = ((Cons)(iter003.value));
                subsumedP = false;
                { Cons clause2 = null;
                  Cons iter004 = entries.theConsList;

                  loop004 : for (;!(iter004 == Stella.NIL); iter004 = iter004.rest) {
                    clause2 = ((Cons)(iter004.value));
                    if (!(clause1 == clause2)) {
                      subsumedP = true;
                      { Stella_Object arg1 = null;
                        Cons iter005 = clause1.rest;
                        Stella_Object arg2 = null;
                        Cons iter006 = clause2.rest;

                        loop005 : for (;(!(iter005 == Stella.NIL)) &&
                                  (!(iter006 == Stella.NIL)); iter005 = iter005.rest, iter006 = iter006.rest) {
                          arg1 = iter005.value;
                          arg2 = iter006.value;
                          if ((!Stella_Object.equalConsTreesP(arg1, arg2)) &&
                              ((Stella_Object.symbolP(arg1) &&
                              sharedVariables.memberP(arg1)) ||
                               Stella_Object.consP(arg1))) {
                            subsumedP = false;
                            break loop005;
                          }
                        }
                      }
                      if (subsumedP) {
                        break loop004;
                      }
                    }
                  }
                }
                if (!subsumedP) {
                  result = Cons.cons(clause1, result);
                }
              }
            }
          }
          entries = ((List)(notTable.lookup(operator000)));
          if (entries != null) {
            { Cons clause1 = null;
              Cons iter007 = entries.theConsList;

              for (;!(iter007 == Stella.NIL); iter007 = iter007.rest) {
                clause1 = ((Cons)(iter007.value));
                subsumedP = false;
                { Cons clause2 = null;
                  Cons iter008 = entries.theConsList;

                  loop007 : for (;!(iter008 == Stella.NIL); iter008 = iter008.rest) {
                    clause2 = ((Cons)(iter008.value));
                    if (!(clause1 == clause2)) {
                      subsumedP = true;
                      { Stella_Object arg1 = null;
                        Cons iter009 = clause1.rest;
                        Stella_Object arg2 = null;
                        Cons iter010 = clause2.rest;

                        loop008 : for (;(!(iter009 == Stella.NIL)) &&
                                  (!(iter010 == Stella.NIL)); iter009 = iter009.rest, iter010 = iter010.rest) {
                          arg1 = iter009.value;
                          arg2 = iter010.value;
                          if ((!Stella_Object.equalConsTreesP(arg1, arg2)) &&
                              ((Stella_Object.symbolP(arg1) &&
                              sharedVariables.memberP(arg1)) ||
                               Stella_Object.consP(arg1))) {
                            subsumedP = false;
                            break loop008;
                          }
                        }
                      }
                      if (subsumedP) {
                        break loop007;
                      }
                    }
                  }
                }
                if (!subsumedP) {
                  result = Cons.cons(Cons.list$(Cons.cons(Logic.SYM_STELLA_NOT, Cons.cons(clause1, Cons.cons(Stella.NIL, Stella.NIL)))), result);
                }
              }
            }
          }
        }
      }
      return (result);
    }
  }