The size of formal proofs has some important theoretical implications in computational complexity theory. The problem of determining if some formula of Intuitionistic Propositional Logic and the purely implicational fragment of Minimal Logic (M(contains)) is a tautology is PSPACE-Complete. Any propositional logic with a natural deduction system that satisfies the sub- formula principle is PSPACE. To know if any tautology in M(contains) admits polynomially sized proof is related to whether NP = PSPACE. Proof compression techniques reported in literature use two main approaches to proof compressing: generating already compressed proofs; compressing an already generated proof. Proposed by Gordeev and Haeusler (6), the Horizontal Compression is a natural deduction proof compression technique that uses directed graphs to represent proofs. Given a tautology proof in M(contains), which may have an exponential size in relation to conclusion length, the goal of Horizontal Compression is that the compressed proof has a polynomially limited size in relation to conclusion length. Our work presents the first implementation of Horizontal Compression, together with the first results of the execution of the technique on proofs of M(contains) tautologies.