%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU026+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n012.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:48:01 EDT 2022 % Result : Theorem 76.73s 76.96s % Output : Proof 76.73s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.08 % Problem : SEU026+1 : TPTP v8.1.0. Released v3.2.0. % 0.02/0.09 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.08/0.28 % Computer : n012.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 600 % 0.08/0.28 % DateTime : Mon Jun 20 09:43:22 EDT 2022 % 0.08/0.28 % CPUTime : % 76.73/76.96 % SZS status Theorem % 76.73/76.96 (* PROOF-FOUND *) % 76.73/76.96 (* BEGIN-PROOF *) % 76.73/76.96 % SZS output start Proof % 76.73/76.96 1. (relation T_0) (-. (relation T_0)) ### Axiom % 76.73/76.96 2. (function T_0) (-. (function T_0)) ### Axiom % 76.73/76.96 3. (one_to_one T_0) (-. (one_to_one T_0)) ### Axiom % 76.73/76.96 4. (relation T_0) (-. (relation T_0)) ### Axiom % 76.73/76.96 5. (function T_0) (-. (function T_0)) ### Axiom % 76.73/76.96 6. (-. (relation (function_inverse T_0))) (relation (function_inverse T_0)) ### Axiom % 76.73/76.96 7. ((relation (function_inverse T_0)) /\ (function (function_inverse T_0))) (-. (relation (function_inverse T_0))) ### And 6 % 76.73/76.96 8. (((relation T_0) /\ (function T_0)) => ((relation (function_inverse T_0)) /\ (function (function_inverse T_0)))) (-. (relation (function_inverse T_0))) (function T_0) (relation T_0) ### DisjTree 4 5 7 % 76.73/76.96 9. (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) (-. (relation (function_inverse T_0))) ### All 8 % 76.73/76.96 10. ((relation_rng T_0) != (relation_rng T_0)) ### Refl(=) % 76.73/76.96 11. ((relation_rng T_0) != (relation_rng T_0)) ### Refl(=) % 76.73/76.96 12. (relation T_0) (-. (relation T_0)) ### Axiom % 76.73/76.96 13. ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ((relation_rng (function_inverse T_0)) != (relation_dom T_0)) ### Sym(=) % 76.73/76.96 14. (-. (subset (relation_rng (function_inverse T_0)) (relation_dom T_0))) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ### Refl(subset) 13 % 76.73/76.96 15. ((relation_dom (function_inverse T_0)) != (relation_dom (relation_composition (function_inverse T_0) T_0))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_dom (function_inverse T_0))) ### Sym(=) % 76.73/76.96 16. ((relation T_0) => ((subset (relation_rng (function_inverse T_0)) (relation_dom T_0)) => ((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_dom (function_inverse T_0))))) ((relation_dom (function_inverse T_0)) != (relation_dom (relation_composition (function_inverse T_0) T_0))) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) (relation T_0) ### DisjTree 12 14 15 % 76.73/76.96 17. (All B, ((relation B) => ((subset (relation_rng (function_inverse T_0)) (relation_dom B)) => ((relation_dom (relation_composition (function_inverse T_0) B)) = (relation_dom (function_inverse T_0)))))) (relation T_0) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ((relation_dom (function_inverse T_0)) != (relation_dom (relation_composition (function_inverse T_0) T_0))) ### All 16 % 76.73/76.96 18. ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) ((relation_rng T_0) = (relation_dom (function_inverse T_0))) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) (relation T_0) (All B, ((relation B) => ((subset (relation_rng (function_inverse T_0)) (relation_dom B)) => ((relation_dom (relation_composition (function_inverse T_0) B)) = (relation_dom (function_inverse T_0)))))) ### TransEq-sym 10 11 17 % 76.73/76.96 19. ((relation (function_inverse T_0)) => (All B, ((relation B) => ((subset (relation_rng (function_inverse T_0)) (relation_dom B)) => ((relation_dom (relation_composition (function_inverse T_0) B)) = (relation_dom (function_inverse T_0))))))) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ((relation_rng T_0) = (relation_dom (function_inverse T_0))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### Imply 9 18 % 76.73/76.96 20. (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) ((relation_rng T_0) = (relation_dom (function_inverse T_0))) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ### All 19 % 76.73/76.96 21. (((relation_rng T_0) = (relation_dom (function_inverse T_0))) /\ ((relation_dom T_0) = (relation_rng (function_inverse T_0)))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) ### And 20 % 76.73/76.96 22. (((relation T_0) /\ (function T_0)) => ((one_to_one T_0) => (((relation_rng T_0) = (relation_dom (function_inverse T_0))) /\ ((relation_dom T_0) = (relation_rng (function_inverse T_0)))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (one_to_one T_0) (function T_0) (relation T_0) ### DisjTree 1 2 3 21 % 76.73/76.96 23. (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) (relation T_0) (function T_0) (one_to_one T_0) ((relation_dom (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) ### All 22 % 76.73/76.96 24. (relation T_0) (-. (relation T_0)) ### Axiom % 76.73/76.96 25. (relation T_0) (-. (relation T_0)) ### Axiom % 76.73/76.96 26. (function T_0) (-. (function T_0)) ### Axiom % 76.73/76.96 27. (one_to_one T_0) (-. (one_to_one T_0)) ### Axiom % 76.73/76.96 28. ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ((relation_dom T_0) != (relation_rng (function_inverse T_0))) ### Axiom % 76.73/76.96 29. (-. (subset (relation_dom T_0) (relation_rng (function_inverse T_0)))) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ### Refl(subset) 28 % 76.73/76.96 30. ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) ((relation_rng (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) ### Axiom % 76.73/76.96 31. ((relation (function_inverse T_0)) => ((subset (relation_dom T_0) (relation_rng (function_inverse T_0))) => ((relation_rng (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)))) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### DisjTree 9 29 30 % 76.73/76.96 32. (All B, ((relation B) => ((subset (relation_dom T_0) (relation_rng B)) => ((relation_rng (relation_composition B T_0)) = (relation_rng T_0))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (relation T_0) (function T_0) ((relation_dom T_0) = (relation_rng (function_inverse T_0))) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) ### All 31 % 76.73/76.96 33. (((relation_rng T_0) = (relation_dom (function_inverse T_0))) /\ ((relation_dom T_0) = (relation_rng (function_inverse T_0)))) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All B, ((relation B) => ((subset (relation_dom T_0) (relation_rng B)) => ((relation_rng (relation_composition B T_0)) = (relation_rng T_0))))) ### And 32 % 76.73/76.96 34. (((relation T_0) /\ (function T_0)) => ((one_to_one T_0) => (((relation_rng T_0) = (relation_dom (function_inverse T_0))) /\ ((relation_dom T_0) = (relation_rng (function_inverse T_0)))))) (All B, ((relation B) => ((subset (relation_dom T_0) (relation_rng B)) => ((relation_rng (relation_composition B T_0)) = (relation_rng T_0))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (one_to_one T_0) (function T_0) (relation T_0) ### DisjTree 25 26 27 33 % 76.73/76.98 35. (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) (relation T_0) (function T_0) (one_to_one T_0) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All B, ((relation B) => ((subset (relation_dom T_0) (relation_rng B)) => ((relation_rng (relation_composition B T_0)) = (relation_rng T_0))))) ### All 34 % 76.73/76.98 36. ((relation T_0) => (All B, ((relation B) => ((subset (relation_dom T_0) (relation_rng B)) => ((relation_rng (relation_composition B T_0)) = (relation_rng T_0)))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (one_to_one T_0) (function T_0) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) (relation T_0) ### Imply 24 35 % 76.73/76.98 37. (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_dom A) (relation_rng B)) => ((relation_rng (relation_composition B A)) = (relation_rng A))))))) (relation T_0) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) (function T_0) (one_to_one T_0) ((relation_rng (relation_composition (function_inverse T_0) T_0)) != (relation_rng T_0)) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) ### All 36 % 76.73/76.98 38. (-. (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ ((relation_rng (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_dom A) (relation_rng B)) => ((relation_rng (relation_composition B A)) = (relation_rng A))))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (one_to_one T_0) (function T_0) (relation T_0) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) ### NotAnd 23 37 % 76.73/76.98 39. (-. (((relation T_0) /\ (function T_0)) => ((one_to_one T_0) => (((relation_dom (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)) /\ ((relation_rng (relation_composition (function_inverse T_0) T_0)) = (relation_rng T_0)))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_dom A) (relation_rng B)) => ((relation_rng (relation_composition B A)) = (relation_rng A))))))) ### ConjTree 38 % 76.73/76.98 40. (-. (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_dom (relation_composition (function_inverse A) A)) = (relation_rng A)) /\ ((relation_rng (relation_composition (function_inverse A) A)) = (relation_rng A))))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_dom A) (relation_rng B)) => ((relation_rng (relation_composition B A)) = (relation_rng A))))))) (All A, ((relation A) => (All B, ((relation B) => ((subset (relation_rng A) (relation_dom B)) => ((relation_dom (relation_composition A B)) = (relation_dom A))))))) (All A, (((relation A) /\ (function A)) => ((relation (function_inverse A)) /\ (function (function_inverse A))))) (All A, (((relation A) /\ (function A)) => ((one_to_one A) => (((relation_rng A) = (relation_dom (function_inverse A))) /\ ((relation_dom A) = (relation_rng (function_inverse A))))))) ### NotAllEx 39 % 76.73/76.98 % SZS output end Proof % 76.73/76.98 (* END-PROOF *) %------------------------------------------------------------------------------