Two tautologihood proof systems based on the split method

Two systems for generating of all propositional tautologies and only them are considered. In every of these calculuses there are one axiom and one rule of inference. Proofs for tautologies of many well-known classes with polinomial time recognition algorithm have linear length in these systems. Various formulae's characteristics that influence on length of proofs are studied (one of them is a symmetry of formulae).