%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL452+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n027.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:58 AM UTC 2026 % Result : Theorem 54.45s 54.73s % Output : Proof 54.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL452+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.05 % Command : duper %s % 0.09/0.36 % Computer : n027.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 5 01:07:13 UTC 2026 % 0.09/0.36 % CPUTime : % 54.45/54.73 SZS status Theorem for theBenchmark.p % 54.45/54.73 SZS output start Proof for theBenchmark.p % 54.45/54.73 Clause #9 (by assumption #[]): Eq (Iff or_1 (∀ (X Y : Iota), is_a_theorem (implies X (or X Y)))) True % 54.45/54.73 Clause #19 (by assumption #[]): Eq (Iff cn2 (∀ (P Q : Iota), is_a_theorem (implies P (implies (not P) Q)))) True % 54.45/54.73 Clause #26 (by assumption #[]): Eq (op_or → ∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True % 54.45/54.73 Clause #28 (by assumption #[]): Eq (op_implies_and → ∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True % 54.45/54.73 Clause #31 (by assumption #[]): Eq op_or True % 54.45/54.73 Clause #32 (by assumption #[]): Eq op_implies_and True % 54.45/54.73 Clause #42 (by assumption #[]): Eq or_1 True % 54.45/54.73 Clause #50 (by assumption #[]): Eq (Not cn2) True % 54.45/54.73 Clause #78 (by clausification #[50]): Eq cn2 False % 54.45/54.73 Clause #196 (by clausification #[9]): Or (Eq or_1 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies X (or X Y))) True) % 54.45/54.73 Clause #202 (by clausification #[196]): ∀ (a : Iota), Or (Eq or_1 False) (Eq (∀ (Y : Iota), is_a_theorem (implies a (or a Y))) True) % 54.45/54.73 Clause #203 (by clausification #[202]): ∀ (a a_1 : Iota), Or (Eq or_1 False) (Eq (is_a_theorem (implies a (or a a_1))) True) % 54.45/54.73 Clause #204 (by forward demodulation #[203, 42]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (or a a_1))) True) % 54.45/54.73 Clause #205 (by clausification #[204]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (or a a_1))) True % 54.45/54.73 Clause #212 (by clausification #[19]): Or (Eq cn2 True) (Eq (∀ (P Q : Iota), is_a_theorem (implies P (implies (not P) Q))) False) % 54.45/54.73 Clause #214 (by clausification #[212]): ∀ (a : Iota), % 54.45/54.73 Or (Eq cn2 True) (Eq (Not (∀ (Q : Iota), is_a_theorem (implies (skS.0 30 a) (implies (not (skS.0 30 a)) Q)))) True) % 54.45/54.73 Clause #215 (by clausification #[214]): ∀ (a : Iota), % 54.45/54.73 Or (Eq cn2 True) (Eq (∀ (Q : Iota), is_a_theorem (implies (skS.0 30 a) (implies (not (skS.0 30 a)) Q))) False) % 54.45/54.73 Clause #216 (by clausification #[215]): ∀ (a a_1 : Iota), % 54.45/54.73 Or (Eq cn2 True) (Eq (Not (is_a_theorem (implies (skS.0 30 a) (implies (not (skS.0 30 a)) (skS.0 31 a a_1))))) True) % 54.45/54.73 Clause #217 (by clausification #[216]): ∀ (a a_1 : Iota), % 54.45/54.73 Or (Eq cn2 True) (Eq (is_a_theorem (implies (skS.0 30 a) (implies (not (skS.0 30 a)) (skS.0 31 a a_1)))) False) % 54.45/54.73 Clause #218 (by forward demodulation #[217, 78]): ∀ (a a_1 : Iota), % 54.45/54.73 Or (Eq False True) (Eq (is_a_theorem (implies (skS.0 30 a) (implies (not (skS.0 30 a)) (skS.0 31 a a_1)))) False) % 54.45/54.73 Clause #219 (by clausification #[218]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (skS.0 30 a) (implies (not (skS.0 30 a)) (skS.0 31 a a_1)))) False % 54.45/54.73 Clause #388 (by clausification #[26]): Or (Eq op_or False) (Eq (∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True) % 54.45/54.73 Clause #389 (by clausification #[388]): ∀ (a : Iota), Or (Eq op_or False) (Eq (∀ (Y : Iota), Eq (or a Y) (not (and (not a) (not Y)))) True) % 54.45/54.73 Clause #390 (by clausification #[389]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (Eq (or a a_1) (not (and (not a) (not a_1)))) True) % 54.45/54.73 Clause #391 (by clausification #[390]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 54.45/54.73 Clause #392 (by forward demodulation #[391, 31]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 54.45/54.73 Clause #393 (by clausification #[392]): ∀ (a a_1 : Iota), Eq (or a a_1) (not (and (not a) (not a_1))) % 54.45/54.73 Clause #433 (by clausification #[28]): Or (Eq op_implies_and False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True) % 54.45/54.73 Clause #434 (by clausification #[433]): ∀ (a : Iota), Or (Eq op_implies_and False) (Eq (∀ (Y : Iota), Eq (implies a Y) (not (and a (not Y)))) True) % 54.45/54.73 Clause #435 (by clausification #[434]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (Eq (implies a a_1) (not (and a (not a_1)))) True) % 54.45/54.73 Clause #436 (by clausification #[435]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (implies a a_1) (not (and a (not a_1)))) % 54.45/54.73 Clause #437 (by forward demodulation #[436, 32]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (not (and a (not a_1)))) % 54.45/54.73 Clause #438 (by clausification #[437]): ∀ (a a_1 : Iota), Eq (implies a a_1) (not (and a (not a_1))) % 54.45/54.79 Clause #439 (by superposition #[438, 393]): ∀ (a a_1 : Iota), Eq (or a a_1) (implies (not a) a_1) % 54.45/54.79 Clause #472 (by backward demodulation #[439, 219]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (skS.0 30 a) (or (skS.0 30 a) (skS.0 31 a a_1)))) False % 54.45/54.79 Clause #5809 (by superposition #[472, 205]): Eq False True % 54.45/54.79 Clause #5810 (by clausification #[5809]): False % 54.45/54.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------