%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL469+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.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:00 AM UTC 2026 % Result : Theorem 9.67s 9.91s % Output : Proof 9.67s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL469+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.05 % Command : duper %s % 0.10/0.37 % Computer : n018.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Fri Sep 4 18:45:48 UTC 2026 % 0.10/0.37 % CPUTime : % 9.67/9.91 SZS status Theorem for theBenchmark.p % 9.67/9.91 SZS output start Proof for theBenchmark.p % 9.67/9.91 Clause #9 (by assumption #[]): Eq (Iff or_1 (∀ (X Y : Iota), is_a_theorem (implies X (or X Y)))) True % 9.67/9.91 Clause #19 (by assumption #[]): Eq (Iff cn2 (∀ (P Q : Iota), is_a_theorem (implies P (implies (not P) Q)))) True % 9.67/9.91 Clause #26 (by assumption #[]): Eq (op_or → ∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True % 9.67/9.91 Clause #28 (by assumption #[]): Eq (op_implies_and → ∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True % 9.67/9.91 Clause #31 (by assumption #[]): Eq op_or True % 9.67/9.91 Clause #36 (by assumption #[]): Eq cn2 True % 9.67/9.91 Clause #39 (by assumption #[]): Eq op_implies_and True % 9.67/9.91 Clause #40 (by assumption #[]): Eq (Not or_1) True % 9.67/9.91 Clause #52 (by clausification #[40]): Eq or_1 False % 9.67/9.91 Clause #137 (by clausification #[9]): Or (Eq or_1 True) (Eq (∀ (X Y : Iota), is_a_theorem (implies X (or X Y))) False) % 9.67/9.91 Clause #139 (by clausification #[137]): ∀ (a : Iota), Or (Eq or_1 True) (Eq (Not (∀ (Y : Iota), is_a_theorem (implies (skS.0 21 a) (or (skS.0 21 a) Y)))) True) % 9.67/9.91 Clause #140 (by clausification #[139]): ∀ (a : Iota), Or (Eq or_1 True) (Eq (∀ (Y : Iota), is_a_theorem (implies (skS.0 21 a) (or (skS.0 21 a) Y))) False) % 9.67/9.91 Clause #141 (by clausification #[140]): ∀ (a a_1 : Iota), % 9.67/9.91 Or (Eq or_1 True) (Eq (Not (is_a_theorem (implies (skS.0 21 a) (or (skS.0 21 a) (skS.0 22 a a_1))))) True) % 9.67/9.91 Clause #142 (by clausification #[141]): ∀ (a a_1 : Iota), Or (Eq or_1 True) (Eq (is_a_theorem (implies (skS.0 21 a) (or (skS.0 21 a) (skS.0 22 a a_1)))) False) % 9.67/9.91 Clause #143 (by forward demodulation #[142, 52]): ∀ (a a_1 : Iota), Or (Eq False True) (Eq (is_a_theorem (implies (skS.0 21 a) (or (skS.0 21 a) (skS.0 22 a a_1)))) False) % 9.67/9.91 Clause #144 (by clausification #[143]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (skS.0 21 a) (or (skS.0 21 a) (skS.0 22 a a_1)))) False % 9.67/9.91 Clause #180 (by clausification #[19]): Or (Eq cn2 False) (Eq (∀ (P Q : Iota), is_a_theorem (implies P (implies (not P) Q))) True) % 9.67/9.91 Clause #186 (by clausification #[180]): ∀ (a : Iota), Or (Eq cn2 False) (Eq (∀ (Q : Iota), is_a_theorem (implies a (implies (not a) Q))) True) % 9.67/9.91 Clause #187 (by clausification #[186]): ∀ (a a_1 : Iota), Or (Eq cn2 False) (Eq (is_a_theorem (implies a (implies (not a) a_1))) True) % 9.67/9.91 Clause #188 (by forward demodulation #[187, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (implies (not a) a_1))) True) % 9.67/9.91 Clause #189 (by clausification #[188]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (implies (not a) a_1))) True % 9.67/9.91 Clause #236 (by clausification #[28]): Or (Eq op_implies_and False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True) % 9.67/9.91 Clause #237 (by clausification #[236]): ∀ (a : Iota), Or (Eq op_implies_and False) (Eq (∀ (Y : Iota), Eq (implies a Y) (not (and a (not Y)))) True) % 9.67/9.91 Clause #238 (by clausification #[237]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (Eq (implies a a_1) (not (and a (not a_1)))) True) % 9.67/9.91 Clause #239 (by clausification #[238]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (implies a a_1) (not (and a (not a_1)))) % 9.67/9.91 Clause #240 (by forward demodulation #[239, 39]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (not (and a (not a_1)))) % 9.67/9.91 Clause #241 (by clausification #[240]): ∀ (a a_1 : Iota), Eq (implies a a_1) (not (and a (not a_1))) % 9.67/9.91 Clause #277 (by clausification #[26]): Or (Eq op_or False) (Eq (∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True) % 9.67/9.91 Clause #278 (by clausification #[277]): ∀ (a : Iota), Or (Eq op_or False) (Eq (∀ (Y : Iota), Eq (or a Y) (not (and (not a) (not Y)))) True) % 9.67/9.91 Clause #279 (by clausification #[278]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (Eq (or a a_1) (not (and (not a) (not a_1)))) True) % 9.67/9.91 Clause #280 (by clausification #[279]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 9.67/9.91 Clause #281 (by forward demodulation #[280, 31]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 9.67/9.91 Clause #282 (by clausification #[281]): ∀ (a a_1 : Iota), Eq (or a a_1) (not (and (not a) (not a_1))) % 9.67/9.92 Clause #283 (by superposition #[282, 241]): ∀ (a a_1 : Iota), Eq (implies (not a) a_1) (or a a_1) % 9.67/9.92 Clause #299 (by backward demodulation #[283, 189]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (or a a_1))) True % 9.67/9.92 Clause #303 (by superposition #[299, 144]): Eq True False % 9.67/9.92 Clause #306 (by clausification #[303]): False % 9.67/9.92 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------