%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL459+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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 11:35:59 AM UTC 2026 % Result : Theorem 13.27s 13.55s % Output : Proof 13.27s % 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.04 % Command : duper %s % 0.10/0.35 % Computer : n016.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Fri Sep 4 14:34:28 UTC 2026 % 0.10/0.35 % CPUTime : % 13.27/13.55 SZS status Theorem for theBenchmark.p % 13.27/13.55 SZS output start Proof for theBenchmark.p % 13.27/13.55 Clause #0 (by assumption #[]): Eq (Iff modus_ponens (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y)) True % 13.27/13.55 Clause #4 (by assumption #[]): Eq (Iff implies_2 (∀ (X Y : Iota), is_a_theorem (implies (implies X (implies X Y)) (implies X Y)))) True % 13.27/13.55 Clause #8 (by assumption #[]): Eq (Iff and_3 (∀ (X Y : Iota), is_a_theorem (implies X (implies Y (and X Y))))) True % 13.27/13.55 Clause #15 (by assumption #[]): Eq (Iff kn1 (∀ (P : Iota), is_a_theorem (implies P (and P P)))) True % 13.27/13.55 Clause #34 (by assumption #[]): Eq modus_ponens True % 13.27/13.55 Clause #37 (by assumption #[]): Eq implies_2 True % 13.27/13.55 Clause #41 (by assumption #[]): Eq and_3 True % 13.27/13.55 Clause #49 (by assumption #[]): Eq (Not kn1) True % 13.27/13.55 Clause #51 (by clausification #[0]): Or (Eq modus_ponens False) % 13.27/13.55 (Eq (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y) True) % 13.27/13.55 Clause #77 (by clausification #[49]): Eq kn1 False % 13.27/13.55 Clause #78 (by clausification #[51]): ∀ (a : Iota), % 13.27/13.55 Or (Eq modus_ponens False) % 13.27/13.55 (Eq (∀ (Y : Iota), And (is_a_theorem a) (is_a_theorem (implies a Y)) → is_a_theorem Y) True) % 13.27/13.55 Clause #79 (by clausification #[78]): ∀ (a a_1 : Iota), % 13.27/13.55 Or (Eq modus_ponens False) (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1)) → is_a_theorem a_1) True) % 13.27/13.55 Clause #80 (by clausification #[79]): ∀ (a a_1 : Iota), % 13.27/13.55 Or (Eq modus_ponens False) % 13.27/13.55 (Or (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1))) False) (Eq (is_a_theorem a_1) True)) % 13.27/13.55 Clause #81 (by clausification #[80]): ∀ (a a_1 : Iota), % 13.27/13.55 Or (Eq modus_ponens False) % 13.27/13.55 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 13.27/13.55 Clause #82 (by forward demodulation #[81, 34]): ∀ (a a_1 : Iota), % 13.27/13.55 Or (Eq True False) % 13.27/13.55 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 13.27/13.55 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), % 13.27/13.55 Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False)) % 13.27/13.55 Clause #96 (by clausification #[15]): Or (Eq kn1 True) (Eq (∀ (P : Iota), is_a_theorem (implies P (and P P))) False) % 13.27/13.55 Clause #98 (by clausification #[96]): ∀ (a : Iota), Or (Eq kn1 True) (Eq (Not (is_a_theorem (implies (skS.0 9 a) (and (skS.0 9 a) (skS.0 9 a))))) True) % 13.27/13.55 Clause #99 (by clausification #[98]): ∀ (a : Iota), Or (Eq kn1 True) (Eq (is_a_theorem (implies (skS.0 9 a) (and (skS.0 9 a) (skS.0 9 a)))) False) % 13.27/13.55 Clause #100 (by forward demodulation #[99, 77]): ∀ (a : Iota), Or (Eq False True) (Eq (is_a_theorem (implies (skS.0 9 a) (and (skS.0 9 a) (skS.0 9 a)))) False) % 13.27/13.55 Clause #101 (by clausification #[100]): ∀ (a : Iota), Eq (is_a_theorem (implies (skS.0 9 a) (and (skS.0 9 a) (skS.0 9 a)))) False % 13.27/13.55 Clause #111 (by clausification #[4]): Or (Eq implies_2 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies (implies X (implies X Y)) (implies X Y))) True) % 13.27/13.55 Clause #175 (by clausification #[8]): Or (Eq and_3 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies X (implies Y (and X Y)))) True) % 13.27/13.55 Clause #255 (by clausification #[175]): ∀ (a : Iota), Or (Eq and_3 False) (Eq (∀ (Y : Iota), is_a_theorem (implies a (implies Y (and a Y)))) True) % 13.27/13.55 Clause #256 (by clausification #[255]): ∀ (a a_1 : Iota), Or (Eq and_3 False) (Eq (is_a_theorem (implies a (implies a_1 (and a a_1)))) True) % 13.27/13.55 Clause #257 (by forward demodulation #[256, 41]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (implies a_1 (and a a_1)))) True) % 13.27/13.55 Clause #258 (by clausification #[257]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (implies a_1 (and a a_1)))) True % 13.27/13.55 Clause #259 (by superposition #[258, 83]): ∀ (a a_1 a_2 : Iota), % 13.27/13.55 Or (Eq (is_a_theorem a) True) % 13.27/13.55 (Or (Eq True False) (Eq (is_a_theorem (implies (implies a_1 (implies a_2 (and a_1 a_2))) a)) False)) % 13.27/13.55 Clause #550 (by clausification #[111]): ∀ (a : Iota), % 13.27/13.55 Or (Eq implies_2 False) (Eq (∀ (Y : Iota), is_a_theorem (implies (implies a (implies a Y)) (implies a Y))) True) % 13.27/13.55 Clause #551 (by clausification #[550]): ∀ (a a_1 : Iota), Or (Eq implies_2 False) (Eq (is_a_theorem (implies (implies a (implies a a_1)) (implies a a_1))) True) % 13.27/13.56 Clause #552 (by forward demodulation #[551, 37]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (implies a (implies a a_1)) (implies a a_1))) True) % 13.27/13.56 Clause #553 (by clausification #[552]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (implies a (implies a a_1)) (implies a a_1))) True % 13.27/13.56 Clause #775 (by clausification #[259]): ∀ (a a_1 a_2 : Iota), % 13.27/13.56 Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 (implies a_2 (and a_1 a_2))) a)) False) % 13.27/13.56 Clause #784 (by superposition #[775, 553]): ∀ (a : Iota), Or (Eq (is_a_theorem (implies a (and a a))) True) (Eq False True) % 13.27/13.56 Clause #793 (by clausification #[784]): ∀ (a : Iota), Eq (is_a_theorem (implies a (and a a))) True % 13.27/13.56 Clause #794 (by superposition #[793, 101]): Eq True False % 13.27/13.56 Clause #805 (by clausification #[794]): False % 13.27/13.56 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------