%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : GRP781-1 : TPTP v9.0.0. Released v5.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:08:40 AM UTC 2025
% Result : Unsatisfiable 130.57s 130.87s
% Output : Proof 130.67s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP781-1 : TPTP v9.0.0. Released v5.4.0.
% 0.10/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 17:06:35 EDT 2025
% 0.12/0.33 % CPUTime :
% 130.57/130.87 % SZS status Unsatisfiable
% 130.57/130.87 % SZS output start Proof
% 130.57/130.87 tff(m_type, type, (
% 130.57/130.87 m: ( $i * $i ) > $i)).
% 130.57/130.87 tff(c_type, type, (
% 130.57/130.87 c: ( $i * $i ) > $i)).
% 130.57/130.87 tff(z_type, type, (
% 130.57/130.87 z: $i)).
% 130.57/130.87 tff(y_type, type, (
% 130.57/130.87 y: $i)).
% 130.57/130.87 tff(x_type, type, (
% 130.57/130.87 x: $i)).
% 130.57/130.87 tff(inj_1_type, type, (
% 130.57/130.87 inj_1: ( $i * $i ) > $i)).
% 130.57/130.87 tff(inj_0_type, type, (
% 130.57/130.87 inj_0: ( $i * $i ) > $i)).
% 130.57/130.87 tff(1,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : ((~(m(Z, X) = m(Z, Y))) | (X = Y)) <=> ![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)),
% 130.57/130.87 inference(rewrite,[status(thm)],[])).
% 130.57/130.87 tff(2,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : ((~(m(Z, X) = m(Z, Y))) | (X = Y)) <=> ![Z: $i, Y: $i, X: $i] : ((~(m(Z, X) = m(Z, Y))) | (X = Y))),
% 130.57/130.87 inference(rewrite,[status(thm)],[])).
% 130.57/130.87 tff(3,axiom,(![Z: $i, Y: $i, X: $i] : ((~(m(Z, X) = m(Z, Y))) | (X = Y))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cancellation_001')).
% 130.57/130.87 tff(4,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : ((~(m(Z, X) = m(Z, Y))) | (X = Y))),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[3, 2])).
% 130.57/130.87 tff(5,plain,(
% 130.57/130.87 ![Z: $i, Y: $i, X: $i] : ((~(m(Z, X) = m(Z, Y))) | (X = Y))),
% 130.57/130.87 inference(skolemize,[status(sab)],[4])).
% 130.57/130.87 tff(6,plain,
% 130.57/130.87 (![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[5, 1])).
% 130.57/130.87 tff(7,plain,
% 130.57/130.87 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(x, z), c(y, z)))) = m(c(x, z), c(y, z)))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(8,plain,
% 130.57/130.87 (inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(x, z), c(y, z)))) = m(c(x, z), c(y, z))),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[7, 6])).
% 130.57/130.87 tff(9,plain,
% 130.57/130.87 (^[Z: $i, Y: $i, X: $i] : refl((m(X, m(Y, Z)) = m(m(X, Y), Z)) <=> (m(X, m(Y, Z)) = m(m(X, Y), Z)))),
% 130.57/130.87 inference(bind,[status(th)],[])).
% 130.57/130.87 tff(10,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z)) <=> ![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))),
% 130.57/130.87 inference(quant_intro,[status(thm)],[9])).
% 130.57/130.87 tff(11,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z)) <=> ![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))),
% 130.57/130.87 inference(rewrite,[status(thm)],[])).
% 130.57/130.87 tff(12,axiom,(![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','associativity')).
% 130.57/130.87 tff(13,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[12, 11])).
% 130.57/130.87 tff(14,plain,(
% 130.57/130.87 ![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))),
% 130.57/130.87 inference(skolemize,[status(sab)],[13])).
% 130.57/130.87 tff(15,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[14, 10])).
% 130.57/130.87 tff(16,plain,
% 130.57/130.87 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(x, z), m(z, y))) = m(m(m(z, x), m(x, z)), m(z, y)))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(17,plain,
% 130.57/130.87 (m(m(z, x), m(m(x, z), m(z, y))) = m(m(m(z, x), m(x, z)), m(z, y))),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[16, 15])).
% 130.57/130.87 tff(18,plain,
% 130.57/130.87 (m(m(m(z, x), m(x, z)), m(z, y)) = m(m(z, x), m(m(x, z), m(z, y)))),
% 130.57/130.87 inference(symmetry,[status(thm)],[17])).
% 130.57/130.87 tff(19,plain,
% 130.57/130.87 (m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z))) = m(m(m(z, x), m(m(x, z), m(z, y))), m(c(y, z), c(x, z)))),
% 130.57/130.87 inference(monotonicity,[status(thm)],[18])).
% 130.57/130.87 tff(20,plain,
% 130.57/130.87 (m(m(m(z, x), m(m(x, z), m(z, y))), m(c(y, z), c(x, z))) = m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z)))),
% 130.57/130.87 inference(symmetry,[status(thm)],[19])).
% 130.57/130.87 tff(21,plain,
% 130.57/130.87 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z)))) = m(m(m(z, x), m(m(x, z), m(z, y))), m(c(y, z), c(x, z))))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(22,plain,
% 130.57/130.87 (m(m(z, x), m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z)))) = m(m(m(z, x), m(m(x, z), m(z, y))), m(c(y, z), c(x, z)))),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[21, 15])).
% 130.57/130.87 tff(23,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : ((~(m(X, Z) = m(Y, Z))) | (X = Y)) <=> ![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)),
% 130.57/130.87 inference(rewrite,[status(thm)],[])).
% 130.57/130.87 tff(24,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : ((~(m(X, Z) = m(Y, Z))) | (X = Y)) <=> ![Z: $i, Y: $i, X: $i] : ((~(m(X, Z) = m(Y, Z))) | (X = Y))),
% 130.57/130.87 inference(rewrite,[status(thm)],[])).
% 130.57/130.87 tff(25,axiom,(![Z: $i, Y: $i, X: $i] : ((~(m(X, Z) = m(Y, Z))) | (X = Y))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','cancellation')).
% 130.57/130.87 tff(26,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : ((~(m(X, Z) = m(Y, Z))) | (X = Y))),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[25, 24])).
% 130.57/130.87 tff(27,plain,(
% 130.57/130.87 ![Z: $i, Y: $i, X: $i] : ((~(m(X, Z) = m(Y, Z))) | (X = Y))),
% 130.57/130.87 inference(skolemize,[status(sab)],[26])).
% 130.57/130.87 tff(28,plain,
% 130.57/130.87 (![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[27, 23])).
% 130.57/130.87 tff(29,plain,
% 130.57/130.87 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(x, m(m(c(x, z), m(m(x, m(z, y)), z)), x)) = m(c(x, z), m(m(x, m(z, y)), z)))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(30,plain,
% 130.57/130.87 (inj_0(x, m(m(c(x, z), m(m(x, m(z, y)), z)), x)) = m(c(x, z), m(m(x, m(z, y)), z))),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[29, 28])).
% 130.57/130.87 tff(31,plain,
% 130.57/130.87 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(m(m(x, m(z, y)), z), x)) = m(m(c(x, z), m(m(x, m(z, y)), z)), x))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(32,plain,
% 130.57/130.87 (m(c(x, z), m(m(m(x, m(z, y)), z), x)) = m(m(c(x, z), m(m(x, m(z, y)), z)), x)),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[31, 15])).
% 130.57/130.87 tff(33,plain,
% 130.57/130.87 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, m(z, y)), m(z, x)) = m(m(m(x, m(z, y)), z), x))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(34,plain,
% 130.57/130.87 (m(m(x, m(z, y)), m(z, x)) = m(m(m(x, m(z, y)), z), x)),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[33, 15])).
% 130.57/130.87 tff(35,plain,
% 130.57/130.87 (m(m(m(x, m(z, y)), z), x) = m(m(x, m(z, y)), m(z, x))),
% 130.57/130.87 inference(symmetry,[status(thm)],[34])).
% 130.57/130.87 tff(36,plain,
% 130.57/130.87 (m(c(x, z), m(m(m(x, m(z, y)), z), x)) = m(c(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.87 inference(monotonicity,[status(thm)],[35])).
% 130.57/130.87 tff(37,plain,
% 130.57/130.87 (m(c(x, z), m(m(x, m(z, y)), m(z, x))) = m(c(x, z), m(m(m(x, m(z, y)), z), x))),
% 130.57/130.87 inference(symmetry,[status(thm)],[36])).
% 130.57/130.87 tff(38,plain,
% 130.57/130.87 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x))))) = m(c(x, z), m(m(x, m(z, y)), m(z, x))))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(39,plain,
% 130.57/130.87 (inj_1(m(z, x), m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x))))) = m(c(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[38, 6])).
% 130.57/130.87 tff(40,plain,
% 130.57/130.87 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(x, m(m(x, m(z, y)), m(x, z)))) = m(m(z, x), m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.87 inference(quant_inst,[status(thm)],[])).
% 130.57/130.87 tff(41,plain,
% 130.57/130.87 (m(z, m(x, m(m(x, m(z, y)), m(x, z)))) = m(m(z, x), m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.87 inference(unit_resolution,[status(thm)],[40, 15])).
% 130.57/130.87 tff(42,plain,
% 130.57/130.87 (^[Z: $i, Y: $i, X: $i] : refl((m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y))))) <=> (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y))))))),
% 130.57/130.87 inference(bind,[status(th)],[])).
% 130.57/130.87 tff(43,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y))))) <=> ![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))),
% 130.57/130.87 inference(quant_intro,[status(thm)],[42])).
% 130.57/130.87 tff(44,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y))))) <=> ![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))),
% 130.57/130.87 inference(rewrite,[status(thm)],[])).
% 130.57/130.87 tff(45,axiom,(![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','assumption')).
% 130.57/130.87 tff(46,plain,
% 130.57/130.87 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))),
% 130.57/130.87 inference(modus_ponens,[status(thm)],[45, 44])).
% 130.57/130.88 tff(47,plain,(
% 130.57/130.88 ![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))),
% 130.57/130.88 inference(skolemize,[status(sab)],[46])).
% 130.57/130.88 tff(48,plain,
% 130.57/130.88 (![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))),
% 130.57/130.88 inference(modus_ponens,[status(thm)],[47, 43])).
% 130.57/130.88 tff(49,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(z, m(x, m(m(x, m(z, y)), m(x, z)))) = m(x, m(z, m(m(x, m(z, y)), m(z, x)))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(50,plain,
% 130.57/130.88 (m(z, m(x, m(m(x, m(z, y)), m(x, z)))) = m(x, m(z, m(m(x, m(z, y)), m(z, x))))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[49, 48])).
% 130.57/130.88 tff(51,plain,
% 130.57/130.88 (m(x, m(z, m(m(x, m(z, y)), m(z, x)))) = m(z, m(x, m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[50])).
% 130.57/130.88 tff(52,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(z, m(m(x, m(z, y)), m(z, x)))) = m(m(x, z), m(m(x, m(z, y)), m(z, x))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(53,plain,
% 130.57/130.88 (m(x, m(z, m(m(x, m(z, y)), m(z, x)))) = m(m(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[52, 15])).
% 130.57/130.88 tff(54,plain,
% 130.57/130.88 (m(m(x, z), m(m(x, m(z, y)), m(z, x))) = m(x, m(z, m(m(x, m(z, y)), m(z, x))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[53])).
% 130.57/130.88 tff(55,plain,
% 130.57/130.88 (^[Y: $i, X: $i] : refl((m(Y, m(X, c(X, Y))) = m(X, Y)) <=> (m(Y, m(X, c(X, Y))) = m(X, Y)))),
% 130.57/130.88 inference(bind,[status(th)],[])).
% 130.57/130.88 tff(56,plain,
% 130.57/130.88 (![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y)) <=> ![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))),
% 130.57/130.88 inference(quant_intro,[status(thm)],[55])).
% 130.57/130.88 tff(57,plain,
% 130.57/130.88 (![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y)) <=> ![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))),
% 130.57/130.88 inference(rewrite,[status(thm)],[])).
% 130.57/130.88 tff(58,axiom,(![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','commutator')).
% 130.57/130.88 tff(59,plain,
% 130.57/130.88 (![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))),
% 130.57/130.88 inference(modus_ponens,[status(thm)],[58, 57])).
% 130.57/130.88 tff(60,plain,(
% 130.57/130.88 ![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))),
% 130.57/130.88 inference(skolemize,[status(sab)],[59])).
% 130.57/130.88 tff(61,plain,
% 130.57/130.88 (![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))),
% 130.57/130.88 inference(modus_ponens,[status(thm)],[60, 56])).
% 130.57/130.88 tff(62,plain,
% 130.57/130.88 ((~![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))) | (m(z, m(x, c(x, z))) = m(x, z))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(63,plain,
% 130.57/130.88 (m(z, m(x, c(x, z))) = m(x, z)),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[62, 61])).
% 130.57/130.88 tff(64,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(x, c(x, z))) = m(m(z, x), c(x, z)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(65,plain,
% 130.57/130.88 (m(z, m(x, c(x, z))) = m(m(z, x), c(x, z))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[64, 15])).
% 130.57/130.88 tff(66,plain,
% 130.57/130.88 (m(m(z, x), c(x, z)) = m(z, m(x, c(x, z)))),
% 130.57/130.88 inference(symmetry,[status(thm)],[65])).
% 130.57/130.88 tff(67,plain,
% 130.57/130.88 (m(m(z, x), c(x, z)) = m(x, z)),
% 130.57/130.88 inference(transitivity,[status(thm)],[66, 63])).
% 130.57/130.88 tff(68,plain,
% 130.57/130.88 (m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), m(z, x))) = m(m(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[67])).
% 130.57/130.88 tff(69,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x)))) = m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), m(z, x))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(70,plain,
% 130.57/130.88 (m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x)))) = m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[69, 15])).
% 130.57/130.88 tff(71,plain,
% 130.57/130.88 (m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x)))) = m(m(z, x), m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.88 inference(transitivity,[status(thm)],[70, 68, 54, 51, 41])).
% 130.57/130.88 tff(72,plain,
% 130.57/130.88 (inj_1(m(z, x), m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x))))) = inj_1(m(z, x), m(m(z, x), m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[71])).
% 130.57/130.88 tff(73,plain,
% 130.57/130.88 (inj_1(m(z, x), m(m(z, x), m(m(x, m(z, y)), m(x, z)))) = inj_1(m(z, x), m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x)))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[72])).
% 130.57/130.88 tff(74,plain,
% 130.57/130.88 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(m(x, m(z, y)), m(x, z)))) = m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(75,plain,
% 130.57/130.88 (inj_1(m(z, x), m(m(z, x), m(m(x, m(z, y)), m(x, z)))) = m(m(x, m(z, y)), m(x, z))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[74, 6])).
% 130.57/130.88 tff(76,plain,
% 130.57/130.88 (m(m(x, m(z, y)), m(x, z)) = inj_1(m(z, x), m(m(z, x), m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[75])).
% 130.57/130.88 tff(77,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(z, y)) = m(m(x, z), y))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(78,plain,
% 130.57/130.88 (m(x, m(z, y)) = m(m(x, z), y)),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[77, 15])).
% 130.57/130.88 tff(79,plain,
% 130.57/130.88 (m(m(x, z), y) = m(x, m(z, y))),
% 130.57/130.88 inference(symmetry,[status(thm)],[78])).
% 130.57/130.88 tff(80,plain,
% 130.57/130.88 (m(m(z, m(x, c(x, z))), y) = m(m(x, z), y)),
% 130.57/130.88 inference(monotonicity,[status(thm)],[63])).
% 130.57/130.88 tff(81,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(x, c(x, z)), y)) = m(m(z, m(x, c(x, z))), y))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(82,plain,
% 130.57/130.88 (m(z, m(m(x, c(x, z)), y)) = m(m(z, m(x, c(x, z))), y)),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[81, 15])).
% 130.57/130.88 tff(83,plain,
% 130.57/130.88 (m(z, m(m(x, c(x, z)), y)) = m(x, m(z, y))),
% 130.57/130.88 inference(transitivity,[status(thm)],[82, 80, 79])).
% 130.57/130.88 tff(84,plain,
% 130.57/130.88 (m(m(z, m(m(x, c(x, z)), y)), m(x, z)) = m(m(x, m(z, y)), m(x, z))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[83])).
% 130.57/130.88 tff(85,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(m(x, c(x, z)), y), m(x, z))) = m(m(z, m(m(x, c(x, z)), y)), m(x, z)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(86,plain,
% 130.57/130.88 (m(z, m(m(m(x, c(x, z)), y), m(x, z))) = m(m(z, m(m(x, c(x, z)), y)), m(x, z))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[85, 15])).
% 130.57/130.88 tff(87,plain,
% 130.57/130.88 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(m(m(x, c(x, z)), y), m(x, z)))) = m(m(m(x, c(x, z)), y), m(x, z)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(88,plain,
% 130.57/130.88 (inj_1(m(z, x), m(m(z, x), m(m(m(x, c(x, z)), y), m(x, z)))) = m(m(m(x, c(x, z)), y), m(x, z))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[87, 6])).
% 130.57/130.88 tff(89,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(x, m(m(m(x, c(x, z)), y), m(x, z)))) = m(m(z, x), m(m(m(x, c(x, z)), y), m(x, z))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(90,plain,
% 130.57/130.88 (m(z, m(x, m(m(m(x, c(x, z)), y), m(x, z)))) = m(m(z, x), m(m(m(x, c(x, z)), y), m(x, z)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[89, 15])).
% 130.57/130.88 tff(91,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(x, m(z, m(m(m(x, c(x, z)), y), m(z, x)))) = m(z, m(x, m(m(m(x, c(x, z)), y), m(x, z)))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(92,plain,
% 130.57/130.88 (m(x, m(z, m(m(m(x, c(x, z)), y), m(z, x)))) = m(z, m(x, m(m(m(x, c(x, z)), y), m(x, z))))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[91, 48])).
% 130.57/130.88 tff(93,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(z, m(m(m(x, c(x, z)), y), m(z, x)))) = m(m(x, z), m(m(m(x, c(x, z)), y), m(z, x))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(94,plain,
% 130.57/130.88 (m(x, m(z, m(m(m(x, c(x, z)), y), m(z, x)))) = m(m(x, z), m(m(m(x, c(x, z)), y), m(z, x)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[93, 15])).
% 130.57/130.88 tff(95,plain,
% 130.57/130.88 (m(m(x, z), m(m(m(x, c(x, z)), y), m(z, x))) = m(x, m(z, m(m(m(x, c(x, z)), y), m(z, x))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[94])).
% 130.57/130.88 tff(96,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(m(m(x, c(x, z)), y), m(z, x))) = m(m(m(x, z), m(m(x, c(x, z)), y)), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(97,plain,
% 130.57/130.88 (m(m(x, z), m(m(m(x, c(x, z)), y), m(z, x))) = m(m(m(x, z), m(m(x, c(x, z)), y)), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[96, 15])).
% 130.57/130.88 tff(98,plain,
% 130.57/130.88 (m(m(m(x, z), m(m(x, c(x, z)), y)), m(z, x)) = m(m(x, z), m(m(m(x, c(x, z)), y), m(z, x)))),
% 130.57/130.88 inference(symmetry,[status(thm)],[97])).
% 130.57/130.88 tff(99,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(x, m(z, y))) = m(m(x, x), m(z, y)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(100,plain,
% 130.57/130.88 (m(x, m(x, m(z, y))) = m(m(x, x), m(z, y))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[99, 15])).
% 130.57/130.88 tff(101,plain,
% 130.57/130.88 (m(x, m(z, m(m(x, c(x, z)), y))) = m(x, m(x, m(z, y)))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[83])).
% 130.57/130.88 tff(102,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(z, m(m(x, c(x, z)), y))) = m(m(x, z), m(m(x, c(x, z)), y)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(103,plain,
% 130.57/130.88 (m(x, m(z, m(m(x, c(x, z)), y))) = m(m(x, z), m(m(x, c(x, z)), y))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[102, 15])).
% 130.57/130.88 tff(104,plain,
% 130.57/130.88 (m(m(x, z), m(m(x, c(x, z)), y)) = m(x, m(z, m(m(x, c(x, z)), y)))),
% 130.57/130.88 inference(symmetry,[status(thm)],[103])).
% 130.57/130.88 tff(105,plain,
% 130.57/130.88 (m(m(x, z), m(m(x, c(x, z)), y)) = m(m(x, x), m(z, y))),
% 130.57/130.88 inference(transitivity,[status(thm)],[104, 101, 100])).
% 130.57/130.88 tff(106,plain,
% 130.57/130.88 (m(m(m(x, z), m(m(x, c(x, z)), y)), m(z, x)) = m(m(m(x, x), m(z, y)), m(z, x))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[105])).
% 130.57/130.88 tff(107,plain,
% 130.57/130.88 (m(m(m(x, x), m(z, y)), m(z, x)) = m(m(m(x, z), m(m(x, c(x, z)), y)), m(z, x))),
% 130.57/130.88 inference(symmetry,[status(thm)],[106])).
% 130.57/130.88 tff(108,plain,
% 130.57/130.88 (m(m(m(z, x), c(x, z)), m(m(x, c(x, z)), y)) = m(m(x, z), m(m(x, c(x, z)), y))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[67])).
% 130.57/130.88 tff(109,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(c(x, z), m(m(x, c(x, z)), y))) = m(m(m(z, x), c(x, z)), m(m(x, c(x, z)), y)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(110,plain,
% 130.57/130.88 (m(m(z, x), m(c(x, z), m(m(x, c(x, z)), y))) = m(m(m(z, x), c(x, z)), m(m(x, c(x, z)), y))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[109, 15])).
% 130.57/130.88 tff(111,plain,
% 130.57/130.88 (m(m(z, x), m(c(x, z), m(m(x, c(x, z)), y))) = m(m(x, x), m(z, y))),
% 130.57/130.88 inference(transitivity,[status(thm)],[110, 108, 104, 101, 100])).
% 130.57/130.88 tff(112,plain,
% 130.57/130.88 (m(m(m(z, x), m(c(x, z), m(m(x, c(x, z)), y))), m(z, x)) = m(m(m(x, x), m(z, y)), m(z, x))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[111])).
% 130.57/130.88 tff(113,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x))) = m(m(m(z, x), m(c(x, z), m(m(x, c(x, z)), y))), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(114,plain,
% 130.57/130.88 (m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x))) = m(m(m(z, x), m(c(x, z), m(m(x, c(x, z)), y))), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[113, 15])).
% 130.57/130.88 tff(115,plain,
% 130.57/130.88 (m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x))) = m(m(z, x), m(m(m(x, c(x, z)), y), m(x, z)))),
% 130.57/130.88 inference(transitivity,[status(thm)],[114, 112, 107, 98, 95, 92, 90])).
% 130.57/130.88 tff(116,plain,
% 130.57/130.88 (inj_1(m(z, x), m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x)))) = inj_1(m(z, x), m(m(z, x), m(m(m(x, c(x, z)), y), m(x, z))))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[115])).
% 130.57/130.88 tff(117,plain,
% 130.57/130.88 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x)))) = m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(118,plain,
% 130.57/130.88 (inj_1(m(z, x), m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x)))) = m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[117, 6])).
% 130.57/130.88 tff(119,plain,
% 130.57/130.88 (m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x)) = inj_1(m(z, x), m(m(z, x), m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[118])).
% 130.57/130.88 tff(120,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(m(m(x, c(x, z)), y), m(z, x))) = m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(121,plain,
% 130.57/130.88 (m(c(x, z), m(m(m(x, c(x, z)), y), m(z, x))) = m(m(c(x, z), m(m(x, c(x, z)), y)), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[120, 15])).
% 130.57/130.88 tff(122,plain,
% 130.57/130.88 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(z, m(z, m(m(m(x, c(x, z)), y), m(z, x)))) = m(m(m(x, c(x, z)), y), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(123,plain,
% 130.57/130.88 (inj_1(z, m(z, m(m(m(x, c(x, z)), y), m(z, x)))) = m(m(m(x, c(x, z)), y), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[122, 6])).
% 130.57/130.88 tff(124,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(m(x, c(x, z)), y), m(z, x))) = m(m(z, m(m(x, c(x, z)), y)), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(125,plain,
% 130.57/130.88 (m(z, m(m(m(x, c(x, z)), y), m(z, x))) = m(m(z, m(m(x, c(x, z)), y)), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[124, 15])).
% 130.57/130.88 tff(126,plain,
% 130.57/130.88 (m(m(z, m(m(x, c(x, z)), y)), m(z, x)) = m(z, m(m(m(x, c(x, z)), y), m(z, x)))),
% 130.57/130.88 inference(symmetry,[status(thm)],[125])).
% 130.57/130.88 tff(127,plain,
% 130.57/130.88 (m(m(z, m(m(x, c(x, z)), y)), m(z, x)) = m(m(x, m(z, y)), m(z, x))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[83])).
% 130.57/130.88 tff(128,plain,
% 130.57/130.88 (m(m(x, m(z, y)), m(z, x)) = m(m(z, m(m(x, c(x, z)), y)), m(z, x))),
% 130.57/130.88 inference(symmetry,[status(thm)],[127])).
% 130.57/130.88 tff(129,plain,
% 130.57/130.88 (m(m(m(x, z), y), m(z, x)) = m(m(x, m(z, y)), m(z, x))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[79])).
% 130.57/130.88 tff(130,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(y, m(z, x))) = m(m(m(x, z), y), m(z, x)))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(131,plain,
% 130.57/130.88 (m(m(x, z), m(y, m(z, x))) = m(m(m(x, z), y), m(z, x))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[130, 15])).
% 130.57/130.88 tff(132,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(z, m(y, m(z, x)))) = m(m(x, z), m(y, m(z, x))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(133,plain,
% 130.57/130.88 (m(x, m(z, m(y, m(z, x)))) = m(m(x, z), m(y, m(z, x)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[132, 15])).
% 130.57/130.88 tff(134,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(x, m(z, m(y, m(z, x)))) = m(z, m(x, m(y, m(x, z)))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(135,plain,
% 130.57/130.88 (m(x, m(z, m(y, m(z, x)))) = m(z, m(x, m(y, m(x, z))))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[134, 48])).
% 130.57/130.88 tff(136,plain,
% 130.57/130.88 (m(z, m(x, m(y, m(x, z)))) = m(x, m(z, m(y, m(z, x))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[135])).
% 130.57/130.88 tff(137,plain,
% 130.57/130.88 (m(z, m(x, m(y, m(x, z)))) = m(z, m(m(m(x, c(x, z)), y), m(z, x)))),
% 130.57/130.88 inference(transitivity,[status(thm)],[136, 133, 131, 129, 128, 126])).
% 130.57/130.88 tff(138,plain,
% 130.57/130.88 (inj_1(z, m(z, m(x, m(y, m(x, z))))) = inj_1(z, m(z, m(m(m(x, c(x, z)), y), m(z, x))))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[137])).
% 130.57/130.88 tff(139,plain,
% 130.57/130.88 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(z, m(z, m(x, m(y, m(x, z))))) = m(x, m(y, m(x, z))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(140,plain,
% 130.57/130.88 (inj_1(z, m(z, m(x, m(y, m(x, z))))) = m(x, m(y, m(x, z)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[139, 6])).
% 130.57/130.88 tff(141,plain,
% 130.57/130.88 (m(x, m(y, m(x, z))) = inj_1(z, m(z, m(x, m(y, m(x, z)))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[140])).
% 130.57/130.88 tff(142,plain,
% 130.57/130.88 (m(y, m(z, m(x, c(x, z)))) = m(y, m(x, z))),
% 130.57/130.88 inference(monotonicity,[status(thm)],[63])).
% 130.57/130.88 tff(143,plain,
% 130.57/130.88 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(y, m(z, m(x, c(x, z)))) = m(m(y, z), m(x, c(x, z))))),
% 130.57/130.88 inference(quant_inst,[status(thm)],[])).
% 130.57/130.88 tff(144,plain,
% 130.57/130.88 (m(y, m(z, m(x, c(x, z)))) = m(m(y, z), m(x, c(x, z)))),
% 130.57/130.88 inference(unit_resolution,[status(thm)],[143, 15])).
% 130.57/130.88 tff(145,plain,
% 130.57/130.88 (m(m(y, z), m(x, c(x, z))) = m(y, m(z, m(x, c(x, z))))),
% 130.57/130.88 inference(symmetry,[status(thm)],[144])).
% 130.57/130.88 tff(146,plain,
% 130.57/130.88 (m(m(y, z), m(x, c(x, z))) = m(y, m(x, z))),
% 130.57/130.88 inference(transitivity,[status(thm)],[145, 142])).
% 130.57/130.88 tff(147,plain,
% 130.57/130.88 (m(x, m(m(y, z), m(x, c(x, z)))) = m(x, m(y, m(x, z)))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[146])).
% 130.57/130.89 tff(148,plain,
% 130.57/130.89 (m(x, m(m(y, z), m(x, c(x, z)))) = m(m(m(x, c(x, z)), y), m(z, x))),
% 130.57/130.89 inference(transitivity,[status(thm)],[147, 141, 138, 123])).
% 130.57/130.89 tff(149,plain,
% 130.57/130.89 (m(c(x, z), m(x, m(m(y, z), m(x, c(x, z))))) = m(c(x, z), m(m(m(x, c(x, z)), y), m(z, x)))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[148])).
% 130.57/130.89 tff(150,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(c(x, z), m(x, m(m(y, z), m(x, c(x, z))))) = m(x, m(c(x, z), m(m(y, z), m(c(x, z), x)))))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(151,plain,
% 130.57/130.89 (m(c(x, z), m(x, m(m(y, z), m(x, c(x, z))))) = m(x, m(c(x, z), m(m(y, z), m(c(x, z), x))))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[150, 48])).
% 130.57/130.89 tff(152,plain,
% 130.57/130.89 (m(x, m(c(x, z), m(m(y, z), m(c(x, z), x)))) = m(c(x, z), m(x, m(m(y, z), m(x, c(x, z)))))),
% 130.57/130.89 inference(symmetry,[status(thm)],[151])).
% 130.57/130.89 tff(153,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(m(y, z), m(c(x, z), x))) = m(m(c(x, z), m(y, z)), m(c(x, z), x)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(154,plain,
% 130.57/130.89 (m(c(x, z), m(m(y, z), m(c(x, z), x))) = m(m(c(x, z), m(y, z)), m(c(x, z), x))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[153, 15])).
% 130.57/130.89 tff(155,plain,
% 130.57/130.89 (m(m(c(x, z), m(y, z)), m(c(x, z), x)) = m(c(x, z), m(m(y, z), m(c(x, z), x)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[154])).
% 130.57/130.89 tff(156,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(y, z)) = m(m(c(x, z), y), z))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(157,plain,
% 130.57/130.89 (m(c(x, z), m(y, z)) = m(m(c(x, z), y), z)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[156, 15])).
% 130.57/130.89 tff(158,plain,
% 130.57/130.89 (m(m(c(x, z), m(y, z)), m(c(x, z), x)) = m(m(m(c(x, z), y), z), m(c(x, z), x))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[157])).
% 130.57/130.89 tff(159,plain,
% 130.57/130.89 (m(m(m(c(x, z), y), z), m(c(x, z), x)) = m(m(c(x, z), m(y, z)), m(c(x, z), x))),
% 130.57/130.89 inference(symmetry,[status(thm)],[158])).
% 130.57/130.89 tff(160,plain,
% 130.57/130.89 (m(m(m(c(x, z), y), z), m(c(x, z), x)) = m(c(x, z), m(m(y, z), m(c(x, z), x)))),
% 130.57/130.89 inference(transitivity,[status(thm)],[159, 155])).
% 130.57/130.89 tff(161,plain,
% 130.57/130.89 (m(x, m(m(m(c(x, z), y), z), m(c(x, z), x))) = m(x, m(c(x, z), m(m(y, z), m(c(x, z), x))))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[160])).
% 130.57/130.89 tff(162,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(m(m(c(x, z), y), z), m(c(x, z), x))) = m(m(x, m(m(c(x, z), y), z)), m(c(x, z), x)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(163,plain,
% 130.57/130.89 (m(x, m(m(m(c(x, z), y), z), m(c(x, z), x))) = m(m(x, m(m(c(x, z), y), z)), m(c(x, z), x))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[162, 15])).
% 130.57/130.89 tff(164,plain,
% 130.57/130.89 (m(m(x, m(m(c(x, z), y), z)), m(c(x, z), x)) = m(x, m(m(m(c(x, z), y), z), m(c(x, z), x)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[163])).
% 130.57/130.89 tff(165,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(m(c(x, z), y), z)) = m(m(x, m(c(x, z), y)), z))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(166,plain,
% 130.57/130.89 (m(x, m(m(c(x, z), y), z)) = m(m(x, m(c(x, z), y)), z)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[165, 15])).
% 130.57/130.89 tff(167,plain,
% 130.57/130.89 (m(m(x, m(c(x, z), y)), z) = m(x, m(m(c(x, z), y), z))),
% 130.57/130.89 inference(symmetry,[status(thm)],[166])).
% 130.57/130.89 tff(168,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(c(x, z), y)) = m(m(x, c(x, z)), y))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(169,plain,
% 130.57/130.89 (m(x, m(c(x, z), y)) = m(m(x, c(x, z)), y)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[168, 15])).
% 130.57/130.89 tff(170,plain,
% 130.57/130.89 (m(m(x, m(c(x, z), y)), z) = m(m(m(x, c(x, z)), y), z)),
% 130.57/130.89 inference(monotonicity,[status(thm)],[169])).
% 130.57/130.89 tff(171,plain,
% 130.57/130.89 (m(m(m(x, c(x, z)), y), z) = m(m(x, m(c(x, z), y)), z)),
% 130.57/130.89 inference(symmetry,[status(thm)],[170])).
% 130.57/130.89 tff(172,plain,
% 130.57/130.89 (m(m(m(x, c(x, z)), y), z) = m(x, m(m(c(x, z), y), z))),
% 130.57/130.89 inference(transitivity,[status(thm)],[171, 167])).
% 130.57/130.89 tff(173,plain,
% 130.57/130.89 (m(m(m(m(x, c(x, z)), y), z), m(c(x, z), x)) = m(m(x, m(m(c(x, z), y), z)), m(c(x, z), x))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[172])).
% 130.57/130.89 tff(174,plain,
% 130.57/130.89 (m(m(m(m(x, c(x, z)), y), z), m(c(x, z), x)) = m(m(m(x, c(x, z)), y), m(x, z))),
% 130.57/130.89 inference(transitivity,[status(thm)],[173, 164, 161, 152, 149, 121, 119, 116, 88])).
% 130.57/130.89 tff(175,plain,
% 130.57/130.89 (m(z, m(m(m(m(x, c(x, z)), y), z), m(c(x, z), x))) = m(z, m(m(m(x, c(x, z)), y), m(x, z)))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[174])).
% 130.57/130.89 tff(176,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(m(m(x, c(x, z)), y), z), m(c(x, z), x))) = m(m(z, m(m(m(x, c(x, z)), y), z)), m(c(x, z), x)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(177,plain,
% 130.57/130.89 (m(z, m(m(m(m(x, c(x, z)), y), z), m(c(x, z), x))) = m(m(z, m(m(m(x, c(x, z)), y), z)), m(c(x, z), x))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[176, 15])).
% 130.57/130.89 tff(178,plain,
% 130.57/130.89 (m(m(z, m(m(m(x, c(x, z)), y), z)), m(c(x, z), x)) = m(z, m(m(m(m(x, c(x, z)), y), z), m(c(x, z), x)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[177])).
% 130.57/130.89 tff(179,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(m(x, c(x, z)), y), z)) = m(m(z, m(m(x, c(x, z)), y)), z))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(180,plain,
% 130.57/130.89 (m(z, m(m(m(x, c(x, z)), y), z)) = m(m(z, m(m(x, c(x, z)), y)), z)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[179, 15])).
% 130.57/130.89 tff(181,plain,
% 130.57/130.89 (m(m(z, m(m(x, c(x, z)), y)), z) = m(z, m(m(m(x, c(x, z)), y), z))),
% 130.57/130.89 inference(symmetry,[status(thm)],[180])).
% 130.57/130.89 tff(182,plain,
% 130.57/130.89 (m(m(z, m(m(x, c(x, z)), y)), z) = m(m(x, m(z, y)), z)),
% 130.57/130.89 inference(monotonicity,[status(thm)],[83])).
% 130.57/130.89 tff(183,plain,
% 130.57/130.89 (m(m(x, m(z, y)), z) = m(m(z, m(m(x, c(x, z)), y)), z)),
% 130.57/130.89 inference(symmetry,[status(thm)],[182])).
% 130.57/130.89 tff(184,plain,
% 130.57/130.89 (m(m(x, m(z, y)), z) = m(z, m(m(m(x, c(x, z)), y), z))),
% 130.57/130.89 inference(transitivity,[status(thm)],[183, 181])).
% 130.57/130.89 tff(185,plain,
% 130.57/130.89 (m(m(m(x, m(z, y)), z), m(c(x, z), x)) = m(m(z, m(m(m(x, c(x, z)), y), z)), m(c(x, z), x))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[184])).
% 130.57/130.89 tff(186,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, m(z, y)), z), m(c(x, z), x)) = m(m(m(m(x, m(z, y)), z), c(x, z)), x))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(187,plain,
% 130.57/130.89 (m(m(m(x, m(z, y)), z), m(c(x, z), x)) = m(m(m(m(x, m(z, y)), z), c(x, z)), x)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[186, 15])).
% 130.57/130.89 tff(188,plain,
% 130.57/130.89 (m(m(m(m(x, m(z, y)), z), c(x, z)), x) = m(m(m(x, m(z, y)), z), m(c(x, z), x))),
% 130.57/130.89 inference(symmetry,[status(thm)],[187])).
% 130.57/130.89 tff(189,plain,
% 130.57/130.89 (m(m(m(m(x, m(z, y)), z), c(x, z)), x) = m(m(c(x, z), m(m(x, m(z, y)), z)), x)),
% 130.57/130.89 inference(transitivity,[status(thm)],[188, 185, 178, 175, 86, 84, 76, 73, 39, 37, 32])).
% 130.57/130.89 tff(190,plain,
% 130.57/130.89 (inj_0(x, m(m(m(m(x, m(z, y)), z), c(x, z)), x)) = inj_0(x, m(m(c(x, z), m(m(x, m(z, y)), z)), x))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[189])).
% 130.57/130.89 tff(191,plain,
% 130.57/130.89 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(x, m(m(m(m(x, m(z, y)), z), c(x, z)), x)) = m(m(m(x, m(z, y)), z), c(x, z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(192,plain,
% 130.57/130.89 (inj_0(x, m(m(m(m(x, m(z, y)), z), c(x, z)), x)) = m(m(m(x, m(z, y)), z), c(x, z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[191, 28])).
% 130.57/130.89 tff(193,plain,
% 130.57/130.89 (m(m(m(x, m(z, y)), z), c(x, z)) = inj_0(x, m(m(m(m(x, m(z, y)), z), c(x, z)), x))),
% 130.57/130.89 inference(symmetry,[status(thm)],[192])).
% 130.57/130.89 tff(194,plain,
% 130.57/130.89 (m(m(m(x, z), y), z) = m(m(x, m(z, y)), z)),
% 130.57/130.89 inference(monotonicity,[status(thm)],[79])).
% 130.57/130.89 tff(195,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(y, z)) = m(m(m(x, z), y), z))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(196,plain,
% 130.57/130.89 (m(m(x, z), m(y, z)) = m(m(m(x, z), y), z)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[195, 15])).
% 130.57/130.89 tff(197,plain,
% 130.57/130.89 ((~![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))) | (m(z, m(y, c(y, z))) = m(y, z))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(198,plain,
% 130.57/130.89 (m(z, m(y, c(y, z))) = m(y, z)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[197, 61])).
% 130.57/130.89 tff(199,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(y, c(y, z))) = m(m(z, y), c(y, z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(200,plain,
% 130.57/130.89 (m(z, m(y, c(y, z))) = m(m(z, y), c(y, z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[199, 15])).
% 130.57/130.89 tff(201,plain,
% 130.57/130.89 (m(m(z, y), c(y, z)) = m(z, m(y, c(y, z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[200])).
% 130.57/130.89 tff(202,plain,
% 130.57/130.89 (m(m(z, y), c(y, z)) = m(y, z)),
% 130.57/130.89 inference(transitivity,[status(thm)],[201, 198])).
% 130.57/130.89 tff(203,plain,
% 130.57/130.89 (m(m(x, z), m(m(z, y), c(y, z))) = m(m(x, z), m(y, z))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[202])).
% 130.57/130.89 tff(204,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(m(z, y), c(y, z))) = m(m(m(x, z), m(z, y)), c(y, z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(205,plain,
% 130.57/130.89 (m(m(x, z), m(m(z, y), c(y, z))) = m(m(m(x, z), m(z, y)), c(y, z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[204, 15])).
% 130.57/130.89 tff(206,plain,
% 130.57/130.89 (m(m(m(x, z), m(z, y)), c(y, z)) = m(m(x, z), m(m(z, y), c(y, z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[205])).
% 130.57/130.89 tff(207,plain,
% 130.57/130.89 (m(m(m(x, z), m(z, y)), c(y, z)) = m(m(x, m(z, y)), z)),
% 130.57/130.89 inference(transitivity,[status(thm)],[206, 203, 196, 194])).
% 130.57/130.89 tff(208,plain,
% 130.57/130.89 (m(m(m(m(x, z), m(z, y)), c(y, z)), c(x, z)) = m(m(m(x, m(z, y)), z), c(x, z))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[207])).
% 130.57/130.89 tff(209,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z))) = m(m(m(m(x, z), m(z, y)), c(y, z)), c(x, z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(210,plain,
% 130.57/130.89 (m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z))) = m(m(m(m(x, z), m(z, y)), c(y, z)), c(x, z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[209, 15])).
% 130.57/130.89 tff(211,plain,
% 130.57/130.89 (m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z))) = m(c(x, z), m(m(x, m(z, y)), z))),
% 130.57/130.89 inference(transitivity,[status(thm)],[210, 208, 193, 190, 30])).
% 130.57/130.89 tff(212,plain,
% 130.57/130.89 (m(m(z, x), m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z)))) = m(m(z, x), m(c(x, z), m(m(x, m(z, y)), z)))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[211])).
% 130.57/130.89 tff(213,plain,
% 130.57/130.89 (m(m(z, x), m(c(x, z), m(m(x, m(z, y)), z))) = m(m(z, x), m(m(m(x, z), m(z, y)), m(c(y, z), c(x, z))))),
% 130.57/130.89 inference(symmetry,[status(thm)],[212])).
% 130.57/130.89 tff(214,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(c(x, z), m(m(x, m(z, y)), z))) = m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(215,plain,
% 130.57/130.89 (m(m(z, x), m(c(x, z), m(m(x, m(z, y)), z))) = m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[214, 15])).
% 130.57/130.89 tff(216,plain,
% 130.57/130.89 (m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), z)) = m(m(z, x), m(c(x, z), m(m(x, m(z, y)), z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[215])).
% 130.57/130.89 tff(217,plain,
% 130.57/130.89 (m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), z)) = m(m(x, z), m(m(x, m(z, y)), z))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[67])).
% 130.57/130.89 tff(218,plain,
% 130.57/130.89 (m(m(x, z), m(m(x, m(z, y)), z)) = m(m(m(z, x), c(x, z)), m(m(x, m(z, y)), z))),
% 130.57/130.89 inference(symmetry,[status(thm)],[217])).
% 130.57/130.89 tff(219,plain,
% 130.57/130.89 (m(z, m(m(m(x, c(x, z)), y), z)) = m(m(x, m(z, y)), z)),
% 130.57/130.89 inference(transitivity,[status(thm)],[180, 182])).
% 130.57/130.89 tff(220,plain,
% 130.57/130.89 (m(m(x, z), m(z, m(m(m(x, c(x, z)), y), z))) = m(m(x, z), m(m(x, m(z, y)), z))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[219])).
% 130.57/130.89 tff(221,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(z, m(m(m(x, c(x, z)), y), z))) = m(m(m(x, z), z), m(m(m(x, c(x, z)), y), z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(222,plain,
% 130.57/130.89 (m(m(x, z), m(z, m(m(m(x, c(x, z)), y), z))) = m(m(m(x, z), z), m(m(m(x, c(x, z)), y), z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[221, 15])).
% 130.57/130.89 tff(223,plain,
% 130.57/130.89 (m(m(m(x, z), z), m(m(m(x, c(x, z)), y), z)) = m(m(x, z), m(z, m(m(m(x, c(x, z)), y), z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[222])).
% 130.57/130.89 tff(224,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, c(x, z)), m(y, z)) = m(m(m(x, c(x, z)), y), z))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(225,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(y, z)) = m(m(m(x, c(x, z)), y), z)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[224, 15])).
% 130.57/130.89 tff(226,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(m(z, y), c(y, z))) = m(m(x, c(x, z)), m(y, z))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[202])).
% 130.57/130.89 tff(227,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, c(x, z)), m(m(z, y), c(y, z))) = m(m(m(x, c(x, z)), m(z, y)), c(y, z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(228,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(m(z, y), c(y, z))) = m(m(m(x, c(x, z)), m(z, y)), c(y, z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[227, 15])).
% 130.57/130.89 tff(229,plain,
% 130.57/130.89 (m(m(m(x, c(x, z)), m(z, y)), c(y, z)) = m(m(x, c(x, z)), m(m(z, y), c(y, z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[228])).
% 130.57/130.89 tff(230,plain,
% 130.57/130.89 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(m(z, y), m(x, z)), m(m(c(x, z), x), m(m(z, y), m(x, z)))) = m(c(x, z), x))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(231,plain,
% 130.57/130.89 (inj_0(m(m(z, y), m(x, z)), m(m(c(x, z), x), m(m(z, y), m(x, z)))) = m(c(x, z), x)),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[230, 28])).
% 130.57/130.89 tff(232,plain,
% 130.57/130.89 (m(z, m(y, m(z, m(x, c(x, z))))) = m(z, m(y, m(x, z)))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[142])).
% 130.57/130.89 tff(233,plain,
% 130.57/130.89 (m(z, m(y, m(x, z))) = m(z, m(y, m(z, m(x, c(x, z)))))),
% 130.57/130.89 inference(symmetry,[status(thm)],[232])).
% 130.57/130.89 tff(234,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(y, m(x, z))) = m(m(z, y), m(x, z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(235,plain,
% 130.57/130.89 (m(z, m(y, m(x, z))) = m(m(z, y), m(x, z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[234, 15])).
% 130.57/130.89 tff(236,plain,
% 130.57/130.89 (m(m(z, y), m(x, z)) = m(z, m(y, m(x, z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[235])).
% 130.57/130.89 tff(237,plain,
% 130.57/130.89 (m(m(z, y), m(x, z)) = m(z, m(y, m(z, m(x, c(x, z)))))),
% 130.57/130.89 inference(transitivity,[status(thm)],[236, 233])).
% 130.57/130.89 tff(238,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(m(z, y), m(x, z))) = m(m(x, c(x, z)), m(z, m(y, m(z, m(x, c(x, z))))))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[237])).
% 130.57/130.89 tff(239,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(z, m(y, m(z, m(x, c(x, z)))))) = m(m(x, c(x, z)), m(m(z, y), m(x, z)))),
% 130.57/130.89 inference(symmetry,[status(thm)],[238])).
% 130.57/130.89 tff(240,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(m(x, c(x, z)), m(z, m(y, m(z, m(x, c(x, z)))))) = m(z, m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z)))))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(241,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(z, m(y, m(z, m(x, c(x, z)))))) = m(z, m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z))))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[240, 48])).
% 130.57/130.89 tff(242,plain,
% 130.57/130.89 (m(z, m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z)))) = m(m(x, c(x, z)), m(z, m(y, m(z, m(x, c(x, z))))))),
% 130.57/130.89 inference(symmetry,[status(thm)],[241])).
% 130.57/130.89 tff(243,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z))) = m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(244,plain,
% 130.57/130.89 (m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z))) = m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[243, 15])).
% 130.57/130.89 tff(245,plain,
% 130.57/130.89 (m(z, m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z)))) = m(z, m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))),
% 130.57/130.89 inference(monotonicity,[status(thm)],[244])).
% 130.57/130.89 tff(246,plain,
% 130.57/130.89 (m(z, m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(z, m(m(x, c(x, z)), m(y, m(m(x, c(x, z)), z))))),
% 130.57/130.89 inference(symmetry,[status(thm)],[245])).
% 130.57/130.89 tff(247,plain,
% 130.57/130.89 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(m(z, m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z)))),
% 130.57/130.89 inference(quant_inst,[status(thm)],[])).
% 130.57/130.89 tff(248,plain,
% 130.57/130.89 (m(z, m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(m(z, m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z))),
% 130.57/130.89 inference(unit_resolution,[status(thm)],[247, 15])).
% 130.57/130.90 tff(249,plain,
% 130.57/130.90 (m(m(z, m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z)) = m(z, m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[248])).
% 130.57/130.90 tff(250,plain,
% 130.57/130.90 (m(m(z, m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z)) = m(m(x, m(z, y)), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[83])).
% 130.57/130.90 tff(251,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(m(x, c(x, z)), z)) = m(m(z, m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(symmetry,[status(thm)],[250])).
% 130.57/130.90 tff(252,plain,
% 130.57/130.90 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(x, m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z)))) = m(m(x, m(z, y)), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(253,plain,
% 130.57/130.90 (inj_1(x, m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z)))) = m(m(x, m(z, y)), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[252, 6])).
% 130.57/130.90 tff(254,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(c(x, z), y), m(m(z, x), c(x, z))) = m(m(m(c(x, z), y), m(z, x)), c(x, z)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(255,plain,
% 130.57/130.90 (m(m(c(x, z), y), m(m(z, x), c(x, z))) = m(m(m(c(x, z), y), m(z, x)), c(x, z))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[254, 15])).
% 130.57/130.90 tff(256,plain,
% 130.57/130.90 (m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z)))) = m(m(z, x), m(m(m(c(x, z), y), m(z, x)), c(x, z)))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[255])).
% 130.57/130.90 tff(257,plain,
% 130.57/130.90 (m(m(z, x), m(m(m(c(x, z), y), m(z, x)), c(x, z))) = m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[256])).
% 130.57/130.90 tff(258,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(m(c(x, z), y), m(z, x)), c(x, z))) = m(m(m(z, x), m(m(c(x, z), y), m(z, x))), c(x, z)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(259,plain,
% 130.57/130.90 (m(m(z, x), m(m(m(c(x, z), y), m(z, x)), c(x, z))) = m(m(m(z, x), m(m(c(x, z), y), m(z, x))), c(x, z))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[258, 15])).
% 130.57/130.90 tff(260,plain,
% 130.57/130.90 (m(m(m(z, x), m(m(c(x, z), y), m(z, x))), c(x, z)) = m(m(z, x), m(m(m(c(x, z), y), m(z, x)), c(x, z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[259])).
% 130.57/130.90 tff(261,plain,
% 130.57/130.90 (m(m(m(z, x), c(x, z)), y) = m(m(x, z), y)),
% 130.57/130.90 inference(monotonicity,[status(thm)],[67])).
% 130.57/130.90 tff(262,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(c(x, z), y)) = m(m(m(z, x), c(x, z)), y))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(263,plain,
% 130.57/130.90 (m(m(z, x), m(c(x, z), y)) = m(m(m(z, x), c(x, z)), y)),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[262, 15])).
% 130.57/130.90 tff(264,plain,
% 130.57/130.90 (m(m(z, x), m(c(x, z), y)) = m(x, m(z, y))),
% 130.57/130.90 inference(transitivity,[status(thm)],[263, 261, 79])).
% 130.57/130.90 tff(265,plain,
% 130.57/130.90 (m(m(m(z, x), m(c(x, z), y)), m(z, x)) = m(m(x, m(z, y)), m(z, x))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[264])).
% 130.57/130.90 tff(266,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(c(x, z), y), m(z, x))) = m(m(m(z, x), m(c(x, z), y)), m(z, x)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(267,plain,
% 130.57/130.90 (m(m(z, x), m(m(c(x, z), y), m(z, x))) = m(m(m(z, x), m(c(x, z), y)), m(z, x))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[266, 15])).
% 130.57/130.90 tff(268,plain,
% 130.57/130.90 (m(m(z, x), m(m(c(x, z), y), m(z, x))) = m(m(x, m(z, y)), m(z, x))),
% 130.57/130.90 inference(transitivity,[status(thm)],[267, 265])).
% 130.57/130.90 tff(269,plain,
% 130.57/130.90 (m(m(m(z, x), m(m(c(x, z), y), m(z, x))), c(x, z)) = m(m(m(x, m(z, y)), m(z, x)), c(x, z))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[268])).
% 130.57/130.90 tff(270,plain,
% 130.57/130.90 (m(m(m(x, m(z, y)), m(z, x)), c(x, z)) = m(m(m(z, x), m(m(c(x, z), y), m(z, x))), c(x, z))),
% 130.57/130.90 inference(symmetry,[status(thm)],[269])).
% 130.57/130.90 tff(271,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, m(z, y)), m(m(z, x), c(x, z))) = m(m(m(x, m(z, y)), m(z, x)), c(x, z)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(272,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(m(z, x), c(x, z))) = m(m(m(x, m(z, y)), m(z, x)), c(x, z))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[271, 15])).
% 130.57/130.90 tff(273,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(m(z, x), c(x, z))) = m(m(x, m(z, y)), m(x, z))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[67])).
% 130.57/130.90 tff(274,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(x, z)) = m(m(x, m(z, y)), m(m(z, x), c(x, z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[273])).
% 130.57/130.90 tff(275,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(x, z)) = m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z))))),
% 130.57/130.90 inference(transitivity,[status(thm)],[274, 272, 270, 260, 257])).
% 130.57/130.90 tff(276,plain,
% 130.57/130.90 (m(c(x, z), m(m(x, m(z, y)), m(x, z))) = m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z)))))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[275])).
% 130.57/130.90 tff(277,plain,
% 130.57/130.90 (m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z))))) = m(c(x, z), m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[276])).
% 130.57/130.90 tff(278,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z))))) = m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(279,plain,
% 130.57/130.90 (m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z))))) = m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x)))))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[278, 48])).
% 130.57/130.90 tff(280,plain,
% 130.57/130.90 (m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))) = m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z)))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[279])).
% 130.57/130.90 tff(281,plain,
% 130.57/130.90 (m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))) = m(c(x, z), m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.90 inference(transitivity,[status(thm)],[280, 277])).
% 130.57/130.90 tff(282,plain,
% 130.57/130.90 (m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x)))))) = m(x, m(c(x, z), m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[281])).
% 130.57/130.90 tff(283,plain,
% 130.57/130.90 (m(x, m(c(x, z), m(m(x, m(z, y)), m(x, z)))) = m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[282])).
% 130.57/130.90 tff(284,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(c(x, z), m(m(x, m(z, y)), m(x, z)))) = m(m(x, c(x, z)), m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(285,plain,
% 130.57/130.90 (m(x, m(c(x, z), m(m(x, m(z, y)), m(x, z)))) = m(m(x, c(x, z)), m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[284, 15])).
% 130.57/130.90 tff(286,plain,
% 130.57/130.90 (m(m(x, c(x, z)), m(m(x, m(z, y)), m(x, z))) = m(x, m(c(x, z), m(m(x, m(z, y)), m(x, z))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[285])).
% 130.57/130.90 tff(287,plain,
% 130.57/130.90 (m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z)))) = m(m(m(x, c(x, z)), y), m(x, z))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[63])).
% 130.57/130.90 tff(288,plain,
% 130.57/130.90 (m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z))))) = m(z, m(m(m(x, c(x, z)), y), m(x, z)))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[287])).
% 130.57/130.90 tff(289,plain,
% 130.57/130.90 (m(z, m(m(m(x, c(x, z)), y), m(x, z))) = m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z)))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[288])).
% 130.57/130.90 tff(290,plain,
% 130.57/130.90 (m(m(z, m(m(x, c(x, z)), y)), m(x, z)) = m(z, m(m(m(x, c(x, z)), y), m(x, z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[86])).
% 130.57/130.90 tff(291,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(x, z)) = m(m(z, m(m(x, c(x, z)), y)), m(x, z))),
% 130.57/130.90 inference(symmetry,[status(thm)],[84])).
% 130.57/130.90 tff(292,plain,
% 130.57/130.90 (m(m(x, m(z, y)), m(x, z)) = m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z)))))),
% 130.57/130.90 inference(transitivity,[status(thm)],[291, 290, 289])).
% 130.57/130.90 tff(293,plain,
% 130.57/130.90 (m(m(x, c(x, z)), m(m(x, m(z, y)), m(x, z))) = m(m(x, c(x, z)), m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z))))))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[292])).
% 130.57/130.90 tff(294,plain,
% 130.57/130.90 (m(m(x, c(x, z)), m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z)))))) = m(m(x, c(x, z)), m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[293])).
% 130.57/130.90 tff(295,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(m(x, c(x, z)), m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z)))))) = m(z, m(m(x, c(x, z)), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(296,plain,
% 130.57/130.90 (m(m(x, c(x, z)), m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z)))))) = m(z, m(m(x, c(x, z)), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[295, 48])).
% 130.57/130.90 tff(297,plain,
% 130.57/130.90 (m(z, m(m(x, c(x, z)), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))) = m(m(x, c(x, z)), m(z, m(m(m(x, c(x, z)), y), m(z, m(x, c(x, z))))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[296])).
% 130.57/130.90 tff(298,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(m(x, c(x, z)), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))) = m(m(z, m(x, c(x, z))), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(299,plain,
% 130.57/130.90 (m(z, m(m(x, c(x, z)), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))) = m(m(z, m(x, c(x, z))), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[298, 15])).
% 130.57/130.90 tff(300,plain,
% 130.57/130.90 (m(m(z, m(x, c(x, z))), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(z, m(m(x, c(x, z)), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[299])).
% 130.57/130.90 tff(301,plain,
% 130.57/130.90 (m(x, z) = m(z, m(x, c(x, z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[63])).
% 130.57/130.90 tff(302,plain,
% 130.57/130.90 (m(m(x, z), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(m(z, m(x, c(x, z))), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[301])).
% 130.57/130.90 tff(303,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(m(m(x, z), m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(304,plain,
% 130.57/130.90 (m(m(x, z), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z))) = m(m(m(x, z), m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[303, 15])).
% 130.57/130.90 tff(305,plain,
% 130.57/130.90 (m(m(m(x, z), m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z)) = m(m(x, z), m(m(m(x, c(x, z)), y), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[304])).
% 130.57/130.90 tff(306,plain,
% 130.57/130.90 (m(x, m(x, m(z, y))) = m(x, m(z, m(m(x, c(x, z)), y)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[101])).
% 130.57/130.90 tff(307,plain,
% 130.57/130.90 (m(m(x, x), m(z, y)) = m(x, m(x, m(z, y)))),
% 130.57/130.90 inference(symmetry,[status(thm)],[100])).
% 130.57/130.90 tff(308,plain,
% 130.57/130.90 (m(m(x, x), m(z, y)) = m(m(x, z), m(m(x, c(x, z)), y))),
% 130.57/130.90 inference(transitivity,[status(thm)],[307, 306, 103])).
% 130.57/130.90 tff(309,plain,
% 130.57/130.90 (m(m(m(x, x), m(z, y)), m(m(x, c(x, z)), z)) = m(m(m(x, z), m(m(x, c(x, z)), y)), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[308])).
% 130.57/130.90 tff(310,plain,
% 130.57/130.90 (m(m(x, m(x, m(z, y))), m(m(x, c(x, z)), z)) = m(m(m(x, x), m(z, y)), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[100])).
% 130.57/130.90 tff(311,plain,
% 130.57/130.90 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z))) = m(m(x, m(x, m(z, y))), m(m(x, c(x, z)), z)))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(312,plain,
% 130.57/130.90 (m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z))) = m(m(x, m(x, m(z, y))), m(m(x, c(x, z)), z))),
% 130.57/130.90 inference(unit_resolution,[status(thm)],[311, 15])).
% 130.57/130.90 tff(313,plain,
% 130.57/130.90 (m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z))) = m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))),
% 130.57/130.90 inference(transitivity,[status(thm)],[312, 310, 309, 305, 302, 300, 297, 294, 286, 283])).
% 130.57/130.90 tff(314,plain,
% 130.57/130.90 (inj_1(x, m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z)))) = inj_1(x, m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x)))))))),
% 130.57/130.90 inference(monotonicity,[status(thm)],[313])).
% 130.57/130.90 tff(315,plain,
% 130.57/130.90 (inj_1(x, m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))) = inj_1(x, m(x, m(m(x, m(z, y)), m(m(x, c(x, z)), z))))),
% 130.57/130.90 inference(symmetry,[status(thm)],[314])).
% 130.57/130.90 tff(316,plain,
% 130.57/130.90 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(x, m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))) = m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))),
% 130.57/130.90 inference(quant_inst,[status(thm)],[])).
% 130.57/130.90 tff(317,plain,
% 130.57/130.90 (inj_1(x, m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))))) = m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x)))))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[316, 6])).
% 130.57/130.91 tff(318,plain,
% 130.57/130.91 (m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x))))) = inj_1(x, m(x, m(m(z, x), m(c(x, z), m(m(c(x, z), y), m(c(x, z), m(z, x)))))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[317])).
% 130.57/130.91 tff(319,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(m(z, y), m(x, z))) = m(m(x, m(z, y)), m(x, z)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(320,plain,
% 130.57/130.91 (m(x, m(m(z, y), m(x, z))) = m(m(x, m(z, y)), m(x, z))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[319, 15])).
% 130.57/130.91 tff(321,plain,
% 130.57/130.91 (m(x, m(m(z, y), m(x, z))) = m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z))))),
% 130.57/130.91 inference(transitivity,[status(thm)],[320, 274, 272, 270, 260, 257])).
% 130.57/130.91 tff(322,plain,
% 130.57/130.91 (m(c(x, z), m(x, m(m(z, y), m(x, z)))) = m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(m(z, x), c(x, z)))))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[321])).
% 130.57/130.91 tff(323,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(x, m(m(z, y), m(x, z)))) = m(m(c(x, z), x), m(m(z, y), m(x, z))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(324,plain,
% 130.57/130.91 (m(c(x, z), m(x, m(m(z, y), m(x, z)))) = m(m(c(x, z), x), m(m(z, y), m(x, z)))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[323, 15])).
% 130.57/130.91 tff(325,plain,
% 130.57/130.91 (m(m(c(x, z), x), m(m(z, y), m(x, z))) = m(c(x, z), m(x, m(m(z, y), m(x, z))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[324])).
% 130.57/130.91 tff(326,plain,
% 130.57/130.91 (m(m(c(x, z), x), m(m(z, y), m(x, z))) = m(m(x, c(x, z)), m(m(z, y), m(x, z)))),
% 130.57/130.91 inference(transitivity,[status(thm)],[325, 322, 279, 318, 315, 253, 251, 249, 246, 242, 239])).
% 130.57/130.91 tff(327,plain,
% 130.57/130.91 (inj_0(m(m(z, y), m(x, z)), m(m(c(x, z), x), m(m(z, y), m(x, z)))) = inj_0(m(m(z, y), m(x, z)), m(m(x, c(x, z)), m(m(z, y), m(x, z))))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[326])).
% 130.57/130.91 tff(328,plain,
% 130.57/130.91 (inj_0(m(m(z, y), m(x, z)), m(m(x, c(x, z)), m(m(z, y), m(x, z)))) = inj_0(m(m(z, y), m(x, z)), m(m(c(x, z), x), m(m(z, y), m(x, z))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[327])).
% 130.57/130.91 tff(329,plain,
% 130.57/130.91 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(m(z, y), m(x, z)), m(m(x, c(x, z)), m(m(z, y), m(x, z)))) = m(x, c(x, z)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(330,plain,
% 130.57/130.91 (inj_0(m(m(z, y), m(x, z)), m(m(x, c(x, z)), m(m(z, y), m(x, z)))) = m(x, c(x, z))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[329, 28])).
% 130.57/130.91 tff(331,plain,
% 130.57/130.91 (m(x, c(x, z)) = inj_0(m(m(z, y), m(x, z)), m(m(x, c(x, z)), m(m(z, y), m(x, z))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[330])).
% 130.57/130.91 tff(332,plain,
% 130.57/130.91 (m(x, c(x, z)) = m(c(x, z), x)),
% 130.57/130.91 inference(transitivity,[status(thm)],[331, 328, 231])).
% 130.57/130.91 tff(333,plain,
% 130.57/130.91 (m(m(x, c(x, z)), m(z, y)) = m(m(c(x, z), x), m(z, y))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[332])).
% 130.57/130.91 tff(334,plain,
% 130.57/130.91 (m(m(c(x, z), x), m(z, y)) = m(m(x, c(x, z)), m(z, y))),
% 130.57/130.91 inference(symmetry,[status(thm)],[333])).
% 130.57/130.91 tff(335,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(x, m(z, y))) = m(m(c(x, z), x), m(z, y)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(336,plain,
% 130.57/130.91 (m(c(x, z), m(x, m(z, y))) = m(m(c(x, z), x), m(z, y))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[335, 15])).
% 130.57/130.91 tff(337,plain,
% 130.57/130.91 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(z, x), m(m(c(x, z), m(x, m(z, y))), m(z, x))) = m(c(x, z), m(x, m(z, y))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(338,plain,
% 130.57/130.91 (inj_0(m(z, x), m(m(c(x, z), m(x, m(z, y))), m(z, x))) = m(c(x, z), m(x, m(z, y)))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[337, 28])).
% 130.57/130.91 tff(339,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, m(z, y)), m(c(x, z), m(z, x))) = m(m(m(x, m(z, y)), c(x, z)), m(z, x)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(340,plain,
% 130.57/130.91 (m(m(x, m(z, y)), m(c(x, z), m(z, x))) = m(m(m(x, m(z, y)), c(x, z)), m(z, x))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[339, 15])).
% 130.57/130.91 tff(341,plain,
% 130.57/130.91 (m(m(m(z, x), c(x, z)), y) = m(m(z, x), m(c(x, z), y))),
% 130.57/130.91 inference(symmetry,[status(thm)],[263])).
% 130.57/130.91 tff(342,plain,
% 130.57/130.91 (m(m(x, z), y) = m(m(m(z, x), c(x, z)), y)),
% 130.57/130.91 inference(symmetry,[status(thm)],[261])).
% 130.57/130.91 tff(343,plain,
% 130.57/130.91 (m(x, m(z, y)) = m(m(z, x), m(c(x, z), y))),
% 130.57/130.91 inference(transitivity,[status(thm)],[78, 342, 341])).
% 130.57/130.91 tff(344,plain,
% 130.57/130.91 (m(m(x, m(z, y)), m(c(x, z), m(z, x))) = m(m(m(z, x), m(c(x, z), y)), m(c(x, z), m(z, x)))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[343])).
% 130.57/130.91 tff(345,plain,
% 130.57/130.91 (m(m(m(z, x), m(c(x, z), y)), m(c(x, z), m(z, x))) = m(m(x, m(z, y)), m(c(x, z), m(z, x)))),
% 130.57/130.91 inference(symmetry,[status(thm)],[344])).
% 130.57/130.91 tff(346,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(c(x, z), y), m(c(x, z), m(z, x)))) = m(m(m(z, x), m(c(x, z), y)), m(c(x, z), m(z, x))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(347,plain,
% 130.57/130.91 (m(m(z, x), m(m(c(x, z), y), m(c(x, z), m(z, x)))) = m(m(m(z, x), m(c(x, z), y)), m(c(x, z), m(z, x)))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[346, 15])).
% 130.57/130.91 tff(348,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(y, m(c(x, z), m(z, x)))) = m(m(c(x, z), y), m(c(x, z), m(z, x))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(349,plain,
% 130.57/130.91 (m(c(x, z), m(y, m(c(x, z), m(z, x)))) = m(m(c(x, z), y), m(c(x, z), m(z, x)))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[348, 15])).
% 130.57/130.91 tff(350,plain,
% 130.57/130.91 (m(m(c(x, z), y), m(c(x, z), m(z, x))) = m(c(x, z), m(y, m(c(x, z), m(z, x))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[349])).
% 130.57/130.91 tff(351,plain,
% 130.57/130.91 (m(m(z, x), m(m(c(x, z), y), m(c(x, z), m(z, x)))) = m(m(z, x), m(c(x, z), m(y, m(c(x, z), m(z, x)))))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[350])).
% 130.57/130.91 tff(352,plain,
% 130.57/130.91 (m(m(z, x), m(c(x, z), m(y, m(c(x, z), m(z, x))))) = m(m(z, x), m(m(c(x, z), y), m(c(x, z), m(z, x))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[351])).
% 130.57/130.91 tff(353,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, m(Z, m(Y, X)))) = m(Y, m(X, m(Z, m(X, Y)))))) | (m(c(x, z), m(m(z, x), m(y, m(m(z, x), c(x, z))))) = m(m(z, x), m(c(x, z), m(y, m(c(x, z), m(z, x))))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(354,plain,
% 130.57/130.91 (m(c(x, z), m(m(z, x), m(y, m(m(z, x), c(x, z))))) = m(m(z, x), m(c(x, z), m(y, m(c(x, z), m(z, x)))))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[353, 48])).
% 130.57/130.91 tff(355,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(x, m(y, m(x, z)))) = m(m(z, x), m(y, m(x, z))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(356,plain,
% 130.57/130.91 (m(z, m(x, m(y, m(x, z)))) = m(m(z, x), m(y, m(x, z)))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[355, 15])).
% 130.57/130.91 tff(357,plain,
% 130.57/130.91 (m(m(z, x), m(y, m(x, z))) = m(z, m(x, m(y, m(x, z))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[356])).
% 130.57/130.91 tff(358,plain,
% 130.57/130.91 (m(y, m(m(z, x), c(x, z))) = m(y, m(x, z))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[67])).
% 130.57/130.91 tff(359,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(y, m(m(z, x), c(x, z))) = m(m(y, m(z, x)), c(x, z)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(360,plain,
% 130.57/130.91 (m(y, m(m(z, x), c(x, z))) = m(m(y, m(z, x)), c(x, z))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[359, 15])).
% 130.57/130.91 tff(361,plain,
% 130.57/130.91 (m(m(y, m(z, x)), c(x, z)) = m(y, m(m(z, x), c(x, z)))),
% 130.57/130.91 inference(symmetry,[status(thm)],[360])).
% 130.57/130.91 tff(362,plain,
% 130.57/130.91 (m(m(y, m(z, x)), c(x, z)) = m(y, m(x, z))),
% 130.57/130.91 inference(transitivity,[status(thm)],[361, 358])).
% 130.57/130.91 tff(363,plain,
% 130.57/130.91 (m(m(z, x), m(m(y, m(z, x)), c(x, z))) = m(m(z, x), m(y, m(x, z)))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[362])).
% 130.57/130.91 tff(364,plain,
% 130.57/130.91 (m(m(z, x), m(y, m(m(z, x), c(x, z)))) = m(m(z, x), m(m(y, m(z, x)), c(x, z)))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[360])).
% 130.57/130.91 tff(365,plain,
% 130.57/130.91 (m(m(z, x), m(y, m(m(z, x), c(x, z)))) = m(m(x, m(z, y)), m(z, x))),
% 130.57/130.91 inference(transitivity,[status(thm)],[364, 363, 357, 136, 133, 131, 129])).
% 130.57/130.91 tff(366,plain,
% 130.57/130.91 (m(c(x, z), m(m(z, x), m(y, m(m(z, x), c(x, z))))) = m(c(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[365])).
% 130.57/130.91 tff(367,plain,
% 130.57/130.91 (m(c(x, z), m(m(x, m(z, y)), m(z, x))) = m(c(x, z), m(m(z, x), m(y, m(m(z, x), c(x, z)))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[366])).
% 130.57/130.91 tff(368,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(m(x, m(z, y)), m(z, x))) = m(m(c(x, z), m(x, m(z, y))), m(z, x)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(369,plain,
% 130.57/130.91 (m(c(x, z), m(m(x, m(z, y)), m(z, x))) = m(m(c(x, z), m(x, m(z, y))), m(z, x))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[368, 15])).
% 130.57/130.91 tff(370,plain,
% 130.57/130.91 (m(m(c(x, z), m(x, m(z, y))), m(z, x)) = m(c(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.57/130.91 inference(symmetry,[status(thm)],[369])).
% 130.57/130.91 tff(371,plain,
% 130.57/130.91 (m(m(c(x, z), m(x, m(z, y))), m(z, x)) = m(m(m(x, m(z, y)), c(x, z)), m(z, x))),
% 130.57/130.91 inference(transitivity,[status(thm)],[370, 367, 354, 352, 347, 345, 340])).
% 130.57/130.91 tff(372,plain,
% 130.57/130.91 (inj_0(m(z, x), m(m(c(x, z), m(x, m(z, y))), m(z, x))) = inj_0(m(z, x), m(m(m(x, m(z, y)), c(x, z)), m(z, x)))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[371])).
% 130.57/130.91 tff(373,plain,
% 130.57/130.91 (inj_0(m(z, x), m(m(m(x, m(z, y)), c(x, z)), m(z, x))) = inj_0(m(z, x), m(m(c(x, z), m(x, m(z, y))), m(z, x)))),
% 130.57/130.91 inference(symmetry,[status(thm)],[372])).
% 130.57/130.91 tff(374,plain,
% 130.57/130.91 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(z, x), m(m(m(x, m(z, y)), c(x, z)), m(z, x))) = m(m(x, m(z, y)), c(x, z)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(375,plain,
% 130.57/130.91 (inj_0(m(z, x), m(m(m(x, m(z, y)), c(x, z)), m(z, x))) = m(m(x, m(z, y)), c(x, z))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[374, 28])).
% 130.57/130.91 tff(376,plain,
% 130.57/130.91 (m(m(x, m(z, y)), c(x, z)) = inj_0(m(z, x), m(m(m(x, m(z, y)), c(x, z)), m(z, x)))),
% 130.57/130.91 inference(symmetry,[status(thm)],[375])).
% 130.57/130.91 tff(377,plain,
% 130.57/130.91 (m(m(x, m(z, y)), c(x, z)) = m(m(x, c(x, z)), m(z, y))),
% 130.57/130.91 inference(transitivity,[status(thm)],[376, 373, 338, 336, 334])).
% 130.57/130.91 tff(378,plain,
% 130.57/130.91 (m(m(m(x, m(z, y)), c(x, z)), c(y, z)) = m(m(m(x, c(x, z)), m(z, y)), c(y, z))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[377])).
% 130.57/130.91 tff(379,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, m(z, y)), m(c(x, z), c(y, z))) = m(m(m(x, m(z, y)), c(x, z)), c(y, z)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(380,plain,
% 130.57/130.91 (m(m(x, m(z, y)), m(c(x, z), c(y, z))) = m(m(m(x, m(z, y)), c(x, z)), c(y, z))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[379, 15])).
% 130.57/130.91 tff(381,plain,
% 130.57/130.91 (m(m(x, m(z, y)), m(c(x, z), c(y, z))) = m(m(m(x, c(x, z)), y), z)),
% 130.57/130.91 inference(transitivity,[status(thm)],[380, 378, 229, 226, 225])).
% 130.57/130.91 tff(382,plain,
% 130.57/130.91 (m(m(m(x, z), z), m(m(x, m(z, y)), m(c(x, z), c(y, z)))) = m(m(m(x, z), z), m(m(m(x, c(x, z)), y), z))),
% 130.57/130.91 inference(monotonicity,[status(thm)],[381])).
% 130.57/130.91 tff(383,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, z), z), m(m(x, m(z, y)), m(c(x, z), c(y, z)))) = m(m(m(m(x, z), z), m(x, m(z, y))), m(c(x, z), c(y, z))))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(384,plain,
% 130.57/130.91 (m(m(m(x, z), z), m(m(x, m(z, y)), m(c(x, z), c(y, z)))) = m(m(m(m(x, z), z), m(x, m(z, y))), m(c(x, z), c(y, z)))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[383, 15])).
% 130.57/130.91 tff(385,plain,
% 130.57/130.91 (m(m(m(m(x, z), z), m(x, m(z, y))), m(c(x, z), c(y, z))) = m(m(m(x, z), z), m(m(x, m(z, y)), m(c(x, z), c(y, z))))),
% 130.57/130.91 inference(symmetry,[status(thm)],[384])).
% 130.57/130.91 tff(386,plain,
% 130.57/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, z), z), m(x, m(z, y))) = m(m(m(m(x, z), z), x), m(z, y)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.57/130.91 tff(387,plain,
% 130.57/130.91 (m(m(m(x, z), z), m(x, m(z, y))) = m(m(m(m(x, z), z), x), m(z, y))),
% 130.57/130.91 inference(unit_resolution,[status(thm)],[386, 15])).
% 130.57/130.91 tff(388,plain,
% 130.57/130.91 (m(m(m(m(x, z), z), x), m(z, y)) = m(m(m(x, z), z), m(x, m(z, y)))),
% 130.57/130.91 inference(symmetry,[status(thm)],[387])).
% 130.57/130.91 tff(389,plain,
% 130.57/130.91 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(y, m(x, z)), m(m(m(z, x), m(x, z)), m(y, m(x, z)))) = m(m(z, x), m(x, z)))),
% 130.57/130.91 inference(quant_inst,[status(thm)],[])).
% 130.67/130.91 tff(390,plain,
% 130.67/130.91 (inj_0(m(y, m(x, z)), m(m(m(z, x), m(x, z)), m(y, m(x, z)))) = m(m(z, x), m(x, z))),
% 130.67/130.91 inference(unit_resolution,[status(thm)],[389, 28])).
% 130.67/130.91 tff(391,plain,
% 130.67/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(m(x, z), m(y, m(x, z)))) = m(m(m(z, x), m(x, z)), m(y, m(x, z))))),
% 130.67/130.91 inference(quant_inst,[status(thm)],[])).
% 130.67/130.91 tff(392,plain,
% 130.67/130.91 (m(m(z, x), m(m(x, z), m(y, m(x, z)))) = m(m(m(z, x), m(x, z)), m(y, m(x, z)))),
% 130.67/130.91 inference(unit_resolution,[status(thm)],[391, 15])).
% 130.67/130.91 tff(393,plain,
% 130.67/130.91 (m(m(m(x, z), y), m(x, z)) = m(m(x, m(z, y)), m(x, z))),
% 130.67/130.91 inference(monotonicity,[status(thm)],[79])).
% 130.67/130.91 tff(394,plain,
% 130.67/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(y, m(x, z))) = m(m(m(x, z), y), m(x, z)))),
% 130.67/130.91 inference(quant_inst,[status(thm)],[])).
% 130.67/130.91 tff(395,plain,
% 130.67/130.91 (m(m(x, z), m(y, m(x, z))) = m(m(m(x, z), y), m(x, z))),
% 130.67/130.91 inference(unit_resolution,[status(thm)],[394, 15])).
% 130.67/130.91 tff(396,plain,
% 130.67/130.91 (m(m(x, z), m(y, m(x, z))) = m(m(x, m(z, y)), m(x, z))),
% 130.67/130.91 inference(transitivity,[status(thm)],[395, 393])).
% 130.67/130.91 tff(397,plain,
% 130.67/130.91 (m(m(z, x), m(m(x, z), m(y, m(x, z)))) = m(m(z, x), m(m(x, m(z, y)), m(x, z)))),
% 130.67/130.91 inference(monotonicity,[status(thm)],[396])).
% 130.67/130.91 tff(398,plain,
% 130.67/130.91 (m(m(z, x), m(m(x, m(z, y)), m(x, z))) = m(m(z, x), m(m(x, z), m(y, m(x, z))))),
% 130.67/130.91 inference(symmetry,[status(thm)],[397])).
% 130.67/130.91 tff(399,plain,
% 130.67/130.91 (m(z, m(x, m(y, m(x, z)))) = m(m(x, m(z, y)), m(z, x))),
% 130.67/130.91 inference(transitivity,[status(thm)],[136, 133, 131, 129])).
% 130.67/130.91 tff(400,plain,
% 130.67/130.91 (m(m(x, z), m(z, m(x, m(y, m(x, z))))) = m(m(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.67/130.91 inference(monotonicity,[status(thm)],[399])).
% 130.67/130.91 tff(401,plain,
% 130.67/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(z, m(x, m(y, m(x, z))))) = m(m(m(x, z), z), m(x, m(y, m(x, z)))))),
% 130.67/130.91 inference(quant_inst,[status(thm)],[])).
% 130.67/130.91 tff(402,plain,
% 130.67/130.91 (m(m(x, z), m(z, m(x, m(y, m(x, z))))) = m(m(m(x, z), z), m(x, m(y, m(x, z))))),
% 130.67/130.91 inference(unit_resolution,[status(thm)],[401, 15])).
% 130.67/130.91 tff(403,plain,
% 130.67/130.91 (m(m(m(x, z), z), m(x, m(y, m(x, z)))) = m(m(x, z), m(z, m(x, m(y, m(x, z)))))),
% 130.67/130.91 inference(symmetry,[status(thm)],[402])).
% 130.67/130.91 tff(404,plain,
% 130.67/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, z), z), m(x, m(y, m(x, z)))) = m(m(m(m(x, z), z), x), m(y, m(x, z))))),
% 130.67/130.91 inference(quant_inst,[status(thm)],[])).
% 130.67/130.91 tff(405,plain,
% 130.67/130.91 (m(m(m(x, z), z), m(x, m(y, m(x, z)))) = m(m(m(m(x, z), z), x), m(y, m(x, z)))),
% 130.67/130.91 inference(unit_resolution,[status(thm)],[404, 15])).
% 130.67/130.91 tff(406,plain,
% 130.67/130.91 (m(m(m(m(x, z), z), x), m(y, m(x, z))) = m(m(m(x, z), z), m(x, m(y, m(x, z))))),
% 130.67/130.91 inference(symmetry,[status(thm)],[405])).
% 130.67/130.91 tff(407,plain,
% 130.67/130.91 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(z, x)) = m(m(m(x, z), z), x))),
% 130.67/130.91 inference(quant_inst,[status(thm)],[])).
% 130.67/130.91 tff(408,plain,
% 130.67/130.91 (m(m(x, z), m(z, x)) = m(m(m(x, z), z), x)),
% 130.67/130.91 inference(unit_resolution,[status(thm)],[407, 15])).
% 130.67/130.91 tff(409,plain,
% 130.67/130.91 (m(m(m(x, z), m(z, x)), m(m(y, m(z, x)), c(x, z))) = m(m(m(m(x, z), z), x), m(y, m(x, z)))),
% 130.67/130.91 inference(monotonicity,[status(thm)],[408, 362])).
% 130.67/130.91 tff(410,plain,
% 130.67/130.91 (m(y, m(x, z)) = m(y, m(m(z, x), c(x, z)))),
% 130.67/130.91 inference(symmetry,[status(thm)],[358])).
% 130.67/130.91 tff(411,plain,
% 130.67/130.91 (m(y, m(x, z)) = m(m(y, m(z, x)), c(x, z))),
% 130.67/130.91 inference(transitivity,[status(thm)],[410, 360])).
% 130.67/130.91 tff(412,plain,
% 130.67/130.91 (m(m(m(x, z), m(z, x)), m(y, m(x, z))) = m(m(m(x, z), m(z, x)), m(m(y, m(z, x)), c(x, z)))),
% 130.67/130.91 inference(monotonicity,[status(thm)],[411])).
% 130.67/130.91 tff(413,plain,
% 130.67/130.91 (m(m(m(x, z), m(z, x)), m(y, m(x, z))) = m(m(m(z, x), m(x, z)), m(y, m(x, z)))),
% 130.67/130.91 inference(transitivity,[status(thm)],[412, 409, 406, 403, 400, 54, 51, 41, 398, 392])).
% 130.67/130.91 tff(414,plain,
% 130.67/130.91 (inj_0(m(y, m(x, z)), m(m(m(x, z), m(z, x)), m(y, m(x, z)))) = inj_0(m(y, m(x, z)), m(m(m(z, x), m(x, z)), m(y, m(x, z))))),
% 130.67/130.91 inference(monotonicity,[status(thm)],[413])).
% 130.67/130.91 tff(415,plain,
% 130.67/130.91 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(y, m(x, z)), m(m(m(x, z), m(z, x)), m(y, m(x, z)))) = m(m(x, z), m(z, x)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(416,plain,
% 130.67/130.92 (inj_0(m(y, m(x, z)), m(m(m(x, z), m(z, x)), m(y, m(x, z)))) = m(m(x, z), m(z, x))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[415, 28])).
% 130.67/130.92 tff(417,plain,
% 130.67/130.92 (m(m(x, z), m(z, x)) = inj_0(m(y, m(x, z)), m(m(m(x, z), m(z, x)), m(y, m(x, z))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[416])).
% 130.67/130.92 tff(418,plain,
% 130.67/130.92 (m(m(m(x, z), z), x) = m(m(x, z), m(z, x))),
% 130.67/130.92 inference(symmetry,[status(thm)],[408])).
% 130.67/130.92 tff(419,plain,
% 130.67/130.92 (m(m(m(x, z), z), x) = m(m(z, x), m(x, z))),
% 130.67/130.92 inference(transitivity,[status(thm)],[418, 417, 414, 390])).
% 130.67/130.92 tff(420,plain,
% 130.67/130.92 (m(m(m(m(x, z), z), x), m(z, y)) = m(m(m(z, x), m(x, z)), m(z, y))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[419])).
% 130.67/130.92 tff(421,plain,
% 130.67/130.92 (m(m(m(z, x), m(x, z)), m(z, y)) = m(m(m(m(x, z), z), x), m(z, y))),
% 130.67/130.92 inference(symmetry,[status(thm)],[420])).
% 130.67/130.92 tff(422,plain,
% 130.67/130.92 (m(m(m(z, x), m(x, z)), m(z, y)) = m(m(m(x, z), z), m(x, m(z, y)))),
% 130.67/130.92 inference(transitivity,[status(thm)],[421, 388])).
% 130.67/130.92 tff(423,plain,
% 130.67/130.92 (m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(x, z), c(y, z))) = m(m(m(m(x, z), z), m(x, m(z, y))), m(c(x, z), c(y, z)))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[422])).
% 130.67/130.92 tff(424,plain,
% 130.67/130.92 (m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(x, z), c(y, z))) = m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z)))),
% 130.67/130.92 inference(transitivity,[status(thm)],[423, 385, 382, 223, 220, 218, 216, 213, 22, 20])).
% 130.67/130.92 tff(425,plain,
% 130.67/130.92 (inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(x, z), c(y, z)))) = inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z))))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[424])).
% 130.67/130.92 tff(426,plain,
% 130.67/130.92 (inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z)))) = inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(x, z), c(y, z))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[425])).
% 130.67/130.92 tff(427,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z)))) = m(c(y, z), c(x, z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(428,plain,
% 130.67/130.92 (inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z)))) = m(c(y, z), c(x, z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[427, 6])).
% 130.67/130.92 tff(429,plain,
% 130.67/130.92 (m(c(y, z), c(x, z)) = inj_1(m(m(m(z, x), m(x, z)), m(z, y)), m(m(m(m(z, x), m(x, z)), m(z, y)), m(c(y, z), c(x, z))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[428])).
% 130.67/130.92 tff(430,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(y, m(y, m(c(y, z), c(x, z)))) = m(c(y, z), c(x, z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(431,plain,
% 130.67/130.92 (inj_1(y, m(y, m(c(y, z), c(x, z)))) = m(c(y, z), c(x, z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[430, 6])).
% 130.67/130.92 tff(432,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(x, z), m(m(x, z), m(y, c(m(x, y), z)))) = m(y, c(m(x, y), z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(433,plain,
% 130.67/130.92 (inj_1(m(x, z), m(m(x, z), m(y, c(m(x, y), z)))) = m(y, c(m(x, y), z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[432, 6])).
% 130.67/130.92 tff(434,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(y, c(y, z))) = m(m(c(x, z), y), c(y, z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(435,plain,
% 130.67/130.92 (m(c(x, z), m(y, c(y, z))) = m(m(c(x, z), y), c(y, z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[434, 15])).
% 130.67/130.92 tff(436,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(c(x, z), m(y, c(y, z))))) = m(c(x, z), m(y, c(y, z))))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(437,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(c(x, z), m(y, c(y, z))))) = m(c(x, z), m(y, c(y, z)))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[436, 6])).
% 130.67/130.92 tff(438,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(z, m(x, m(y, c(m(x, y), z)))) = m(m(z, x), m(y, c(m(x, y), z))))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(439,plain,
% 130.67/130.92 (m(z, m(x, m(y, c(m(x, y), z)))) = m(m(z, x), m(y, c(m(x, y), z)))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[438, 15])).
% 130.67/130.92 tff(440,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(y, c(m(x, y), z))) = m(m(x, y), c(m(x, y), z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(441,plain,
% 130.67/130.92 (m(x, m(y, c(m(x, y), z))) = m(m(x, y), c(m(x, y), z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[440, 15])).
% 130.67/130.92 tff(442,plain,
% 130.67/130.92 (m(z, m(x, m(y, c(m(x, y), z)))) = m(z, m(m(x, y), c(m(x, y), z)))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[441])).
% 130.67/130.92 tff(443,plain,
% 130.67/130.92 (m(z, m(m(x, y), c(m(x, y), z))) = m(z, m(x, m(y, c(m(x, y), z))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[442])).
% 130.67/130.92 tff(444,plain,
% 130.67/130.92 ((~![Y: $i, X: $i] : (m(Y, m(X, c(X, Y))) = m(X, Y))) | (m(z, m(m(x, y), c(m(x, y), z))) = m(m(x, y), z))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(445,plain,
% 130.67/130.92 (m(z, m(m(x, y), c(m(x, y), z))) = m(m(x, y), z)),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[444, 61])).
% 130.67/130.92 tff(446,plain,
% 130.67/130.92 (m(m(x, y), z) = m(z, m(m(x, y), c(m(x, y), z)))),
% 130.67/130.92 inference(symmetry,[status(thm)],[445])).
% 130.67/130.92 tff(447,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(y, z)) = m(m(x, y), z))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(448,plain,
% 130.67/130.92 (m(x, m(y, z)) = m(m(x, y), z)),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[447, 15])).
% 130.67/130.92 tff(449,plain,
% 130.67/130.92 (m(x, m(z, m(y, c(y, z)))) = m(x, m(y, z))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[198])).
% 130.67/130.92 tff(450,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(z, m(y, c(y, z)))) = m(m(x, z), m(y, c(y, z))))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(451,plain,
% 130.67/130.92 (m(x, m(z, m(y, c(y, z)))) = m(m(x, z), m(y, c(y, z)))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[450, 15])).
% 130.67/130.92 tff(452,plain,
% 130.67/130.92 (m(m(x, z), m(y, c(y, z))) = m(x, m(z, m(y, c(y, z))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[451])).
% 130.67/130.92 tff(453,plain,
% 130.67/130.92 (m(m(m(z, x), c(x, z)), m(y, c(y, z))) = m(m(x, z), m(y, c(y, z)))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[67])).
% 130.67/130.92 tff(454,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(z, x), m(c(x, z), m(y, c(y, z)))) = m(m(m(z, x), c(x, z)), m(y, c(y, z))))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(455,plain,
% 130.67/130.92 (m(m(z, x), m(c(x, z), m(y, c(y, z)))) = m(m(m(z, x), c(x, z)), m(y, c(y, z)))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[454, 15])).
% 130.67/130.92 tff(456,plain,
% 130.67/130.92 (m(m(z, x), m(c(x, z), m(y, c(y, z)))) = m(m(z, x), m(y, c(m(x, y), z)))),
% 130.67/130.92 inference(transitivity,[status(thm)],[455, 453, 452, 449, 448, 446, 443, 439])).
% 130.67/130.92 tff(457,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(c(x, z), m(y, c(y, z))))) = inj_1(m(z, x), m(m(z, x), m(y, c(m(x, y), z))))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[456])).
% 130.67/130.92 tff(458,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(y, c(m(x, y), z)))) = inj_1(m(z, x), m(m(z, x), m(c(x, z), m(y, c(y, z)))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[457])).
% 130.67/130.92 tff(459,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(y, c(m(x, y), z)))) = m(y, c(m(x, y), z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(460,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(y, c(m(x, y), z)))) = m(y, c(m(x, y), z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[459, 6])).
% 130.67/130.92 tff(461,plain,
% 130.67/130.92 (m(y, c(m(x, y), z)) = inj_1(m(z, x), m(m(z, x), m(y, c(m(x, y), z))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[460])).
% 130.67/130.92 tff(462,plain,
% 130.67/130.92 (m(y, c(m(x, y), z)) = m(m(c(x, z), y), c(y, z))),
% 130.67/130.92 inference(transitivity,[status(thm)],[461, 458, 437, 435])).
% 130.67/130.92 tff(463,plain,
% 130.67/130.92 (m(m(x, z), m(y, c(m(x, y), z))) = m(m(x, z), m(m(c(x, z), y), c(y, z)))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[462])).
% 130.67/130.92 tff(464,plain,
% 130.67/130.92 (m(m(x, z), m(m(c(x, z), y), c(y, z))) = m(m(x, z), m(y, c(m(x, y), z)))),
% 130.67/130.92 inference(symmetry,[status(thm)],[463])).
% 130.67/130.92 tff(465,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(m(c(x, z), y), c(y, z))) = m(m(m(x, z), m(c(x, z), y)), c(y, z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(466,plain,
% 130.67/130.92 (m(m(x, z), m(m(c(x, z), y), c(y, z))) = m(m(m(x, z), m(c(x, z), y)), c(y, z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[465, 15])).
% 130.67/130.92 tff(467,plain,
% 130.67/130.92 (m(m(m(x, z), m(c(x, z), y)), c(y, z)) = m(m(x, z), m(m(c(x, z), y), c(y, z)))),
% 130.67/130.92 inference(symmetry,[status(thm)],[466])).
% 130.67/130.92 tff(468,plain,
% 130.67/130.92 (m(c(x, z), m(m(z, x), m(c(x, z), y))) = m(c(x, z), m(x, m(z, y)))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[264])).
% 130.67/130.92 tff(469,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(m(z, x), m(c(x, z), y))) = m(m(c(x, z), m(z, x)), m(c(x, z), y)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(470,plain,
% 130.67/130.92 (m(c(x, z), m(m(z, x), m(c(x, z), y))) = m(m(c(x, z), m(z, x)), m(c(x, z), y))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[469, 15])).
% 130.67/130.92 tff(471,plain,
% 130.67/130.92 (m(m(c(x, z), m(z, x)), m(c(x, z), y)) = m(c(x, z), m(m(z, x), m(c(x, z), y)))),
% 130.67/130.92 inference(symmetry,[status(thm)],[470])).
% 130.67/130.92 tff(472,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(m(c(x, z), y), m(z, x)), m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x)))) = m(c(x, z), m(z, x)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(473,plain,
% 130.67/130.92 (inj_0(m(m(c(x, z), y), m(z, x)), m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x)))) = m(c(x, z), m(z, x))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[472, 28])).
% 130.67/130.92 tff(474,plain,
% 130.67/130.92 (m(m(m(x, z), y), m(x, z)) = m(m(x, z), m(y, m(x, z)))),
% 130.67/130.92 inference(symmetry,[status(thm)],[395])).
% 130.67/130.92 tff(475,plain,
% 130.67/130.92 (m(m(x, m(z, y)), m(x, z)) = m(m(m(x, z), y), m(x, z))),
% 130.67/130.92 inference(symmetry,[status(thm)],[393])).
% 130.67/130.92 tff(476,plain,
% 130.67/130.92 (m(c(x, z), m(m(x, m(z, y)), m(z, x))) = inj_1(m(z, x), m(m(z, x), m(c(x, z), m(m(x, m(z, y)), m(z, x)))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[39])).
% 130.67/130.92 tff(477,plain,
% 130.67/130.92 (m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(z, x)))) = m(c(x, z), m(m(x, m(z, y)), m(z, x)))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[268])).
% 130.67/130.92 tff(478,plain,
% 130.67/130.92 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(z, x)))) = m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x))))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(479,plain,
% 130.67/130.92 (m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(z, x)))) = m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x)))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[478, 15])).
% 130.67/130.92 tff(480,plain,
% 130.67/130.92 (m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x))) = m(c(x, z), m(m(z, x), m(m(c(x, z), y), m(z, x))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[479])).
% 130.67/130.92 tff(481,plain,
% 130.67/130.92 (m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x))) = m(m(x, z), m(y, m(x, z)))),
% 130.67/130.92 inference(transitivity,[status(thm)],[480, 477, 476, 72, 75, 475, 474])).
% 130.67/130.92 tff(482,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(y, m(x, z)))) = m(y, m(x, z)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(483,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(y, m(x, z)))) = m(y, m(x, z))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[482, 6])).
% 130.67/130.92 tff(484,plain,
% 130.67/130.92 (m(m(x, z), m(y, m(z, x))) = m(x, m(z, m(y, m(z, x))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[133])).
% 130.67/130.92 tff(485,plain,
% 130.67/130.92 (m(m(m(x, z), y), m(z, x)) = m(m(x, z), m(y, m(z, x)))),
% 130.67/130.92 inference(symmetry,[status(thm)],[131])).
% 130.67/130.92 tff(486,plain,
% 130.67/130.92 (m(m(x, m(z, y)), m(z, x)) = m(m(m(x, z), y), m(z, x))),
% 130.67/130.92 inference(symmetry,[status(thm)],[129])).
% 130.67/130.92 tff(487,plain,
% 130.67/130.92 (m(m(z, x), m(m(c(x, z), y), m(z, x))) = m(m(z, x), m(y, m(x, z)))),
% 130.67/130.92 inference(transitivity,[status(thm)],[267, 265, 486, 485, 484, 135, 356])).
% 130.67/130.92 tff(488,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(m(c(x, z), y), m(z, x)))) = inj_1(m(z, x), m(m(z, x), m(y, m(x, z))))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[487])).
% 130.67/130.92 tff(489,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(z, x), m(m(z, x), m(m(c(x, z), y), m(z, x)))) = m(m(c(x, z), y), m(z, x)))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.92 tff(490,plain,
% 130.67/130.92 (inj_1(m(z, x), m(m(z, x), m(m(c(x, z), y), m(z, x)))) = m(m(c(x, z), y), m(z, x))),
% 130.67/130.92 inference(unit_resolution,[status(thm)],[489, 6])).
% 130.67/130.92 tff(491,plain,
% 130.67/130.92 (m(m(c(x, z), y), m(z, x)) = inj_1(m(z, x), m(m(z, x), m(m(c(x, z), y), m(z, x))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[490])).
% 130.67/130.92 tff(492,plain,
% 130.67/130.92 (m(m(c(x, z), y), m(z, x)) = m(y, m(x, z))),
% 130.67/130.92 inference(transitivity,[status(thm)],[491, 488, 483])).
% 130.67/130.92 tff(493,plain,
% 130.67/130.92 (inj_0(m(m(c(x, z), y), m(z, x)), m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x)))) = inj_0(m(y, m(x, z)), m(m(x, z), m(y, m(x, z))))),
% 130.67/130.92 inference(monotonicity,[status(thm)],[492, 481])).
% 130.67/130.92 tff(494,plain,
% 130.67/130.92 (inj_0(m(y, m(x, z)), m(m(x, z), m(y, m(x, z)))) = inj_0(m(m(c(x, z), y), m(z, x)), m(m(c(x, z), m(z, x)), m(m(c(x, z), y), m(z, x))))),
% 130.67/130.92 inference(symmetry,[status(thm)],[493])).
% 130.67/130.92 tff(495,plain,
% 130.67/130.92 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(m(y, m(x, z)), m(m(x, z), m(y, m(x, z)))) = m(x, z))),
% 130.67/130.92 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(496,plain,
% 130.67/130.93 (inj_0(m(y, m(x, z)), m(m(x, z), m(y, m(x, z)))) = m(x, z)),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[495, 28])).
% 130.67/130.93 tff(497,plain,
% 130.67/130.93 (m(x, z) = inj_0(m(y, m(x, z)), m(m(x, z), m(y, m(x, z))))),
% 130.67/130.93 inference(symmetry,[status(thm)],[496])).
% 130.67/130.93 tff(498,plain,
% 130.67/130.93 (m(x, z) = m(c(x, z), m(z, x))),
% 130.67/130.93 inference(transitivity,[status(thm)],[497, 494, 473])).
% 130.67/130.93 tff(499,plain,
% 130.67/130.93 (m(m(x, z), m(c(x, z), y)) = m(m(c(x, z), m(z, x)), m(c(x, z), y))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[498])).
% 130.67/130.93 tff(500,plain,
% 130.67/130.93 (m(m(x, z), m(c(x, z), y)) = m(m(x, c(x, z)), m(z, y))),
% 130.67/130.93 inference(transitivity,[status(thm)],[499, 471, 468, 336, 334])).
% 130.67/130.93 tff(501,plain,
% 130.67/130.93 (m(m(m(x, z), m(c(x, z), y)), c(y, z)) = m(m(m(x, c(x, z)), m(z, y)), c(y, z))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[500])).
% 130.67/130.93 tff(502,plain,
% 130.67/130.93 (m(m(m(x, c(x, z)), m(z, y)), c(y, z)) = m(m(m(x, z), m(c(x, z), y)), c(y, z))),
% 130.67/130.93 inference(symmetry,[status(thm)],[501])).
% 130.67/130.93 tff(503,plain,
% 130.67/130.93 (m(m(x, c(x, z)), m(y, z)) = m(m(x, c(x, z)), m(m(z, y), c(y, z)))),
% 130.67/130.93 inference(symmetry,[status(thm)],[226])).
% 130.67/130.93 tff(504,plain,
% 130.67/130.93 (m(m(m(x, c(x, z)), y), z) = m(m(x, c(x, z)), m(y, z))),
% 130.67/130.93 inference(symmetry,[status(thm)],[225])).
% 130.67/130.93 tff(505,plain,
% 130.67/130.93 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(x, m(m(m(m(x, c(x, z)), y), z), x)) = m(m(m(x, c(x, z)), y), z))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(506,plain,
% 130.67/130.93 (inj_0(x, m(m(m(m(x, c(x, z)), y), z), x)) = m(m(m(x, c(x, z)), y), z)),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[505, 28])).
% 130.67/130.93 tff(507,plain,
% 130.67/130.93 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, c(x, z)), y), m(z, x)) = m(m(m(m(x, c(x, z)), y), z), x))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(508,plain,
% 130.67/130.93 (m(m(m(x, c(x, z)), y), m(z, x)) = m(m(m(m(x, c(x, z)), y), z), x)),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[507, 15])).
% 130.67/130.93 tff(509,plain,
% 130.67/130.93 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(x, m(m(y, z), m(x, c(x, z)))) = m(m(x, m(y, z)), m(x, c(x, z))))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(510,plain,
% 130.67/130.93 (m(x, m(m(y, z), m(x, c(x, z)))) = m(m(x, m(y, z)), m(x, c(x, z)))),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[509, 15])).
% 130.67/130.93 tff(511,plain,
% 130.67/130.93 (m(m(x, m(y, z)), m(x, c(x, z))) = m(x, m(m(y, z), m(x, c(x, z))))),
% 130.67/130.93 inference(symmetry,[status(thm)],[510])).
% 130.67/130.93 tff(512,plain,
% 130.67/130.93 (m(c(x, z), x) = inj_0(m(m(z, y), m(x, z)), m(m(c(x, z), x), m(m(z, y), m(x, z))))),
% 130.67/130.93 inference(symmetry,[status(thm)],[231])).
% 130.67/130.93 tff(513,plain,
% 130.67/130.93 (m(c(x, z), x) = m(x, c(x, z))),
% 130.67/130.93 inference(transitivity,[status(thm)],[512, 327, 330])).
% 130.67/130.93 tff(514,plain,
% 130.67/130.93 (m(m(x, y), z) = m(x, m(y, z))),
% 130.67/130.93 inference(symmetry,[status(thm)],[448])).
% 130.67/130.93 tff(515,plain,
% 130.67/130.93 (m(m(m(x, y), z), m(c(x, z), x)) = m(m(x, m(y, z)), m(x, c(x, z)))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[514, 513])).
% 130.67/130.93 tff(516,plain,
% 130.67/130.93 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(m(x, y), z), m(c(x, z), x)) = m(m(m(m(x, y), z), c(x, z)), x))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(517,plain,
% 130.67/130.93 (m(m(m(x, y), z), m(c(x, z), x)) = m(m(m(m(x, y), z), c(x, z)), x)),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[516, 15])).
% 130.67/130.93 tff(518,plain,
% 130.67/130.93 (m(m(m(m(x, y), z), c(x, z)), x) = m(m(m(x, y), z), m(c(x, z), x))),
% 130.67/130.93 inference(symmetry,[status(thm)],[517])).
% 130.67/130.93 tff(519,plain,
% 130.67/130.93 (m(m(m(m(x, y), z), c(x, z)), x) = m(m(m(m(x, c(x, z)), y), z), x)),
% 130.67/130.93 inference(transitivity,[status(thm)],[518, 515, 511, 147, 141, 138, 123, 508])).
% 130.67/130.93 tff(520,plain,
% 130.67/130.93 (inj_0(x, m(m(m(m(x, y), z), c(x, z)), x)) = inj_0(x, m(m(m(m(x, c(x, z)), y), z), x))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[519])).
% 130.67/130.93 tff(521,plain,
% 130.67/130.93 ((~![Xk!0: $i, Xk!1: $i] : (inj_0(Xk!0, m(Xk!1, Xk!0)) = Xk!1)) | (inj_0(x, m(m(m(m(x, y), z), c(x, z)), x)) = m(m(m(x, y), z), c(x, z)))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(522,plain,
% 130.67/130.93 (inj_0(x, m(m(m(m(x, y), z), c(x, z)), x)) = m(m(m(x, y), z), c(x, z))),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[521, 28])).
% 130.67/130.93 tff(523,plain,
% 130.67/130.93 (m(m(m(x, y), z), c(x, z)) = inj_0(x, m(m(m(m(x, y), z), c(x, z)), x))),
% 130.67/130.93 inference(symmetry,[status(thm)],[522])).
% 130.67/130.93 tff(524,plain,
% 130.67/130.93 (m(m(x, z), m(y, c(y, z))) = m(m(x, y), z)),
% 130.67/130.93 inference(transitivity,[status(thm)],[452, 449, 448])).
% 130.67/130.93 tff(525,plain,
% 130.67/130.93 (m(m(m(x, z), m(y, c(y, z))), c(x, z)) = m(m(m(x, y), z), c(x, z))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[524])).
% 130.67/130.93 tff(526,plain,
% 130.67/130.93 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(m(x, z), m(m(y, c(y, z)), c(x, z))) = m(m(m(x, z), m(y, c(y, z))), c(x, z)))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(527,plain,
% 130.67/130.93 (m(m(x, z), m(m(y, c(y, z)), c(x, z))) = m(m(m(x, z), m(y, c(y, z))), c(x, z))),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[526, 15])).
% 130.67/130.93 tff(528,plain,
% 130.67/130.93 (m(m(x, z), m(m(y, c(y, z)), c(x, z))) = m(m(x, z), m(y, c(m(x, y), z)))),
% 130.67/130.93 inference(transitivity,[status(thm)],[527, 525, 523, 520, 506, 504, 503, 228, 502, 467, 464])).
% 130.67/130.93 tff(529,plain,
% 130.67/130.93 (inj_1(m(x, z), m(m(x, z), m(m(y, c(y, z)), c(x, z)))) = inj_1(m(x, z), m(m(x, z), m(y, c(m(x, y), z))))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[528])).
% 130.67/130.93 tff(530,plain,
% 130.67/130.93 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(m(x, z), m(m(x, z), m(m(y, c(y, z)), c(x, z)))) = m(m(y, c(y, z)), c(x, z)))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(531,plain,
% 130.67/130.93 (inj_1(m(x, z), m(m(x, z), m(m(y, c(y, z)), c(x, z)))) = m(m(y, c(y, z)), c(x, z))),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[530, 6])).
% 130.67/130.93 tff(532,plain,
% 130.67/130.93 (m(m(y, c(y, z)), c(x, z)) = inj_1(m(x, z), m(m(x, z), m(m(y, c(y, z)), c(x, z))))),
% 130.67/130.93 inference(symmetry,[status(thm)],[531])).
% 130.67/130.93 tff(533,plain,
% 130.67/130.93 ((~![Z: $i, Y: $i, X: $i] : (m(X, m(Y, Z)) = m(m(X, Y), Z))) | (m(y, m(c(y, z), c(x, z))) = m(m(y, c(y, z)), c(x, z)))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(534,plain,
% 130.67/130.93 (m(y, m(c(y, z), c(x, z))) = m(m(y, c(y, z)), c(x, z))),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[533, 15])).
% 130.67/130.93 tff(535,plain,
% 130.67/130.93 (m(y, m(c(y, z), c(x, z))) = m(y, c(m(x, y), z))),
% 130.67/130.93 inference(transitivity,[status(thm)],[534, 532, 529, 433])).
% 130.67/130.93 tff(536,plain,
% 130.67/130.93 (inj_1(y, m(y, m(c(y, z), c(x, z)))) = inj_1(y, m(y, c(m(x, y), z)))),
% 130.67/130.93 inference(monotonicity,[status(thm)],[535])).
% 130.67/130.93 tff(537,plain,
% 130.67/130.93 (inj_1(y, m(y, c(m(x, y), z))) = inj_1(y, m(y, m(c(y, z), c(x, z))))),
% 130.67/130.93 inference(symmetry,[status(thm)],[536])).
% 130.67/130.93 tff(538,plain,
% 130.67/130.93 ((~![Xk!0: $i, Xk!1: $i] : (inj_1(Xk!1, m(Xk!1, Xk!0)) = Xk!0)) | (inj_1(y, m(y, c(m(x, y), z))) = c(m(x, y), z))),
% 130.67/130.93 inference(quant_inst,[status(thm)],[])).
% 130.67/130.93 tff(539,plain,
% 130.67/130.93 (inj_1(y, m(y, c(m(x, y), z))) = c(m(x, y), z)),
% 130.67/130.93 inference(unit_resolution,[status(thm)],[538, 6])).
% 130.67/130.93 tff(540,plain,
% 130.67/130.93 (c(m(x, y), z) = inj_1(y, m(y, c(m(x, y), z)))),
% 130.67/130.93 inference(symmetry,[status(thm)],[539])).
% 130.67/130.93 tff(541,plain,
% 130.67/130.93 (c(m(x, y), z) = m(c(x, z), c(y, z))),
% 130.67/130.93 inference(transitivity,[status(thm)],[540, 537, 431, 429, 426, 8])).
% 130.67/130.93 tff(542,plain,
% 130.67/130.93 ((~(c(m(x, y), z) = m(c(x, z), c(y, z)))) <=> (~(c(m(x, y), z) = m(c(x, z), c(y, z))))),
% 130.67/130.93 inference(rewrite,[status(thm)],[])).
% 130.67/130.93 tff(543,axiom,(~(c(m(x, y), z) = m(c(x, z), c(y, z)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','distributivity')).
% 130.67/130.97 tff(544,plain,
% 130.67/130.97 (~(c(m(x, y), z) = m(c(x, z), c(y, z)))),
% 130.67/130.97 inference(modus_ponens,[status(thm)],[543, 542])).
% 130.67/130.97 tff(545,plain,
% 130.67/130.97 ($false),
% 130.67/130.97 inference(unit_resolution,[status(thm)],[544, 541])).
% 130.67/130.97 % SZS output end Proof
% 130.67/130.97 % E exiting
%------------------------------------------------------------------------------