%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM545+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:21:21 AM UTC 2025
% Result : Theorem 1.08s 1.29s
% Output : Proof 1.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NUM545+1 : TPTP v9.0.0. Released v4.0.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n014.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Fri Jun 20 01:24:39 EDT 2025
% 0.12/0.34 % CPUTime :
% 1.08/1.29 % SZS status Theorem
% 1.08/1.29 % SZS output start Proof
% 1.08/1.29 tff(sdtlseqdt0_type, type, (
% 1.08/1.29 sdtlseqdt0: ( $i * $i ) > $o)).
% 1.08/1.29 tff(szmzazxdt0_type, type, (
% 1.08/1.29 szmzazxdt0: $i > $i)).
% 1.08/1.29 tff(xS_type, type, (
% 1.08/1.29 xS: $i)).
% 1.08/1.29 tff(aElementOf0_type, type, (
% 1.08/1.29 aElementOf0: ( $i * $i ) > $o)).
% 1.08/1.29 tff(szNzAzT0_type, type, (
% 1.08/1.29 szNzAzT0: $i)).
% 1.08/1.29 tff(sz00_type, type, (
% 1.08/1.29 sz00: $i)).
% 1.08/1.29 tff(szszuzczcdt0_type, type, (
% 1.08/1.29 szszuzczcdt0: $i > $i)).
% 1.08/1.29 tff(aSubsetOf0_type, type, (
% 1.08/1.29 aSubsetOf0: ( $i * $i ) > $o)).
% 1.08/1.29 tff(slbdtrb0_type, type, (
% 1.08/1.29 slbdtrb0: $i > $i)).
% 1.08/1.29 tff(slcrc0_type, type, (
% 1.08/1.29 slcrc0: $i)).
% 1.08/1.29 tff(aSet0_type, type, (
% 1.08/1.29 aSet0: $i > $o)).
% 1.08/1.29 tff(tptp_fun_W2_1_type, type, (
% 1.08/1.29 tptp_fun_W2_1: ( $i * $i ) > $i)).
% 1.08/1.29 tff(isCountable0_type, type, (
% 1.08/1.29 isCountable0: $i > $o)).
% 1.08/1.29 tff(isFinite0_type, type, (
% 1.08/1.29 isFinite0: $i > $o)).
% 1.08/1.29 tff(tptp_fun_W2_7_type, type, (
% 1.08/1.29 tptp_fun_W2_7: ( $i * $i ) > $i)).
% 1.08/1.29 tff(1,plain,
% 1.08/1.29 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0)))))),
% 1.08/1.29 inference(bind,[status(th)],[])).
% 1.08/1.29 tff(2,plain,
% 1.08/1.29 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))),
% 1.08/1.29 inference(quant_intro,[status(thm)],[1])).
% 1.08/1.29 tff(3,plain,
% 1.08/1.29 (^[W0: $i] : trans(monotonicity(rewrite((aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0))) <=> (~((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0)))))), ((~(aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))) <=> (~(~((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0)))))))), rewrite((~(~((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0)))))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))), ((~(aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))))),
% 1.08/1.29 inference(bind,[status(th)],[])).
% 1.08/1.29 tff(4,plain,
% 1.08/1.29 (![W0: $i] : (~(aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))),
% 1.08/1.29 inference(quant_intro,[status(thm)],[3])).
% 1.08/1.29 tff(5,plain,
% 1.08/1.29 ((~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))) <=> (~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0))))),
% 1.08/1.29 inference(rewrite,[status(thm)],[])).
% 1.08/1.29 tff(6,axiom,(~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__')).
% 1.08/1.29 tff(7,plain,
% 1.08/1.29 (~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[6, 5])).
% 1.08/1.29 tff(8,plain,
% 1.08/1.29 (~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[7, 5])).
% 1.08/1.29 tff(9,plain,
% 1.08/1.29 (~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[8, 5])).
% 1.08/1.29 tff(10,plain,
% 1.08/1.29 (~?[W0: $i] : (aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[9, 5])).
% 1.08/1.29 tff(11,plain,
% 1.08/1.29 (^[W0: $i] : refl($oeq((~(aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0)))), (~(aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0))))))),
% 1.08/1.29 inference(bind,[status(th)],[])).
% 1.08/1.29 tff(12,plain,(
% 1.08/1.29 ![W0: $i] : (~(aElementOf0(W0, szNzAzT0) & aSubsetOf0(xS, slbdtrb0(W0))))),
% 1.08/1.29 inference(nnf-neg,[status(sab)],[10, 11])).
% 1.08/1.29 tff(13,plain,
% 1.08/1.29 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[12, 4])).
% 1.08/1.29 tff(14,plain,
% 1.08/1.29 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[13, 2])).
% 1.08/1.29 tff(15,plain,
% 1.08/1.29 ((slbdtrb0(sz00) = slcrc0) <=> (slbdtrb0(sz00) = slcrc0)),
% 1.08/1.29 inference(rewrite,[status(thm)],[])).
% 1.08/1.29 tff(16,axiom,(slbdtrb0(sz00) = slcrc0), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSegZero')).
% 1.08/1.29 tff(17,plain,
% 1.08/1.29 (slbdtrb0(sz00) = slcrc0),
% 1.08/1.29 inference(modus_ponens,[status(thm)],[16, 15])).
% 1.08/1.29 tff(18,plain,
% 1.08/1.30 (slcrc0 = slbdtrb0(sz00)),
% 1.08/1.30 inference(symmetry,[status(thm)],[17])).
% 1.08/1.30 tff(19,assumption,(xS = slcrc0), introduced(assumption)).
% 1.08/1.30 tff(20,plain,
% 1.08/1.30 (xS = slbdtrb0(sz00)),
% 1.08/1.30 inference(transitivity,[status(thm)],[19, 18])).
% 1.08/1.30 tff(21,plain,
% 1.08/1.30 (aSubsetOf0(xS, slbdtrb0(sz00)) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))),
% 1.08/1.30 inference(monotonicity,[status(thm)],[20])).
% 1.08/1.30 tff(22,plain,
% 1.08/1.30 (aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00)) <=> aSubsetOf0(xS, slbdtrb0(sz00))),
% 1.08/1.30 inference(symmetry,[status(thm)],[21])).
% 1.08/1.30 tff(23,plain,
% 1.08/1.30 (^[W0: $i, W1: $i] : refl(((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(24,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) <=> ![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[23])).
% 1.08/1.30 tff(25,plain,
% 1.08/1.30 (^[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))))), (((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> (((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))))), rewrite((((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))), (((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(26,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> ![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[25])).
% 1.08/1.30 tff(27,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> ![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(28,plain,
% 1.08/1.30 (^[W0: $i, W1: $i] : rewrite(((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(29,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1)))) <=> ![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[28])).
% 1.08/1.30 tff(30,axiom,(![W0: $i, W1: $i] : ((aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0)) => (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSegLess')).
% 1.08/1.30 tff(31,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[30, 29])).
% 1.08/1.30 tff(32,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[31, 27])).
% 1.08/1.30 tff(33,plain,(
% 1.08/1.30 ![W0: $i, W1: $i] : ((~(aElementOf0(W0, szNzAzT0) & aElementOf0(W1, szNzAzT0))) | (sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))))),
% 1.08/1.30 inference(skolemize,[status(sab)],[32])).
% 1.08/1.30 tff(34,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[33, 26])).
% 1.08/1.30 tff(35,plain,
% 1.08/1.30 (![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[34, 24])).
% 1.08/1.30 tff(36,plain,
% 1.08/1.30 (aElementOf0(sz00, szNzAzT0) <=> aElementOf0(sz00, szNzAzT0)),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(37,axiom,(aElementOf0(sz00, szNzAzT0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mZeroNum')).
% 1.08/1.30 tff(38,plain,
% 1.08/1.30 (aElementOf0(sz00, szNzAzT0)),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[37, 36])).
% 1.08/1.30 tff(39,plain,
% 1.08/1.30 (((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(sz00, szNzAzT0)) | (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))))) <=> ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(sz00, szNzAzT0)) | (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(40,plain,
% 1.08/1.30 (((sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(sz00, szNzAzT0))) <=> ((~aElementOf0(sz00, szNzAzT0)) | (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(41,plain,
% 1.08/1.30 (((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(sz00, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((~aElementOf0(sz00, szNzAzT0)) | (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00)))))),
% 1.08/1.30 inference(monotonicity,[status(thm)],[40])).
% 1.08/1.30 tff(42,plain,
% 1.08/1.30 (((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(sz00, szNzAzT0)))) <=> ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(sz00, szNzAzT0)) | (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))))),
% 1.08/1.30 inference(transitivity,[status(thm)],[41, 39])).
% 1.08/1.30 tff(43,plain,
% 1.08/1.30 ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | ((sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))) | (~aElementOf0(sz00, szNzAzT0)) | (~aElementOf0(sz00, szNzAzT0)))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(44,plain,
% 1.08/1.30 ((~![W0: $i, W1: $i] : ((sdtlseqdt0(W0, W1) <=> aSubsetOf0(slbdtrb0(W0), slbdtrb0(W1))) | (~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W0, szNzAzT0)))) | (~aElementOf0(sz00, szNzAzT0)) | (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00)))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[43, 42])).
% 1.08/1.30 tff(45,plain,
% 1.08/1.30 (sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[44, 38, 35])).
% 1.08/1.30 tff(46,plain,
% 1.08/1.30 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0)) <=> ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0)))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(47,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0)) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[46])).
% 1.08/1.30 tff(48,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0)) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(49,plain,
% 1.08/1.30 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, W0)) <=> ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0)))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(50,plain,
% 1.08/1.30 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, W0)) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[49])).
% 1.08/1.30 tff(51,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => sdtlseqdt0(W0, W0))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mLessRefl')).
% 1.08/1.30 tff(52,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[51, 50])).
% 1.08/1.30 tff(53,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[52, 48])).
% 1.08/1.30 tff(54,plain,(
% 1.08/1.30 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(skolemize,[status(sab)],[53])).
% 1.08/1.30 tff(55,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[54, 47])).
% 1.08/1.30 tff(56,plain,
% 1.08/1.30 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))) | ((~aElementOf0(sz00, szNzAzT0)) | sdtlseqdt0(sz00, sz00))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))) | (~aElementOf0(sz00, szNzAzT0)) | sdtlseqdt0(sz00, sz00))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(57,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))) | ((~aElementOf0(sz00, szNzAzT0)) | sdtlseqdt0(sz00, sz00))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(58,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | sdtlseqdt0(W0, W0))) | (~aElementOf0(sz00, szNzAzT0)) | sdtlseqdt0(sz00, sz00)),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[57, 56])).
% 1.08/1.30 tff(59,plain,
% 1.08/1.30 (sdtlseqdt0(sz00, sz00)),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[58, 38, 55])).
% 1.08/1.30 tff(60,plain,
% 1.08/1.30 ((~(sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00)))) | (~sdtlseqdt0(sz00, sz00)) | aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))),
% 1.08/1.30 inference(tautology,[status(thm)],[])).
% 1.08/1.30 tff(61,plain,
% 1.08/1.30 ((~(sdtlseqdt0(sz00, sz00) <=> aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00)))) | aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[60, 59])).
% 1.08/1.30 tff(62,plain,
% 1.08/1.30 (aSubsetOf0(slbdtrb0(sz00), slbdtrb0(sz00))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[61, 45])).
% 1.08/1.30 tff(63,plain,
% 1.08/1.30 (aSubsetOf0(xS, slbdtrb0(sz00))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[62, 22])).
% 1.08/1.30 tff(64,plain,
% 1.08/1.30 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(sz00))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | (~aElementOf0(sz00, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(sz00))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(65,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(sz00))))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(66,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | (~aElementOf0(sz00, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(sz00)))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[65, 64])).
% 1.08/1.30 tff(67,plain,
% 1.08/1.30 (~aSubsetOf0(xS, slbdtrb0(sz00))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[66, 38, 14])).
% 1.08/1.30 tff(68,plain,
% 1.08/1.30 ($false),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[67, 63])).
% 1.08/1.30 tff(69,plain,(~(xS = slcrc0)), inference(lemma,lemma(discharge,[]))).
% 1.08/1.30 tff(70,plain,
% 1.08/1.30 (((xS = slcrc0) | aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))) <=> ((xS = slcrc0) | aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(71,plain,
% 1.08/1.30 (((~(xS = slcrc0)) => aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))) <=> ((xS = slcrc0) | aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(72,axiom,((~(xS = slcrc0)) => aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__2035')).
% 1.08/1.30 tff(73,plain,
% 1.08/1.30 ((xS = slcrc0) | aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[72, 71])).
% 1.08/1.30 tff(74,plain,
% 1.08/1.30 ((xS = slcrc0) | aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[73, 70])).
% 1.08/1.30 tff(75,plain,
% 1.08/1.30 (aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[74, 69])).
% 1.08/1.30 tff(76,plain,
% 1.08/1.30 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | ((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | (~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(77,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | ((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS))))))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(78,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(W0))))) | (~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (~aSubsetOf0(xS, slbdtrb0(szszuzczcdt0(szmzazxdt0(xS)))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[77, 76])).
% 1.08/1.30 tff(79,plain,
% 1.08/1.30 (~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[78, 75, 14])).
% 1.08/1.30 tff(80,plain,
% 1.08/1.30 (((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (szszuzczcdt0(szmzazxdt0(xS)) = sz00)) | aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)),
% 1.08/1.30 inference(tautology,[status(thm)],[])).
% 1.08/1.30 tff(81,plain,
% 1.08/1.30 ((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (szszuzczcdt0(szmzazxdt0(xS)) = sz00)),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[80, 79])).
% 1.08/1.30 tff(82,plain,
% 1.08/1.30 (^[W0: $i] : refl(((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(83,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[82])).
% 1.08/1.30 tff(84,plain,
% 1.08/1.30 (^[W0: $i] : rewrite(((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00)))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(85,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[84])).
% 1.08/1.30 tff(86,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(87,plain,
% 1.08/1.30 (^[W0: $i] : rewrite((aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(88,plain,
% 1.08/1.30 (![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00)))) <=> ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[87])).
% 1.08/1.30 tff(89,axiom,(![W0: $i] : (aElementOf0(W0, szNzAzT0) => (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mSuccNum')).
% 1.08/1.30 tff(90,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[89, 88])).
% 1.08/1.30 tff(91,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[90, 86])).
% 1.08/1.30 tff(92,plain,(
% 1.08/1.30 ![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (aElementOf0(szszuzczcdt0(W0), szNzAzT0) & (~(szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(skolemize,[status(sab)],[91])).
% 1.08/1.30 tff(93,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[92, 85])).
% 1.08/1.30 tff(94,plain,
% 1.08/1.30 (![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[93, 83])).
% 1.08/1.30 tff(95,plain,
% 1.08/1.30 (((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(szmzazxdt0(xS), szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (szszuzczcdt0(szmzazxdt0(xS)) = sz00))))) <=> ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(szmzazxdt0(xS), szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (szszuzczcdt0(szmzazxdt0(xS)) = sz00))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(96,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | ((~aElementOf0(szmzazxdt0(xS), szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (szszuzczcdt0(szmzazxdt0(xS)) = sz00))))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(97,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aElementOf0(W0, szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(W0), szNzAzT0)) | (szszuzczcdt0(W0) = sz00))))) | (~aElementOf0(szmzazxdt0(xS), szNzAzT0)) | (~((~aElementOf0(szszuzczcdt0(szmzazxdt0(xS)), szNzAzT0)) | (szszuzczcdt0(szmzazxdt0(xS)) = sz00)))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[96, 95])).
% 1.08/1.30 tff(98,plain,
% 1.08/1.30 (~aElementOf0(szmzazxdt0(xS), szNzAzT0)),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[97, 94, 81])).
% 1.08/1.30 tff(99,plain,
% 1.08/1.30 (aSet0(szNzAzT0) <=> aSet0(szNzAzT0)),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(100,axiom,(aSet0(szNzAzT0) & isCountable0(szNzAzT0)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mNATSet')).
% 1.08/1.30 tff(101,plain,
% 1.08/1.30 (aSet0(szNzAzT0)),
% 1.08/1.30 inference(and_elim,[status(thm)],[100])).
% 1.08/1.30 tff(102,plain,
% 1.08/1.30 (aSet0(szNzAzT0)),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[101, 99])).
% 1.08/1.30 tff(103,plain,
% 1.08/1.30 (^[W0: $i] : rewrite(((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))))))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(104,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[103])).
% 1.08/1.30 tff(105,plain,
% 1.08/1.30 (^[W0: $i] : refl(((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(106,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[105])).
% 1.08/1.30 tff(107,plain,
% 1.08/1.30 (^[W0: $i] : rewrite(((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(108,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[107])).
% 1.08/1.30 tff(109,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))))),
% 1.08/1.30 inference(transitivity,[status(thm)],[108, 106])).
% 1.08/1.30 tff(110,plain,
% 1.08/1.30 (^[W0: $i] : rewrite(((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))) <=> ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(111,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[110])).
% 1.08/1.30 tff(112,plain,
% 1.08/1.30 (^[W0: $i] : rewrite(((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | ((~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))) <=> ((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(113,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | ((~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[112])).
% 1.08/1.30 tff(114,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(115,plain,
% 1.08/1.30 (^[W0: $i] : trans(monotonicity(quant_intro(proof_bind(^[W1: $i] : rewrite((aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0)))) <=> (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))), (![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0)))) <=> ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))), ((aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0))))) <=> (aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))), rewrite((aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))) <=> ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))), ((aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0))))) <=> ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))))),
% 1.08/1.30 inference(bind,[status(th)],[])).
% 1.08/1.30 tff(116,plain,
% 1.08/1.30 (![W0: $i] : (aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0))))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 1.08/1.30 inference(quant_intro,[status(thm)],[115])).
% 1.08/1.30 tff(117,axiom,(![W0: $i] : (aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mDefSub')).
% 1.08/1.30 tff(118,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[117, 116])).
% 1.08/1.30 tff(119,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[118, 114])).
% 1.08/1.30 tff(120,plain,(
% 1.08/1.30 ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | ((~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0)))))))),
% 1.08/1.30 inference(skolemize,[status(sab)],[119])).
% 1.08/1.30 tff(121,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (((~aSubsetOf0(W1, W0)) | (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))) & (aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[120, 113])).
% 1.08/1.30 tff(122,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[121, 111])).
% 1.08/1.30 tff(123,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))) | (~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[122, 109])).
% 1.08/1.30 tff(124,plain,
% 1.08/1.30 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[123, 104])).
% 1.08/1.30 tff(125,plain,
% 1.08/1.30 (((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))))))) | ((~aSet0(szNzAzT0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0))))))))))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))))))) | (~aSet0(szNzAzT0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0))))))))))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(126,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))))))) | ((~aSet0(szNzAzT0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0))))))))))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(127,plain,
% 1.08/1.30 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, W0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, W0), W1)) | aElementOf0(tptp_fun_W2_1(W1, W0), W0))))) | (~((~aSubsetOf0(W1, W0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0))))))))))) | (~aSet0(szNzAzT0)) | ![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0)))))))))),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[126, 125])).
% 1.08/1.30 tff(128,plain,
% 1.08/1.30 (![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0)))))))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[127, 124, 102])).
% 1.08/1.30 tff(129,plain,
% 1.08/1.30 ((~![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0)))))))))) | (~((~(aSubsetOf0(xS, szNzAzT0) | (~aSet0(xS)) | (~((~aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), xS)) | aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))))))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(130,plain,
% 1.08/1.30 (~((~(aSubsetOf0(xS, szNzAzT0) | (~aSet0(xS)) | (~((~aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), xS)) | aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[129, 128])).
% 1.08/1.30 tff(131,plain,
% 1.08/1.30 (((~(aSubsetOf0(xS, szNzAzT0) | (~aSet0(xS)) | (~((~aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), xS)) | aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))))) | ((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))),
% 1.08/1.30 inference(tautology,[status(thm)],[])).
% 1.08/1.30 tff(132,plain,
% 1.08/1.30 ((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[131, 130])).
% 1.08/1.30 tff(133,plain,
% 1.08/1.30 (aSubsetOf0(xS, szNzAzT0) <=> aSubsetOf0(xS, szNzAzT0)),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(134,axiom,(aSubsetOf0(xS, szNzAzT0) & isFinite0(xS)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1986')).
% 1.08/1.30 tff(135,plain,
% 1.08/1.30 (aSubsetOf0(xS, szNzAzT0)),
% 1.08/1.30 inference(and_elim,[status(thm)],[134])).
% 1.08/1.30 tff(136,plain,
% 1.08/1.30 (aSubsetOf0(xS, szNzAzT0)),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[135, 133])).
% 1.08/1.30 tff(137,plain,
% 1.08/1.30 ((~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))),
% 1.08/1.30 inference(tautology,[status(thm)],[])).
% 1.08/1.30 tff(138,plain,
% 1.08/1.30 ((~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[137, 136])).
% 1.08/1.30 tff(139,plain,
% 1.08/1.30 (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[138, 132])).
% 1.08/1.30 tff(140,plain,
% 1.08/1.30 (((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))) | ![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))),
% 1.08/1.30 inference(tautology,[status(thm)],[])).
% 1.08/1.30 tff(141,plain,
% 1.08/1.30 (![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[140, 139])).
% 1.08/1.30 tff(142,plain,
% 1.08/1.30 (((~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))) | ((~aElementOf0(szmzazxdt0(xS), xS)) | aElementOf0(szmzazxdt0(xS), szNzAzT0))) <=> ((~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))) | (~aElementOf0(szmzazxdt0(xS), xS)) | aElementOf0(szmzazxdt0(xS), szNzAzT0))),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(143,plain,
% 1.08/1.30 ((~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))) | ((~aElementOf0(szmzazxdt0(xS), xS)) | aElementOf0(szmzazxdt0(xS), szNzAzT0))),
% 1.08/1.30 inference(quant_inst,[status(thm)],[])).
% 1.08/1.30 tff(144,plain,
% 1.08/1.30 ((~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))) | (~aElementOf0(szmzazxdt0(xS), xS)) | aElementOf0(szmzazxdt0(xS), szNzAzT0)),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[143, 142])).
% 1.08/1.30 tff(145,plain,
% 1.08/1.30 (~aElementOf0(szmzazxdt0(xS), xS)),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[144, 141, 98])).
% 1.08/1.30 tff(146,plain,
% 1.08/1.30 (((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))) | aElementOf0(szmzazxdt0(xS), xS)),
% 1.08/1.30 inference(tautology,[status(thm)],[])).
% 1.08/1.30 tff(147,plain,
% 1.08/1.30 ((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))),
% 1.08/1.30 inference(unit_resolution,[status(thm)],[146, 145])).
% 1.08/1.30 tff(148,plain,
% 1.08/1.30 (isFinite0(xS) <=> isFinite0(xS)),
% 1.08/1.30 inference(rewrite,[status(thm)],[])).
% 1.08/1.30 tff(149,plain,
% 1.08/1.30 (isFinite0(xS)),
% 1.08/1.30 inference(and_elim,[status(thm)],[134])).
% 1.08/1.30 tff(150,plain,
% 1.08/1.30 (isFinite0(xS)),
% 1.08/1.30 inference(modus_ponens,[status(thm)],[149, 148])).
% 1.08/1.30 tff(151,plain,
% 1.08/1.30 (^[W0: $i] : trans(monotonicity(quant_intro(proof_bind(^[W1: $i] : rewrite((~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))) <=> (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))), (![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))) <=> ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))), (((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))))))))), rewrite(((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))), (((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))))),
% 1.08/1.31 inference(bind,[status(th)],[])).
% 1.08/1.31 tff(152,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))),
% 1.08/1.31 inference(quant_intro,[status(thm)],[151])).
% 1.08/1.31 tff(153,plain,
% 1.08/1.31 (^[W0: $i] : refl(((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))))),
% 1.08/1.31 inference(bind,[status(th)],[])).
% 1.08/1.31 tff(154,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))),
% 1.08/1.31 inference(quant_intro,[status(thm)],[153])).
% 1.08/1.31 tff(155,plain,
% 1.08/1.31 (^[W0: $i] : rewrite(((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))))),
% 1.08/1.31 inference(bind,[status(th)],[])).
% 1.08/1.31 tff(156,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))),
% 1.08/1.31 inference(quant_intro,[status(thm)],[155])).
% 1.08/1.31 tff(157,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))),
% 1.08/1.31 inference(transitivity,[status(thm)],[156, 154])).
% 1.08/1.31 tff(158,plain,
% 1.08/1.31 (^[W0: $i] : trans(monotonicity(trans(monotonicity(rewrite((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0))) <=> (~((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0))))), ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) <=> (~(~((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0))))))), rewrite((~(~((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)))), ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0))))), quant_intro(proof_bind(^[W1: $i] : trans(monotonicity(rewrite(((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) <=> ((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))), rewrite(((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))) <=> ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))), ((((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) <=> (((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))), rewrite((((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) <=> (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))), ((((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) <=> (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))))), (![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) <=> ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))), (((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))) <=> (((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0))) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))))), rewrite((((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0))) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))), (((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))) <=> ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))))),
% 1.08/1.31 inference(bind,[status(th)],[])).
% 1.08/1.31 tff(159,plain,
% 1.08/1.31 (![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))) <=> ![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))),
% 1.08/1.31 inference(quant_intro,[status(thm)],[158])).
% 1.08/1.31 tff(160,plain,
% 1.08/1.31 (^[W0: $i] : rewrite(((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((W1 = szmzazxdt0(W0)) | ((~aElementOf0(W1, W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))) <=> ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))),
% 1.08/1.31 inference(bind,[status(th)],[])).
% 1.08/1.31 tff(161,plain,
% 1.08/1.31 (![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((W1 = szmzazxdt0(W0)) | ((~aElementOf0(W1, W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))) <=> ![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))),
% 1.08/1.31 inference(quant_intro,[status(thm)],[160])).
% 1.08/1.31 tff(162,plain,
% 1.08/1.31 (![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))) <=> ![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))),
% 1.08/1.31 inference(rewrite,[status(thm)],[])).
% 1.08/1.31 tff(163,plain,
% 1.08/1.31 (^[W0: $i] : trans(monotonicity(rewrite(((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0)) & (~(W0 = slcrc0))) <=> (aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))), quant_intro(proof_bind(^[W1: $i] : rewrite(((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W2, W1)))) <=> ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))), (![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W2, W1)))) <=> ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))), ((((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0)) & (~(W0 = slcrc0))) => ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W2, W1))))) <=> ((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0))) => ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))), rewrite(((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0))) => ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))) <=> ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))), ((((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0)) & (~(W0 = slcrc0))) => ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W2, W1))))) <=> ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))))),
% 1.08/1.31 inference(bind,[status(th)],[])).
% 1.08/1.31 tff(164,plain,
% 1.08/1.31 (![W0: $i] : (((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0)) & (~(W0 = slcrc0))) => ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W2, W1))))) <=> ![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))),
% 1.08/1.31 inference(quant_intro,[status(thm)],[163])).
% 1.08/1.31 tff(165,axiom,(![W0: $i] : (((aSubsetOf0(W0, szNzAzT0) & isFinite0(W0)) & (~(W0 = slcrc0))) => ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W2, W1)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mDefMax')).
% 1.08/1.31 tff(166,plain,
% 1.08/1.31 (![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[165, 164])).
% 1.08/1.31 tff(167,plain,
% 1.08/1.31 (![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : ((W1 = szmzazxdt0(W0)) <=> (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[166, 162])).
% 1.08/1.31 tff(168,plain,(
% 1.08/1.31 ![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((W1 = szmzazxdt0(W0)) | ((~aElementOf0(W1, W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1)))))))),
% 1.08/1.31 inference(skolemize,[status(sab)],[167])).
% 1.08/1.31 tff(169,plain,
% 1.08/1.31 (![W0: $i] : ((~(aSubsetOf0(W0, szNzAzT0) & isFinite0(W0) & (~(W0 = slcrc0)))) | ![W1: $i] : (((~(W1 = szmzazxdt0(W0))) | (aElementOf0(W1, W0) & ![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1)))) & ((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[168, 161])).
% 1.08/1.31 tff(170,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[169, 159])).
% 1.08/1.31 tff(171,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))) | (~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))))))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[170, 157])).
% 1.08/1.31 tff(172,plain,
% 1.08/1.31 (![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[171, 152])).
% 1.08/1.31 tff(173,plain,
% 1.08/1.31 (((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | ((xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~isFinite0(xS)))) <=> ((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | (xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~isFinite0(xS)))),
% 1.08/1.31 inference(rewrite,[status(thm)],[])).
% 1.08/1.31 tff(174,plain,
% 1.08/1.31 (((xS = slcrc0) | (~isFinite0(xS)) | (~aSubsetOf0(xS, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) <=> ((xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~isFinite0(xS)))),
% 1.08/1.31 inference(rewrite,[status(thm)],[])).
% 1.08/1.31 tff(175,plain,
% 1.08/1.31 (((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | ((xS = slcrc0) | (~isFinite0(xS)) | (~aSubsetOf0(xS, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))))) <=> ((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | ((xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~isFinite0(xS))))),
% 1.08/1.31 inference(monotonicity,[status(thm)],[174])).
% 1.08/1.31 tff(176,plain,
% 1.08/1.31 (((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | ((xS = slcrc0) | (~isFinite0(xS)) | (~aSubsetOf0(xS, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))))) <=> ((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | (xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~isFinite0(xS)))),
% 1.08/1.31 inference(transitivity,[status(thm)],[175, 173])).
% 1.08/1.31 tff(177,plain,
% 1.08/1.31 ((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | ((xS = slcrc0) | (~isFinite0(xS)) | (~aSubsetOf0(xS, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))))),
% 1.08/1.31 inference(quant_inst,[status(thm)],[])).
% 1.08/1.31 tff(178,plain,
% 1.08/1.31 ((~![W0: $i] : ((W0 = slcrc0) | (~isFinite0(W0)) | (~aSubsetOf0(W0, szNzAzT0)) | ![W1: $i] : (~((~((~aElementOf0(W1, W0)) | (W1 = szmzazxdt0(W0)) | (~((~aElementOf0(tptp_fun_W2_7(W1, W0), W0)) | sdtlseqdt0(tptp_fun_W2_7(W1, W0), W1))))) | (~((~(W1 = szmzazxdt0(W0))) | (~((~aElementOf0(W1, W0)) | (~![W2: $i] : ((~aElementOf0(W2, W0)) | sdtlseqdt0(W2, W1))))))))))) | (xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1))))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~isFinite0(xS))),
% 1.08/1.31 inference(modus_ponens,[status(thm)],[177, 176])).
% 1.08/1.31 tff(179,plain,
% 1.08/1.31 ((xS = slcrc0) | ![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))),
% 1.08/1.31 inference(unit_resolution,[status(thm)],[178, 172, 136, 150])).
% 1.08/1.31 tff(180,plain,
% 1.08/1.31 (![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))),
% 1.08/1.31 inference(unit_resolution,[status(thm)],[179, 69])).
% 1.08/1.31 tff(181,plain,
% 1.08/1.31 (((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))))) <=> ((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS)))))))),
% 1.08/1.31 inference(rewrite,[status(thm)],[])).
% 1.08/1.31 tff(182,plain,
% 1.08/1.31 ((~((~((~aElementOf0(szmzazxdt0(xS), xS)) | (szmzazxdt0(xS) = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(szmzazxdt0(xS), xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(szmzazxdt0(xS), xS), szmzazxdt0(xS)))))) | (~((~(szmzazxdt0(xS) = szmzazxdt0(xS))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS)))))))))) <=> (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))))),
% 1.08/1.31 inference(rewrite,[status(thm)],[])).
% 1.08/1.31 tff(183,plain,
% 1.08/1.31 (((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~((~aElementOf0(szmzazxdt0(xS), xS)) | (szmzazxdt0(xS) = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(szmzazxdt0(xS), xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(szmzazxdt0(xS), xS), szmzazxdt0(xS)))))) | (~((~(szmzazxdt0(xS) = szmzazxdt0(xS))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))))))))) <=> ((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS)))))))),
% 1.08/1.31 inference(monotonicity,[status(thm)],[182])).
% 1.08/1.31 tff(184,plain,
% 1.08/1.31 (((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~((~aElementOf0(szmzazxdt0(xS), xS)) | (szmzazxdt0(xS) = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(szmzazxdt0(xS), xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(szmzazxdt0(xS), xS), szmzazxdt0(xS)))))) | (~((~(szmzazxdt0(xS) = szmzazxdt0(xS))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))))))))) <=> ((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS)))))))),
% 1.08/1.31 inference(transitivity,[status(thm)],[183, 181])).
% 1.08/1.31 tff(185,plain,
% 1.08/1.31 ((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~((~aElementOf0(szmzazxdt0(xS), xS)) | (szmzazxdt0(xS) = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(szmzazxdt0(xS), xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(szmzazxdt0(xS), xS), szmzazxdt0(xS)))))) | (~((~(szmzazxdt0(xS) = szmzazxdt0(xS))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))))))))),
% 1.16/1.32 inference(quant_inst,[status(thm)],[])).
% 1.16/1.32 tff(186,plain,
% 1.16/1.32 ((~![W1: $i] : (~((~((~aElementOf0(W1, xS)) | (W1 = szmzazxdt0(xS)) | (~((~aElementOf0(tptp_fun_W2_7(W1, xS), xS)) | sdtlseqdt0(tptp_fun_W2_7(W1, xS), W1))))) | (~((~(W1 = szmzazxdt0(xS))) | (~((~aElementOf0(W1, xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, W1)))))))))) | (~((~aElementOf0(szmzazxdt0(xS), xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | sdtlseqdt0(W2, szmzazxdt0(xS))))))),
% 1.16/1.32 inference(modus_ponens,[status(thm)],[185, 184])).
% 1.16/1.32 tff(187,plain,
% 1.16/1.32 ($false),
% 1.16/1.32 inference(unit_resolution,[status(thm)],[186, 180, 147])).
% 1.16/1.32 % SZS output end Proof
% 1.16/1.32 % E exiting
%------------------------------------------------------------------------------