%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : LAT386+4 : TPTP v9.0.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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:14:37 AM UTC 2025
% Result : Theorem 0.20s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : LAT386+4 : TPTP v9.0.0. Released v4.0.0.
% 0.11/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n004.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu Jun 19 20:50:38 EDT 2025
% 0.12/0.33 % CPUTime :
% 0.20/0.49 % SZS status Theorem
% 0.20/0.49 % SZS output start Proof
% 0.20/0.49 tff(aElementOf0_type, type, (
% 0.20/0.49 aElementOf0: ( $i * $i ) > $o)).
% 0.20/0.49 tff(szRzazndt0_type, type, (
% 0.20/0.49 szRzazndt0: $i > $i)).
% 0.20/0.49 tff(xf_type, type, (
% 0.20/0.49 xf: $i)).
% 0.20/0.49 tff(sdtlpdtrp0_type, type, (
% 0.20/0.49 sdtlpdtrp0: ( $i * $i ) > $i)).
% 0.20/0.49 tff(tptp_fun_W0_17_type, type, (
% 0.20/0.49 tptp_fun_W0_17: $i)).
% 0.20/0.49 tff(szDzozmdt0_type, type, (
% 0.20/0.49 szDzozmdt0: $i > $i)).
% 0.20/0.49 tff(xU_type, type, (
% 0.20/0.49 xU: $i)).
% 0.20/0.49 tff(isMonotone0_type, type, (
% 0.20/0.49 isMonotone0: $i > $o)).
% 0.20/0.49 tff(sdtlseqdt0_type, type, (
% 0.20/0.49 sdtlseqdt0: ( $i * $i ) > $o)).
% 0.20/0.49 tff(aFunction0_type, type, (
% 0.20/0.49 aFunction0: $i > $o)).
% 0.20/0.49 tff(aCompleteLattice0_type, type, (
% 0.20/0.49 aCompleteLattice0: $i > $o)).
% 0.20/0.49 tff(aSupremumOfIn0_type, type, (
% 0.20/0.49 aSupremumOfIn0: ( $i * $i * $i ) > $o)).
% 0.20/0.49 tff(aUpperBoundOfIn0_type, type, (
% 0.20/0.49 aUpperBoundOfIn0: ( $i * $i * $i ) > $o)).
% 0.20/0.49 tff(aInfimumOfIn0_type, type, (
% 0.20/0.49 aInfimumOfIn0: ( $i * $i * $i ) > $o)).
% 0.20/0.49 tff(aLowerBoundOfIn0_type, type, (
% 0.20/0.49 aLowerBoundOfIn0: ( $i * $i * $i ) > $o)).
% 0.20/0.49 tff(aSubsetOf0_type, type, (
% 0.20/0.49 aSubsetOf0: ( $i * $i ) > $o)).
% 0.20/0.49 tff(aSet0_type, type, (
% 0.20/0.49 aSet0: $i > $o)).
% 0.20/0.49 tff(isOn0_type, type, (
% 0.20/0.49 isOn0: ( $i * $i ) > $o)).
% 0.20/0.49 tff(xT_type, type, (
% 0.20/0.49 xT: $i)).
% 0.20/0.49 tff(xP_type, type, (
% 0.20/0.49 xP: $i)).
% 0.20/0.49 tff(tptp_fun_W1_15_type, type, (
% 0.20/0.49 tptp_fun_W1_15: $i > $i)).
% 0.20/0.49 tff(cS1241_type, type, (
% 0.20/0.49 cS1241: ( $i * $i * $i ) > $i)).
% 0.20/0.49 tff(xp_type, type, (
% 0.20/0.49 xp: $i)).
% 0.20/0.49 tff(tptp_fun_W0_18_type, type, (
% 0.20/0.49 tptp_fun_W0_18: $i)).
% 0.20/0.49 tff(tptp_fun_W1_16_type, type, (
% 0.20/0.49 tptp_fun_W1_16: $i > $i)).
% 0.20/0.49 tff(aFixedPointOf0_type, type, (
% 0.20/0.49 aFixedPointOf0: ( $i * $i ) > $o)).
% 0.20/0.49 tff(xS_type, type, (
% 0.20/0.49 xS: $i)).
% 0.20/0.49 tff(cS1142_type, type, (
% 0.20/0.49 cS1142: $i > $i)).
% 0.20/0.49 tff(tptp_fun_W2_1_type, type, (
% 0.20/0.49 tptp_fun_W2_1: ( $i * $i ) > $i)).
% 0.20/0.49 tff(tptp_fun_W2_9_type, type, (
% 0.20/0.49 tptp_fun_W2_9: $i > $i)).
% 0.20/0.49 tff(tptp_fun_W1_10_type, type, (
% 0.20/0.49 tptp_fun_W1_10: $i > $i)).
% 0.20/0.49 tff(aElement0_type, type, (
% 0.20/0.49 aElement0: $i > $o)).
% 0.20/0.49 tff(1,plain,
% 0.20/0.49 ((szRzazndt0(xf) = xU) <=> (szRzazndt0(xf) = xU)),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(2,axiom,((((((((aSet0(xU) & ![W0: $i] : (((aSet0(W0) & ![W1: $i] : (aElementOf0(W1, W0) => aElementOf0(W1, xU))) | aSubsetOf0(W0, xU)) => ?[W1: $i] : ((((((aElementOf0(W1, xU) & aElementOf0(W1, xU)) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W1, W2))) & aLowerBoundOfIn0(W1, W0, xU)) & ![W2: $i] : (((aElementOf0(W2, xU) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W2, W3))) | aLowerBoundOfIn0(W2, W0, xU)) => sdtlseqdt0(W2, W1))) & aInfimumOfIn0(W1, W0, xU)) & ?[W2: $i] : (((((aElementOf0(W2, xU) & aElementOf0(W2, xU)) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W3, W2))) & aUpperBoundOfIn0(W2, W0, xU)) & ![W3: $i] : (((aElementOf0(W3, xU) & ![W4: $i] : (aElementOf0(W4, W0) => sdtlseqdt0(W4, W3))) | aUpperBoundOfIn0(W3, W0, xU)) => sdtlseqdt0(W2, W3))) & aSupremumOfIn0(W2, W0, xU))))) & aCompleteLattice0(xU)) & aFunction0(xf)) & ![W0: $i, W1: $i] : ((aElementOf0(W0, szDzozmdt0(xf)) & aElementOf0(W1, szDzozmdt0(xf))) => (sdtlseqdt0(W0, W1) => sdtlseqdt0(sdtlpdtrp0(xf, W0), sdtlpdtrp0(xf, W1))))) & isMonotone0(xf)) & (szDzozmdt0(xf) = szRzazndt0(xf))) & (szRzazndt0(xf) = xU)) & isOn0(xf, xU)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1123')).
% 0.20/0.49 tff(3,plain,
% 0.20/0.49 (((((((aSet0(xU) & ![W0: $i] : (((aSet0(W0) & ![W1: $i] : (aElementOf0(W1, W0) => aElementOf0(W1, xU))) | aSubsetOf0(W0, xU)) => ?[W1: $i] : ((((((aElementOf0(W1, xU) & aElementOf0(W1, xU)) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W1, W2))) & aLowerBoundOfIn0(W1, W0, xU)) & ![W2: $i] : (((aElementOf0(W2, xU) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W2, W3))) | aLowerBoundOfIn0(W2, W0, xU)) => sdtlseqdt0(W2, W1))) & aInfimumOfIn0(W1, W0, xU)) & ?[W2: $i] : (((((aElementOf0(W2, xU) & aElementOf0(W2, xU)) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W3, W2))) & aUpperBoundOfIn0(W2, W0, xU)) & ![W3: $i] : (((aElementOf0(W3, xU) & ![W4: $i] : (aElementOf0(W4, W0) => sdtlseqdt0(W4, W3))) | aUpperBoundOfIn0(W3, W0, xU)) => sdtlseqdt0(W2, W3))) & aSupremumOfIn0(W2, W0, xU))))) & aCompleteLattice0(xU)) & aFunction0(xf)) & ![W0: $i, W1: $i] : ((aElementOf0(W0, szDzozmdt0(xf)) & aElementOf0(W1, szDzozmdt0(xf))) => (sdtlseqdt0(W0, W1) => sdtlseqdt0(sdtlpdtrp0(xf, W0), sdtlpdtrp0(xf, W1))))) & isMonotone0(xf)) & (szDzozmdt0(xf) = szRzazndt0(xf))) & (szRzazndt0(xf) = xU)),
% 0.20/0.49 inference(and_elim,[status(thm)],[2])).
% 0.20/0.49 tff(4,plain,
% 0.20/0.49 (szRzazndt0(xf) = xU),
% 0.20/0.49 inference(and_elim,[status(thm)],[3])).
% 0.20/0.49 tff(5,plain,
% 0.20/0.49 (szRzazndt0(xf) = xU),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[4, 1])).
% 0.20/0.49 tff(6,plain,
% 0.20/0.49 ((szDzozmdt0(xf) = szRzazndt0(xf)) <=> (szDzozmdt0(xf) = szRzazndt0(xf))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.49 tff(7,plain,
% 0.20/0.49 ((((((aSet0(xU) & ![W0: $i] : (((aSet0(W0) & ![W1: $i] : (aElementOf0(W1, W0) => aElementOf0(W1, xU))) | aSubsetOf0(W0, xU)) => ?[W1: $i] : ((((((aElementOf0(W1, xU) & aElementOf0(W1, xU)) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W1, W2))) & aLowerBoundOfIn0(W1, W0, xU)) & ![W2: $i] : (((aElementOf0(W2, xU) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W2, W3))) | aLowerBoundOfIn0(W2, W0, xU)) => sdtlseqdt0(W2, W1))) & aInfimumOfIn0(W1, W0, xU)) & ?[W2: $i] : (((((aElementOf0(W2, xU) & aElementOf0(W2, xU)) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W3, W2))) & aUpperBoundOfIn0(W2, W0, xU)) & ![W3: $i] : (((aElementOf0(W3, xU) & ![W4: $i] : (aElementOf0(W4, W0) => sdtlseqdt0(W4, W3))) | aUpperBoundOfIn0(W3, W0, xU)) => sdtlseqdt0(W2, W3))) & aSupremumOfIn0(W2, W0, xU))))) & aCompleteLattice0(xU)) & aFunction0(xf)) & ![W0: $i, W1: $i] : ((aElementOf0(W0, szDzozmdt0(xf)) & aElementOf0(W1, szDzozmdt0(xf))) => (sdtlseqdt0(W0, W1) => sdtlseqdt0(sdtlpdtrp0(xf, W0), sdtlpdtrp0(xf, W1))))) & isMonotone0(xf)) & (szDzozmdt0(xf) = szRzazndt0(xf))),
% 0.20/0.49 inference(and_elim,[status(thm)],[3])).
% 0.20/0.49 tff(8,plain,
% 0.20/0.49 (szDzozmdt0(xf) = szRzazndt0(xf)),
% 0.20/0.49 inference(and_elim,[status(thm)],[7])).
% 0.20/0.49 tff(9,plain,
% 0.20/0.49 (szDzozmdt0(xf) = szRzazndt0(xf)),
% 0.20/0.49 inference(modus_ponens,[status(thm)],[8, 6])).
% 0.20/0.49 tff(10,plain,
% 0.20/0.49 (szDzozmdt0(xf) = xU),
% 0.20/0.49 inference(transitivity,[status(thm)],[9, 5])).
% 0.20/0.49 tff(11,plain,
% 0.20/0.49 (aElementOf0(W0!17, szDzozmdt0(xf)) <=> aElementOf0(W0!17, xU)),
% 0.20/0.49 inference(monotonicity,[status(thm)],[10])).
% 0.20/0.49 tff(12,plain,
% 0.20/0.49 (aElementOf0(W0!17, xU) <=> aElementOf0(W0!17, szDzozmdt0(xf))),
% 0.20/0.49 inference(symmetry,[status(thm)],[11])).
% 0.20/0.49 tff(13,plain,
% 0.20/0.49 (^[W0: $i] : rewrite((~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(14,plain,
% 0.20/0.49 (![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> ![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[13])).
% 0.20/0.49 tff(15,plain,
% 0.20/0.49 (^[W0: $i] : refl((~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(16,plain,
% 0.20/0.49 (![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> ![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[15])).
% 0.20/0.49 tff(17,plain,
% 0.20/0.49 (^[W0: $i] : rewrite((~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(18,plain,
% 0.20/0.49 (![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> ![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[17])).
% 0.20/0.49 tff(19,plain,
% 0.20/0.49 (![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))) <=> ![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.49 inference(transitivity,[status(thm)],[18, 16])).
% 0.20/0.49 tff(20,plain,
% 0.20/0.49 (^[W0: $i] : trans(monotonicity(rewrite(((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) <=> ((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))), trans(monotonicity(rewrite(((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))) <=> (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))), ((aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) <=> (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))), rewrite((aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))) <=> (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))), ((aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) <=> (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))), ((((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))) <=> (((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))), rewrite((((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) <=> (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))), ((((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))) <=> (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(21,plain,
% 0.20/0.49 (![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))) <=> ![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[20])).
% 0.20/0.49 tff(22,plain,
% 0.20/0.49 (^[W0: $i] : rewrite((((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | aElementOf0(W0, xP))) <=> (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.49 inference(bind,[status(th)],[])).
% 0.20/0.49 tff(23,plain,
% 0.20/0.49 (![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | aElementOf0(W0, xP))) <=> ![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))),
% 0.20/0.49 inference(quant_intro,[status(thm)],[22])).
% 0.20/0.49 tff(24,plain,
% 0.20/0.49 (![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & ((~(aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & (aUpperBoundOfIn0(W0, xT, xU) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))) | aElementOf0(W0, xP))) <=> ![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & ((~(aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & (aUpperBoundOfIn0(W0, xT, xU) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))) | aElementOf0(W0, xP)))),
% 0.20/0.49 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(25,plain,
% 0.20/0.50 (^[W0: $i] : rewrite(((aElementOf0(W0, xP) => (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & ![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0))) & aUpperBoundOfIn0(W0, xT, xU))) & (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & (![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0)) | aUpperBoundOfIn0(W0, xT, xU))) => aElementOf0(W0, xP))) <=> (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & ((~(aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & (aUpperBoundOfIn0(W0, xT, xU) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))) | aElementOf0(W0, xP))))),
% 0.20/0.50 inference(bind,[status(th)],[])).
% 0.20/0.50 tff(26,plain,
% 0.20/0.50 (![W0: $i] : ((aElementOf0(W0, xP) => (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & ![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0))) & aUpperBoundOfIn0(W0, xT, xU))) & (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & (![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0)) | aUpperBoundOfIn0(W0, xT, xU))) => aElementOf0(W0, xP))) <=> ![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & ((~(aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & (aUpperBoundOfIn0(W0, xT, xU) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))) | aElementOf0(W0, xP)))),
% 0.20/0.50 inference(quant_intro,[status(thm)],[25])).
% 0.20/0.50 tff(27,axiom,((aSet0(xP) & ![W0: $i] : ((aElementOf0(W0, xP) => (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & ![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0))) & aUpperBoundOfIn0(W0, xT, xU))) & (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & (![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0)) | aUpperBoundOfIn0(W0, xT, xU))) => aElementOf0(W0, xP)))) & (xP = cS1241(xU, xf, xT))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1244')).
% 0.20/0.50 tff(28,plain,
% 0.20/0.50 (aSet0(xP) & ![W0: $i] : ((aElementOf0(W0, xP) => (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & ![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0))) & aUpperBoundOfIn0(W0, xT, xU))) & (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & (![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0)) | aUpperBoundOfIn0(W0, xT, xU))) => aElementOf0(W0, xP)))),
% 0.20/0.50 inference(and_elim,[status(thm)],[27])).
% 0.20/0.50 tff(29,plain,
% 0.20/0.50 (![W0: $i] : ((aElementOf0(W0, xP) => (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & ![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0))) & aUpperBoundOfIn0(W0, xT, xU))) & (((aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) & (![W1: $i] : (aElementOf0(W1, xT) => sdtlseqdt0(W1, W0)) | aUpperBoundOfIn0(W0, xT, xU))) => aElementOf0(W0, xP)))),
% 0.20/0.50 inference(and_elim,[status(thm)],[28])).
% 0.20/0.50 tff(30,plain,
% 0.20/0.50 (![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & ((~(aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & (aUpperBoundOfIn0(W0, xT, xU) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))) | aElementOf0(W0, xP)))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[29, 26])).
% 0.20/0.50 tff(31,plain,
% 0.20/0.50 (![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & ((~(aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & (aUpperBoundOfIn0(W0, xT, xU) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))) | aElementOf0(W0, xP)))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[30, 24])).
% 0.20/0.50 tff(32,plain,(
% 0.20/0.50 ![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | aElementOf0(W0, xP)))),
% 0.20/0.50 inference(skolemize,[status(sab)],[31])).
% 0.20/0.50 tff(33,plain,
% 0.20/0.50 (![W0: $i] : (((~aElementOf0(W0, xP)) | (aElementOf0(W0, xU) & sdtlseqdt0(sdtlpdtrp0(xf, W0), W0) & ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)) & aUpperBoundOfIn0(W0, xT, xU))) & (aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | ((~aUpperBoundOfIn0(W0, xT, xU)) & (~((~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[32, 23])).
% 0.20/0.50 tff(34,plain,
% 0.20/0.50 (![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[33, 21])).
% 0.20/0.50 tff(35,plain,
% 0.20/0.50 (![W0: $i] : (~((~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0))))))) | (~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0)))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[34, 19])).
% 0.20/0.50 tff(36,plain,
% 0.20/0.50 (![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[35, 14])).
% 0.20/0.50 tff(37,plain,
% 0.20/0.50 (((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU))))))))) <=> ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(38,plain,
% 0.20/0.50 ((~((~(aElementOf0(W0!17, xP) | (~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17))))) | (~((~aElementOf0(W0!17, xP)) | (~((~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))))))))) <=> (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(39,plain,
% 0.20/0.50 (((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17))))) | (~((~aElementOf0(W0!17, xP)) | (~((~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17)))))))))) <=> ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)))))))))),
% 0.20/0.50 inference(monotonicity,[status(thm)],[38])).
% 0.20/0.50 tff(40,plain,
% 0.20/0.50 (((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17))))) | (~((~aElementOf0(W0!17, xP)) | (~((~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17)))))))))) <=> ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)))))))))),
% 0.20/0.50 inference(transitivity,[status(thm)],[39, 37])).
% 0.20/0.50 tff(41,plain,
% 0.20/0.50 ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17))))) | (~((~aElementOf0(W0!17, xP)) | (~((~aElementOf0(W0!17, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17)))))))))),
% 0.20/0.50 inference(quant_inst,[status(thm)],[])).
% 0.20/0.50 tff(42,plain,
% 0.20/0.50 ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU))))))))),
% 0.20/0.50 inference(modus_ponens,[status(thm)],[41, 40])).
% 0.20/0.50 tff(43,plain,
% 0.20/0.50 (~((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)))))))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[42, 36])).
% 0.20/0.50 tff(44,plain,
% 0.20/0.50 (((~(aElementOf0(W0!17, xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)) | (~(aUpperBoundOfIn0(W0!17, xT, xU) | sdtlseqdt0(tptp_fun_W1_15(W0!17), W0!17) | (~aElementOf0(tptp_fun_W1_15(W0!17), xT)))))) | (~((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU))))))) | ((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU)))))),
% 0.20/0.50 inference(tautology,[status(thm)],[])).
% 0.20/0.50 tff(45,plain,
% 0.20/0.50 ((~aElementOf0(W0!17, xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0!17))) | (~aUpperBoundOfIn0(W0!17, xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0!17), W0!17)) | (~aElementOf0(W0!17, xU))))),
% 0.20/0.50 inference(unit_resolution,[status(thm)],[44, 43])).
% 0.20/0.50 tff(46,plain,
% 0.20/0.50 (((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))))))) <=> ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(47,plain,
% 0.20/0.50 ((~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))))))))) <=> (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))))))),
% 0.20/0.50 inference(rewrite,[status(thm)],[])).
% 0.20/0.50 tff(48,plain,
% 0.20/0.50 (((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18))))))))))) <=> ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))))))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[47])).
% 0.20/0.51 tff(49,plain,
% 0.20/0.51 (((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18))))))))))) <=> ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))))))),
% 0.20/0.51 inference(transitivity,[status(thm)],[48, 46])).
% 0.20/0.51 tff(50,plain,
% 0.20/0.51 ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18))))))))))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(51,plain,
% 0.20/0.51 ((~![W0: $i] : (~((~(aElementOf0(W0, xP) | (~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~(aUpperBoundOfIn0(W0, xT, xU) | (~aElementOf0(tptp_fun_W1_15(W0), xT)) | sdtlseqdt0(tptp_fun_W1_15(W0), W0))))) | (~((~aElementOf0(W0, xP)) | (~((~aElementOf0(W0, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, W0), W0)) | (~aUpperBoundOfIn0(W0, xT, xU)) | (~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, W0)))))))))) | (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[50, 49])).
% 0.20/0.51 tff(52,plain,
% 0.20/0.51 (~((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[51, 36])).
% 0.20/0.51 tff(53,plain,
% 0.20/0.51 (((~(aElementOf0(tptp_fun_W1_16(W0!18), xP) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)) | (~(aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU) | sdtlseqdt0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18)) | (~aElementOf0(tptp_fun_W1_15(tptp_fun_W1_16(W0!18)), xT)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))))) | ((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))),
% 0.20/0.51 inference(tautology,[status(thm)],[])).
% 0.20/0.51 tff(54,plain,
% 0.20/0.51 ((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[53, 52])).
% 0.20/0.51 tff(55,plain,
% 0.20/0.51 (^[W0: $i] : refl((~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS))))) <=> (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(56,plain,
% 0.20/0.51 (![W0: $i] : (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS))))) <=> ![W0: $i] : (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[55])).
% 0.20/0.51 tff(57,plain,
% 0.20/0.51 (^[W0: $i] : trans(monotonicity(rewrite(((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) <=> ((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))), rewrite(((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS)) <=> ((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS))), ((((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS))) <=> (((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf))))) & ((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS))))), rewrite((((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf))))) & ((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS))) <=> (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))), ((((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS))) <=> (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(58,plain,
% 0.20/0.51 (![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS))) <=> ![W0: $i] : (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[57])).
% 0.20/0.51 tff(59,plain,
% 0.20/0.51 (![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS))) <=> ![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS)))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(60,plain,
% 0.20/0.51 (^[W0: $i] : rewrite(((aElementOf0(W0, xS) => ((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) & aFixedPointOf0(W0, xf))) & (((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) | aFixedPointOf0(W0, xf)) => aElementOf0(W0, xS))) <=> (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS))))),
% 0.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(61,plain,
% 0.20/0.51 (![W0: $i] : ((aElementOf0(W0, xS) => ((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) & aFixedPointOf0(W0, xf))) & (((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) | aFixedPointOf0(W0, xf)) => aElementOf0(W0, xS))) <=> ![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS)))),
% 0.20/0.51 inference(quant_intro,[status(thm)],[60])).
% 0.20/0.51 tff(62,axiom,((aSet0(xS) & ![W0: $i] : ((aElementOf0(W0, xS) => ((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) & aFixedPointOf0(W0, xf))) & (((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) | aFixedPointOf0(W0, xf)) => aElementOf0(W0, xS)))) & (xS = cS1142(xf))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1144')).
% 0.20/0.51 tff(63,plain,
% 0.20/0.51 (aSet0(xS) & ![W0: $i] : ((aElementOf0(W0, xS) => ((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) & aFixedPointOf0(W0, xf))) & (((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) | aFixedPointOf0(W0, xf)) => aElementOf0(W0, xS)))),
% 0.20/0.51 inference(and_elim,[status(thm)],[62])).
% 0.20/0.51 tff(64,plain,
% 0.20/0.51 (![W0: $i] : ((aElementOf0(W0, xS) => ((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) & aFixedPointOf0(W0, xf))) & (((aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)) | aFixedPointOf0(W0, xf)) => aElementOf0(W0, xS)))),
% 0.20/0.51 inference(and_elim,[status(thm)],[63])).
% 0.20/0.51 tff(65,plain,
% 0.20/0.51 (![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS)))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[64, 61])).
% 0.20/0.51 tff(66,plain,
% 0.20/0.51 (![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS)))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[65, 59])).
% 0.20/0.51 tff(67,plain,(
% 0.20/0.51 ![W0: $i] : (((~aElementOf0(W0, xS)) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0) & aFixedPointOf0(W0, xf))) & ((~(aFixedPointOf0(W0, xf) | (aElementOf0(W0, szDzozmdt0(xf)) & (sdtlpdtrp0(xf, W0) = W0)))) | aElementOf0(W0, xS)))),
% 0.20/0.51 inference(skolemize,[status(sab)],[66])).
% 0.20/0.51 tff(68,plain,
% 0.20/0.51 (![W0: $i] : (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[67, 58])).
% 0.20/0.51 tff(69,plain,
% 0.20/0.51 (![W0: $i] : (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[68, 56])).
% 0.20/0.51 tff(70,plain,
% 0.20/0.51 ((~![W0: $i] : (~((~((~aElementOf0(W0, xS)) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)) | (~aFixedPointOf0(W0, xf)))))) | (~((~(aFixedPointOf0(W0, xf) | (~((~aElementOf0(W0, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0) = W0)))))) | aElementOf0(W0, xS)))))) | (~((~((~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf)))))) | (~((~(aFixedPointOf0(W0!18, xf) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)))))) | aElementOf0(W0!18, xS)))))),
% 0.20/0.51 inference(quant_inst,[status(thm)],[])).
% 0.20/0.51 tff(71,plain,
% 0.20/0.51 (~((~((~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf)))))) | (~((~(aFixedPointOf0(W0!18, xf) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)))))) | aElementOf0(W0!18, xS))))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[70, 69])).
% 0.20/0.51 tff(72,plain,
% 0.20/0.51 (((~((~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf)))))) | (~((~(aFixedPointOf0(W0!18, xf) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)))))) | aElementOf0(W0!18, xS)))) | ((~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf)))))),
% 0.20/0.51 inference(tautology,[status(thm)],[])).
% 0.20/0.51 tff(73,plain,
% 0.20/0.51 ((~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf))))),
% 0.20/0.51 inference(unit_resolution,[status(thm)],[72, 71])).
% 0.20/0.51 tff(74,plain,
% 0.20/0.51 ((xS = cS1142(xf)) <=> (xS = cS1142(xf))),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(75,plain,
% 0.20/0.51 (xS = cS1142(xf)),
% 0.20/0.51 inference(and_elim,[status(thm)],[62])).
% 0.20/0.51 tff(76,plain,
% 0.20/0.51 (xS = cS1142(xf)),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[75, 74])).
% 0.20/0.51 tff(77,plain,
% 0.20/0.51 (aElementOf0(W0!18, xS) <=> aElementOf0(W0!18, cS1142(xf))),
% 0.20/0.51 inference(monotonicity,[status(thm)],[76])).
% 0.20/0.51 tff(78,plain,
% 0.20/0.51 (aElementOf0(W0!18, cS1142(xf)) <=> aElementOf0(W0!18, xS)),
% 0.20/0.51 inference(symmetry,[status(thm)],[77])).
% 0.20/0.51 tff(79,plain,
% 0.20/0.51 (cS1142(xf) = xS),
% 0.20/0.51 inference(symmetry,[status(thm)],[76])).
% 0.20/0.51 tff(80,plain,
% 0.20/0.51 (aSet0(cS1142(xf)) <=> aSet0(xS)),
% 0.20/0.51 inference(monotonicity,[status(thm)],[79])).
% 0.20/0.51 tff(81,plain,
% 0.20/0.51 (aSet0(xS) <=> aSet0(cS1142(xf))),
% 0.20/0.51 inference(symmetry,[status(thm)],[80])).
% 0.20/0.51 tff(82,plain,
% 0.20/0.51 (aSet0(xS) <=> aSet0(xS)),
% 0.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(83,plain,
% 0.20/0.51 (aSet0(xS)),
% 0.20/0.51 inference(and_elim,[status(thm)],[63])).
% 0.20/0.51 tff(84,plain,
% 0.20/0.51 (aSet0(xS)),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[83, 82])).
% 0.20/0.51 tff(85,plain,
% 0.20/0.51 (aSet0(cS1142(xf))),
% 0.20/0.51 inference(modus_ponens,[status(thm)],[84, 81])).
% 0.20/0.51 tff(86,plain,
% 0.20/0.51 (^[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.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(87,plain,
% 0.20/0.51 (![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.20/0.51 inference(quant_intro,[status(thm)],[86])).
% 0.20/0.51 tff(88,plain,
% 0.20/0.51 (^[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.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(89,plain,
% 0.20/0.51 (![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.20/0.51 inference(quant_intro,[status(thm)],[88])).
% 0.20/0.51 tff(90,plain,
% 0.20/0.51 (^[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.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(91,plain,
% 0.20/0.51 (![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.20/0.51 inference(quant_intro,[status(thm)],[90])).
% 0.20/0.51 tff(92,plain,
% 0.20/0.51 (![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.20/0.51 inference(transitivity,[status(thm)],[91, 89])).
% 0.20/0.51 tff(93,plain,
% 0.20/0.51 (^[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.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(94,plain,
% 0.20/0.51 (![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.20/0.51 inference(quant_intro,[status(thm)],[93])).
% 0.20/0.51 tff(95,plain,
% 0.20/0.51 (^[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.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(96,plain,
% 0.20/0.51 (![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.20/0.51 inference(quant_intro,[status(thm)],[95])).
% 0.20/0.51 tff(97,plain,
% 0.20/0.51 (![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.20/0.51 inference(rewrite,[status(thm)],[])).
% 0.20/0.51 tff(98,plain,
% 0.20/0.51 (^[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.20/0.51 inference(bind,[status(th)],[])).
% 0.20/0.51 tff(99,plain,
% 0.20/0.51 (![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.20/0.51 inference(quant_intro,[status(thm)],[98])).
% 0.20/0.51 tff(100,axiom,(![W0: $i] : (aSet0(W0) => ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : (aElementOf0(W2, W1) => aElementOf0(W2, W0)))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mDefSub')).
% 0.20/0.52 tff(101,plain,
% 0.20/0.52 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[100, 99])).
% 0.20/0.52 tff(102,plain,
% 0.20/0.52 (![W0: $i] : ((~aSet0(W0)) | ![W1: $i] : (aSubsetOf0(W1, W0) <=> (aSet0(W1) & ![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, W0)))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[101, 97])).
% 0.20/0.52 tff(103,plain,(
% 0.20/0.52 ![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.20/0.52 inference(skolemize,[status(sab)],[102])).
% 0.20/0.52 tff(104,plain,
% 0.20/0.52 (![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.20/0.52 inference(modus_ponens,[status(thm)],[103, 96])).
% 0.20/0.52 tff(105,plain,
% 0.20/0.52 (![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.20/0.52 inference(modus_ponens,[status(thm)],[104, 94])).
% 0.20/0.52 tff(106,plain,
% 0.20/0.52 (![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.20/0.52 inference(modus_ponens,[status(thm)],[105, 92])).
% 0.20/0.52 tff(107,plain,
% 0.20/0.52 (![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.20/0.52 inference(modus_ponens,[status(thm)],[106, 87])).
% 0.20/0.52 tff(108,plain,
% 0.20/0.52 (((~![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(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))) <=> ((~![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(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(109,plain,
% 0.20/0.52 (((~aSet0(cS1142(xf))) | ![W1: $i] : (~((~(aSubsetOf0(W1, cS1142(xf)) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf))))))))))) <=> ((~aSet0(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(110,plain,
% 0.20/0.52 (((~![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(cS1142(xf))) | ![W1: $i] : (~((~(aSubsetOf0(W1, cS1142(xf)) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))) <=> ((~![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(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf))))))))))))),
% 0.20/0.52 inference(monotonicity,[status(thm)],[109])).
% 0.20/0.52 tff(111,plain,
% 0.20/0.52 (((~![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(cS1142(xf))) | ![W1: $i] : (~((~(aSubsetOf0(W1, cS1142(xf)) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))) <=> ((~![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(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))),
% 0.20/0.52 inference(transitivity,[status(thm)],[110, 108])).
% 0.20/0.52 tff(112,plain,
% 0.20/0.52 ((~![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(cS1142(xf))) | ![W1: $i] : (~((~(aSubsetOf0(W1, cS1142(xf)) | (~aSet0(W1)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf)))))))))))),
% 0.20/0.52 inference(quant_inst,[status(thm)],[])).
% 0.20/0.52 tff(113,plain,
% 0.20/0.52 ((~![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(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf))))))))))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[112, 111])).
% 0.20/0.52 tff(114,plain,
% 0.20/0.52 ((~aSet0(cS1142(xf))) | ![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf))))))))))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[113, 107])).
% 0.20/0.52 tff(115,plain,
% 0.20/0.52 (![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf))))))))))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[114, 85])).
% 0.20/0.52 tff(116,plain,
% 0.20/0.52 ((~![W1: $i] : (~((~((~aSet0(W1)) | aSubsetOf0(W1, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), W1)) | aElementOf0(tptp_fun_W2_1(W1, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(W1, cS1142(xf))) | (~((~aSet0(W1)) | (~![W2: $i] : ((~aElementOf0(W2, W1)) | aElementOf0(W2, cS1142(xf))))))))))) | (~((~((~aSet0(xT)) | aSubsetOf0(xT, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(xT, cS1142(xf)), xT)) | aElementOf0(tptp_fun_W2_1(xT, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf))))))))))),
% 0.20/0.52 inference(quant_inst,[status(thm)],[])).
% 0.20/0.52 tff(117,plain,
% 0.20/0.52 (~((~((~aSet0(xT)) | aSubsetOf0(xT, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(xT, cS1142(xf)), xT)) | aElementOf0(tptp_fun_W2_1(xT, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))))))))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[116, 115])).
% 0.20/0.52 tff(118,plain,
% 0.20/0.52 (((~((~aSet0(xT)) | aSubsetOf0(xT, cS1142(xf)) | (~((~aElementOf0(tptp_fun_W2_1(xT, cS1142(xf)), xT)) | aElementOf0(tptp_fun_W2_1(xT, cS1142(xf)), cS1142(xf)))))) | (~((~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf))))))))) | ((~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))))))),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(119,plain,
% 0.20/0.52 ((~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf))))))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[118, 117])).
% 0.20/0.52 tff(120,plain,
% 0.20/0.52 (aSubsetOf0(xT, cS1142(xf)) <=> aSubsetOf0(xT, xS)),
% 0.20/0.52 inference(monotonicity,[status(thm)],[79])).
% 0.20/0.52 tff(121,plain,
% 0.20/0.52 (aSubsetOf0(xT, xS) <=> aSubsetOf0(xT, cS1142(xf))),
% 0.20/0.52 inference(symmetry,[status(thm)],[120])).
% 0.20/0.52 tff(122,plain,
% 0.20/0.52 (aSubsetOf0(xT, xS) <=> aSubsetOf0(xT, xS)),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(123,axiom,((aSet0(xT) & ![W0: $i] : (aElementOf0(W0, xT) => aElementOf0(W0, xS))) & aSubsetOf0(xT, xS)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1173')).
% 0.20/0.52 tff(124,plain,
% 0.20/0.52 (aSubsetOf0(xT, xS)),
% 0.20/0.52 inference(and_elim,[status(thm)],[123])).
% 0.20/0.52 tff(125,plain,
% 0.20/0.52 (aSubsetOf0(xT, xS)),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[124, 122])).
% 0.20/0.52 tff(126,plain,
% 0.20/0.52 (aSubsetOf0(xT, cS1142(xf))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[125, 121])).
% 0.20/0.52 tff(127,plain,
% 0.20/0.52 ((~((~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))))))) | (~aSubsetOf0(xT, cS1142(xf))) | (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf))))))),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(128,plain,
% 0.20/0.52 (~((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[127, 126, 119])).
% 0.20/0.52 tff(129,plain,
% 0.20/0.52 (((~aSet0(xT)) | (~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf))))) | ![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(130,plain,
% 0.20/0.52 (![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[129, 128])).
% 0.20/0.52 tff(131,assumption,(~(aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp)))), introduced(assumption)).
% 0.20/0.52 tff(132,plain,
% 0.20/0.52 ((aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp))) | aElementOf0(W0!18, xT)),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(133,plain,
% 0.20/0.52 (aElementOf0(W0!18, xT)),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[132, 131])).
% 0.20/0.52 tff(134,plain,
% 0.20/0.52 (((~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))) | ((~aElementOf0(W0!18, xT)) | aElementOf0(W0!18, cS1142(xf)))) <=> ((~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))) | (~aElementOf0(W0!18, xT)) | aElementOf0(W0!18, cS1142(xf)))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(135,plain,
% 0.20/0.52 ((~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))) | ((~aElementOf0(W0!18, xT)) | aElementOf0(W0!18, cS1142(xf)))),
% 0.20/0.52 inference(quant_inst,[status(thm)],[])).
% 0.20/0.52 tff(136,plain,
% 0.20/0.52 ((~![W2: $i] : ((~aElementOf0(W2, xT)) | aElementOf0(W2, cS1142(xf)))) | (~aElementOf0(W0!18, xT)) | aElementOf0(W0!18, cS1142(xf))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[135, 134])).
% 0.20/0.52 tff(137,plain,
% 0.20/0.52 (aElementOf0(W0!18, cS1142(xf))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[136, 133, 130])).
% 0.20/0.52 tff(138,plain,
% 0.20/0.52 (aElementOf0(W0!18, xS)),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[137, 78])).
% 0.20/0.52 tff(139,plain,
% 0.20/0.52 ((~((~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf)))))) | (~aElementOf0(W0!18, xS)) | (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf))))),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(140,plain,
% 0.20/0.52 (~((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf)))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[139, 138, 73])).
% 0.20/0.52 tff(141,plain,
% 0.20/0.52 (((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf))) | (sdtlpdtrp0(xf, W0!18) = W0!18)),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(142,plain,
% 0.20/0.52 (sdtlpdtrp0(xf, W0!18) = W0!18),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[141, 140])).
% 0.20/0.52 tff(143,plain,
% 0.20/0.52 (sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) <=> sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp))),
% 0.20/0.52 inference(monotonicity,[status(thm)],[142])).
% 0.20/0.52 tff(144,plain,
% 0.20/0.52 (sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp)) <=> sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp))),
% 0.20/0.52 inference(symmetry,[status(thm)],[143])).
% 0.20/0.52 tff(145,plain,
% 0.20/0.52 ((~sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp))) <=> (~sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)))),
% 0.20/0.52 inference(monotonicity,[status(thm)],[144])).
% 0.20/0.52 tff(146,plain,
% 0.20/0.52 ((aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp))) | (~sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp)))),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(147,plain,
% 0.20/0.52 (~sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[146, 131])).
% 0.20/0.52 tff(148,plain,
% 0.20/0.52 (~sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[147, 145])).
% 0.20/0.52 tff(149,plain,
% 0.20/0.52 (((~aElementOf0(W0!18, szDzozmdt0(xf))) | (~(sdtlpdtrp0(xf, W0!18) = W0!18)) | (~aFixedPointOf0(W0!18, xf))) | aElementOf0(W0!18, szDzozmdt0(xf))),
% 0.20/0.52 inference(tautology,[status(thm)],[])).
% 0.20/0.52 tff(150,plain,
% 0.20/0.52 (aElementOf0(W0!18, szDzozmdt0(xf))),
% 0.20/0.52 inference(unit_resolution,[status(thm)],[149, 140])).
% 0.20/0.52 tff(151,plain,
% 0.20/0.52 (aElementOf0(xp, szDzozmdt0(xf)) <=> aElementOf0(xp, xU)),
% 0.20/0.52 inference(monotonicity,[status(thm)],[10])).
% 0.20/0.52 tff(152,plain,
% 0.20/0.52 (aElementOf0(xp, xU) <=> aElementOf0(xp, szDzozmdt0(xf))),
% 0.20/0.52 inference(symmetry,[status(thm)],[151])).
% 0.20/0.52 tff(153,plain,
% 0.20/0.52 (aElementOf0(xp, xU) <=> aElementOf0(xp, xU)),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(154,axiom,(((((aElementOf0(xp, xU) & aElementOf0(xp, xU)) & ![W0: $i] : (aElementOf0(W0, xP) => sdtlseqdt0(xp, W0))) & aLowerBoundOfIn0(xp, xP, xU)) & ![W0: $i] : (((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp))) & aInfimumOfIn0(xp, xP, xU)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__1261')).
% 0.20/0.52 tff(155,plain,
% 0.20/0.52 ((((aElementOf0(xp, xU) & aElementOf0(xp, xU)) & ![W0: $i] : (aElementOf0(W0, xP) => sdtlseqdt0(xp, W0))) & aLowerBoundOfIn0(xp, xP, xU)) & ![W0: $i] : (((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp))),
% 0.20/0.52 inference(and_elim,[status(thm)],[154])).
% 0.20/0.52 tff(156,plain,
% 0.20/0.52 (((aElementOf0(xp, xU) & aElementOf0(xp, xU)) & ![W0: $i] : (aElementOf0(W0, xP) => sdtlseqdt0(xp, W0))) & aLowerBoundOfIn0(xp, xP, xU)),
% 0.20/0.52 inference(and_elim,[status(thm)],[155])).
% 0.20/0.52 tff(157,plain,
% 0.20/0.52 ((aElementOf0(xp, xU) & aElementOf0(xp, xU)) & ![W0: $i] : (aElementOf0(W0, xP) => sdtlseqdt0(xp, W0))),
% 0.20/0.52 inference(and_elim,[status(thm)],[156])).
% 0.20/0.52 tff(158,plain,
% 0.20/0.52 (aElementOf0(xp, xU) & aElementOf0(xp, xU)),
% 0.20/0.52 inference(and_elim,[status(thm)],[157])).
% 0.20/0.52 tff(159,plain,
% 0.20/0.52 (aElementOf0(xp, xU)),
% 0.20/0.52 inference(and_elim,[status(thm)],[158])).
% 0.20/0.52 tff(160,plain,
% 0.20/0.52 (aElementOf0(xp, xU)),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[159, 153])).
% 0.20/0.52 tff(161,plain,
% 0.20/0.52 (aElementOf0(xp, szDzozmdt0(xf))),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[160, 152])).
% 0.20/0.52 tff(162,plain,
% 0.20/0.52 (aFunction0(xf) <=> aFunction0(xf)),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(163,plain,
% 0.20/0.52 (((((aSet0(xU) & ![W0: $i] : (((aSet0(W0) & ![W1: $i] : (aElementOf0(W1, W0) => aElementOf0(W1, xU))) | aSubsetOf0(W0, xU)) => ?[W1: $i] : ((((((aElementOf0(W1, xU) & aElementOf0(W1, xU)) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W1, W2))) & aLowerBoundOfIn0(W1, W0, xU)) & ![W2: $i] : (((aElementOf0(W2, xU) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W2, W3))) | aLowerBoundOfIn0(W2, W0, xU)) => sdtlseqdt0(W2, W1))) & aInfimumOfIn0(W1, W0, xU)) & ?[W2: $i] : (((((aElementOf0(W2, xU) & aElementOf0(W2, xU)) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W3, W2))) & aUpperBoundOfIn0(W2, W0, xU)) & ![W3: $i] : (((aElementOf0(W3, xU) & ![W4: $i] : (aElementOf0(W4, W0) => sdtlseqdt0(W4, W3))) | aUpperBoundOfIn0(W3, W0, xU)) => sdtlseqdt0(W2, W3))) & aSupremumOfIn0(W2, W0, xU))))) & aCompleteLattice0(xU)) & aFunction0(xf)) & ![W0: $i, W1: $i] : ((aElementOf0(W0, szDzozmdt0(xf)) & aElementOf0(W1, szDzozmdt0(xf))) => (sdtlseqdt0(W0, W1) => sdtlseqdt0(sdtlpdtrp0(xf, W0), sdtlpdtrp0(xf, W1))))) & isMonotone0(xf)),
% 0.20/0.52 inference(and_elim,[status(thm)],[7])).
% 0.20/0.52 tff(164,plain,
% 0.20/0.52 ((((aSet0(xU) & ![W0: $i] : (((aSet0(W0) & ![W1: $i] : (aElementOf0(W1, W0) => aElementOf0(W1, xU))) | aSubsetOf0(W0, xU)) => ?[W1: $i] : ((((((aElementOf0(W1, xU) & aElementOf0(W1, xU)) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W1, W2))) & aLowerBoundOfIn0(W1, W0, xU)) & ![W2: $i] : (((aElementOf0(W2, xU) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W2, W3))) | aLowerBoundOfIn0(W2, W0, xU)) => sdtlseqdt0(W2, W1))) & aInfimumOfIn0(W1, W0, xU)) & ?[W2: $i] : (((((aElementOf0(W2, xU) & aElementOf0(W2, xU)) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W3, W2))) & aUpperBoundOfIn0(W2, W0, xU)) & ![W3: $i] : (((aElementOf0(W3, xU) & ![W4: $i] : (aElementOf0(W4, W0) => sdtlseqdt0(W4, W3))) | aUpperBoundOfIn0(W3, W0, xU)) => sdtlseqdt0(W2, W3))) & aSupremumOfIn0(W2, W0, xU))))) & aCompleteLattice0(xU)) & aFunction0(xf)) & ![W0: $i, W1: $i] : ((aElementOf0(W0, szDzozmdt0(xf)) & aElementOf0(W1, szDzozmdt0(xf))) => (sdtlseqdt0(W0, W1) => sdtlseqdt0(sdtlpdtrp0(xf, W0), sdtlpdtrp0(xf, W1))))),
% 0.20/0.52 inference(and_elim,[status(thm)],[163])).
% 0.20/0.52 tff(165,plain,
% 0.20/0.52 (((aSet0(xU) & ![W0: $i] : (((aSet0(W0) & ![W1: $i] : (aElementOf0(W1, W0) => aElementOf0(W1, xU))) | aSubsetOf0(W0, xU)) => ?[W1: $i] : ((((((aElementOf0(W1, xU) & aElementOf0(W1, xU)) & ![W2: $i] : (aElementOf0(W2, W0) => sdtlseqdt0(W1, W2))) & aLowerBoundOfIn0(W1, W0, xU)) & ![W2: $i] : (((aElementOf0(W2, xU) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W2, W3))) | aLowerBoundOfIn0(W2, W0, xU)) => sdtlseqdt0(W2, W1))) & aInfimumOfIn0(W1, W0, xU)) & ?[W2: $i] : (((((aElementOf0(W2, xU) & aElementOf0(W2, xU)) & ![W3: $i] : (aElementOf0(W3, W0) => sdtlseqdt0(W3, W2))) & aUpperBoundOfIn0(W2, W0, xU)) & ![W3: $i] : (((aElementOf0(W3, xU) & ![W4: $i] : (aElementOf0(W4, W0) => sdtlseqdt0(W4, W3))) | aUpperBoundOfIn0(W3, W0, xU)) => sdtlseqdt0(W2, W3))) & aSupremumOfIn0(W2, W0, xU))))) & aCompleteLattice0(xU)) & aFunction0(xf)),
% 0.20/0.52 inference(and_elim,[status(thm)],[164])).
% 0.20/0.52 tff(166,plain,
% 0.20/0.52 (aFunction0(xf)),
% 0.20/0.52 inference(and_elim,[status(thm)],[165])).
% 0.20/0.52 tff(167,plain,
% 0.20/0.52 (aFunction0(xf)),
% 0.20/0.52 inference(modus_ponens,[status(thm)],[166, 162])).
% 0.20/0.52 tff(168,plain,
% 0.20/0.52 (^[W0: $i] : rewrite(((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0))))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(169,plain,
% 0.20/0.52 (![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[168])).
% 0.20/0.52 tff(170,plain,
% 0.20/0.52 (^[W0: $i] : refl(((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(171,plain,
% 0.20/0.52 (![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[170])).
% 0.20/0.52 tff(172,plain,
% 0.20/0.52 (^[W0: $i] : rewrite(((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(173,plain,
% 0.20/0.52 (![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[172])).
% 0.20/0.52 tff(174,plain,
% 0.20/0.52 (![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))))),
% 0.20/0.52 inference(transitivity,[status(thm)],[173, 171])).
% 0.20/0.52 tff(175,plain,
% 0.20/0.52 (^[W0: $i] : rewrite(((~aFunction0(W0)) | (((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))) & (isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~(aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0)) & aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))) <=> ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))))),
% 0.20/0.52 inference(bind,[status(th)],[])).
% 0.20/0.52 tff(176,plain,
% 0.20/0.52 (![W0: $i] : ((~aFunction0(W0)) | (((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))) & (isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~(aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0)) & aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))))),
% 0.20/0.52 inference(quant_intro,[status(thm)],[175])).
% 0.20/0.52 tff(177,plain,
% 0.20/0.52 (![W0: $i] : ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))))),
% 0.20/0.52 inference(rewrite,[status(thm)],[])).
% 0.20/0.52 tff(178,plain,
% 0.20/0.52 (^[W0: $i] : trans(monotonicity(rewrite((isMonotone0(W0) <=> ![W1: $i, W2: $i] : ((aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))) => (sdtlseqdt0(W1, W2) => sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2))))) <=> (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))))))), ((aFunction0(W0) => (isMonotone0(W0) <=> ![W1: $i, W2: $i] : ((aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))) => (sdtlseqdt0(W1, W2) => sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)))))) <=> (aFunction0(W0) => (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))))))))), rewrite((aFunction0(W0) => (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))))))) <=> ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))))), ((aFunction0(W0) => (isMonotone0(W0) <=> ![W1: $i, W2: $i] : ((aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))) => (sdtlseqdt0(W1, W2) => sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)))))) <=> ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(179,plain,
% 0.20/0.53 (![W0: $i] : (aFunction0(W0) => (isMonotone0(W0) <=> ![W1: $i, W2: $i] : ((aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))) => (sdtlseqdt0(W1, W2) => sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)))))) <=> ![W0: $i] : ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[178])).
% 0.20/0.53 tff(180,axiom,(![W0: $i] : (aFunction0(W0) => (isMonotone0(W0) <=> ![W1: $i, W2: $i] : ((aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0))) => (sdtlseqdt0(W1, W2) => sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','mDefMonot')).
% 0.20/0.53 tff(181,plain,
% 0.20/0.53 (![W0: $i] : ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[180, 179])).
% 0.20/0.53 tff(182,plain,
% 0.20/0.53 (![W0: $i] : ((~aFunction0(W0)) | (isMonotone0(W0) <=> ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[181, 177])).
% 0.20/0.53 tff(183,plain,(
% 0.20/0.53 ![W0: $i] : ((~aFunction0(W0)) | (((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~(aElementOf0(W1, szDzozmdt0(W0)) & aElementOf0(W2, szDzozmdt0(W0)))))) & (isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~(aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0)) & aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0)))))))))),
% 0.20/0.53 inference(skolemize,[status(sab)],[182])).
% 0.20/0.53 tff(184,plain,
% 0.20/0.53 (![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[183, 176])).
% 0.20/0.53 tff(185,plain,
% 0.20/0.53 (![W0: $i] : ((~aFunction0(W0)) | (~((~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))) | (~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[184, 174])).
% 0.20/0.53 tff(186,plain,
% 0.20/0.53 (![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[185, 169])).
% 0.20/0.53 tff(187,plain,
% 0.20/0.53 (((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | ((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))) <=> ((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | (~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(188,plain,
% 0.20/0.53 (((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~(sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))))))) <=> ((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(189,plain,
% 0.20/0.53 (((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | ((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~(sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))) <=> ((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | ((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))))))))),
% 0.20/0.53 inference(monotonicity,[status(thm)],[188])).
% 0.20/0.53 tff(190,plain,
% 0.20/0.53 (((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | ((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~(sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))) <=> ((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | (~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))),
% 0.20/0.53 inference(transitivity,[status(thm)],[189, 187])).
% 0.20/0.53 tff(191,plain,
% 0.20/0.53 ((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | ((~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~(sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))))),
% 0.20/0.53 inference(quant_inst,[status(thm)],[])).
% 0.20/0.53 tff(192,plain,
% 0.20/0.53 ((~![W0: $i] : ((~aFunction0(W0)) | (~((~(isMonotone0(W0) | (~(sdtlseqdt0(sdtlpdtrp0(W0, tptp_fun_W1_10(W0)), sdtlpdtrp0(W0, tptp_fun_W2_9(W0))) | (~sdtlseqdt0(tptp_fun_W1_10(W0), tptp_fun_W2_9(W0))) | (~aElementOf0(tptp_fun_W1_10(W0), szDzozmdt0(W0))) | (~aElementOf0(tptp_fun_W2_9(W0), szDzozmdt0(W0))))))) | (~((~isMonotone0(W0)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(W0, W1), sdtlpdtrp0(W0, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(W0))) | (~aElementOf0(W2, szDzozmdt0(W0)))))))))) | (~aFunction0(xf)) | (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[191, 190])).
% 0.20/0.53 tff(193,plain,
% 0.20/0.53 (~((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[192, 186, 167])).
% 0.20/0.53 tff(194,plain,
% 0.20/0.53 (((~(isMonotone0(xf) | (~((~aElementOf0(tptp_fun_W2_9(xf), szDzozmdt0(xf))) | (~aElementOf0(tptp_fun_W1_10(xf), szDzozmdt0(xf))) | (~sdtlseqdt0(tptp_fun_W1_10(xf), tptp_fun_W2_9(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_10(xf)), sdtlpdtrp0(xf, tptp_fun_W2_9(xf))))))) | (~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))))) | ((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(195,plain,
% 0.20/0.53 ((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[194, 193])).
% 0.20/0.53 tff(196,plain,
% 0.20/0.53 (isMonotone0(xf) <=> isMonotone0(xf)),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(197,plain,
% 0.20/0.53 (isMonotone0(xf)),
% 0.20/0.53 inference(and_elim,[status(thm)],[163])).
% 0.20/0.53 tff(198,plain,
% 0.20/0.53 (isMonotone0(xf)),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[197, 196])).
% 0.20/0.53 tff(199,plain,
% 0.20/0.53 ((~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))) | (~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))),
% 0.20/0.53 inference(tautology,[status(thm)],[])).
% 0.20/0.53 tff(200,plain,
% 0.20/0.53 ((~((~isMonotone0(xf)) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf)))))) | ![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[199, 198])).
% 0.20/0.53 tff(201,plain,
% 0.20/0.53 (![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[200, 195])).
% 0.20/0.53 tff(202,plain,
% 0.20/0.53 (((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | ((~aElementOf0(xp, szDzozmdt0(xf))) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)))) <=> ((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | (~aElementOf0(xp, szDzozmdt0(xf))) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(203,plain,
% 0.20/0.53 ((sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | (~aElementOf0(xp, szDzozmdt0(xf)))) <=> ((~aElementOf0(xp, szDzozmdt0(xf))) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(204,plain,
% 0.20/0.53 (((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | (sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | (~aElementOf0(xp, szDzozmdt0(xf))))) <=> ((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | ((~aElementOf0(xp, szDzozmdt0(xf))) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp))))),
% 0.20/0.53 inference(monotonicity,[status(thm)],[203])).
% 0.20/0.53 tff(205,plain,
% 0.20/0.53 (((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | (sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | (~aElementOf0(xp, szDzozmdt0(xf))))) <=> ((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | (~aElementOf0(xp, szDzozmdt0(xf))) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)))),
% 0.20/0.53 inference(transitivity,[status(thm)],[204, 202])).
% 0.20/0.53 tff(206,plain,
% 0.20/0.53 ((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | (sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp)) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | (~aElementOf0(xp, szDzozmdt0(xf))))),
% 0.20/0.53 inference(quant_inst,[status(thm)],[])).
% 0.20/0.53 tff(207,plain,
% 0.20/0.53 ((~![W1: $i, W2: $i] : (sdtlseqdt0(sdtlpdtrp0(xf, W1), sdtlpdtrp0(xf, W2)) | (~sdtlseqdt0(W1, W2)) | (~aElementOf0(W1, szDzozmdt0(xf))) | (~aElementOf0(W2, szDzozmdt0(xf))))) | (~aElementOf0(xp, szDzozmdt0(xf))) | (~aElementOf0(W0!18, szDzozmdt0(xf))) | sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[206, 205])).
% 0.20/0.53 tff(208,plain,
% 0.20/0.53 (sdtlseqdt0(sdtlpdtrp0(xf, W0!18), sdtlpdtrp0(xf, xp)) | (~sdtlseqdt0(W0!18, xp))),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[207, 201, 161, 150])).
% 0.20/0.53 tff(209,plain,
% 0.20/0.53 (~sdtlseqdt0(W0!18, xp)),
% 0.20/0.53 inference(unit_resolution,[status(thm)],[208, 148])).
% 0.20/0.53 tff(210,plain,
% 0.20/0.53 (^[W0: $i] : refl((sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU)))) <=> (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU)))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(211,plain,
% 0.20/0.53 (![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU)))) <=> ![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[210])).
% 0.20/0.53 tff(212,plain,
% 0.20/0.53 (^[W0: $i] : trans(monotonicity(rewrite((((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU))) <=> (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU)))), ((sdtlseqdt0(W0, xp) | (((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU)))) <=> (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU)))))), rewrite((sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU)))) <=> (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))), ((sdtlseqdt0(W0, xp) | (((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU)))) <=> (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(213,plain,
% 0.20/0.53 (![W0: $i] : (sdtlseqdt0(W0, xp) | (((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU)))) <=> ![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[212])).
% 0.20/0.53 tff(214,plain,
% 0.20/0.53 (^[W0: $i] : rewrite(((((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp)) <=> (sdtlseqdt0(W0, xp) | (((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU)))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(215,plain,
% 0.20/0.53 (![W0: $i] : ((((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp)) <=> ![W0: $i] : (sdtlseqdt0(W0, xp) | (((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU))))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[214])).
% 0.20/0.53 tff(216,plain,
% 0.20/0.53 (![W0: $i] : ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp)) <=> ![W0: $i] : ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))),
% 0.20/0.53 inference(rewrite,[status(thm)],[])).
% 0.20/0.53 tff(217,plain,
% 0.20/0.53 (^[W0: $i] : trans(monotonicity(rewrite(((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) <=> ((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))), ((((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp)) <=> (((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp)))), rewrite((((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp)) <=> ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))), ((((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp)) <=> ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))))),
% 0.20/0.53 inference(bind,[status(th)],[])).
% 0.20/0.53 tff(218,plain,
% 0.20/0.53 (![W0: $i] : (((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp)) <=> ![W0: $i] : ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))),
% 0.20/0.53 inference(quant_intro,[status(thm)],[217])).
% 0.20/0.53 tff(219,plain,
% 0.20/0.53 (![W0: $i] : (((aElementOf0(W0, xU) & ![W1: $i] : (aElementOf0(W1, xP) => sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU)) => sdtlseqdt0(W0, xp))),
% 0.20/0.53 inference(and_elim,[status(thm)],[155])).
% 0.20/0.53 tff(220,plain,
% 0.20/0.53 (![W0: $i] : ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[219, 218])).
% 0.20/0.53 tff(221,plain,
% 0.20/0.53 (![W0: $i] : ((~((aElementOf0(W0, xU) & ![W1: $i] : ((~aElementOf0(W1, xP)) | sdtlseqdt0(W0, W1))) | aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[220, 216])).
% 0.20/0.53 tff(222,plain,(
% 0.20/0.53 ![W0: $i] : ((((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU))) | sdtlseqdt0(W0, xp))),
% 0.20/0.53 inference(skolemize,[status(sab)],[221])).
% 0.20/0.53 tff(223,plain,
% 0.20/0.53 (![W0: $i] : (sdtlseqdt0(W0, xp) | (((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0))))) & (~aLowerBoundOfIn0(W0, xP, xU))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[222, 215])).
% 0.20/0.53 tff(224,plain,
% 0.20/0.53 (![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[223, 213])).
% 0.20/0.53 tff(225,plain,
% 0.20/0.53 (![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))),
% 0.20/0.53 inference(modus_ponens,[status(thm)],[224, 211])).
% 0.20/0.53 tff(226,plain,
% 0.20/0.53 (((~![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))) | (sdtlseqdt0(W0!18, xp) | (~((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU))))) <=> ((~![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))) | sdtlseqdt0(W0!18, xp) | (~((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU))))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(227,plain,
% 0.20/0.54 ((~![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))) | (sdtlseqdt0(W0!18, xp) | (~((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU))))),
% 0.20/0.54 inference(quant_inst,[status(thm)],[])).
% 0.20/0.54 tff(228,plain,
% 0.20/0.54 ((~![W0: $i] : (sdtlseqdt0(W0, xp) | (~((~((~aElementOf0(W0, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0), xP)) | sdtlseqdt0(W0, tptp_fun_W1_16(W0)))))) | aLowerBoundOfIn0(W0, xP, xU))))) | sdtlseqdt0(W0!18, xp) | (~((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU)))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[227, 226])).
% 0.20/0.54 tff(229,plain,
% 0.20/0.54 (sdtlseqdt0(W0!18, xp) | (~((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU)))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[228, 225])).
% 0.20/0.54 tff(230,plain,
% 0.20/0.54 (~((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[229, 209])).
% 0.20/0.54 tff(231,plain,
% 0.20/0.54 (((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | aLowerBoundOfIn0(W0!18, xP, xU)) | ((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))),
% 0.20/0.54 inference(tautology,[status(thm)],[])).
% 0.20/0.54 tff(232,plain,
% 0.20/0.54 ((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[231, 230])).
% 0.20/0.54 tff(233,plain,
% 0.20/0.54 (szRzazndt0(xf) = szDzozmdt0(xf)),
% 0.20/0.54 inference(symmetry,[status(thm)],[9])).
% 0.20/0.54 tff(234,plain,
% 0.20/0.54 (xU = szRzazndt0(xf)),
% 0.20/0.54 inference(symmetry,[status(thm)],[5])).
% 0.20/0.54 tff(235,plain,
% 0.20/0.54 (xU = szDzozmdt0(xf)),
% 0.20/0.54 inference(transitivity,[status(thm)],[234, 233])).
% 0.20/0.54 tff(236,plain,
% 0.20/0.54 (aElementOf0(W0!18, xU) <=> aElementOf0(W0!18, szDzozmdt0(xf))),
% 0.20/0.54 inference(monotonicity,[status(thm)],[235])).
% 0.20/0.54 tff(237,plain,
% 0.20/0.54 (aElementOf0(W0!18, szDzozmdt0(xf)) <=> aElementOf0(W0!18, xU)),
% 0.20/0.54 inference(symmetry,[status(thm)],[236])).
% 0.20/0.54 tff(238,plain,
% 0.20/0.54 (aElementOf0(W0!18, xU)),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[150, 237])).
% 0.20/0.54 tff(239,plain,
% 0.20/0.54 ((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | (~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))))),
% 0.20/0.54 inference(tautology,[status(thm)],[])).
% 0.20/0.54 tff(240,plain,
% 0.20/0.54 ((~((~aElementOf0(W0!18, xU)) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))))) | (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[239, 238])).
% 0.20/0.54 tff(241,plain,
% 0.20/0.54 (~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[240, 232])).
% 0.20/0.54 tff(242,plain,
% 0.20/0.54 (((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))) | aElementOf0(tptp_fun_W1_16(W0!18), xP)),
% 0.20/0.54 inference(tautology,[status(thm)],[])).
% 0.20/0.54 tff(243,plain,
% 0.20/0.54 (aElementOf0(tptp_fun_W1_16(W0!18), xP)),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[242, 241])).
% 0.20/0.54 tff(244,plain,
% 0.20/0.54 ((~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))),
% 0.20/0.54 inference(tautology,[status(thm)],[])).
% 0.20/0.54 tff(245,plain,
% 0.20/0.54 ((~((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))))) | (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[244, 243])).
% 0.20/0.54 tff(246,plain,
% 0.20/0.54 (~((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU)))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[245, 54])).
% 0.20/0.54 tff(247,plain,
% 0.20/0.54 (((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aUpperBoundOfIn0(tptp_fun_W1_16(W0!18), xT, xU)) | (~sdtlseqdt0(sdtlpdtrp0(xf, tptp_fun_W1_16(W0!18)), tptp_fun_W1_16(W0!18))) | (~aElementOf0(tptp_fun_W1_16(W0!18), xU))) | ![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))),
% 0.20/0.54 inference(tautology,[status(thm)],[])).
% 0.20/0.54 tff(248,plain,
% 0.20/0.54 (![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[247, 246])).
% 0.20/0.54 tff(249,plain,
% 0.20/0.54 (((~aElementOf0(tptp_fun_W1_16(W0!18), xP)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))) | (~sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))),
% 0.20/0.54 inference(tautology,[status(thm)],[])).
% 0.20/0.54 tff(250,plain,
% 0.20/0.54 (~sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[249, 241])).
% 0.20/0.54 tff(251,plain,
% 0.20/0.54 (((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | ((~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))) <=> ((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(252,plain,
% 0.20/0.54 ((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | ((~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18)))),
% 0.20/0.54 inference(quant_inst,[status(thm)],[])).
% 0.20/0.54 tff(253,plain,
% 0.20/0.54 ((~![W1: $i] : ((~aElementOf0(W1, xT)) | sdtlseqdt0(W1, tptp_fun_W1_16(W0!18)))) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, tptp_fun_W1_16(W0!18))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[252, 251])).
% 0.20/0.54 tff(254,plain,
% 0.20/0.54 ($false),
% 0.20/0.54 inference(unit_resolution,[status(thm)],[253, 133, 250, 248])).
% 0.20/0.54 tff(255,plain,(aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp))), inference(lemma,lemma(discharge,[]))).
% 0.20/0.54 tff(256,plain,
% 0.20/0.54 ((((~aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU)) & (~((~aElementOf0(W0!17, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0!17)))) | ((~aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU)) & (~((~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp)))))) <=> ((~(aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | (~aElementOf0(W0!17, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0!17))) | (~(aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | (~aElementOf0(W0!18, xT)) | sdtlseqdt0(W0!18, sdtlpdtrp0(xf, xp)))))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(257,plain,
% 0.20/0.54 ((aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))) <=> (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(258,plain,
% 0.20/0.54 ((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) <=> (aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0)))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(259,plain,
% 0.20/0.54 (((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))))) <=> ((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))),
% 0.20/0.54 inference(monotonicity,[status(thm)],[258, 257])).
% 0.20/0.54 tff(260,plain,
% 0.20/0.54 ((~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))) <=> (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))))))),
% 0.20/0.54 inference(monotonicity,[status(thm)],[259])).
% 0.20/0.54 tff(261,plain,
% 0.20/0.54 ((~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))) <=> (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))))))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(262,plain,
% 0.20/0.54 ((~((![W0: $i] : (aElementOf0(W0, xP) => sdtlseqdt0(sdtlpdtrp0(xf, xp), W0)) | aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU)) & (![W0: $i] : (aElementOf0(W0, xT) => sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))) | aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU)))) <=> (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))))))),
% 0.20/0.54 inference(rewrite,[status(thm)],[])).
% 0.20/0.54 tff(263,axiom,(~((![W0: $i] : (aElementOf0(W0, xP) => sdtlseqdt0(sdtlpdtrp0(xf, xp), W0)) | aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU)) & (![W0: $i] : (aElementOf0(W0, xT) => sdtlseqdt0(W0, sdtlpdtrp0(xf, xp))) | aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU)))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','m__')).
% 0.20/0.54 tff(264,plain,
% 0.20/0.54 (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[263, 262])).
% 0.20/0.54 tff(265,plain,
% 0.20/0.54 (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[264, 260])).
% 0.20/0.54 tff(266,plain,
% 0.20/0.54 (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[265, 261])).
% 0.20/0.54 tff(267,plain,
% 0.20/0.54 (~((aLowerBoundOfIn0(sdtlpdtrp0(xf, xp), xP, xU) | ![W0: $i] : ((~aElementOf0(W0, xP)) | sdtlseqdt0(sdtlpdtrp0(xf, xp), W0))) & (aUpperBoundOfIn0(sdtlpdtrp0(xf, xp), xT, xU) | ![W0: $i] : ((~aElementOf0(W0, xT)) | sdtlseqdt0(W0, sdtlpdtrp0(xf, xp)))))),
% 0.20/0.54 inference(modus_ponens,[status(thm)],[266, 260])).
% 0.20/0.54 unexpected number of arguments: (let ((a!1 (~ (not (aLowerBoundOfIn0 (sdtlpdtrp0 xf xp) xP xU))
% 0.20/0.54 (not (aLowerBoundOfIn0 (sdtlpdtrp0 xf xp) xP xU))))
% 0.20/0.54 (a!2 (forall ((W0 $i))
% 0.20/0.54 (or (not (aElementOf0 W0 xP)) (sdtlseqdt0 (sdtlpdtrp0 xf xp) W0))))
% 0.20/0.54 (a!3 (not (or (not (aElementOf0 W0!17 xP))
% 0.20/0.54 (sdtlseqdt0 (sdtlpdtrp0 xf xp) W0!17))))
% 0.20/0.54 (a!7 (~ (not (aUpperBoundOfIn0 (sdtlpdtrp0 xf xp) xT xU))
% 0.20/0.54 (not (aUpperBoundOfIn0 (sdtlpdtrp0 xf xp) xT xU))))
% 0.20/0.54 (a!8 (forall ((W0 $i))
% 0.20/0.54 (or (not (aElementOf0 W0 xT)) (sdtlseqdt0 W0 (sdtlpdtrp0 xf xp)))))
% 0.20/0.54 (a!9 (not (or (not (aElementOf0 W0!18 xT))
% 0.20/0.54 (sdtlseqdt0 W0!18 (sdtlpdtrp0 xf xp))))))
% 0.20/0.54 (let ((a!4 (not (or (aLowerBoundOfIn0 (sdtlpdtrp0 xf xp) xP xU) a!2)))
% 0.20/0.54 (a!5 (and (not (aLowerBoundOfIn0 (sdtlpdtrp0 xf xp) xP xU)) a!3))
% 0.20/0.54 (a!10 (not (or (aUpperBoundOfIn0 (sdtlpdtrp0 xf xp) xT xU) a!8)))
% 0.20/0.54 (a!11 (and (not (aUpperBoundOfIn0 (sdtlpdtrp0 xf xp) xT xU)) a!9))
% 0.20/0.54 (a!13 (and (or (aLowerBoundOfIn0 (sdtlpdtrp0 xf xp) xP xU) a!2)
% 0.20/0.54 (or (aUpperBoundOfIn0 (sdtlpdtrp0 xf xp) xT xU) a!8))))
% 0.20/0.54 (let ((a!6 (nnf-neg (refl a!1) (sk (~ (not a!2) a!3)) (~ a!4 a!5)))
% 0.20/0.54 (a!12 (nnf-neg (refl a!7) (sk (~ (not a!8) a!9)) (~ a!10 a!11))))
% 0.20/0.54 (nnf-neg a!6 a!12 (~ (not a!13) (or a!5 a!11))))))
% 0.20/0.54 Proof display could not be completed: unexpected number of arguments
% 0.20/0.55 % E exiting
%------------------------------------------------------------------------------