    for clause in L:
        csat = False
        for p in clause:
            if not sm_doi.fixed_excludes_implicant(state,p):
                csat = True
                break
        if not csat:
            return False
    return True

def reduce_rspace(L,primes):
    &#34;&#34;&#34;Reduce the rspace L for the system given by primes so that trivially fixed
    nodes are factored out. The first element of the returned rspace (L2) will
    specify these trivially fixed nodes (i.e., they are factored on t