%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN551+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n002.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:39:33 AM UTC 2025
% Result : Theorem 0.19s 0.38s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYN551+1 : TPTP v9.0.0. Bugfixed v3.1.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n002.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 : Fri Jun 20 12:39:32 EDT 2025
% 0.12/0.34 % CPUTime :
% 0.19/0.38 % SZS status Theorem
% 0.19/0.38 % SZS output start Proof
% 0.19/0.38 tff(f_type, type, (
% 0.19/0.38 f: $i > $i)).
% 0.19/0.38 tff(g_type, type, (
% 0.19/0.38 g: $i > $i)).
% 0.19/0.38 tff(tptp_fun_X_0_type, type, (
% 0.19/0.38 tptp_fun_X_0: $i)).
% 0.19/0.38 tff(tptp_fun_X_3_type, type, (
% 0.19/0.38 tptp_fun_X_3: $i)).
% 0.19/0.38 tff(tptp_fun_Z_1_type, type, (
% 0.19/0.38 tptp_fun_Z_1: $i)).
% 0.19/0.38 tff(tptp_fun_Y_2_type, type, (
% 0.19/0.38 tptp_fun_Y_2: $i)).
% 0.19/0.38 tff(tptp_fun_Z_4_type, type, (
% 0.19/0.38 tptp_fun_Z_4: $i)).
% 0.19/0.38 tff(tptp_fun_Y_5_type, type, (
% 0.19/0.38 tptp_fun_Y_5: $i)).
% 0.19/0.38 tff(1,assumption,(~((~(X!3 = g(f(X!3)))) | (~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))))), introduced(assumption)).
% 0.19/0.38 tff(2,plain,
% 0.19/0.38 (((~(X!3 = g(f(X!3)))) | (~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y))))))) | (X!3 = g(f(X!3)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(3,plain,
% 0.19/0.38 (X!3 = g(f(X!3))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[2, 1])).
% 0.19/0.38 tff(4,assumption,(X!3 = g(f(X!3))), introduced(assumption)).
% 0.19/0.38 tff(5,plain,
% 0.19/0.38 (g(f(X!3)) = X!3),
% 0.19/0.38 inference(symmetry,[status(thm)],[4])).
% 0.19/0.38 tff(6,plain,
% 0.19/0.38 (f(g(f(X!3))) = f(X!3)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[5])).
% 0.19/0.38 tff(7,plain,
% 0.19/0.38 (g(f(g(f(X!3)))) = g(f(X!3))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[6])).
% 0.19/0.38 tff(8,plain,
% 0.19/0.38 (g(f(X!3)) = g(f(g(f(X!3))))),
% 0.19/0.38 inference(symmetry,[status(thm)],[7])).
% 0.19/0.38 tff(9,assumption,(~(g(f(X!3)) = g(f(g(f(X!3)))))), introduced(assumption)).
% 0.19/0.38 tff(10,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[9, 8])).
% 0.19/0.38 tff(11,plain,((g(f(X!3)) = g(f(g(f(X!3))))) | (~(X!3 = g(f(X!3))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(12,plain,
% 0.19/0.38 (g(f(X!3)) = g(f(g(f(X!3))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[11, 3])).
% 0.19/0.38 tff(13,plain,
% 0.19/0.38 (((~(X!3 = g(f(X!3)))) | (~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y))))))) | ![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(14,plain,
% 0.19/0.38 (![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[13, 1])).
% 0.19/0.38 tff(15,assumption,(~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))), introduced(assumption)).
% 0.19/0.38 tff(16,plain,
% 0.19/0.38 (((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))) | (Z!1 = f(g(Z!1)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(17,plain,
% 0.19/0.38 (Z!1 = f(g(Z!1))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[16, 15])).
% 0.19/0.38 tff(18,plain,
% 0.19/0.38 (f(g(Z!1)) = Z!1),
% 0.19/0.38 inference(symmetry,[status(thm)],[17])).
% 0.19/0.38 tff(19,plain,
% 0.19/0.38 (g(f(g(Z!1))) = g(Z!1)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[18])).
% 0.19/0.38 tff(20,plain,
% 0.19/0.38 (g(Z!1) = g(f(g(Z!1)))),
% 0.19/0.38 inference(symmetry,[status(thm)],[19])).
% 0.19/0.38 tff(21,plain,
% 0.19/0.38 (g(f(X!3)) = g(f(g(f(X!3))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[11, 4])).
% 0.19/0.38 tff(22,assumption,(![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))), introduced(assumption)).
% 0.19/0.38 tff(23,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((~(g(f(X!3)) = g(f(g(f(X!3)))))) | (g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(f(X!3)) = g(f(g(f(X!3)))))) | (g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(24,plain,
% 0.19/0.38 (((g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(f(X!3)) = g(f(g(f(X!3))))))) <=> ((~(g(f(X!3)) = g(f(g(f(X!3)))))) | (g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(25,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(f(X!3)) = g(f(g(f(X!3)))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((~(g(f(X!3)) = g(f(g(f(X!3)))))) | (g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1)))))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[24])).
% 0.19/0.38 tff(26,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(f(X!3)) = g(f(g(f(X!3)))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(f(X!3)) = g(f(g(f(X!3)))))) | (g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))))),
% 0.19/0.38 inference(transitivity,[status(thm)],[25, 23])).
% 0.19/0.38 tff(27,plain,
% 0.19/0.38 ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(f(X!3)) = g(f(g(f(X!3)))))))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(28,plain,
% 0.19/0.38 ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(f(X!3)) = g(f(g(f(X!3)))))) | (g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1)))))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[27, 26])).
% 0.19/0.38 tff(29,plain,
% 0.19/0.38 ((g(f(X!3)) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1)))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[28, 22, 21])).
% 0.19/0.38 tff(30,plain,
% 0.19/0.38 (g(f(X!3)) = g(Z!1)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[29, 20])).
% 0.19/0.38 tff(31,plain,
% 0.19/0.38 (g(Z!1) = g(f(X!3))),
% 0.19/0.38 inference(symmetry,[status(thm)],[30])).
% 0.19/0.38 tff(32,plain,
% 0.19/0.38 (g(Z!1) = X!3),
% 0.19/0.38 inference(transitivity,[status(thm)],[31, 5])).
% 0.19/0.38 tff(33,plain,
% 0.19/0.38 (f(g(Z!1)) = f(X!3)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[32])).
% 0.19/0.38 tff(34,plain,
% 0.19/0.38 (f(X!3) = f(g(Z!1))),
% 0.19/0.38 inference(symmetry,[status(thm)],[33])).
% 0.19/0.38 tff(35,plain,
% 0.19/0.38 (((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))) | (Y!2 = f(g(Y!2)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(36,plain,
% 0.19/0.38 (Y!2 = f(g(Y!2))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[35, 15])).
% 0.19/0.38 tff(37,plain,
% 0.19/0.38 (f(g(Y!2)) = Y!2),
% 0.19/0.38 inference(symmetry,[status(thm)],[36])).
% 0.19/0.38 tff(38,plain,
% 0.19/0.38 (g(f(g(Y!2))) = g(Y!2)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[37])).
% 0.19/0.38 tff(39,plain,
% 0.19/0.38 (g(Y!2) = g(f(g(Y!2)))),
% 0.19/0.38 inference(symmetry,[status(thm)],[38])).
% 0.19/0.38 tff(40,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(41,plain,
% 0.19/0.38 (((g(Y!2) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(Y!2) = g(f(g(Y!2)))))) <=> ((~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(42,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(Y!2) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(Y!2) = g(f(g(Y!2))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2)))))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[41])).
% 0.19/0.38 tff(43,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(Y!2) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(Y!2) = g(f(g(Y!2))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2))))))),
% 0.19/0.38 inference(transitivity,[status(thm)],[42, 40])).
% 0.19/0.38 tff(44,plain,
% 0.19/0.38 ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(Y!2) = g(Z!1)) | (~(g(Z!1) = g(f(g(Z!1))))) | (~(g(Y!2) = g(f(g(Y!2))))))),
% 0.19/0.38 inference(quant_inst,[status(thm)],[])).
% 0.19/0.38 tff(45,plain,
% 0.19/0.38 ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2)))))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[44, 43])).
% 0.19/0.38 tff(46,plain,
% 0.19/0.38 ((~(g(Z!1) = g(f(g(Z!1))))) | (g(Y!2) = g(Z!1)) | (~(g(Y!2) = g(f(g(Y!2)))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[45, 22])).
% 0.19/0.38 tff(47,plain,
% 0.19/0.38 (g(Y!2) = g(Z!1)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[46, 20, 39])).
% 0.19/0.38 tff(48,plain,
% 0.19/0.38 (g(Y!2) = X!3),
% 0.19/0.38 inference(transitivity,[status(thm)],[47, 31, 5])).
% 0.19/0.38 tff(49,plain,
% 0.19/0.38 (f(g(Y!2)) = f(X!3)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[48])).
% 0.19/0.38 tff(50,plain,
% 0.19/0.38 (Y!2 = Z!1),
% 0.19/0.38 inference(transitivity,[status(thm)],[36, 49, 34, 18])).
% 0.19/0.38 tff(51,plain,
% 0.19/0.38 (((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))) | (~(Y!2 = Z!1))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(52,plain,
% 0.19/0.38 (~(Y!2 = Z!1)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[51, 15])).
% 0.19/0.38 tff(53,plain,
% 0.19/0.38 ($false),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[52, 50])).
% 0.19/0.38 tff(54,plain,(((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))) | (~(X!3 = g(f(X!3)))) | (~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y))))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.38 tff(55,plain,
% 0.19/0.38 ((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[54, 3, 14])).
% 0.19/0.38 tff(56,assumption,(~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))), introduced(assumption)).
% 0.19/0.38 tff(57,plain,
% 0.19/0.38 (((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))) | (Y!5 = g(f(Y!5)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(58,plain,
% 0.19/0.38 (Y!5 = g(f(Y!5))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[57, 56])).
% 0.19/0.38 tff(59,plain,
% 0.19/0.38 (g(f(Y!5)) = Y!5),
% 0.19/0.38 inference(symmetry,[status(thm)],[58])).
% 0.19/0.38 tff(60,plain,
% 0.19/0.38 (f(g(f(Y!5))) = f(Y!5)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[59])).
% 0.19/0.38 tff(61,plain,
% 0.19/0.38 (g(f(g(f(Y!5)))) = g(f(Y!5))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[60])).
% 0.19/0.38 tff(62,plain,
% 0.19/0.38 (g(f(Y!5)) = g(f(g(f(Y!5))))),
% 0.19/0.38 inference(symmetry,[status(thm)],[61])).
% 0.19/0.38 tff(63,plain,
% 0.19/0.38 (((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))) | (Z!4 = g(f(Z!4)))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(64,plain,
% 0.19/0.38 (Z!4 = g(f(Z!4))),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[63, 56])).
% 0.19/0.38 tff(65,plain,
% 0.19/0.38 (g(f(Z!4)) = Z!4),
% 0.19/0.38 inference(symmetry,[status(thm)],[64])).
% 0.19/0.38 tff(66,plain,
% 0.19/0.38 ((g(f(Y!5)) = g(f(Z!4))) <=> (Y!5 = Z!4)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[59, 65])).
% 0.19/0.38 tff(67,plain,
% 0.19/0.38 ((Y!5 = Z!4) <=> (g(f(Y!5)) = g(f(Z!4)))),
% 0.19/0.38 inference(symmetry,[status(thm)],[66])).
% 0.19/0.38 tff(68,plain,
% 0.19/0.38 ((~(Y!5 = Z!4)) <=> (~(g(f(Y!5)) = g(f(Z!4))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[67])).
% 0.19/0.38 tff(69,plain,
% 0.19/0.38 (((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))) | (~(Y!5 = Z!4))),
% 0.19/0.38 inference(tautology,[status(thm)],[])).
% 0.19/0.38 tff(70,plain,
% 0.19/0.38 (~(Y!5 = Z!4)),
% 0.19/0.38 inference(unit_resolution,[status(thm)],[69, 56])).
% 0.19/0.38 tff(71,plain,
% 0.19/0.38 (~(g(f(Y!5)) = g(f(Z!4)))),
% 0.19/0.38 inference(modus_ponens,[status(thm)],[70, 68])).
% 0.19/0.38 tff(72,plain,
% 0.19/0.38 (f(g(f(Z!4))) = f(Z!4)),
% 0.19/0.38 inference(monotonicity,[status(thm)],[65])).
% 0.19/0.38 tff(73,plain,
% 0.19/0.38 (g(f(g(f(Z!4)))) = g(f(Z!4))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[72])).
% 0.19/0.38 tff(74,plain,
% 0.19/0.38 (g(f(Z!4)) = g(f(g(f(Z!4))))),
% 0.19/0.38 inference(symmetry,[status(thm)],[73])).
% 0.19/0.38 tff(75,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(76,plain,
% 0.19/0.38 (((g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (~(g(f(Y!5)) = g(f(g(f(Y!5))))))) <=> ((~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))),
% 0.19/0.38 inference(rewrite,[status(thm)],[])).
% 0.19/0.38 tff(77,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5))))))))),
% 0.19/0.38 inference(monotonicity,[status(thm)],[76])).
% 0.19/0.38 tff(78,plain,
% 0.19/0.38 (((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))) <=> ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))),
% 0.19/0.38 inference(transitivity,[status(thm)],[77, 75])).
% 0.19/0.38 tff(79,plain,
% 0.19/0.38 ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | ((g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (~(g(f(Y!5)) = g(f(g(f(Y!5)))))))),
% 0.19/0.39 inference(quant_inst,[status(thm)],[])).
% 0.19/0.39 tff(80,plain,
% 0.19/0.39 ((~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y)))))) | (~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5))))))),
% 0.19/0.39 inference(modus_ponens,[status(thm)],[79, 78])).
% 0.19/0.39 tff(81,plain,
% 0.19/0.39 ((~(g(f(Z!4)) = g(f(g(f(Z!4)))))) | (g(f(Y!5)) = g(f(Z!4))) | (~(g(f(Y!5)) = g(f(g(f(Y!5))))))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[80, 22])).
% 0.19/0.39 tff(82,plain,
% 0.19/0.39 ($false),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[81, 74, 71, 62])).
% 0.19/0.39 tff(83,plain,(((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))) | (~![Y: $i, Z: $i] : ((Y = Z) | (~(Z = g(f(Z)))) | (~(Y = g(f(Y))))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.39 tff(84,plain,
% 0.19/0.39 ((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[83, 14])).
% 0.19/0.39 tff(85,plain,
% 0.19/0.39 (f(X!3) = f(g(f(X!3)))),
% 0.19/0.39 inference(symmetry,[status(thm)],[6])).
% 0.19/0.39 tff(86,assumption,(![X: $i] : (~(X = f(g(X))))), introduced(assumption)).
% 0.19/0.39 tff(87,plain,
% 0.19/0.39 ((~![X: $i] : (~(X = f(g(X))))) | (~(f(X!3) = f(g(f(X!3)))))),
% 0.19/0.39 inference(quant_inst,[status(thm)],[])).
% 0.19/0.39 tff(88,plain,
% 0.19/0.39 ($false),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[87, 86, 85])).
% 0.19/0.39 tff(89,plain,((~![X: $i] : (~(X = f(g(X))))) | (~(X!3 = g(f(X!3))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.39 tff(90,plain,
% 0.19/0.39 (~![X: $i] : (~(X = f(g(X))))),
% 0.19/0.39 inference(unit_resolution,[status(thm)],[89, 3])).
% 0.19/0.39 tff(91,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))) <=> ((~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))) | ![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(92,plain,
% 0.19/0.39 ((~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))) <=> (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(93,plain,
% 0.19/0.39 ((~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) <=> (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(94,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))) <=> (![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[93, 92])).
% 0.19/0.39 tff(95,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))) <=> ((~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))) | ![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))))),
% 0.19/0.39 inference(transitivity,[status(thm)],[94, 91])).
% 0.19/0.39 tff(96,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))) <=> (![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(97,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))) <=> (![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(98,plain,
% 0.19/0.39 ((~((~((Y!5 = g(f(Y!5))) & (Z!4 = g(f(Z!4))))) | (Y!5 = Z!4))) <=> (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(99,plain,
% 0.19/0.39 ((~((~((Y!2 = f(g(Y!2))) & (Z!1 = f(g(Z!1))))) | (Y!2 = Z!1))) <=> (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1))))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(100,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | (~((~((Y!2 = f(g(Y!2))) & (Z!1 = f(g(Z!1))))) | (Y!2 = Z!1))) | ![X: $i] : (~(X = g(f(X)))) | (~((~((Y!5 = g(f(Y!5))) & (Z!4 = g(f(Z!4))))) | (Y!5 = Z!4)))) <=> (![X: $i] : (~(X = f(g(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[99, 98])).
% 0.19/0.39 tff(101,plain,
% 0.19/0.39 ((![X: $i] : (~(X = f(g(X)))) | (~((~((Y!2 = f(g(Y!2))) & (Z!1 = f(g(Z!1))))) | (Y!2 = Z!1))) | ![X: $i] : (~(X = g(f(X)))) | (~((~((Y!5 = g(f(Y!5))) & (Z!4 = g(f(Z!4))))) | (Y!5 = Z!4)))) <=> (![X: $i] : (~(X = f(g(X)))) | ![X: $i] : (~(X = g(f(X)))) | (~((Y!2 = Z!1) | (~(Y!2 = f(g(Y!2)))) | (~(Z!1 = f(g(Z!1)))))) | (~((Y!5 = Z!4) | (~(Y!5 = g(f(Y!5)))) | (~(Z!4 = g(f(Z!4)))))))),
% 0.19/0.39 inference(transitivity,[status(thm)],[100, 97])).
% 0.19/0.39 tff(102,plain,
% 0.19/0.39 (((((X!0 = f(g(X!0))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) | ((X!3 = g(f(X!3))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))) & ((![X: $i] : (~(X = f(g(X)))) | (~((~((Y!2 = f(g(Y!2))) & (Z!1 = f(g(Z!1))))) | (Y!2 = Z!1)))) | (![X: $i] : (~(X = g(f(X)))) | (~((~((Y!5 = g(f(Y!5))) & (Z!4 = g(f(Z!4))))) | (Y!5 = Z!4)))))) <=> ((((X!0 = f(g(X!0))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) | ((X!3 = g(f(X!3))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))) & (![X: $i] : (~(X = f(g(X)))) | (~((~((Y!2 = f(g(Y!2))) & (Z!1 = f(g(Z!1))))) | (Y!2 = Z!1))) | ![X: $i] : (~(X = g(f(X)))) | (~((~((Y!5 = g(f(Y!5))) & (Z!4 = g(f(Z!4))))) | (Y!5 = Z!4)))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(103,plain,
% 0.19/0.39 ((~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))) <=> (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(104,plain,
% 0.19/0.39 ((?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(105,plain,
% 0.19/0.39 ((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z)))),
% 0.19/0.39 inference(rewrite,[status(thm)],[])).
% 0.19/0.39 tff(106,plain,
% 0.19/0.39 (((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))) <=> ((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[105, 104])).
% 0.19/0.39 tff(107,plain,
% 0.19/0.39 ((~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))) <=> (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))))),
% 0.19/0.39 inference(monotonicity,[status(thm)],[106])).
% 0.19/0.40 tff(108,plain,
% 0.19/0.40 ((~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))) <=> (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))))),
% 0.19/0.40 inference(transitivity,[status(thm)],[107, 103])).
% 0.19/0.40 tff(109,plain,
% 0.19/0.40 (((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : (((Y = f(g(Y))) & (Z = f(g(Z)))) => (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : (((Y = g(f(Y))) & (Z = g(f(Z)))) => (Y = Z)))) <=> ((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))),
% 0.19/0.40 inference(rewrite,[status(thm)],[])).
% 0.19/0.40 tff(110,plain,
% 0.19/0.40 ((~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : (((Y = f(g(Y))) & (Z = f(g(Z)))) => (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : (((Y = g(f(Y))) & (Z = g(f(Z)))) => (Y = Z))))) <=> (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))))),
% 0.19/0.40 inference(monotonicity,[status(thm)],[109])).
% 0.19/0.40 tff(111,plain,
% 0.19/0.40 ((~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : (((Y = f(g(Y))) & (Z = f(g(Z)))) => (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : (((Y = g(f(Y))) & (Z = g(f(Z)))) => (Y = Z))))) <=> (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z)))))),
% 0.19/0.40 inference(transitivity,[status(thm)],[110, 103])).
% 0.19/0.40 tff(112,axiom,(~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : (((Y = f(g(Y))) & (Z = f(g(Z)))) => (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : (((Y = g(f(Y))) & (Z = g(f(Z)))) => (Y = Z))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','prove_this_cute_thing')).
% 0.19/0.40 tff(113,plain,
% 0.19/0.40 (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.19/0.40 tff(114,plain,
% 0.19/0.40 (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[113, 108])).
% 0.19/0.40 tff(115,plain,
% 0.19/0.40 (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[114, 103])).
% 0.19/0.40 tff(116,plain,
% 0.19/0.40 (~((?[X: $i] : (X = f(g(X))) & ![Y: $i, Z: $i] : ((~((Y = f(g(Y))) & (Z = f(g(Z))))) | (Y = Z))) <=> (?[X: $i] : (X = g(f(X))) & ![Y: $i, Z: $i] : ((~((Y = g(f(Y))) & (Z = g(f(Z))))) | (Y = Z))))),
% 0.19/0.40 inference(modus_ponens,[status(thm)],[115, 108])).
% 0.19/0.40 unexpected number of arguments: (let ((a!1 (exists ((X $i)) (= X (f (g X)))))
% 0.19/0.40 (a!3 (lambda ((Y $i) (Z $i))
% 0.19/0.40 (let ((a!1 (and (= Y (f (g Y))) (= Z (f (g Z))))))
% 0.19/0.40 (refl (~ (or (not a!1) (= Y Z)) (or (not a!1) (= Y Z)))))))
% 0.19/0.40 (a!4 (forall ((Y $i) (Z $i))
% 0.19/0.40 (let ((a!1 (and (= Y (f (g Y))) (= Z (f (g Z))))))
% 0.19/0.40 (or (not a!1) (= Y Z)))))
% 0.19/0.40 (a!6 (proof-bind (lambda ((X $i))
% 0.19/0.40 (let ((a!1 (not (= X (f (g X))))))
% 0.19/0.40 (refl (~ a!1 a!1))))))
% 0.19/0.40 (a!7 (forall ((X $i)) (not (= X (f (g X))))))
% 0.19/0.40 (a!8 (and (= Y!2 (f (g Y!2))) (= Z!1 (f (g Z!1)))))
% 0.19/0.40 (a!12 (exists ((X $i)) (= X (g (f X)))))
% 0.19/0.40 (a!14 (lambda ((Y $i) (Z $i))
% 0.19/0.40 (let ((a!1 (and (= Y (g (f Y))) (= Z (g (f Z))))))
% 0.19/0.40 (refl (~ (or (not a!1) (= Y Z)) (or (not a!1) (= Y Z)))))))
% 0.19/0.40 (a!15 (forall ((Y $i) (Z $i))
% 0.19/0.40 (let ((a!1 (and (= Y (g (f Y))) (= Z (g (f Z))))))
% 0.19/0.40 (or (not a!1) (= Y Z)))))
% 0.19/0.40 (a!17 (proof-bind (lambda ((X $i))
% 0.19/0.40 (let ((a!1 (not (= X (g (f X))))))
% 0.19/0.40 (refl (~ a!1 a!1))))))
% 0.19/0.40 (a!18 (forall ((X $i)) (not (= X (g (f X))))))
% 0.19/0.40 (a!19 (and (= Y!5 (g (f Y!5))) (= Z!4 (g (f Z!4))))))
% 0.19/0.40 (let ((a!2 (~ a!1 (= X!0 (f (g X!0)))))
% 0.19/0.40 (a!5 (and (= X!0 (f (g X!0))) a!4))
% 0.19/0.40 (a!9 (~ (not a!4) (not (or (not a!8) (= Y!2 Z!1)))))
% 0.19/0.40 (a!10 (or a!7 (not (or (not a!8) (= Y!2 Z!1)))))
% 0.19/0.40 (a!13 (~ a!12 (= X!3 (g (f X!3)))))
% 0.19/0.40 (a!16 (and (= X!3 (g (f X!3))) a!15))
% 0.19/0.40 (a!20 (~ (not a!15) (not (or (not a!19) (= Y!5 Z!4)))))
% 0.19/0.40 (a!21 (or a!18 (not (or (not a!19) (= Y!5 Z!4))))))
% 0.19/0.40 (let ((a!11 (nnf-neg (nnf-neg a!6 (~ (not a!1) a!7))
% 0.19/0.40 (sk a!9)
% 0.19/0.40 (~ (not (and a!1 a!4)) a!10)))
% 0.19/0.40 (a!22 (nnf-neg (nnf-neg a!17 (~ (not a!12) a!18))
% 0.19/0.40 (sk a!20)
% 0.19/0.40 (~ (not (and a!12 a!15)) a!21)))
% 0.19/0.40 (a!23 (~ (not (= (and a!1 a!4) (and a!12 a!15)))
% 0.19/0.40 (and (or a!5 a!16) (or a!10 a!21)))))
% 0.19/0.40 (nnf-neg (monotonicity (sk a!2)
% 0.19/0.40 (nnf-pos (proof-bind a!3) (~ a!4 a!4))
% 0.19/0.40 (~ (and a!1 a!4) a!5))
% 0.19/0.40 a!11
% 0.19/0.40 (monotonicity (sk a!13)
% 0.19/0.40 (nnf-pos (proof-bind a!14) (~ a!15 a!15))
% 0.19/0.40 (~ (and a!12 a!15) a!16))
% 0.19/0.40 a!22
% 0.19/0.40 a!23))))
% 0.19/0.40 Proof display could not be completed: unexpected number of arguments
% 0.19/0.41 % E exiting
%------------------------------------------------------------------------------