%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM541+2 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n001.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:21:20 AM UTC 2025
% Result : Theorem 0.19s 0.52s
% Output : Proof 0.38s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM541+2 : TPTP v9.0.0. Released v4.0.0.
% 0.03/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n001.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 01:28:04 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.19/0.52 % SZS status Theorem
% 0.19/0.52 % SZS output start Proof
% 0.19/0.52 tff(szszuzczcdt0_type, type, (
% 0.19/0.52 szszuzczcdt0: $i > $i)).
% 0.19/0.52 tff(xn_type, type, (
% 0.19/0.52 xn: $i)).
% 0.19/0.52 tff(xm_type, type, (
% 0.19/0.52 xm: $i)).
% 0.19/0.52 tff(aElementOf0_type, type, (
% 0.19/0.52 aElementOf0: ( $i * $i ) > $o)).
% 0.19/0.52 tff(slbdtrb0_type, type, (
% 0.19/0.52 slbdtrb0: $i > $i)).
% 0.19/0.52 tff(sdtlseqdt0_type, type, (
% 0.19/0.52 sdtlseqdt0: ( $i * $i ) > $o)).
% 0.19/0.52 tff(tptp_fun_W1_4_type, type, (
% 0.19/0.52 tptp_fun_W1_4: $i > $i)).
% 0.19/0.52 tff(szNzAzT0_type, type, (
% 0.19/0.52 szNzAzT0: $i)).
% 0.19/0.52 tff(sz00_type, type, (
% 0.19/0.52 sz00: $i)).
% 0.19/0.52 tff(1,plain,
% 0.19/0.52 (aElementOf0(xn, szNzAzT0) <=> aElementOf0(xn, szNzAzT0)),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(2,axiom,(aElementOf0(xm, szNzAzT0) & aElementOf0(xn, szNzAzT0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__1936')).
% 0.19/0.52 tff(3,plain,
% 0.19/0.52 (aElementOf0(xn, szNzAzT0)),
% 0.19/0.52 inference(and_elim,[status(thm)],[2])).
% 0.19/0.52 tff(4,plain,
% 0.19/0.52 (aElementOf0(xn, szNzAzT0)),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[3, 1])).
% 0.19/0.52 tff(5,plain,
% 0.19/0.52 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(6,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[5])).
% 0.19/0.52 tff(7,plain,
% 0.19/0.52 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(8,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[7])).
% 0.19/0.52 tff(9,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(10,plain,
% 0.19/0.52 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(11,plain,
% 0.19/0.52 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[10])).
% 0.19/0.52 tff(12,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mSuccNum')).
% 0.19/0.52 tff(13,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[12, 11])).
% 0.19/0.52 tff(14,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[13, 9])).
% 0.19/0.52 tff(15,plain,(
% 0.19/0.52 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(skolemize,[status(sab)],[14])).
% 0.19/0.52 tff(16,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[15, 8])).
% 0.19/0.52 tff(17,plain,
% 0.19/0.52 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[16, 6])).
% 0.19/0.52 tff(18,plain,
% 0.19/0.52 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(19,plain,
% 0.19/0.52 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))))),
% 0.19/0.52 inference(quant_inst,[status(thm)],[])).
% 0.19/0.52 tff(20,plain,
% 0.19/0.52 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(xn, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00)))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.19/0.52 tff(21,plain,
% 0.19/0.52 (~((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[20, 17, 4])).
% 0.19/0.52 tff(22,plain,
% 0.19/0.52 (((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00)) | (~(szszuzczcdt0(xn) = sz00))),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(23,plain,
% 0.19/0.52 (~(szszuzczcdt0(xn) = sz00)),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[22, 21])).
% 0.19/0.52 tff(24,plain,
% 0.19/0.52 (((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00)) | aElementOf0(szszuzczcdt0(xn), szNzAzT0)),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(25,plain,
% 0.19/0.52 (aElementOf0(szszuzczcdt0(xn), szNzAzT0)),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[24, 21])).
% 0.19/0.52 tff(26,plain,
% 0.19/0.52 (^[W0: $i] : refl(((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(27,plain,
% 0.19/0.52 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))) <=> ![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[26])).
% 0.19/0.52 tff(28,plain,
% 0.19/0.52 (^[W0: $i] : trans(monotonicity(rewrite((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) <=> (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))), (((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))))), rewrite(((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))), (((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(29,plain,
% 0.19/0.52 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))) <=> ![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[28])).
% 0.19/0.52 tff(30,plain,
% 0.19/0.52 (^[W0: $i] : rewrite(((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0))) <=> ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0))))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(31,plain,
% 0.19/0.52 (![W0: $i] : ((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[30])).
% 0.19/0.52 tff(32,plain,
% 0.19/0.52 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(33,plain,
% 0.19/0.52 (^[W0: $i] : trans(monotonicity(rewrite(((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1)))) <=> ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))), ((aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))))), rewrite((aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))), ((aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(34,plain,
% 0.19/0.52 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))))) <=> ![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[33])).
% 0.19/0.52 tff(35,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => ((W0 = sz00) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mNatExtra')).
% 0.19/0.52 tff(36,plain,
% 0.19/0.52 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[35, 34])).
% 0.19/0.52 tff(37,plain,
% 0.19/0.52 (![W0: $i] : (?[W1: $i] : (aElementOf0(W1, szNzAzT0) & (W0 = szszuzczcdt0(W1))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[36, 32])).
% 0.19/0.52 tff(38,plain,(
% 0.19/0.52 ![W0: $i] : ((aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))) | (W0 = sz00) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(skolemize,[status(sab)],[37])).
% 0.19/0.52 tff(39,plain,
% 0.19/0.52 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (aElementOf0(tptp_fun_W1_4(W0), szNzAzT0) & (W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[38, 31])).
% 0.19/0.52 tff(40,plain,
% 0.19/0.52 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[39, 29])).
% 0.19/0.52 tff(41,plain,
% 0.19/0.52 (![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[40, 27])).
% 0.19/0.52 tff(42,plain,
% 0.19/0.52 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(43,plain,
% 0.19/0.52 (((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))))) <=> ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(44,plain,
% 0.19/0.52 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))))))),
% 0.19/0.52 inference(monotonicity,[status(thm)],[43])).
% 0.19/0.52 tff(45,plain,
% 0.19/0.52 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.19/0.52 inference(transitivity,[status(thm)],[44, 42])).
% 0.19/0.52 tff(46,plain,
% 0.19/0.52 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xn) = sz00) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))))),
% 0.19/0.52 inference(quant_inst,[status(thm)],[])).
% 0.19/0.52 tff(47,plain,
% 0.19/0.52 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (szszuzczcdt0(xn) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[46, 45])).
% 0.19/0.52 tff(48,plain,
% 0.19/0.52 (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[47, 41, 25, 23])).
% 0.19/0.52 tff(49,plain,
% 0.19/0.52 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))) | (szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(50,plain,
% 0.19/0.52 (szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[49, 48])).
% 0.19/0.52 tff(51,plain,
% 0.19/0.52 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn)))))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(52,plain,
% 0.19/0.52 (aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[51, 48])).
% 0.19/0.52 tff(53,plain,
% 0.19/0.52 (^[W0: $i, W1: $i] : refl(((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(54,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[53])).
% 0.19/0.52 tff(55,plain,
% 0.19/0.52 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), (((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))), rewrite(((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))), (((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(56,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[55])).
% 0.19/0.52 tff(57,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(58,plain,
% 0.19/0.52 (^[W0: $i, W1: $i] : trans(monotonicity(rewrite(((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1)) <=> ((~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (W0 = W1))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1))) <=> ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (W0 = W1))))), rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (W0 = W1))) <=> ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1))) <=> ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))))),
% 0.19/0.52 inference(bind,[status(th)],[])).
% 0.19/0.52 tff(59,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.52 inference(quant_intro,[status(thm)],[58])).
% 0.19/0.52 tff(60,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((szszuzczcdt0(W0) = szszuzczcdt0(W1)) => (W0 = W1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mSuccEquSucc')).
% 0.19/0.52 tff(61,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[60, 59])).
% 0.19/0.52 tff(62,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[61, 57])).
% 0.19/0.52 tff(63,plain,(
% 0.19/0.52 ![W0: $i, W1: $i] : ((W0 = W1) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.52 inference(skolemize,[status(sab)],[62])).
% 0.19/0.52 tff(64,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[63, 56])).
% 0.19/0.52 tff(65,plain,
% 0.19/0.52 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[64, 54])).
% 0.19/0.52 tff(66,plain,
% 0.19/0.52 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (xn = tptp_fun_W1_4(szszuzczcdt0(xn))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (xn = tptp_fun_W1_4(szszuzczcdt0(xn))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(67,plain,
% 0.19/0.52 (((xn = tptp_fun_W1_4(szszuzczcdt0(xn))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (~aElementOf0(xn, szNzAzT0))) <=> ((~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (xn = tptp_fun_W1_4(szszuzczcdt0(xn))))),
% 0.19/0.52 inference(rewrite,[status(thm)],[])).
% 0.19/0.52 tff(68,plain,
% 0.19/0.52 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xn = tptp_fun_W1_4(szszuzczcdt0(xn))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (~aElementOf0(xn, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (xn = tptp_fun_W1_4(szszuzczcdt0(xn)))))),
% 0.19/0.52 inference(monotonicity,[status(thm)],[67])).
% 0.19/0.52 tff(69,plain,
% 0.19/0.52 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xn = tptp_fun_W1_4(szszuzczcdt0(xn))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (~aElementOf0(xn, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (xn = tptp_fun_W1_4(szszuzczcdt0(xn))))),
% 0.19/0.52 inference(transitivity,[status(thm)],[68, 66])).
% 0.19/0.52 tff(70,plain,
% 0.19/0.52 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xn = tptp_fun_W1_4(szszuzczcdt0(xn))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (~aElementOf0(xn, szNzAzT0)))),
% 0.19/0.52 inference(quant_inst,[status(thm)],[])).
% 0.19/0.52 tff(71,plain,
% 0.19/0.52 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xn)), szNzAzT0)) | (~(szszuzczcdt0(xn) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))))) | (xn = tptp_fun_W1_4(szszuzczcdt0(xn)))),
% 0.19/0.52 inference(modus_ponens,[status(thm)],[70, 69])).
% 0.19/0.52 tff(72,plain,
% 0.19/0.52 (xn = tptp_fun_W1_4(szszuzczcdt0(xn))),
% 0.19/0.52 inference(unit_resolution,[status(thm)],[71, 65, 4, 52, 50])).
% 0.19/0.52 tff(73,assumption,(~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))), introduced(assumption)).
% 0.19/0.52 tff(74,plain,
% 0.19/0.52 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))) | ((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))),
% 0.19/0.52 inference(tautology,[status(thm)],[])).
% 0.19/0.52 tff(75,plain,
% 0.19/0.52 ((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[74, 73])).
% 0.19/0.53 tff(76,plain,
% 0.19/0.53 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(77,plain,
% 0.19/0.53 (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[76, 73])).
% 0.19/0.53 tff(78,plain,
% 0.19/0.53 (aElementOf0(xm, szNzAzT0) <=> aElementOf0(xm, szNzAzT0)),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(79,plain,
% 0.19/0.53 (aElementOf0(xm, szNzAzT0)),
% 0.19/0.53 inference(and_elim,[status(thm)],[2])).
% 0.19/0.53 tff(80,plain,
% 0.19/0.53 (aElementOf0(xm, szNzAzT0)),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[79, 78])).
% 0.19/0.53 tff(81,plain,
% 0.19/0.53 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(xm, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(xm, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(82,plain,
% 0.19/0.53 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(xm, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00))))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(83,plain,
% 0.19/0.53 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(xm, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[82, 81])).
% 0.19/0.53 tff(84,plain,
% 0.19/0.53 (~((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[83, 17, 80])).
% 0.19/0.53 tff(85,plain,
% 0.19/0.53 (((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00)) | aElementOf0(szszuzczcdt0(xm), szNzAzT0)),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(86,plain,
% 0.19/0.53 (aElementOf0(szszuzczcdt0(xm), szNzAzT0)),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[85, 84])).
% 0.19/0.53 tff(87,plain,
% 0.19/0.53 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(88,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[87])).
% 0.19/0.53 tff(89,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(90,plain,
% 0.19/0.53 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(91,plain,
% 0.19/0.53 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, szszuzczcdt0(W0))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[90])).
% 0.19/0.53 tff(92,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, szszuzczcdt0(W0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mLessSucc')).
% 0.19/0.53 tff(93,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[92, 91])).
% 0.19/0.53 tff(94,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[93, 89])).
% 0.19/0.53 tff(95,plain,(
% 0.19/0.53 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(skolemize,[status(sab)],[94])).
% 0.19/0.53 tff(96,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[95, 88])).
% 0.19/0.53 tff(97,plain,
% 0.19/0.53 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | ((~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn)))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(98,plain,
% 0.19/0.53 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | ((~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(99,plain,
% 0.19/0.53 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, szszuzczcdt0(W0)))) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(xn, szszuzczcdt0(xn))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[98, 97])).
% 0.19/0.53 tff(100,plain,
% 0.19/0.53 (sdtlseqdt0(xn, szszuzczcdt0(xn))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[99, 96, 4])).
% 0.19/0.53 tff(101,plain,
% 0.19/0.53 (^[W0: $i, W1: $i, W2: $i] : refl((sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0))) <=> (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(102,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[101])).
% 0.19/0.53 tff(103,plain,
% 0.19/0.53 (^[W0: $i, W1: $i, W2: $i] : trans(monotonicity(trans(monotonicity(rewrite((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2)) <=> (~((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1))))), ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) <=> (~(~((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1))))))), rewrite((~(~((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1))))) <=> ((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)))), ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) <=> ((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1))))), trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)) <=> (~((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))) <=> (~(~((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))) <=> ((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)))) <=> (sdtlseqdt0(W0, W2) | ((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1))) | ((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))), rewrite((sdtlseqdt0(W0, W2) | ((~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1))) | ((~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) <=> (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))), ((sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)))) <=> (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(104,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)))) <=> ![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[103])).
% 0.19/0.53 tff(105,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)))) <=> ![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(106,plain,
% 0.19/0.53 (^[W0: $i, W1: $i, W2: $i] : trans(monotonicity(rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) & aElementOf0(W2, szNzAzT0)) <=> (aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))), rewrite(((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2)) => sdtlseqdt0(W0, W2)) <=> ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | sdtlseqdt0(W0, W2))), ((((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) & aElementOf0(W2, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2)) => sdtlseqdt0(W0, W2))) <=> ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)) => ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | sdtlseqdt0(W0, W2))))), rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0)) => ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | sdtlseqdt0(W0, W2))) <=> (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))), ((((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) & aElementOf0(W2, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2)) => sdtlseqdt0(W0, W2))) <=> (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(107,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) & aElementOf0(W2, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2)) => sdtlseqdt0(W0, W2))) <=> ![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[106])).
% 0.19/0.53 tff(108,axiom,(![W0: $i, W1: $i, W2: $i] : (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) & aElementOf0(W2, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2)) => sdtlseqdt0(W0, W2)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mLessTrans')).
% 0.19/0.53 tff(109,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[108, 107])).
% 0.19/0.53 tff(110,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[109, 105])).
% 0.19/0.53 tff(111,plain,(
% 0.19/0.53 ![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W2))) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0) & aElementOf0(W2, szNzAzT0))))),
% 0.19/0.53 inference(skolemize,[status(sab)],[110])).
% 0.19/0.53 tff(112,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[111, 104])).
% 0.19/0.53 tff(113,plain,
% 0.19/0.53 (![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[112, 102])).
% 0.19/0.53 tff(114,plain,
% 0.19/0.53 (((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))) <=> ((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(115,plain,
% 0.19/0.53 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0))) <=> (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(116,plain,
% 0.19/0.53 (((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))) <=> ((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn)))))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[115])).
% 0.19/0.53 tff(117,plain,
% 0.19/0.53 (((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))) <=> ((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.19/0.53 inference(transitivity,[status(thm)],[116, 114])).
% 0.19/0.53 tff(118,plain,
% 0.19/0.53 ((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(119,plain,
% 0.19/0.53 ((~![W0: $i, W1: $i, W2: $i] : (sdtlseqdt0(W0, W2) | (~aElementOf0(W2, szNzAzT0)) | (~aElementOf0(W1, szNzAzT0)) | (~sdtlseqdt0(W1, W2)) | (~sdtlseqdt0(W0, W1)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.19/0.53 tff(120,plain,
% 0.19/0.53 (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~sdtlseqdt0(szszuzczcdt0(xm), xn))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[119, 113, 4, 100, 86, 25])).
% 0.19/0.53 tff(121,plain,
% 0.19/0.53 (~sdtlseqdt0(szszuzczcdt0(xm), xn)),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[120, 77])).
% 0.19/0.53 tff(122,plain,
% 0.19/0.53 (((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))) | sdtlseqdt0(szszuzczcdt0(xm), xn)),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(123,plain,
% 0.19/0.53 ((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[122, 121])).
% 0.19/0.53 tff(124,plain,
% 0.19/0.53 ((~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))) | (xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(125,plain,
% 0.19/0.53 (xm = xn),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[124, 123, 75])).
% 0.19/0.53 tff(126,plain,
% 0.19/0.53 (((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00)) | (~(szszuzczcdt0(xm) = sz00))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(127,plain,
% 0.19/0.53 (~(szszuzczcdt0(xm) = sz00)),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[126, 84])).
% 0.19/0.53 tff(128,plain,
% 0.19/0.53 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(129,plain,
% 0.19/0.53 (((szszuzczcdt0(xm) = sz00) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm)))))))) <=> ((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(130,plain,
% 0.19/0.53 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xm) = sz00) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm)))))))))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[129])).
% 0.19/0.53 tff(131,plain,
% 0.19/0.53 (((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xm) = sz00) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))) <=> ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))),
% 0.19/0.53 inference(transitivity,[status(thm)],[130, 128])).
% 0.19/0.53 tff(132,plain,
% 0.19/0.53 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | ((szszuzczcdt0(xm) = sz00) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(133,plain,
% 0.19/0.53 ((~![W0: $i] : ((W0 = sz00) | (~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(tptp_fun_W1_4(W0), szNzAzT0)) | (~(W0 = szszuzczcdt0(tptp_fun_W1_4(W0)))))))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = sz00) | (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm)))))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[132, 131])).
% 0.19/0.53 tff(134,plain,
% 0.19/0.53 (~((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[133, 41, 86, 127])).
% 0.19/0.53 tff(135,plain,
% 0.19/0.53 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm)))))) | (szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(136,plain,
% 0.19/0.53 (szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm)))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[135, 134])).
% 0.19/0.53 tff(137,plain,
% 0.19/0.53 (((~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm)))))) | aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)),
% 0.19/0.53 inference(tautology,[status(thm)],[])).
% 0.19/0.53 tff(138,plain,
% 0.19/0.53 (aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[137, 134])).
% 0.19/0.53 tff(139,plain,
% 0.19/0.53 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (xm = tptp_fun_W1_4(szszuzczcdt0(xm))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (xm = tptp_fun_W1_4(szszuzczcdt0(xm))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(140,plain,
% 0.19/0.53 (((xm = tptp_fun_W1_4(szszuzczcdt0(xm))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (~aElementOf0(xm, szNzAzT0))) <=> ((~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (xm = tptp_fun_W1_4(szszuzczcdt0(xm))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(141,plain,
% 0.19/0.53 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = tptp_fun_W1_4(szszuzczcdt0(xm))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (~aElementOf0(xm, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (xm = tptp_fun_W1_4(szszuzczcdt0(xm)))))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[140])).
% 0.19/0.53 tff(142,plain,
% 0.19/0.53 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = tptp_fun_W1_4(szszuzczcdt0(xm))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (~aElementOf0(xm, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (xm = tptp_fun_W1_4(szszuzczcdt0(xm))))),
% 0.19/0.53 inference(transitivity,[status(thm)],[141, 139])).
% 0.19/0.53 tff(143,plain,
% 0.19/0.53 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = tptp_fun_W1_4(szszuzczcdt0(xm))) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (~aElementOf0(xm, szNzAzT0)))),
% 0.19/0.53 inference(quant_inst,[status(thm)],[])).
% 0.19/0.53 tff(144,plain,
% 0.19/0.53 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(tptp_fun_W1_4(szszuzczcdt0(xm)), szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xm))))) | (xm = tptp_fun_W1_4(szszuzczcdt0(xm)))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[143, 142])).
% 0.19/0.53 tff(145,plain,
% 0.19/0.53 (xm = tptp_fun_W1_4(szszuzczcdt0(xm))),
% 0.19/0.53 inference(unit_resolution,[status(thm)],[144, 65, 80, 138, 136])).
% 0.19/0.53 tff(146,plain,
% 0.19/0.53 (tptp_fun_W1_4(szszuzczcdt0(xm)) = xm),
% 0.19/0.53 inference(symmetry,[status(thm)],[145])).
% 0.19/0.53 tff(147,plain,
% 0.19/0.53 (tptp_fun_W1_4(szszuzczcdt0(xm)) = tptp_fun_W1_4(szszuzczcdt0(xn))),
% 0.19/0.53 inference(transitivity,[status(thm)],[146, 125, 72])).
% 0.19/0.53 tff(148,plain,
% 0.19/0.53 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xm))) <=> sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn)))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[147])).
% 0.19/0.53 tff(149,plain,
% 0.19/0.53 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn))) <=> sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xm)))),
% 0.19/0.53 inference(symmetry,[status(thm)],[148])).
% 0.19/0.53 tff(150,plain,
% 0.19/0.53 ((~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn)))) <=> (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xm))))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[149])).
% 0.19/0.53 tff(151,plain,
% 0.19/0.53 (tptp_fun_W1_4(szszuzczcdt0(xn)) = xn),
% 0.19/0.53 inference(symmetry,[status(thm)],[72])).
% 0.19/0.53 tff(152,plain,
% 0.19/0.53 (szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))) = szszuzczcdt0(xn)),
% 0.19/0.53 inference(symmetry,[status(thm)],[50])).
% 0.19/0.53 tff(153,plain,
% 0.19/0.53 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn))) <=> sdtlseqdt0(szszuzczcdt0(xn), xn)),
% 0.19/0.53 inference(monotonicity,[status(thm)],[152, 151])).
% 0.19/0.53 tff(154,plain,
% 0.19/0.53 (sdtlseqdt0(szszuzczcdt0(xn), xn) <=> sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn)))),
% 0.19/0.53 inference(symmetry,[status(thm)],[153])).
% 0.19/0.53 tff(155,plain,
% 0.19/0.53 ((~sdtlseqdt0(szszuzczcdt0(xn), xn)) <=> (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn))))),
% 0.19/0.53 inference(monotonicity,[status(thm)],[154])).
% 0.19/0.53 tff(156,plain,
% 0.19/0.53 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(157,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[156])).
% 0.19/0.53 tff(158,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(rewrite,[status(thm)],[])).
% 0.19/0.53 tff(159,plain,
% 0.19/0.53 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (~(W0 = szszuzczcdt0(W0)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0)))))),
% 0.19/0.53 inference(bind,[status(th)],[])).
% 0.19/0.53 tff(160,plain,
% 0.19/0.53 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (~(W0 = szszuzczcdt0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(quant_intro,[status(thm)],[159])).
% 0.19/0.53 tff(161,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (~(W0 = szszuzczcdt0(W0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mNatNSucc')).
% 0.19/0.53 tff(162,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[161, 160])).
% 0.19/0.53 tff(163,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[162, 158])).
% 0.19/0.53 tff(164,plain,(
% 0.19/0.53 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(skolemize,[status(sab)],[163])).
% 0.19/0.53 tff(165,plain,
% 0.19/0.53 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))),
% 0.19/0.53 inference(modus_ponens,[status(thm)],[164, 157])).
% 0.19/0.54 tff(166,plain,
% 0.19/0.54 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | ((~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | (~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(167,plain,
% 0.19/0.54 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | ((~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn))))),
% 0.19/0.54 inference(quant_inst,[status(thm)],[])).
% 0.19/0.54 tff(168,plain,
% 0.19/0.54 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~(W0 = szszuzczcdt0(W0))))) | (~aElementOf0(xn, szNzAzT0)) | (~(xn = szszuzczcdt0(xn)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[167, 166])).
% 0.19/0.54 tff(169,plain,
% 0.19/0.54 (~(xn = szszuzczcdt0(xn))),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[168, 165, 4])).
% 0.19/0.54 tff(170,plain,
% 0.19/0.54 (^[W0: $i, W1: $i] : refl(((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))),
% 0.19/0.54 inference(bind,[status(th)],[])).
% 0.19/0.54 tff(171,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.19/0.54 inference(quant_intro,[status(thm)],[170])).
% 0.19/0.54 tff(172,plain,
% 0.19/0.54 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), trans(monotonicity(rewrite((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) <=> (~((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))), ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) <=> (~(~((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))))), rewrite((~(~((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))) <=> ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))), ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) <=> ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0))))), (((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ((W0 = W1) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))))), rewrite(((W0 = W1) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | ((~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))), (((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))))),
% 0.19/0.54 inference(bind,[status(th)],[])).
% 0.19/0.54 tff(173,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.19/0.54 inference(quant_intro,[status(thm)],[172])).
% 0.19/0.54 tff(174,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(175,plain,
% 0.19/0.54 (^[W0: $i, W1: $i] : trans(monotonicity(rewrite(((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1)) <=> ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) | (W0 = W1))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1))) <=> ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) | (W0 = W1))))), rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))) | (W0 = W1))) <=> ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))), (((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1))) <=> ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))))),
% 0.19/0.54 inference(bind,[status(th)],[])).
% 0.19/0.54 tff(176,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1))) <=> ![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.19/0.54 inference(quant_intro,[status(thm)],[175])).
% 0.19/0.54 tff(177,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => ((sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0)) => (W0 = W1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mLessASymm')).
% 0.19/0.54 tff(178,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[177, 176])).
% 0.19/0.54 tff(179,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[178, 174])).
% 0.19/0.54 tff(180,plain,(
% 0.19/0.54 ![W0: $i, W1: $i] : ((W0 = W1) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (~(sdtlseqdt0(W0, W1) & sdtlseqdt0(W1, W0))))),
% 0.19/0.54 inference(skolemize,[status(sab)],[179])).
% 0.19/0.54 tff(181,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[180, 173])).
% 0.19/0.54 tff(182,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[181, 171])).
% 0.19/0.54 tff(183,plain,
% 0.19/0.54 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(184,plain,
% 0.19/0.54 (((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn))) <=> ((~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(185,plain,
% 0.19/0.54 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn)))))),
% 0.19/0.54 inference(monotonicity,[status(thm)],[184])).
% 0.19/0.54 tff(186,plain,
% 0.19/0.54 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))))),
% 0.19/0.54 inference(transitivity,[status(thm)],[185, 183])).
% 0.19/0.54 tff(187,plain,
% 0.19/0.54 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)))),
% 0.19/0.54 inference(quant_inst,[status(thm)],[])).
% 0.19/0.54 tff(188,plain,
% 0.19/0.54 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~aElementOf0(xn, szNzAzT0)) | (xn = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn)) | (~sdtlseqdt0(xn, szszuzczcdt0(xn)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[187, 186])).
% 0.19/0.54 tff(189,plain,
% 0.19/0.54 ((~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xn), xn))),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[188, 182, 4, 100, 169])).
% 0.19/0.54 tff(190,plain,
% 0.19/0.54 (~sdtlseqdt0(szszuzczcdt0(xn), xn)),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[189, 25])).
% 0.19/0.54 tff(191,plain,
% 0.19/0.54 (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xn)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[190, 155])).
% 0.19/0.54 tff(192,plain,
% 0.19/0.54 (~sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xm)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[191, 150])).
% 0.19/0.54 tff(193,plain,
% 0.19/0.54 (sdtlseqdt0(szszuzczcdt0(xn), xm) <=> sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xm)))),
% 0.19/0.54 inference(monotonicity,[status(thm)],[50, 145])).
% 0.19/0.54 tff(194,plain,
% 0.19/0.54 (^[W0: $i, W1: $i] : refl((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))),
% 0.19/0.54 inference(bind,[status(th)],[])).
% 0.19/0.54 tff(195,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.54 inference(quant_intro,[status(thm)],[194])).
% 0.19/0.54 tff(196,plain,
% 0.19/0.54 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))), ((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))), rewrite((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), ((sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))),
% 0.19/0.54 inference(bind,[status(th)],[])).
% 0.19/0.54 tff(197,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.54 inference(quant_intro,[status(thm)],[196])).
% 0.19/0.54 tff(198,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(199,plain,
% 0.19/0.54 (^[W0: $i, W1: $i] : rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0))) <=> (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)))))),
% 0.19/0.54 inference(bind,[status(th)],[])).
% 0.19/0.54 tff(200,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0))) <=> ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.54 inference(quant_intro,[status(thm)],[199])).
% 0.19/0.54 tff(201,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mLessTotal')).
% 0.19/0.54 tff(202,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[201, 200])).
% 0.19/0.54 tff(203,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[202, 198])).
% 0.19/0.54 tff(204,plain,(
% 0.19/0.54 ![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))))),
% 0.19/0.54 inference(skolemize,[status(sab)],[203])).
% 0.19/0.54 tff(205,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[204, 197])).
% 0.19/0.54 tff(206,plain,
% 0.19/0.54 (![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[205, 195])).
% 0.19/0.54 tff(207,plain,
% 0.19/0.54 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(208,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0))) <=> (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(209,plain,
% 0.19/0.54 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm)))),
% 0.19/0.54 inference(monotonicity,[status(thm)],[208])).
% 0.19/0.54 tff(210,plain,
% 0.19/0.54 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm))),
% 0.19/0.54 inference(transitivity,[status(thm)],[209, 207])).
% 0.19/0.54 tff(211,plain,
% 0.19/0.54 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xn), xm) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))),
% 0.19/0.54 inference(quant_inst,[status(thm)],[])).
% 0.19/0.54 tff(212,plain,
% 0.19/0.54 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[211, 210])).
% 0.19/0.54 tff(213,plain,
% 0.19/0.54 (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[212, 206, 80, 25])).
% 0.19/0.54 tff(214,plain,
% 0.19/0.54 (sdtlseqdt0(szszuzczcdt0(xn), xm)),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[213, 77])).
% 0.19/0.54 tff(215,plain,
% 0.19/0.54 (sdtlseqdt0(szszuzczcdt0(tptp_fun_W1_4(szszuzczcdt0(xn))), tptp_fun_W1_4(szszuzczcdt0(xm)))),
% 0.19/0.54 inference(modus_ponens,[status(thm)],[214, 193])).
% 0.19/0.54 tff(216,plain,
% 0.19/0.54 ($false),
% 0.19/0.54 inference(unit_resolution,[status(thm)],[215, 192])).
% 0.19/0.54 tff(217,plain,(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))), inference(lemma,lemma(discharge,[]))).
% 0.19/0.54 tff(218,plain,
% 0.19/0.54 ((~(~((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))))))) <=> ((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(219,plain,
% 0.19/0.54 (((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))) <=> (~((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(220,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))) <=> (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(221,plain,
% 0.19/0.54 ((~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))) <=> (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(222,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))) <=> (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))),
% 0.19/0.54 inference(monotonicity,[status(thm)],[221])).
% 0.19/0.54 tff(223,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))) <=> (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))),
% 0.19/0.54 inference(transitivity,[status(thm)],[222, 220])).
% 0.19/0.54 tff(224,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) <=> (sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(225,plain,
% 0.19/0.54 ((~(~((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))))) <=> ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(226,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))) <=> (~((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))))),
% 0.19/0.54 inference(rewrite,[status(thm)],[])).
% 0.19/0.54 tff(227,plain,
% 0.19/0.54 ((~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) <=> (~(~((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))))),
% 0.19/0.54 inference(monotonicity,[status(thm)],[226])).
% 0.19/0.54 tff(228,plain,
% 0.19/0.54 ((~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) <=> ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))),
% 0.19/0.54 inference(transitivity,[status(thm)],[227, 225])).
% 0.19/0.54 tff(229,plain,
% 0.19/0.54 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) <=> (sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))))),
% 0.19/0.55 inference(monotonicity,[status(thm)],[228])).
% 0.19/0.55 tff(230,plain,
% 0.19/0.55 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) <=> (sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))),
% 0.19/0.55 inference(transitivity,[status(thm)],[229, 224])).
% 0.19/0.55 tff(231,plain,
% 0.19/0.55 (((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))))) <=> ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))))),
% 0.19/0.55 inference(monotonicity,[status(thm)],[230, 223])).
% 0.19/0.55 tff(232,plain,
% 0.19/0.55 (((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))))) <=> (~((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))))))),
% 0.19/0.55 inference(transitivity,[status(thm)],[231, 219])).
% 0.19/0.55 tff(233,plain,
% 0.19/0.55 ((~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))) <=> (~(~((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))))))),
% 0.19/0.55 inference(monotonicity,[status(thm)],[232])).
% 0.19/0.55 tff(234,plain,
% 0.19/0.55 ((~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))) <=> ((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn))))))))))),
% 0.19/0.55 inference(transitivity,[status(thm)],[233, 218])).
% 0.19/0.55 tff(235,plain,
% 0.19/0.55 (((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))))) <=> ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.19/0.55 inference(rewrite,[status(thm)],[])).
% 0.19/0.55 tff(236,plain,
% 0.19/0.55 ((~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))) <=> (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))))))),
% 0.19/0.55 inference(monotonicity,[status(thm)],[235])).
% 0.19/0.55 tff(237,plain,
% 0.19/0.55 ((~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))) <=> (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))))))),
% 0.19/0.55 inference(rewrite,[status(thm)],[])).
% 0.19/0.55 tff(238,plain,
% 0.19/0.55 ((~(((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))) => ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn))) | (xm = xn))) & (((sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))) | (xm = xn)) => (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))))) <=> (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))))))))),
% 0.19/0.55 inference(rewrite,[status(thm)],[])).
% 0.19/0.55 tff(239,axiom,(~(((sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))) => ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn))) | (xm = xn))) & (((sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn))) | (xm = xn)) => (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__')).
% 0.19/0.55 tff(240,plain,
% 0.19/0.55 (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.19/0.55 inference(modus_ponens,[status(thm)],[239, 238])).
% 0.38/0.55 tff(241,plain,
% 0.38/0.55 (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[240, 236])).
% 0.38/0.55 tff(242,plain,
% 0.38/0.55 (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[241, 237])).
% 0.38/0.55 tff(243,plain,
% 0.38/0.55 (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[242, 236])).
% 0.38/0.55 tff(244,plain,
% 0.38/0.55 (~((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) & aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) & (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (sdtlseqdt0(szszuzczcdt0(xm), xn) & aElementOf0(xm, slbdtrb0(xn)))))))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[243, 236])).
% 0.38/0.55 tff(245,plain,
% 0.38/0.55 ((~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))) | (~(sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn)) | aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))) | (~((xm = xn) | (~((~sdtlseqdt0(szszuzczcdt0(xm), xn)) | (~aElementOf0(xm, slbdtrb0(xn)))))))))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[244, 234])).
% 0.38/0.55 tff(246,plain,
% 0.38/0.55 (~(sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn)))))),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[245, 217])).
% 0.38/0.55 tff(247,plain,
% 0.38/0.55 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) | (~(xm = xn))),
% 0.38/0.55 inference(tautology,[status(thm)],[])).
% 0.38/0.55 tff(248,plain,
% 0.38/0.55 (~(xm = xn)),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[247, 246])).
% 0.38/0.55 tff(249,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = xn) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (xm = xn) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))))),
% 0.38/0.55 inference(rewrite,[status(thm)],[])).
% 0.38/0.55 tff(250,plain,
% 0.38/0.55 (((xm = xn) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))) | (~aElementOf0(xm, szNzAzT0))) <=> ((xm = xn) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))))),
% 0.38/0.55 inference(rewrite,[status(thm)],[])).
% 0.38/0.55 tff(251,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = xn) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))) | (~aElementOf0(xm, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = xn) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn)))))),
% 0.38/0.55 inference(monotonicity,[status(thm)],[250])).
% 0.38/0.55 tff(252,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = xn) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))) | (~aElementOf0(xm, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (xm = xn) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))))),
% 0.38/0.55 inference(transitivity,[status(thm)],[251, 249])).
% 0.38/0.55 tff(253,plain,
% 0.38/0.55 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | ((xm = xn) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))) | (~aElementOf0(xm, szNzAzT0)))),
% 0.38/0.55 inference(quant_inst,[status(thm)],[])).
% 0.38/0.55 tff(254,plain,
% 0.38/0.55 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~(szszuzczcdt0(W0) = szszuzczcdt0(W1))) | (~aElementOf0(W0, szNzAzT0)))) | (xm = xn) | (~aElementOf0(xm, szNzAzT0)) | (~aElementOf0(xn, szNzAzT0)) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn)))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[253, 252])).
% 0.38/0.55 tff(255,plain,
% 0.38/0.55 ((xm = xn) | (~(szszuzczcdt0(xm) = szszuzczcdt0(xn)))),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[254, 65, 80, 4])).
% 0.38/0.55 tff(256,plain,
% 0.38/0.55 (~(szszuzczcdt0(xm) = szszuzczcdt0(xn))),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[255, 248])).
% 0.38/0.55 tff(257,plain,
% 0.38/0.55 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) | sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))),
% 0.38/0.55 inference(tautology,[status(thm)],[])).
% 0.38/0.55 tff(258,plain,
% 0.38/0.55 (sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[257, 246])).
% 0.38/0.55 tff(259,plain,
% 0.38/0.55 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | aElementOf0(xm, slbdtrb0(xn)) | (xm = xn) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~aElementOf0(xm, slbdtrb0(szszuzczcdt0(xn))))) | (~sdtlseqdt0(szszuzczcdt0(xm), xn))),
% 0.38/0.55 inference(tautology,[status(thm)],[])).
% 0.38/0.55 tff(260,plain,
% 0.38/0.55 (~sdtlseqdt0(szszuzczcdt0(xm), xn)),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[259, 246])).
% 0.38/0.55 tff(261,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), xn) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), xn) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))),
% 0.38/0.55 inference(rewrite,[status(thm)],[])).
% 0.38/0.55 tff(262,plain,
% 0.38/0.55 ((sdtlseqdt0(szszuzczcdt0(xm), xn) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0))) <=> (sdtlseqdt0(szszuzczcdt0(xm), xn) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))),
% 0.38/0.55 inference(rewrite,[status(thm)],[])).
% 0.38/0.55 tff(263,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), xn) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), xn) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0))))),
% 0.38/0.55 inference(monotonicity,[status(thm)],[262])).
% 0.38/0.55 tff(264,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), xn) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), xn) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))),
% 0.38/0.55 inference(transitivity,[status(thm)],[263, 261])).
% 0.38/0.55 tff(265,plain,
% 0.38/0.55 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (sdtlseqdt0(szszuzczcdt0(xm), xn) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(xn, szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)))),
% 0.38/0.55 inference(quant_inst,[status(thm)],[])).
% 0.38/0.55 tff(266,plain,
% 0.38/0.55 ((~![W0: $i, W1: $i] : (sdtlseqdt0(W0, W1) | sdtlseqdt0(szszuzczcdt0(W1), W0) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | sdtlseqdt0(szszuzczcdt0(xm), xn) | (~aElementOf0(xn, szNzAzT0)) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0))),
% 0.38/0.55 inference(modus_ponens,[status(thm)],[265, 264])).
% 0.38/0.55 tff(267,plain,
% 0.38/0.55 (sdtlseqdt0(szszuzczcdt0(xm), xn) | sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[266, 206, 4, 86])).
% 0.38/0.55 tff(268,plain,
% 0.38/0.55 (sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))),
% 0.38/0.55 inference(unit_resolution,[status(thm)],[267, 260])).
% 0.38/0.55 tff(269,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))),
% 0.38/0.55 inference(rewrite,[status(thm)],[])).
% 0.38/0.55 tff(270,plain,
% 0.38/0.55 (((szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm)))) <=> ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))),
% 0.38/0.55 inference(rewrite,[status(thm)],[])).
% 0.38/0.55 tff(271,plain,
% 0.38/0.55 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0))))),
% 0.38/0.56 inference(monotonicity,[status(thm)],[270])).
% 0.38/0.56 tff(272,plain,
% 0.38/0.56 (((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))))) <=> ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)))),
% 0.38/0.56 inference(transitivity,[status(thm)],[271, 269])).
% 0.38/0.56 tff(273,plain,
% 0.38/0.56 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | ((szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0)) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))))),
% 0.38/0.56 inference(quant_inst,[status(thm)],[])).
% 0.38/0.56 tff(274,plain,
% 0.38/0.56 ((~![W0: $i, W1: $i] : ((W0 = W1) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)) | (~sdtlseqdt0(W0, W1)) | (~sdtlseqdt0(W1, W0)))) | (~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (~aElementOf0(szszuzczcdt0(xm), szNzAzT0)) | (szszuzczcdt0(xm) = szszuzczcdt0(xn)) | (~aElementOf0(szszuzczcdt0(xn), szNzAzT0))),
% 0.38/0.56 inference(modus_ponens,[status(thm)],[273, 272])).
% 0.38/0.56 tff(275,plain,
% 0.38/0.56 ((~sdtlseqdt0(szszuzczcdt0(xm), szszuzczcdt0(xn))) | (~sdtlseqdt0(szszuzczcdt0(xn), szszuzczcdt0(xm))) | (szszuzczcdt0(xm) = szszuzczcdt0(xn))),
% 0.38/0.56 inference(unit_resolution,[status(thm)],[274, 182, 86, 25])).
% 0.38/0.56 tff(276,plain,
% 0.38/0.56 ($false),
% 0.38/0.56 inference(unit_resolution,[status(thm)],[275, 268, 258, 256])).
% 0.38/0.56 % SZS output end Proof
% 0.38/0.56 % E exiting
%------------------------------------------------------------------------------