%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM411+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 : n013.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 14:42:13 EDT 2022 % Result : Theorem 2.97s 3.19s % Output : Proof 2.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM411+1 : TPTP v8.1.0. Released v3.2.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n013.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 : Tue Jul 5 05:26:59 EDT 2022 % 0.12/0.34 % CPUTime : % 2.97/3.19 % SZS status Theorem % 2.97/3.19 (* PROOF-FOUND *) % 2.97/3.19 (* BEGIN-PROOF *) % 2.97/3.19 % SZS output start Proof % 2.97/3.19 1. (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence_of T_0 T_1)) ### Axiom % 2.97/3.19 2. (-. (relation T_0)) (relation T_0) ### Axiom % 2.97/3.19 3. ((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0))) (-. (relation T_0)) ### ConjTree 2 % 2.97/3.19 4. ((transfinite_sequence_of T_0 T_1) => ((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0)))) (-. (relation T_0)) (transfinite_sequence_of T_0 T_1) ### Imply 1 3 % 2.97/3.19 5. (All B, ((transfinite_sequence_of B T_1) => ((relation B) /\ ((function B) /\ (transfinite_sequence B))))) (transfinite_sequence_of T_0 T_1) (-. (relation T_0)) ### All 4 % 2.97/3.19 6. (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (-. (relation T_0)) (transfinite_sequence_of T_0 T_1) ### All 5 % 2.97/3.19 7. (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence_of T_0 T_1)) ### Axiom % 2.97/3.19 8. (-. (function T_0)) (function T_0) ### Axiom % 2.97/3.19 9. ((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0))) (-. (function T_0)) ### ConjTree 8 % 2.97/3.19 10. ((transfinite_sequence_of T_0 T_1) => ((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0)))) (-. (function T_0)) (transfinite_sequence_of T_0 T_1) ### Imply 7 9 % 2.97/3.19 11. (All B, ((transfinite_sequence_of B T_1) => ((relation B) /\ ((function B) /\ (transfinite_sequence B))))) (transfinite_sequence_of T_0 T_1) (-. (function T_0)) ### All 10 % 2.97/3.19 12. (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (-. (function T_0)) (transfinite_sequence_of T_0 T_1) ### All 11 % 2.97/3.19 13. (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence_of T_0 T_1)) ### Axiom % 2.97/3.19 14. (-. (transfinite_sequence T_0)) (transfinite_sequence T_0) ### Axiom % 2.97/3.19 15. ((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0))) (-. (transfinite_sequence T_0)) ### ConjTree 14 % 2.97/3.19 16. ((transfinite_sequence_of T_0 T_1) => ((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0)))) (-. (transfinite_sequence T_0)) (transfinite_sequence_of T_0 T_1) ### Imply 13 15 % 2.97/3.19 17. (All B, ((transfinite_sequence_of B T_1) => ((relation B) /\ ((function B) /\ (transfinite_sequence B))))) (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence T_0)) ### All 16 % 2.97/3.19 18. (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (-. (transfinite_sequence T_0)) (transfinite_sequence_of T_0 T_1) ### All 17 % 2.97/3.19 19. (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence_of T_0 T_1)) ### Axiom % 2.97/3.19 20. (-. (subset (relation_rng T_0) T_1)) (subset (relation_rng T_0) T_1) ### Axiom % 2.97/3.19 21. ((transfinite_sequence_of T_0 T_1) <=> (subset (relation_rng T_0) T_1)) (-. (subset (relation_rng T_0) T_1)) (transfinite_sequence_of T_0 T_1) ### Equiv 19 20 % 2.97/3.19 22. (((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0))) => ((transfinite_sequence_of T_0 T_1) <=> (subset (relation_rng T_0) T_1))) (-. (subset (relation_rng T_0) T_1)) (transfinite_sequence_of T_0 T_1) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) ### DisjTree 6 12 18 21 % 2.97/3.19 23. (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_1) <=> (subset (relation_rng B) T_1)))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (transfinite_sequence_of T_0 T_1) (-. (subset (relation_rng T_0) T_1)) ### All 22 % 2.97/3.19 24. (T_2 != T_2) ### Refl(=) % 2.97/3.19 25. (-. (subset (relation_rng T_0) T_2)) (subset T_1 T_2) (transfinite_sequence_of T_0 T_1) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_1) <=> (subset (relation_rng B) T_1)))) ### Trans 23 24 % 2.97/3.19 26. (-. (transfinite_sequence_of T_0 T_2)) (transfinite_sequence_of T_0 T_2) ### Axiom % 2.97/3.19 27. ((transfinite_sequence_of T_0 T_2) <=> (subset (relation_rng T_0) T_2)) (-. (transfinite_sequence_of T_0 T_2)) (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_1) <=> (subset (relation_rng B) T_1)))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (transfinite_sequence_of T_0 T_1) (subset T_1 T_2) ### Equiv 25 26 % 2.97/3.19 28. (((relation T_0) /\ ((function T_0) /\ (transfinite_sequence T_0))) => ((transfinite_sequence_of T_0 T_2) <=> (subset (relation_rng T_0) T_2))) (subset T_1 T_2) (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_1) <=> (subset (relation_rng B) T_1)))) (-. (transfinite_sequence_of T_0 T_2)) (transfinite_sequence_of T_0 T_1) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) ### DisjTree 6 12 18 27 % 2.97/3.19 29. (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_2) <=> (subset (relation_rng B) T_2)))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence_of T_0 T_2)) (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_1) <=> (subset (relation_rng B) T_1)))) (subset T_1 T_2) ### All 28 % 2.97/3.19 30. (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) (subset T_1 T_2) (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B T_1) <=> (subset (relation_rng B) T_1)))) (-. (transfinite_sequence_of T_0 T_2)) (transfinite_sequence_of T_0 T_1) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) ### All 29 % 2.97/3.19 31. (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (transfinite_sequence_of T_0 T_1) (-. (transfinite_sequence_of T_0 T_2)) (subset T_1 T_2) (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) ### All 30 % 2.97/3.19 32. (-. ((transfinite_sequence_of T_0 T_1) => (transfinite_sequence_of T_0 T_2))) (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) (subset T_1 T_2) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) ### NotImply 31 % 2.97/3.19 33. (-. (All C, ((transfinite_sequence_of C T_1) => (transfinite_sequence_of C T_2)))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (subset T_1 T_2) (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) ### NotAllEx 32 % 2.97/3.19 34. (-. ((subset T_1 T_2) => (All C, ((transfinite_sequence_of C T_1) => (transfinite_sequence_of C T_2))))) (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) ### NotImply 33 % 2.97/3.19 35. (-. (All B, ((subset T_1 B) => (All C, ((transfinite_sequence_of C T_1) => (transfinite_sequence_of C B)))))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) ### NotAllEx 34 % 2.97/3.19 36. (-. (All A, (All B, ((subset A B) => (All C, ((transfinite_sequence_of C A) => (transfinite_sequence_of C B))))))) (All A, (All B, (((relation B) /\ ((function B) /\ (transfinite_sequence B))) => ((transfinite_sequence_of B A) <=> (subset (relation_rng B) A))))) (All A, (All B, ((transfinite_sequence_of B A) => ((relation B) /\ ((function B) /\ (transfinite_sequence B)))))) ### NotAllEx 35 % 2.97/3.19 % SZS output end Proof % 2.97/3.19 (* END-PROOF *) %------------------------------------------------------------------------------