%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL488+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:36:01 AM UTC 2026 % Result : Theorem 18.06s 18.38s % Output : Proof 18.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL488+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : duper %s % 0.08/0.36 % Computer : n016.cluster.edu % 0.08/0.36 % Model : x86_64 x86_64 % 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.36 % Memory : 8046.5625MB % 0.08/0.36 % OS : Linux 6.8.0-71-generic % 0.08/0.36 % CPULimit : 300 % 0.08/0.36 % WCLimit : 300 % 0.08/0.36 % DateTime : Sat Sep 5 07:16:29 UTC 2026 % 0.14/0.36 % CPUTime : % 18.06/18.38 SZS status Theorem for theBenchmark.p % 18.06/18.38 SZS output start Proof for theBenchmark.p % 18.06/18.38 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 % 18.06/18.38 Clause #7 (by assumption #[]): Eq (Iff and_2 (∀ (X Y : Iota), is_a_theorem (implies (and X Y) Y))) True % 18.06/18.38 Clause #22 (by assumption #[]): Eq (Iff r2 (∀ (P Q : Iota), is_a_theorem (implies Q (or P Q)))) True % 18.06/18.38 Clause #23 (by assumption #[]): Eq (Iff r3 (∀ (P Q : Iota), is_a_theorem (implies (or P Q) (or Q P)))) True % 18.06/18.38 Clause #26 (by assumption #[]): Eq (op_or → ∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True % 18.06/18.38 Clause #27 (by assumption #[]): Eq (op_and → ∀ (X Y : Iota), Eq (and X Y) (not (or (not X) (not Y)))) True % 18.06/18.38 Clause #28 (by assumption #[]): Eq (op_implies_and → ∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True % 18.06/18.38 Clause #29 (by assumption #[]): Eq (op_implies_or → ∀ (X Y : Iota), Eq (implies X Y) (or (not X) Y)) True % 18.06/18.38 Clause #31 (by assumption #[]): Eq op_implies_or True % 18.06/18.38 Clause #32 (by assumption #[]): Eq op_and True % 18.06/18.38 Clause #34 (by assumption #[]): Eq modus_ponens True % 18.06/18.38 Clause #36 (by assumption #[]): Eq r2 True % 18.06/18.38 Clause #37 (by assumption #[]): Eq r3 True % 18.06/18.38 Clause #41 (by assumption #[]): Eq op_or True % 18.06/18.38 Clause #42 (by assumption #[]): Eq op_implies_and True % 18.06/18.38 Clause #43 (by assumption #[]): Eq (Not and_2) True % 18.06/18.38 Clause #45 (by clausification #[0]): Or (Eq modus_ponens False) % 18.06/18.38 (Eq (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y) True) % 18.06/18.38 Clause #64 (by clausification #[43]): Eq and_2 False % 18.06/18.38 Clause #65 (by clausification #[45]): ∀ (a : Iota), % 18.06/18.38 Or (Eq modus_ponens False) % 18.06/18.38 (Eq (∀ (Y : Iota), And (is_a_theorem a) (is_a_theorem (implies a Y)) → is_a_theorem Y) True) % 18.06/18.38 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), % 18.06/18.38 Or (Eq modus_ponens False) (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1)) → is_a_theorem a_1) True) % 18.06/18.38 Clause #67 (by clausification #[66]): ∀ (a a_1 : Iota), % 18.06/18.38 Or (Eq modus_ponens False) % 18.06/18.38 (Or (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1))) False) (Eq (is_a_theorem a_1) True)) % 18.06/18.38 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), % 18.06/18.38 Or (Eq modus_ponens False) % 18.06/18.38 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 18.06/18.38 Clause #69 (by forward demodulation #[68, 34]): ∀ (a a_1 : Iota), % 18.06/18.38 Or (Eq True False) % 18.06/18.38 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 18.06/18.38 Clause #70 (by clausification #[69]): ∀ (a a_1 : Iota), % 18.06/18.38 Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False)) % 18.06/18.38 Clause #121 (by clausification #[22]): Or (Eq r2 False) (Eq (∀ (P Q : Iota), is_a_theorem (implies Q (or P Q))) True) % 18.06/18.38 Clause #133 (by clausification #[121]): ∀ (a : Iota), Or (Eq r2 False) (Eq (∀ (Q : Iota), is_a_theorem (implies Q (or a Q))) True) % 18.06/18.38 Clause #134 (by clausification #[133]): ∀ (a a_1 : Iota), Or (Eq r2 False) (Eq (is_a_theorem (implies a (or a_1 a))) True) % 18.06/18.38 Clause #135 (by forward demodulation #[134, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (or a_1 a))) True) % 18.06/18.38 Clause #136 (by clausification #[135]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (or a_1 a))) True % 18.06/18.38 Clause #138 (by superposition #[136, 70]): ∀ (a a_1 a_2 : Iota), % 18.06/18.38 Or (Eq (is_a_theorem a) True) (Or (Eq True False) (Eq (is_a_theorem (implies (implies a_1 (or a_2 a_1)) a)) False)) % 18.06/18.38 Clause #141 (by clausification #[7]): Or (Eq and_2 True) (Eq (∀ (X Y : Iota), is_a_theorem (implies (and X Y) Y)) False) % 18.06/18.38 Clause #143 (by clausification #[141]): ∀ (a : Iota), Or (Eq and_2 True) (Eq (Not (∀ (Y : Iota), is_a_theorem (implies (and (skS.0 18 a) Y) Y))) True) % 18.06/18.38 Clause #144 (by clausification #[143]): ∀ (a : Iota), Or (Eq and_2 True) (Eq (∀ (Y : Iota), is_a_theorem (implies (and (skS.0 18 a) Y) Y)) False) % 18.06/18.38 Clause #145 (by clausification #[144]): ∀ (a a_1 : Iota), % 18.06/18.38 Or (Eq and_2 True) (Eq (Not (is_a_theorem (implies (and (skS.0 18 a) (skS.0 19 a a_1)) (skS.0 19 a a_1)))) True) % 18.16/18.40 Clause #146 (by clausification #[145]): ∀ (a a_1 : Iota), % 18.16/18.40 Or (Eq and_2 True) (Eq (is_a_theorem (implies (and (skS.0 18 a) (skS.0 19 a a_1)) (skS.0 19 a a_1))) False) % 18.16/18.40 Clause #147 (by forward demodulation #[146, 64]): ∀ (a a_1 : Iota), % 18.16/18.40 Or (Eq False True) (Eq (is_a_theorem (implies (and (skS.0 18 a) (skS.0 19 a a_1)) (skS.0 19 a a_1))) False) % 18.16/18.40 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (and (skS.0 18 a) (skS.0 19 a a_1)) (skS.0 19 a a_1))) False % 18.16/18.40 Clause #224 (by clausification #[29]): Or (Eq op_implies_or False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (or (not X) Y)) True) % 18.16/18.40 Clause #225 (by clausification #[224]): ∀ (a : Iota), Or (Eq op_implies_or False) (Eq (∀ (Y : Iota), Eq (implies a Y) (or (not a) Y)) True) % 18.16/18.40 Clause #226 (by clausification #[225]): ∀ (a a_1 : Iota), Or (Eq op_implies_or False) (Eq (Eq (implies a a_1) (or (not a) a_1)) True) % 18.16/18.40 Clause #227 (by clausification #[226]): ∀ (a a_1 : Iota), Or (Eq op_implies_or False) (Eq (implies a a_1) (or (not a) a_1)) % 18.16/18.40 Clause #228 (by forward demodulation #[227, 31]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (or (not a) a_1)) % 18.16/18.40 Clause #229 (by clausification #[228]): ∀ (a a_1 : Iota), Eq (implies a a_1) (or (not a) a_1) % 18.16/18.40 Clause #244 (by clausification #[23]): Or (Eq r3 False) (Eq (∀ (P Q : Iota), is_a_theorem (implies (or P Q) (or Q P))) True) % 18.16/18.40 Clause #250 (by clausification #[244]): ∀ (a : Iota), Or (Eq r3 False) (Eq (∀ (Q : Iota), is_a_theorem (implies (or a Q) (or Q a))) True) % 18.16/18.40 Clause #251 (by clausification #[250]): ∀ (a a_1 : Iota), Or (Eq r3 False) (Eq (is_a_theorem (implies (or a a_1) (or a_1 a))) True) % 18.16/18.40 Clause #252 (by forward demodulation #[251, 37]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (or a a_1) (or a_1 a))) True) % 18.16/18.40 Clause #253 (by clausification #[252]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a a_1) (or a_1 a))) True % 18.16/18.40 Clause #269 (by clausification #[28]): Or (Eq op_implies_and False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True) % 18.16/18.40 Clause #270 (by clausification #[269]): ∀ (a : Iota), Or (Eq op_implies_and False) (Eq (∀ (Y : Iota), Eq (implies a Y) (not (and a (not Y)))) True) % 18.16/18.40 Clause #271 (by clausification #[270]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (Eq (implies a a_1) (not (and a (not a_1)))) True) % 18.16/18.40 Clause #272 (by clausification #[271]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (implies a a_1) (not (and a (not a_1)))) % 18.16/18.40 Clause #273 (by forward demodulation #[272, 42]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (not (and a (not a_1)))) % 18.16/18.40 Clause #274 (by clausification #[273]): ∀ (a a_1 : Iota), Eq (implies a a_1) (not (and a (not a_1))) % 18.16/18.40 Clause #365 (by clausification #[26]): Or (Eq op_or False) (Eq (∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True) % 18.16/18.40 Clause #366 (by clausification #[365]): ∀ (a : Iota), Or (Eq op_or False) (Eq (∀ (Y : Iota), Eq (or a Y) (not (and (not a) (not Y)))) True) % 18.16/18.40 Clause #367 (by clausification #[366]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (Eq (or a a_1) (not (and (not a) (not a_1)))) True) % 18.16/18.40 Clause #368 (by clausification #[367]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 18.16/18.40 Clause #369 (by forward demodulation #[368, 41]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 18.16/18.40 Clause #370 (by clausification #[369]): ∀ (a a_1 : Iota), Eq (or a a_1) (not (and (not a) (not a_1))) % 18.16/18.40 Clause #371 (by superposition #[370, 274]): ∀ (a a_1 : Iota), Eq (implies (not a) a_1) (or a a_1) % 18.16/18.40 Clause #425 (by clausification #[27]): Or (Eq op_and False) (Eq (∀ (X Y : Iota), Eq (and X Y) (not (or (not X) (not Y)))) True) % 18.16/18.40 Clause #426 (by clausification #[425]): ∀ (a : Iota), Or (Eq op_and False) (Eq (∀ (Y : Iota), Eq (and a Y) (not (or (not a) (not Y)))) True) % 18.16/18.40 Clause #427 (by clausification #[426]): ∀ (a a_1 : Iota), Or (Eq op_and False) (Eq (Eq (and a a_1) (not (or (not a) (not a_1)))) True) % 18.16/18.40 Clause #428 (by clausification #[427]): ∀ (a a_1 : Iota), Or (Eq op_and False) (Eq (and a a_1) (not (or (not a) (not a_1)))) % 18.16/18.44 Clause #429 (by forward demodulation #[428, 32]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (and a a_1) (not (or (not a) (not a_1)))) % 18.16/18.44 Clause #430 (by clausification #[429]): ∀ (a a_1 : Iota), Eq (and a a_1) (not (or (not a) (not a_1))) % 18.16/18.44 Clause #431 (by forward demodulation #[430, 229]): ∀ (a a_1 : Iota), Eq (and a a_1) (not (implies a (not a_1))) % 18.16/18.44 Clause #446 (by superposition #[431, 371]): ∀ (a a_1 a_2 : Iota), Eq (implies (and a a_1) a_2) (or (implies a (not a_1)) a_2) % 18.16/18.44 Clause #678 (by clausification #[138]): ∀ (a a_1 a_2 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 (or a_2 a_1)) a)) False) % 18.16/18.44 Clause #690 (by superposition #[678, 229]): ∀ (a a_1 a_2 : Iota), % 18.16/18.44 Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 (implies a_2 a_1)) a)) False) % 18.16/18.44 Clause #841 (by superposition #[690, 371]): ∀ (a a_1 a_2 : Iota), % 18.16/18.44 Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (or a_1 (implies a_2 (not a_1))) a)) False) % 18.16/18.44 Clause #6365 (by superposition #[841, 253]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (or (implies a (not a_1)) a_1)) True) (Eq False True) % 18.16/18.44 Clause #6405 (by clausification #[6365]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (implies a (not a_1)) a_1)) True % 18.16/18.44 Clause #6406 (by forward demodulation #[6405, 446]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (and a a_1) a_1)) True % 18.16/18.44 Clause #6407 (by superposition #[6406, 148]): Eq True False % 18.16/18.44 Clause #6415 (by clausification #[6407]): False % 18.16/18.44 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------