#NEWLINE# def _clausify( expression ) : #NEWLINE# #INDENT# '\n    :param expression: a skolemized expression in CNF\n    ' #NEWLINE# if isinstance ( expression , AndExpression ) : #NEWLINE# #INDENT# return ( _clausify ( expression . first ) + _clausify ( expression . second ) ) #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( expression , OrExpression ) : #NEWLINE# #INDENT# first = _clausify ( expression . first ) #NEWLINE# second = _clausify ( expression . second ) #NEWLINE# assert ( len ( first ) == 1 ) #NEWLINE# assert ( len ( second ) == 1 ) #NEWLINE# return [ ( first [ 0 ] + second [ 0 ] ) ] #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( expression , EqualityExpression ) : #NEWLINE# #INDENT# return [ Clause ( [ expression ] ) ] #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( expression , ApplicationExpression ) : #NEWLINE# #INDENT# return [ Clause ( [ expression ] ) ] #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( expression , NegatedExpression ) : #NEWLINE# #INDENT# if isinstance ( expression . term , ApplicationExpression ) : #NEWLINE# #INDENT# return [ Clause ( [ expression ] ) ] #NEWLINE# #UNINDENT# else : #NEWLINE# #INDENT# if isinstance ( expression . term , EqualityExpression ) : #NEWLINE# #INDENT# return [ Clause ( [ expression ] ) ] #NEWLINE# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# #UNINDENT# raise ProverParseError ( )