%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : PUZ128+2 : 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 : n020.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 18:27:55 EDT 2022 % Result : Theorem 0.91s 1.15s % Output : Proof 0.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PUZ128+2 : TPTP v8.1.0. Released v4.0.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n020.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 : Sat May 28 21:12:09 EDT 2022 % 0.12/0.33 % CPUTime : % 0.91/1.15 % SZS status Theorem % 0.91/1.15 (* PROOF-FOUND *) % 0.91/1.15 (* BEGIN-PROOF *) % 0.91/1.15 % SZS output start Proof % 0.91/1.15 1. ((Iokaste) = T_0) (T_0 != (Iokaste)) ### Sym(=) % 0.91/1.15 2. (-. (parent (Iokaste))) (parent T_0) ((Iokaste) = T_0) ### P-NotP 1 % 0.91/1.15 3. ((Oedipus) = T_1) (T_1 != (Oedipus)) ### Sym(=) % 0.91/1.15 4. (-. (patricide (Oedipus))) (patricide T_1) ((Oedipus) = T_1) ### P-NotP 3 % 0.91/1.15 5. (parent T_2) (-. (parent T_2)) ### Axiom % 0.91/1.15 6. (-. True) ### NotTrue % 0.91/1.15 7. (parent T_0) (-. (parent T_0)) ### Axiom % 0.91/1.15 8. (patricide T_3) (-. (patricide T_3)) ### Axiom % 0.91/1.15 9. (parent T_4) (-. (parent T_4)) ### Axiom % 0.91/1.15 10. (-. True) ### NotTrue % 0.91/1.15 11. (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (Ex F, ((patricide F) /\ ((Thersandros) = F))) ### Axiom % 0.91/1.15 12. (relation T_4 (of) (Thersandros)) (-. (relation T_4 (of) (Thersandros))) ### Axiom % 0.91/1.15 13. (T_4 = T_3) (T_3 != T_4) ### Sym(=) % 0.91/1.15 14. ((Iokaste) = T_0) (T_0 != (Iokaste)) ### Sym(=) % 0.91/1.15 15. (T_5 != T_5) ### Refl(=) % 0.91/1.15 16. (T_5 != T_0) ((Iokaste) = T_5) ((Iokaste) = T_0) ### Trans-sym 14 15 % 0.91/1.15 17. ((of) != (of)) ### NotEqual % 0.91/1.15 18. ((Polyneikes) != (Polyneikes)) ### NotEqual % 0.91/1.15 19. (T_4 = T_3) (T_4 != T_3) ### Axiom % 0.91/1.15 20. ((Polyneikes) != T_3) ((Polyneikes) = T_4) (T_4 = T_3) ### Trans 18 19 % 0.91/1.15 21. (-. (relation T_0 (of) T_3)) (relation T_5 (of) (Polyneikes)) (T_4 = T_3) ((Polyneikes) = T_4) ((Iokaste) = T_0) ((Iokaste) = T_5) ### P-NotP 16 17 20 % 0.91/1.15 22. ((Iokaste) = T_0) ((Iokaste) != T_0) ### Axiom % 0.91/1.15 23. (-. ((parent T_0) /\ ((patricide T_3) /\ ((parent T_4) /\ (True /\ ((-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) /\ ((relation T_4 (of) (Thersandros)) /\ ((T_3 = T_4) /\ ((relation T_0 (of) T_3) /\ ((Iokaste) = T_0)))))))))) ((Iokaste) = T_5) ((Iokaste) = T_0) ((Polyneikes) = T_4) (relation T_5 (of) (Polyneikes)) (T_4 = T_3) (relation T_4 (of) (Thersandros)) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (parent T_4) (patricide T_3) (parent T_0) ### DisjTree 7 8 9 10 11 12 13 21 22 % 0.91/1.15 24. (-. (Ex D, ((parent T_0) /\ ((patricide T_3) /\ ((parent T_4) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation T_4 (of) D) /\ ((T_3 = T_4) /\ ((relation T_0 (of) T_3) /\ ((Iokaste) = T_0))))))))))) (parent T_0) (patricide T_3) (parent T_4) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (relation T_4 (of) (Thersandros)) (T_4 = T_3) (relation T_5 (of) (Polyneikes)) ((Polyneikes) = T_4) ((Iokaste) = T_0) ((Iokaste) = T_5) ### NotExists 23 % 0.91/1.15 25. (-. (Ex C, (Ex D, ((parent T_0) /\ ((patricide T_3) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((T_3 = C) /\ ((relation T_0 (of) T_3) /\ ((Iokaste) = T_0)))))))))))) ((Iokaste) = T_5) ((Iokaste) = T_0) ((Polyneikes) = T_4) (relation T_5 (of) (Polyneikes)) (T_4 = T_3) (relation T_4 (of) (Thersandros)) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (parent T_4) (patricide T_3) (parent T_0) ### NotExists 24 % 0.91/1.15 26. (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) (parent T_0) (patricide T_3) (parent T_4) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (relation T_4 (of) (Thersandros)) (T_4 = T_3) (relation T_5 (of) (Polyneikes)) ((Polyneikes) = T_4) ((Iokaste) = T_0) ((Iokaste) = T_5) ### NotExists 25 % 0.91/1.15 27. ((patricide T_3) /\ (T_4 = T_3)) ((Iokaste) = T_5) ((Iokaste) = T_0) ((Polyneikes) = T_4) (relation T_5 (of) (Polyneikes)) (relation T_4 (of) (Thersandros)) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (parent T_4) (parent T_0) (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) ### And 26 % 0.91/1.15 28. (Ex E, ((patricide E) /\ (T_4 = E))) (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) (parent T_0) (parent T_4) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (relation T_4 (of) (Thersandros)) (relation T_5 (of) (Polyneikes)) ((Polyneikes) = T_4) ((Iokaste) = T_0) ((Iokaste) = T_5) ### Exists 27 % 0.91/1.15 29. (T_2 != T_2) ### Refl(=) % 0.91/1.15 30. ((Polyneikes) = T_4) ((Polyneikes) != T_4) ### Axiom % 0.91/1.15 31. (-. (relation T_2 (of) T_4)) (relation T_2 (of) (Polyneikes)) ((Polyneikes) = T_4) ### P-NotP 29 17 30 % 0.91/1.15 32. ((Oedipus) = T_2) ((Oedipus) != T_2) ### Axiom % 0.91/1.15 33. ((Iokaste) = T_0) (T_0 != (Iokaste)) ### Sym(=) % 0.91/1.15 34. ((Oedipus) != (Oedipus)) ### NotEqual % 0.91/1.15 35. (-. (relation (Iokaste) (of) (Oedipus))) (relation T_0 (of) (Oedipus)) ((Iokaste) = T_0) ### P-NotP 33 17 34 % 0.91/1.15 36. ((Iokaste) != (Iokaste)) ### NotEqual % 0.91/1.15 37. (-. ((parent (Iokaste)) /\ ((patricide (Oedipus)) /\ ((parent T_2) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (T_4 = E)))) /\ ((relation T_2 (of) T_4) /\ (((Oedipus) = T_2) /\ ((relation (Iokaste) (of) (Oedipus)) /\ ((Iokaste) = (Iokaste))))))))))) (relation T_0 (of) (Oedipus)) ((Oedipus) = T_2) (relation T_2 (of) (Polyneikes)) ((Iokaste) = T_5) ((Polyneikes) = T_4) (relation T_5 (of) (Polyneikes)) (relation T_4 (of) (Thersandros)) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (parent T_4) (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) (parent T_2) ((Oedipus) = T_1) (patricide T_1) ((Iokaste) = T_0) (parent T_0) ### DisjTree 2 4 5 6 28 31 32 35 36 % 0.91/1.15 38. (-. (Ex D, ((parent (Iokaste)) /\ ((patricide (Oedipus)) /\ ((parent T_2) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation T_2 (of) D) /\ (((Oedipus) = T_2) /\ ((relation (Iokaste) (of) (Oedipus)) /\ ((Iokaste) = (Iokaste)))))))))))) (parent T_0) ((Iokaste) = T_0) (patricide T_1) ((Oedipus) = T_1) (parent T_2) (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) (parent T_4) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (relation T_4 (of) (Thersandros)) (relation T_5 (of) (Polyneikes)) ((Polyneikes) = T_4) ((Iokaste) = T_5) (relation T_2 (of) (Polyneikes)) ((Oedipus) = T_2) (relation T_0 (of) (Oedipus)) ### NotExists 37 % 0.91/1.15 39. (-. (Ex C, (Ex D, ((parent (Iokaste)) /\ ((patricide (Oedipus)) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ (((Oedipus) = C) /\ ((relation (Iokaste) (of) (Oedipus)) /\ ((Iokaste) = (Iokaste))))))))))))) (relation T_0 (of) (Oedipus)) ((Oedipus) = T_2) (relation T_2 (of) (Polyneikes)) ((Iokaste) = T_5) ((Polyneikes) = T_4) (relation T_5 (of) (Polyneikes)) (relation T_4 (of) (Thersandros)) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (parent T_4) (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) (parent T_2) ((Oedipus) = T_1) (patricide T_1) ((Iokaste) = T_0) (parent T_0) ### NotExists 38 % 0.91/1.15 40. (-. (Ex B, (Ex C, (Ex D, ((parent (Iokaste)) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation (Iokaste) (of) B) /\ ((Iokaste) = (Iokaste)))))))))))))) (parent T_0) ((Iokaste) = T_0) (patricide T_1) ((Oedipus) = T_1) (parent T_2) (-. (Ex B, (Ex C, (Ex D, ((parent T_0) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation T_0 (of) B) /\ ((Iokaste) = T_0))))))))))))) (parent T_4) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (relation T_4 (of) (Thersandros)) (relation T_5 (of) (Polyneikes)) ((Polyneikes) = T_4) ((Iokaste) = T_5) (relation T_2 (of) (Polyneikes)) ((Oedipus) = T_2) (relation T_0 (of) (Oedipus)) ### NotExists 39 % 0.91/1.15 41. (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) (relation T_0 (of) (Oedipus)) ((Oedipus) = T_2) (relation T_2 (of) (Polyneikes)) ((Iokaste) = T_5) ((Polyneikes) = T_4) (relation T_5 (of) (Polyneikes)) (relation T_4 (of) (Thersandros)) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (parent T_4) (parent T_2) ((Oedipus) = T_1) (patricide T_1) ((Iokaste) = T_0) (parent T_0) (-. (Ex B, (Ex C, (Ex D, ((parent (Iokaste)) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation (Iokaste) (of) B) /\ ((Iokaste) = (Iokaste)))))))))))))) ### NotExists 40 % 0.91/1.16 42. (parent T_0) ((Iokaste) = T_0) (patricide T_1) ((Oedipus) = T_1) (parent T_2) (parent T_4) (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))) (relation T_4 (of) (Thersandros)) (relation T_5 (of) (Polyneikes)) ((Polyneikes) = T_4) ((Iokaste) = T_5) (relation T_2 (of) (Polyneikes)) ((Oedipus) = T_2) (relation T_0 (of) (Oedipus)) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### NotExists 41 % 0.91/1.16 43. ((parent T_0) /\ ((relation T_0 (of) (Oedipus)) /\ (((Iokaste) = T_0) /\ ((parent T_5) /\ ((relation T_5 (of) (Polyneikes)) /\ (((Iokaste) = T_5) /\ ((parent T_2) /\ ((relation T_2 (of) (Polyneikes)) /\ (((Oedipus) = T_2) /\ ((parent T_4) /\ ((relation T_4 (of) (Thersandros)) /\ (((Polyneikes) = T_4) /\ ((patricide T_1) /\ (((Oedipus) = T_1) /\ (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))))))))))))))))) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### ConjTree 42 % 0.91/1.16 44. (Ex E, ((parent T_0) /\ ((relation T_0 (of) (Oedipus)) /\ (((Iokaste) = T_0) /\ ((parent T_5) /\ ((relation T_5 (of) (Polyneikes)) /\ (((Iokaste) = T_5) /\ ((parent T_2) /\ ((relation T_2 (of) (Polyneikes)) /\ (((Oedipus) = T_2) /\ ((parent T_4) /\ ((relation T_4 (of) (Thersandros)) /\ (((Polyneikes) = T_4) /\ ((patricide E) /\ (((Oedipus) = E) /\ (-. (Ex F, ((patricide F) /\ ((Thersandros) = F))))))))))))))))))) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### Exists 43 % 0.91/1.16 45. (Ex D, (Ex E, ((parent T_0) /\ ((relation T_0 (of) (Oedipus)) /\ (((Iokaste) = T_0) /\ ((parent T_5) /\ ((relation T_5 (of) (Polyneikes)) /\ (((Iokaste) = T_5) /\ ((parent T_2) /\ ((relation T_2 (of) (Polyneikes)) /\ (((Oedipus) = T_2) /\ ((parent D) /\ ((relation D (of) (Thersandros)) /\ (((Polyneikes) = D) /\ ((patricide E) /\ (((Oedipus) = E) /\ (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))))))))))))))))))) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### Exists 44 % 0.91/1.16 46. (Ex C, (Ex D, (Ex E, ((parent T_0) /\ ((relation T_0 (of) (Oedipus)) /\ (((Iokaste) = T_0) /\ ((parent T_5) /\ ((relation T_5 (of) (Polyneikes)) /\ (((Iokaste) = T_5) /\ ((parent C) /\ ((relation C (of) (Polyneikes)) /\ (((Oedipus) = C) /\ ((parent D) /\ ((relation D (of) (Thersandros)) /\ (((Polyneikes) = D) /\ ((patricide E) /\ (((Oedipus) = E) /\ (-. (Ex F, ((patricide F) /\ ((Thersandros) = F))))))))))))))))))))) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### Exists 45 % 0.91/1.16 47. (Ex B, (Ex C, (Ex D, (Ex E, ((parent T_0) /\ ((relation T_0 (of) (Oedipus)) /\ (((Iokaste) = T_0) /\ ((parent B) /\ ((relation B (of) (Polyneikes)) /\ (((Iokaste) = B) /\ ((parent C) /\ ((relation C (of) (Polyneikes)) /\ (((Oedipus) = C) /\ ((parent D) /\ ((relation D (of) (Thersandros)) /\ (((Polyneikes) = D) /\ ((patricide E) /\ (((Oedipus) = E) /\ (-. (Ex F, ((patricide F) /\ ((Thersandros) = F)))))))))))))))))))))) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### Exists 46 % 0.91/1.16 48. (Ex A, (Ex B, (Ex C, (Ex D, (Ex E, ((parent A) /\ ((relation A (of) (Oedipus)) /\ (((Iokaste) = A) /\ ((parent B) /\ ((relation B (of) (Polyneikes)) /\ (((Iokaste) = B) /\ ((parent C) /\ ((relation C (of) (Polyneikes)) /\ (((Oedipus) = C) /\ ((parent D) /\ ((relation D (of) (Thersandros)) /\ (((Polyneikes) = D) /\ ((patricide E) /\ (((Oedipus) = E) /\ (-. (Ex F, ((patricide F) /\ ((Thersandros) = F))))))))))))))))))))))) (-. (Ex A, (Ex B, (Ex C, (Ex D, ((parent A) /\ ((patricide B) /\ ((parent C) /\ (True /\ ((-. (Ex E, ((patricide E) /\ (D = E)))) /\ ((relation C (of) D) /\ ((B = C) /\ ((relation A (of) B) /\ ((Iokaste) = A)))))))))))))) ### Exists 47 % 0.91/1.16 % SZS output end Proof % 0.91/1.16 (* END-PROOF *) %------------------------------------------------------------------------------