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