%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SEV567+1 : TPTP v9.1.0. Released v9.1.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n015.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:29:25 AM UTC 2025
% Result : Theorem 14.32s 14.59s
% Output : Proof 14.48s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SEV567+1 : TPTP v9.1.0. Released v9.1.0.
% 0.10/0.11 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n015.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.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Fri Jun 20 07:42:11 EDT 2025
% 0.11/0.33 % CPUTime :
% 14.32/14.59 % SZS status Theorem
% 14.32/14.59 % SZS output start Proof
% 14.32/14.59 tff(mem_type, type, (
% 14.32/14.59 mem: ( $i * $i ) > $o)).
% 14.32/14.59 tff(s_type, type, (
% 14.32/14.59 s: $i > $i)).
% 14.32/14.59 tff(e_type, type, (
% 14.32/14.59 e: $i)).
% 14.32/14.59 tff(a_type, type, (
% 14.32/14.59 a: ( $i * $i ) > $i)).
% 14.32/14.59 tff(n_type, type, (
% 14.32/14.59 n: $i > $i)).
% 14.32/14.59 tff(u_type, type, (
% 14.32/14.59 u: ( $i * $i ) > $i)).
% 14.32/14.59 tff(tptp_fun_Z_0_type, type, (
% 14.32/14.59 tptp_fun_Z_0: ( $i * $i ) > $i)).
% 14.32/14.59 tff(subq_type, type, (
% 14.32/14.59 subq: ( $i * $i ) > $o)).
% 14.32/14.59 tff(1,assumption,(~(mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))))), introduced(assumption)).
% 14.32/14.59 tff(2,plain,
% 14.32/14.59 (^[X: $i, Y: $i, Z: $i] : refl((mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y))) <=> (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y))))),
% 14.32/14.59 inference(bind,[status(th)],[])).
% 14.32/14.59 tff(3,plain,
% 14.32/14.59 (![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y))) <=> ![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(quant_intro,[status(thm)],[2])).
% 14.32/14.59 tff(4,plain,
% 14.32/14.59 (![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y))) <=> ![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(5,plain,
% 14.32/14.59 (^[X: $i, Y: $i, Z: $i] : rewrite((mem(X, u(Y, Z)) <=> (mem(X, Y) | mem(X, Z))) <=> (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y))))),
% 14.32/14.59 inference(bind,[status(th)],[])).
% 14.32/14.59 tff(6,plain,
% 14.32/14.59 (![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Y) | mem(X, Z))) <=> ![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(quant_intro,[status(thm)],[5])).
% 14.32/14.59 tff(7,axiom,(![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Y) | mem(X, Z)))), file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax','u_ax')).
% 14.32/14.59 tff(8,plain,
% 14.32/14.59 (![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[7, 6])).
% 14.32/14.59 tff(9,plain,
% 14.32/14.59 (![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[8, 4])).
% 14.32/14.59 tff(10,plain,(
% 14.32/14.59 ![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(skolemize,[status(sab)],[9])).
% 14.32/14.59 tff(11,plain,
% 14.32/14.59 (![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[10, 3])).
% 14.32/14.59 tff(12,plain,
% 14.32/14.59 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(13,plain,
% 14.32/14.59 ((mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), s(e)) | mem(a(n(e), n(e)), e))) <=> (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(14,plain,
% 14.32/14.59 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), s(e)) | mem(a(n(e), n(e)), e)))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[13])).
% 14.32/14.59 tff(15,plain,
% 14.32/14.59 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), s(e)) | mem(a(n(e), n(e)), e)))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))))),
% 14.32/14.59 inference(transitivity,[status(thm)],[14, 12])).
% 14.32/14.59 tff(16,plain,
% 14.32/14.59 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), s(e)) | mem(a(n(e), n(e)), e)))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(17,plain,
% 14.32/14.59 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[16, 15])).
% 14.32/14.59 tff(18,plain,
% 14.32/14.59 ($false),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[17, 11, 1])).
% 14.32/14.59 tff(19,plain,(mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))), inference(lemma,lemma(discharge,[]))).
% 14.32/14.59 tff(20,assumption,(mem(a(n(e), n(e)), e)), introduced(assumption)).
% 14.32/14.59 tff(21,plain,
% 14.32/14.59 (^[X: $i] : refl((~mem(X, e)) <=> (~mem(X, e)))),
% 14.32/14.59 inference(bind,[status(th)],[])).
% 14.32/14.59 tff(22,plain,
% 14.32/14.59 (![X: $i] : (~mem(X, e)) <=> ![X: $i] : (~mem(X, e))),
% 14.32/14.59 inference(quant_intro,[status(thm)],[21])).
% 14.32/14.59 tff(23,plain,
% 14.32/14.59 (![X: $i] : (~mem(X, e)) <=> ![X: $i] : (~mem(X, e))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(24,axiom,(![X: $i] : (~mem(X, e))), file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax','e_ax')).
% 14.32/14.59 tff(25,plain,
% 14.32/14.59 (![X: $i] : (~mem(X, e))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[24, 23])).
% 14.32/14.59 tff(26,plain,(
% 14.32/14.59 ![X: $i] : (~mem(X, e))),
% 14.32/14.59 inference(skolemize,[status(sab)],[25])).
% 14.32/14.59 tff(27,plain,
% 14.32/14.59 (![X: $i] : (~mem(X, e))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[26, 22])).
% 14.32/14.59 tff(28,plain,
% 14.32/14.59 ((~![X: $i] : (~mem(X, e))) | (~mem(a(n(e), n(e)), e))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(29,plain,
% 14.32/14.59 ($false),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[28, 27, 20])).
% 14.32/14.59 tff(30,plain,(~mem(a(n(e), n(e)), e)), inference(lemma,lemma(discharge,[]))).
% 14.32/14.59 tff(31,assumption,(~(mem(a(n(e), n(e)), s(e)) <=> (a(n(e), n(e)) = e))), introduced(assumption)).
% 14.32/14.59 tff(32,plain,
% 14.32/14.59 (^[X: $i, Y: $i] : refl((mem(X, s(Y)) <=> (X = Y)) <=> (mem(X, s(Y)) <=> (X = Y)))),
% 14.32/14.59 inference(bind,[status(th)],[])).
% 14.32/14.59 tff(33,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y)) <=> ![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))),
% 14.32/14.59 inference(quant_intro,[status(thm)],[32])).
% 14.32/14.59 tff(34,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y)) <=> ![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(35,axiom,(![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))), file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax','s_ax')).
% 14.32/14.59 tff(36,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[35, 34])).
% 14.32/14.59 tff(37,plain,(
% 14.32/14.59 ![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))),
% 14.32/14.59 inference(skolemize,[status(sab)],[36])).
% 14.32/14.59 tff(38,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[37, 33])).
% 14.32/14.59 tff(39,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(n(e), n(e)), s(e)) <=> (a(n(e), n(e)) = e))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(40,plain,
% 14.32/14.59 ($false),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[39, 38, 31])).
% 14.32/14.59 tff(41,plain,(mem(a(n(e), n(e)), s(e)) <=> (a(n(e), n(e)) = e)), inference(lemma,lemma(discharge,[]))).
% 14.32/14.59 tff(42,assumption,(a(n(e), n(e)) = e), introduced(assumption)).
% 14.32/14.59 tff(43,plain,
% 14.32/14.59 (e = a(n(e), n(e))),
% 14.32/14.59 inference(symmetry,[status(thm)],[42])).
% 14.32/14.59 tff(44,assumption,(e = a(n(e), n(e))), introduced(assumption)).
% 14.32/14.59 tff(45,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e))) <=> (tptp_fun_Z_0(s(e), a(n(e), n(e))) = a(e, e)))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(46,plain,
% 14.32/14.59 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e))) <=> (tptp_fun_Z_0(s(e), a(n(e), n(e))) = a(e, e))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[45, 38])).
% 14.32/14.59 tff(47,plain,
% 14.32/14.59 (^[X: $i] : refl((n(X) = a(X, X)) <=> (n(X) = a(X, X)))),
% 14.32/14.59 inference(bind,[status(th)],[])).
% 14.32/14.59 tff(48,plain,
% 14.32/14.59 (![X: $i] : (n(X) = a(X, X)) <=> ![X: $i] : (n(X) = a(X, X))),
% 14.32/14.59 inference(quant_intro,[status(thm)],[47])).
% 14.32/14.59 tff(49,plain,
% 14.32/14.59 (![X: $i] : (n(X) = a(X, X)) <=> ![X: $i] : (n(X) = a(X, X))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(50,axiom,(![X: $i] : (n(X) = a(X, X))), file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax','n_def')).
% 14.32/14.59 tff(51,plain,
% 14.32/14.59 (![X: $i] : (n(X) = a(X, X))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[50, 49])).
% 14.32/14.59 tff(52,plain,(
% 14.32/14.59 ![X: $i] : (n(X) = a(X, X))),
% 14.32/14.59 inference(skolemize,[status(sab)],[51])).
% 14.32/14.59 tff(53,plain,
% 14.32/14.59 (![X: $i] : (n(X) = a(X, X))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[52, 48])).
% 14.32/14.59 tff(54,plain,
% 14.32/14.59 ((~![X: $i] : (n(X) = a(X, X))) | (n(e) = a(e, e))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(55,plain,
% 14.32/14.59 (n(e) = a(e, e)),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[54, 53])).
% 14.32/14.59 tff(56,plain,
% 14.32/14.59 (a(e, e) = n(e)),
% 14.32/14.59 inference(symmetry,[status(thm)],[55])).
% 14.32/14.59 tff(57,plain,
% 14.32/14.59 (s(a(e, e)) = s(n(e))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[56])).
% 14.32/14.59 tff(58,plain,
% 14.32/14.59 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e))) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e)))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[57])).
% 14.32/14.59 tff(59,plain,
% 14.32/14.59 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e)))),
% 14.32/14.59 inference(symmetry,[status(thm)],[58])).
% 14.32/14.59 tff(60,plain,
% 14.32/14.59 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e)))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(61,plain,
% 14.32/14.59 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e)))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e)))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[60, 11])).
% 14.32/14.59 tff(62,plain,
% 14.32/14.59 (a(a(e, e), a(e, e)) = a(n(e), n(e))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[56, 56])).
% 14.32/14.59 tff(63,plain,
% 14.32/14.59 (^[X: $i, Y: $i] : refl((a(X, Y) = u(X, s(Y))) <=> (a(X, Y) = u(X, s(Y))))),
% 14.32/14.59 inference(bind,[status(th)],[])).
% 14.32/14.59 tff(64,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y))) <=> ![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))),
% 14.32/14.59 inference(quant_intro,[status(thm)],[63])).
% 14.32/14.59 tff(65,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y))) <=> ![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))),
% 14.32/14.59 inference(rewrite,[status(thm)],[])).
% 14.32/14.59 tff(66,axiom,(![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))), file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax','a_def')).
% 14.32/14.59 tff(67,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[66, 65])).
% 14.32/14.59 tff(68,plain,(
% 14.32/14.59 ![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))),
% 14.32/14.59 inference(skolemize,[status(sab)],[67])).
% 14.32/14.59 tff(69,plain,
% 14.32/14.59 (![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))),
% 14.32/14.59 inference(modus_ponens,[status(thm)],[68, 64])).
% 14.32/14.59 tff(70,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(a(e, e), a(e, e)) = u(a(e, e), s(a(e, e))))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(71,plain,
% 14.32/14.59 (a(a(e, e), a(e, e)) = u(a(e, e), s(a(e, e)))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[70, 69])).
% 14.32/14.59 tff(72,plain,
% 14.32/14.59 (u(a(e, e), s(a(e, e))) = a(a(e, e), a(e, e))),
% 14.32/14.59 inference(symmetry,[status(thm)],[71])).
% 14.32/14.59 tff(73,plain,
% 14.32/14.59 (s(n(e)) = s(a(e, e))),
% 14.32/14.59 inference(symmetry,[status(thm)],[57])).
% 14.32/14.59 tff(74,plain,
% 14.32/14.59 (u(a(e, e), s(n(e))) = u(a(e, e), s(a(e, e)))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[73])).
% 14.32/14.59 tff(75,plain,
% 14.32/14.59 (u(a(e, e), s(n(e))) = a(n(e), n(e))),
% 14.32/14.59 inference(transitivity,[status(thm)],[74, 72, 62])).
% 14.32/14.59 tff(76,plain,
% 14.32/14.59 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e)))) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[75])).
% 14.32/14.59 tff(77,plain,
% 14.32/14.59 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e))) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e))))),
% 14.32/14.59 inference(symmetry,[status(thm)],[76])).
% 14.32/14.59 tff(78,assumption,(~(mem(a(e, e), s(e)) <=> (a(e, e) = e))), introduced(assumption)).
% 14.32/14.59 tff(79,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(e)) <=> (a(e, e) = e))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(80,plain,
% 14.32/14.59 ($false),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[79, 38, 78])).
% 14.32/14.59 tff(81,plain,(mem(a(e, e), s(e)) <=> (a(e, e) = e)), inference(lemma,lemma(discharge,[]))).
% 14.32/14.59 tff(82,plain,
% 14.32/14.59 ((~![X: $i] : (n(X) = a(X, X))) | (n(n(e)) = a(n(e), n(e)))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(83,plain,
% 14.32/14.59 (n(n(e)) = a(n(e), n(e))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[82, 53])).
% 14.32/14.59 tff(84,assumption,(a(e, e) = e), introduced(assumption)).
% 14.32/14.59 tff(85,plain,
% 14.32/14.59 (e = a(e, e)),
% 14.32/14.59 inference(symmetry,[status(thm)],[84])).
% 14.32/14.59 tff(86,plain,
% 14.32/14.59 (e = n(e)),
% 14.32/14.59 inference(transitivity,[status(thm)],[85, 56])).
% 14.32/14.59 tff(87,plain,
% 14.32/14.59 (n(e) = n(n(e))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[86])).
% 14.32/14.59 tff(88,plain,
% 14.32/14.59 (a(e, e) = a(n(e), n(e))),
% 14.32/14.59 inference(transitivity,[status(thm)],[56, 87, 83])).
% 14.32/14.59 tff(89,assumption,(a(e, e) = a(n(e), n(e))), introduced(assumption)).
% 14.32/14.59 tff(90,plain,
% 14.32/14.59 (a(n(e), n(e)) = a(e, e)),
% 14.32/14.59 inference(symmetry,[status(thm)],[89])).
% 14.32/14.59 tff(91,plain,
% 14.32/14.59 (n(n(e)) = n(e)),
% 14.32/14.59 inference(transitivity,[status(thm)],[83, 90, 56])).
% 14.32/14.59 tff(92,plain,
% 14.32/14.59 (a(n(e), n(n(e))) = a(n(e), n(e))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[91])).
% 14.32/14.59 tff(93,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(n(e), n(n(e))) = u(n(e), s(n(n(e)))))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(94,plain,
% 14.32/14.59 (a(n(e), n(n(e))) = u(n(e), s(n(n(e))))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[93, 69])).
% 14.32/14.59 tff(95,plain,
% 14.32/14.59 (u(n(e), s(n(n(e)))) = a(n(e), n(n(e)))),
% 14.32/14.59 inference(symmetry,[status(thm)],[94])).
% 14.32/14.59 tff(96,plain,
% 14.32/14.59 (u(n(e), s(n(n(e)))) = a(n(e), n(e))),
% 14.32/14.59 inference(transitivity,[status(thm)],[95, 92])).
% 14.32/14.59 tff(97,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))) <=> (u(n(e), s(n(n(e)))) = a(n(e), n(e))))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(98,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))) <=> (u(n(e), s(n(n(e)))) = a(n(e), n(e)))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[97, 38])).
% 14.32/14.59 tff(99,plain,
% 14.32/14.59 (a(n(e), n(e)) = n(n(e))),
% 14.32/14.59 inference(symmetry,[status(thm)],[83])).
% 14.32/14.59 tff(100,plain,
% 14.32/14.59 (s(a(n(e), n(e))) = s(n(n(e)))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[99])).
% 14.32/14.59 tff(101,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))) <=> mem(u(n(e), s(n(n(e)))), s(n(n(e))))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[100])).
% 14.32/14.59 tff(102,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) <=> mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e))))),
% 14.32/14.59 inference(symmetry,[status(thm)],[101])).
% 14.32/14.59 tff(103,plain,
% 14.32/14.59 ((~mem(u(n(e), s(n(n(e)))), s(n(n(e))))) <=> (~mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[102])).
% 14.32/14.59 tff(104,plain,
% 14.32/14.59 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))) <=> (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(105,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))) <=> (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e)))),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[104, 11])).
% 14.32/14.59 tff(106,plain,
% 14.32/14.59 (u(a(e, e), s(n(n(e)))) = u(n(e), s(n(n(e))))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[56])).
% 14.32/14.59 tff(107,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))) <=> mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[106])).
% 14.32/14.59 tff(108,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e))))) <=> mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e)))))),
% 14.32/14.59 inference(symmetry,[status(thm)],[107])).
% 14.32/14.59 tff(109,plain,
% 14.32/14.59 ((~mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))) <=> (~mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))))),
% 14.32/14.59 inference(monotonicity,[status(thm)],[108])).
% 14.32/14.59 tff(110,plain,
% 14.32/14.59 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(u(n(e), s(n(n(e)))), s(e)) <=> (u(n(e), s(n(n(e)))) = e))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(111,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), s(e)) <=> (u(n(e), s(n(n(e)))) = e)),
% 14.32/14.59 inference(unit_resolution,[status(thm)],[110, 38])).
% 14.32/14.59 tff(112,plain,
% 14.32/14.59 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(u(n(e), s(n(n(e)))), u(e, s(e))) <=> (mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e)))),
% 14.32/14.59 inference(quant_inst,[status(thm)],[])).
% 14.32/14.59 tff(113,plain,
% 14.32/14.59 (mem(u(n(e), s(n(n(e)))), u(e, s(e))) <=> (mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[112, 11])).
% 14.44/14.59 tff(114,plain,
% 14.44/14.59 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(e, e) = u(e, s(e)))),
% 14.44/14.59 inference(quant_inst,[status(thm)],[])).
% 14.44/14.59 tff(115,plain,
% 14.44/14.59 (a(e, e) = u(e, s(e))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[114, 69])).
% 14.44/14.59 tff(116,plain,
% 14.44/14.59 (u(e, s(e)) = a(e, e)),
% 14.44/14.59 inference(symmetry,[status(thm)],[115])).
% 14.44/14.59 tff(117,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), u(e, s(e))) <=> mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.59 inference(monotonicity,[status(thm)],[116])).
% 14.44/14.59 tff(118,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), a(e, e)) <=> mem(u(n(e), s(n(n(e)))), u(e, s(e)))),
% 14.44/14.59 inference(symmetry,[status(thm)],[117])).
% 14.44/14.59 tff(119,assumption,(mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))), introduced(assumption)).
% 14.44/14.59 tff(120,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e)))))),
% 14.44/14.59 inference(modus_ponens,[status(thm)],[119, 108])).
% 14.44/14.59 tff(121,plain,
% 14.44/14.59 ((~(mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))) <=> (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))))) | (~mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e)))))) | (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e)))),
% 14.44/14.59 inference(tautology,[status(thm)],[])).
% 14.44/14.59 tff(122,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[121, 120, 105])).
% 14.44/14.59 tff(123,assumption,(~mem(u(n(e), s(n(n(e)))), a(e, e))), introduced(assumption)).
% 14.44/14.59 tff(124,plain,
% 14.44/14.59 ((~(mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e)))) | mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.59 inference(tautology,[status(thm)],[])).
% 14.44/14.59 tff(125,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), s(n(n(e))))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[124, 123, 122])).
% 14.44/14.59 tff(126,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e))))),
% 14.44/14.59 inference(modus_ponens,[status(thm)],[125, 102])).
% 14.44/14.59 tff(127,plain,
% 14.44/14.59 ((~(mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))) <=> (u(n(e), s(n(n(e)))) = a(n(e), n(e))))) | (~mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e))))) | (u(n(e), s(n(n(e)))) = a(n(e), n(e)))),
% 14.44/14.59 inference(tautology,[status(thm)],[])).
% 14.44/14.59 tff(128,plain,
% 14.44/14.59 (u(n(e), s(n(n(e)))) = a(n(e), n(e))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[127, 126, 98])).
% 14.44/14.59 tff(129,plain,
% 14.44/14.59 (a(n(e), n(e)) = u(n(e), s(n(n(e))))),
% 14.44/14.59 inference(symmetry,[status(thm)],[128])).
% 14.44/14.59 tff(130,plain,
% 14.44/14.59 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(n(e), n(e)), s(a(e, e))) <=> (a(n(e), n(e)) = a(e, e)))),
% 14.44/14.59 inference(quant_inst,[status(thm)],[])).
% 14.44/14.59 tff(131,plain,
% 14.44/14.59 (mem(a(n(e), n(e)), s(a(e, e))) <=> (a(n(e), n(e)) = a(e, e))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[130, 38])).
% 14.44/14.59 tff(132,plain,
% 14.44/14.59 (mem(a(n(e), n(e)), s(a(e, e))) <=> mem(a(n(e), n(e)), s(n(e)))),
% 14.44/14.59 inference(monotonicity,[status(thm)],[57])).
% 14.44/14.59 tff(133,plain,
% 14.44/14.59 (mem(a(n(e), n(e)), s(n(e))) <=> mem(a(n(e), n(e)), s(a(e, e)))),
% 14.44/14.59 inference(symmetry,[status(thm)],[132])).
% 14.44/14.59 tff(134,plain,
% 14.44/14.59 (mem(a(n(e), n(e)), a(e, e)) <=> mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.59 inference(monotonicity,[status(thm)],[129])).
% 14.44/14.59 tff(135,plain,
% 14.44/14.59 (mem(u(n(e), s(n(n(e)))), a(e, e)) <=> mem(a(n(e), n(e)), a(e, e))),
% 14.44/14.59 inference(symmetry,[status(thm)],[134])).
% 14.44/14.59 tff(136,plain,
% 14.44/14.59 ((~mem(u(n(e), s(n(n(e)))), a(e, e))) <=> (~mem(a(n(e), n(e)), a(e, e)))),
% 14.44/14.59 inference(monotonicity,[status(thm)],[135])).
% 14.44/14.59 tff(137,plain,
% 14.44/14.59 (~mem(a(n(e), n(e)), a(e, e))),
% 14.44/14.59 inference(modus_ponens,[status(thm)],[123, 136])).
% 14.44/14.59 tff(138,plain,
% 14.44/14.59 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(e)))) <=> (mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e))))),
% 14.44/14.59 inference(quant_inst,[status(thm)],[])).
% 14.44/14.59 tff(139,plain,
% 14.44/14.59 (mem(a(n(e), n(e)), u(a(e, e), s(n(e)))) <=> (mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e)))),
% 14.44/14.59 inference(unit_resolution,[status(thm)],[138, 11])).
% 14.44/14.59 tff(140,plain,
% 14.44/14.59 (u(a(e, e), s(n(e))) = u(n(e), s(n(n(e))))),
% 14.44/14.59 inference(transitivity,[status(thm)],[74, 72, 62, 129])).
% 14.44/14.59 tff(141,plain,
% 14.44/14.60 (mem(a(n(e), n(e)), u(a(e, e), s(n(e)))) <=> mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[129, 140])).
% 14.44/14.60 tff(142,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e))))) <=> mem(a(n(e), n(e)), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(symmetry,[status(thm)],[141])).
% 14.44/14.60 tff(143,plain,
% 14.44/14.60 (mem(a(n(e), n(e)), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[119, 142])).
% 14.44/14.60 tff(144,plain,
% 14.44/14.60 ((~(mem(a(n(e), n(e)), u(a(e, e), s(n(e)))) <=> (mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e))))) | (~mem(a(n(e), n(e)), u(a(e, e), s(n(e))))) | (mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e)))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(145,plain,
% 14.44/14.60 (mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[144, 143, 139])).
% 14.44/14.60 tff(146,plain,
% 14.44/14.60 ((~(mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e)))) | mem(a(n(e), n(e)), s(n(e))) | mem(a(n(e), n(e)), a(e, e))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(147,plain,
% 14.44/14.60 (mem(a(n(e), n(e)), s(n(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[146, 145, 137])).
% 14.44/14.60 tff(148,plain,
% 14.44/14.60 (mem(a(n(e), n(e)), s(a(e, e)))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[147, 133])).
% 14.44/14.60 tff(149,plain,
% 14.44/14.60 ((~(mem(a(n(e), n(e)), s(a(e, e))) <=> (a(n(e), n(e)) = a(e, e)))) | (~mem(a(n(e), n(e)), s(a(e, e)))) | (a(n(e), n(e)) = a(e, e))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(150,plain,
% 14.44/14.60 (a(n(e), n(e)) = a(e, e)),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[149, 148, 131])).
% 14.44/14.60 tff(151,plain,
% 14.44/14.60 (a(e, e) = a(n(e), n(e))),
% 14.44/14.60 inference(symmetry,[status(thm)],[150])).
% 14.44/14.60 tff(152,plain,
% 14.44/14.60 (a(e, e) = u(n(e), s(n(n(e))))),
% 14.44/14.60 inference(transitivity,[status(thm)],[151, 129])).
% 14.44/14.60 tff(153,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), a(e, e)) <=> mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[152])).
% 14.44/14.60 tff(154,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e))))) <=> mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.60 inference(symmetry,[status(thm)],[153])).
% 14.44/14.60 tff(155,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[119, 154])).
% 14.44/14.60 tff(156,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[123, 155])).
% 14.44/14.60 tff(157,plain,(mem(u(n(e), s(n(n(e)))), a(e, e)) | (~mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e))))))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(158,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), a(e, e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[157, 119])).
% 14.44/14.60 tff(159,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), u(e, s(e)))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[158, 118])).
% 14.44/14.60 tff(160,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), u(e, s(e))) <=> (mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e)))) | (~mem(u(n(e), s(n(n(e)))), u(e, s(e)))) | (mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(161,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e)),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[160, 159, 113])).
% 14.44/14.60 tff(162,assumption,(mem(u(n(e), s(n(n(e)))), e)), introduced(assumption)).
% 14.44/14.60 tff(163,plain,
% 14.44/14.60 ((~![X: $i] : (~mem(X, e))) | (~mem(u(n(e), s(n(n(e)))), e))),
% 14.44/14.60 inference(quant_inst,[status(thm)],[])).
% 14.44/14.60 tff(164,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[163, 27, 162])).
% 14.44/14.60 tff(165,plain,(~mem(u(n(e), s(n(n(e)))), e)), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(166,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e))) | mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e)),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(167,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), s(e)) | mem(u(n(e), s(n(n(e)))), e))) | mem(u(n(e), s(n(n(e)))), s(e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[166, 165])).
% 14.44/14.60 tff(168,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), s(e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[167, 161])).
% 14.44/14.60 tff(169,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), s(e)) <=> (u(n(e), s(n(n(e)))) = e))) | (~mem(u(n(e), s(n(n(e)))), s(e))) | (u(n(e), s(n(n(e)))) = e)),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(170,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), s(e)) <=> (u(n(e), s(n(n(e)))) = e))) | (u(n(e), s(n(n(e)))) = e)),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[169, 168])).
% 14.44/14.60 tff(171,plain,
% 14.44/14.60 (u(n(e), s(n(n(e)))) = e),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[170, 111])).
% 14.44/14.60 tff(172,plain,
% 14.44/14.60 (e = u(n(e), s(n(n(e))))),
% 14.44/14.60 inference(symmetry,[status(thm)],[171])).
% 14.44/14.60 tff(173,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), e) <=> mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[172])).
% 14.44/14.60 tff(174,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e))))) <=> mem(u(n(e), s(n(n(e)))), e)),
% 14.44/14.60 inference(symmetry,[status(thm)],[173])).
% 14.44/14.60 tff(175,plain,
% 14.44/14.60 (mem(u(n(e), s(n(n(e)))), e)),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[119, 174])).
% 14.44/14.60 tff(176,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[165, 175])).
% 14.44/14.60 tff(177,plain,(~mem(u(n(e), s(n(n(e)))), u(n(e), s(n(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(178,plain,
% 14.44/14.60 (~mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e)))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[177, 109])).
% 14.44/14.60 tff(179,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))) <=> (mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))))) | mem(u(n(e), s(n(n(e)))), u(a(e, e), s(n(n(e))))) | (~(mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(180,plain,
% 14.44/14.60 (~(mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[179, 178, 105])).
% 14.44/14.60 tff(181,plain,
% 14.44/14.60 ((mem(u(n(e), s(n(n(e)))), s(n(n(e)))) | mem(u(n(e), s(n(n(e)))), a(e, e))) | (~mem(u(n(e), s(n(n(e)))), s(n(n(e)))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(182,plain,
% 14.44/14.60 (~mem(u(n(e), s(n(n(e)))), s(n(n(e))))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[181, 180])).
% 14.44/14.60 tff(183,plain,
% 14.44/14.60 (~mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[182, 103])).
% 14.44/14.60 tff(184,plain,
% 14.44/14.60 ((~(mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))) <=> (u(n(e), s(n(n(e)))) = a(n(e), n(e))))) | mem(u(n(e), s(n(n(e)))), s(a(n(e), n(e)))) | (~(u(n(e), s(n(n(e)))) = a(n(e), n(e))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(185,plain,
% 14.44/14.60 (~(u(n(e), s(n(n(e)))) = a(n(e), n(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[184, 183, 98])).
% 14.44/14.60 tff(186,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[185, 96])).
% 14.44/14.60 tff(187,plain,(~(a(e, e) = a(n(e), n(e)))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(188,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[187, 88])).
% 14.44/14.60 tff(189,plain,(~(a(e, e) = e)), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(190,plain,
% 14.44/14.60 ((~(mem(a(e, e), s(e)) <=> (a(e, e) = e))) | (~mem(a(e, e), s(e))) | (a(e, e) = e)),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(191,plain,
% 14.44/14.60 ((~(mem(a(e, e), s(e)) <=> (a(e, e) = e))) | (~mem(a(e, e), s(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[190, 189])).
% 14.44/14.60 tff(192,plain,
% 14.44/14.60 (~mem(a(e, e), s(e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[191, 81])).
% 14.44/14.60 tff(193,assumption,(![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))), introduced(assumption)).
% 14.44/14.60 tff(194,assumption,(~(mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))), introduced(assumption)).
% 14.44/14.60 tff(195,plain,
% 14.44/14.60 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e))))))),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(196,plain,
% 14.44/14.60 ((mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), s(n(e))) | mem(a(e, e), a(e, e)))) <=> (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(197,plain,
% 14.44/14.60 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), s(n(e))) | mem(a(e, e), a(e, e))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e))))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[196])).
% 14.44/14.60 tff(198,plain,
% 14.44/14.60 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), s(n(e))) | mem(a(e, e), a(e, e))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e))))))),
% 14.44/14.60 inference(transitivity,[status(thm)],[197, 195])).
% 14.44/14.60 tff(199,plain,
% 14.44/14.60 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), s(n(e))) | mem(a(e, e), a(e, e))))),
% 14.44/14.60 inference(quant_inst,[status(thm)],[])).
% 14.44/14.60 tff(200,plain,
% 14.44/14.60 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[199, 198])).
% 14.44/14.60 tff(201,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[200, 11, 194])).
% 14.44/14.60 tff(202,plain,(mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(203,plain,
% 14.44/14.60 (mem(a(e, e), s(a(e, e))) <=> mem(a(e, e), s(n(e)))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[57])).
% 14.44/14.60 tff(204,plain,
% 14.44/14.60 (mem(a(e, e), s(n(e))) <=> mem(a(e, e), s(a(e, e)))),
% 14.44/14.60 inference(symmetry,[status(thm)],[203])).
% 14.44/14.60 tff(205,plain,
% 14.44/14.60 ((~mem(a(e, e), s(n(e)))) <=> (~mem(a(e, e), s(a(e, e))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[204])).
% 14.44/14.60 tff(206,assumption,(~mem(a(e, e), s(n(e)))), introduced(assumption)).
% 14.44/14.60 tff(207,plain,
% 14.44/14.60 (~mem(a(e, e), s(a(e, e)))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[206, 205])).
% 14.44/14.60 tff(208,plain,
% 14.44/14.60 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(e, e), s(a(e, e)))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(e, e), s(a(e, e))))),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(209,plain,
% 14.44/14.60 ((mem(a(e, e), s(a(e, e))) <=> $true) <=> mem(a(e, e), s(a(e, e)))),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(210,plain,
% 14.44/14.60 ((a(e, e) = a(e, e)) <=> $true),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(211,plain,
% 14.44/14.60 ((mem(a(e, e), s(a(e, e))) <=> (a(e, e) = a(e, e))) <=> (mem(a(e, e), s(a(e, e))) <=> $true)),
% 14.44/14.60 inference(monotonicity,[status(thm)],[210])).
% 14.44/14.60 tff(212,plain,
% 14.44/14.60 ((mem(a(e, e), s(a(e, e))) <=> (a(e, e) = a(e, e))) <=> mem(a(e, e), s(a(e, e)))),
% 14.44/14.60 inference(transitivity,[status(thm)],[211, 209])).
% 14.44/14.60 tff(213,plain,
% 14.44/14.60 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(a(e, e))) <=> (a(e, e) = a(e, e)))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(e, e), s(a(e, e))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[212])).
% 14.44/14.60 tff(214,plain,
% 14.44/14.60 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(a(e, e))) <=> (a(e, e) = a(e, e)))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(e, e), s(a(e, e))))),
% 14.44/14.60 inference(transitivity,[status(thm)],[213, 208])).
% 14.44/14.60 tff(215,plain,
% 14.44/14.60 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(a(e, e))) <=> (a(e, e) = a(e, e)))),
% 14.44/14.60 inference(quant_inst,[status(thm)],[])).
% 14.44/14.60 tff(216,plain,
% 14.44/14.60 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(e, e), s(a(e, e)))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[215, 214])).
% 14.44/14.60 tff(217,plain,
% 14.44/14.60 (mem(a(e, e), s(a(e, e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[216, 38])).
% 14.44/14.60 tff(218,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[217, 207])).
% 14.44/14.60 tff(219,plain,(mem(a(e, e), s(n(e)))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(220,plain,
% 14.44/14.60 ((mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))) | (~mem(a(e, e), s(n(e))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(221,plain,
% 14.44/14.60 (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[220, 219])).
% 14.44/14.60 tff(222,plain,
% 14.44/14.60 ((~(mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))) | mem(a(e, e), u(a(e, e), s(n(e)))) | (~(mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(223,plain,
% 14.44/14.60 ((~(mem(a(e, e), u(a(e, e), s(n(e)))) <=> (mem(a(e, e), a(e, e)) | mem(a(e, e), s(n(e)))))) | mem(a(e, e), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[222, 221])).
% 14.44/14.60 tff(224,plain,
% 14.44/14.60 (mem(a(e, e), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[223, 202])).
% 14.44/14.60 tff(225,plain,
% 14.44/14.60 (mem(a(e, e), u(a(e, e), s(n(e)))) <=> mem(a(e, e), a(n(e), n(e)))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[75])).
% 14.44/14.60 tff(226,plain,
% 14.44/14.60 (mem(a(e, e), a(n(e), n(e))) <=> mem(a(e, e), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(symmetry,[status(thm)],[225])).
% 14.44/14.60 tff(227,plain,
% 14.44/14.60 ((~mem(a(e, e), a(n(e), n(e)))) <=> (~mem(a(e, e), u(a(e, e), s(n(e)))))),
% 14.44/14.60 inference(monotonicity,[status(thm)],[226])).
% 14.44/14.60 tff(228,assumption,(~mem(a(e, e), a(n(e), n(e)))), introduced(assumption)).
% 14.44/14.60 tff(229,plain,
% 14.44/14.60 (~mem(a(e, e), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[228, 227])).
% 14.44/14.60 tff(230,assumption,(mem(a(e, e), u(a(e, e), s(n(e))))), introduced(assumption)).
% 14.44/14.60 tff(231,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[230, 229])).
% 14.44/14.60 tff(232,plain,((~mem(a(e, e), u(a(e, e), s(n(e))))) | mem(a(e, e), a(n(e), n(e)))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(233,plain,
% 14.44/14.60 (mem(a(e, e), a(n(e), n(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[232, 224])).
% 14.44/14.60 tff(234,plain,
% 14.44/14.60 (((~![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))) | ((~mem(a(e, e), a(n(e), n(e)))) | mem(a(e, e), s(e)))) <=> ((~![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))) | (~mem(a(e, e), a(n(e), n(e)))) | mem(a(e, e), s(e)))),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(235,plain,
% 14.44/14.60 ((~![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))) | ((~mem(a(e, e), a(n(e), n(e)))) | mem(a(e, e), s(e)))),
% 14.44/14.60 inference(quant_inst,[status(thm)],[])).
% 14.44/14.60 tff(236,plain,
% 14.44/14.60 ((~![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))) | (~mem(a(e, e), a(n(e), n(e)))) | mem(a(e, e), s(e))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[235, 234])).
% 14.44/14.60 tff(237,plain,
% 14.44/14.60 ($false),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[236, 233, 193, 192])).
% 14.44/14.60 tff(238,plain,(~![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.60 tff(239,plain,
% 14.44/14.60 (^[X: $i, Y: $i] : refl((~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))) <=> (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))))),
% 14.44/14.60 inference(bind,[status(th)],[])).
% 14.44/14.60 tff(240,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))) <=> ![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))),
% 14.44/14.60 inference(quant_intro,[status(thm)],[239])).
% 14.44/14.60 tff(241,plain,
% 14.44/14.60 (^[X: $i, Y: $i] : rewrite((~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))) <=> (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))))),
% 14.44/14.60 inference(bind,[status(th)],[])).
% 14.44/14.60 tff(242,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))) <=> ![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))),
% 14.44/14.60 inference(quant_intro,[status(thm)],[241])).
% 14.44/14.60 tff(243,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))) <=> ![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))),
% 14.44/14.60 inference(transitivity,[status(thm)],[242, 240])).
% 14.44/14.60 tff(244,plain,
% 14.44/14.60 (^[X: $i, Y: $i] : trans(monotonicity(rewrite(((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) <=> ((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))), rewrite((subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))) <=> (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))), ((((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) & (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))) <=> (((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) & (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))))), rewrite((((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) & (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))) <=> (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))), ((((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) & (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))) <=> (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))))),
% 14.44/14.60 inference(bind,[status(th)],[])).
% 14.44/14.60 tff(245,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) & (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y))))) <=> ![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))),
% 14.44/14.60 inference(quant_intro,[status(thm)],[244])).
% 14.44/14.60 tff(246,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) <=> ![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))),
% 14.44/14.60 inference(rewrite,[status(thm)],[])).
% 14.44/14.60 tff(247,plain,
% 14.44/14.60 (^[X: $i, Y: $i] : rewrite((subq(X, Y) <=> ![Z: $i] : (mem(Z, X) => mem(Z, Y))) <=> (subq(X, Y) <=> ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))))),
% 14.44/14.60 inference(bind,[status(th)],[])).
% 14.44/14.60 tff(248,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : (mem(Z, X) => mem(Z, Y))) <=> ![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))),
% 14.44/14.60 inference(quant_intro,[status(thm)],[247])).
% 14.44/14.60 tff(249,axiom,(![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : (mem(Z, X) => mem(Z, Y)))), file('/export/starexec/sandbox2/benchmark/Axioms/SET010+0.ax','subq_def')).
% 14.44/14.60 tff(250,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[249, 248])).
% 14.44/14.60 tff(251,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (subq(X, Y) <=> ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[250, 246])).
% 14.44/14.60 tff(252,plain,(
% 14.44/14.60 ![X: $i, Y: $i] : (((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y))) & (subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))),
% 14.44/14.60 inference(skolemize,[status(sab)],[251])).
% 14.44/14.60 tff(253,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[252, 245])).
% 14.44/14.60 tff(254,plain,
% 14.44/14.60 (![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[253, 243])).
% 14.44/14.60 tff(255,plain,
% 14.44/14.60 ((~![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))) | (~((~((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e))))) | (~(subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))))))))),
% 14.44/14.60 inference(quant_inst,[status(thm)],[])).
% 14.44/14.60 tff(256,plain,
% 14.44/14.60 (~((~((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e))))) | (~(subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)))))))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[255, 254])).
% 14.44/14.60 tff(257,plain,
% 14.44/14.60 (((~((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e))))) | (~(subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))))))) | ((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(258,plain,
% 14.44/14.60 ((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[257, 256])).
% 14.44/14.60 tff(259,plain,
% 14.44/14.60 ((~((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e))))) | (~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(260,plain,
% 14.44/14.60 ((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[259, 258])).
% 14.44/14.60 tff(261,plain,
% 14.44/14.60 (~subq(a(n(e), n(e)), s(e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[260, 238])).
% 14.44/14.60 tff(262,plain,
% 14.44/14.60 (((~((~subq(a(n(e), n(e)), s(e))) | ![Z: $i] : ((~mem(Z, a(n(e), n(e)))) | mem(Z, s(e))))) | (~(subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))))))) | (subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(263,plain,
% 14.44/14.60 (subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[262, 256])).
% 14.44/14.60 tff(264,plain,
% 14.44/14.60 ((~(subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)))))) | subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(265,plain,
% 14.44/14.60 (subq(a(n(e), n(e)), s(e)) | (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[264, 263])).
% 14.44/14.60 tff(266,plain,
% 14.44/14.60 (~((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[265, 261])).
% 14.44/14.60 tff(267,plain,
% 14.44/14.60 (((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(268,plain,
% 14.44/14.60 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[267, 266])).
% 14.44/14.60 tff(269,plain,
% 14.44/14.60 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e))))),
% 14.44/14.60 inference(modus_ponens,[status(thm)],[268, 77])).
% 14.44/14.60 tff(270,plain,
% 14.44/14.60 ((~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e)))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))))) | (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(a(e, e), s(n(e))))) | (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e)))),
% 14.44/14.60 inference(tautology,[status(thm)],[])).
% 14.44/14.60 tff(271,plain,
% 14.44/14.60 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))),
% 14.44/14.60 inference(unit_resolution,[status(thm)],[270, 269, 61])).
% 14.44/14.60 tff(272,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e))) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[116])).
% 14.44/14.61 tff(273,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e)) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e)))),
% 14.44/14.61 inference(symmetry,[status(thm)],[272])).
% 14.44/14.61 tff(274,assumption,(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))), introduced(assumption)).
% 14.44/14.61 tff(275,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e)))),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[274, 273])).
% 14.44/14.61 tff(276,plain,
% 14.44/14.61 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)))),
% 14.44/14.61 inference(quant_inst,[status(thm)],[])).
% 14.44/14.61 tff(277,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[276, 11])).
% 14.44/14.61 tff(278,assumption,(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)), introduced(assumption)).
% 14.44/14.61 tff(279,plain,
% 14.44/14.61 ((~![X: $i] : (~mem(X, e))) | (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e))),
% 14.44/14.61 inference(quant_inst,[status(thm)],[])).
% 14.44/14.61 tff(280,plain,
% 14.44/14.61 ($false),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[279, 27, 278])).
% 14.44/14.61 tff(281,plain,(~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)), inference(lemma,lemma(discharge,[]))).
% 14.44/14.61 tff(282,plain,
% 14.44/14.61 (((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(n(e), n(e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))) | (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(283,plain,
% 14.44/14.61 (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[282, 266])).
% 14.44/14.61 tff(284,plain,
% 14.44/14.61 ((~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(285,plain,
% 14.44/14.61 (~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[284, 283, 281])).
% 14.44/14.61 tff(286,plain,
% 14.44/14.61 ((~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)))) | (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e)))) | (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(287,plain,
% 14.44/14.61 ((~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e))) <=> (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(e)) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)))) | (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[286, 285])).
% 14.44/14.61 tff(288,plain,
% 14.44/14.61 (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), u(e, s(e)))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[287, 277])).
% 14.44/14.61 tff(289,plain,
% 14.44/14.61 ($false),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[288, 275])).
% 14.44/14.61 tff(290,plain,(~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.61 tff(291,plain,
% 14.44/14.61 ((~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e)))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e))) | mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(292,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(n(e)))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[291, 290, 271])).
% 14.44/14.61 tff(293,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e)))),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[292, 59])).
% 14.44/14.61 tff(294,plain,
% 14.44/14.61 ((~(mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e))) <=> (tptp_fun_Z_0(s(e), a(n(e), n(e))) = a(e, e)))) | (~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), s(a(e, e)))) | (tptp_fun_Z_0(s(e), a(n(e), n(e))) = a(e, e))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(295,plain,
% 14.44/14.61 (tptp_fun_Z_0(s(e), a(n(e), n(e))) = a(e, e)),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[294, 293, 46])).
% 14.44/14.61 tff(296,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e) <=> mem(a(e, e), a(n(e), n(e)))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[295, 44])).
% 14.44/14.61 tff(297,plain,
% 14.44/14.61 (mem(a(e, e), a(n(e), n(e))) <=> mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)),
% 14.44/14.61 inference(symmetry,[status(thm)],[296])).
% 14.44/14.61 tff(298,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), e)),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[233, 297])).
% 14.44/14.61 tff(299,plain,
% 14.44/14.61 ($false),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[281, 298])).
% 14.44/14.61 tff(300,plain,(~(e = a(n(e), n(e)))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.61 tff(301,plain,
% 14.44/14.61 ($false),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[300, 43])).
% 14.44/14.61 tff(302,plain,(~(a(n(e), n(e)) = e)), inference(lemma,lemma(discharge,[]))).
% 14.44/14.61 tff(303,plain,
% 14.44/14.61 ((~(mem(a(n(e), n(e)), s(e)) <=> (a(n(e), n(e)) = e))) | (~mem(a(n(e), n(e)), s(e))) | (a(n(e), n(e)) = e)),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(304,plain,
% 14.44/14.61 ((~(mem(a(n(e), n(e)), s(e)) <=> (a(n(e), n(e)) = e))) | (~mem(a(n(e), n(e)), s(e)))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[303, 302])).
% 14.44/14.61 tff(305,plain,
% 14.44/14.61 (~mem(a(n(e), n(e)), s(e))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[304, 41])).
% 14.44/14.61 tff(306,plain,
% 14.44/14.61 ((~(mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))) | mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(307,plain,
% 14.44/14.61 (~(mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[306, 305, 30])).
% 14.44/14.61 tff(308,plain,
% 14.44/14.61 (mem(a(n(e), n(e)), u(e, s(e))) <=> mem(a(n(e), n(e)), a(e, e))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[116])).
% 14.44/14.61 tff(309,plain,
% 14.44/14.61 (mem(a(n(e), n(e)), a(e, e)) <=> mem(a(n(e), n(e)), u(e, s(e)))),
% 14.44/14.61 inference(symmetry,[status(thm)],[308])).
% 14.44/14.61 tff(310,assumption,(a(e, e) = u(n(e), n(s(n(e))))), introduced(assumption)).
% 14.44/14.61 tff(311,plain,
% 14.44/14.61 (u(n(e), n(s(n(e)))) = a(e, e)),
% 14.44/14.61 inference(symmetry,[status(thm)],[310])).
% 14.44/14.61 tff(312,plain,
% 14.44/14.61 ((~![X: $i] : (n(X) = a(X, X))) | (n(s(n(e))) = a(s(n(e)), s(n(e))))),
% 14.44/14.61 inference(quant_inst,[status(thm)],[])).
% 14.44/14.61 tff(313,plain,
% 14.44/14.61 (n(s(n(e))) = a(s(n(e)), s(n(e)))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[312, 53])).
% 14.44/14.61 tff(314,plain,
% 14.44/14.61 (a(s(n(e)), s(n(e))) = n(s(n(e)))),
% 14.44/14.61 inference(symmetry,[status(thm)],[313])).
% 14.44/14.61 tff(315,plain,
% 14.44/14.61 (u(n(e), n(s(n(e)))) = n(e)),
% 14.44/14.61 inference(transitivity,[status(thm)],[311, 56])).
% 14.44/14.61 tff(316,plain,
% 14.44/14.61 (u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) = u(n(e), n(s(n(e))))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[315, 314])).
% 14.44/14.61 tff(317,plain,
% 14.44/14.61 (u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) = a(e, e)),
% 14.44/14.61 inference(transitivity,[status(thm)],[316, 311])).
% 14.44/14.61 tff(318,plain,
% 14.44/14.61 (mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) <=> mem(a(e, e), a(e, e))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[311, 317])).
% 14.44/14.61 tff(319,plain,
% 14.44/14.61 (mem(a(e, e), a(e, e)) <=> mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))))),
% 14.44/14.61 inference(symmetry,[status(thm)],[318])).
% 14.44/14.61 tff(320,plain,
% 14.44/14.61 ((~mem(a(e, e), a(e, e))) <=> (~mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[319])).
% 14.44/14.61 tff(321,plain,
% 14.44/14.61 (mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e)) <=> mem(a(e, e), a(e, e))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[295])).
% 14.44/14.61 tff(322,plain,
% 14.44/14.61 ((~mem(tptp_fun_Z_0(s(e), a(n(e), n(e))), a(e, e))) <=> (~mem(a(e, e), a(e, e)))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[321])).
% 14.44/14.61 tff(323,plain,
% 14.44/14.61 (~mem(a(e, e), a(e, e))),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[290, 322])).
% 14.44/14.61 tff(324,plain,
% 14.44/14.61 (~mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))))),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[323, 320])).
% 14.44/14.61 tff(325,plain,
% 14.44/14.61 (mem(a(e, e), a(s(n(e)), s(n(e)))) <=> mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[310])).
% 14.44/14.61 tff(326,plain,
% 14.44/14.61 (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) <=> mem(a(e, e), a(s(n(e)), s(n(e))))),
% 14.44/14.61 inference(symmetry,[status(thm)],[325])).
% 14.44/14.61 tff(327,plain,
% 14.44/14.61 ((~mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) <=> (~mem(a(e, e), a(s(n(e)), s(n(e)))))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[326])).
% 14.44/14.61 tff(328,assumption,(~mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))), introduced(assumption)).
% 14.44/14.61 tff(329,plain,
% 14.44/14.61 (~mem(a(e, e), a(s(n(e)), s(n(e))))),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[328, 327])).
% 14.44/14.61 tff(330,plain,
% 14.44/14.61 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(s(n(e)), s(n(e))) = u(s(n(e)), s(s(n(e)))))),
% 14.44/14.61 inference(quant_inst,[status(thm)],[])).
% 14.44/14.61 tff(331,plain,
% 14.44/14.61 (a(s(n(e)), s(n(e))) = u(s(n(e)), s(s(n(e))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[330, 69])).
% 14.44/14.61 tff(332,plain,
% 14.44/14.61 (u(s(n(e)), s(s(n(e)))) = a(s(n(e)), s(n(e)))),
% 14.44/14.61 inference(symmetry,[status(thm)],[331])).
% 14.44/14.61 tff(333,plain,
% 14.44/14.61 (mem(a(e, e), u(s(n(e)), s(s(n(e))))) <=> mem(a(e, e), a(s(n(e)), s(n(e))))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[332])).
% 14.44/14.61 tff(334,plain,
% 14.44/14.61 (mem(a(e, e), a(s(n(e)), s(n(e)))) <=> mem(a(e, e), u(s(n(e)), s(s(n(e)))))),
% 14.44/14.61 inference(symmetry,[status(thm)],[333])).
% 14.44/14.61 tff(335,plain,
% 14.44/14.61 ((~mem(a(e, e), a(s(n(e)), s(n(e))))) <=> (~mem(a(e, e), u(s(n(e)), s(s(n(e))))))),
% 14.44/14.61 inference(monotonicity,[status(thm)],[334])).
% 14.44/14.61 tff(336,assumption,(~mem(a(e, e), a(s(n(e)), s(n(e))))), introduced(assumption)).
% 14.44/14.61 tff(337,plain,
% 14.44/14.61 (~mem(a(e, e), u(s(n(e)), s(s(n(e)))))),
% 14.44/14.61 inference(modus_ponens,[status(thm)],[336, 335])).
% 14.44/14.61 tff(338,plain,
% 14.44/14.61 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(e)), s(s(n(e))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e)))))),
% 14.44/14.61 inference(quant_inst,[status(thm)],[])).
% 14.44/14.61 tff(339,plain,
% 14.44/14.61 (mem(a(e, e), u(s(n(e)), s(s(n(e))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[338, 11])).
% 14.44/14.61 tff(340,plain,
% 14.44/14.61 ((mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e)))) | (~mem(a(e, e), s(n(e))))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(341,plain,
% 14.44/14.61 (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e)))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[340, 219])).
% 14.44/14.61 tff(342,plain,
% 14.44/14.61 ((~(mem(a(e, e), u(s(n(e)), s(s(n(e))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e)))))) | mem(a(e, e), u(s(n(e)), s(s(n(e))))) | (~(mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e)))))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(343,plain,
% 14.44/14.61 ((~(mem(a(e, e), u(s(n(e)), s(s(n(e))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(n(e)))))) | mem(a(e, e), u(s(n(e)), s(s(n(e)))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[342, 341])).
% 14.44/14.61 tff(344,plain,
% 14.44/14.61 (mem(a(e, e), u(s(n(e)), s(s(n(e)))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[343, 339])).
% 14.44/14.61 tff(345,plain,
% 14.44/14.61 ($false),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[344, 337])).
% 14.44/14.61 tff(346,plain,(mem(a(e, e), a(s(n(e)), s(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.61 tff(347,plain,
% 14.44/14.61 ($false),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[346, 329])).
% 14.44/14.61 tff(348,plain,(mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | (~(a(e, e) = u(n(e), n(s(n(e))))))), inference(lemma,lemma(discharge,[]))).
% 14.44/14.61 tff(349,plain,
% 14.44/14.61 (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[348, 310])).
% 14.44/14.61 tff(350,plain,
% 14.44/14.61 ((mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))) | (~mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))))),
% 14.44/14.61 inference(tautology,[status(thm)],[])).
% 14.44/14.61 tff(351,plain,
% 14.44/14.61 (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))),
% 14.44/14.61 inference(unit_resolution,[status(thm)],[350, 349])).
% 14.44/14.61 tff(352,assumption,(~(mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) <=> (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))))), introduced(assumption)).
% 14.44/14.61 tff(353,plain,
% 14.44/14.61 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) <=> (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))))),
% 14.44/14.61 inference(quant_inst,[status(thm)],[])).
% 14.46/14.61 tff(354,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[353, 11, 352])).
% 14.46/14.61 tff(355,plain,(mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) <=> (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e))))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(356,plain,
% 14.46/14.61 ((~(mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) <=> (mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))))) | mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) | (~(mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))))),
% 14.46/14.61 inference(tautology,[status(thm)],[])).
% 14.46/14.61 tff(357,plain,
% 14.46/14.61 (mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e))))) | (~(mem(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))) | mem(u(n(e), n(s(n(e)))), u(n(e), n(s(n(e)))))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[356, 355])).
% 14.46/14.61 tff(358,plain,
% 14.46/14.61 (mem(u(n(e), n(s(n(e)))), u(u(n(e), n(s(n(e)))), a(s(n(e)), s(n(e)))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[357, 351])).
% 14.46/14.61 tff(359,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[358, 324])).
% 14.46/14.61 tff(360,plain,(~(a(e, e) = u(n(e), n(s(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(361,assumption,(~(mem(a(e, e), s(u(n(e), n(s(n(e)))))) <=> (a(e, e) = u(n(e), n(s(n(e))))))), introduced(assumption)).
% 14.46/14.61 tff(362,plain,
% 14.46/14.61 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(u(n(e), n(s(n(e)))))) <=> (a(e, e) = u(n(e), n(s(n(e))))))),
% 14.46/14.61 inference(quant_inst,[status(thm)],[])).
% 14.46/14.61 tff(363,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[362, 38, 361])).
% 14.46/14.61 tff(364,plain,(mem(a(e, e), s(u(n(e), n(s(n(e)))))) <=> (a(e, e) = u(n(e), n(s(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(365,plain,
% 14.46/14.61 ((~(mem(a(e, e), s(u(n(e), n(s(n(e)))))) <=> (a(e, e) = u(n(e), n(s(n(e))))))) | (~mem(a(e, e), s(u(n(e), n(s(n(e))))))) | (a(e, e) = u(n(e), n(s(n(e)))))),
% 14.46/14.61 inference(tautology,[status(thm)],[])).
% 14.46/14.61 tff(366,plain,
% 14.46/14.61 ((~mem(a(e, e), s(u(n(e), n(s(n(e))))))) | (a(e, e) = u(n(e), n(s(n(e)))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[365, 364])).
% 14.46/14.61 tff(367,plain,
% 14.46/14.61 (~mem(a(e, e), s(u(n(e), n(s(n(e))))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[366, 360])).
% 14.46/14.61 tff(368,assumption,(a(e, e) = u(s(n(e)), s(n(n(e))))), introduced(assumption)).
% 14.46/14.61 tff(369,plain,
% 14.46/14.61 (u(s(n(e)), s(n(n(e)))) = a(e, e)),
% 14.46/14.61 inference(symmetry,[status(thm)],[368])).
% 14.46/14.61 tff(370,plain,
% 14.46/14.61 (mem(a(e, e), u(s(n(e)), s(n(n(e))))) <=> mem(a(e, e), a(e, e))),
% 14.46/14.61 inference(monotonicity,[status(thm)],[369])).
% 14.46/14.61 tff(371,plain,
% 14.46/14.61 (mem(a(e, e), a(e, e)) <=> mem(a(e, e), u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(symmetry,[status(thm)],[370])).
% 14.46/14.61 tff(372,plain,
% 14.46/14.61 ((~mem(a(e, e), a(e, e))) <=> (~mem(a(e, e), u(s(n(e)), s(n(n(e))))))),
% 14.46/14.61 inference(monotonicity,[status(thm)],[371])).
% 14.46/14.61 tff(373,plain,
% 14.46/14.61 (~mem(a(e, e), u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(modus_ponens,[status(thm)],[323, 372])).
% 14.46/14.61 tff(374,assumption,(~(mem(a(e, e), u(s(n(e)), s(n(n(e))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))))), introduced(assumption)).
% 14.46/14.61 tff(375,plain,
% 14.46/14.61 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(e)), s(n(n(e))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))))),
% 14.46/14.61 inference(quant_inst,[status(thm)],[])).
% 14.46/14.61 tff(376,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[375, 11, 374])).
% 14.46/14.61 tff(377,plain,(mem(a(e, e), u(s(n(e)), s(n(n(e))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(378,plain,
% 14.46/14.61 ((mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))) | (~mem(a(e, e), s(n(e))))),
% 14.46/14.61 inference(tautology,[status(thm)],[])).
% 14.46/14.61 tff(379,plain,
% 14.46/14.61 (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[378, 219])).
% 14.46/14.61 tff(380,plain,
% 14.46/14.61 ((~(mem(a(e, e), u(s(n(e)), s(n(n(e))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))))) | mem(a(e, e), u(s(n(e)), s(n(n(e))))) | (~(mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))))),
% 14.46/14.61 inference(tautology,[status(thm)],[])).
% 14.46/14.61 tff(381,plain,
% 14.46/14.61 ((~(mem(a(e, e), u(s(n(e)), s(n(n(e))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(n(e)))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[380, 379])).
% 14.46/14.61 tff(382,plain,
% 14.46/14.61 (mem(a(e, e), u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[381, 377])).
% 14.46/14.61 tff(383,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[382, 373])).
% 14.46/14.61 tff(384,plain,(~(a(e, e) = u(s(n(e)), s(n(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(385,assumption,(~(mem(a(e, e), s(u(s(n(e)), s(n(n(e)))))) <=> (a(e, e) = u(s(n(e)), s(n(n(e))))))), introduced(assumption)).
% 14.46/14.61 tff(386,plain,
% 14.46/14.61 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(u(s(n(e)), s(n(n(e)))))) <=> (a(e, e) = u(s(n(e)), s(n(n(e))))))),
% 14.46/14.61 inference(quant_inst,[status(thm)],[])).
% 14.46/14.61 tff(387,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[386, 38, 385])).
% 14.46/14.61 tff(388,plain,(mem(a(e, e), s(u(s(n(e)), s(n(n(e)))))) <=> (a(e, e) = u(s(n(e)), s(n(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(389,plain,
% 14.46/14.61 ((~(mem(a(e, e), s(u(s(n(e)), s(n(n(e)))))) <=> (a(e, e) = u(s(n(e)), s(n(n(e))))))) | (~mem(a(e, e), s(u(s(n(e)), s(n(n(e))))))) | (a(e, e) = u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(tautology,[status(thm)],[])).
% 14.46/14.61 tff(390,plain,
% 14.46/14.61 ((~mem(a(e, e), s(u(s(n(e)), s(n(n(e))))))) | (a(e, e) = u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[389, 388])).
% 14.46/14.61 tff(391,plain,
% 14.46/14.61 (~mem(a(e, e), s(u(s(n(e)), s(n(n(e))))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[390, 384])).
% 14.46/14.61 tff(392,plain,
% 14.46/14.61 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(s(n(e)), n(n(e))) = u(s(n(e)), s(n(n(e)))))),
% 14.46/14.61 inference(quant_inst,[status(thm)],[])).
% 14.46/14.61 tff(393,plain,
% 14.46/14.61 (a(s(n(e)), n(n(e))) = u(s(n(e)), s(n(n(e))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[392, 69])).
% 14.46/14.61 tff(394,plain,
% 14.46/14.61 (u(s(n(e)), s(n(n(e)))) = a(s(n(e)), n(n(e)))),
% 14.46/14.61 inference(symmetry,[status(thm)],[393])).
% 14.46/14.61 tff(395,plain,
% 14.46/14.61 (s(u(s(n(e)), s(n(n(e))))) = s(a(s(n(e)), n(n(e))))),
% 14.46/14.61 inference(monotonicity,[status(thm)],[394])).
% 14.46/14.61 tff(396,plain,
% 14.46/14.61 (mem(a(e, e), s(u(s(n(e)), s(n(n(e)))))) <=> mem(a(e, e), s(a(s(n(e)), n(n(e)))))),
% 14.46/14.61 inference(monotonicity,[status(thm)],[395])).
% 14.46/14.61 tff(397,plain,
% 14.46/14.61 (mem(a(e, e), s(a(s(n(e)), n(n(e))))) <=> mem(a(e, e), s(u(s(n(e)), s(n(n(e))))))),
% 14.46/14.61 inference(symmetry,[status(thm)],[396])).
% 14.46/14.61 tff(398,assumption,(mem(a(e, e), s(a(s(n(e)), n(n(e)))))), introduced(assumption)).
% 14.46/14.61 tff(399,plain,
% 14.46/14.61 (mem(a(e, e), s(u(s(n(e)), s(n(n(e))))))),
% 14.46/14.61 inference(modus_ponens,[status(thm)],[398, 397])).
% 14.46/14.61 tff(400,assumption,(~mem(a(e, e), s(u(s(n(e)), s(n(n(e))))))), introduced(assumption)).
% 14.46/14.61 tff(401,plain,
% 14.46/14.61 ($false),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[400, 399])).
% 14.46/14.61 tff(402,plain,(mem(a(e, e), s(u(s(n(e)), s(n(n(e)))))) | (~mem(a(e, e), s(a(s(n(e)), n(n(e))))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.61 tff(403,plain,
% 14.46/14.61 (~mem(a(e, e), s(a(s(n(e)), n(n(e)))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[402, 391])).
% 14.46/14.61 tff(404,plain,
% 14.46/14.61 ((~(mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))) | mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))),
% 14.46/14.61 inference(tautology,[status(thm)],[])).
% 14.46/14.61 tff(405,plain,
% 14.46/14.61 ((~(mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[404, 403])).
% 14.46/14.61 tff(406,plain,
% 14.46/14.61 (~(mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))),
% 14.46/14.61 inference(unit_resolution,[status(thm)],[405, 367])).
% 14.46/14.61 tff(407,assumption,(~(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))), introduced(assumption)).
% 14.46/14.61 tff(408,plain,
% 14.46/14.61 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(409,plain,
% 14.46/14.62 ($false),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[408, 11, 407])).
% 14.46/14.62 tff(410,plain,(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.62 tff(411,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))) | (~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) | (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(412,plain,
% 14.46/14.62 ((~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) | (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[411, 410])).
% 14.46/14.62 tff(413,plain,
% 14.46/14.62 (~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[412, 406])).
% 14.46/14.62 tff(414,assumption,(~(mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))))), introduced(assumption)).
% 14.46/14.62 tff(415,plain,
% 14.46/14.62 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(416,plain,
% 14.46/14.62 ($false),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[415, 11, 414])).
% 14.46/14.62 tff(417,plain,(mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.62 tff(418,plain,
% 14.46/14.62 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))) = u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(419,plain,
% 14.46/14.62 (a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))) = u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[418, 69])).
% 14.46/14.62 tff(420,plain,
% 14.46/14.62 (u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))) = a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[419])).
% 14.46/14.62 tff(421,plain,
% 14.46/14.62 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))) = u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(422,plain,
% 14.46/14.62 (a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))) = u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[421, 69])).
% 14.46/14.62 tff(423,plain,
% 14.46/14.62 (u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))) = a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[422])).
% 14.46/14.62 tff(424,plain,
% 14.46/14.62 (u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) = u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[423, 420])).
% 14.46/14.62 tff(425,plain,
% 14.46/14.62 (mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) <=> mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[424])).
% 14.46/14.62 tff(426,plain,
% 14.46/14.62 (mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))) <=> mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[425])).
% 14.46/14.62 tff(427,plain,
% 14.46/14.62 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))) = u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(428,plain,
% 14.46/14.62 (a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))) = u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e)))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[427, 69])).
% 14.46/14.62 tff(429,plain,
% 14.46/14.62 (u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))) = a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[428])).
% 14.46/14.62 tff(430,plain,
% 14.46/14.62 (u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) = u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[429])).
% 14.46/14.62 tff(431,plain,
% 14.46/14.62 (mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[430])).
% 14.46/14.62 tff(432,plain,
% 14.46/14.62 (mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[431])).
% 14.46/14.62 tff(433,plain,
% 14.46/14.62 ((~mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) <=> (~mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[432])).
% 14.46/14.62 tff(434,assumption,(~mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))), introduced(assumption)).
% 14.46/14.62 tff(435,plain,
% 14.46/14.62 (~mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(modus_ponens,[status(thm)],[434, 433])).
% 14.46/14.62 tff(436,plain,
% 14.46/14.62 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(437,plain,
% 14.46/14.62 (mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e)))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[436, 11])).
% 14.46/14.62 tff(438,plain,
% 14.46/14.62 ((~![X: $i] : (n(X) = a(X, X))) | (n(a(s(n(e)), n(n(e)))) = a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(439,plain,
% 14.46/14.62 (n(a(s(n(e)), n(n(e)))) = a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[438, 53])).
% 14.46/14.62 tff(440,plain,
% 14.46/14.62 (a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))) = n(a(s(n(e)), n(n(e))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[439])).
% 14.46/14.62 tff(441,plain,
% 14.46/14.62 (u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) = u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[440])).
% 14.46/14.62 tff(442,plain,
% 14.46/14.62 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) <=> mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[441])).
% 14.46/14.62 tff(443,plain,
% 14.46/14.62 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) <=> mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[442])).
% 14.46/14.62 tff(444,plain,
% 14.46/14.62 ((~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> (~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[443])).
% 14.46/14.62 tff(445,assumption,(~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), introduced(assumption)).
% 14.46/14.62 tff(446,plain,
% 14.46/14.62 (~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(modus_ponens,[status(thm)],[445, 444])).
% 14.46/14.62 tff(447,plain,
% 14.46/14.62 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(448,plain,
% 14.46/14.62 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e)))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[447, 11])).
% 14.46/14.62 tff(449,plain,
% 14.46/14.62 (a(u(s(n(e)), s(n(n(e)))), u(s(n(e)), s(n(n(e))))) = a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[394, 394])).
% 14.46/14.62 tff(450,plain,
% 14.46/14.62 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(u(s(n(e)), s(n(n(e)))), u(s(n(e)), s(n(n(e))))) = u(u(s(n(e)), s(n(n(e)))), s(u(s(n(e)), s(n(n(e)))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(451,plain,
% 14.46/14.62 (a(u(s(n(e)), s(n(n(e)))), u(s(n(e)), s(n(n(e))))) = u(u(s(n(e)), s(n(n(e)))), s(u(s(n(e)), s(n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[450, 69])).
% 14.46/14.62 tff(452,plain,
% 14.46/14.62 (u(u(s(n(e)), s(n(n(e)))), s(u(s(n(e)), s(n(n(e)))))) = a(u(s(n(e)), s(n(n(e)))), u(s(n(e)), s(n(n(e)))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[451])).
% 14.46/14.62 tff(453,plain,
% 14.46/14.62 (s(a(s(n(e)), n(n(e)))) = s(u(s(n(e)), s(n(n(e)))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[395])).
% 14.46/14.62 tff(454,plain,
% 14.46/14.62 (u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e))))) = u(u(s(n(e)), s(n(n(e)))), s(u(s(n(e)), s(n(n(e))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[453])).
% 14.46/14.62 tff(455,plain,
% 14.46/14.62 (u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e))))) = a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))),
% 14.46/14.62 inference(transitivity,[status(thm)],[454, 452, 449])).
% 14.46/14.62 tff(456,plain,
% 14.46/14.62 (mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))) <=> mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[455])).
% 14.46/14.62 tff(457,plain,
% 14.46/14.62 (mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) <=> mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(symmetry,[status(thm)],[456])).
% 14.46/14.62 tff(458,plain,
% 14.46/14.62 ((~mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) <=> (~mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(monotonicity,[status(thm)],[457])).
% 14.46/14.62 tff(459,assumption,(~mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))), introduced(assumption)).
% 14.46/14.62 tff(460,plain,
% 14.46/14.62 (~mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(modus_ponens,[status(thm)],[459, 458])).
% 14.46/14.62 tff(461,plain,
% 14.46/14.62 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))))),
% 14.46/14.62 inference(quant_inst,[status(thm)],[])).
% 14.46/14.62 tff(462,plain,
% 14.46/14.62 (mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[461, 11])).
% 14.46/14.62 tff(463,plain,
% 14.46/14.62 ((mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))) | (~mem(a(e, e), u(s(n(e)), s(n(n(e))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(464,plain,
% 14.46/14.62 (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[463, 382])).
% 14.46/14.62 tff(465,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))))) | mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))) | (~(mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(466,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), s(a(s(n(e)), n(n(e))))) | mem(a(e, e), u(s(n(e)), s(n(n(e)))))))) | mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[465, 464])).
% 14.46/14.62 tff(467,plain,
% 14.46/14.62 (mem(a(e, e), u(u(s(n(e)), s(n(n(e)))), s(a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[466, 462])).
% 14.46/14.62 tff(468,plain,
% 14.46/14.62 ($false),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[467, 460])).
% 14.46/14.62 tff(469,plain,(mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.62 tff(470,plain,
% 14.46/14.62 ((mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))) | (~mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(471,plain,
% 14.46/14.62 (mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[470, 469])).
% 14.46/14.62 tff(472,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))) | mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) | (~(mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(473,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e)))))) <=> (mem(a(e, e), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))) | mem(a(e, e), s(u(n(e), n(s(n(e))))))))) | mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[472, 471])).
% 14.46/14.62 tff(474,plain,
% 14.46/14.62 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), a(a(s(n(e)), n(n(e))), a(s(n(e)), n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[473, 448])).
% 14.46/14.62 tff(475,plain,
% 14.46/14.62 ($false),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[474, 446])).
% 14.46/14.62 tff(476,plain,(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.62 tff(477,plain,
% 14.46/14.62 ((mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))) | (~mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(478,plain,
% 14.46/14.62 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))),
% 14.46/14.62 inference(unit_resolution,[status(thm)],[477, 476])).
% 14.46/14.62 tff(479,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))))) | mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) | (~(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))))),
% 14.46/14.62 inference(tautology,[status(thm)],[])).
% 14.46/14.62 tff(480,plain,
% 14.46/14.62 ((~(mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))))))) | mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))),
% 14.46/14.63 inference(unit_resolution,[status(thm)],[479, 478])).
% 14.46/14.63 tff(481,plain,
% 14.46/14.63 (mem(a(e, e), u(u(a(n(s(s(n(e)))), s(n(n(e)))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))),
% 14.46/14.63 inference(unit_resolution,[status(thm)],[480, 437])).
% 14.46/14.63 tff(482,plain,
% 14.46/14.63 ($false),
% 14.46/14.63 inference(unit_resolution,[status(thm)],[481, 435])).
% 14.46/14.63 tff(483,plain,(mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))), inference(lemma,lemma(discharge,[]))).
% 14.46/14.63 tff(484,plain,
% 14.46/14.63 ((~![X: $i, Y: $i] : (~((~((~subq(X, Y)) | ![Z: $i] : ((~mem(Z, X)) | mem(Z, Y)))) | (~(subq(X, Y) | (~((~mem(tptp_fun_Z_0(Y, X), X)) | mem(tptp_fun_Z_0(Y, X), Y)))))))) | (~((~((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))) | (~(subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))) | (~((~mem(tptp_fun_Z_0(u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(tptp_fun_Z_0(u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))))))),
% 14.46/14.63 inference(quant_inst,[status(thm)],[])).
% 14.46/14.63 tff(485,plain,
% 14.46/14.63 (~((~((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))) | (~(subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))) | (~((~mem(tptp_fun_Z_0(u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(tptp_fun_Z_0(u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))))))),
% 14.46/14.63 inference(unit_resolution,[status(thm)],[484, 254])).
% 14.46/14.63 tff(486,plain,
% 14.46/14.63 (((~((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))) | (~(subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))) | (~((~mem(tptp_fun_Z_0(u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(tptp_fun_Z_0(u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e))))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))))) | ((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))),
% 14.46/14.63 inference(tautology,[status(thm)],[])).
% 14.46/14.63 tff(487,plain,
% 14.46/14.63 ((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))),
% 14.46/14.63 inference(unit_resolution,[status(thm)],[486, 485])).
% 14.46/14.63 tff(488,plain,
% 14.46/14.63 (subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))) <=> subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.46/14.63 inference(rewrite,[status(thm)],[])).
% 14.46/14.63 tff(489,plain,
% 14.46/14.63 ((~(~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))) <=> subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.46/14.63 inference(rewrite,[status(thm)],[])).
% 14.46/14.63 tff(490,axiom,(~(~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','nsubq_1950_1948')).
% 14.46/14.63 tff(491,plain,
% 14.46/14.63 (subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.46/14.63 inference(modus_ponens,[status(thm)],[490, 489])).
% 14.46/14.63 tff(492,plain,
% 14.46/14.63 (subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.46/14.63 inference(modus_ponens,[status(thm)],[491, 488])).
% 14.46/14.63 tff(493,plain,
% 14.46/14.63 ((~((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))) | (~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))),
% 14.48/14.63 inference(tautology,[status(thm)],[])).
% 14.48/14.63 tff(494,plain,
% 14.48/14.63 ((~((~subq(u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))))) | ![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))),
% 14.48/14.63 inference(unit_resolution,[status(thm)],[493, 492])).
% 14.48/14.63 tff(495,plain,
% 14.48/14.63 (![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))),
% 14.48/14.63 inference(unit_resolution,[status(thm)],[494, 487])).
% 14.48/14.63 tff(496,plain,
% 14.48/14.63 (((~![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))) | ((~mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))) <=> ((~![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))) | (~mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))),
% 14.48/14.63 inference(rewrite,[status(thm)],[])).
% 14.48/14.63 tff(497,plain,
% 14.48/14.63 ((~![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))) | ((~mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))),
% 14.48/14.63 inference(quant_inst,[status(thm)],[])).
% 14.48/14.63 tff(498,plain,
% 14.48/14.63 ((~![Z: $i] : ((~mem(Z, u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(Z, u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e)))))))) | (~mem(a(e, e), u(a(a(n(s(s(n(e)))), s(n(n(e)))), a(n(e), n(n(e)))), u(s(u(n(e), n(s(n(e))))), n(a(s(n(e)), n(n(e)))))))) | mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.48/14.63 inference(modus_ponens,[status(thm)],[497, 496])).
% 14.48/14.64 tff(499,plain,
% 14.48/14.64 (mem(a(e, e), u(a(u(n(s(s(n(e)))), n(s(n(n(e))))), a(n(e), n(n(e)))), a(s(u(n(e), n(s(n(e))))), a(s(n(e)), n(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[498, 495, 483])).
% 14.48/14.64 tff(500,plain,
% 14.48/14.64 (mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[499, 426])).
% 14.48/14.64 tff(501,assumption,(~mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))))), introduced(assumption)).
% 14.48/14.64 tff(502,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[501, 500])).
% 14.48/14.64 tff(503,plain,(mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(504,plain,
% 14.48/14.64 ((~(mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))))) | (~mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))))) | (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(505,plain,
% 14.48/14.64 ((~(mem(a(e, e), u(u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e))))))) <=> (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))))) | (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[504, 503])).
% 14.48/14.64 tff(506,plain,
% 14.48/14.64 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[505, 417])).
% 14.48/14.64 tff(507,plain,
% 14.48/14.64 ((~(mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))))) | mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(508,plain,
% 14.48/14.64 (mem(a(e, e), u(s(u(n(e), n(s(n(e))))), s(a(s(n(e)), n(n(e)))))) | mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[507, 506])).
% 14.48/14.64 tff(509,plain,
% 14.48/14.64 (mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[508, 413])).
% 14.48/14.64 tff(510,assumption,(~(mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))) <=> (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))))), introduced(assumption)).
% 14.48/14.64 tff(511,plain,
% 14.48/14.64 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))) <=> (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(512,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[511, 11, 510])).
% 14.48/14.64 tff(513,plain,(mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))) <=> (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e)))))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(514,plain,
% 14.48/14.64 ((~(mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e)))))) <=> (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))))) | (~mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))) | (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e)))))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(515,plain,
% 14.48/14.64 ((~mem(a(e, e), u(u(n(s(s(n(e)))), n(s(n(n(e))))), s(a(n(e), n(n(e))))))) | (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e)))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[514, 513])).
% 14.48/14.64 tff(516,plain,
% 14.48/14.64 (mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[515, 509])).
% 14.48/14.64 tff(517,assumption,(a(e, e) = s(s(n(e)))), introduced(assumption)).
% 14.48/14.64 tff(518,plain,
% 14.48/14.64 (s(s(n(e))) = a(e, e)),
% 14.48/14.64 inference(symmetry,[status(thm)],[517])).
% 14.48/14.64 tff(519,plain,
% 14.48/14.64 (mem(s(n(e)), s(s(n(e)))) <=> mem(s(n(e)), a(e, e))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[518])).
% 14.48/14.64 tff(520,plain,
% 14.48/14.64 (mem(s(n(e)), a(e, e)) <=> mem(s(n(e)), s(s(n(e))))),
% 14.48/14.64 inference(symmetry,[status(thm)],[519])).
% 14.48/14.64 tff(521,plain,
% 14.48/14.64 ((~mem(s(n(e)), a(e, e))) <=> (~mem(s(n(e)), s(s(n(e)))))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[520])).
% 14.48/14.64 tff(522,assumption,(mem(a(s(n(e)), s(n(e))), e)), introduced(assumption)).
% 14.48/14.64 tff(523,plain,
% 14.48/14.64 ((~![X: $i] : (~mem(X, e))) | (~mem(a(s(n(e)), s(n(e))), e))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(524,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[523, 27, 522])).
% 14.48/14.64 tff(525,plain,(~mem(a(s(n(e)), s(n(e))), e)), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(526,assumption,(s(n(e)) = e), introduced(assumption)).
% 14.48/14.64 tff(527,plain,
% 14.48/14.64 (e = s(n(e))),
% 14.48/14.64 inference(symmetry,[status(thm)],[526])).
% 14.48/14.64 tff(528,plain,
% 14.48/14.64 (n(e) = n(s(n(e)))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[527])).
% 14.48/14.64 tff(529,plain,
% 14.48/14.64 (n(s(n(e))) = n(e)),
% 14.48/14.64 inference(symmetry,[status(thm)],[528])).
% 14.48/14.64 tff(530,plain,
% 14.48/14.64 (a(s(n(e)), s(n(e))) = a(e, e)),
% 14.48/14.64 inference(transitivity,[status(thm)],[314, 529, 55])).
% 14.48/14.64 tff(531,plain,
% 14.48/14.64 (mem(a(s(n(e)), s(n(e))), e) <=> mem(a(e, e), s(n(e)))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[530, 527])).
% 14.48/14.64 tff(532,plain,
% 14.48/14.64 (mem(a(e, e), s(n(e))) <=> mem(a(s(n(e)), s(n(e))), e)),
% 14.48/14.64 inference(symmetry,[status(thm)],[531])).
% 14.48/14.64 tff(533,plain,
% 14.48/14.64 (mem(a(s(n(e)), s(n(e))), e)),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[219, 532])).
% 14.48/14.64 tff(534,assumption,(~mem(a(s(n(e)), s(n(e))), e)), introduced(assumption)).
% 14.48/14.64 tff(535,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[534, 533])).
% 14.48/14.64 tff(536,plain,(mem(a(s(n(e)), s(n(e))), e) | (~(s(n(e)) = e))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(537,plain,
% 14.48/14.64 (~(s(n(e)) = e)),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[536, 525])).
% 14.48/14.64 tff(538,assumption,(~(mem(s(n(e)), s(e)) <=> (s(n(e)) = e))), introduced(assumption)).
% 14.48/14.64 tff(539,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(s(n(e)), s(e)) <=> (s(n(e)) = e))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(540,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[539, 38, 538])).
% 14.48/14.64 tff(541,plain,(mem(s(n(e)), s(e)) <=> (s(n(e)) = e)), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(542,plain,
% 14.48/14.64 ((~(mem(s(n(e)), s(e)) <=> (s(n(e)) = e))) | (~mem(s(n(e)), s(e))) | (s(n(e)) = e)),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(543,plain,
% 14.48/14.64 ((~mem(s(n(e)), s(e))) | (s(n(e)) = e)),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[542, 541])).
% 14.48/14.64 tff(544,plain,
% 14.48/14.64 (~mem(s(n(e)), s(e))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[543, 537])).
% 14.48/14.64 tff(545,plain,
% 14.48/14.64 (mem(s(n(e)), u(e, s(e))) <=> mem(s(n(e)), a(e, e))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[116])).
% 14.48/14.64 tff(546,plain,
% 14.48/14.64 (mem(s(n(e)), a(e, e)) <=> mem(s(n(e)), u(e, s(e)))),
% 14.48/14.64 inference(symmetry,[status(thm)],[545])).
% 14.48/14.64 tff(547,assumption,(mem(s(n(e)), a(e, e))), introduced(assumption)).
% 14.48/14.64 tff(548,plain,
% 14.48/14.64 (mem(s(n(e)), u(e, s(e)))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[547, 546])).
% 14.48/14.64 tff(549,plain,
% 14.48/14.64 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(s(n(e)), u(e, s(e))) <=> (mem(s(n(e)), s(e)) | mem(s(n(e)), e)))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(550,plain,
% 14.48/14.64 (mem(s(n(e)), u(e, s(e))) <=> (mem(s(n(e)), s(e)) | mem(s(n(e)), e))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[549, 11])).
% 14.48/14.64 tff(551,assumption,(mem(s(n(e)), e)), introduced(assumption)).
% 14.48/14.64 tff(552,plain,
% 14.48/14.64 ((~![X: $i] : (~mem(X, e))) | (~mem(s(n(e)), e))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(553,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[552, 27, 551])).
% 14.48/14.64 tff(554,plain,(~mem(s(n(e)), e)), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(555,assumption,(~mem(s(n(e)), s(e))), introduced(assumption)).
% 14.48/14.64 tff(556,plain,
% 14.48/14.64 ((~(mem(s(n(e)), s(e)) | mem(s(n(e)), e))) | mem(s(n(e)), s(e)) | mem(s(n(e)), e)),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(557,plain,
% 14.48/14.64 (~(mem(s(n(e)), s(e)) | mem(s(n(e)), e))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[556, 555, 554])).
% 14.48/14.64 tff(558,plain,
% 14.48/14.64 ((~(mem(s(n(e)), u(e, s(e))) <=> (mem(s(n(e)), s(e)) | mem(s(n(e)), e)))) | (~mem(s(n(e)), u(e, s(e)))) | (mem(s(n(e)), s(e)) | mem(s(n(e)), e))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(559,plain,
% 14.48/14.64 ((~(mem(s(n(e)), u(e, s(e))) <=> (mem(s(n(e)), s(e)) | mem(s(n(e)), e)))) | (~mem(s(n(e)), u(e, s(e))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[558, 557])).
% 14.48/14.64 tff(560,plain,
% 14.48/14.64 (~mem(s(n(e)), u(e, s(e)))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[559, 550])).
% 14.48/14.64 tff(561,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[560, 548])).
% 14.48/14.64 tff(562,plain,((~mem(s(n(e)), a(e, e))) | mem(s(n(e)), s(e))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(563,plain,
% 14.48/14.64 (~mem(s(n(e)), a(e, e))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[562, 544])).
% 14.48/14.64 tff(564,plain,
% 14.48/14.64 (~mem(s(n(e)), s(s(n(e))))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[563, 521])).
% 14.48/14.64 tff(565,assumption,(~mem(s(n(e)), s(s(n(e))))), introduced(assumption)).
% 14.48/14.64 tff(566,plain,
% 14.48/14.64 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(s(n(e)), s(s(n(e))))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(s(n(e)), s(s(n(e)))))),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(567,plain,
% 14.48/14.64 ((mem(s(n(e)), s(s(n(e)))) <=> $true) <=> mem(s(n(e)), s(s(n(e))))),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(568,plain,
% 14.48/14.64 ((s(n(e)) = s(n(e))) <=> $true),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(569,plain,
% 14.48/14.64 ((mem(s(n(e)), s(s(n(e)))) <=> (s(n(e)) = s(n(e)))) <=> (mem(s(n(e)), s(s(n(e)))) <=> $true)),
% 14.48/14.64 inference(monotonicity,[status(thm)],[568])).
% 14.48/14.64 tff(570,plain,
% 14.48/14.64 ((mem(s(n(e)), s(s(n(e)))) <=> (s(n(e)) = s(n(e)))) <=> mem(s(n(e)), s(s(n(e))))),
% 14.48/14.64 inference(transitivity,[status(thm)],[569, 567])).
% 14.48/14.64 tff(571,plain,
% 14.48/14.64 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(s(n(e)), s(s(n(e)))) <=> (s(n(e)) = s(n(e))))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(s(n(e)), s(s(n(e)))))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[570])).
% 14.48/14.64 tff(572,plain,
% 14.48/14.64 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(s(n(e)), s(s(n(e)))) <=> (s(n(e)) = s(n(e))))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(s(n(e)), s(s(n(e)))))),
% 14.48/14.64 inference(transitivity,[status(thm)],[571, 566])).
% 14.48/14.64 tff(573,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(s(n(e)), s(s(n(e)))) <=> (s(n(e)) = s(n(e))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(574,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(s(n(e)), s(s(n(e))))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[573, 572])).
% 14.48/14.64 tff(575,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[574, 38, 565])).
% 14.48/14.64 tff(576,plain,(mem(s(n(e)), s(s(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(577,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[576, 564])).
% 14.48/14.64 tff(578,plain,(~(a(e, e) = s(s(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(579,assumption,(~(mem(a(e, e), s(s(s(n(e))))) <=> (a(e, e) = s(s(n(e)))))), introduced(assumption)).
% 14.48/14.64 tff(580,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(s(s(n(e))))) <=> (a(e, e) = s(s(n(e)))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(581,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[580, 38, 579])).
% 14.48/14.64 tff(582,plain,(mem(a(e, e), s(s(s(n(e))))) <=> (a(e, e) = s(s(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(583,plain,
% 14.48/14.64 ((~(mem(a(e, e), s(s(s(n(e))))) <=> (a(e, e) = s(s(n(e)))))) | (~mem(a(e, e), s(s(s(n(e)))))) | (a(e, e) = s(s(n(e))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(584,plain,
% 14.48/14.64 ((~mem(a(e, e), s(s(s(n(e)))))) | (a(e, e) = s(s(n(e))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[583, 582])).
% 14.48/14.64 tff(585,plain,
% 14.48/14.64 (~mem(a(e, e), s(s(s(n(e)))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[584, 578])).
% 14.48/14.64 tff(586,assumption,(mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))), introduced(assumption)).
% 14.48/14.64 tff(587,assumption,(~mem(a(e, e), s(s(s(n(e)))))), introduced(assumption)).
% 14.48/14.64 tff(588,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(s(s(n(e))), s(s(n(e)))) = u(s(s(n(e))), s(s(s(n(e))))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(589,plain,
% 14.48/14.64 (a(s(s(n(e))), s(s(n(e)))) = u(s(s(n(e))), s(s(s(n(e)))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[588, 69])).
% 14.48/14.64 tff(590,plain,
% 14.48/14.64 (u(s(s(n(e))), s(s(s(n(e))))) = a(s(s(n(e))), s(s(n(e))))),
% 14.48/14.64 inference(symmetry,[status(thm)],[589])).
% 14.48/14.64 tff(591,plain,
% 14.48/14.64 (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[590])).
% 14.48/14.64 tff(592,plain,
% 14.48/14.64 (mem(a(e, e), a(s(s(n(e))), s(s(n(e))))) <=> mem(a(e, e), u(s(s(n(e))), s(s(s(n(e))))))),
% 14.48/14.64 inference(symmetry,[status(thm)],[591])).
% 14.48/14.64 tff(593,plain,
% 14.48/14.64 (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e))))))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[586, 592])).
% 14.48/14.64 tff(594,plain,
% 14.48/14.64 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))))),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(595,plain,
% 14.48/14.64 ((mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(s(n(e))))) | mem(a(e, e), s(s(n(e)))))) <=> (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))))),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(596,plain,
% 14.48/14.64 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(s(n(e))))) | mem(a(e, e), s(s(n(e))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[595])).
% 14.48/14.64 tff(597,plain,
% 14.48/14.64 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(s(n(e))))) | mem(a(e, e), s(s(n(e))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))))),
% 14.48/14.64 inference(transitivity,[status(thm)],[596, 594])).
% 14.48/14.64 tff(598,plain,
% 14.48/14.64 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(s(n(e))))) | mem(a(e, e), s(s(n(e))))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(599,plain,
% 14.48/14.64 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[598, 597])).
% 14.48/14.64 tff(600,plain,
% 14.48/14.64 (mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[599, 11])).
% 14.48/14.64 tff(601,assumption,(~mem(a(e, e), s(s(n(e))))), introduced(assumption)).
% 14.48/14.64 tff(602,plain,
% 14.48/14.64 ((~(mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))) | mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(603,plain,
% 14.48/14.64 (~(mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[602, 601, 587])).
% 14.48/14.64 tff(604,plain,
% 14.48/14.64 ((~(mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))))) | (~mem(a(e, e), u(s(s(n(e))), s(s(s(n(e))))))) | (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e))))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(605,plain,
% 14.48/14.64 ((~(mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))) <=> (mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))))) | (~mem(a(e, e), u(s(s(n(e))), s(s(s(n(e)))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[604, 603])).
% 14.48/14.64 tff(606,plain,
% 14.48/14.64 (~mem(a(e, e), u(s(s(n(e))), s(s(s(n(e))))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[605, 600])).
% 14.48/14.64 tff(607,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[606, 593])).
% 14.48/14.64 tff(608,plain,((~mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))) | mem(a(e, e), s(s(n(e)))) | mem(a(e, e), s(s(s(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(609,plain,
% 14.48/14.64 (mem(a(e, e), s(s(n(e))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[608, 587, 586])).
% 14.48/14.64 tff(610,assumption,(~(mem(a(e, e), s(s(n(e)))) <=> (a(e, e) = s(n(e))))), introduced(assumption)).
% 14.48/14.64 tff(611,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(s(n(e)))) <=> (a(e, e) = s(n(e))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(612,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[611, 38, 610])).
% 14.48/14.64 tff(613,plain,(mem(a(e, e), s(s(n(e)))) <=> (a(e, e) = s(n(e)))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(614,plain,
% 14.48/14.64 ((~(mem(a(e, e), s(s(n(e)))) <=> (a(e, e) = s(n(e))))) | (~mem(a(e, e), s(s(n(e))))) | (a(e, e) = s(n(e)))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(615,plain,
% 14.48/14.64 ((~mem(a(e, e), s(s(n(e))))) | (a(e, e) = s(n(e)))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[614, 613])).
% 14.48/14.64 tff(616,plain,
% 14.48/14.64 (a(e, e) = s(n(e))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[615, 609])).
% 14.48/14.64 tff(617,plain,
% 14.48/14.64 (s(n(e)) = a(e, e)),
% 14.48/14.64 inference(symmetry,[status(thm)],[616])).
% 14.48/14.64 tff(618,plain,
% 14.48/14.64 (s(n(e)) = n(e)),
% 14.48/14.64 inference(transitivity,[status(thm)],[617, 56])).
% 14.48/14.64 tff(619,plain,
% 14.48/14.64 (s(s(n(e))) = s(n(e))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[618])).
% 14.48/14.64 tff(620,plain,
% 14.48/14.64 (s(n(e)) = s(s(n(e)))),
% 14.48/14.64 inference(symmetry,[status(thm)],[619])).
% 14.48/14.64 tff(621,plain,
% 14.48/14.64 (a(e, e) = s(s(n(e)))),
% 14.48/14.64 inference(transitivity,[status(thm)],[616, 620])).
% 14.48/14.64 tff(622,plain,
% 14.48/14.64 ((~(mem(a(e, e), s(s(s(n(e))))) <=> (a(e, e) = s(s(n(e)))))) | mem(a(e, e), s(s(s(n(e))))) | (~(a(e, e) = s(s(n(e)))))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(623,plain,
% 14.48/14.64 (mem(a(e, e), s(s(s(n(e))))) | (~(a(e, e) = s(s(n(e)))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[622, 582])).
% 14.48/14.64 tff(624,plain,
% 14.48/14.64 (~(a(e, e) = s(s(n(e))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[623, 587])).
% 14.48/14.64 tff(625,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[624, 621])).
% 14.48/14.64 tff(626,plain,(mem(a(e, e), s(s(s(n(e))))) | (~mem(a(e, e), a(s(s(n(e))), s(s(n(e))))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(627,plain,
% 14.48/14.64 (~mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[626, 585])).
% 14.48/14.64 tff(628,assumption,(a(e, e) = s(n(n(e)))), introduced(assumption)).
% 14.48/14.64 tff(629,plain,
% 14.48/14.64 (s(n(n(e))) = a(e, e)),
% 14.48/14.64 inference(symmetry,[status(thm)],[628])).
% 14.48/14.64 tff(630,plain,
% 14.48/14.64 (s(a(n(e), n(e))) = a(e, e)),
% 14.48/14.64 inference(transitivity,[status(thm)],[100, 629])).
% 14.48/14.64 tff(631,plain,
% 14.48/14.64 (mem(e, s(a(n(e), n(e)))) <=> mem(e, a(e, e))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[630])).
% 14.48/14.64 tff(632,plain,
% 14.48/14.64 (mem(e, a(e, e)) <=> mem(e, s(a(n(e), n(e))))),
% 14.48/14.64 inference(symmetry,[status(thm)],[631])).
% 14.48/14.64 tff(633,plain,
% 14.48/14.64 (mem(e, u(e, s(e))) <=> mem(e, a(e, e))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[116])).
% 14.48/14.64 tff(634,plain,
% 14.48/14.64 (mem(e, a(e, e)) <=> mem(e, u(e, s(e)))),
% 14.48/14.64 inference(symmetry,[status(thm)],[633])).
% 14.48/14.64 tff(635,plain,
% 14.48/14.64 ((~mem(e, a(e, e))) <=> (~mem(e, u(e, s(e))))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[634])).
% 14.48/14.64 tff(636,assumption,(~mem(e, a(e, e))), introduced(assumption)).
% 14.48/14.64 tff(637,plain,
% 14.48/14.64 (~mem(e, u(e, s(e)))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[636, 635])).
% 14.48/14.64 tff(638,plain,
% 14.48/14.64 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(e, u(e, s(e))) <=> (mem(e, s(e)) | mem(e, e)))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(639,plain,
% 14.48/14.64 (mem(e, u(e, s(e))) <=> (mem(e, s(e)) | mem(e, e))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[638, 11])).
% 14.48/14.64 tff(640,assumption,(~mem(e, s(e))), introduced(assumption)).
% 14.48/14.64 tff(641,plain,
% 14.48/14.64 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(e, s(e))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(e, s(e)))),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(642,plain,
% 14.48/14.64 ((mem(e, s(e)) <=> $true) <=> mem(e, s(e))),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(643,plain,
% 14.48/14.64 ((e = e) <=> $true),
% 14.48/14.64 inference(rewrite,[status(thm)],[])).
% 14.48/14.64 tff(644,plain,
% 14.48/14.64 ((mem(e, s(e)) <=> (e = e)) <=> (mem(e, s(e)) <=> $true)),
% 14.48/14.64 inference(monotonicity,[status(thm)],[643])).
% 14.48/14.64 tff(645,plain,
% 14.48/14.64 ((mem(e, s(e)) <=> (e = e)) <=> mem(e, s(e))),
% 14.48/14.64 inference(transitivity,[status(thm)],[644, 642])).
% 14.48/14.64 tff(646,plain,
% 14.48/14.64 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(e, s(e)) <=> (e = e))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(e, s(e)))),
% 14.48/14.64 inference(monotonicity,[status(thm)],[645])).
% 14.48/14.64 tff(647,plain,
% 14.48/14.64 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(e, s(e)) <=> (e = e))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(e, s(e)))),
% 14.48/14.64 inference(transitivity,[status(thm)],[646, 641])).
% 14.48/14.64 tff(648,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(e, s(e)) <=> (e = e))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(649,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(e, s(e))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[648, 647])).
% 14.48/14.64 tff(650,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[649, 38, 640])).
% 14.48/14.64 tff(651,plain,(mem(e, s(e))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(652,plain,
% 14.48/14.64 ((mem(e, s(e)) | mem(e, e)) | (~mem(e, s(e)))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(653,plain,
% 14.48/14.64 (mem(e, s(e)) | mem(e, e)),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[652, 651])).
% 14.48/14.64 tff(654,plain,
% 14.48/14.64 ((~(mem(e, u(e, s(e))) <=> (mem(e, s(e)) | mem(e, e)))) | mem(e, u(e, s(e))) | (~(mem(e, s(e)) | mem(e, e)))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(655,plain,
% 14.48/14.64 ((~(mem(e, u(e, s(e))) <=> (mem(e, s(e)) | mem(e, e)))) | mem(e, u(e, s(e)))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[654, 653])).
% 14.48/14.64 tff(656,plain,
% 14.48/14.64 (mem(e, u(e, s(e)))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[655, 639])).
% 14.48/14.64 tff(657,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[656, 637])).
% 14.48/14.64 tff(658,plain,(mem(e, a(e, e))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(659,plain,
% 14.48/14.64 (mem(e, s(a(n(e), n(e))))),
% 14.48/14.64 inference(modus_ponens,[status(thm)],[658, 632])).
% 14.48/14.64 tff(660,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(e, s(a(n(e), n(e)))) <=> (e = a(n(e), n(e))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(661,plain,
% 14.48/14.64 (mem(e, s(a(n(e), n(e)))) <=> (e = a(n(e), n(e)))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[660, 38])).
% 14.48/14.64 tff(662,plain,
% 14.48/14.64 ((~(mem(e, s(a(n(e), n(e)))) <=> (e = a(n(e), n(e))))) | (~mem(e, s(a(n(e), n(e))))) | (e = a(n(e), n(e)))),
% 14.48/14.64 inference(tautology,[status(thm)],[])).
% 14.48/14.64 tff(663,plain,
% 14.48/14.64 ((~(mem(e, s(a(n(e), n(e)))) <=> (e = a(n(e), n(e))))) | (~mem(e, s(a(n(e), n(e)))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[662, 300])).
% 14.48/14.64 tff(664,plain,
% 14.48/14.64 (~mem(e, s(a(n(e), n(e))))),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[663, 661])).
% 14.48/14.64 tff(665,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[664, 659])).
% 14.48/14.64 tff(666,plain,(~(a(e, e) = s(n(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.64 tff(667,assumption,(~(mem(a(e, e), s(s(n(n(e))))) <=> (a(e, e) = s(n(n(e)))))), introduced(assumption)).
% 14.48/14.64 tff(668,plain,
% 14.48/14.64 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(s(n(n(e))))) <=> (a(e, e) = s(n(n(e)))))),
% 14.48/14.64 inference(quant_inst,[status(thm)],[])).
% 14.48/14.64 tff(669,plain,
% 14.48/14.64 ($false),
% 14.48/14.64 inference(unit_resolution,[status(thm)],[668, 38, 667])).
% 14.48/14.64 tff(670,plain,(mem(a(e, e), s(s(n(n(e))))) <=> (a(e, e) = s(n(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.65 tff(671,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(s(n(n(e))))) <=> (a(e, e) = s(n(n(e)))))) | (~mem(a(e, e), s(s(n(n(e)))))) | (a(e, e) = s(n(n(e))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(672,plain,
% 14.48/14.65 ((~mem(a(e, e), s(s(n(n(e)))))) | (a(e, e) = s(n(n(e))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[671, 670])).
% 14.48/14.65 tff(673,plain,
% 14.48/14.65 (~mem(a(e, e), s(s(n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[672, 666])).
% 14.48/14.65 tff(674,plain,
% 14.48/14.65 ((~![X: $i, Y: $i] : (a(X, Y) = u(X, s(Y)))) | (a(s(n(n(e))), s(n(n(e)))) = u(s(n(n(e))), s(s(n(n(e))))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(675,plain,
% 14.48/14.65 (a(s(n(n(e))), s(n(n(e)))) = u(s(n(n(e))), s(s(n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[674, 69])).
% 14.48/14.65 tff(676,plain,
% 14.48/14.65 (u(s(n(n(e))), s(s(n(n(e))))) = a(s(n(n(e))), s(n(n(e))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[675])).
% 14.48/14.65 tff(677,plain,
% 14.48/14.65 (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> mem(a(e, e), a(s(n(n(e))), s(n(n(e)))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[676])).
% 14.48/14.65 tff(678,plain,
% 14.48/14.65 (mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) <=> mem(a(e, e), u(s(n(n(e))), s(s(n(n(e))))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[677])).
% 14.48/14.65 tff(679,assumption,(mem(a(e, e), a(s(n(n(e))), s(n(n(e)))))), introduced(assumption)).
% 14.48/14.65 tff(680,plain,
% 14.48/14.65 (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e))))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[679, 678])).
% 14.48/14.65 tff(681,plain,
% 14.48/14.65 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e)))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))))),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(682,plain,
% 14.48/14.65 ((mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(s(n(n(e))))) | mem(a(e, e), s(n(n(e)))))) <=> (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e)))))))),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(683,plain,
% 14.48/14.65 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(s(n(n(e))))) | mem(a(e, e), s(n(n(e))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[682])).
% 14.48/14.65 tff(684,plain,
% 14.48/14.65 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(s(n(n(e))))) | mem(a(e, e), s(n(n(e))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))))),
% 14.48/14.65 inference(transitivity,[status(thm)],[683, 681])).
% 14.48/14.65 tff(685,plain,
% 14.48/14.65 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(s(n(n(e))))) | mem(a(e, e), s(n(n(e))))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(686,plain,
% 14.48/14.65 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e)))))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[685, 684])).
% 14.48/14.65 tff(687,plain,
% 14.48/14.65 (mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[686, 11])).
% 14.48/14.65 tff(688,assumption,(~mem(a(e, e), s(s(n(n(e)))))), introduced(assumption)).
% 14.48/14.65 tff(689,plain,
% 14.48/14.65 (mem(a(e, e), s(a(n(e), n(e)))) <=> mem(a(e, e), s(n(n(e))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[100])).
% 14.48/14.65 tff(690,plain,
% 14.48/14.65 (mem(a(e, e), s(n(n(e)))) <=> mem(a(e, e), s(a(n(e), n(e))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[689])).
% 14.48/14.65 tff(691,assumption,(mem(a(e, e), s(n(n(e))))), introduced(assumption)).
% 14.48/14.65 tff(692,plain,
% 14.48/14.65 (mem(a(e, e), s(a(n(e), n(e))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[691, 690])).
% 14.48/14.65 tff(693,plain,
% 14.48/14.65 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(a(n(e), n(e)))) <=> (a(e, e) = a(n(e), n(e))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(694,plain,
% 14.48/14.65 (mem(a(e, e), s(a(n(e), n(e)))) <=> (a(e, e) = a(n(e), n(e)))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[693, 38])).
% 14.48/14.65 tff(695,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(a(n(e), n(e)))) <=> (a(e, e) = a(n(e), n(e))))) | (~mem(a(e, e), s(a(n(e), n(e))))) | (a(e, e) = a(n(e), n(e)))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(696,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(a(n(e), n(e)))) <=> (a(e, e) = a(n(e), n(e))))) | (~mem(a(e, e), s(a(n(e), n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[695, 187])).
% 14.48/14.65 tff(697,plain,
% 14.48/14.65 (~mem(a(e, e), s(a(n(e), n(e))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[696, 694])).
% 14.48/14.65 tff(698,plain,
% 14.48/14.65 ($false),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[697, 692])).
% 14.48/14.65 tff(699,plain,(~mem(a(e, e), s(n(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.65 tff(700,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))) | mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e)))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(701,plain,
% 14.48/14.65 (~(mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[700, 699, 688])).
% 14.48/14.65 tff(702,plain,
% 14.48/14.65 ((~(mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e)))))))) | (~mem(a(e, e), u(s(n(n(e))), s(s(n(n(e))))))) | (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e))))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(703,plain,
% 14.48/14.65 ((~(mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))) <=> (mem(a(e, e), s(n(n(e)))) | mem(a(e, e), s(s(n(n(e)))))))) | (~mem(a(e, e), u(s(n(n(e))), s(s(n(n(e)))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[702, 701])).
% 14.48/14.65 tff(704,plain,
% 14.48/14.65 (~mem(a(e, e), u(s(n(n(e))), s(s(n(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[703, 687])).
% 14.48/14.65 tff(705,plain,
% 14.48/14.65 ($false),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[704, 680])).
% 14.48/14.65 tff(706,plain,((~mem(a(e, e), a(s(n(n(e))), s(n(n(e)))))) | mem(a(e, e), s(s(n(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.65 tff(707,plain,
% 14.48/14.65 (~mem(a(e, e), a(s(n(n(e))), s(n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[706, 673])).
% 14.48/14.65 tff(708,plain,
% 14.48/14.65 ((~![X: $i] : (n(X) = a(X, X))) | (n(s(n(n(e)))) = a(s(n(n(e))), s(n(n(e)))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(709,plain,
% 14.48/14.65 (n(s(n(n(e)))) = a(s(n(n(e))), s(n(n(e))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[708, 53])).
% 14.48/14.65 tff(710,plain,
% 14.48/14.65 (a(s(n(n(e))), s(n(n(e)))) = n(s(n(n(e))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[709])).
% 14.48/14.65 tff(711,plain,
% 14.48/14.65 ((~![X: $i] : (n(X) = a(X, X))) | (n(s(s(n(e)))) = a(s(s(n(e))), s(s(n(e)))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(712,plain,
% 14.48/14.65 (n(s(s(n(e)))) = a(s(s(n(e))), s(s(n(e))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[711, 53])).
% 14.48/14.65 tff(713,plain,
% 14.48/14.65 (a(s(s(n(e))), s(s(n(e)))) = n(s(s(n(e))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[712])).
% 14.48/14.65 tff(714,plain,
% 14.48/14.65 (u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e))))) = u(n(s(s(n(e)))), n(s(n(n(e)))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[713, 710])).
% 14.48/14.65 tff(715,plain,
% 14.48/14.65 (mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e)))))) <=> mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[714])).
% 14.48/14.65 tff(716,plain,
% 14.48/14.65 (mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e)))))) <=> mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e))))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[715])).
% 14.48/14.65 tff(717,assumption,(mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))), introduced(assumption)).
% 14.48/14.65 tff(718,plain,
% 14.48/14.65 (mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e))))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[717, 716])).
% 14.48/14.65 tff(719,plain,
% 14.48/14.65 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e)))))) <=> (mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(720,plain,
% 14.48/14.65 (mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e)))))) <=> (mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[719, 11])).
% 14.48/14.65 tff(721,assumption,(~mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))), introduced(assumption)).
% 14.48/14.65 tff(722,assumption,(~mem(a(e, e), a(s(n(n(e))), s(n(n(e)))))), introduced(assumption)).
% 14.48/14.65 tff(723,plain,
% 14.48/14.65 ((~(mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e))))))) | mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(724,plain,
% 14.48/14.65 (~(mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[723, 722, 721])).
% 14.48/14.65 tff(725,plain,
% 14.48/14.65 ((~(mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e)))))) <=> (mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))))) | (~mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e))))))) | (mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e))))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(726,plain,
% 14.48/14.65 ((~(mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e)))))) <=> (mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))))) | (~mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e)))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[725, 724])).
% 14.48/14.65 tff(727,plain,
% 14.48/14.65 (~mem(a(e, e), u(a(s(s(n(e))), s(s(n(e)))), a(s(n(n(e))), s(n(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[726, 720])).
% 14.48/14.65 tff(728,plain,
% 14.48/14.65 ($false),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[727, 718])).
% 14.48/14.65 tff(729,plain,((~mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))) | mem(a(e, e), a(s(n(n(e))), s(n(n(e))))) | mem(a(e, e), a(s(s(n(e))), s(s(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.65 tff(730,plain,
% 14.48/14.65 (~mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[729, 707, 627])).
% 14.48/14.65 tff(731,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e)))))))) | mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e))))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(732,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(a(n(e), n(n(e))))) | mem(a(e, e), u(n(s(s(n(e)))), n(s(n(n(e)))))))) | mem(a(e, e), s(a(n(e), n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[731, 730])).
% 14.48/14.65 tff(733,plain,
% 14.48/14.65 (mem(a(e, e), s(a(n(e), n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[732, 516])).
% 14.48/14.65 tff(734,plain,
% 14.48/14.65 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(e, e), s(u(n(e), s(n(n(e)))))) <=> (a(e, e) = u(n(e), s(n(n(e))))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(735,plain,
% 14.48/14.65 (mem(a(e, e), s(u(n(e), s(n(n(e)))))) <=> (a(e, e) = u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[734, 38])).
% 14.48/14.65 tff(736,plain,
% 14.48/14.65 (s(u(n(e), s(n(n(e))))) = s(a(n(e), n(n(e))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[95])).
% 14.48/14.65 tff(737,plain,
% 14.48/14.65 (mem(a(e, e), s(u(n(e), s(n(n(e)))))) <=> mem(a(e, e), s(a(n(e), n(n(e)))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[736])).
% 14.48/14.65 tff(738,plain,
% 14.48/14.65 (mem(a(e, e), s(a(n(e), n(n(e))))) <=> mem(a(e, e), s(u(n(e), s(n(n(e))))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[737])).
% 14.48/14.65 tff(739,assumption,(mem(a(e, e), s(a(n(e), n(n(e)))))), introduced(assumption)).
% 14.48/14.65 tff(740,plain,
% 14.48/14.65 (mem(a(e, e), s(u(n(e), s(n(n(e))))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[739, 738])).
% 14.48/14.65 tff(741,plain,
% 14.48/14.65 ((a(e, e) = u(n(e), s(n(n(e))))) <=> (u(n(e), s(n(n(e)))) = a(e, e))),
% 14.48/14.65 inference(commutativity,[status(thm)],[])).
% 14.48/14.65 tff(742,plain,
% 14.48/14.65 ((u(n(e), s(n(n(e)))) = a(e, e)) <=> (a(e, e) = u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[741])).
% 14.48/14.65 tff(743,plain,
% 14.48/14.65 ((~(u(n(e), s(n(n(e)))) = a(e, e))) <=> (~(a(e, e) = u(n(e), s(n(n(e))))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[742])).
% 14.48/14.65 tff(744,assumption,(~(u(n(e), s(n(n(e)))) = a(e, e))), introduced(assumption)).
% 14.48/14.65 tff(745,plain,
% 14.48/14.65 (~(a(e, e) = u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[744, 743])).
% 14.48/14.65 tff(746,plain,
% 14.48/14.65 ((~(mem(a(e, e), s(u(n(e), s(n(n(e)))))) <=> (a(e, e) = u(n(e), s(n(n(e))))))) | (~mem(a(e, e), s(u(n(e), s(n(n(e))))))) | (a(e, e) = u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(747,plain,
% 14.48/14.65 ($false),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[746, 745, 740, 735])).
% 14.48/14.65 tff(748,plain,((~mem(a(e, e), s(a(n(e), n(n(e)))))) | (u(n(e), s(n(n(e)))) = a(e, e))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.65 tff(749,plain,
% 14.48/14.65 (u(n(e), s(n(n(e)))) = a(e, e)),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[748, 733])).
% 14.48/14.65 tff(750,assumption,(u(n(e), s(n(n(e)))) = a(e, e)), introduced(assumption)).
% 14.48/14.65 tff(751,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), u(n(e), s(n(n(e))))) <=> mem(a(n(e), n(e)), a(e, e))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[750])).
% 14.48/14.65 tff(752,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), a(e, e)) <=> mem(a(n(e), n(e)), u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[751])).
% 14.48/14.65 tff(753,plain,
% 14.48/14.65 ((~mem(a(n(e), n(e)), a(e, e))) <=> (~mem(a(n(e), n(e)), u(n(e), s(n(n(e))))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[752])).
% 14.48/14.65 tff(754,assumption,(~mem(a(n(e), n(e)), a(e, e))), introduced(assumption)).
% 14.48/14.65 tff(755,plain,
% 14.48/14.65 (~mem(a(n(e), n(e)), u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[754, 753])).
% 14.48/14.65 tff(756,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> mem(a(n(e), n(e)), u(n(e), s(n(n(e)))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[106])).
% 14.48/14.65 tff(757,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), u(n(e), s(n(n(e))))) <=> mem(a(n(e), n(e)), u(a(e, e), s(n(n(e)))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[756])).
% 14.48/14.65 tff(758,plain,
% 14.48/14.65 ((~mem(a(n(e), n(e)), u(n(e), s(n(n(e)))))) <=> (~mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[757])).
% 14.48/14.65 tff(759,assumption,(~mem(a(n(e), n(e)), u(n(e), s(n(n(e)))))), introduced(assumption)).
% 14.48/14.65 tff(760,plain,
% 14.48/14.65 (~mem(a(n(e), n(e)), u(a(e, e), s(n(n(e)))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[759, 758])).
% 14.48/14.65 tff(761,plain,
% 14.48/14.65 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e)))))))),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(762,plain,
% 14.48/14.65 ((mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), s(n(n(e)))) | mem(a(n(e), n(e)), a(e, e)))) <=> (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))))),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(763,plain,
% 14.48/14.65 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), s(n(n(e)))) | mem(a(n(e), n(e)), a(e, e))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e)))))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[762])).
% 14.48/14.65 tff(764,plain,
% 14.48/14.65 (((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), s(n(n(e)))) | mem(a(n(e), n(e)), a(e, e))))) <=> ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e)))))))),
% 14.48/14.65 inference(transitivity,[status(thm)],[763, 761])).
% 14.48/14.65 tff(765,plain,
% 14.48/14.65 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), s(n(n(e)))) | mem(a(n(e), n(e)), a(e, e))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(766,plain,
% 14.48/14.65 ((~![X: $i, Y: $i, Z: $i] : (mem(X, u(Y, Z)) <=> (mem(X, Z) | mem(X, Y)))) | (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[765, 764])).
% 14.48/14.65 tff(767,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[766, 11])).
% 14.48/14.65 tff(768,plain,
% 14.48/14.65 (s(n(n(e))) = s(a(n(e), n(e)))),
% 14.48/14.65 inference(symmetry,[status(thm)],[100])).
% 14.48/14.65 tff(769,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), s(n(n(e)))) <=> mem(a(n(e), n(e)), s(a(n(e), n(e))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[768])).
% 14.48/14.65 tff(770,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> mem(a(n(e), n(e)), s(n(n(e))))),
% 14.48/14.65 inference(symmetry,[status(thm)],[769])).
% 14.48/14.65 tff(771,plain,
% 14.48/14.65 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(n(e), n(e)), s(a(n(e), n(e))))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(n(e), n(e)), s(a(n(e), n(e)))))),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(772,plain,
% 14.48/14.65 ((mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> $true) <=> mem(a(n(e), n(e)), s(a(n(e), n(e))))),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(773,plain,
% 14.48/14.65 ((a(n(e), n(e)) = a(n(e), n(e))) <=> $true),
% 14.48/14.65 inference(rewrite,[status(thm)],[])).
% 14.48/14.65 tff(774,plain,
% 14.48/14.65 ((mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> (a(n(e), n(e)) = a(n(e), n(e)))) <=> (mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> $true)),
% 14.48/14.65 inference(monotonicity,[status(thm)],[773])).
% 14.48/14.65 tff(775,plain,
% 14.48/14.65 ((mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> (a(n(e), n(e)) = a(n(e), n(e)))) <=> mem(a(n(e), n(e)), s(a(n(e), n(e))))),
% 14.48/14.65 inference(transitivity,[status(thm)],[774, 772])).
% 14.48/14.65 tff(776,plain,
% 14.48/14.65 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> (a(n(e), n(e)) = a(n(e), n(e))))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(n(e), n(e)), s(a(n(e), n(e)))))),
% 14.48/14.65 inference(monotonicity,[status(thm)],[775])).
% 14.48/14.65 tff(777,plain,
% 14.48/14.65 (((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> (a(n(e), n(e)) = a(n(e), n(e))))) <=> ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(n(e), n(e)), s(a(n(e), n(e)))))),
% 14.48/14.65 inference(transitivity,[status(thm)],[776, 771])).
% 14.48/14.65 tff(778,plain,
% 14.48/14.65 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | (mem(a(n(e), n(e)), s(a(n(e), n(e)))) <=> (a(n(e), n(e)) = a(n(e), n(e))))),
% 14.48/14.65 inference(quant_inst,[status(thm)],[])).
% 14.48/14.65 tff(779,plain,
% 14.48/14.65 ((~![X: $i, Y: $i] : (mem(X, s(Y)) <=> (X = Y))) | mem(a(n(e), n(e)), s(a(n(e), n(e))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[778, 777])).
% 14.48/14.65 tff(780,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), s(a(n(e), n(e))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[779, 38])).
% 14.48/14.65 tff(781,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), s(n(n(e))))),
% 14.48/14.65 inference(modus_ponens,[status(thm)],[780, 770])).
% 14.48/14.65 tff(782,assumption,(~mem(a(n(e), n(e)), s(n(n(e))))), introduced(assumption)).
% 14.48/14.65 tff(783,plain,
% 14.48/14.65 ($false),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[782, 781])).
% 14.48/14.65 tff(784,plain,(mem(a(n(e), n(e)), s(n(n(e))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.65 tff(785,plain,
% 14.48/14.65 ((mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))) | (~mem(a(n(e), n(e)), s(n(n(e)))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(786,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[785, 784])).
% 14.48/14.65 tff(787,plain,
% 14.48/14.65 ((~(mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))))) | mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) | (~(mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))))),
% 14.48/14.65 inference(tautology,[status(thm)],[])).
% 14.48/14.65 tff(788,plain,
% 14.48/14.65 ((~(mem(a(n(e), n(e)), u(a(e, e), s(n(n(e))))) <=> (mem(a(n(e), n(e)), a(e, e)) | mem(a(n(e), n(e)), s(n(n(e))))))) | mem(a(n(e), n(e)), u(a(e, e), s(n(n(e)))))),
% 14.48/14.65 inference(unit_resolution,[status(thm)],[787, 786])).
% 14.48/14.65 tff(789,plain,
% 14.48/14.65 (mem(a(n(e), n(e)), u(a(e, e), s(n(n(e)))))),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[788, 767])).
% 14.48/14.66 tff(790,plain,
% 14.48/14.66 ($false),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[789, 760])).
% 14.48/14.66 tff(791,plain,(mem(a(n(e), n(e)), u(n(e), s(n(n(e)))))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.66 tff(792,plain,
% 14.48/14.66 ($false),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[791, 755])).
% 14.48/14.66 tff(793,plain,(mem(a(n(e), n(e)), a(e, e)) | (~(u(n(e), s(n(n(e)))) = a(e, e)))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.66 tff(794,plain,
% 14.48/14.66 (mem(a(n(e), n(e)), a(e, e))),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[793, 749])).
% 14.48/14.66 tff(795,plain,
% 14.48/14.66 (mem(a(n(e), n(e)), u(e, s(e)))),
% 14.48/14.66 inference(modus_ponens,[status(thm)],[794, 309])).
% 14.48/14.66 tff(796,assumption,(~mem(a(n(e), n(e)), u(e, s(e)))), introduced(assumption)).
% 14.48/14.66 tff(797,plain,
% 14.48/14.66 ($false),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[796, 795])).
% 14.48/14.66 tff(798,plain,(mem(a(n(e), n(e)), u(e, s(e)))), inference(lemma,lemma(discharge,[]))).
% 14.48/14.66 tff(799,plain,
% 14.48/14.66 ((~(mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))))) | (~mem(a(n(e), n(e)), u(e, s(e)))) | (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e)))),
% 14.48/14.66 inference(tautology,[status(thm)],[])).
% 14.48/14.66 tff(800,plain,
% 14.48/14.66 (~(mem(a(n(e), n(e)), u(e, s(e))) <=> (mem(a(n(e), n(e)), e) | mem(a(n(e), n(e)), s(e))))),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[799, 798, 307])).
% 14.48/14.66 tff(801,plain,
% 14.48/14.66 ($false),
% 14.48/14.66 inference(unit_resolution,[status(thm)],[800, 19])).
% 14.48/14.66 % SZS output end Proof
% 14.48/14.67 % E exiting
%------------------------------------------------------------------------------