%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SYN943+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n016.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 : Thu Jul 21 12:47:25 EDT 2022 % Result : Theorem 0.23s 0.45s % Output : Proof 0.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SYN943+1 : TPTP v8.1.0. Released v3.1.0. % 0.08/0.15 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.37 % Computer : n016.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Mon Jul 11 12:08:27 EDT 2022 % 0.15/0.37 % CPUTime : % 0.23/0.45 % SZS status Theorem % 0.23/0.45 (* PROOF-FOUND *) % 0.23/0.45 (* BEGIN-PROOF *) % 0.23/0.45 % SZS output start Proof % 0.23/0.45 1. (e T_0) (-. (e T_0)) ### Axiom % 0.23/0.45 2. (p T_0) (-. (p T_0)) ### Axiom % 0.23/0.45 3. (g T_0) (-. (g T_0)) ### Axiom % 0.23/0.45 4. (-. ((p T_0) /\ (g T_0))) (g T_0) (p T_0) ### NotAnd 2 3 % 0.23/0.45 5. (-. (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 zenon_X2) => (p zenon_X2)))))) => (((p T_0) /\ (g T_0)) \/ ((p zenon_X3) /\ (c zenon_X3))))) (p T_0) (g T_0) ### ConjTree 4 % 0.23/0.45 6. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p T_0) /\ (g T_0)) \/ ((p zenon_X3) /\ (c zenon_X3)))))) (g T_0) (p T_0) ### NotExists 5 % 0.23/0.45 7. (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p T_0) /\ (g T_0)) \/ ((p X4) /\ (c X4))))))) (p T_0) (g T_0) ### NotExists 6 % 0.23/0.45 8. (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (g T_0) (p T_0) ### NotExists 7 % 0.23/0.45 9. (e T_0) (-. (e T_0)) ### Axiom % 0.23/0.45 10. (-. (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 zenon_X5) => (p zenon_X5)))))) => (((p T_0) /\ (g T_0)) \/ ((p zenon_X6) /\ (c zenon_X6))))) (p T_0) (g T_0) ### ConjTree 4 % 0.23/0.45 11. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p T_0) /\ (g T_0)) \/ ((p zenon_X6) /\ (c zenon_X6)))))) (g T_0) (p T_0) ### NotExists 10 % 0.23/0.45 12. (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p T_0) /\ (g T_0)) \/ ((p X4) /\ (c X4))))))) (p T_0) (g T_0) ### NotExists 11 % 0.23/0.45 13. (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (g T_0) (p T_0) ### NotExists 12 % 0.23/0.45 14. (s T_0 (f T_0)) (-. (s T_0 (f T_0))) ### Axiom % 0.23/0.45 15. (-. (p (f T_0))) (p (f T_0)) ### Axiom % 0.23/0.45 16. ((s T_0 (f T_0)) => (p (f T_0))) (-. (p (f T_0))) (s T_0 (f T_0)) ### Imply 14 15 % 0.23/0.45 17. (-. (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 (f T_0)) => (p (f T_0))))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7)))))) (s T_0 (f T_0)) (-. (p (f T_0))) ### ConjTree 16 % 0.23/0.45 18. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (p (f T_0))) (s T_0 (f T_0)) ### NotExists 17 % 0.23/0.45 19. (c (f T_0)) (-. (c (f T_0))) ### Axiom % 0.23/0.45 20. (-. ((p (f T_0)) /\ (c (f T_0)))) (c (f T_0)) (s T_0 (f T_0)) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) ### NotAnd 18 19 % 0.23/0.45 21. (-. (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 zenon_X9) => (p zenon_X9)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p (f T_0)) /\ (c (f T_0)))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (s T_0 (f T_0)) (c (f T_0)) ### ConjTree 20 % 0.23/0.45 22. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p (f T_0)) /\ (c (f T_0))))))) (c (f T_0)) (s T_0 (f T_0)) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) ### NotExists 21 % 0.23/0.45 23. (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p X4) /\ (c X4))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (s T_0 (f T_0)) (c (f T_0)) ### NotExists 22 % 0.23/0.45 24. ((e T_0) => ((g T_0) \/ (c (f T_0)))) (s T_0 (f T_0)) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p X4) /\ (c X4))))))) (p T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (e T_0) ### DisjTree 9 13 23 % 0.23/0.45 25. (-. (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 zenon_X11) => (p zenon_X11)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p zenon_X12) /\ (c zenon_X12))))) (e T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (p T_0) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p X4) /\ (c X4))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (s T_0 (f T_0)) ### ConjTree 24 % 0.23/0.45 26. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p zenon_X12) /\ (c zenon_X12)))))) (s T_0 (f T_0)) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p X4) /\ (c X4))))))) (p T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (e T_0) ### NotExists 25 % 0.23/0.47 27. (e T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (p T_0) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X10) /\ (g zenon_X10)) \/ ((p X4) /\ (c X4))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (s T_0 (f T_0)) ### NotExists 26 % 0.23/0.47 28. (s T_0 (f T_0)) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (p T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e T_0) => ((g T_0) \/ (c (f T_0)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (e T_0) ### NotExists 27 % 0.23/0.47 29. (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (e T_0) (p T_0) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (s T_0 (f T_0)) ### NotExists 28 % 0.23/0.47 30. ((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (p T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (e T_0) ### DisjTree 1 8 29 % 0.23/0.47 31. (-. (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 zenon_X13) => (p zenon_X13)))))) => (((p zenon_X14) /\ (g zenon_X14)) \/ ((p zenon_X15) /\ (c zenon_X15))))) (e T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (p T_0) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) ### ConjTree 30 % 0.23/0.47 32. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X14) /\ (g zenon_X14)) \/ ((p zenon_X15) /\ (c zenon_X15)))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (p T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (e T_0) ### NotExists 31 % 0.23/0.47 33. (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X14) /\ (g zenon_X14)) \/ ((p X4) /\ (c X4))))))) (e T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (p T_0) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) ### NotExists 32 % 0.23/0.47 34. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (p T_0) (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e zenon_X1) => ((g zenon_X1) \/ (c (f zenon_X1)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (e T_0) ### NotExists 33 % 0.23/0.47 35. (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e T_0) => ((g T_0) \/ (s T_0 (f T_0)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (e T_0) (p T_0) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) ### NotExists 34 % 0.23/0.47 36. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p (f zenon_X7)) /\ (c (f zenon_X7))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (p T_0) (e T_0) ### NotExists 35 % 0.23/0.47 37. (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p X4) /\ (c X4))))))) (e T_0) (p T_0) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) ### NotExists 36 % 0.23/0.48 38. (-. (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 zenon_X16) => (p zenon_X16)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p zenon_X17) /\ (c zenon_X17))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p X4) /\ (c X4))))))) ### ConjTree 37 % 0.23/0.48 39. (-. (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p zenon_X17) /\ (c zenon_X17)))))) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p X4) /\ (c X4))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) ### NotExists 38 % 0.23/0.48 40. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p zenon_X8) /\ (g zenon_X8)) \/ ((p X4) /\ (c X4))))))) ### NotExists 39 % 0.23/0.48 41. (-. (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e zenon_X7) => ((g zenon_X7) \/ (c (f zenon_X7)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) ### NotExists 40 % 0.23/0.48 42. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) (-. (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e zenon_X4) => ((g zenon_X4) \/ (s zenon_X4 (f zenon_X4)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))) ### NotExists 41 % 0.23/0.48 43. (-. (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p T_0) /\ ((e T_0) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s T_0 Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4)))))))))) ### NotExists 42 % 0.23/0.48 44. (-. (All A, (Ex X, (Ex X2, (Ex X3, (Ex X4, (Ex Y, (((p A) /\ ((e A) /\ (((e X) => ((g X) \/ (s X (f X)))) /\ (((e X2) => ((g X2) \/ (c (f X2)))) /\ ((s A Y) => (p Y)))))) => (((p X3) /\ (g X3)) \/ ((p X4) /\ (c X4))))))))))) ### NotAllEx 43 % 0.23/0.48 % SZS output end Proof % 0.23/0.48 (* END-PROOF *) %------------------------------------------------------------------------------