def unit_propagate(clauses, symbol):
 output = []
 for c in clauses:
  if (c.func != Or):
   output.append(c)
   continue
  for arg in c.args:
   if (arg == (~ symbol)):
    output.append(Or(*[x for x in c.args if (x != (~ symbol))]))
    break
   if (arg == symbol):
    break
  else:
   output.append(c)
 return output

def unit_propagate ( clauses , symbol ) : output = [ ] for c in clauses : if ( c . func != Or ) : output . append ( c ) continue for arg in c . args : if ( arg == ( ~ symbol ) ) : output . append ( Or ( * [ x for x in c . args if ( x != ( ~ symbol ) ) ] ) ) break if ( arg == symbol ) : break else : output . append ( c ) return output
returns an equivalent set of clauses if a set of clauses contains the unit clause l .