for (int i = 0; i < trace.size(); i++) {            //For each clause
            for (int j = i + 1; i < trace.size(); j++) {    //For each clause after

                for (Literal li : trace.getClause(i).getLiterals()) {    //For each literal in the ith clause
                    for (Literal lj : trace.getClause(j).getLiterals()) {//For each literal in the jth clause
                        if (li.getName().equals(lj.getName()) &&              //If the literal name matches
                            li.getArguments().equals(lj.getArguments()) &&    //And the literals arguments matches
                            li.getTruth() != lj.getTruth()) {                 //But the truth value doesn't
                            //Create a new clause with the remaining literals from each clause

                        }
                    }
                }
            }
        }