%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM558+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 : n017.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:43:36 EDT 2022 % Result : Theorem 150.01s 150.25s % Output : Proof 150.01s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM558+3 : TPTP v8.1.0. Released v4.0.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Fri Jul 8 00:33:15 EDT 2022 % 0.13/0.34 % CPUTime : % 150.01/150.25 % SZS status Theorem % 150.01/150.25 (* PROOF-FOUND *) % 150.01/150.25 (* BEGIN-PROOF *) % 150.01/150.25 % SZS output start Proof % 150.01/150.25 1. (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (-. (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk)))) ### Axiom % 150.01/150.25 2. (-. (aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk)))) (aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk))) ### Axiom % 150.01/150.25 3. ((aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk)))) (-. (aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk)))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) ### Imply 1 2 % 150.01/150.25 4. (All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (-. (aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk)))) ### All 3 % 150.01/150.25 5. (aSet0 (xS)) (-. (aSet0 (xS))) ### Axiom % 150.01/150.25 6. (aElementOf0 (xx) (xS)) (-. (aElementOf0 (xx) (xS))) ### Axiom % 150.01/150.25 7. (-. (aElement0 (xx))) (aElement0 (xx)) ### Axiom % 150.01/150.25 8. ((aElementOf0 (xx) (xS)) => (aElement0 (xx))) (-. (aElement0 (xx))) (aElementOf0 (xx) (xS)) ### Imply 6 7 % 150.01/150.25 9. (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1))) (aElementOf0 (xx) (xS)) (-. (aElement0 (xx))) ### All 8 % 150.01/150.25 10. ((aSet0 (xS)) => (All W1, ((aElementOf0 W1 (xS)) => (aElement0 W1)))) (-. (aElement0 (xx))) (aElementOf0 (xx) (xS)) (aSet0 (xS)) ### Imply 5 9 % 150.01/150.25 11. (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (aElementOf0 (xx) (xS)) (-. (aElement0 (xx))) ### All 10 % 150.01/150.25 12. ((xx) != (xx)) ### NotEqual % 150.01/150.25 13. (-. ((aElementOf0 (xx) (sdtmndt0 (xQ) (xy))) \/ ((xx) = (xx)))) ### NotOr 12 % 150.01/150.25 14. (-. ((aElement0 (xx)) /\ ((aElementOf0 (xx) (sdtmndt0 (xQ) (xy))) \/ ((xx) = (xx))))) (aElementOf0 (xx) (xS)) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) ### NotAnd 11 13 % 150.01/150.25 15. (-. (aElementOf0 (xx) (xP))) (aElementOf0 (xx) (xP)) ### Axiom % 150.01/150.25 16. ((aElementOf0 (xx) (xP)) <=> ((aElement0 (xx)) /\ ((aElementOf0 (xx) (sdtmndt0 (xQ) (xy))) \/ ((xx) = (xx))))) (-. (aElementOf0 (xx) (xP))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (aElementOf0 (xx) (xS)) ### Equiv 14 15 % 150.01/150.25 17. (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) (aElementOf0 (xx) (xS)) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 (xx) (xP))) ### All 16 % 150.01/150.25 18. (-. (aElementOf0 (xx) (xT))) (aElementOf0 (xx) (xT)) ### Axiom % 150.01/150.25 19. ((aElementOf0 (xx) (xP)) => (aElementOf0 (xx) (xT))) (-. (aElementOf0 (xx) (xT))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (aElementOf0 (xx) (xS)) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) ### Imply 17 18 % 150.01/150.25 20. (All W1, ((aElementOf0 W1 (xP)) => (aElementOf0 W1 (xT)))) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) (aElementOf0 (xx) (xS)) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 (xx) (xT))) ### All 19 % 150.01/150.25 21. ((aSet0 (xP)) /\ ((All W1, ((aElementOf0 W1 (xP)) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 (xP) (xT)) /\ ((sbrdtbr0 (xP)) = (xk))))) (-. (aElementOf0 (xx) (xT))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (aElementOf0 (xx) (xS)) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) ### ConjTree 20 % 150.01/150.25 22. ((aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk))) => ((aSet0 (xP)) /\ ((All W1, ((aElementOf0 W1 (xP)) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 (xP) (xT)) /\ ((sbrdtbr0 (xP)) = (xk)))))) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) (aElementOf0 (xx) (xS)) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 (xx) (xT))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) ### Imply 4 21 % 150.01/150.25 23. (((aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk))) => ((aSet0 (xP)) /\ ((All W1, ((aElementOf0 W1 (xP)) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 (xP) (xT)) /\ ((sbrdtbr0 (xP)) = (xk)))))) /\ (((((aSet0 (xP)) /\ (All W1, ((aElementOf0 W1 (xP)) => (aElementOf0 W1 (xT))))) \/ (aSubsetOf0 (xP) (xT))) /\ ((sbrdtbr0 (xP)) = (xk))) => (aElementOf0 (xP) (slbdtsldtrb0 (xT) (xk))))) (All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (-. (aElementOf0 (xx) (xT))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aSet0 (xS)) (aElementOf0 (xx) (xS)) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) ### And 22 % 150.01/150.25 24. (All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 W0 (xT)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT))))) \/ (aSubsetOf0 W0 (xT))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk)))))) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) (aElementOf0 (xx) (xS)) (aSet0 (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 (xx) (xT))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) ### All 23 % 150.01/150.25 25. ((aSet0 (xS)) /\ ((aSet0 (xT)) /\ ((xk) != (sz00)))) (All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (-. (aElementOf0 (xx) (xT))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aElementOf0 (xx) (xS)) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) (All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 W0 (xT)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT))))) \/ (aSubsetOf0 W0 (xT))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk)))))) ### ConjTree 24 % 150.01/150.25 26. ((aSet0 (slbdtsldtrb0 (xS) (xk))) /\ ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS))))) \/ (aSubsetOf0 W0 (xS))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk)))))) /\ ((aSet0 (slbdtsldtrb0 (xT) (xk))) /\ ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 W0 (xT)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT))))) \/ (aSubsetOf0 W0 (xT))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk)))))) /\ ((All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) /\ ((aSubsetOf0 (slbdtsldtrb0 (xS) (xk)) (slbdtsldtrb0 (xT) (xk))) /\ (-. ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS))))) \/ (aSubsetOf0 W0 (xS))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk)))))) => ((-. (Ex W0, (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))))) \/ ((slbdtsldtrb0 (xS) (xk)) = (slcrc0))))))))))) (All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) (aElementOf0 (xx) (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 (xx) (xT))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) ((aSet0 (xS)) /\ ((aSet0 (xT)) /\ ((xk) != (sz00)))) ### ConjTree 25 % 150.01/150.26 27. ((aSet0 (sdtmndt0 (xQ) (xy))) /\ ((All W0, ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xQ)) /\ (W0 != (xy)))))) /\ ((aSet0 (xP)) /\ ((All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) /\ ((xP) = (sdtpldt0 (sdtmndt0 (xQ) (xy)) (xx))))))) ((aSet0 (xS)) /\ ((aSet0 (xT)) /\ ((xk) != (sz00)))) (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk))) (-. (aElementOf0 (xx) (xT))) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (aElementOf0 (xx) (xS)) ((aSet0 (slbdtsldtrb0 (xS) (xk))) /\ ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS))))) \/ (aSubsetOf0 W0 (xS))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk)))))) /\ ((aSet0 (slbdtsldtrb0 (xT) (xk))) /\ ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 W0 (xT)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT))))) \/ (aSubsetOf0 W0 (xT))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk)))))) /\ ((All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) /\ ((aSubsetOf0 (slbdtsldtrb0 (xS) (xk)) (slbdtsldtrb0 (xT) (xk))) /\ (-. ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS))))) \/ (aSubsetOf0 W0 (xS))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk)))))) => ((-. (Ex W0, (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))))) \/ ((slbdtsldtrb0 (xS) (xk)) = (slcrc0))))))))))) ### ConjTree 26 % 150.01/150.26 28. ((All W0, ((aElementOf0 W0 (xP)) => (aElementOf0 W0 (xS)))) /\ ((aSubsetOf0 (xP) (xS)) /\ (((sbrdtbr0 (xP)) = (xk)) /\ (aElementOf0 (xP) (slbdtsldtrb0 (xS) (xk)))))) ((aSet0 (slbdtsldtrb0 (xS) (xk))) /\ ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS))))) \/ (aSubsetOf0 W0 (xS))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk)))))) /\ ((aSet0 (slbdtsldtrb0 (xT) (xk))) /\ ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT)))) /\ ((aSubsetOf0 W0 (xT)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xT))))) \/ (aSubsetOf0 W0 (xT))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk)))))) /\ ((All W0, ((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xT) (xk))))) /\ ((aSubsetOf0 (slbdtsldtrb0 (xS) (xk)) (slbdtsldtrb0 (xT) (xk))) /\ (-. ((All W0, (((aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))) => ((aSet0 W0) /\ ((All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS)))) /\ ((aSubsetOf0 W0 (xS)) /\ ((sbrdtbr0 W0) = (xk)))))) /\ (((((aSet0 W0) /\ (All W1, ((aElementOf0 W1 W0) => (aElementOf0 W1 (xS))))) \/ (aSubsetOf0 W0 (xS))) /\ ((sbrdtbr0 W0) = (xk))) => (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk)))))) => ((-. (Ex W0, (aElementOf0 W0 (slbdtsldtrb0 (xS) (xk))))) \/ ((slbdtsldtrb0 (xS) (xk)) = (slcrc0))))))))))) (aElementOf0 (xx) (xS)) (All W0, ((aSet0 W0) => (All W1, ((aElementOf0 W1 W0) => (aElement0 W1))))) (-. (aElementOf0 (xx) (xT))) ((aSet0 (xS)) /\ ((aSet0 (xT)) /\ ((xk) != (sz00)))) ((aSet0 (sdtmndt0 (xQ) (xy))) /\ ((All W0, ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (xQ)) /\ (W0 != (xy)))))) /\ ((aSet0 (xP)) /\ ((All W0, ((aElementOf0 W0 (xP)) <=> ((aElement0 W0) /\ ((aElementOf0 W0 (sdtmndt0 (xQ) (xy))) \/ (W0 = (xx)))))) /\ ((xP) = (sdtpldt0 (sdtmndt0 (xQ) (xy)) (xx))))))) ### ConjTree 27 % 150.01/150.26 % SZS output end Proof % 150.01/150.26 (* END-PROOF *) %------------------------------------------------------------------------------