%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEV580+1 : TPTP v9.1.0. Released v9.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n009.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 : 300s % DateTime : Tue Apr 1 02:03:38 AM UTC 2025 % Result : Theorem 0.12s 0.40s % Output : Proof 0.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEV580+1 : TPTP v9.1.0. Released v9.1.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n009.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 : 300 % 0.12/0.33 % DateTime : Mon Mar 31 13:10:58 EDT 2025 % 0.12/0.33 % CPUTime : % 0.12/0.40 % SZS status Theorem % 0.12/0.40 (* PROOF-FOUND *) % 0.12/0.40 (* BEGIN-PROOF *) % 0.12/0.40 % SZS output start Proof % 0.12/0.40 1. (T_0 != (u (n (e)) (n (s (n (e)))))) (T_0 = (u (n (e)) (n (s (n (e)))))) ### Axiom % 0.12/0.40 2. (mem T_0 (s (u (n (e)) (n (s (n (e))))))) (T_0 != (u (n (e)) (n (s (n (e)))))) ### Extension/test/s_ax 1 % 0.12/0.40 3. (T_1 != T_1) ### Refl(=) % 0.12/0.40 4. (T_0 = (s (s (n (e))))) (T_0 != (s (s (n (e))))) ### Axiom % 0.12/0.40 5. (-. (mem T_1 (s (s (n (e)))))) (mem T_1 T_0) (T_0 = (s (s (n (e))))) ### P-NotP 3 4 % 0.12/0.40 6. (mem T_0 (s (s (s (n (e)))))) (mem T_1 T_0) (-. (mem T_1 (s (s (n (e)))))) ### Extension/test/s_ax 5 % 0.12/0.40 7. (-. (mem T_0 (n (s (n (n (e))))))) (mem T_0 (n (s (n (n (e)))))) ### Axiom % 0.12/0.40 8. (mem T_0 (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (-. (mem T_0 (n (s (n (n (e))))))) (-. (mem T_1 (s (s (n (e)))))) (mem T_1 T_0) ### Extension/test/u_ax 6 7 % 0.12/0.40 9. (mem T_0 (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e)))))))) (mem T_1 T_0) (-. (mem T_1 (s (s (n (e)))))) (-. (mem T_0 (n (s (n (n (e))))))) (T_0 != (u (n (e)) (n (s (n (e)))))) ### Extension/test/u_ax 2 8 % 0.12/0.40 10. (T_0 != (n (n (n (e))))) (T_0 = (n (n (n (e))))) ### Axiom % 0.12/0.40 11. (mem T_0 (s (n (n (n (e)))))) (T_0 != (n (n (n (e))))) ### Extension/test/s_ax 10 % 0.12/0.40 12. (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) (T_0 != (n (n (n (e))))) (T_0 != (u (n (e)) (n (s (n (e)))))) (-. (mem T_0 (n (s (n (n (e))))))) (-. (mem T_1 (s (s (n (e)))))) (mem T_1 T_0) ### Extension/test/u_ax 9 11 % 0.12/0.40 13. (-. (mem T_0 (s (n (n (n (e))))))) (mem T_1 T_0) (-. (mem T_1 (s (s (n (e)))))) (-. (mem T_0 (n (s (n (n (e))))))) (T_0 != (u (n (e)) (n (s (n (e)))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) ### Extension/test/not_s_ax 12 % 0.12/0.40 14. (-. (subq T_0 (s (s (n (e)))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) (T_0 != (u (n (e)) (n (s (n (e)))))) (-. (mem T_0 (n (s (n (n (e))))))) (-. (mem T_0 (s (n (n (n (e))))))) ### Extension/test/not_subq_def 13 % 0.12/0.40 15. (-. (mem T_0 (p (s (s (n (e))))))) (-. (mem T_0 (s (n (n (n (e))))))) (-. (mem T_0 (n (s (n (n (e))))))) (T_0 != (u (n (e)) (n (s (n (e)))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) ### Extension/test/not_p_ax 14 % 0.12/0.40 16. (-. (mem T_0 (u (p (s (s (n (e))))) (n (s (n (n (e)))))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) (T_0 != (u (n (e)) (n (s (n (e)))))) (-. (mem T_0 (s (n (n (n (e))))))) ### Extension/test/not_u_ax 15 % 0.12/0.40 17. (-. (mem T_0 (s (u (n (e)) (n (s (n (e)))))))) (-. (mem T_0 (s (n (n (n (e))))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) (-. (mem T_0 (u (p (s (s (n (e))))) (n (s (n (n (e)))))))) ### Extension/test/not_s_ax 16 % 0.12/0.40 18. (-. (mem T_0 (u (s (u (n (e)) (n (s (n (e)))))) (u (p (s (s (n (e))))) (n (s (n (n (e))))))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) (-. (mem T_0 (s (n (n (n (e))))))) ### Extension/test/not_u_ax 17 % 0.12/0.40 19. (-. (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (p (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e)))))))) (mem T_0 (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e))))))) ### Extension/test/not_u_ax 18 % 0.12/0.40 20. (-. (subq (u (u (s (u (n (e)) (n (s (n (e)))))) (u (s (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e)))))) (u (u (s (u (n (e)) (n (s (n (e)))))) (u (p (s (s (n (e))))) (n (s (n (n (e))))))) (s (n (n (n (e)))))))) ### Extension/test/not_subq_def 19 % 0.12/0.40 % SZS output end Proof % 0.12/0.40 (* END-PROOF *) %------------------------------------------------------------------------------