Lord! What are the program for automated theorem proving Gerhard Gentzen-style without using prenex form for formulas ? With respect Alexander A. Dorin e-mail alex_dorin at rambler.ru skype alexander_a_dorin