%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL538+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n028.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:36:05 AM UTC 2026 % Result : Theorem 175.49s 175.85s % Output : Proof 175.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL538+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : duper %s % 0.09/0.35 % Computer : n028.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 : Sat Sep 5 05:42:44 UTC 2026 % 0.09/0.36 % CPUTime : % 175.49/175.85 SZS status Theorem for theBenchmark.p % 175.49/175.85 SZS output start Proof for theBenchmark.p % 175.49/175.85 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 % 175.49/175.85 Clause #34 (by assumption #[]): Eq modus_ponens True % 175.49/175.85 Clause #50 (by assumption #[]): Eq % 175.49/175.85 (Iff modus_ponens_strict_implies % 175.49/175.85 (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (strict_implies X Y)) → is_a_theorem Y)) % 175.49/175.85 True % 175.49/175.85 Clause #54 (by assumption #[]): Eq (Iff axiom_M (∀ (X : Iota), is_a_theorem (implies (necessarily X) X))) True % 175.49/175.85 Clause #74 (by assumption #[]): Eq (op_strict_implies → ∀ (X Y : Iota), Eq (strict_implies X Y) (necessarily (implies X Y))) True % 175.49/175.85 Clause #79 (by assumption #[]): Eq axiom_M True % 175.49/175.85 Clause #83 (by assumption #[]): Eq op_strict_implies True % 175.49/175.85 Clause #85 (by assumption #[]): Eq (Not modus_ponens_strict_implies) True % 175.49/175.85 Clause #87 (by clausification #[0]): Or (Eq modus_ponens False) % 175.49/175.85 (Eq (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y) True) % 175.49/175.86 Clause #127 (by clausification #[85]): Eq modus_ponens_strict_implies False % 175.49/175.86 Clause #128 (by clausification #[87]): ∀ (a : Iota), % 175.49/175.86 Or (Eq modus_ponens False) % 175.49/175.86 (Eq (∀ (Y : Iota), And (is_a_theorem a) (is_a_theorem (implies a Y)) → is_a_theorem Y) True) % 175.49/175.86 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens False) (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1)) → is_a_theorem a_1) True) % 175.49/175.86 Clause #130 (by clausification #[129]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens False) % 175.49/175.86 (Or (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1))) False) (Eq (is_a_theorem a_1) True)) % 175.49/175.86 Clause #131 (by clausification #[130]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens False) % 175.49/175.86 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 175.49/175.86 Clause #132 (by forward demodulation #[131, 34]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq True False) % 175.49/175.86 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 175.49/175.86 Clause #133 (by clausification #[132]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False)) % 175.49/175.86 Clause #154 (by clausification #[50]): Or (Eq modus_ponens_strict_implies True) % 175.49/175.86 (Eq (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (strict_implies X Y)) → is_a_theorem Y) False) % 175.49/175.86 Clause #156 (by clausification #[154]): ∀ (a : Iota), % 175.49/175.86 Or (Eq modus_ponens_strict_implies True) % 175.49/175.86 (Eq % 175.49/175.86 (Not % 175.49/175.86 (∀ (Y : Iota), And (is_a_theorem (skS.0 14 a)) (is_a_theorem (strict_implies (skS.0 14 a) Y)) → is_a_theorem Y)) % 175.49/175.86 True) % 175.49/175.86 Clause #157 (by clausification #[156]): ∀ (a : Iota), % 175.49/175.86 Or (Eq modus_ponens_strict_implies True) % 175.49/175.86 (Eq (∀ (Y : Iota), And (is_a_theorem (skS.0 14 a)) (is_a_theorem (strict_implies (skS.0 14 a) Y)) → is_a_theorem Y) % 175.49/175.86 False) % 175.49/175.86 Clause #158 (by clausification #[157]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens_strict_implies True) % 175.49/175.86 (Eq % 175.49/175.86 (Not % 175.49/175.86 (And (is_a_theorem (skS.0 14 a)) (is_a_theorem (strict_implies (skS.0 14 a) (skS.0 15 a a_1))) → % 175.49/175.86 is_a_theorem (skS.0 15 a a_1))) % 175.49/175.86 True) % 175.49/175.86 Clause #159 (by clausification #[158]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens_strict_implies True) % 175.49/175.86 (Eq % 175.49/175.86 (And (is_a_theorem (skS.0 14 a)) (is_a_theorem (strict_implies (skS.0 14 a) (skS.0 15 a a_1))) → % 175.49/175.86 is_a_theorem (skS.0 15 a a_1)) % 175.49/175.86 False) % 175.49/175.86 Clause #160 (by clausification #[159]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens_strict_implies True) % 175.49/175.86 (Eq (And (is_a_theorem (skS.0 14 a)) (is_a_theorem (strict_implies (skS.0 14 a) (skS.0 15 a a_1)))) True) % 175.49/175.86 Clause #161 (by clausification #[159]): ∀ (a a_1 : Iota), Or (Eq modus_ponens_strict_implies True) (Eq (is_a_theorem (skS.0 15 a a_1)) False) % 175.49/175.86 Clause #162 (by clausification #[160]): ∀ (a a_1 : Iota), % 175.49/175.86 Or (Eq modus_ponens_strict_implies True) (Eq (is_a_theorem (strict_implies (skS.0 14 a) (skS.0 15 a a_1))) True) % 175.49/175.86 Clause #163 (by clausification #[160]): ∀ (a : Iota), Or (Eq modus_ponens_strict_implies True) (Eq (is_a_theorem (skS.0 14 a)) True) % 175.58/176.01 Clause #164 (by forward demodulation #[162, 127]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (is_a_theorem (strict_implies (skS.0 14 a) (skS.0 15 a a_1))) True) % 175.58/176.01 Clause #165 (by clausification #[164]): ∀ (a a_1 : Iota), Eq (is_a_theorem (strict_implies (skS.0 14 a) (skS.0 15 a a_1))) True % 175.58/176.01 Clause #166 (by superposition #[165, 133]): ∀ (a a_1 a_2 : Iota), % 175.58/176.01 Or (Eq (is_a_theorem a) True) % 175.58/176.01 (Or (Eq True False) (Eq (is_a_theorem (implies (strict_implies (skS.0 14 a_1) (skS.0 15 a_1 a_2)) a)) False)) % 175.58/176.01 Clause #174 (by clausification #[54]): Or (Eq axiom_M False) (Eq (∀ (X : Iota), is_a_theorem (implies (necessarily X) X)) True) % 175.58/176.01 Clause #178 (by clausification #[174]): ∀ (a : Iota), Or (Eq axiom_M False) (Eq (is_a_theorem (implies (necessarily a) a)) True) % 175.58/176.01 Clause #179 (by forward demodulation #[178, 79]): ∀ (a : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (necessarily a) a)) True) % 175.58/176.01 Clause #180 (by clausification #[179]): ∀ (a : Iota), Eq (is_a_theorem (implies (necessarily a) a)) True % 175.58/176.01 Clause #265 (by forward demodulation #[163, 127]): ∀ (a : Iota), Or (Eq False True) (Eq (is_a_theorem (skS.0 14 a)) True) % 175.58/176.01 Clause #266 (by clausification #[265]): ∀ (a : Iota), Eq (is_a_theorem (skS.0 14 a)) True % 175.58/176.01 Clause #267 (by superposition #[266, 133]): ∀ (a a_1 : Iota), % 175.58/176.01 Or (Eq (is_a_theorem a) True) (Or (Eq True False) (Eq (is_a_theorem (implies (skS.0 14 a_1) a)) False)) % 175.58/176.01 Clause #623 (by forward demodulation #[161, 127]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (is_a_theorem (skS.0 15 a a_1)) False) % 175.58/176.01 Clause #624 (by clausification #[623]): ∀ (a a_1 : Iota), Eq (is_a_theorem (skS.0 15 a a_1)) False % 175.58/176.01 Clause #1053 (by clausification #[74]): Or (Eq op_strict_implies False) (Eq (∀ (X Y : Iota), Eq (strict_implies X Y) (necessarily (implies X Y))) True) % 175.58/176.01 Clause #1054 (by clausification #[1053]): ∀ (a : Iota), % 175.58/176.01 Or (Eq op_strict_implies False) (Eq (∀ (Y : Iota), Eq (strict_implies a Y) (necessarily (implies a Y))) True) % 175.58/176.01 Clause #1055 (by clausification #[1054]): ∀ (a a_1 : Iota), Or (Eq op_strict_implies False) (Eq (Eq (strict_implies a a_1) (necessarily (implies a a_1))) True) % 175.58/176.01 Clause #1056 (by clausification #[1055]): ∀ (a a_1 : Iota), Or (Eq op_strict_implies False) (Eq (strict_implies a a_1) (necessarily (implies a a_1))) % 175.58/176.01 Clause #1057 (by forward demodulation #[1056, 83]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (strict_implies a a_1) (necessarily (implies a a_1))) % 175.58/176.01 Clause #1058 (by clausification #[1057]): ∀ (a a_1 : Iota), Eq (strict_implies a a_1) (necessarily (implies a a_1)) % 175.58/176.01 Clause #1089 (by superposition #[1058, 180]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (strict_implies a a_1) (implies a a_1))) True % 175.58/176.01 Clause #1276 (by clausification #[166]): ∀ (a a_1 a_2 : Iota), % 175.58/176.01 Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (strict_implies (skS.0 14 a_1) (skS.0 15 a_1 a_2)) a)) False) % 175.58/176.01 Clause #1283 (by superposition #[1276, 1089]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (implies (skS.0 14 a) (skS.0 15 a a_1))) True) (Eq False True) % 175.58/176.01 Clause #1504 (by clausification #[267]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (skS.0 14 a_1) a)) False) % 175.58/176.01 Clause #20047 (by clausification #[1283]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (skS.0 14 a) (skS.0 15 a a_1))) True % 175.58/176.01 Clause #20048 (by superposition #[20047, 1504]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (skS.0 15 a a_1)) True) (Eq True False) % 175.58/176.01 Clause #20133 (by clausification #[20048]): ∀ (a a_1 : Iota), Eq (is_a_theorem (skS.0 15 a a_1)) True % 175.58/176.01 Clause #20134 (by superposition #[20133, 624]): Eq True False % 175.58/176.01 Clause #20137 (by clausification #[20134]): False % 175.58/176.01 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------