%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : LCL459+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 01:32:18 PM UTC 2026 % Result : Theorem 0.14s 41.82s % Output : Proof 0.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL459+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.03 % Command : run_zenon %s %d % 0.09/0.35 % Computer : n020.cluster.edu % 0.09/0.35 % Model : x86_64 x86_64 % 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.35 % Memory : 8046.5625MB % 0.09/0.35 % OS : Linux 6.8.0-71-generic % 0.09/0.35 % CPULimit : 300 % 0.09/0.35 % WCLimit : 300 % 0.09/0.35 % DateTime : Fri Sep 4 14:30:42 UTC 2026 % 0.09/0.35 % CPUTime : % 0.14/41.82 (* PROOF-FOUND *) % 0.14/41.82 % SZS status Theorem % 0.14/41.82 (* BEGIN-PROOF *) % 0.14/41.82 % SZS output start Proof % 0.14/41.82 Theorem rosser_kn1 : (kn1). % 0.14/41.82 Proof. % 0.14/41.82 apply NNPP. intro zenon_G. % 0.14/41.82 apply (zenon_equiv_s _ _ modus_ponens); [ zenon_intro zenon_H34; zenon_intro zenon_H33 | zenon_intro hilbert_modus_ponens; zenon_intro zenon_H32 ]. % 0.14/41.82 exact (zenon_H34 hilbert_modus_ponens). % 0.14/41.82 apply (zenon_equiv_s _ _ implies_2); [ zenon_intro zenon_H37; zenon_intro zenon_H36 | zenon_intro hilbert_implies_2; zenon_intro zenon_H35 ]. % 0.14/41.82 exact (zenon_H37 hilbert_implies_2). % 0.14/41.82 apply (zenon_equiv_s _ _ and_3); [ zenon_intro zenon_H3a; zenon_intro zenon_H39 | zenon_intro hilbert_and_3; zenon_intro zenon_H38 ]. % 0.14/41.82 exact (zenon_H3a hilbert_and_3). % 0.14/41.82 apply (zenon_equiv_s _ _ kn1); [ zenon_intro zenon_G; zenon_intro zenon_H3d | zenon_intro zenon_H3c; zenon_intro zenon_H3b ]. % 0.14/41.82 apply (zenon_notallex_s (fun P : zenon_U => (is_a_theorem (implies P (and P P)))) zenon_H3d); [ zenon_intro zenon_H3e; idtac ]. % 0.14/41.82 elim zenon_H3e. zenon_intro zenon_TP_cl. zenon_intro zenon_H40. % 0.14/41.82 generalize (zenon_H38 zenon_TP_cl). zenon_intro zenon_H41. % 0.14/41.82 generalize (zenon_H41 zenon_TP_cl). zenon_intro zenon_H42. % 0.14/41.82 generalize (zenon_H35 zenon_TP_cl). zenon_intro zenon_H43. % 0.14/41.82 generalize (zenon_H43 (and zenon_TP_cl zenon_TP_cl)). zenon_intro zenon_H44. % 0.14/41.82 generalize (zenon_H32 (implies zenon_TP_cl (implies zenon_TP_cl (and zenon_TP_cl zenon_TP_cl)))). zenon_intro zenon_H45. % 0.14/41.82 generalize (zenon_H45 (implies zenon_TP_cl (and zenon_TP_cl zenon_TP_cl))). zenon_intro zenon_H46. % 0.14/41.82 apply (zenon_imply_s _ _ zenon_H46); [ zenon_intro zenon_H48 | zenon_intro zenon_H47 ]. % 0.14/41.82 apply (zenon_notand_s _ _ zenon_H48); [ zenon_intro zenon_H4a | zenon_intro zenon_H49 ]. % 0.14/41.82 exact (zenon_H4a zenon_H42). % 0.14/41.82 exact (zenon_H49 zenon_H44). % 0.14/41.82 exact (zenon_H40 zenon_H47). % 0.14/41.82 exact (zenon_G zenon_H3c). % 0.14/41.82 Qed. % 0.14/41.82 % SZS output end Proof % 0.14/41.82 (* END-PROOF *) % 0.14/41.82 nodes searched: 86910 % 0.14/41.82 max branch formulas: 50440 % 0.14/41.82 proof nodes created: 1519 % 0.14/41.82 formulas created: 647984 % 0.14/41.82 %------------------------------------------------------------------------------