QCNFClauseList propagate_literal(const QCNFLiteral& lit, const QCNFClause& c) {
    LOG_PRINT(LOG_DEBUG) << "propagate_literal called with lit=" << lit.first->toString()
            << " and clause c=" << convertFromQCNFClause(c).toString() << std::endl;
    boost::shared_ptr<Sentence> cnfLit = lit.first;
    // first figure out what kind of literal we have here.
    std::queue<QCNFClause> toProcess;
    QCNFClauseList processed;

    toProcess.push(c);
    while (!toProcess.empty()) {
        QCNFClause qClause = toProcess.front();
        LOG_PRINT(LOG_DEBUG) << "working on " << convertFromQCNFClause(qClause).toString() << std::endl;
        CNFClause cClause = qClause.first;
        toProcess.pop();
        bool addCurrentClause = true;
        if (isSimpleLiteral(cnfLit)) {
            // search for an occurrence of this atom in c
            CNFClause::iterator it = cClause.begin();
            while (it != cClause.end()) {
                boost::shared_ptr<Sentence> currentLit = *it;
                if (isSimpleLiteral(currentLit) && *cnfLit == *currentLit) {    // Propagating P into P
                    // if they intersect, rewrite the clause over the time where they don't intersect and continue
                    SISet litSet = lit.second;
                    SISet currentSet = qClause.second;
                    SISet intersect = intersection(litSet, currentSet);

                    if (intersect.size() != 0) {
                        LOG_PRINT(LOG_DEBUG) << "propagating " << cnfLit->toString() << " into " << currentLit->toString() << std::endl;

                        // if there is still a timepoint that the clause applies to, rewrite and continue
                        SISet leftover = currentSet;
                        leftover.subtract(intersect);
                        if (leftover.size() != 0) {
                            QCNFClause qRestricted = qClause;
                            qRestricted.second = leftover;
                            toProcess.push(qRestricted);
                            addCurrentClause = false;
                            break;
                        }
                    }
                } else if (isSimpleLiteral(currentLit) && isNegatedLiteral(currentLit, cnfLit)) {
                    // propagating !P into P (or vice versa)
                    // if they intersect, generate two clauses
                    SISet litSet = lit.second;
                    SISet currentSet = qClause.second;
                    SISet intersect = intersection(litSet, currentSet);

                    if (intersect.size() != 0) {
                        LOG_PRINT(LOG_DEBUG) << "propagating " << cnfLit->toString() << " into " << currentLit->toString() << std::endl;

                        SISet leftover = currentSet;
                        leftover.subtract(intersect);
                        if (leftover.size() != 0) {
                            // add a copy of this sentence only over leftover
                            QCNFClause qRestricted = qClause;
                            qRestricted.second = leftover;
                            toProcess.push(qRestricted);
                        }
                        // delete the current literal and rewrite the time where it applies
                        it = cClause.erase(it);
                        qClause.first = cClause;
                        qClause.second = intersect;
                        continue;
                    }
                } else if (boost::dynamic_pointer_cast<LiquidOp>(currentLit) != 0) {    // propagating P into [...]
                    boost::shared_ptr<LiquidOp> liqLit = boost::dynamic_pointer_cast<LiquidOp>(currentLit);
                    // first convert the time into a liquid interval
                    SISet liqLitSet = lit.second;
                    liqLitSet.setForceLiquid(true);
                    SISet currentSet = qClause.second;
                    SISet intersect = intersection(liqLitSet, currentSet);
                    if (intersect.size() != 0) {
                        // this is kinda cheap but it should work
                        // call this function again on the inside and fix the resulting sentence if necessary
                        QCNFLiteral newLit;
                        newLit.first = lit.first;
                        newLit.second = liqLitSet;

                        QCNFClause newClause;
                        SISet liqClauseSet = currentSet;
                        liqClauseSet.setForceLiquid(true);
                        newClause.first = convertToCNFClause(liqLit);
                        newClause.second = liqClauseSet;
                        QCNFClauseList newClauseList = propagate_literal(newLit, newClause);

                        // TODO: complete this!
                        throw std::runtime_error("unimplemented!");
                    }
                } else if (boost::dynamic_pointer_cast<DiamondOp>(currentLit) != 0) {
                    boost::shared_ptr<DiamondOp> diaCurrentLit = boost::dynamic_pointer_cast<DiamondOp>(currentLit);
                    // check to make sure we can propagate here

                    if (!(*diaCurrentLit->sentence() == *cnfLit) && isNegatedLiteral(diaCurrentLit->sentence(), cnfLit)) {
                        it++;
                        continue;
                    }

                    // double check that there is only one relation for now
                    if (diaCurrentLit->relations().size() != 1) {
                        throw std::runtime_error("handling more than one relation on a single diamond literal is currently unimplemented in unit_prop()");
                    }

                    Interval::INTERVAL_RELATION rel = *(diaCurrentLit->relations().begin());
                    SISet satisfiesRel = lit.second.satisfiesRelation(rel);
                    std::cout << "satisfiesRel = " << satisfiesRel.toString() << ", qclause.second = " << qClause.second.toString() << std::endl;
                    SISet intersect = intersection(satisfiesRel, qClause.second);
                    std::cout << "intersect = " << intersect.toString() << std::endl;
                    // if they don't intersect, nothing to propagate
                    if (intersect.size() == 0) {
                        it++;
                        continue;
                    }

                    if (*cnfLit == *diaCurrentLit->sentence()) {
                        // clause is satisfied, we can drop it (over the intersection that is)
                        SISet leftover = qClause.second;
                        leftover.subtract(intersect);
                        if (leftover.size() != 0) {
                            QCNFClause qRestricted = qClause;
                            qRestricted.second = leftover;
                            toProcess.push(qRestricted);
                            addCurrentClause = false;
                            break;
                        }
                    } else if (isNegatedLiteral(cnfLit, diaCurrentLit->sentence())) {

                    }


                }
                it++;
            }
        }
        if (addCurrentClause) processed.push_back(qClause);

    }
    LOG_PRINT(LOG_DEBUG) << "returning..." << std::endl;
    return processed;
}