%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : NUM565+1 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n008.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:25 AM UTC 2025
% Result : Theorem 0.78s 0.98s
% Output : Proof 0.78s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUM565+1 : TPTP v9.0.0. Released v4.0.0.
% 0.07/0.13 % Command : run_E %s %d THM
% 0.13/0.35 % Computer : n008.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Fri Jun 20 01:27:03 EDT 2025
% 0.13/0.35 % CPUTime :
% 0.78/0.98 % SZS status Theorem
% 0.78/0.98 % SZS output start Proof
% 0.78/0.98 tff(sdtlpdtrp0_type, type, (
% 0.78/0.98 sdtlpdtrp0: ( $i * $i ) > $i)).
% 0.78/0.98 tff(slcrc0_type, type, (
% 0.78/0.98 slcrc0: $i)).
% 0.78/0.98 tff(xc_type, type, (
% 0.78/0.98 xc: $i)).
% 0.78/0.98 tff(tptp_fun_W0_21_type, type, (
% 0.78/0.98 tptp_fun_W0_21: $i)).
% 0.78/0.98 tff(sz00_type, type, (
% 0.78/0.98 sz00: $i)).
% 0.78/0.98 tff(sbrdtbr0_type, type, (
% 0.78/0.98 sbrdtbr0: $i > $i)).
% 0.78/0.98 tff(aSet0_type, type, (
% 0.78/0.98 aSet0: $i > $o)).
% 0.78/0.98 tff(aElementOf0_type, type, (
% 0.78/0.98 aElementOf0: ( $i * $i ) > $o)).
% 0.78/0.98 tff(xS_type, type, (
% 0.78/0.98 xS: $i)).
% 0.78/0.98 tff(aSubsetOf0_type, type, (
% 0.78/0.98 aSubsetOf0: ( $i * $i ) > $o)).
% 0.78/0.98 tff(tptp_fun_W2_1_type, type, (
% 0.78/0.98 tptp_fun_W2_1: ( $i * $i ) > $i)).
% 0.78/0.98 tff(szNzAzT0_type, type, (
% 0.78/0.98 szNzAzT0: $i)).
% 0.78/0.98 tff(isCountable0_type, type, (
% 0.78/0.98 isCountable0: $i > $o)).
% 0.78/0.98 tff(slbdtsldtrb0_type, type, (
% 0.78/0.98 slbdtsldtrb0: ( $i * $i ) > $i)).
% 0.78/0.98 tff(xK_type, type, (
% 0.78/0.98 xK: $i)).
% 0.78/0.98 tff(tptp_fun_W3_10_type, type, (
% 0.78/0.98 tptp_fun_W3_10: ( $i * $i * $i ) > $i)).
% 0.78/0.98 tff(1,plain,
% 0.78/0.98 (aSet0(szNzAzT0) <=> aSet0(szNzAzT0)),
% 0.78/0.98 inference(rewrite,[status(thm)],[])).
% 0.78/0.98 tff(2,axiom,(aSet0(szNzAzT0) & isCountable0(szNzAzT0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mNATSet')).
% 0.78/0.98 tff(3,plain,
% 0.78/0.98 (aSet0(szNzAzT0)),
% 0.78/0.98 inference(and_elim,[status(thm)],[2])).
% 0.78/0.98 tff(4,plain,
% 0.78/0.98 (aSet0(szNzAzT0)),
% 0.78/0.98 inference(modus_ponens,[status(thm)],[3, 1])).
% 0.78/0.98 tff(5,plain,
% 0.78/0.98 (^[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)))))))))))),
% 0.78/0.98 inference(bind,[status(th)],[])).
% 0.78/0.98 tff(6,plain,
% 0.78/0.98 (![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))))))))))),
% 0.78/0.98 inference(quant_intro,[status(thm)],[5])).
% 0.78/0.98 tff(7,plain,
% 0.78/0.98 (^[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)))))))))),
% 0.78/0.98 inference(bind,[status(th)],[])).
% 0.78/0.98 tff(8,plain,
% 0.78/0.98 (![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))))))))),
% 0.78/0.98 inference(quant_intro,[status(thm)],[7])).
% 0.78/0.98 tff(9,plain,
% 0.78/0.98 (^[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)))))))))),
% 0.78/0.98 inference(bind,[status(th)],[])).
% 0.78/0.98 tff(10,plain,
% 0.78/0.98 (![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))))))))),
% 0.78/0.98 inference(quant_intro,[status(thm)],[9])).
% 0.78/0.98 tff(11,plain,
% 0.78/0.98 (![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))))))))),
% 0.78/0.98 inference(transitivity,[status(thm)],[10, 8])).
% 0.78/0.98 tff(12,plain,
% 0.78/0.98 (^[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)))))))))),
% 0.78/0.98 inference(bind,[status(th)],[])).
% 0.78/0.98 tff(13,plain,
% 0.78/0.98 (![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))))))))),
% 0.78/0.98 inference(quant_intro,[status(thm)],[12])).
% 0.78/0.98 tff(14,plain,
% 0.78/0.98 (^[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)))))))),
% 0.78/0.98 inference(bind,[status(th)],[])).
% 0.78/0.98 tff(15,plain,
% 0.78/0.98 (![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))))))),
% 0.78/0.98 inference(quant_intro,[status(thm)],[14])).
% 0.78/0.98 tff(16,plain,
% 0.78/0.98 (![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)))))),
% 0.78/0.98 inference(rewrite,[status(thm)],[])).
% 0.78/0.98 tff(17,plain,
% 0.78/0.98 (^[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)))))))),
% 0.78/0.98 inference(bind,[status(th)],[])).
% 0.78/0.98 tff(18,plain,
% 0.78/0.98 (![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)))))),
% 0.78/0.98 inference(quant_intro,[status(thm)],[17])).
% 0.78/0.98 tff(19,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')).
% 0.78/0.98 tff(20,plain,
% 0.78/0.98 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 0.78/0.98 inference(modus_ponens,[status(thm)],[19, 18])).
% 0.78/0.98 tff(21,plain,
% 0.78/0.98 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 0.78/0.98 inference(modus_ponens,[status(thm)],[20, 16])).
% 0.78/0.98 tff(22,plain,(
% 0.78/0.98 ![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)))))))),
% 0.78/0.98 inference(skolemize,[status(sab)],[21])).
% 0.78/0.98 tff(23,plain,
% 0.78/0.98 (![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))))))),
% 0.78/0.98 inference(modus_ponens,[status(thm)],[22, 15])).
% 0.78/0.98 tff(24,plain,
% 0.78/0.98 (![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))))))))),
% 0.78/0.98 inference(modus_ponens,[status(thm)],[23, 13])).
% 0.78/0.98 tff(25,plain,
% 0.78/0.98 (![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))))))))),
% 0.78/0.98 inference(modus_ponens,[status(thm)],[24, 11])).
% 0.78/0.99 tff(26,plain,
% 0.78/0.99 (![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))))))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[25, 6])).
% 0.78/0.99 tff(27,plain,
% 0.78/0.99 (((~![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))))))))))),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(28,plain,
% 0.78/0.99 ((~![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))))))))))),
% 0.78/0.99 inference(quant_inst,[status(thm)],[])).
% 0.78/0.99 tff(29,plain,
% 0.78/0.99 ((~![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)))))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[28, 27])).
% 0.78/0.99 tff(30,plain,
% 0.78/0.99 (![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)))))))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[29, 26, 4])).
% 0.78/0.99 tff(31,plain,
% 0.78/0.99 ((~![W1: $i] : (~((~(aSubsetOf0(W1, szNzAzT0) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), W1)) | aElementOf0(tptp_fun_W2_1(W1, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(W1, szNzAzT0)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, szNzAzT0)))))))))) | (~((~(aSubsetOf0(xS, szNzAzT0) | (~aSet0(xS)) | (~((~aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), xS)) | aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))))))),
% 0.78/0.99 inference(quant_inst,[status(thm)],[])).
% 0.78/0.99 tff(32,plain,
% 0.78/0.99 (~((~(aSubsetOf0(xS, szNzAzT0) | (~aSet0(xS)) | (~((~aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), xS)) | aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[31, 30])).
% 0.78/0.99 tff(33,plain,
% 0.78/0.99 (((~(aSubsetOf0(xS, szNzAzT0) | (~aSet0(xS)) | (~((~aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), xS)) | aElementOf0(tptp_fun_W2_1(xS, szNzAzT0), szNzAzT0))))) | (~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))))) | ((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))),
% 0.78/0.99 inference(tautology,[status(thm)],[])).
% 0.78/0.99 tff(34,plain,
% 0.78/0.99 ((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[33, 32])).
% 0.78/0.99 tff(35,plain,
% 0.78/0.99 (aSubsetOf0(xS, szNzAzT0) <=> aSubsetOf0(xS, szNzAzT0)),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(36,axiom,(aSubsetOf0(xS, szNzAzT0) & isCountable0(xS)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__3435')).
% 0.78/0.99 tff(37,plain,
% 0.78/0.99 (aSubsetOf0(xS, szNzAzT0)),
% 0.78/0.99 inference(and_elim,[status(thm)],[36])).
% 0.78/0.99 tff(38,plain,
% 0.78/0.99 (aSubsetOf0(xS, szNzAzT0)),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[37, 35])).
% 0.78/0.99 tff(39,plain,
% 0.78/0.99 ((~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))) | (~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))),
% 0.78/0.99 inference(tautology,[status(thm)],[])).
% 0.78/0.99 tff(40,plain,
% 0.78/0.99 ((~((~aSubsetOf0(xS, szNzAzT0)) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))))) | (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[39, 38])).
% 0.78/0.99 tff(41,plain,
% 0.78/0.99 (~((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[40, 34])).
% 0.78/0.99 tff(42,plain,
% 0.78/0.99 (((~aSet0(xS)) | (~![W2: $i] : ((~aElementOf0(W2, xS)) | aElementOf0(W2, szNzAzT0)))) | aSet0(xS)),
% 0.78/0.99 inference(tautology,[status(thm)],[])).
% 0.78/0.99 tff(43,plain,
% 0.78/0.99 (aSet0(xS)),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[42, 41])).
% 0.78/0.99 tff(44,plain,
% 0.78/0.99 (((~![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(xS)) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))) <=> ((~![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(xS)) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(45,plain,
% 0.78/0.99 (((~aSet0(xS)) | ![W1: $i] : (~((~(aSubsetOf0(W1, xS) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) <=> ((~aSet0(xS)) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(46,plain,
% 0.78/0.99 (((~![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(xS)) | ![W1: $i] : (~((~(aSubsetOf0(W1, xS) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))) <=> ((~![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(xS)) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))))),
% 0.78/0.99 inference(monotonicity,[status(thm)],[45])).
% 0.78/0.99 tff(47,plain,
% 0.78/0.99 (((~![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(xS)) | ![W1: $i] : (~((~(aSubsetOf0(W1, xS) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))) <=> ((~![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(xS)) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(transitivity,[status(thm)],[46, 44])).
% 0.78/0.99 tff(48,plain,
% 0.78/0.99 ((~![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(xS)) | ![W1: $i] : (~((~(aSubsetOf0(W1, xS) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(quant_inst,[status(thm)],[])).
% 0.78/0.99 tff(49,plain,
% 0.78/0.99 ((~![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(xS)) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[48, 47])).
% 0.78/0.99 tff(50,plain,
% 0.78/0.99 (![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[49, 26, 43])).
% 0.78/0.99 tff(51,plain,
% 0.78/0.99 (((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))))) <=> ((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(52,plain,
% 0.78/0.99 ((~((~((~aSet0(W0!21)) | aSubsetOf0(W0!21, xS) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))))) <=> (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))))),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(53,plain,
% 0.78/0.99 (((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~((~aSet0(W0!21)) | aSubsetOf0(W0!21, xS) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))))) <=> ((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(monotonicity,[status(thm)],[52])).
% 0.78/0.99 tff(54,plain,
% 0.78/0.99 (((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~((~aSet0(W0!21)) | aSubsetOf0(W0!21, xS) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))))) <=> ((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))))))),
% 0.78/0.99 inference(transitivity,[status(thm)],[53, 51])).
% 0.78/0.99 tff(55,plain,
% 0.78/0.99 ((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~((~aSet0(W0!21)) | aSubsetOf0(W0!21, xS) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))))),
% 0.78/0.99 inference(quant_inst,[status(thm)],[])).
% 0.78/0.99 tff(56,plain,
% 0.78/0.99 ((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, xS) | (~((~aElementOf0(tptp_fun_W2_1(W1, xS), W1)) | aElementOf0(tptp_fun_W2_1(W1, xS), xS))))) | (~((~aSubsetOf0(W1, xS)) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, xS)))))))))) | (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[55, 54])).
% 0.78/0.99 tff(57,plain,
% 0.78/0.99 (~((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[56, 50])).
% 0.78/0.99 tff(58,plain,
% 0.78/0.99 (((~(aSubsetOf0(W0!21, xS) | (~aSet0(W0!21)) | (~((~aElementOf0(tptp_fun_W2_1(W0!21, xS), W0!21)) | aElementOf0(tptp_fun_W2_1(W0!21, xS), xS))))) | (~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))))) | ((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))),
% 0.78/0.99 inference(tautology,[status(thm)],[])).
% 0.78/0.99 tff(59,plain,
% 0.78/0.99 ((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))),
% 0.78/0.99 inference(unit_resolution,[status(thm)],[58, 57])).
% 0.78/0.99 tff(60,plain,
% 0.78/0.99 (^[W0: $i, W1: $i] : trans(monotonicity(quant_intro(proof_bind(^[W2: $i] : rewrite((~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))) <=> (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))), (![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))) <=> ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))), (((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2))))))))))))), rewrite(((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2))))))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))), (((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))))),
% 0.78/0.99 inference(bind,[status(th)],[])).
% 0.78/0.99 tff(61,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/0.99 inference(quant_intro,[status(thm)],[60])).
% 0.78/0.99 tff(62,plain,
% 0.78/0.99 (^[W0: $i, W1: $i] : refl(((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))))),
% 0.78/0.99 inference(bind,[status(th)],[])).
% 0.78/0.99 tff(63,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))),
% 0.78/0.99 inference(quant_intro,[status(thm)],[62])).
% 0.78/0.99 tff(64,plain,
% 0.78/0.99 (^[W0: $i, W1: $i] : rewrite(((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))))),
% 0.78/0.99 inference(bind,[status(th)],[])).
% 0.78/0.99 tff(65,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))),
% 0.78/0.99 inference(quant_intro,[status(thm)],[64])).
% 0.78/0.99 tff(66,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))),
% 0.78/0.99 inference(transitivity,[status(thm)],[65, 63])).
% 0.78/0.99 tff(67,plain,
% 0.78/0.99 (^[W0: $i, W1: $i] : trans(monotonicity(trans(monotonicity(rewrite((aSet0(W0) & aElementOf0(W1, szNzAzT0)) <=> (~((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0))))), ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) <=> (~(~((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0))))))), rewrite((~(~((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0))))) <=> ((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0)))), ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) <=> ((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0))))), quant_intro(proof_bind(^[W2: $i] : trans(monotonicity(rewrite(((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) <=> ((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))), trans(monotonicity(trans(monotonicity(trans(trans(monotonicity(rewrite((aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)) <=> (~((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))), ((aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> (aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (~((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))))), rewrite((aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (~((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))) <=> (~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))), ((aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> (~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))), rewrite((~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))) <=> (~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))), ((aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> (~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))), ((~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))) <=> (~(~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))), rewrite((~(~(((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) <=> (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))), ((~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))) <=> (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))), (((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))) <=> ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))), rewrite(((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))) <=> ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))), (((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))) <=> ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))), ((((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))) <=> (((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2))))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))), rewrite((((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2))))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) <=> (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))), ((((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))) <=> (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))))), (![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))) <=> ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))), (((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))))) <=> (((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))))), rewrite((((~aSet0(W0)) | (~aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))), (((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))))) <=> ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))))),
% 0.78/0.99 inference(bind,[status(th)],[])).
% 0.78/0.99 tff(68,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))))) <=> ![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))),
% 0.78/0.99 inference(quant_intro,[status(thm)],[67])).
% 0.78/0.99 tff(69,plain,
% 0.78/0.99 (^[W0: $i, W1: $i] : rewrite(((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | ((~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))))) <=> ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))))))),
% 0.78/0.99 inference(bind,[status(th)],[])).
% 0.78/0.99 tff(70,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | ((~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))))) <=> ![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))))),
% 0.78/0.99 inference(quant_intro,[status(thm)],[69])).
% 0.78/0.99 tff(71,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1)))))) <=> ![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))))),
% 0.78/0.99 inference(rewrite,[status(thm)],[])).
% 0.78/0.99 tff(72,plain,
% 0.78/0.99 (^[W0: $i, W1: $i] : rewrite(((aSet0(W0) & aElementOf0(W1, szNzAzT0)) => ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1)))))) <=> ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1)))))))),
% 0.78/0.99 inference(bind,[status(th)],[])).
% 0.78/0.99 tff(73,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((aSet0(W0) & aElementOf0(W1, szNzAzT0)) => ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1)))))) <=> ![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))))),
% 0.78/0.99 inference(quant_intro,[status(thm)],[72])).
% 0.78/0.99 tff(74,axiom,(![W0: $i, W1: $i] : ((aSet0(W0) & aElementOf0(W1, szNzAzT0)) => ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mDefSel')).
% 0.78/0.99 tff(75,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[74, 73])).
% 0.78/0.99 tff(76,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : ((W2 = slbdtsldtrb0(W0, W1)) <=> (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[75, 71])).
% 0.78/0.99 tff(77,plain,(
% 0.78/0.99 ![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | ((~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))))))))),
% 0.78/0.99 inference(skolemize,[status(sab)],[76])).
% 0.78/0.99 tff(78,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~(aSet0(W0) & aElementOf0(W1, szNzAzT0))) | ![W2: $i] : (((~(W2 = slbdtsldtrb0(W0, W1))) | (aSet0(W2) & ![W3: $i] : (aElementOf0(W3, W2) <=> (aSubsetOf0(W3, W0) & (sbrdtbr0(W3) = W1))))) & ((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (~(aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2) <=> (aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0) & (sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1)))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[77, 70])).
% 0.78/0.99 tff(79,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))),
% 0.78/0.99 inference(modus_ponens,[status(thm)],[78, 68])).
% 0.78/0.99 tff(80,plain,
% 0.78/0.99 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))) | (~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))))))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[79, 66])).
% 0.78/1.00 tff(81,plain,
% 0.78/1.00 (![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[80, 61])).
% 0.78/1.00 tff(82,plain,
% 0.78/1.00 (aElementOf0(sz00, szNzAzT0) <=> aElementOf0(sz00, szNzAzT0)),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(83,axiom,(aElementOf0(sz00, szNzAzT0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mZeroNum')).
% 0.78/1.00 tff(84,plain,
% 0.78/1.00 (aElementOf0(sz00, szNzAzT0)),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.78/1.00 tff(85,plain,
% 0.78/1.00 (((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | ((~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))) <=> ((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | (~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(86,plain,
% 0.78/1.00 (((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))) <=> ((~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(87,plain,
% 0.78/1.00 (^[W2: $i] : rewrite((~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))) <=> (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(bind,[status(th)],[])).
% 0.78/1.00 tff(88,plain,
% 0.78/1.00 (![W2: $i] : (~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))) <=> ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))),
% 0.78/1.00 inference(quant_intro,[status(thm)],[87])).
% 0.78/1.00 tff(89,plain,
% 0.78/1.00 (((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))) <=> ((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(monotonicity,[status(thm)],[88])).
% 0.78/1.00 tff(90,plain,
% 0.78/1.00 (((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))) <=> ((~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(transitivity,[status(thm)],[89, 86])).
% 0.78/1.00 tff(91,plain,
% 0.78/1.00 (((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))) <=> ((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | ((~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))))),
% 0.78/1.00 inference(monotonicity,[status(thm)],[90])).
% 0.78/1.00 tff(92,plain,
% 0.78/1.00 (((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))) <=> ((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | (~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(transitivity,[status(thm)],[91, 85])).
% 0.78/1.00 tff(93,plain,
% 0.78/1.00 ((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | ((~aElementOf0(sz00, szNzAzT0)) | (~aSet0(xS)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(xS, sz00)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2)))))))))))),
% 0.78/1.00 inference(quant_inst,[status(thm)],[])).
% 0.78/1.00 tff(94,plain,
% 0.78/1.00 ((~![W0: $i, W1: $i] : ((~aElementOf0(W1, szNzAzT0)) | (~aSet0(W0)) | ![W2: $i] : (~((~((W2 = slbdtsldtrb0(W0, W1)) | (~aSet0(W2)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, W1, W0), W0)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, W1, W0)) = W1))) <=> aElementOf0(tptp_fun_W3_10(W2, W1, W0), W2)))) | (~((~(W2 = slbdtsldtrb0(W0, W1))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, W0)) | (~(sbrdtbr0(W3) = W1))) <=> aElementOf0(W3, W2)))))))))))) | (~aSet0(xS)) | (~aElementOf0(sz00, szNzAzT0)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[93, 92])).
% 0.78/1.00 tff(95,plain,
% 0.78/1.00 ((~aSet0(xS)) | ![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[94, 84, 81])).
% 0.78/1.00 tff(96,plain,
% 0.78/1.00 (![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[95, 43])).
% 0.78/1.00 tff(97,plain,
% 0.78/1.00 ((~![W2: $i] : (~((~((~aSet0(W2)) | (W2 = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(W2, sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(W2, sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(W2, sz00, xS), W2)))) | (~((~(W2 = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(W2)) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, W2))))))))))) | (~((~((~aSet0(slbdtsldtrb0(xS, xK))) | (slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS), slbdtsldtrb0(xS, xK))))) | (~((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK)))))))))))),
% 0.78/1.00 inference(quant_inst,[status(thm)],[])).
% 0.78/1.00 tff(98,plain,
% 0.78/1.00 (~((~((~aSet0(slbdtsldtrb0(xS, xK))) | (slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS), slbdtsldtrb0(xS, xK))))) | (~((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))))))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[97, 96])).
% 0.78/1.00 tff(99,plain,
% 0.78/1.00 (((~((~aSet0(slbdtsldtrb0(xS, xK))) | (slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00)) | (((~aSubsetOf0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS), xS)) | (~(sbrdtbr0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS)) = sz00))) <=> aElementOf0(tptp_fun_W3_10(slbdtsldtrb0(xS, xK), sz00, xS), slbdtsldtrb0(xS, xK))))) | (~((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK)))))))))) | ((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))))))),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(100,plain,
% 0.78/1.00 ((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK)))))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[99, 98])).
% 0.78/1.00 tff(101,plain,
% 0.78/1.00 ((xK = sz00) <=> (xK = sz00)),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(102,axiom,(xK = sz00), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__3462')).
% 0.78/1.00 tff(103,plain,
% 0.78/1.00 (xK = sz00),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[102, 101])).
% 0.78/1.00 tff(104,plain,
% 0.78/1.00 (sz00 = xK),
% 0.78/1.00 inference(symmetry,[status(thm)],[103])).
% 0.78/1.00 tff(105,plain,
% 0.78/1.00 (slbdtsldtrb0(xS, sz00) = slbdtsldtrb0(xS, xK)),
% 0.78/1.00 inference(monotonicity,[status(thm)],[104])).
% 0.78/1.00 tff(106,plain,
% 0.78/1.00 (slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00)),
% 0.78/1.00 inference(symmetry,[status(thm)],[105])).
% 0.78/1.00 tff(107,plain,
% 0.78/1.00 ((~((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))))))) | (~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK)))))))),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(108,plain,
% 0.78/1.00 ((~((~(slbdtsldtrb0(xS, xK) = slbdtsldtrb0(xS, sz00))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))))))) | (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK)))))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[107, 106])).
% 0.78/1.00 tff(109,plain,
% 0.78/1.00 (~((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[108, 100])).
% 0.78/1.00 tff(110,plain,
% 0.78/1.00 (((~aSet0(slbdtsldtrb0(xS, xK))) | (~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK)))))) | ![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(111,plain,
% 0.78/1.00 (![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[110, 109])).
% 0.78/1.00 tff(112,plain,
% 0.78/1.00 ((~![W3: $i] : (~(((~aSubsetOf0(W3, xS)) | (~(sbrdtbr0(W3) = sz00))) <=> aElementOf0(W3, slbdtsldtrb0(xS, xK))))) | (~(((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00))) <=> aElementOf0(W0!21, slbdtsldtrb0(xS, xK))))),
% 0.78/1.00 inference(quant_inst,[status(thm)],[])).
% 0.78/1.00 tff(113,plain,
% 0.78/1.00 (~(((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00))) <=> aElementOf0(W0!21, slbdtsldtrb0(xS, xK)))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[112, 111])).
% 0.78/1.00 tff(114,plain,
% 0.78/1.00 (aElementOf0(W0!21, slbdtsldtrb0(xS, xK)) <=> aElementOf0(W0!21, slbdtsldtrb0(xS, sz00))),
% 0.78/1.00 inference(monotonicity,[status(thm)],[106])).
% 0.78/1.00 tff(115,plain,
% 0.78/1.00 (aElementOf0(W0!21, slbdtsldtrb0(xS, sz00)) <=> aElementOf0(W0!21, slbdtsldtrb0(xS, xK))),
% 0.78/1.00 inference(symmetry,[status(thm)],[114])).
% 0.78/1.00 tff(116,plain,
% 0.78/1.00 ((~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))) <=> (~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0))))),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(117,plain,
% 0.78/1.00 ((~![W0: $i] : (aElementOf0(W0, slbdtsldtrb0(xS, sz00)) => (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))) <=> (~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0))))),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(118,axiom,(~![W0: $i] : (aElementOf0(W0, slbdtsldtrb0(xS, sz00)) => (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','m__')).
% 0.78/1.00 tff(119,plain,
% 0.78/1.00 (~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[118, 117])).
% 0.78/1.00 tff(120,plain,
% 0.78/1.00 (~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[119, 116])).
% 0.78/1.00 tff(121,plain,
% 0.78/1.00 (~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[120, 116])).
% 0.78/1.00 tff(122,plain,
% 0.78/1.00 (~![W0: $i] : ((~aElementOf0(W0, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0) = sdtlpdtrp0(xc, slcrc0)))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[121, 116])).
% 0.78/1.00 tff(123,plain,(
% 0.78/1.00 ~((~aElementOf0(W0!21, slbdtsldtrb0(xS, sz00))) | (sdtlpdtrp0(xc, W0!21) = sdtlpdtrp0(xc, slcrc0)))),
% 0.78/1.00 inference(skolemize,[status(sab)],[122])).
% 0.78/1.00 tff(124,plain,
% 0.78/1.00 (aElementOf0(W0!21, slbdtsldtrb0(xS, sz00))),
% 0.78/1.00 inference(or_elim,[status(thm)],[123])).
% 0.78/1.00 tff(125,plain,
% 0.78/1.00 (aElementOf0(W0!21, slbdtsldtrb0(xS, xK))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[124, 115])).
% 0.78/1.00 tff(126,plain,
% 0.78/1.00 ((((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00))) <=> aElementOf0(W0!21, slbdtsldtrb0(xS, xK))) | (~((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00)))) | (~aElementOf0(W0!21, slbdtsldtrb0(xS, xK)))),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(127,plain,
% 0.78/1.00 (~((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00)))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[126, 125, 113])).
% 0.78/1.00 tff(128,plain,
% 0.78/1.00 (((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00))) | aSubsetOf0(W0!21, xS)),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(129,plain,
% 0.78/1.00 (aSubsetOf0(W0!21, xS)),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[128, 127])).
% 0.78/1.00 tff(130,plain,
% 0.78/1.00 ((~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))) | (~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(131,plain,
% 0.78/1.00 ((~((~aSubsetOf0(W0!21, xS)) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))))) | (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[130, 129])).
% 0.78/1.00 tff(132,plain,
% 0.78/1.00 (~((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS))))),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[131, 59])).
% 0.78/1.00 tff(133,plain,
% 0.78/1.00 (((~aSet0(W0!21)) | (~![W2: $i] : ((~aElementOf0(W2, W0!21)) | aElementOf0(W2, xS)))) | aSet0(W0!21)),
% 0.78/1.00 inference(tautology,[status(thm)],[])).
% 0.78/1.00 tff(134,plain,
% 0.78/1.00 (aSet0(W0!21)),
% 0.78/1.00 inference(unit_resolution,[status(thm)],[133, 132])).
% 0.78/1.00 tff(135,plain,
% 0.78/1.00 (^[W0: $i] : refl(((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))))),
% 0.78/1.00 inference(bind,[status(th)],[])).
% 0.78/1.00 tff(136,plain,
% 0.78/1.00 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.00 inference(quant_intro,[status(thm)],[135])).
% 0.78/1.00 tff(137,plain,
% 0.78/1.00 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.00 inference(rewrite,[status(thm)],[])).
% 0.78/1.00 tff(138,plain,
% 0.78/1.00 (^[W0: $i] : rewrite((aSet0(W0) => ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))))),
% 0.78/1.00 inference(bind,[status(th)],[])).
% 0.78/1.00 tff(139,plain,
% 0.78/1.00 (![W0: $i] : (aSet0(W0) => ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0))) <=> ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.00 inference(quant_intro,[status(thm)],[138])).
% 0.78/1.00 tff(140,axiom,(![W0: $i] : (aSet0(W0) => ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','mCardEmpty')).
% 0.78/1.00 tff(141,plain,
% 0.78/1.00 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.00 inference(modus_ponens,[status(thm)],[140, 139])).
% 0.78/1.00 tff(142,plain,
% 0.78/1.00 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.01 inference(modus_ponens,[status(thm)],[141, 137])).
% 0.78/1.01 tff(143,plain,(
% 0.78/1.01 ![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.01 inference(skolemize,[status(sab)],[142])).
% 0.78/1.01 tff(144,plain,
% 0.78/1.01 (![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))),
% 0.78/1.01 inference(modus_ponens,[status(thm)],[143, 136])).
% 0.78/1.01 tff(145,plain,
% 0.78/1.01 (((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(W0!21)) | ((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0)))) <=> ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | (~aSet0(W0!21)) | ((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0)))),
% 0.78/1.01 inference(rewrite,[status(thm)],[])).
% 0.78/1.01 tff(146,plain,
% 0.78/1.01 ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | ((~aSet0(W0!21)) | ((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0)))),
% 0.78/1.01 inference(quant_inst,[status(thm)],[])).
% 0.78/1.01 tff(147,plain,
% 0.78/1.01 ((~![W0: $i] : ((~aSet0(W0)) | ((sbrdtbr0(W0) = sz00) <=> (W0 = slcrc0)))) | (~aSet0(W0!21)) | ((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0))),
% 0.78/1.01 inference(modus_ponens,[status(thm)],[146, 145])).
% 0.78/1.01 tff(148,plain,
% 0.78/1.01 ((~aSet0(W0!21)) | ((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0))),
% 0.78/1.01 inference(unit_resolution,[status(thm)],[147, 144])).
% 0.78/1.01 tff(149,plain,
% 0.78/1.01 ((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0)),
% 0.78/1.01 inference(unit_resolution,[status(thm)],[148, 134])).
% 0.78/1.01 tff(150,plain,
% 0.78/1.01 (((~aSubsetOf0(W0!21, xS)) | (~(sbrdtbr0(W0!21) = sz00))) | (sbrdtbr0(W0!21) = sz00)),
% 0.78/1.01 inference(tautology,[status(thm)],[])).
% 0.78/1.01 tff(151,plain,
% 0.78/1.01 (sbrdtbr0(W0!21) = sz00),
% 0.78/1.01 inference(unit_resolution,[status(thm)],[150, 127])).
% 0.78/1.01 tff(152,plain,
% 0.78/1.01 ((~((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0))) | (~(sbrdtbr0(W0!21) = sz00)) | (W0!21 = slcrc0)),
% 0.78/1.01 inference(tautology,[status(thm)],[])).
% 0.78/1.01 tff(153,plain,
% 0.78/1.01 ((~((sbrdtbr0(W0!21) = sz00) <=> (W0!21 = slcrc0))) | (W0!21 = slcrc0)),
% 0.78/1.01 inference(unit_resolution,[status(thm)],[152, 151])).
% 0.78/1.01 tff(154,plain,
% 0.78/1.01 (W0!21 = slcrc0),
% 0.78/1.01 inference(unit_resolution,[status(thm)],[153, 149])).
% 0.78/1.01 tff(155,plain,
% 0.78/1.01 (sdtlpdtrp0(xc, W0!21) = sdtlpdtrp0(xc, slcrc0)),
% 0.78/1.01 inference(monotonicity,[status(thm)],[154])).
% 0.78/1.01 tff(156,plain,
% 0.78/1.01 (~(sdtlpdtrp0(xc, W0!21) = sdtlpdtrp0(xc, slcrc0))),
% 0.78/1.01 inference(or_elim,[status(thm)],[123])).
% 0.78/1.01 tff(157,plain,
% 0.78/1.01 ($false),
% 0.78/1.01 inference(unit_resolution,[status(thm)],[156, 155])).
% 0.78/1.01 % SZS output end Proof
% 0.78/1.01 % E exiting
%------------------------------------------------------------------------------