def find_pure_symbol(symbols, unknown_clauses):
 for sym in symbols:
  (found_pos, found_neg) = (False, False)
  for c in unknown_clauses:
   if ((not found_pos) and (sym in disjuncts(c))):
    found_pos = True
   if ((not found_neg) and (Not(sym) in disjuncts(c))):
    found_neg = True
  if (found_pos != found_neg):
   return (sym, found_pos)
 return (None, None)

def find_pure_symbol ( symbols , unknown_clauses ) : for sym in symbols : ( found_pos , found_neg ) = ( False , False ) for c in unknown_clauses : if ( ( not found_pos ) and ( sym in disjuncts ( c ) ) ) : found_pos = True if ( ( not found_neg ) and ( Not ( sym ) in disjuncts ( c ) ) ) : found_neg = True if ( found_pos != found_neg ) : return ( sym , found_pos ) return ( None , None )
find a symbol and its value if it appears only as a positive literal in clauses .