%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL529+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:04 AM UTC 2026 % Result : Theorem 6.07s 6.31s % Output : Proof 6.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL529+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : duper %s % 0.11/0.35 % Computer : n018.cluster.edu % 0.11/0.35 % Model : x86_64 x86_64 % 0.11/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.35 % Memory : 8046.5625MB % 0.11/0.35 % OS : Linux 6.8.0-71-generic % 0.11/0.36 % CPULimit : 300 % 0.11/0.36 % WCLimit : 300 % 0.11/0.36 % DateTime : Sat Sep 5 15:34:34 UTC 2026 % 0.11/0.36 % CPUTime : % 6.07/6.31 SZS status Theorem for theBenchmark.p % 6.07/6.31 SZS output start Proof for theBenchmark.p % 6.07/6.31 Clause #6 (by assumption #[]): Eq (Iff and_1 (∀ (X Y : Iota), is_a_theorem (implies (and X Y) X))) True % 6.07/6.31 Clause #39 (by assumption #[]): Eq and_1 True % 6.07/6.31 Clause #49 (by assumption #[]): Eq (Iff necessitation (∀ (X : Iota), is_a_theorem X → is_a_theorem (necessarily X))) True % 6.07/6.31 Clause #63 (by assumption #[]): Eq (Iff axiom_m2 (∀ (X Y : Iota), is_a_theorem (strict_implies (and X Y) X))) True % 6.07/6.31 Clause #74 (by assumption #[]): Eq (op_strict_implies → ∀ (X Y : Iota), Eq (strict_implies X Y) (necessarily (implies X Y))) True % 6.07/6.31 Clause #77 (by assumption #[]): Eq necessitation True % 6.07/6.31 Clause #82 (by assumption #[]): Eq op_strict_implies True % 6.07/6.31 Clause #84 (by assumption #[]): Eq (Not axiom_m2) True % 6.07/6.31 Clause #126 (by clausification #[84]): Eq axiom_m2 False % 6.07/6.31 Clause #134 (by clausification #[49]): Or (Eq necessitation False) (Eq (∀ (X : Iota), is_a_theorem X → is_a_theorem (necessarily X)) True) % 6.07/6.31 Clause #140 (by clausification #[134]): ∀ (a : Iota), Or (Eq necessitation False) (Eq (is_a_theorem a → is_a_theorem (necessarily a)) True) % 6.07/6.31 Clause #141 (by clausification #[140]): ∀ (a : Iota), Or (Eq necessitation False) (Or (Eq (is_a_theorem a) False) (Eq (is_a_theorem (necessarily a)) True)) % 6.07/6.31 Clause #142 (by forward demodulation #[141, 77]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (is_a_theorem a) False) (Eq (is_a_theorem (necessarily a)) True)) % 6.07/6.31 Clause #143 (by clausification #[142]): ∀ (a : Iota), Or (Eq (is_a_theorem a) False) (Eq (is_a_theorem (necessarily a)) True) % 6.07/6.31 Clause #180 (by clausification #[6]): Or (Eq and_1 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies (and X Y) X)) True) % 6.07/6.31 Clause #356 (by clausification #[63]): Or (Eq axiom_m2 True) (Eq (∀ (X Y : Iota), is_a_theorem (strict_implies (and X Y) X)) False) % 6.07/6.31 Clause #358 (by clausification #[356]): ∀ (a : Iota), % 6.07/6.31 Or (Eq axiom_m2 True) (Eq (Not (∀ (Y : Iota), is_a_theorem (strict_implies (and (skS.0 45 a) Y) (skS.0 45 a)))) True) % 6.07/6.31 Clause #359 (by clausification #[358]): ∀ (a : Iota), % 6.07/6.31 Or (Eq axiom_m2 True) (Eq (∀ (Y : Iota), is_a_theorem (strict_implies (and (skS.0 45 a) Y) (skS.0 45 a))) False) % 6.07/6.31 Clause #360 (by clausification #[359]): ∀ (a a_1 : Iota), % 6.07/6.31 Or (Eq axiom_m2 True) (Eq (Not (is_a_theorem (strict_implies (and (skS.0 45 a) (skS.0 46 a a_1)) (skS.0 45 a)))) True) % 6.07/6.31 Clause #361 (by clausification #[360]): ∀ (a a_1 : Iota), % 6.07/6.31 Or (Eq axiom_m2 True) (Eq (is_a_theorem (strict_implies (and (skS.0 45 a) (skS.0 46 a a_1)) (skS.0 45 a))) False) % 6.07/6.31 Clause #362 (by forward demodulation #[361, 126]): ∀ (a a_1 : Iota), % 6.07/6.31 Or (Eq False True) (Eq (is_a_theorem (strict_implies (and (skS.0 45 a) (skS.0 46 a a_1)) (skS.0 45 a))) False) % 6.07/6.31 Clause #363 (by clausification #[362]): ∀ (a a_1 : Iota), Eq (is_a_theorem (strict_implies (and (skS.0 45 a) (skS.0 46 a a_1)) (skS.0 45 a))) False % 6.07/6.31 Clause #379 (by clausification #[180]): ∀ (a : Iota), Or (Eq and_1 False) (Eq (∀ (Y : Iota), is_a_theorem (implies (and a Y) a)) True) % 6.07/6.31 Clause #380 (by clausification #[379]): ∀ (a a_1 : Iota), Or (Eq and_1 False) (Eq (is_a_theorem (implies (and a a_1) a)) True) % 6.07/6.31 Clause #381 (by forward demodulation #[380, 39]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (and a a_1) a)) True) % 6.07/6.31 Clause #382 (by clausification #[381]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (and a a_1) a)) True % 6.07/6.31 Clause #385 (by superposition #[382, 143]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (necessarily (implies (and a a_1) a))) True) % 6.07/6.31 Clause #395 (by clausification #[385]): ∀ (a a_1 : Iota), Eq (is_a_theorem (necessarily (implies (and a a_1) a))) True % 6.07/6.31 Clause #969 (by clausification #[74]): Or (Eq op_strict_implies False) (Eq (∀ (X Y : Iota), Eq (strict_implies X Y) (necessarily (implies X Y))) True) % 6.07/6.31 Clause #970 (by clausification #[969]): ∀ (a : Iota), % 6.07/6.31 Or (Eq op_strict_implies False) (Eq (∀ (Y : Iota), Eq (strict_implies a Y) (necessarily (implies a Y))) True) % 6.07/6.31 Clause #971 (by clausification #[970]): ∀ (a a_1 : Iota), Or (Eq op_strict_implies False) (Eq (Eq (strict_implies a a_1) (necessarily (implies a a_1))) True) % 6.07/6.32 Clause #972 (by clausification #[971]): ∀ (a a_1 : Iota), Or (Eq op_strict_implies False) (Eq (strict_implies a a_1) (necessarily (implies a a_1))) % 6.07/6.32 Clause #973 (by forward demodulation #[972, 82]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (strict_implies a a_1) (necessarily (implies a a_1))) % 6.07/6.32 Clause #974 (by clausification #[973]): ∀ (a a_1 : Iota), Eq (strict_implies a a_1) (necessarily (implies a a_1)) % 6.07/6.32 Clause #983 (by backward demodulation #[974, 395]): ∀ (a a_1 : Iota), Eq (is_a_theorem (strict_implies (and a a_1) a)) True % 6.07/6.32 Clause #1018 (by superposition #[983, 363]): Eq True False % 6.07/6.32 Clause #1030 (by clausification #[1018]): False % 6.07/6.32 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------