%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SYN076+1 : TPTP v9.0.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.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:38:10 AM UTC 2025
% Result : Theorem 2.85s 3.10s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN076+1 : TPTP v9.0.0. Released v2.0.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n014.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.33 % CPULimit : 300
% 0.11/0.33 % WCLimit : 300
% 0.11/0.33 % DateTime : Fri Jun 20 12:28:09 EDT 2025
% 0.11/0.33 % CPUTime :
% 2.85/3.10 % SZS status Theorem
% 2.85/3.10 % SZS output start Proof
% 2.85/3.10 tff(big_f_type, type, (
% 2.85/3.10 big_f: ( $i * $i ) > $o)).
% 2.85/3.10 tff(tptp_fun_X_1_type, type, (
% 2.85/3.10 tptp_fun_X_1: $i)).
% 2.85/3.10 tff(tptp_fun_X_5_type, type, (
% 2.85/3.10 tptp_fun_X_5: $i > $i)).
% 2.85/3.10 tff(tptp_fun_Y_0_type, type, (
% 2.85/3.10 tptp_fun_Y_0: $i)).
% 2.85/3.10 tff(tptp_fun_Y_4_type, type, (
% 2.85/3.10 tptp_fun_Y_4: ( $i * $i ) > $i)).
% 2.85/3.10 tff(tptp_fun_Z_2_type, type, (
% 2.85/3.10 tptp_fun_Z_2: $i)).
% 2.85/3.10 tff(tptp_fun_W_3_type, type, (
% 2.85/3.10 tptp_fun_W_3: $i > $i)).
% 2.85/3.10 tff(tptp_fun_Y1_11_type, type, (
% 2.85/3.10 tptp_fun_Y1_11: $i > $i)).
% 2.85/3.10 tff(tptp_fun_W1_8_type, type, (
% 2.85/3.10 tptp_fun_W1_8: $i)).
% 2.85/3.10 tff(tptp_fun_Z1_12_type, type, (
% 2.85/3.10 tptp_fun_Z1_12: $i > $i)).
% 2.85/3.10 tff(tptp_fun_Z1_9_type, type, (
% 2.85/3.10 tptp_fun_Z1_9: $i > $i)).
% 2.85/3.10 tff(tptp_fun_Y_7_type, type, (
% 2.85/3.10 tptp_fun_Y_7: ( $i * $i ) > $i)).
% 2.85/3.10 tff(tptp_fun_X1_10_type, type, (
% 2.85/3.10 tptp_fun_X1_10: ( $i * $i ) > $i)).
% 2.85/3.10 tff(tptp_fun_X1_13_type, type, (
% 2.85/3.10 tptp_fun_X1_13: ( $i * $i ) > $i)).
% 2.85/3.10 tff(tptp_fun_W_6_type, type, (
% 2.85/3.10 tptp_fun_W_6: $i > $i)).
% 2.85/3.10 tff(1,plain,
% 2.85/3.10 ((tptp_fun_W_3(Z!2) = X!1) <=> (X!1 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(commutativity,[status(thm)],[])).
% 2.85/3.10 tff(2,plain,
% 2.85/3.10 ((X!1 = tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = X!1)),
% 2.85/3.10 inference(symmetry,[status(thm)],[1])).
% 2.85/3.10 tff(3,assumption,(~(Z!2 = Y!0)), introduced(assumption)).
% 2.85/3.10 tff(4,plain,
% 2.85/3.10 ((Y!0 = Z!2) <=> (Z!2 = Y!0)),
% 2.85/3.10 inference(commutativity,[status(thm)],[])).
% 2.85/3.10 tff(5,assumption,(Y!0 = Z!2), introduced(assumption)).
% 2.85/3.10 tff(6,plain,
% 2.85/3.10 (Z!2 = Y!0),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[5, 4])).
% 2.85/3.10 tff(7,plain,
% 2.85/3.10 ($false),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[3, 6])).
% 2.85/3.10 tff(8,plain,((~(Y!0 = Z!2)) | (Z!2 = Y!0)), inference(lemma,lemma(discharge,[]))).
% 2.85/3.10 tff(9,plain,
% 2.85/3.10 (~(Y!0 = Z!2)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[8, 3])).
% 2.85/3.10 tff(10,plain,
% 2.85/3.10 (((~(X!1 = Y!0)) & ![Z: $i] : ((Z = Y!0) | (Z = X!1))) <=> ((~(X!1 = Y!0)) & ![Z: $i] : ((Z = Y!0) | (Z = X!1)))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(11,plain,
% 2.85/3.10 (?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = Y) | (Z = X))) <=> ?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = Y) | (Z = X)))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(12,plain,
% 2.85/3.10 (^[X: $i, Y: $i] : rewrite(((~(X = Y)) & ![Z: $i] : ((Z = X) | (Z = Y))) <=> ((~(X = Y)) & ![Z: $i] : ((Z = Y) | (Z = X))))),
% 2.85/3.10 inference(bind,[status(th)],[])).
% 2.85/3.10 tff(13,plain,
% 2.85/3.10 (?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = X) | (Z = Y))) <=> ?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = Y) | (Z = X)))),
% 2.85/3.10 inference(quant_intro,[status(thm)],[12])).
% 2.85/3.10 tff(14,axiom,(?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = X) | (Z = Y)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pel53_1')).
% 2.85/3.10 tff(15,plain,
% 2.85/3.10 (?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = Y) | (Z = X)))),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[14, 13])).
% 2.85/3.10 tff(16,plain,
% 2.85/3.10 (?[X: $i, Y: $i] : ((~(X = Y)) & ![Z: $i] : ((Z = Y) | (Z = X)))),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[15, 11])).
% 2.85/3.10 tff(17,plain,
% 2.85/3.10 ((~(X!1 = Y!0)) & ![Z: $i] : ((Z = Y!0) | (Z = X!1))),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[16, 10])).
% 2.85/3.10 tff(18,plain,
% 2.85/3.10 (![Z: $i] : ((Z = Y!0) | (Z = X!1))),
% 2.85/3.10 inference(and_elim,[status(thm)],[17])).
% 2.85/3.10 tff(19,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((Z!2 = Y!0) | (Z!2 = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (Z!2 = Y!0) | (Z!2 = X!1))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(20,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((Z!2 = Y!0) | (Z!2 = X!1))),
% 2.85/3.10 inference(quant_inst,[status(thm)],[])).
% 2.85/3.10 tff(21,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (Z!2 = Y!0) | (Z!2 = X!1)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[20, 19])).
% 2.85/3.10 tff(22,plain,
% 2.85/3.10 ((Z!2 = Y!0) | (Z!2 = X!1)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[21, 18])).
% 2.85/3.10 tff(23,plain,
% 2.85/3.10 (Z!2 = X!1),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[22, 3])).
% 2.85/3.10 tff(24,assumption,(~(Y!0 = Z!2)), introduced(assumption)).
% 2.85/3.10 tff(25,assumption,(Z!2 = X!1), introduced(assumption)).
% 2.85/3.10 tff(26,assumption,(~(W1!8 = Y!0)), introduced(assumption)).
% 2.85/3.10 tff(27,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((W1!8 = Y!0) | (W1!8 = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (W1!8 = Y!0) | (W1!8 = X!1))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(28,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((W1!8 = Y!0) | (W1!8 = X!1))),
% 2.85/3.10 inference(quant_inst,[status(thm)],[])).
% 2.85/3.10 tff(29,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (W1!8 = Y!0) | (W1!8 = X!1)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[28, 27])).
% 2.85/3.10 tff(30,plain,
% 2.85/3.10 ((W1!8 = Y!0) | (W1!8 = X!1)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[29, 18])).
% 2.85/3.10 tff(31,plain,
% 2.85/3.10 (W1!8 = X!1),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[30, 26])).
% 2.85/3.10 tff(32,plain,
% 2.85/3.10 (X!1 = W1!8),
% 2.85/3.10 inference(symmetry,[status(thm)],[31])).
% 2.85/3.10 tff(33,plain,
% 2.85/3.10 ((Y!0 = tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = Y!0)),
% 2.85/3.10 inference(commutativity,[status(thm)],[])).
% 2.85/3.10 tff(34,plain,
% 2.85/3.10 ((tptp_fun_W_3(Z!2) = Y!0) <=> (Y!0 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(symmetry,[status(thm)],[33])).
% 2.85/3.10 tff(35,plain,
% 2.85/3.10 (X!1 = Z!2),
% 2.85/3.10 inference(symmetry,[status(thm)],[25])).
% 2.85/3.10 tff(36,plain,
% 2.85/3.10 (tptp_fun_W_3(X!1) = tptp_fun_W_3(Z!2)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[35])).
% 2.85/3.10 tff(37,plain,
% 2.85/3.10 (tptp_fun_W_3(Z!2) = tptp_fun_W_3(X!1)),
% 2.85/3.10 inference(symmetry,[status(thm)],[36])).
% 2.85/3.10 tff(38,plain,
% 2.85/3.10 ((tptp_fun_W_3(Z!2) = Y!0) <=> (tptp_fun_W_3(X!1) = Y!0)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[37])).
% 2.85/3.10 tff(39,plain,
% 2.85/3.10 ((tptp_fun_W_3(X!1) = Y!0) <=> (tptp_fun_W_3(Z!2) = Y!0)),
% 2.85/3.10 inference(symmetry,[status(thm)],[38])).
% 2.85/3.10 tff(40,assumption,(~(tptp_fun_Y1_11(X!1) = X!1)), introduced(assumption)).
% 2.85/3.10 tff(41,plain,
% 2.85/3.10 (big_f(X!1, W1!8) <=> big_f(Z!2, X!1)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[35, 31])).
% 2.85/3.10 tff(42,plain,
% 2.85/3.10 ((~big_f(X!1, W1!8)) <=> (~big_f(Z!2, X!1))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[41])).
% 2.85/3.10 tff(43,assumption,(~big_f(X!1, W1!8)), introduced(assumption)).
% 2.85/3.10 tff(44,plain,
% 2.85/3.10 (~big_f(Z!2, X!1)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[43, 42])).
% 2.85/3.10 tff(45,assumption,(~(tptp_fun_Z1_12(X!1) = X!1)), introduced(assumption)).
% 2.85/3.10 tff(46,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(47,plain,
% 2.85/3.10 (((tptp_fun_Z1_12(X!1) = Y!0) | (tptp_fun_Z1_12(X!1) = X!1)) <=> ((tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(48,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_12(X!1) = Y!0) | (tptp_fun_Z1_12(X!1) = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0)))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[47])).
% 2.85/3.10 tff(49,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_12(X!1) = Y!0) | (tptp_fun_Z1_12(X!1) = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0))),
% 2.85/3.10 inference(transitivity,[status(thm)],[48, 46])).
% 2.85/3.10 tff(50,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_12(X!1) = Y!0) | (tptp_fun_Z1_12(X!1) = X!1))),
% 2.85/3.10 inference(quant_inst,[status(thm)],[])).
% 2.85/3.10 tff(51,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[50, 49])).
% 2.85/3.10 tff(52,plain,
% 2.85/3.10 ((tptp_fun_Z1_12(X!1) = X!1) | (tptp_fun_Z1_12(X!1) = Y!0)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[51, 18])).
% 2.85/3.10 tff(53,plain,
% 2.85/3.10 (tptp_fun_Z1_12(X!1) = Y!0),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[52, 45])).
% 2.85/3.10 tff(54,assumption,(tptp_fun_Z1_12(X!1) = Y!0), introduced(assumption)).
% 2.85/3.10 tff(55,assumption,(tptp_fun_Y1_11(X!1) = X!1), introduced(assumption)).
% 2.85/3.10 tff(56,plain,
% 2.85/3.10 (X!1 = tptp_fun_Y1_11(X!1)),
% 2.85/3.10 inference(symmetry,[status(thm)],[55])).
% 2.85/3.10 tff(57,assumption,(~big_f(Z!2, X!1)), introduced(assumption)).
% 2.85/3.10 tff(58,assumption,(tptp_fun_X_5(X!1) = X!1), introduced(assumption)).
% 2.85/3.10 tff(59,plain,
% 2.85/3.10 (big_f(tptp_fun_X_5(X!1), W1!8) <=> big_f(X!1, W1!8)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[58])).
% 2.85/3.10 tff(60,plain,
% 2.85/3.10 (big_f(X!1, W1!8) <=> big_f(tptp_fun_X_5(X!1), W1!8)),
% 2.85/3.10 inference(symmetry,[status(thm)],[59])).
% 2.85/3.10 tff(61,plain,
% 2.85/3.10 ((~big_f(X!1, W1!8)) <=> (~big_f(tptp_fun_X_5(X!1), W1!8))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[60])).
% 2.85/3.10 tff(62,assumption,(W1!8 = Y!0), introduced(assumption)).
% 2.85/3.10 tff(63,plain,
% 2.85/3.10 (Y!0 = W1!8),
% 2.85/3.10 inference(symmetry,[status(thm)],[62])).
% 2.85/3.10 tff(64,plain,
% 2.85/3.10 (big_f(Y!0, W1!8) <=> big_f(W1!8, W1!8)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[63])).
% 2.85/3.10 tff(65,plain,
% 2.85/3.10 (big_f(W1!8, W1!8) <=> big_f(Y!0, W1!8)),
% 2.85/3.10 inference(symmetry,[status(thm)],[64])).
% 2.85/3.10 tff(66,plain,
% 2.85/3.10 (X!1 = tptp_fun_X_5(X!1)),
% 2.85/3.10 inference(symmetry,[status(thm)],[58])).
% 2.85/3.10 tff(67,plain,
% 2.85/3.10 (tptp_fun_X1_10(X!1, Z!2) = tptp_fun_X1_10(tptp_fun_X_5(X!1), X!1)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[66, 25])).
% 2.85/3.10 tff(68,plain,
% 2.85/3.10 (tptp_fun_X1_10(tptp_fun_X_5(X!1), X!1) = tptp_fun_X1_10(X!1, Z!2)),
% 2.85/3.10 inference(symmetry,[status(thm)],[67])).
% 2.85/3.10 tff(69,plain,
% 2.85/3.10 (tptp_fun_Z1_9(W1!8) = tptp_fun_Z1_9(Y!0)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[62])).
% 2.85/3.10 tff(70,assumption,(tptp_fun_W_3(Z!2) = Y!0), introduced(assumption)).
% 2.85/3.10 tff(71,plain,
% 2.85/3.10 ((X!1 = tptp_fun_W_3(X!1)) <=> (tptp_fun_W_3(X!1) = X!1)),
% 2.85/3.10 inference(commutativity,[status(thm)],[])).
% 2.85/3.10 tff(72,plain,
% 2.85/3.10 ((X!1 = tptp_fun_W_3(Z!2)) <=> (X!1 = tptp_fun_W_3(X!1))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[37])).
% 2.85/3.10 tff(73,plain,
% 2.85/3.10 ((X!1 = tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(X!1) = X!1)),
% 2.85/3.10 inference(transitivity,[status(thm)],[72, 71])).
% 2.85/3.10 tff(74,plain,
% 2.85/3.10 ((tptp_fun_W_3(X!1) = X!1) <=> (X!1 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(symmetry,[status(thm)],[73])).
% 2.85/3.10 tff(75,plain,
% 2.85/3.10 ((Y!0 = X!1) <=> (X!1 = Y!0)),
% 2.85/3.10 inference(commutativity,[status(thm)],[])).
% 2.85/3.10 tff(76,plain,
% 2.85/3.10 (tptp_fun_W_3(X!1) = Y!0),
% 2.85/3.10 inference(transitivity,[status(thm)],[36, 70])).
% 2.85/3.10 tff(77,plain,
% 2.85/3.10 ((tptp_fun_W_3(X!1) = X!1) <=> (Y!0 = X!1)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[76])).
% 2.85/3.10 tff(78,plain,
% 2.85/3.10 ((tptp_fun_W_3(X!1) = X!1) <=> (X!1 = Y!0)),
% 2.85/3.10 inference(transitivity,[status(thm)],[77, 75])).
% 2.85/3.10 tff(79,plain,
% 2.85/3.10 ((X!1 = Y!0) <=> (tptp_fun_W_3(X!1) = X!1)),
% 2.85/3.10 inference(symmetry,[status(thm)],[78])).
% 2.85/3.10 tff(80,plain,
% 2.85/3.10 ((X!1 = Y!0) <=> (X!1 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(transitivity,[status(thm)],[79, 74])).
% 2.85/3.10 tff(81,plain,
% 2.85/3.10 ((~(X!1 = Y!0)) <=> (~(X!1 = tptp_fun_W_3(Z!2)))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[80])).
% 2.85/3.10 tff(82,plain,
% 2.85/3.10 (~(X!1 = Y!0)),
% 2.85/3.10 inference(and_elim,[status(thm)],[17])).
% 2.85/3.10 tff(83,plain,
% 2.85/3.10 (~(X!1 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[82, 81])).
% 2.85/3.10 tff(84,assumption,(~(tptp_fun_X_5(Y!0) = X!1)), introduced(assumption)).
% 2.85/3.10 tff(85,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_X_5(Y!0) = Y!0) | (tptp_fun_X_5(Y!0) = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_X_5(Y!0) = Y!0) | (tptp_fun_X_5(Y!0) = X!1))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(86,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_X_5(Y!0) = Y!0) | (tptp_fun_X_5(Y!0) = X!1))),
% 2.85/3.10 inference(quant_inst,[status(thm)],[])).
% 2.85/3.10 tff(87,plain,
% 2.85/3.10 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_X_5(Y!0) = Y!0) | (tptp_fun_X_5(Y!0) = X!1)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[86, 85])).
% 2.85/3.10 tff(88,plain,
% 2.85/3.10 ((tptp_fun_X_5(Y!0) = Y!0) | (tptp_fun_X_5(Y!0) = X!1)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[87, 18])).
% 2.85/3.10 tff(89,plain,
% 2.85/3.10 (tptp_fun_X_5(Y!0) = Y!0),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[88, 84])).
% 2.85/3.10 tff(90,plain,
% 2.85/3.10 ((X!1 = W1!8) <=> (X!1 = Y!0)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[62])).
% 2.85/3.10 tff(91,plain,
% 2.85/3.10 ((X!1 = Y!0) <=> (X!1 = W1!8)),
% 2.85/3.10 inference(symmetry,[status(thm)],[90])).
% 2.85/3.10 tff(92,plain,
% 2.85/3.10 ((~(X!1 = Y!0)) <=> (~(X!1 = W1!8))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[91])).
% 2.85/3.10 tff(93,plain,
% 2.85/3.10 (~(X!1 = W1!8)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[82, 92])).
% 2.85/3.10 tff(94,assumption,(X!1 = W1!8), introduced(assumption)).
% 2.85/3.10 tff(95,plain,
% 2.85/3.10 ($false),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[94, 93])).
% 2.85/3.10 tff(96,plain,((~(W1!8 = Y!0)) | (~(X!1 = W1!8))), inference(lemma,lemma(discharge,[]))).
% 2.85/3.10 tff(97,plain,
% 2.85/3.10 (~(X!1 = W1!8)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[96, 62])).
% 2.85/3.10 tff(98,plain,
% 2.85/3.10 ((tptp_fun_X_5(Y!0) = Z!2) <=> (tptp_fun_X_5(Y!0) = X!1)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[25])).
% 2.85/3.10 tff(99,assumption,(tptp_fun_X_5(Y!0) = Z!2), introduced(assumption)).
% 2.85/3.10 tff(100,plain,
% 2.85/3.10 (tptp_fun_X_5(Y!0) = X!1),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[99, 98])).
% 2.85/3.10 tff(101,plain,
% 2.85/3.10 ($false),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[84, 100])).
% 2.85/3.10 tff(102,plain,((~(tptp_fun_X_5(Y!0) = Z!2)) | (tptp_fun_X_5(Y!0) = X!1) | (~(Z!2 = X!1))), inference(lemma,lemma(discharge,[]))).
% 2.85/3.10 tff(103,plain,
% 2.85/3.10 (~(tptp_fun_X_5(Y!0) = Z!2)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[102, 84, 25])).
% 2.85/3.10 tff(104,assumption,(~(tptp_fun_X_5(Y!0) = Z!2)), introduced(assumption)).
% 2.85/3.10 tff(105,assumption,(tptp_fun_X_5(Y!0) = Y!0), introduced(assumption)).
% 2.85/3.10 tff(106,plain,
% 2.85/3.10 (Y!0 = tptp_fun_X_5(Y!0)),
% 2.85/3.10 inference(symmetry,[status(thm)],[105])).
% 2.85/3.10 tff(107,plain,
% 2.85/3.10 (tptp_fun_Y_4(X!1, Y!0) = tptp_fun_Y_4(X!1, tptp_fun_X_5(Y!0))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[106])).
% 2.85/3.10 tff(108,assumption,(~big_f(tptp_fun_X_5(Y!0), X!1)), introduced(assumption)).
% 2.85/3.10 tff(109,plain,
% 2.85/3.10 ((Z!2 = tptp_fun_Z1_12(Y!0)) <=> (tptp_fun_Z1_12(Y!0) = Z!2)),
% 2.85/3.10 inference(commutativity,[status(thm)],[])).
% 2.85/3.10 tff(110,plain,
% 2.85/3.10 ((tptp_fun_Z1_12(Y!0) = Z!2) <=> (Z!2 = tptp_fun_Z1_12(Y!0))),
% 2.85/3.10 inference(symmetry,[status(thm)],[109])).
% 2.85/3.10 tff(111,plain,
% 2.85/3.10 ((tptp_fun_Z1_12(Y!0) = X!1) <=> (tptp_fun_Z1_12(Y!0) = Z!2)),
% 2.85/3.10 inference(monotonicity,[status(thm)],[35])).
% 2.85/3.10 tff(112,plain,
% 2.85/3.10 ((tptp_fun_Z1_12(Y!0) = X!1) <=> (Z!2 = tptp_fun_Z1_12(Y!0))),
% 2.85/3.10 inference(transitivity,[status(thm)],[111, 110])).
% 2.85/3.10 tff(113,assumption,(~big_f(W1!8, W1!8)), introduced(assumption)).
% 2.85/3.10 tff(114,assumption,(tptp_fun_Y1_11(Y!0) = Y!0), introduced(assumption)).
% 2.85/3.10 tff(115,plain,
% 2.85/3.10 (tptp_fun_Y1_11(Y!0) = W1!8),
% 2.85/3.10 inference(transitivity,[status(thm)],[114, 63])).
% 2.85/3.10 tff(116,plain,
% 2.85/3.10 ((~big_f(W1!8, W1!8)) <=> (~big_f(Y!0, W1!8))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[65])).
% 2.85/3.10 tff(117,plain,
% 2.85/3.10 (~big_f(Y!0, W1!8)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[113, 116])).
% 2.85/3.10 tff(118,assumption,(![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))), introduced(assumption)).
% 2.85/3.10 tff(119,plain,
% 2.85/3.10 ((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | (big_f(Z!2, X!1) <=> (X!1 = tptp_fun_W_3(Z!2)))),
% 2.85/3.10 inference(quant_inst,[status(thm)],[])).
% 2.85/3.10 tff(120,plain,
% 2.85/3.10 (big_f(Z!2, X!1) <=> (X!1 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[119, 118])).
% 2.85/3.10 tff(121,plain,
% 2.85/3.10 ((~(big_f(Z!2, X!1) <=> (X!1 = tptp_fun_W_3(Z!2)))) | big_f(Z!2, X!1) | (~(X!1 = tptp_fun_W_3(Z!2)))),
% 2.85/3.10 inference(tautology,[status(thm)],[])).
% 2.85/3.10 tff(122,plain,
% 2.85/3.10 (~(X!1 = tptp_fun_W_3(Z!2))),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[121, 120, 57])).
% 2.85/3.10 tff(123,assumption,(tptp_fun_W_3(Z!2) = X!1), introduced(assumption)).
% 2.85/3.10 tff(124,plain,
% 2.85/3.10 (X!1 = tptp_fun_W_3(Z!2)),
% 2.85/3.10 inference(modus_ponens,[status(thm)],[123, 1])).
% 2.85/3.10 tff(125,assumption,(~(X!1 = tptp_fun_W_3(Z!2))), introduced(assumption)).
% 2.85/3.10 tff(126,plain,
% 2.85/3.10 ($false),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[125, 124])).
% 2.85/3.10 tff(127,plain,((~(tptp_fun_W_3(Z!2) = X!1)) | (X!1 = tptp_fun_W_3(Z!2))), inference(lemma,lemma(discharge,[]))).
% 2.85/3.10 tff(128,plain,
% 2.85/3.10 (~(tptp_fun_W_3(Z!2) = X!1)),
% 2.85/3.10 inference(unit_resolution,[status(thm)],[127, 122])).
% 2.85/3.10 tff(129,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(130,plain,
% 2.85/3.10 (((tptp_fun_W_3(Z!2) = Y!0) | (tptp_fun_W_3(Z!2) = X!1)) <=> ((tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0))),
% 2.85/3.10 inference(rewrite,[status(thm)],[])).
% 2.85/3.10 tff(131,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_W_3(Z!2) = Y!0) | (tptp_fun_W_3(Z!2) = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0)))),
% 2.85/3.10 inference(monotonicity,[status(thm)],[130])).
% 2.85/3.10 tff(132,plain,
% 2.85/3.10 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_W_3(Z!2) = Y!0) | (tptp_fun_W_3(Z!2) = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0))),
% 2.85/3.11 inference(transitivity,[status(thm)],[131, 129])).
% 2.85/3.11 tff(133,plain,
% 2.85/3.11 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_W_3(Z!2) = Y!0) | (tptp_fun_W_3(Z!2) = X!1))),
% 2.85/3.11 inference(quant_inst,[status(thm)],[])).
% 2.85/3.11 tff(134,plain,
% 2.85/3.11 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0)),
% 2.85/3.11 inference(modus_ponens,[status(thm)],[133, 132])).
% 2.85/3.11 tff(135,plain,
% 2.85/3.11 ((tptp_fun_W_3(Z!2) = X!1) | (tptp_fun_W_3(Z!2) = Y!0)),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[134, 18])).
% 2.85/3.11 tff(136,plain,
% 2.85/3.11 (tptp_fun_W_3(Z!2) = Y!0),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[135, 128])).
% 2.85/3.11 tff(137,plain,
% 2.85/3.11 (tptp_fun_W_3(Z!2) = W1!8),
% 2.85/3.11 inference(transitivity,[status(thm)],[136, 63])).
% 2.85/3.11 tff(138,plain,
% 2.85/3.11 (big_f(Z!2, tptp_fun_W_3(Z!2)) <=> big_f(X!1, W1!8)),
% 2.85/3.11 inference(monotonicity,[status(thm)],[25, 137])).
% 2.85/3.11 tff(139,plain,
% 2.85/3.11 (big_f(X!1, W1!8) <=> big_f(Z!2, tptp_fun_W_3(Z!2))),
% 2.85/3.11 inference(symmetry,[status(thm)],[138])).
% 2.85/3.11 tff(140,plain,
% 2.85/3.11 ((~big_f(X!1, W1!8)) <=> (~big_f(Z!2, tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(monotonicity,[status(thm)],[139])).
% 2.85/3.11 tff(141,plain,
% 2.85/3.11 (~big_f(Z!2, tptp_fun_W_3(Z!2))),
% 2.85/3.11 inference(modus_ponens,[status(thm)],[43, 140])).
% 2.85/3.11 tff(142,plain,
% 2.85/3.11 (((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | big_f(Z!2, tptp_fun_W_3(Z!2))) <=> ((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | big_f(Z!2, tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(143,plain,
% 2.85/3.11 ((big_f(Z!2, tptp_fun_W_3(Z!2)) <=> $true) <=> big_f(Z!2, tptp_fun_W_3(Z!2))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(144,plain,
% 2.85/3.11 ((tptp_fun_W_3(Z!2) = tptp_fun_W_3(Z!2)) <=> $true),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(145,plain,
% 2.85/3.11 ((big_f(Z!2, tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = tptp_fun_W_3(Z!2))) <=> (big_f(Z!2, tptp_fun_W_3(Z!2)) <=> $true)),
% 2.85/3.11 inference(monotonicity,[status(thm)],[144])).
% 2.85/3.11 tff(146,plain,
% 2.85/3.11 ((big_f(Z!2, tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = tptp_fun_W_3(Z!2))) <=> big_f(Z!2, tptp_fun_W_3(Z!2))),
% 2.85/3.11 inference(transitivity,[status(thm)],[145, 143])).
% 2.85/3.11 tff(147,plain,
% 2.85/3.11 (((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | (big_f(Z!2, tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = tptp_fun_W_3(Z!2)))) <=> ((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | big_f(Z!2, tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(monotonicity,[status(thm)],[146])).
% 2.85/3.11 tff(148,plain,
% 2.85/3.11 (((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | (big_f(Z!2, tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = tptp_fun_W_3(Z!2)))) <=> ((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | big_f(Z!2, tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(transitivity,[status(thm)],[147, 142])).
% 2.85/3.11 tff(149,plain,
% 2.85/3.11 ((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | (big_f(Z!2, tptp_fun_W_3(Z!2)) <=> (tptp_fun_W_3(Z!2) = tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(quant_inst,[status(thm)],[])).
% 2.85/3.11 tff(150,plain,
% 2.85/3.11 ((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | big_f(Z!2, tptp_fun_W_3(Z!2))),
% 2.85/3.11 inference(modus_ponens,[status(thm)],[149, 148])).
% 2.85/3.11 tff(151,plain,
% 2.85/3.11 (big_f(Z!2, tptp_fun_W_3(Z!2))),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[150, 118])).
% 2.85/3.11 tff(152,plain,
% 2.85/3.11 ($false),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[151, 141])).
% 2.85/3.11 tff(153,plain,((~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) | big_f(X!1, W1!8) | (~(W1!8 = Y!0)) | (~(Z!2 = X!1)) | big_f(Z!2, X!1)), inference(lemma,lemma(discharge,[]))).
% 2.85/3.11 tff(154,plain,
% 2.85/3.11 (~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[153, 43, 25, 62, 57])).
% 2.85/3.11 tff(155,plain,
% 2.85/3.11 (((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))) <=> ((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(156,plain,
% 2.85/3.11 ((~(~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))) <=> ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(157,plain,
% 2.85/3.11 (($false | (~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))) <=> (~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(158,plain,
% 2.85/3.11 ((~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))) <=> (~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(159,plain,
% 2.85/3.11 ((~$true) <=> $false),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(160,plain,
% 2.85/3.11 (($true | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W)))) <=> $true),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(161,plain,
% 2.85/3.11 ((Z!2 = Z!2) <=> $true),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(162,plain,
% 2.85/3.11 (((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W)))) <=> ($true | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))),
% 2.85/3.11 inference(monotonicity,[status(thm)],[161])).
% 2.85/3.11 tff(163,plain,
% 2.85/3.11 (((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W)))) <=> $true),
% 2.85/3.11 inference(transitivity,[status(thm)],[162, 160])).
% 2.85/3.11 tff(164,plain,
% 2.85/3.11 ((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) <=> (~$true)),
% 2.85/3.11 inference(monotonicity,[status(thm)],[163])).
% 2.85/3.11 tff(165,plain,
% 2.85/3.11 ((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) <=> $false),
% 2.85/3.11 inference(transitivity,[status(thm)],[164, 159])).
% 2.85/3.11 tff(166,plain,
% 2.85/3.11 (((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))) <=> ($false | (~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))),
% 2.85/3.11 inference(monotonicity,[status(thm)],[165, 158])).
% 2.85/3.11 tff(167,plain,
% 2.85/3.11 (((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))) <=> (~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))),
% 2.85/3.11 inference(transitivity,[status(thm)],[166, 157])).
% 2.85/3.11 tff(168,plain,
% 2.85/3.11 ((~((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))))) <=> (~(~![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))),
% 2.85/3.11 inference(monotonicity,[status(thm)],[167])).
% 2.85/3.11 tff(169,plain,
% 2.85/3.11 ((~((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))))) <=> ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(transitivity,[status(thm)],[168, 156])).
% 2.85/3.11 tff(170,plain,
% 2.85/3.11 (((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | (~((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))))) <=> ((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))),
% 2.85/3.11 inference(monotonicity,[status(thm)],[169])).
% 2.85/3.11 tff(171,plain,
% 2.85/3.11 (((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | (~((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))))) <=> ((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2))))),
% 2.85/3.11 inference(transitivity,[status(thm)],[170, 155])).
% 2.85/3.11 tff(172,plain,
% 2.85/3.11 ((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | (~((~((Z!2 = Z!2) | ![W: $i] : (~(big_f(Z!2, tptp_fun_Y_4(W, Z!2)) <=> (tptp_fun_Y_4(W, Z!2) = W))))) | (~((~(Z!2 = Z!2)) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))))))),
% 2.85/3.11 inference(quant_inst,[status(thm)],[])).
% 2.85/3.11 tff(173,plain,
% 2.85/3.11 ((~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))) | ![Y: $i] : (big_f(Z!2, Y) <=> (Y = tptp_fun_W_3(Z!2)))),
% 2.85/3.11 inference(modus_ponens,[status(thm)],[172, 171])).
% 2.85/3.11 tff(174,plain,
% 2.85/3.11 (~![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X)))))))),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[173, 154])).
% 2.85/3.11 tff(175,assumption,(~big_f(Y!0, W1!8)), introduced(assumption)).
% 2.85/3.11 tff(176,plain,
% 2.85/3.11 ((Y!0 = tptp_fun_Z1_9(W1!8)) <=> (tptp_fun_Z1_9(W1!8) = Y!0)),
% 2.85/3.11 inference(commutativity,[status(thm)],[])).
% 2.85/3.11 tff(177,plain,
% 2.85/3.11 ((tptp_fun_Z1_9(W1!8) = Y!0) <=> (Y!0 = tptp_fun_Z1_9(W1!8))),
% 2.85/3.11 inference(symmetry,[status(thm)],[176])).
% 2.85/3.11 tff(178,assumption,(![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))), introduced(assumption)).
% 2.85/3.11 tff(179,plain,
% 2.85/3.11 ((~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))) | (big_f(X!1, W1!8) <=> (X!1 = tptp_fun_Z1_9(W1!8)))),
% 2.85/3.11 inference(quant_inst,[status(thm)],[])).
% 2.85/3.11 tff(180,plain,
% 2.85/3.11 (big_f(X!1, W1!8) <=> (X!1 = tptp_fun_Z1_9(W1!8))),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[179, 178])).
% 2.85/3.11 tff(181,plain,
% 2.85/3.11 ((~(big_f(X!1, W1!8) <=> (X!1 = tptp_fun_Z1_9(W1!8)))) | big_f(X!1, W1!8) | (~(X!1 = tptp_fun_Z1_9(W1!8)))),
% 2.85/3.11 inference(tautology,[status(thm)],[])).
% 2.85/3.11 tff(182,plain,
% 2.85/3.11 (~(X!1 = tptp_fun_Z1_9(W1!8))),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[181, 180, 43])).
% 2.85/3.11 tff(183,plain,
% 2.85/3.11 ((X!1 = tptp_fun_Z1_9(W1!8)) <=> (tptp_fun_Z1_9(W1!8) = X!1)),
% 2.85/3.11 inference(commutativity,[status(thm)],[])).
% 2.85/3.11 tff(184,plain,
% 2.85/3.11 ((tptp_fun_Z1_9(W1!8) = X!1) <=> (X!1 = tptp_fun_Z1_9(W1!8))),
% 2.85/3.11 inference(symmetry,[status(thm)],[183])).
% 2.85/3.11 tff(185,assumption,(tptp_fun_Z1_9(W1!8) = X!1), introduced(assumption)).
% 2.85/3.11 tff(186,plain,
% 2.85/3.11 (X!1 = tptp_fun_Z1_9(W1!8)),
% 2.85/3.11 inference(modus_ponens,[status(thm)],[185, 184])).
% 2.85/3.11 tff(187,assumption,(~(X!1 = tptp_fun_Z1_9(W1!8))), introduced(assumption)).
% 2.85/3.11 tff(188,plain,
% 2.85/3.11 ($false),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[187, 186])).
% 2.85/3.11 tff(189,plain,((~(tptp_fun_Z1_9(W1!8) = X!1)) | (X!1 = tptp_fun_Z1_9(W1!8))), inference(lemma,lemma(discharge,[]))).
% 2.85/3.11 tff(190,plain,
% 2.85/3.11 (~(tptp_fun_Z1_9(W1!8) = X!1)),
% 2.85/3.11 inference(unit_resolution,[status(thm)],[189, 182])).
% 2.85/3.11 tff(191,plain,
% 2.85/3.11 (((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_9(W1!8) = Y!0) | (tptp_fun_Z1_9(W1!8) = X!1))) <=> ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_Z1_9(W1!8) = Y!0) | (tptp_fun_Z1_9(W1!8) = X!1))),
% 2.85/3.11 inference(rewrite,[status(thm)],[])).
% 2.85/3.11 tff(192,plain,
% 2.85/3.11 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | ((tptp_fun_Z1_9(W1!8) = Y!0) | (tptp_fun_Z1_9(W1!8) = X!1))),
% 2.85/3.11 inference(quant_inst,[status(thm)],[])).
% 2.85/3.11 tff(193,plain,
% 2.85/3.11 ((~![Z: $i] : ((Z = Y!0) | (Z = X!1))) | (tptp_fun_Z1_9(W1!8) = Y!0) | (tptp_fun_Z1_9(W1!8) = X!1)),
% 2.85/3.11 inference(modus_ponens,[status(thm)],[192, 191])).
% 2.85/3.11 tff(194,plain,
% 2.85/3.11 ((tptp_fun_Z1_9(W1!8) = Y!0) | (tptp_fun_Z1_9(W1!8) = X!1)),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[193, 18])).
% 2.95/3.11 tff(195,plain,
% 2.95/3.11 (tptp_fun_Z1_9(W1!8) = Y!0),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[194, 190])).
% 2.95/3.11 tff(196,plain,
% 2.95/3.11 (Y!0 = tptp_fun_Z1_9(W1!8)),
% 2.95/3.11 inference(modus_ponens,[status(thm)],[195, 177])).
% 2.95/3.11 tff(197,plain,
% 2.95/3.11 ((~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))) | (big_f(Y!0, W1!8) <=> (Y!0 = tptp_fun_Z1_9(W1!8)))),
% 2.95/3.11 inference(quant_inst,[status(thm)],[])).
% 2.95/3.11 tff(198,plain,
% 2.95/3.11 (big_f(Y!0, W1!8) <=> (Y!0 = tptp_fun_Z1_9(W1!8))),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[197, 178])).
% 2.95/3.11 tff(199,plain,
% 2.95/3.11 ((~(big_f(Y!0, W1!8) <=> (Y!0 = tptp_fun_Z1_9(W1!8)))) | big_f(Y!0, W1!8) | (~(Y!0 = tptp_fun_Z1_9(W1!8)))),
% 2.95/3.11 inference(tautology,[status(thm)],[])).
% 2.95/3.11 tff(200,plain,
% 2.95/3.11 (~(Y!0 = tptp_fun_Z1_9(W1!8))),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[199, 198, 175])).
% 2.95/3.11 tff(201,plain,
% 2.95/3.11 ($false),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[200, 196])).
% 2.95/3.11 tff(202,plain,((~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))) | big_f(Y!0, W1!8) | big_f(X!1, W1!8)), inference(lemma,lemma(discharge,[]))).
% 2.95/3.11 tff(203,plain,
% 2.95/3.11 (~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[202, 43, 175])).
% 2.95/3.11 tff(204,plain,
% 2.95/3.11 (((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))) <=> ((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(205,plain,
% 2.95/3.11 ((~(~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))) <=> ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(206,plain,
% 2.95/3.11 (($false | (~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))) <=> (~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(207,plain,
% 2.95/3.11 ((~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))) <=> (~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(208,plain,
% 2.95/3.11 (($true | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1)))) <=> $true),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(209,plain,
% 2.95/3.11 ((W1!8 = W1!8) <=> $true),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(210,plain,
% 2.95/3.11 (((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1)))) <=> ($true | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))),
% 2.95/3.11 inference(monotonicity,[status(thm)],[209])).
% 2.95/3.11 tff(211,plain,
% 2.95/3.11 (((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1)))) <=> $true),
% 2.95/3.11 inference(transitivity,[status(thm)],[210, 208])).
% 2.95/3.11 tff(212,plain,
% 2.95/3.11 ((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) <=> (~$true)),
% 2.95/3.11 inference(monotonicity,[status(thm)],[211])).
% 2.95/3.11 tff(213,plain,
% 2.95/3.11 ((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) <=> $false),
% 2.95/3.11 inference(transitivity,[status(thm)],[212, 159])).
% 2.95/3.11 tff(214,plain,
% 2.95/3.11 (((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))) <=> ($false | (~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))),
% 2.95/3.11 inference(monotonicity,[status(thm)],[213, 207])).
% 2.95/3.11 tff(215,plain,
% 2.95/3.11 (((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))) <=> (~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))),
% 2.95/3.11 inference(transitivity,[status(thm)],[214, 206])).
% 2.95/3.11 tff(216,plain,
% 2.95/3.11 ((~((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))))) <=> (~(~![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))),
% 2.95/3.11 inference(monotonicity,[status(thm)],[215])).
% 2.95/3.11 tff(217,plain,
% 2.95/3.11 ((~((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))))) <=> ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))),
% 2.95/3.11 inference(transitivity,[status(thm)],[216, 205])).
% 2.95/3.11 tff(218,plain,
% 2.95/3.11 (((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | (~((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))))) <=> ((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))),
% 2.95/3.11 inference(monotonicity,[status(thm)],[217])).
% 2.95/3.11 tff(219,plain,
% 2.95/3.11 (((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | (~((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))))) <=> ((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8))))),
% 2.95/3.11 inference(transitivity,[status(thm)],[218, 204])).
% 2.95/3.11 tff(220,plain,
% 2.95/3.11 ((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | (~((~((W1!8 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, W1!8), W1!8) <=> (tptp_fun_X1_10(Z1, W1!8) = Z1))))) | (~((~(W1!8 = W1!8)) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))))))),
% 2.95/3.11 inference(quant_inst,[status(thm)],[])).
% 2.95/3.11 tff(221,plain,
% 2.95/3.11 ((~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))) | ![X1: $i] : (big_f(X1, W1!8) <=> (X1 = tptp_fun_Z1_9(W1!8)))),
% 2.95/3.11 inference(modus_ponens,[status(thm)],[220, 219])).
% 2.95/3.11 tff(222,plain,
% 2.95/3.11 (~![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1)))))))),
% 2.95/3.11 inference(unit_resolution,[status(thm)],[221, 203])).
% 2.95/3.11 tff(223,plain,
% 2.95/3.11 ((![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~(![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))))) | ![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~(![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8))))))) <=> (![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~((~(X = Z!2)) | ![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))))))) | ![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~((~(Y1 = W1!8)) | ![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))))))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(224,plain,
% 2.95/3.11 ((![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~(![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))))) | ![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~(![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8))))))) <=> (![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~(![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))))) | ![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~(![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8)))))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(225,plain,
% 2.95/3.11 ((![X: $i] : (((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W)))) & (![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))) | ![Y1: $i] : (((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1)))) & (![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8))))) <=> (![X: $i] : (~((~((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))))) | (~(![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))))) | ![Y1: $i] : (~((~((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))))) | (~(![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8)))))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(226,plain,
% 2.95/3.11 (((![X: $i] : ((![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W))) | (X = Z!2)) & (![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))) | ![Y1: $i] : ((![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1))) | (Y1 = W1!8)) & (![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8))))) & (![Z: $i] : ((![Y: $i] : (big_f(tptp_fun_X_5(Z), Y) <=> (Y = tptp_fun_W_6(Z))) | (tptp_fun_X_5(Z) = Z)) & (![W: $i] : (~(big_f(tptp_fun_X_5(Z), tptp_fun_Y_7(W, Z)) <=> (tptp_fun_Y_7(W, Z) = W))) | (~(tptp_fun_X_5(Z) = Z)))) | ![W1: $i] : ((![X1: $i] : (big_f(X1, tptp_fun_Y1_11(W1)) <=> (X1 = tptp_fun_Z1_12(W1))) | (tptp_fun_Y1_11(W1) = W1)) & (![Z1: $i] : (~(big_f(tptp_fun_X1_13(Z1, W1), tptp_fun_Y1_11(W1)) <=> (tptp_fun_X1_13(Z1, W1) = Z1))) | (~(tptp_fun_Y1_11(W1) = W1)))))) <=> ((![X: $i] : (((X = Z!2) | ![W: $i] : (~(big_f(X, tptp_fun_Y_4(W, X)) <=> (tptp_fun_Y_4(W, X) = W)))) & (![Y: $i] : (big_f(X, Y) <=> (Y = tptp_fun_W_3(X))) | (~(X = Z!2)))) | ![Y1: $i] : (((Y1 = W1!8) | ![Z1: $i] : (~(big_f(tptp_fun_X1_10(Z1, Y1), Y1) <=> (tptp_fun_X1_10(Z1, Y1) = Z1)))) & (![X1: $i] : (big_f(X1, Y1) <=> (X1 = tptp_fun_Z1_9(Y1))) | (~(Y1 = W1!8))))) & (![Z: $i] : (((tptp_fun_X_5(Z) = Z) | ![Y: $i] : (big_f(tptp_fun_X_5(Z), Y) <=> (Y = tptp_fun_W_6(Z)))) & (![W: $i] : (~(big_f(tptp_fun_X_5(Z), tptp_fun_Y_7(W, Z)) <=> (tptp_fun_Y_7(W, Z) = W))) | (~(tptp_fun_X_5(Z) = Z)))) | ![W1: $i] : (((tptp_fun_Y1_11(W1) = W1) | ![X1: $i] : (big_f(X1, tptp_fun_Y1_11(W1)) <=> (X1 = tptp_fun_Z1_12(W1)))) & (![Z1: $i] : (~(big_f(tptp_fun_X1_13(Z1, W1), tptp_fun_Y1_11(W1)) <=> (tptp_fun_X1_13(Z1, W1) = Z1))) | (~(tptp_fun_Y1_11(W1) = W1))))))),
% 2.95/3.11 inference(rewrite,[status(thm)],[])).
% 2.95/3.11 tff(227,plain,
% 2.95/3.11 ((~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))) <=> (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1))))),
% 2.95/3.13 inference(rewrite,[status(thm)],[])).
% 2.95/3.13 tff(228,plain,
% 2.95/3.13 ((?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1))) <=> (?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))),
% 2.95/3.13 inference(rewrite,[status(thm)],[])).
% 2.95/3.13 tff(229,plain,
% 2.95/3.13 ((~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))) <=> (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1))))),
% 2.95/3.13 inference(monotonicity,[status(thm)],[228])).
% 2.95/3.13 tff(230,plain,
% 2.95/3.13 ((~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))) <=> (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1))))),
% 2.95/3.13 inference(transitivity,[status(thm)],[229, 227])).
% 2.95/3.13 tff(231,axiom,(~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','pel53')).
% 2.95/3.13 tff(232,plain,
% 2.95/3.13 (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))),
% 2.95/3.13 inference(modus_ponens,[status(thm)],[231, 230])).
% 2.95/3.13 tff(233,plain,
% 2.95/3.13 (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))),
% 2.95/3.13 inference(modus_ponens,[status(thm)],[232, 230])).
% 2.95/3.13 tff(234,plain,
% 2.95/3.13 (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))),
% 2.95/3.13 inference(modus_ponens,[status(thm)],[233, 227])).
% 2.95/3.13 tff(235,plain,
% 2.95/3.13 (~(?[Z: $i] : ![X: $i] : (?[W: $i] : ![Y: $i] : (big_f(X, Y) <=> (Y = W)) <=> (X = Z)) <=> ?[W1: $i] : ![Y1: $i] : (?[Z1: $i] : ![X1: $i] : (big_f(X1, Y1) <=> (X1 = Z1)) <=> (Y1 = W1)))),
% 2.95/3.13 inference(modus_ponens,[status(thm)],[234, 230])).
% 2.95/3.13 unexpected number of arguments: (let ((a!1 (exists ((Z $i))
% 2.95/3.13 (forall ((X $i))
% 2.95/3.13 (let ((a!1 (exists ((W $i))
% 2.95/3.13 (forall ((Y $i)) (= (big_f X Y) (= Y W))))))
% 2.95/3.13 (= a!1 (= X Z))))))
% 2.95/3.13 (a!2 (forall ((X $i))
% 2.95/3.13 (let ((a!1 (exists ((W $i))
% 2.95/3.13 (forall ((Y $i)) (= (big_f X Y) (= Y W))))))
% 2.95/3.13 (= a!1 (= X Z!2)))))
% 2.95/3.13 (a!3 (lambda ((X $i))
% 2.95/3.13 (let ((a!1 (exists ((W $i))
% 2.95/3.13 (forall ((Y $i)) (= (big_f X Y) (= Y W)))))
% 2.95/3.13 (a!2 (forall ((Y $i)) (= (big_f X Y) (= Y (W!3 X)))))
% 2.95/3.13 (a!4 (lambda ((W $i))
% 2.95/3.13 (let ((a!1 (forall ((Y $i)) (= (big_f X Y) (= Y W))))
% 2.95/3.13 (a!2 (not (= (big_f X (Y!4 W X))
% 2.95/3.13 (= (Y!4 W X) W)))))
% 2.95/3.13 (sk (~ (not a!1) a!2)))))
% 2.95/3.13 (a!5 (forall ((W $i))
% 2.95/3.13 (not (= (big_f X (Y!4 W X)) (= (Y!4 W X) W)))))
% 2.95/3.13 (a!6 (refl (~ (not (= X Z!2)) (not (= X Z!2))))))
% 2.95/3.13 (let ((a!3 (nnf-pos (proof-bind (lambda ((Y $i))
% 2.95/3.13 (let ((a!1 (~ (= (big_f X Y)
% 2.95/3.13 (= Y (W!3 X)))
% 2.95/3.13 (= (big_f X Y)
% 2.95/3.13 (= Y (W!3 X))))))
% 2.95/3.13 (refl a!1))))
% 2.95/3.13 (~ a!2 a!2)))
% 2.95/3.13 (a!7 (and (or a!5 (= X Z!2)) (or a!2 (not (= X Z!2))))))
% 2.95/3.13 (nnf-pos (trans (sk (~ a!1 a!2)) a!3 (~ a!1 a!2))
% 2.95/3.13 (nnf-neg (proof-bind a!4) (~ (not a!1) a!5))
% 2.95/3.13 (refl (~ (= X Z!2) (= X Z!2)))
% 2.95/3.13 a!6
% 2.95/3.13 (~ (= a!1 (= X Z!2)) a!7))))))
% 2.95/3.13 (a!4 (forall ((X $i))
% 2.95/3.13 (let ((a!1 (forall ((W $i))
% 2.95/3.13 (not (= (big_f X (Y!4 W X)) (= (Y!4 W X) W)))))
% 2.95/3.13 (a!2 (forall ((Y $i)) (= (big_f X Y) (= Y (W!3 X))))))
% 2.95/3.13 (and (or a!1 (= X Z!2)) (or a!2 (not (= X Z!2)))))))
% 2.95/3.13 (a!5 (lambda ((Z $i))
% 2.95/3.13 (let ((a!1 (forall ((X $i))
% 2.95/3.13 (let ((a!1 (exists ((W $i))
% 2.95/3.13 (forall ((Y $i)) (= (big_f X Y) (= Y W))))))
% 2.95/3.13 (= a!1 (= X Z)))))
% 2.95/3.13 (a!2 (exists ((W $i))
% 2.95/3.13 (forall ((Y $i)) (= (big_f (X!5 Z) Y) (= Y W)))))
% 2.95/3.13 (a!4 (forall ((Y $i)) (= (big_f (X!5 Z) Y) (= Y (W!6 Z)))))
% 2.95/3.13 (a!6 (lambda ((W $i))
% 2.95/3.13 (let ((a!1 (forall ((Y $i))
% 2.95/3.13 (= (big_f (X!5 Z) Y) (= Y W))))
% 2.95/3.13 (a!2 (not (= (big_f (X!5 Z) (Y!7 W Z))
% 2.95/3.13 (= (Y!7 W Z) W)))))
% 2.95/3.13 (sk (~ (not a!1) a!2)))))
% 2.95/3.13 (a!7 (forall ((W $i))
% 2.95/3.13 (not (= (big_f (X!5 Z) (Y!7 W Z)) (= (Y!7 W Z) W)))))
% 2.95/3.13 (a!8 (refl (~ (= (X!5 Z) Z) (= (X!5 Z) Z))))
% 2.95/3.13 (a!9 (~ (not (= (X!5 Z) Z)) (not (= (X!5 Z) Z)))))
% 2.95/3.13 (let ((a!3 (not (= a!2 (= (X!5 Z) Z))))
% 2.95/3.13 (a!5 (nnf-pos (proof-bind (lambda ((Y $i))
% 2.95/3.13 (let ((a!1 (~ (= (big_f (X!5 Z)
% 2.95/3.13 Y)
% 2.95/3.13 (= Y (W!6 Z)))
% 2.95/3.13 (= (big_f (X!5 Z)
% 2.95/3.13 Y)
% 2.95/3.13 (= Y (W!6 Z))))))
% 2.95/3.13 (refl a!1))))
% 2.95/3.13 (~ a!4 a!4)))
% 2.95/3.13 (a!10 (or a!7 (not (= (X!5 Z) Z)))))
% 2.95/3.13 (let ((a!11 (and (or a!4 (= (X!5 Z) Z)) a!10)))
% 2.95/3.13 (let ((a!12 (nnf-neg (trans (sk (~ a!2 a!4)) a!5 (~ a!2 a!4))
% 2.95/3.13 (nnf-neg (proof-bind a!6) (~ (not a!2) a!7))
% 2.95/3.13 a!8
% 2.95/3.13 (refl a!9)
% 2.95/3.13 (~ a!3 a!11))))
% 2.95/3.13 (trans (sk (~ (not a!1) a!3)) a!12 (~ (not a!1) a!11))))))))
% 2.95/3.13 (a!6 (forall ((Z $i))
% 2.95/3.13 (let ((a!1 (forall ((Y $i)) (= (big_f (X!5 Z) Y) (= Y (W!6 Z)))))
% 2.95/3.13 (a!2 (forall ((W $i))
% 2.95/3.13 (not (= (big_f (X!5 Z) (Y!7 W Z)) (= (Y!7 W Z) W))))))
% 2.95/3.13 (let ((a!3 (or a!2 (not (= (X!5 Z) Z)))))
% 2.95/3.13 (and (or a!1 (= (X!5 Z) Z)) a!3)))))
% 2.95/3.13 (a!7 (exists ((W1 $i))
% 2.95/3.13 (forall ((Y1 $i))
% 2.95/3.13 (let ((a!1 (exists ((Z1 $i))
% 2.95/3.13 (forall ((X1 $i)) (= (big_f X1 Y1) (= X1 Z1))))))
% 2.95/3.13 (= a!1 (= Y1 W1))))))
% 2.95/3.13 (a!8 (forall ((Y1 $i))
% 2.95/3.13 (let ((a!1 (exists ((Z1 $i))
% 2.95/3.13 (forall ((X1 $i)) (= (big_f X1 Y1) (= X1 Z1))))))
% 2.95/3.13 (= a!1 (= Y1 W1!8)))))
% 2.95/3.13 (a!9 (lambda ((Y1 $i))
% 2.95/3.13 (let ((a!1 (exists ((Z1 $i))
% 2.95/3.13 (forall ((X1 $i)) (= (big_f X1 Y1) (= X1 Z1)))))
% 2.95/3.13 (a!2 (forall ((X1 $i)) (= (big_f X1 Y1) (= X1 (Z1!9 Y1)))))
% 2.95/3.13 (a!4 (lambda ((Z1 $i))
% 2.95/3.13 (let ((a!1 (forall ((X1 $i))
% 2.95/3.13 (= (big_f X1 Y1) (= X1 Z1))))
% 2.95/3.13 (a!2 (not (= (big_f (X1!10 Z1 Y1) Y1)
% 2.95/3.13 (= (X1!10 Z1 Y1) Z1)))))
% 2.95/3.13 (sk (~ (not a!1) a!2)))))
% 2.95/3.13 (a!5 (forall ((Z1 $i))
% 2.95/3.13 (not (= (big_f (X1!10 Z1 Y1) Y1) (= (X1!10 Z1 Y1) Z1)))))
% 2.95/3.13 (a!6 (refl (~ (not (= Y1 W1!8)) (not (= Y1 W1!8))))))
% 2.95/3.13 (let ((a!3 (nnf-pos (proof-bind (lambda ((X1 $i))
% 2.95/3.13 (let ((a!1 (~ (= (big_f X1 Y1)
% 2.95/3.13 (= X1 (Z1!9 Y1)))
% 2.95/3.13 (= (big_f X1 Y1)
% 2.95/3.13 (= X1 (Z1!9 Y1))))))
% 2.95/3.13 (refl a!1))))
% 2.95/3.13 (~ a!2 a!2)))
% 2.95/3.13 (a!7 (and (or a!5 (= Y1 W1!8)) (or a!2 (not (= Y1 W1!8))))))
% 2.95/3.13 (nnf-pos (trans (sk (~ a!1 a!2)) a!3 (~ a!1 a!2))
% 2.95/3.13 (nnf-neg (proof-bind a!4) (~ (not a!1) a!5))
% 2.95/3.13 (refl (~ (= Y1 W1!8) (= Y1 W1!8)))
% 2.95/3.13 a!6
% 2.95/3.13 (~ (= a!1 (= Y1 W1!8)) a!7))))))
% 2.95/3.13 (a!10 (forall ((Y1 $i))
% 2.95/3.13 (let ((a!1 (forall ((Z1 $i))
% 2.95/3.13 (not (= (big_f (X1!10 Z1 Y1) Y1)
% 2.95/3.13 (= (X1!10 Z1 Y1) Z1)))))
% 2.95/3.13 (a!2 (forall ((X1 $i)) (= (big_f X1 Y1) (= X1 (Z1!9 Y1))))))
% 2.95/3.13 (and (or a!1 (= Y1 W1!8)) (or a!2 (not (= Y1 W1!8)))))))
% 2.95/3.13 (a!11 (lambda ((W1 $i))
% 2.95/3.13 (let ((a!1 (forall ((Y1 $i))
% 2.95/3.13 (let ((a!1 (exists ((Z1 $i))
% 2.95/3.13 (forall ((X1 $i))
% 2.95/3.13 (= (big_f X1 Y1) (= X1 Z1))))))
% 2.95/3.13 (= a!1 (= Y1 W1)))))
% 2.95/3.13 (a!2 (exists ((Z1 $i))
% 2.95/3.13 (forall ((X1 $i))
% 2.95/3.13 (= (big_f X1 (Y1!11 W1)) (= X1 Z1)))))
% 2.95/3.13 (a!4 (forall ((X1 $i))
% 2.95/3.13 (= (big_f X1 (Y1!11 W1)) (= X1 (Z1!12 W1)))))
% 2.95/3.13 (a!6 (lambda ((Z1 $i))
% 2.95/3.13 (let ((a!1 (forall ((X1 $i))
% 2.95/3.13 (= (big_f X1 (Y1!11 W1)) (= X1 Z1))))
% 2.95/3.13 (a!2 (not (= (big_f (X1!13 Z1 W1) (Y1!11 W1))
% 2.95/3.13 (= (X1!13 Z1 W1) Z1)))))
% 2.95/3.13 (sk (~ (not a!1) a!2)))))
% 2.95/3.13 (a!7 (forall ((Z1 $i))
% 2.95/3.13 (not (= (big_f (X1!13 Z1 W1) (Y1!11 W1))
% 2.95/3.13 (= (X1!13 Z1 W1) Z1)))))
% 2.95/3.13 (a!8 (refl (~ (= (Y1!11 W1) W1) (= (Y1!11 W1) W1))))
% 2.95/3.13 (a!9 (~ (not (= (Y1!11 W1) W1)) (not (= (Y1!11 W1) W1)))))
% 2.95/3.13 (let ((a!3 (not (= a!2 (= (Y1!11 W1) W1))))
% 2.95/3.13 (a!5 (nnf-pos (proof-bind (lambda ((X1 $i))
% 2.95/3.13 (let ((a!1 (~ (= (big_f X1
% 2.95/3.13 (Y1!11 W1))
% 2.95/3.13 (= X1
% 2.95/3.13 (Z1!12 W1)))
% 2.95/3.13 (= (big_f X1
% 2.95/3.13 (Y1!11 W1))
% 2.95/3.13 (= X1
% 2.95/3.13 (Z1!12 W1))))))
% 2.95/3.13 (refl a!1))))
% 2.95/3.13 (~ a!4 a!4)))
% 2.95/3.13 (a!10 (or a!7 (not (= (Y1!11 W1) W1)))))
% 2.95/3.13 (let ((a!11 (and (or a!4 (= (Y1!11 W1) W1)) a!10)))
% 2.95/3.13 (let ((a!12 (nnf-neg (trans (sk (~ a!2 a!4)) a!5 (~ a!2 a!4))
% 2.95/3.13 (nnf-neg (proof-bind a!6) (~ (not a!2) a!7))
% 2.95/3.13 a!8
% 2.95/3.13 (refl a!9)
% 2.95/3.13 (~ a!3 a!11))))
% 2.95/3.13 (trans (sk (~ (not a!1) a!3)) a!12 (~ (not a!1) a!11))))))))
% 2.95/3.13 (a!12 (forall ((W1 $i))
% 2.95/3.13 (let ((a!1 (forall ((X1 $i))
% 2.95/3.13 (= (big_f X1 (Y1!11 W1)) (= X1 (Z1!12 W1)))))
% 2.95/3.13 (a!2 (forall ((Z1 $i))
% 2.95/3.13 (not (= (big_f (X1!13 Z1 W1) (Y1!11 W1))
% 2.95/3.13 (= (X1!13 Z1 W1) Z1))))))
% 2.95/3.13 (let ((a!3 (or a!2 (not (= (Y1!11 W1) W1)))))
% 2.95/3.13 (and (or a!1 (= (Y1!11 W1) W1)) a!3))))))
% 2.95/3.13 (nnf-neg (trans (sk (~ a!1 a!2))
% 2.95/3.13 (nnf-pos (proof-bind a!3) (~ a!2 a!4))
% 2.95/3.13 (~ a!1 a!4))
% 2.95/3.13 (nnf-neg (proof-bind a!5) (~ (not a!1) a!6))
% 2.95/3.13 (trans (sk (~ a!7 a!8))
% 2.95/3.13 (nnf-pos (proof-bind a!9) (~ a!8 a!10))
% 2.95/3.13 (~ a!7 a!10))
% 2.95/3.13 (nnf-neg (proof-bind a!11) (~ (not a!7) a!12))
% 2.95/3.13 (~ (not (= a!1 a!7)) (and (or a!4 a!10) (or a!6 a!12)))))
% 2.95/3.13 Proof display could not be completed: unexpected number of arguments
% 2.95/3.14 % E exiting
%------------------------------------------------------------------------------