%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM600+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.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:32 AM UTC 2025
% Result : Theorem 31.14s 31.33s
% Output : Proof 31.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : NUM600+1 : TPTP v9.0.0. Released v4.0.0.
% 0.04/0.12 % Command : run_E %s %d THM
% 0.12/0.34 % Computer : n010.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:35:41 EDT 2025
% 0.12/0.34 % CPUTime :
% 31.14/31.33 % SZS status Theorem
% 31.14/31.33 % SZS output start Proof
% 31.14/31.33 tff(aElementOf0_type, type, (
% 31.14/31.33 aElementOf0: ( $i * $i ) > $o)).
% 31.14/31.33 tff(szNzAzT0_type, type, (
% 31.14/31.33 szNzAzT0: $i)).
% 31.14/31.33 tff(tptp_fun_W4_13_type, type, (
% 31.14/31.33 tptp_fun_W4_13: ( $i * $i * $i ) > $i)).
% 31.14/31.33 tff(xe_type, type, (
% 31.14/31.33 xe: $i)).
% 31.14/31.33 tff(sdtlbdtrb0_type, type, (
% 31.14/31.33 sdtlbdtrb0: ( $i * $i ) > $i)).
% 31.14/31.33 tff(szDzizrdt0_type, type, (
% 31.14/31.33 szDzizrdt0: $i > $i)).
% 31.14/31.33 tff(xd_type, type, (
% 31.14/31.33 xd: $i)).
% 31.14/31.33 tff(tptp_fun_W0_24_type, type, (
% 31.14/31.33 tptp_fun_W0_24: $i)).
% 31.14/31.33 tff(sdtlpdtrp0_type, type, (
% 31.14/31.33 sdtlpdtrp0: ( $i * $i ) > $i)).
% 31.14/31.33 tff(sdtlcdtrc0_type, type, (
% 31.14/31.33 sdtlcdtrc0: ( $i * $i ) > $i)).
% 31.14/31.33 tff(aSet0_type, type, (
% 31.14/31.33 aSet0: $i > $o)).
% 31.14/31.33 tff(tptp_fun_W3_14_type, type, (
% 31.14/31.33 tptp_fun_W3_14: ( $i * $i * $i ) > $i)).
% 31.14/31.33 tff(tptp_fun_W4_15_type, type, (
% 31.14/31.33 tptp_fun_W4_15: ( $i * $i * $i ) > $i)).
% 31.14/31.33 tff(aSubsetOf0_type, type, (
% 31.14/31.33 aSubsetOf0: ( $i * $i ) > $o)).
% 31.14/31.33 tff(szDzozmdt0_type, type, (
% 31.14/31.33 szDzozmdt0: $i > $i)).
% 31.14/31.33 tff(aFunction0_type, type, (
% 31.14/31.33 aFunction0: $i > $o)).
% 31.14/31.33 tff(xC_type, type, (
% 31.14/31.33 xC: $i)).
% 31.14/31.33 tff(slbdtsldtrb0_type, type, (
% 31.14/31.33 slbdtsldtrb0: ( $i * $i ) > $i)).
% 31.14/31.33 tff(xk_type, type, (
% 31.14/31.33 xk: $i)).
% 31.14/31.33 tff(szszuzczcdt0_type, type, (
% 31.14/31.33 szszuzczcdt0: $i > $i)).
% 31.14/31.33 tff(xN_type, type, (
% 31.14/31.33 xN: $i)).
% 31.14/31.33 tff(szmzizndt0_type, type, (
% 31.14/31.33 szmzizndt0: $i > $i)).
% 31.14/31.33 tff(aElement0_type, type, (
% 31.14/31.33 aElement0: $i > $o)).
% 31.14/31.33 tff(xT_type, type, (
% 31.14/31.33 xT: $i)).
% 31.14/31.33 tff(isFinite0_type, type, (
% 31.14/31.33 isFinite0: $i > $o)).
% 31.14/31.33 tff(isCountable0_type, type, (
% 31.14/31.33 isCountable0: $i > $o)).
% 31.14/31.33 tff(xO_type, type, (
% 31.14/31.33 xO: $i)).
% 31.14/31.33 tff(tptp_fun_W2_1_type, type, (
% 31.14/31.33 tptp_fun_W2_1: ( $i * $i ) > $i)).
% 31.14/31.33 tff(1,plain,
% 31.14/31.33 ((szDzozmdt0(xd) = szNzAzT0) <=> (szDzozmdt0(xd) = szNzAzT0)),
% 31.14/31.33 inference(rewrite,[status(thm)],[])).
% 31.14/31.33 tff(2,axiom,((aFunction0(xd) & (szDzozmdt0(xd) = szNzAzT0)) & ![W0: $i] : (aElementOf0(W0, szNzAzT0) => ![W1: $i] : ((aSet0(W1) & aElementOf0(W1, slbdtsldtrb0(sdtlpdtrp0(xN, szszuzczcdt0(W0)), xk))) => (sdtlpdtrp0(xd, W0) = sdtlpdtrp0(sdtlpdtrp0(xC, W0), W1))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__4730')).
% 31.14/31.33 tff(3,plain,
% 31.14/31.33 (aFunction0(xd) & (szDzozmdt0(xd) = szNzAzT0)),
% 31.14/31.33 inference(and_elim,[status(thm)],[2])).
% 31.14/31.33 tff(4,plain,
% 31.14/31.33 (szDzozmdt0(xd) = szNzAzT0),
% 31.14/31.33 inference(and_elim,[status(thm)],[3])).
% 31.14/31.33 tff(5,plain,
% 31.14/31.33 (szDzozmdt0(xd) = szNzAzT0),
% 31.14/31.33 inference(modus_ponens,[status(thm)],[4, 1])).
% 31.14/31.33 tff(6,plain,
% 31.14/31.33 (szNzAzT0 = szDzozmdt0(xd)),
% 31.14/31.33 inference(symmetry,[status(thm)],[5])).
% 31.14/31.33 tff(7,plain,
% 31.14/31.33 ((szDzozmdt0(xe) = szNzAzT0) <=> (szDzozmdt0(xe) = szNzAzT0)),
% 31.14/31.33 inference(rewrite,[status(thm)],[])).
% 31.14/31.33 tff(8,axiom,((aFunction0(xe) & (szDzozmdt0(xe) = szNzAzT0)) & ![W0: $i] : (aElementOf0(W0, szNzAzT0) => (sdtlpdtrp0(xe, W0) = szmzizndt0(sdtlpdtrp0(xN, W0))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__4660')).
% 31.14/31.33 tff(9,plain,
% 31.14/31.33 (aFunction0(xe) & (szDzozmdt0(xe) = szNzAzT0)),
% 31.14/31.33 inference(and_elim,[status(thm)],[8])).
% 31.14/31.33 tff(10,plain,
% 31.14/31.33 (szDzozmdt0(xe) = szNzAzT0),
% 31.14/31.33 inference(and_elim,[status(thm)],[9])).
% 31.14/31.33 tff(11,plain,
% 31.14/31.33 (szDzozmdt0(xe) = szNzAzT0),
% 31.14/31.33 inference(modus_ponens,[status(thm)],[10, 7])).
% 31.14/31.33 tff(12,plain,
% 31.14/31.33 (szDzozmdt0(xe) = szDzozmdt0(xd)),
% 31.14/31.33 inference(transitivity,[status(thm)],[11, 6])).
% 31.14/31.33 tff(13,plain,
% 31.14/31.33 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe)) <=> aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd))),
% 31.14/31.33 inference(monotonicity,[status(thm)],[12])).
% 31.14/31.33 tff(14,plain,
% 31.14/31.33 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)) <=> aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))),
% 31.14/31.33 inference(symmetry,[status(thm)],[13])).
% 31.14/31.33 tff(15,plain,
% 31.14/31.33 (aSet0(xT) <=> aSet0(xT)),
% 31.14/31.33 inference(rewrite,[status(thm)],[])).
% 31.14/31.33 tff(16,axiom,(aSet0(xT) & isFinite0(xT)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__3291')).
% 31.14/31.33 tff(17,plain,
% 31.14/31.33 (aSet0(xT)),
% 31.14/31.33 inference(and_elim,[status(thm)],[16])).
% 31.14/31.33 tff(18,plain,
% 31.14/31.33 (aSet0(xT)),
% 31.14/31.33 inference(modus_ponens,[status(thm)],[17, 15])).
% 31.14/31.33 tff(19,plain,
% 31.14/31.33 (^[W0: $i] : refl(((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))))),
% 31.14/31.33 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(20,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[19])).
% 31.14/31.34 tff(21,plain,
% 31.14/31.34 (^[W0: $i] : rewrite(((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(22,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[21])).
% 31.14/31.34 tff(23,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(transitivity,[status(thm)],[22, 20])).
% 31.14/31.34 tff(24,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(25,plain,
% 31.14/31.34 (^[W0: $i] : trans(monotonicity(quant_intro(proof_bind(^[W1: $i] : rewrite((aElementOf0(W1, W0) => aElement0(W1)) <=> (aElement0(W1) | (~aElementOf0(W1, W0))))), (![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1)) <=> ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))), ((aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1))) <=> (aSet0(W0) => ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))))), rewrite((aSet0(W0) => ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0)))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))), ((aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1))) <=> ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(26,plain,
% 31.14/31.34 (![W0: $i] : (aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1))) <=> ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[25])).
% 31.14/31.34 tff(27,axiom,(![W0: $i] : (aSet0(W0) => ![W1: $i] : (aElementOf0(W1, W0) => aElement0(W1)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mEOfElem')).
% 31.14/31.34 tff(28,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[27, 26])).
% 31.14/31.34 tff(29,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[28, 24])).
% 31.14/31.34 tff(30,plain,(
% 31.14/31.34 ![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(skolemize,[status(sab)],[29])).
% 31.14/31.34 tff(31,plain,
% 31.14/31.34 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[30, 23])).
% 31.14/31.34 tff(32,plain,
% 31.14/31.34 (((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | ((~aSet0(xT)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT))))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | (~aSet0(xT)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT))))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(33,plain,
% 31.14/31.34 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | ((~aSet0(xT)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT))))),
% 31.14/31.34 inference(quant_inst,[status(thm)],[])).
% 31.14/31.34 tff(34,plain,
% 31.14/31.34 ((~![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, W0))))) | (~aSet0(xT)) | ![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT)))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[33, 32])).
% 31.14/31.34 tff(35,plain,
% 31.14/31.34 (![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT)))),
% 31.14/31.34 inference(unit_resolution,[status(thm)],[34, 31, 18])).
% 31.14/31.34 tff(36,plain,
% 31.14/31.34 (aElementOf0(szDzizrdt0(xd), xT) <=> aElementOf0(szDzizrdt0(xd), xT)),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(37,axiom,(aElementOf0(szDzizrdt0(xd), xT) & isCountable0(sdtlbdtrb0(xd, szDzizrdt0(xd)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__4854')).
% 31.14/31.34 tff(38,plain,
% 31.14/31.34 (aElementOf0(szDzizrdt0(xd), xT)),
% 31.14/31.34 inference(and_elim,[status(thm)],[37])).
% 31.14/31.34 tff(39,plain,
% 31.14/31.34 (aElementOf0(szDzizrdt0(xd), xT)),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[38, 36])).
% 31.14/31.34 tff(40,plain,
% 31.14/31.34 (((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT)))) | (aElement0(szDzizrdt0(xd)) | (~aElementOf0(szDzizrdt0(xd), xT)))) <=> ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT)))) | aElement0(szDzizrdt0(xd)) | (~aElementOf0(szDzizrdt0(xd), xT)))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(41,plain,
% 31.14/31.34 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT)))) | (aElement0(szDzizrdt0(xd)) | (~aElementOf0(szDzizrdt0(xd), xT)))),
% 31.14/31.34 inference(quant_inst,[status(thm)],[])).
% 31.14/31.34 tff(42,plain,
% 31.14/31.34 ((~![W1: $i] : (aElement0(W1) | (~aElementOf0(W1, xT)))) | aElement0(szDzizrdt0(xd)) | (~aElementOf0(szDzizrdt0(xd), xT))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[41, 40])).
% 31.14/31.34 tff(43,plain,
% 31.14/31.34 (aElement0(szDzizrdt0(xd))),
% 31.14/31.34 inference(unit_resolution,[status(thm)],[42, 39, 35])).
% 31.14/31.34 tff(44,plain,
% 31.14/31.34 (aFunction0(xd) <=> aFunction0(xd)),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(45,plain,
% 31.14/31.34 (aFunction0(xd)),
% 31.14/31.34 inference(and_elim,[status(thm)],[3])).
% 31.14/31.34 tff(46,plain,
% 31.14/31.34 (aFunction0(xd)),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[45, 44])).
% 31.14/31.34 tff(47,plain,
% 31.14/31.34 (^[W0: $i, W1: $i] : refl((aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0))) <=> (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(48,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0))) <=> ![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[47])).
% 31.14/31.34 tff(49,plain,
% 31.14/31.34 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aFunction0(W0) & aElement0(W1)) <=> (~((~aElement0(W1)) | (~aFunction0(W0))))), ((~(aFunction0(W0) & aElement0(W1))) <=> (~(~((~aElement0(W1)) | (~aFunction0(W0))))))), rewrite((~(~((~aElement0(W1)) | (~aFunction0(W0))))) <=> ((~aElement0(W1)) | (~aFunction0(W0)))), ((~(aFunction0(W0) & aElement0(W1))) <=> ((~aElement0(W1)) | (~aFunction0(W0))))), (((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> (((~aElement0(W1)) | (~aFunction0(W0))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))))), rewrite((((~aElement0(W1)) | (~aFunction0(W0))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))), (((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(50,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> ![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[49])).
% 31.14/31.34 tff(51,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> ![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(52,plain,
% 31.14/31.34 (^[W0: $i, W1: $i] : rewrite(((aFunction0(W0) & aElement0(W1)) => aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(53,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : ((aFunction0(W0) & aElement0(W1)) => aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0))) <=> ![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[52])).
% 31.14/31.34 tff(54,axiom,(![W0: $i, W1: $i] : ((aFunction0(W0) & aElement0(W1)) => aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mPttSet')).
% 31.14/31.34 tff(55,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[54, 53])).
% 31.14/31.34 tff(56,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[55, 51])).
% 31.14/31.34 tff(57,plain,(
% 31.14/31.34 ![W0: $i, W1: $i] : ((~(aFunction0(W0) & aElement0(W1))) | aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)))),
% 31.14/31.34 inference(skolemize,[status(sab)],[56])).
% 31.14/31.34 tff(58,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[57, 50])).
% 31.14/31.34 tff(59,plain,
% 31.14/31.34 (![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[58, 48])).
% 31.14/31.34 tff(60,plain,
% 31.14/31.34 (((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | ((~aFunction0(xd)) | (~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)))) <=> ((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | (~aFunction0(xd)) | (~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(61,plain,
% 31.14/31.34 ((aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)) | (~aElement0(szDzizrdt0(xd))) | (~aFunction0(xd))) <=> ((~aFunction0(xd)) | (~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(62,plain,
% 31.14/31.34 (((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)) | (~aElement0(szDzizrdt0(xd))) | (~aFunction0(xd)))) <=> ((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | ((~aFunction0(xd)) | (~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd))))),
% 31.14/31.34 inference(monotonicity,[status(thm)],[61])).
% 31.14/31.34 tff(63,plain,
% 31.14/31.34 (((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)) | (~aElement0(szDzizrdt0(xd))) | (~aFunction0(xd)))) <=> ((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | (~aFunction0(xd)) | (~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)))),
% 31.14/31.34 inference(transitivity,[status(thm)],[62, 60])).
% 31.14/31.34 tff(64,plain,
% 31.14/31.34 ((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)) | (~aElement0(szDzizrdt0(xd))) | (~aFunction0(xd)))),
% 31.14/31.34 inference(quant_inst,[status(thm)],[])).
% 31.14/31.34 tff(65,plain,
% 31.14/31.34 ((~![W0: $i, W1: $i] : (aSubsetOf0(sdtlbdtrb0(W0, W1), szDzozmdt0(W0)) | (~aElement0(W1)) | (~aFunction0(W0)))) | (~aFunction0(xd)) | (~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[64, 63])).
% 31.14/31.34 tff(66,plain,
% 31.14/31.34 ((~aElement0(szDzizrdt0(xd))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd))),
% 31.14/31.34 inference(unit_resolution,[status(thm)],[65, 59, 46])).
% 31.14/31.34 tff(67,plain,
% 31.14/31.34 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd))),
% 31.14/31.34 inference(unit_resolution,[status(thm)],[66, 43])).
% 31.14/31.34 tff(68,plain,
% 31.14/31.34 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[67, 14])).
% 31.14/31.34 tff(69,plain,
% 31.14/31.34 (aFunction0(xe) <=> aFunction0(xe)),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(70,plain,
% 31.14/31.34 (aFunction0(xe)),
% 31.14/31.34 inference(and_elim,[status(thm)],[9])).
% 31.14/31.34 tff(71,plain,
% 31.14/31.34 (aFunction0(xe)),
% 31.14/31.34 inference(modus_ponens,[status(thm)],[70, 69])).
% 31.14/31.34 tff(72,plain,
% 31.14/31.34 (^[W0: $i] : rewrite(((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))))))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(73,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[72])).
% 31.14/31.34 tff(74,plain,
% 31.14/31.34 (^[W0: $i] : refl(((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(75,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[74])).
% 31.14/31.34 tff(76,plain,
% 31.14/31.34 (^[W0: $i] : rewrite(((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(77,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[76])).
% 31.14/31.34 tff(78,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))))))),
% 31.14/31.34 inference(transitivity,[status(thm)],[77, 75])).
% 31.14/31.34 tff(79,plain,
% 31.14/31.34 (^[W0: $i] : rewrite(((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(80,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[79])).
% 31.14/31.34 tff(81,plain,
% 31.14/31.34 (^[W0: $i] : rewrite(((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | ((~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))),
% 31.14/31.34 inference(bind,[status(th)],[])).
% 31.14/31.34 tff(82,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | ((~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))),
% 31.14/31.34 inference(quant_intro,[status(thm)],[81])).
% 31.14/31.34 tff(83,plain,
% 31.14/31.34 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))),
% 31.14/31.34 inference(rewrite,[status(thm)],[])).
% 31.14/31.34 tff(84,plain,
% 31.14/31.34 (^[W0: $i] : trans(monotonicity(quant_intro(proof_bind(^[W1: $i] : rewrite((aSubsetOf0(W1, szDzozmdt0(W0)) => ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))) <=> ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))), (![W1: $i] : (aSubsetOf0(W1, szDzozmdt0(W0)) => ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))) <=> ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))), ((aFunction0(W0) => ![W1: $i] : (aSubsetOf0(W1, szDzozmdt0(W0)) => ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) <=> (aFunction0(W0) => ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))))), rewrite((aFunction0(W0) => ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))), ((aFunction0(W0) => ![W1: $i] : (aSubsetOf0(W1, szDzozmdt0(W0)) => ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) <=> ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))))),
% 31.14/31.35 inference(bind,[status(th)],[])).
% 31.14/31.35 tff(85,plain,
% 31.14/31.35 (![W0: $i] : (aFunction0(W0) => ![W1: $i] : (aSubsetOf0(W1, szDzozmdt0(W0)) => ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))),
% 31.14/31.35 inference(quant_intro,[status(thm)],[84])).
% 31.14/31.35 tff(86,axiom,(![W0: $i] : (aFunction0(W0) => ![W1: $i] : (aSubsetOf0(W1, szDzozmdt0(W0)) => ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mDefSImg')).
% 31.14/31.35 tff(87,plain,
% 31.14/31.35 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))),
% 31.14/31.35 inference(modus_ponens,[status(thm)],[86, 85])).
% 31.14/31.35 tff(88,plain,
% 31.14/31.35 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : ((W2 = sdtlcdtrc0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> ?[W4: $i] : (aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3)))))))),
% 31.14/31.35 inference(modus_ponens,[status(thm)],[87, 83])).
% 31.14/31.35 tff(89,plain,(
% 31.14/31.35 ![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | ((~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))))),
% 31.14/31.35 inference(skolemize,[status(sab)],[88])).
% 31.14/31.35 tff(90,plain,
% 31.14/31.35 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (((~(W2 = sdtlcdtrc0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (((~aElementOf0(W3, W2)) | (aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3))) & (aElementOf0(W3, W2) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = W3))))))) & ((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | ((aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1) & (sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0)))) & ((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : (~(aElementOf0(W4, W1) & (sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))),
% 31.14/31.35 inference(modus_ponens,[status(thm)],[89, 82])).
% 31.14/31.35 tff(91,plain,
% 31.14/31.35 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))))))),
% 31.14/31.35 inference(modus_ponens,[status(thm)],[90, 80])).
% 31.14/31.35 tff(92,plain,
% 31.14/31.35 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3)))))))))))) | (~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0))))))))))))))),
% 31.14/31.35 inference(modus_ponens,[status(thm)],[91, 78])).
% 31.14/31.35 tff(93,plain,
% 31.14/31.35 (![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))),
% 31.14/31.35 inference(modus_ponens,[status(thm)],[92, 73])).
% 31.14/31.35 tff(94,plain,
% 31.14/31.35 (((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | ((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))))))))))))))) <=> ((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | (~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))))))))))))))),
% 31.16/31.35 inference(rewrite,[status(thm)],[])).
% 31.16/31.35 tff(95,plain,
% 31.16/31.35 (((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(xe, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3)))))))))))))))) <=> ((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))))))))))))))),
% 31.16/31.35 inference(rewrite,[status(thm)],[])).
% 31.16/31.35 tff(96,plain,
% 31.16/31.35 (((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | ((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(xe, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))))))))))))))) <=> ((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | ((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))))),
% 31.16/31.35 inference(monotonicity,[status(thm)],[95])).
% 31.16/31.35 tff(97,plain,
% 31.16/31.35 (((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | ((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(xe, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))))))))))))))) <=> ((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | (~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))))))))))))))),
% 31.16/31.35 inference(transitivity,[status(thm)],[96, 94])).
% 31.16/31.35 tff(98,plain,
% 31.16/31.35 ((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | ((~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(xe, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))))))))))))))),
% 31.16/31.35 inference(quant_inst,[status(thm)],[])).
% 31.16/31.35 tff(99,plain,
% 31.16/31.35 ((~![W0: $i] : ((~aFunction0(W0)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(W0))) | ![W2: $i] : (~((~((W2 = sdtlcdtrc0(W0, W1)) | (~aSet0(W2)) | (~((~(aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_15(W2, W1, W0)) = tptp_fun_W3_14(W2, W1, W0))))))) | (~((~aElementOf0(tptp_fun_W3_14(W2, W1, W0), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = tptp_fun_W3_14(W2, W1, W0)))))))))) | (~((~(W2 = sdtlcdtrc0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, W0), W1)) | (~(sdtlpdtrp0(W0, tptp_fun_W4_13(W3, W1, W0)) = W3)))))) | (~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(W0, W4) = W3))))))))))))))))) | (~aFunction0(xe)) | ![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))),
% 31.16/31.36 inference(modus_ponens,[status(thm)],[98, 97])).
% 31.16/31.36 tff(100,plain,
% 31.16/31.36 (![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))),
% 31.16/31.36 inference(unit_resolution,[status(thm)],[99, 93, 71])).
% 31.16/31.36 tff(101,plain,
% 31.16/31.36 (((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))) <=> ((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | (~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))),
% 31.16/31.36 inference(rewrite,[status(thm)],[])).
% 31.16/31.36 tff(102,plain,
% 31.16/31.36 (((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) <=> ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))),
% 31.16/31.36 inference(rewrite,[status(thm)],[])).
% 31.16/31.36 tff(103,plain,
% 31.16/31.36 (((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))) <=> ((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))))),
% 31.16/31.36 inference(monotonicity,[status(thm)],[102])).
% 31.16/31.36 tff(104,plain,
% 31.16/31.36 (((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))) <=> ((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | (~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))),
% 31.16/31.36 inference(transitivity,[status(thm)],[103, 101])).
% 31.16/31.36 tff(105,plain,
% 31.16/31.36 ((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))))),
% 31.16/31.36 inference(quant_inst,[status(thm)],[])).
% 31.16/31.36 tff(106,plain,
% 31.16/31.36 ((~![W1: $i] : ((~aSubsetOf0(W1, szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, W1)) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, W1, xe)))))) | (~(aElementOf0(tptp_fun_W3_14(W2, W1, xe), W2) | (~((~aElementOf0(tptp_fun_W4_15(W2, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, W1, xe)) = tptp_fun_W3_14(W2, W1, xe))))))))))) | (~((~(W2 = sdtlcdtrc0(xe, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, W1)) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, W1, xe), W1)) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, W1, xe)) = W3))))))))))))))))) | (~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))),
% 31.16/31.36 inference(modus_ponens,[status(thm)],[105, 104])).
% 31.16/31.36 tff(107,plain,
% 31.16/31.36 ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xe))) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))),
% 31.16/31.36 inference(unit_resolution,[status(thm)],[106, 100])).
% 31.16/31.36 tff(108,plain,
% 31.16/31.36 (![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))),
% 31.16/31.36 inference(unit_resolution,[status(thm)],[107, 68])).
% 31.16/31.36 tff(109,plain,
% 31.16/31.36 (((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))) <=> ((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))),
% 31.16/31.37 inference(rewrite,[status(thm)],[])).
% 31.16/31.37 tff(110,plain,
% 31.16/31.37 ((~((~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))))))))) | (~((~(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))))) <=> (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))),
% 31.16/31.37 inference(rewrite,[status(thm)],[])).
% 31.16/31.37 tff(111,plain,
% 31.16/31.37 (((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))))))))) | (~((~(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) <=> ((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))),
% 31.16/31.37 inference(monotonicity,[status(thm)],[110])).
% 31.16/31.37 tff(112,plain,
% 31.16/31.37 (((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))))))))) | (~((~(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) <=> ((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))))),
% 31.16/31.37 inference(transitivity,[status(thm)],[111, 109])).
% 31.16/31.37 tff(113,plain,
% 31.16/31.37 ((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))), sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))))))))) | (~((~(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))),
% 31.16/31.37 inference(quant_inst,[status(thm)],[])).
% 31.16/31.37 tff(114,plain,
% 31.16/31.37 ((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~((~aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2)) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)))))) | (~((~((~aElementOf0(tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_15(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe))))) | aElementOf0(tptp_fun_W3_14(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), W2))))))) | (~((~(W2 = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aSet0(W2)) | (~![W3: $i] : (~((~(aElementOf0(W3, W2) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, W2)) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))))))) | (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))))),
% 31.16/31.37 inference(modus_ponens,[status(thm)],[113, 112])).
% 31.16/31.37 tff(115,plain,
% 31.16/31.37 (~((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))))),
% 31.16/31.37 inference(unit_resolution,[status(thm)],[114, 108])).
% 31.16/31.37 tff(116,plain,
% 31.16/31.37 (((~aSet0(sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3)))))))))) | ![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))),
% 31.16/31.37 inference(tautology,[status(thm)],[])).
% 31.16/31.37 tff(117,plain,
% 31.16/31.37 (![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))),
% 31.16/31.37 inference(unit_resolution,[status(thm)],[116, 115])).
% 31.16/31.37 tff(118,plain,
% 31.16/31.37 ((~![W3: $i] : (~((~(aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W3))))) | (~((~aElementOf0(W3, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W3, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W3))))))))) | (~((~(aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W0!24))))) | (~((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))))))))),
% 31.16/31.37 inference(quant_inst,[status(thm)],[])).
% 31.16/31.37 tff(119,plain,
% 31.16/31.37 (~((~(aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W0!24))))) | (~((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))))))),
% 31.16/31.37 inference(unit_resolution,[status(thm)],[118, 117])).
% 31.16/31.37 tff(120,plain,
% 31.16/31.37 (((~(aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | ![W4: $i] : ((~aElementOf0(W4, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W4) = W0!24))))) | (~((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))))))) | ((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))))),
% 31.16/31.37 inference(tautology,[status(thm)],[])).
% 31.16/31.37 tff(121,plain,
% 31.16/31.37 ((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))))),
% 31.16/31.37 inference(unit_resolution,[status(thm)],[120, 119])).
% 31.16/31.37 tff(122,plain,
% 31.16/31.37 ((xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) <=> (xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))),
% 31.16/31.37 inference(rewrite,[status(thm)],[])).
% 31.16/31.37 tff(123,axiom,(aSet0(xO) & (xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__4891')).
% 31.16/31.37 tff(124,plain,
% 31.16/31.37 (xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))),
% 31.16/31.37 inference(and_elim,[status(thm)],[123])).
% 31.16/31.37 tff(125,plain,
% 31.16/31.37 (xO = sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))),
% 31.16/31.37 inference(modus_ponens,[status(thm)],[124, 122])).
% 31.16/31.37 tff(126,plain,
% 31.16/31.37 (sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))) = xO),
% 31.16/31.37 inference(symmetry,[status(thm)],[125])).
% 31.16/31.37 tff(127,plain,
% 31.16/31.37 (aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd)))) <=> aElementOf0(W0!24, xO)),
% 31.16/31.37 inference(monotonicity,[status(thm)],[126])).
% 31.16/31.37 tff(128,plain,
% 31.16/31.37 (aElementOf0(W0!24, xO) <=> aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))),
% 31.16/31.37 inference(symmetry,[status(thm)],[127])).
% 31.16/31.37 tff(129,plain,
% 31.16/31.37 ((aElementOf0(W0!24, xO) & ![W1: $i] : (~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24)))) <=> (aElementOf0(W0!24, xO) & ![W1: $i] : (~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24))))),
% 31.16/31.37 inference(rewrite,[status(thm)],[])).
% 31.16/31.37 tff(130,plain,
% 31.16/31.37 ((~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0)))) <=> (~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0))))),
% 31.16/31.37 inference(rewrite,[status(thm)],[])).
% 31.16/31.37 tff(131,plain,
% 31.16/31.37 ((~![W0: $i] : (aElementOf0(W0, xO) => ?[W1: $i] : ((aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) & (sdtlpdtrp0(xe, W1) = W0)))) <=> (~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0))))),
% 31.16/31.37 inference(rewrite,[status(thm)],[])).
% 31.16/31.37 tff(132,axiom,(~![W0: $i] : (aElementOf0(W0, xO) => ?[W1: $i] : ((aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) & (sdtlpdtrp0(xe, W1) = W0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__')).
% 31.16/31.37 tff(133,plain,
% 31.16/31.37 (~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0)))),
% 31.16/31.37 inference(modus_ponens,[status(thm)],[132, 131])).
% 31.16/31.37 tff(134,plain,
% 31.16/31.37 (~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0)))),
% 31.16/31.37 inference(modus_ponens,[status(thm)],[133, 130])).
% 31.16/31.37 tff(135,plain,
% 31.16/31.37 (~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0)))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[134, 130])).
% 31.16/31.38 tff(136,plain,
% 31.16/31.38 (~![W0: $i] : ((~aElementOf0(W0, xO)) | ?[W1: $i] : (aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0)))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[135, 130])).
% 31.16/31.38 tff(137,plain,
% 31.16/31.38 (aElementOf0(W0!24, xO) & ![W1: $i] : (~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24)))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[136, 129])).
% 31.16/31.38 tff(138,plain,
% 31.16/31.38 (aElementOf0(W0!24, xO)),
% 31.16/31.38 inference(and_elim,[status(thm)],[137])).
% 31.16/31.38 tff(139,plain,
% 31.16/31.38 (aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[138, 128])).
% 31.16/31.38 tff(140,plain,
% 31.16/31.38 ((~((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))))) | (~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))))),
% 31.16/31.38 inference(tautology,[status(thm)],[])).
% 31.16/31.38 tff(141,plain,
% 31.16/31.38 ((~((~aElementOf0(W0!24, sdtlcdtrc0(xe, sdtlbdtrb0(xd, szDzizrdt0(xd))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))))) | (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))))),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[140, 139])).
% 31.16/31.38 tff(142,plain,
% 31.16/31.38 (~((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[141, 121])).
% 31.16/31.38 tff(143,plain,
% 31.16/31.38 (((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))) | (sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)),
% 31.16/31.38 inference(tautology,[status(thm)],[])).
% 31.16/31.38 tff(144,plain,
% 31.16/31.38 (sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[143, 142])).
% 31.16/31.38 tff(145,plain,
% 31.16/31.38 (((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))) | aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))),
% 31.16/31.38 inference(tautology,[status(thm)],[])).
% 31.16/31.38 tff(146,plain,
% 31.16/31.38 (aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[145, 142])).
% 31.16/31.38 tff(147,plain,
% 31.16/31.38 (^[W1: $i] : refl(((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(148,plain,
% 31.16/31.38 (![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24))) <=> ![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[147])).
% 31.16/31.38 tff(149,plain,
% 31.16/31.38 (^[W1: $i] : trans(monotonicity(rewrite((aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24)) <=> (~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24))))), ((~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24))) <=> (~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24))))))), rewrite((~(~((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))), ((~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(150,plain,
% 31.16/31.38 (![W1: $i] : (~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24))) <=> ![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[149])).
% 31.16/31.38 tff(151,plain,
% 31.16/31.38 (![W1: $i] : (~(aElementOf0(W1, szNzAzT0) & aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd))) & (sdtlpdtrp0(xe, W1) = W0!24)))),
% 31.16/31.38 inference(and_elim,[status(thm)],[137])).
% 31.16/31.38 tff(152,plain,
% 31.16/31.38 (![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[151, 150])).
% 31.16/31.38 tff(153,plain,
% 31.16/31.38 (![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[152, 148])).
% 31.16/31.38 tff(154,plain,
% 31.16/31.38 (((~![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))) | ((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0)) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))) <=> ((~![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0)) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))),
% 31.16/31.38 inference(rewrite,[status(thm)],[])).
% 31.16/31.38 tff(155,plain,
% 31.16/31.38 ((~![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))) | ((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0)) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24)))),
% 31.16/31.38 inference(quant_inst,[status(thm)],[])).
% 31.16/31.38 tff(156,plain,
% 31.16/31.38 ((~![W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aElementOf0(W1, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, W1) = W0!24)))) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0)) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~(sdtlpdtrp0(xe, tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe)) = W0!24))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[155, 154])).
% 31.16/31.38 tff(157,plain,
% 31.16/31.38 (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0)),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[156, 153, 146, 144])).
% 31.16/31.38 tff(158,plain,
% 31.16/31.38 (aSet0(szNzAzT0) <=> aSet0(szNzAzT0)),
% 31.16/31.38 inference(rewrite,[status(thm)],[])).
% 31.16/31.38 tff(159,axiom,(aSet0(szNzAzT0) & isCountable0(szNzAzT0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mNATSet')).
% 31.16/31.38 tff(160,plain,
% 31.16/31.38 (aSet0(szNzAzT0)),
% 31.16/31.38 inference(and_elim,[status(thm)],[159])).
% 31.16/31.38 tff(161,plain,
% 31.16/31.38 (aSet0(szNzAzT0)),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[160, 158])).
% 31.16/31.38 tff(162,plain,
% 31.16/31.38 (^[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)))))))))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(163,plain,
% 31.16/31.38 (![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))))))))))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[162])).
% 31.16/31.38 tff(164,plain,
% 31.16/31.38 (^[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)))))))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(165,plain,
% 31.16/31.38 (![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))))))))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[164])).
% 31.16/31.38 tff(166,plain,
% 31.16/31.38 (^[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)))))))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(167,plain,
% 31.16/31.38 (![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))))))))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[166])).
% 31.16/31.38 tff(168,plain,
% 31.16/31.38 (![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))))))))),
% 31.16/31.38 inference(transitivity,[status(thm)],[167, 165])).
% 31.16/31.38 tff(169,plain,
% 31.16/31.38 (^[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)))))))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(170,plain,
% 31.16/31.38 (![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))))))))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[169])).
% 31.16/31.38 tff(171,plain,
% 31.16/31.38 (^[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)))))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(172,plain,
% 31.16/31.38 (![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))))))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[171])).
% 31.16/31.38 tff(173,plain,
% 31.16/31.38 (![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)))))),
% 31.16/31.38 inference(rewrite,[status(thm)],[])).
% 31.16/31.38 tff(174,plain,
% 31.16/31.38 (^[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)))))))),
% 31.16/31.38 inference(bind,[status(th)],[])).
% 31.16/31.38 tff(175,plain,
% 31.16/31.38 (![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)))))),
% 31.16/31.38 inference(quant_intro,[status(thm)],[174])).
% 31.16/31.38 tff(176,axiom,(![W0: $i] : (aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mDefSub')).
% 31.16/31.38 tff(177,plain,
% 31.16/31.38 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[176, 175])).
% 31.16/31.38 tff(178,plain,
% 31.16/31.38 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[177, 173])).
% 31.16/31.38 tff(179,plain,(
% 31.16/31.38 ![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)))))))),
% 31.16/31.38 inference(skolemize,[status(sab)],[178])).
% 31.16/31.38 tff(180,plain,
% 31.16/31.38 (![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))))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[179, 172])).
% 31.16/31.38 tff(181,plain,
% 31.16/31.38 (![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))))))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[180, 170])).
% 31.16/31.38 tff(182,plain,
% 31.16/31.38 (![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))))))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[181, 168])).
% 31.16/31.38 tff(183,plain,
% 31.16/31.38 (![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))))))))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[182, 163])).
% 31.16/31.38 tff(184,plain,
% 31.16/31.38 (((~![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))))))))))),
% 31.16/31.38 inference(rewrite,[status(thm)],[])).
% 31.16/31.38 tff(185,plain,
% 31.16/31.38 ((~![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))))))))))),
% 31.16/31.38 inference(quant_inst,[status(thm)],[])).
% 31.16/31.38 tff(186,plain,
% 31.16/31.38 ((~![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)))))))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[185, 184])).
% 31.16/31.38 tff(187,plain,
% 31.16/31.38 (![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)))))))))),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[186, 183, 161])).
% 31.16/31.38 tff(188,plain,
% 31.16/31.38 (((~![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)))))))))) | (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, 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)))))))))) | (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))))))),
% 31.16/31.38 inference(rewrite,[status(thm)],[])).
% 31.16/31.38 tff(189,plain,
% 31.16/31.38 ((~((~(aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))))) <=> (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))))))),
% 31.16/31.38 inference(rewrite,[status(thm)],[])).
% 31.16/31.38 tff(190,plain,
% 31.16/31.38 (((~![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(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, 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)))))))))) | (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))))))),
% 31.16/31.38 inference(monotonicity,[status(thm)],[189])).
% 31.16/31.38 tff(191,plain,
% 31.16/31.38 (((~![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(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, 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)))))))))) | (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))))))),
% 31.16/31.38 inference(transitivity,[status(thm)],[190, 188])).
% 31.16/31.38 tff(192,plain,
% 31.16/31.38 ((~![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(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))))))),
% 31.16/31.38 inference(quant_inst,[status(thm)],[])).
% 31.16/31.38 tff(193,plain,
% 31.16/31.38 ((~![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)))))))))) | (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))))))),
% 31.16/31.38 inference(modus_ponens,[status(thm)],[192, 191])).
% 31.16/31.38 tff(194,plain,
% 31.16/31.38 (~((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))))),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[193, 187])).
% 31.16/31.38 tff(195,plain,
% 31.16/31.38 (((~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) | (~((~aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W2_1(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))))) | ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))),
% 31.16/31.38 inference(tautology,[status(thm)],[])).
% 31.16/31.38 tff(196,plain,
% 31.16/31.38 ((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))),
% 31.16/31.38 inference(unit_resolution,[status(thm)],[195, 194])).
% 31.16/31.38 tff(197,plain,
% 31.16/31.38 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0) <=> aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd))),
% 31.16/31.38 inference(monotonicity,[status(thm)],[6])).
% 31.16/31.38 tff(198,plain,
% 31.16/31.38 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szDzozmdt0(xd)) <=> aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)),
% 31.24/31.45 inference(symmetry,[status(thm)],[197])).
% 31.24/31.45 tff(199,plain,
% 31.24/31.45 (aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)),
% 31.24/31.45 inference(modus_ponens,[status(thm)],[67, 198])).
% 31.24/31.45 tff(200,plain,
% 31.24/31.45 ((~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))) | (~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))),
% 31.24/31.45 inference(tautology,[status(thm)],[])).
% 31.24/31.45 tff(201,plain,
% 31.24/31.45 ((~((~aSubsetOf0(sdtlbdtrb0(xd, szDzizrdt0(xd)), szNzAzT0)) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))))) | (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))))),
% 31.24/31.45 inference(unit_resolution,[status(thm)],[200, 199])).
% 31.24/31.45 tff(202,plain,
% 31.24/31.45 (~((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))))),
% 31.24/31.45 inference(unit_resolution,[status(thm)],[201, 196])).
% 31.24/31.45 tff(203,plain,
% 31.24/31.45 (((~aSet0(sdtlbdtrb0(xd, szDzizrdt0(xd)))) | (~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0)))) | ![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))),
% 31.24/31.45 inference(tautology,[status(thm)],[])).
% 31.24/31.45 tff(204,plain,
% 31.24/31.45 (![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))),
% 31.24/31.45 inference(unit_resolution,[status(thm)],[203, 202])).
% 31.24/31.45 tff(205,plain,
% 31.24/31.45 (((~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))) | ((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0))) <=> ((~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0))),
% 31.24/31.45 inference(rewrite,[status(thm)],[])).
% 31.24/31.45 tff(206,plain,
% 31.24/31.45 ((~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))) | ((~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0))),
% 31.24/31.45 inference(quant_inst,[status(thm)],[])).
% 31.24/31.45 tff(207,plain,
% 31.24/31.45 ((~![W2: $i] : ((~aElementOf0(W2, sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(W2, szNzAzT0))) | (~aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), sdtlbdtrb0(xd, szDzizrdt0(xd)))) | aElementOf0(tptp_fun_W4_13(W0!24, sdtlbdtrb0(xd, szDzizrdt0(xd)), xe), szNzAzT0)),
% 31.24/31.45 inference(modus_ponens,[status(thm)],[206, 205])).
% 31.24/31.45 tff(208,plain,
% 31.24/31.45 ($false),
% 31.24/31.45 inference(unit_resolution,[status(thm)],[207, 204, 146, 157])).
% 31.24/31.45 % SZS output end Proof
% 31.28/31.55 % E exiting
%------------------------------------------------------------------------------