%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM455+6 : 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 : n015.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:42:37 EDT 2022 % Result : Theorem 244.15s 244.40s % Output : Proof 244.15s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.14 % Problem : NUM455+6 : TPTP v8.1.0. Released v4.0.0. % 0.04/0.14 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.36 % Computer : n015.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 600 % 0.15/0.36 % DateTime : Wed Jul 6 15:03:03 EDT 2022 % 0.15/0.36 % CPUTime : % 244.15/244.40 % SZS status Theorem % 244.15/244.40 (* PROOF-FOUND *) % 244.15/244.40 (* BEGIN-PROOF *) % 244.15/244.40 % SZS output start Proof % 244.15/244.40 1. (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) ### Axiom % 244.15/244.40 2. (-. (((aInteger0 (sdtpldt0 (sz10) (xp))) /\ ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (xp)) (sz10) (xp))))) \/ (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))))) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ### NotOr 1 % 244.15/244.40 3. (-. (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))))) (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10)))) ### Axiom % 244.15/244.40 4. ((((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10)))) /\ (aElementOf0 (sdtpldt0 (sz10) (xp)) (cS2200))) (-. (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))))) ### And 3 % 244.15/244.40 5. (-. (-. ((((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10)))) /\ (aElementOf0 (sdtpldt0 (sz10) (xp)) (cS2200))))) (-. (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))))) ### NotNot 4 % 244.15/244.40 6. (-. ((((aInteger0 (sdtpldt0 (sz10) (xp))) /\ ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (xp)) (sz10) (xp))))) \/ (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. ((((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10)))) /\ (aElementOf0 (sdtpldt0 (sz10) (xp)) (cS2200)))))) (-. (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))))) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ### NotAnd 2 5 % 244.15/244.40 7. (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))))) ### NotExists 6 % 244.15/244.40 8. ((sdtpldt0 (sz10) (xp)) != (sz10)) ((sdtpldt0 (sz10) (xp)) = (sz10)) ### Axiom % 244.15/244.40 9. ((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))) ### Axiom % 244.15/244.40 10. (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10)))) ((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) ((sdtpldt0 (sz10) (xp)) != (sz10)) ### Or 8 9 % 244.15/244.40 11. ((aElementOf0 (sdtpldt0 (sz10) (xp)) (stldt0 (sbsmnsldt0 (xS)))) <=> (((sdtpldt0 (sz10) (xp)) = (sz10)) \/ ((sdtpldt0 (sz10) (xp)) = (smndt0 (sz10))))) ((sdtpldt0 (sz10) (xp)) != (sz10)) ((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) ### Equiv 7 10 % 244.15/244.40 12. (All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) ((sdtpldt0 (sz10) (xp)) != (sz10)) ### All 11 % 244.15/244.40 13. (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) ### Axiom % 244.15/244.40 14. (-. (((aInteger0 (sdtpldt0 (sz10) (smndt0 (xp)))) /\ ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (smndt0 (xp))) (sz10) (xp))))) \/ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))))) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ### NotOr 13 % 244.15/244.40 15. (-. (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))))) (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10)))) ### Axiom % 244.15/244.40 16. ((((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10)))) /\ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (cS2200))) (-. (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))))) ### And 15 % 244.15/244.40 17. (-. (-. ((((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10)))) /\ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (cS2200))))) (-. (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))))) ### NotNot 16 % 244.15/244.40 18. (-. ((((aInteger0 (sdtpldt0 (sz10) (smndt0 (xp)))) /\ ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (smndt0 (xp))) (sz10) (xp))))) \/ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. ((((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10)))) /\ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (cS2200)))))) (-. (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))))) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ### NotAnd 14 17 % 244.15/244.40 19. (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))))) ### NotExists 18 % 244.15/244.40 20. ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) ((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) ### Axiom % 244.15/244.40 21. ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10))) ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))) ### Axiom % 244.15/244.40 22. (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10)))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) ### Or 20 21 % 244.15/244.40 23. ((aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (stldt0 (sbsmnsldt0 (xS)))) <=> (((sdtpldt0 (sz10) (smndt0 (xp))) = (sz10)) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) = (smndt0 (sz10))))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10))) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) ### Equiv 19 22 % 244.15/244.41 24. (All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) ### All 23 % 244.15/244.41 25. (((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10)))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ((sdtpldt0 (sz10) (xp)) != (sz10)) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))))) ### Or 12 24 % 244.15/244.41 26. ((aSet0 (sbsmnsldt0 (xS))) /\ ((All W0, ((aElementOf0 W0 (sbsmnsldt0 (xS))) <=> ((aInteger0 W0) /\ (Ex W1, ((aElementOf0 W1 (xS)) /\ (aElementOf0 W0 W1)))))) /\ ((aSet0 (stldt0 (sbsmnsldt0 (xS)))) /\ ((All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (sbsmnsldt0 (xS))))))) /\ ((All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))))) /\ ((stldt0 (sbsmnsldt0 (xS))) = (cS2076))))))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ((sdtpldt0 (sz10) (xp)) != (sz10)) (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) (((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10)))) ### ConjTree 25 % 244.15/244.41 27. ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))))) /\ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))) /\ ((sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (xp)) (sz10) (xp)) /\ ((aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) /\ ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))))) /\ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))) /\ ((sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (smndt0 (xp))) (sz10) (xp)) /\ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))))))))) (((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10)))) ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10)) ((sdtpldt0 (sz10) (xp)) != (sz10)) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) ((aSet0 (sbsmnsldt0 (xS))) /\ ((All W0, ((aElementOf0 W0 (sbsmnsldt0 (xS))) <=> ((aInteger0 W0) /\ (Ex W1, ((aElementOf0 W1 (xS)) /\ (aElementOf0 W0 W1)))))) /\ ((aSet0 (stldt0 (sbsmnsldt0 (xS)))) /\ ((All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (sbsmnsldt0 (xS))))))) /\ ((All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))))) /\ ((stldt0 (sbsmnsldt0 (xS))) = (cS2076))))))) ### ConjTree 26 % 244.15/244.41 28. (((sdtpldt0 (sz10) (xp)) != (sz10)) /\ ((sdtpldt0 (sz10) (smndt0 (xp))) != (sz10))) ((aSet0 (sbsmnsldt0 (xS))) /\ ((All W0, ((aElementOf0 W0 (sbsmnsldt0 (xS))) <=> ((aInteger0 W0) /\ (Ex W1, ((aElementOf0 W1 (xS)) /\ (aElementOf0 W0 W1)))))) /\ ((aSet0 (stldt0 (sbsmnsldt0 (xS)))) /\ ((All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((aInteger0 W0) /\ (-. (aElementOf0 W0 (sbsmnsldt0 (xS))))))) /\ ((All W0, ((aElementOf0 W0 (stldt0 (sbsmnsldt0 (xS)))) <=> ((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))))) /\ ((stldt0 (sbsmnsldt0 (xS))) = (cS2076))))))) (-. (Ex W0, ((((aInteger0 W0) /\ ((Ex W1, ((aInteger0 W1) /\ ((sdtasdt0 (xp) W1) = (sdtpldt0 W0 (smndt0 (sz10)))))) \/ ((aDivisorOf0 (xp) (sdtpldt0 W0 (smndt0 (sz10)))) \/ (sdteqdtlpzmzozddtrp0 W0 (sz10) (xp))))) \/ (aElementOf0 W0 (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))) /\ (-. (((W0 = (sz10)) \/ (W0 = (smndt0 (sz10)))) /\ (aElementOf0 W0 (cS2200))))))) (((sdtpldt0 (sz10) (xp)) != (smndt0 (sz10))) \/ ((sdtpldt0 (sz10) (smndt0 (xp))) != (smndt0 (sz10)))) ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))))) /\ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (xp)) (smndt0 (sz10)))) /\ ((sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (xp)) (sz10) (xp)) /\ ((aElementOf0 (sdtpldt0 (sz10) (xp)) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp))) /\ ((Ex W0, ((aInteger0 W0) /\ ((sdtasdt0 (xp) W0) = (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))))) /\ ((aDivisorOf0 (xp) (sdtpldt0 (sdtpldt0 (sz10) (smndt0 (xp))) (smndt0 (sz10)))) /\ ((sdteqdtlpzmzozddtrp0 (sdtpldt0 (sz10) (smndt0 (xp))) (sz10) (xp)) /\ (aElementOf0 (sdtpldt0 (sz10) (smndt0 (xp))) (szAzrzSzezqlpdtcmdtrp0 (sz10) (xp)))))))))) ### And 27 % 244.15/244.41 % SZS output end Proof % 244.15/244.41 (* END-PROOF *) %------------------------------------------------------------------------------