%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM633+3 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n009.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 : 600s % DateTime : Mon Jul 18 14:44:20 EDT 2022 % Result : Theorem 38.93s 39.16s % Output : Proof 38.93s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : NUM633+3 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n009.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 : 600 % 0.12/0.33 % DateTime : Wed Jul 6 13:12:52 EDT 2022 % 0.12/0.33 % CPUTime : % 38.93/39.16 % SZS status Theorem % 38.93/39.16 (* PROOF-FOUND *) % 38.93/39.16 (* BEGIN-PROOF *) % 38.93/39.16 % SZS output start Proof % 38.93/39.16 1. (aElementOf0 (szDzizrdt0 (xd)) (xT)) (-. (aElementOf0 (szDzizrdt0 (xd)) (xT))) ### Axiom % 38.93/39.16 2. (aSubsetOf0 (xO) (xS)) (-. (aSubsetOf0 (xO) (xS))) ### Axiom % 38.93/39.16 3. (-. (((aSet0 (xO)) /\ (All W0, ((aElementOf0 W0 (xO)) => (aElementOf0 W0 (xS))))) \/ (aSubsetOf0 (xO) (xS)))) (aSubsetOf0 (xO) (xS)) ### NotOr 2 % 38.93/39.16 4. (isCountable0 (xO)) (-. (isCountable0 (xO))) ### Axiom % 38.93/39.16 5. (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK))) (-. (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK)))) ### Axiom % 38.93/39.16 6. (-. (((((aSet0 T_0) /\ (All W3, ((aElementOf0 W3 T_0) => (aElementOf0 W3 (xO))))) \/ (aSubsetOf0 T_0 (xO))) /\ ((sbrdtbr0 T_0) = (xK))) \/ (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK))))) (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK))) ### NotOr 5 % 38.93/39.16 7. ((sdtlpdtrp0 (xc) T_0) != (szDzizrdt0 (xd))) ((sdtlpdtrp0 (xc) T_0) = (szDzizrdt0 (xd))) ### Axiom % 38.93/39.16 8. ((-. ((-. (Ex W1, (aElementOf0 W1 T_0))) \/ (T_0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 T_0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 T_0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 T_0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 T_0 (xS)) /\ ((All W1, ((aElementOf0 W1 T_0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 T_0 (xS)) /\ ((aElementOf0 T_0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) T_0) = (szDzizrdt0 (xd))))))))))) ((sdtlpdtrp0 (xc) T_0) != (szDzizrdt0 (xd))) ### ConjTree 7 % 38.93/39.16 9. ((((((aSet0 T_0) /\ (All W3, ((aElementOf0 W3 T_0) => (aElementOf0 W3 (xO))))) \/ (aSubsetOf0 T_0 (xO))) /\ ((sbrdtbr0 T_0) = (xK))) \/ (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 T_0))) \/ (T_0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 T_0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 T_0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 T_0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 T_0 (xS)) /\ ((All W1, ((aElementOf0 W1 T_0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 T_0 (xS)) /\ ((aElementOf0 T_0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) T_0) = (szDzizrdt0 (xd)))))))))))) ((sdtlpdtrp0 (xc) T_0) != (szDzizrdt0 (xd))) (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK))) ### Imply 6 8 % 38.93/39.16 10. (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK))) ((sdtlpdtrp0 (xc) T_0) != (szDzizrdt0 (xd))) ### All 9 % 38.93/39.16 11. (-. (((aSet0 T_0) /\ ((All W3, ((aElementOf0 W3 T_0) => (aElementOf0 W3 (xO)))) /\ ((aSubsetOf0 T_0 (xO)) /\ (((sbrdtbr0 T_0) = (xK)) /\ (aElementOf0 T_0 (slbdtsldtrb0 (xO) (xK))))))) => ((sdtlpdtrp0 (xc) T_0) = (szDzizrdt0 (xd))))) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) ### ConjTree 10 % 38.93/39.16 12. (-. (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 (xO)))) /\ ((aSubsetOf0 W2 (xO)) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 (xO) (xK))))))) => ((sdtlpdtrp0 (xc) W2) = (szDzizrdt0 (xd)))))) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) ### NotAllEx 11 % 38.93/39.16 13. (-. ((((aSet0 (xO)) /\ (All W0, ((aElementOf0 W0 (xO)) => (aElementOf0 W0 (xS))))) \/ (aSubsetOf0 (xO) (xS))) /\ ((isCountable0 (xO)) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 (xO)))) /\ ((aSubsetOf0 W2 (xO)) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 (xO) (xK))))))) => ((sdtlpdtrp0 (xc) W2) = (szDzizrdt0 (xd)))))))) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) (isCountable0 (xO)) (aSubsetOf0 (xO) (xS)) ### DisjTree 3 4 12 % 38.93/39.16 14. (-. (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = (szDzizrdt0 (xd))))))))) (aSubsetOf0 (xO) (xS)) (isCountable0 (xO)) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) ### NotExists 13 % 38.93/39.16 15. (-. ((aElementOf0 (szDzizrdt0 (xd)) (xT)) /\ (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = (szDzizrdt0 (xd)))))))))) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) (isCountable0 (xO)) (aSubsetOf0 (xO) (xS)) (aElementOf0 (szDzizrdt0 (xd)) (xT)) ### NotAnd 1 14 % 38.93/39.16 16. (-. (Ex W0, ((aElementOf0 W0 (xT)) /\ (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = W0))))))))) (aElementOf0 (szDzizrdt0 (xd)) (xT)) (aSubsetOf0 (xO) (xS)) (isCountable0 (xO)) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) ### NotExists 15 % 38.93/39.17 17. ((aElementOf0 (szDzizrdt0 (xd)) (xT)) /\ ((aSet0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) /\ (All W0, ((aElementOf0 W0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) <=> ((aElementOf0 W0 (szDzozmdt0 (xd))) /\ ((sdtlpdtrp0 (xd) W0) = (szDzizrdt0 (xd)))))))) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) (isCountable0 (xO)) (aSubsetOf0 (xO) (xS)) (-. (Ex W0, ((aElementOf0 W0 (xT)) /\ (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = W0))))))))) ### ConjTree 16 % 38.93/39.17 18. ((aSet0 (xO)) /\ (isCountable0 (xO))) (-. (Ex W0, ((aElementOf0 W0 (xT)) /\ (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = W0))))))))) (aSubsetOf0 (xO) (xS)) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) ((aElementOf0 (szDzizrdt0 (xd)) (xT)) /\ ((aSet0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) /\ (All W0, ((aElementOf0 W0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) <=> ((aElementOf0 W0 (szDzozmdt0 (xd))) /\ ((sdtlpdtrp0 (xd) W0) = (szDzizrdt0 (xd)))))))) ### And 17 % 38.93/39.17 19. ((All W0, ((aElementOf0 W0 (xO)) => (aElementOf0 W0 (xS)))) /\ (aSubsetOf0 (xO) (xS))) ((aElementOf0 (szDzizrdt0 (xd)) (xT)) /\ ((aSet0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) /\ (All W0, ((aElementOf0 W0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) <=> ((aElementOf0 W0 (szDzozmdt0 (xd))) /\ ((sdtlpdtrp0 (xd) W0) = (szDzizrdt0 (xd)))))))) (All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) (-. (Ex W0, ((aElementOf0 W0 (xT)) /\ (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = W0))))))))) ((aSet0 (xO)) /\ (isCountable0 (xO))) ### And 18 % 38.93/39.17 20. (-. ((All W0, ((((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xO))))) \/ (aSubsetOf0 W0 (xO))) /\ ((sbrdtbr0 W0) = (xK))) \/ (aElementOf0 W0 (slbdtsldtrb0 (xO) (xK)))) => ((-. ((-. (Ex W1, (aElementOf0 W1 W0))) \/ (W0 = (slcrc0)))) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (szNzAzT0)))) /\ ((aSubsetOf0 W0 (szNzAzT0)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((aElementOf0 W0 (szDzozmdt0 (xc))) /\ ((sdtlpdtrp0 (xc) W0) = (szDzizrdt0 (xd))))))))))))) => (Ex W0, ((aElementOf0 W0 (xT)) /\ (Ex W1, ((((aSet0 W1) /\ (All W2, ((aElementOf0 W2 W1) => (aElementOf0 W2 (xS))))) \/ (aSubsetOf0 W1 (xS))) /\ ((isCountable0 W1) /\ (All W2, (((aSet0 W2) /\ ((All W3, ((aElementOf0 W3 W2) => (aElementOf0 W3 W1))) /\ ((aSubsetOf0 W2 W1) /\ (((sbrdtbr0 W2) = (xK)) /\ (aElementOf0 W2 (slbdtsldtrb0 W1 (xK))))))) => ((sdtlpdtrp0 (xc) W2) = W0)))))))))) ((aSet0 (xO)) /\ (isCountable0 (xO))) ((aElementOf0 (szDzizrdt0 (xd)) (xT)) /\ ((aSet0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) /\ (All W0, ((aElementOf0 W0 (sdtlbdtrb0 (xd) (szDzizrdt0 (xd)))) <=> ((aElementOf0 W0 (szDzozmdt0 (xd))) /\ ((sdtlpdtrp0 (xd) W0) = (szDzizrdt0 (xd)))))))) ((All W0, ((aElementOf0 W0 (xO)) => (aElementOf0 W0 (xS)))) /\ (aSubsetOf0 (xO) (xS))) ### NotImply 19 % 38.93/39.17 % SZS output end Proof % 38.93/39.17 (* END-PROOF *) %------------------------------------------------------------------------------