Converted names map to use *Formula as keys for future operations
Added next step of Tseitin algorithm which computes shorter names per subformula