Untitled

import itertools

def pl_resolution(clauses):
    def negate_literal(literal):
        if literal.startswith('~'):
            return literal[1:]
        else:
            return '~' + literal

    def resolve(ci, cj):
        resolvents = []
        for di in ci:
            for dj in cj:
                if di == negate_literal(dj):
                    new_clause = list(set(ci + cj) - {di, dj})
                    if new_clause:
                        resolvents.append(new_clause)
        return resolvents

    def is_subset(c1, c2):
        return all(any(x in d for d in c2) for x in c1)

    new_clauses = clauses[:]
    while True:
        new = []
        for (ci, cj) in itertools.combinations(new_clauses, 2):
            resolvents = resolve(ci, cj)
            for resolvent in resolvents:
                if not resolvent:
                    return True
                if not any(is_subset(resolvent, clause) for clause in new_clauses + new):
                    new.append(resolvent)
        if all(any(is_subset(c, new) for new in new_clauses) for c in new):
            return False
        new_clauses.extend(new)

# Example usage
clauses = [
    ['P', 'Q'],
    ['~P'],
    ['~Q']
]

if pl_resolution(clauses):
    print("The set of clauses is unsatisfiable (contradiction found).")
else:
    print("The set of clauses is satisfiable (no contradiction found).")