%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL451+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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 11.79s 12.12s % Output : Proof 11.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL451+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : duper %s % 0.11/0.37 % Computer : n007.cluster.edu % 0.11/0.37 % Model : x86_64 x86_64 % 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.37 % Memory : 8046.5625MB % 0.11/0.37 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Fri Sep 4 20:38:09 UTC 2026 % 0.11/0.37 % CPUTime : % 11.79/12.12 SZS status Theorem for theBenchmark.p % 11.79/12.12 SZS output start Proof for theBenchmark.p % 11.79/12.12 Clause #5 (by assumption #[]): Eq (Iff implies_3 (∀ (X Y Z : Iota), is_a_theorem (implies (implies X Y) (implies (implies Y Z) (implies X Z))))) True % 11.79/12.12 Clause #18 (by assumption #[]): Eq (Iff cn1 (∀ (P Q R : Iota), is_a_theorem (implies (implies P Q) (implies (implies Q R) (implies P R))))) True % 11.79/12.12 Clause #38 (by assumption #[]): Eq implies_3 True % 11.79/12.12 Clause #50 (by assumption #[]): Eq (Not cn1) True % 11.79/12.12 Clause #78 (by clausification #[50]): Eq cn1 False % 11.79/12.12 Clause #134 (by clausification #[5]): Or (Eq implies_3 False) % 11.79/12.12 (Eq (∀ (X Y Z : Iota), is_a_theorem (implies (implies X Y) (implies (implies Y Z) (implies X Z)))) True) % 11.79/12.12 Clause #315 (by clausification #[18]): Or (Eq cn1 True) % 11.79/12.12 (Eq (∀ (P Q R : Iota), is_a_theorem (implies (implies P Q) (implies (implies Q R) (implies P R)))) False) % 11.79/12.12 Clause #317 (by clausification #[315]): ∀ (a : Iota), % 11.79/12.12 Or (Eq cn1 True) % 11.79/12.12 (Eq % 11.79/12.12 (Not % 11.79/12.12 (∀ (Q R : Iota), % 11.79/12.12 is_a_theorem (implies (implies (skS.0 46 a) Q) (implies (implies Q R) (implies (skS.0 46 a) R))))) % 11.79/12.12 True) % 11.79/12.12 Clause #318 (by clausification #[317]): ∀ (a : Iota), % 11.79/12.12 Or (Eq cn1 True) % 11.79/12.12 (Eq % 11.79/12.12 (∀ (Q R : Iota), is_a_theorem (implies (implies (skS.0 46 a) Q) (implies (implies Q R) (implies (skS.0 46 a) R)))) % 11.79/12.12 False) % 11.79/12.12 Clause #319 (by clausification #[318]): ∀ (a a_1 : Iota), % 11.79/12.12 Or (Eq cn1 True) % 11.79/12.12 (Eq % 11.79/12.12 (Not % 11.79/12.12 (∀ (R : Iota), % 11.79/12.12 is_a_theorem % 11.79/12.12 (implies (implies (skS.0 46 a) (skS.0 47 a a_1)) % 11.79/12.12 (implies (implies (skS.0 47 a a_1) R) (implies (skS.0 46 a) R))))) % 11.79/12.12 True) % 11.79/12.12 Clause #320 (by clausification #[319]): ∀ (a a_1 : Iota), % 11.79/12.12 Or (Eq cn1 True) % 11.79/12.12 (Eq % 11.79/12.12 (∀ (R : Iota), % 11.79/12.12 is_a_theorem % 11.79/12.12 (implies (implies (skS.0 46 a) (skS.0 47 a a_1)) % 11.79/12.12 (implies (implies (skS.0 47 a a_1) R) (implies (skS.0 46 a) R)))) % 11.79/12.12 False) % 11.79/12.12 Clause #321 (by clausification #[320]): ∀ (a a_1 a_2 : Iota), % 11.79/12.12 Or (Eq cn1 True) % 11.79/12.12 (Eq % 11.79/12.12 (Not % 11.79/12.12 (is_a_theorem % 11.79/12.12 (implies (implies (skS.0 46 a) (skS.0 47 a a_1)) % 11.79/12.12 (implies (implies (skS.0 47 a a_1) (skS.0 48 a a_1 a_2)) (implies (skS.0 46 a) (skS.0 48 a a_1 a_2)))))) % 11.79/12.12 True) % 11.79/12.12 Clause #322 (by clausification #[321]): ∀ (a a_1 a_2 : Iota), % 11.79/12.12 Or (Eq cn1 True) % 11.79/12.12 (Eq % 11.79/12.12 (is_a_theorem % 11.79/12.12 (implies (implies (skS.0 46 a) (skS.0 47 a a_1)) % 11.79/12.12 (implies (implies (skS.0 47 a a_1) (skS.0 48 a a_1 a_2)) (implies (skS.0 46 a) (skS.0 48 a a_1 a_2))))) % 11.79/12.12 False) % 11.79/12.12 Clause #323 (by forward demodulation #[322, 78]): ∀ (a a_1 a_2 : Iota), % 11.79/12.12 Or (Eq False True) % 11.79/12.12 (Eq % 11.79/12.12 (is_a_theorem % 11.79/12.12 (implies (implies (skS.0 46 a) (skS.0 47 a a_1)) % 11.79/12.12 (implies (implies (skS.0 47 a a_1) (skS.0 48 a a_1 a_2)) (implies (skS.0 46 a) (skS.0 48 a a_1 a_2))))) % 11.79/12.12 False) % 11.79/12.12 Clause #324 (by clausification #[323]): ∀ (a a_1 a_2 : Iota), % 11.79/12.12 Eq % 11.79/12.12 (is_a_theorem % 11.79/12.12 (implies (implies (skS.0 46 a) (skS.0 47 a a_1)) % 11.79/12.12 (implies (implies (skS.0 47 a a_1) (skS.0 48 a a_1 a_2)) (implies (skS.0 46 a) (skS.0 48 a a_1 a_2))))) % 11.79/12.12 False % 11.79/12.12 Clause #630 (by clausification #[134]): ∀ (a : Iota), % 11.79/12.12 Or (Eq implies_3 False) % 11.79/12.12 (Eq (∀ (Y Z : Iota), is_a_theorem (implies (implies a Y) (implies (implies Y Z) (implies a Z)))) True) % 11.79/12.12 Clause #631 (by clausification #[630]): ∀ (a a_1 : Iota), % 11.79/12.12 Or (Eq implies_3 False) % 11.79/12.12 (Eq (∀ (Z : Iota), is_a_theorem (implies (implies a a_1) (implies (implies a_1 Z) (implies a Z)))) True) % 11.79/12.12 Clause #632 (by clausification #[631]): ∀ (a a_1 a_2 : Iota), % 11.79/12.12 Or (Eq implies_3 False) (Eq (is_a_theorem (implies (implies a a_1) (implies (implies a_1 a_2) (implies a a_2)))) True) % 11.79/12.12 Clause #633 (by forward demodulation #[632, 38]): ∀ (a a_1 a_2 : Iota), % 11.79/12.12 Or (Eq True False) (Eq (is_a_theorem (implies (implies a a_1) (implies (implies a_1 a_2) (implies a a_2)))) True) % 11.79/12.12 Clause #634 (by clausification #[633]): ∀ (a a_1 a_2 : Iota), Eq (is_a_theorem (implies (implies a a_1) (implies (implies a_1 a_2) (implies a a_2)))) True % 11.79/12.12 Clause #637 (by superposition #[634, 324]): Eq True False % 11.79/12.12 Clause #645 (by clausification #[637]): False % 11.79/12.12 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------