%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU212+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n011.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 : Tue Jul 19 14:49:14 EDT 2022 % Result : Theorem 241.09s 241.39s % Output : Proof 241.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SEU212+1 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n011.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 : Sun Jun 19 18:52:39 EDT 2022 % 0.12/0.33 % CPUTime : % 241.09/241.39 % SZS status Theorem % 241.09/241.39 (* PROOF-FOUND *) % 241.09/241.39 (* BEGIN-PROOF *) % 241.09/241.39 % SZS output start Proof % 241.09/241.39 1. (relation T_0) (-. (relation T_0)) ### Axiom % 241.09/241.39 2. (function T_0) (-. (function T_0)) ### Axiom % 241.09/241.39 3. (in T_1 (relation_dom T_0)) (-. (in T_1 (relation_dom T_0))) ### Axiom % 241.09/241.39 4. (T_2 = (apply T_0 T_1)) (T_2 != (apply T_0 T_1)) ### Axiom % 241.09/241.39 5. (-. (in (ordered_pair T_1 T_2) T_0)) (in (ordered_pair T_1 T_2) T_0) ### Axiom % 241.09/241.39 6. ((T_2 = (apply T_0 T_1)) <=> (in (ordered_pair T_1 T_2) T_0)) (-. (in (ordered_pair T_1 T_2) T_0)) (T_2 = (apply T_0 T_1)) ### Equiv 4 5 % 241.09/241.39 7. ((in T_1 (relation_dom T_0)) => ((T_2 = (apply T_0 T_1)) <=> (in (ordered_pair T_1 T_2) T_0))) (T_2 = (apply T_0 T_1)) (-. (in (ordered_pair T_1 T_2) T_0)) (in T_1 (relation_dom T_0)) ### Imply 3 6 % 241.09/241.39 8. (((in T_1 (relation_dom T_0)) => ((T_2 = (apply T_0 T_1)) <=> (in (ordered_pair T_1 T_2) T_0))) /\ ((-. (in T_1 (relation_dom T_0))) => ((T_2 = (apply T_0 T_1)) <=> (T_2 = (empty_set))))) (in T_1 (relation_dom T_0)) (-. (in (ordered_pair T_1 T_2) T_0)) (T_2 = (apply T_0 T_1)) ### And 7 % 241.09/241.39 9. (All C, (((in T_1 (relation_dom T_0)) => ((C = (apply T_0 T_1)) <=> (in (ordered_pair T_1 C) T_0))) /\ ((-. (in T_1 (relation_dom T_0))) => ((C = (apply T_0 T_1)) <=> (C = (empty_set)))))) (T_2 = (apply T_0 T_1)) (-. (in (ordered_pair T_1 T_2) T_0)) (in T_1 (relation_dom T_0)) ### All 8 % 241.09/241.39 10. (All B, (All C, (((in B (relation_dom T_0)) => ((C = (apply T_0 B)) <=> (in (ordered_pair B C) T_0))) /\ ((-. (in B (relation_dom T_0))) => ((C = (apply T_0 B)) <=> (C = (empty_set))))))) (in T_1 (relation_dom T_0)) (-. (in (ordered_pair T_1 T_2) T_0)) (T_2 = (apply T_0 T_1)) ### All 9 % 241.09/241.39 11. (((relation T_0) /\ (function T_0)) => (All B, (All C, (((in B (relation_dom T_0)) => ((C = (apply T_0 B)) <=> (in (ordered_pair B C) T_0))) /\ ((-. (in B (relation_dom T_0))) => ((C = (apply T_0 B)) <=> (C = (empty_set)))))))) (T_2 = (apply T_0 T_1)) (-. (in (ordered_pair T_1 T_2) T_0)) (in T_1 (relation_dom T_0)) (function T_0) (relation T_0) ### DisjTree 1 2 10 % 241.09/241.39 12. (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) (relation T_0) (function T_0) (in T_1 (relation_dom T_0)) (-. (in (ordered_pair T_1 T_2) T_0)) (T_2 = (apply T_0 T_1)) ### All 11 % 241.09/241.39 13. ((in T_1 (relation_dom T_0)) /\ (T_2 = (apply T_0 T_1))) (-. (in (ordered_pair T_1 T_2) T_0)) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) ### And 12 % 241.09/241.39 14. (relation T_0) (-. (relation T_0)) ### Axiom % 241.09/241.39 15. ((relation_dom T_0) != (relation_dom T_0)) ### Refl(=) % 241.09/241.39 16. (in (ordered_pair T_1 T_2) T_0) (-. (in (ordered_pair T_1 T_2) T_0)) ### Axiom % 241.09/241.39 17. (-. (Ex D, (in (ordered_pair T_1 D) T_0))) (in (ordered_pair T_1 T_2) T_0) ### NotExists 16 % 241.09/241.39 18. (-. (in T_1 (relation_dom T_0))) (in T_1 (relation_dom T_0)) ### Axiom % 241.09/241.39 19. ((in T_1 (relation_dom T_0)) <=> (Ex D, (in (ordered_pair T_1 D) T_0))) (-. (in T_1 (relation_dom T_0))) (in (ordered_pair T_1 T_2) T_0) ### Equiv 17 18 % 241.09/241.39 20. (All C, ((in C (relation_dom T_0)) <=> (Ex D, (in (ordered_pair C D) T_0)))) (in (ordered_pair T_1 T_2) T_0) (-. (in T_1 (relation_dom T_0))) ### All 19 % 241.09/241.39 21. (((relation_dom T_0) = (relation_dom T_0)) <=> (All C, ((in C (relation_dom T_0)) <=> (Ex D, (in (ordered_pair C D) T_0))))) (-. (in T_1 (relation_dom T_0))) (in (ordered_pair T_1 T_2) T_0) ### Equiv 15 20 % 241.09/241.39 22. (All B, ((B = (relation_dom T_0)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) T_0)))))) (in (ordered_pair T_1 T_2) T_0) (-. (in T_1 (relation_dom T_0))) ### All 21 % 241.09/241.39 23. ((relation T_0) => (All B, ((B = (relation_dom T_0)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) T_0))))))) (-. (in T_1 (relation_dom T_0))) (in (ordered_pair T_1 T_2) T_0) (relation T_0) ### Imply 14 22 % 241.09/241.39 24. (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (relation T_0) (in (ordered_pair T_1 T_2) T_0) (-. (in T_1 (relation_dom T_0))) ### All 23 % 241.09/241.39 25. (relation T_0) (-. (relation T_0)) ### Axiom % 241.09/241.39 26. (function T_0) (-. (function T_0)) ### Axiom % 241.09/241.39 27. (relation T_0) (-. (relation T_0)) ### Axiom % 241.09/241.39 28. ((relation_dom T_0) != (relation_dom T_0)) ### Refl(=) % 241.09/241.39 29. (in (ordered_pair T_1 T_2) T_0) (-. (in (ordered_pair T_1 T_2) T_0)) ### Axiom % 241.09/241.39 30. (T_2 != (apply T_0 T_1)) (T_2 = (apply T_0 T_1)) ### Axiom % 241.09/241.39 31. ((T_2 = (apply T_0 T_1)) <=> (in (ordered_pair T_1 T_2) T_0)) (T_2 != (apply T_0 T_1)) (in (ordered_pair T_1 T_2) T_0) ### Equiv 29 30 % 241.09/241.39 32. ((in T_1 (relation_dom T_0)) => ((T_2 = (apply T_0 T_1)) <=> (in (ordered_pair T_1 T_2) T_0))) (T_2 != (apply T_0 T_1)) (in (ordered_pair T_1 T_2) T_0) (All C, ((in C (relation_dom T_0)) <=> (Ex D, (in (ordered_pair C D) T_0)))) ### Imply 20 31 % 241.09/241.39 33. (((in T_1 (relation_dom T_0)) => ((T_2 = (apply T_0 T_1)) <=> (in (ordered_pair T_1 T_2) T_0))) /\ ((-. (in T_1 (relation_dom T_0))) => ((T_2 = (apply T_0 T_1)) <=> (T_2 = (empty_set))))) (All C, ((in C (relation_dom T_0)) <=> (Ex D, (in (ordered_pair C D) T_0)))) (in (ordered_pair T_1 T_2) T_0) (T_2 != (apply T_0 T_1)) ### And 32 % 241.09/241.39 34. (All C, (((in T_1 (relation_dom T_0)) => ((C = (apply T_0 T_1)) <=> (in (ordered_pair T_1 C) T_0))) /\ ((-. (in T_1 (relation_dom T_0))) => ((C = (apply T_0 T_1)) <=> (C = (empty_set)))))) (T_2 != (apply T_0 T_1)) (in (ordered_pair T_1 T_2) T_0) (All C, ((in C (relation_dom T_0)) <=> (Ex D, (in (ordered_pair C D) T_0)))) ### All 33 % 241.09/241.39 35. (((relation_dom T_0) = (relation_dom T_0)) <=> (All C, ((in C (relation_dom T_0)) <=> (Ex D, (in (ordered_pair C D) T_0))))) (in (ordered_pair T_1 T_2) T_0) (T_2 != (apply T_0 T_1)) (All C, (((in T_1 (relation_dom T_0)) => ((C = (apply T_0 T_1)) <=> (in (ordered_pair T_1 C) T_0))) /\ ((-. (in T_1 (relation_dom T_0))) => ((C = (apply T_0 T_1)) <=> (C = (empty_set)))))) ### Equiv 28 34 % 241.09/241.39 36. (All B, ((B = (relation_dom T_0)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) T_0)))))) (All C, (((in T_1 (relation_dom T_0)) => ((C = (apply T_0 T_1)) <=> (in (ordered_pair T_1 C) T_0))) /\ ((-. (in T_1 (relation_dom T_0))) => ((C = (apply T_0 T_1)) <=> (C = (empty_set)))))) (T_2 != (apply T_0 T_1)) (in (ordered_pair T_1 T_2) T_0) ### All 35 % 241.09/241.39 37. (All B, (All C, (((in B (relation_dom T_0)) => ((C = (apply T_0 B)) <=> (in (ordered_pair B C) T_0))) /\ ((-. (in B (relation_dom T_0))) => ((C = (apply T_0 B)) <=> (C = (empty_set))))))) (in (ordered_pair T_1 T_2) T_0) (T_2 != (apply T_0 T_1)) (All B, ((B = (relation_dom T_0)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) T_0)))))) ### All 36 % 241.09/241.39 38. ((relation T_0) => (All B, ((B = (relation_dom T_0)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) T_0))))))) (T_2 != (apply T_0 T_1)) (in (ordered_pair T_1 T_2) T_0) (All B, (All C, (((in B (relation_dom T_0)) => ((C = (apply T_0 B)) <=> (in (ordered_pair B C) T_0))) /\ ((-. (in B (relation_dom T_0))) => ((C = (apply T_0 B)) <=> (C = (empty_set))))))) (relation T_0) ### Imply 27 37 % 241.09/241.39 39. (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (relation T_0) (All B, (All C, (((in B (relation_dom T_0)) => ((C = (apply T_0 B)) <=> (in (ordered_pair B C) T_0))) /\ ((-. (in B (relation_dom T_0))) => ((C = (apply T_0 B)) <=> (C = (empty_set))))))) (in (ordered_pair T_1 T_2) T_0) (T_2 != (apply T_0 T_1)) ### All 38 % 241.09/241.39 40. (((relation T_0) /\ (function T_0)) => (All B, (All C, (((in B (relation_dom T_0)) => ((C = (apply T_0 B)) <=> (in (ordered_pair B C) T_0))) /\ ((-. (in B (relation_dom T_0))) => ((C = (apply T_0 B)) <=> (C = (empty_set)))))))) (T_2 != (apply T_0 T_1)) (in (ordered_pair T_1 T_2) T_0) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (function T_0) (relation T_0) ### DisjTree 25 26 39 % 241.09/241.39 41. (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) (relation T_0) (function T_0) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (in (ordered_pair T_1 T_2) T_0) (T_2 != (apply T_0 T_1)) ### All 40 % 241.09/241.39 42. (-. ((in T_1 (relation_dom T_0)) /\ (T_2 = (apply T_0 T_1)))) (function T_0) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) (in (ordered_pair T_1 T_2) T_0) (relation T_0) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) ### NotAnd 24 41 % 241.09/241.39 43. (-. ((in (ordered_pair T_1 T_2) T_0) <=> ((in T_1 (relation_dom T_0)) /\ (T_2 = (apply T_0 T_1))))) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) (relation T_0) (function T_0) ### NotEquiv 13 42 % 241.09/241.39 44. (-. (((relation T_0) /\ (function T_0)) => ((in (ordered_pair T_1 T_2) T_0) <=> ((in T_1 (relation_dom T_0)) /\ (T_2 = (apply T_0 T_1)))))) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) ### ConjTree 43 % 241.09/241.39 45. (-. (All C, (((relation C) /\ (function C)) => ((in (ordered_pair T_1 T_2) C) <=> ((in T_1 (relation_dom C)) /\ (T_2 = (apply C T_1))))))) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) ### NotAllEx 44 % 241.09/241.39 46. (-. (All B, (All C, (((relation C) /\ (function C)) => ((in (ordered_pair T_1 B) C) <=> ((in T_1 (relation_dom C)) /\ (B = (apply C T_1)))))))) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) ### NotAllEx 45 % 241.09/241.39 47. (-. (All A, (All B, (All C, (((relation C) /\ (function C)) => ((in (ordered_pair A B) C) <=> ((in A (relation_dom C)) /\ (B = (apply C A))))))))) (All A, ((relation A) => (All B, ((B = (relation_dom A)) <=> (All C, ((in C B) <=> (Ex D, (in (ordered_pair C D) A)))))))) (All A, (((relation A) /\ (function A)) => (All B, (All C, (((in B (relation_dom A)) => ((C = (apply A B)) <=> (in (ordered_pair B C) A))) /\ ((-. (in B (relation_dom A))) => ((C = (apply A B)) <=> (C = (empty_set))))))))) ### NotAllEx 46 % 241.09/241.39 % SZS output end Proof % 241.09/241.39 (* END-PROOF *) %------------------------------------------------------------------------------