%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL465+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n010.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 5.79s 6.11s % Output : Proof 5.79s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL465+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.05 % Command : duper %s % 0.12/0.37 % Computer : n010.cluster.edu % 0.12/0.37 % Model : x86_64 x86_64 % 0.12/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.37 % Memory : 8046.5625MB % 0.12/0.37 % OS : Linux 6.8.0-71-generic % 0.12/0.37 % CPULimit : 300 % 0.12/0.37 % WCLimit : 300 % 0.12/0.37 % DateTime : Fri Sep 4 21:20:53 UTC 2026 % 0.12/0.38 % CPUTime : % 5.79/6.11 SZS status Theorem for theBenchmark.p % 5.79/6.11 SZS output start Proof for theBenchmark.p % 5.79/6.11 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 % 5.79/6.11 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 % 5.79/6.11 Clause #35 (by assumption #[]): Eq cn1 True % 5.79/6.11 Clause #40 (by assumption #[]): Eq (Not implies_3) True % 5.79/6.11 Clause #52 (by clausification #[40]): Eq implies_3 False % 5.79/6.11 Clause #129 (by clausification #[5]): Or (Eq implies_3 True) % 5.79/6.11 (Eq (∀ (X Y Z : Iota), is_a_theorem (implies (implies X Y) (implies (implies Y Z) (implies X Z)))) False) % 5.79/6.11 Clause #131 (by clausification #[129]): ∀ (a : Iota), % 5.79/6.11 Or (Eq implies_3 True) % 5.79/6.11 (Eq % 5.79/6.11 (Not % 5.79/6.11 (∀ (Y Z : Iota), % 5.79/6.11 is_a_theorem (implies (implies (skS.0 18 a) Y) (implies (implies Y Z) (implies (skS.0 18 a) Z))))) % 5.79/6.11 True) % 5.79/6.11 Clause #132 (by clausification #[131]): ∀ (a : Iota), % 5.79/6.11 Or (Eq implies_3 True) % 5.79/6.11 (Eq % 5.79/6.11 (∀ (Y Z : Iota), is_a_theorem (implies (implies (skS.0 18 a) Y) (implies (implies Y Z) (implies (skS.0 18 a) Z)))) % 5.79/6.11 False) % 5.79/6.11 Clause #133 (by clausification #[132]): ∀ (a a_1 : Iota), % 5.79/6.11 Or (Eq implies_3 True) % 5.79/6.11 (Eq % 5.79/6.11 (Not % 5.79/6.11 (∀ (Z : Iota), % 5.79/6.11 is_a_theorem % 5.79/6.11 (implies (implies (skS.0 18 a) (skS.0 19 a a_1)) % 5.79/6.11 (implies (implies (skS.0 19 a a_1) Z) (implies (skS.0 18 a) Z))))) % 5.79/6.11 True) % 5.79/6.11 Clause #134 (by clausification #[133]): ∀ (a a_1 : Iota), % 5.79/6.11 Or (Eq implies_3 True) % 5.79/6.11 (Eq % 5.79/6.11 (∀ (Z : Iota), % 5.79/6.11 is_a_theorem % 5.79/6.11 (implies (implies (skS.0 18 a) (skS.0 19 a a_1)) % 5.79/6.11 (implies (implies (skS.0 19 a a_1) Z) (implies (skS.0 18 a) Z)))) % 5.79/6.11 False) % 5.79/6.11 Clause #135 (by clausification #[134]): ∀ (a a_1 a_2 : Iota), % 5.79/6.11 Or (Eq implies_3 True) % 5.79/6.11 (Eq % 5.79/6.11 (Not % 5.79/6.11 (is_a_theorem % 5.79/6.11 (implies (implies (skS.0 18 a) (skS.0 19 a a_1)) % 5.79/6.11 (implies (implies (skS.0 19 a a_1) (skS.0 20 a a_1 a_2)) (implies (skS.0 18 a) (skS.0 20 a a_1 a_2)))))) % 5.79/6.11 True) % 5.79/6.11 Clause #136 (by clausification #[135]): ∀ (a a_1 a_2 : Iota), % 5.79/6.11 Or (Eq implies_3 True) % 5.79/6.11 (Eq % 5.79/6.11 (is_a_theorem % 5.79/6.11 (implies (implies (skS.0 18 a) (skS.0 19 a a_1)) % 5.79/6.11 (implies (implies (skS.0 19 a a_1) (skS.0 20 a a_1 a_2)) (implies (skS.0 18 a) (skS.0 20 a a_1 a_2))))) % 5.79/6.11 False) % 5.79/6.11 Clause #137 (by forward demodulation #[136, 52]): ∀ (a a_1 a_2 : Iota), % 5.79/6.11 Or (Eq False True) % 5.79/6.11 (Eq % 5.79/6.11 (is_a_theorem % 5.79/6.11 (implies (implies (skS.0 18 a) (skS.0 19 a a_1)) % 5.79/6.11 (implies (implies (skS.0 19 a a_1) (skS.0 20 a a_1 a_2)) (implies (skS.0 18 a) (skS.0 20 a a_1 a_2))))) % 5.79/6.11 False) % 5.79/6.11 Clause #138 (by clausification #[137]): ∀ (a a_1 a_2 : Iota), % 5.79/6.11 Eq % 5.79/6.11 (is_a_theorem % 5.79/6.11 (implies (implies (skS.0 18 a) (skS.0 19 a a_1)) % 5.79/6.11 (implies (implies (skS.0 19 a a_1) (skS.0 20 a a_1 a_2)) (implies (skS.0 18 a) (skS.0 20 a a_1 a_2))))) % 5.79/6.11 False % 5.79/6.11 Clause #264 (by clausification #[18]): Or (Eq cn1 False) % 5.79/6.11 (Eq (∀ (P Q R : Iota), is_a_theorem (implies (implies P Q) (implies (implies Q R) (implies P R)))) True) % 5.79/6.11 Clause #918 (by clausification #[264]): ∀ (a : Iota), % 5.79/6.11 Or (Eq cn1 False) % 5.79/6.11 (Eq (∀ (Q R : Iota), is_a_theorem (implies (implies a Q) (implies (implies Q R) (implies a R)))) True) % 5.79/6.11 Clause #919 (by clausification #[918]): ∀ (a a_1 : Iota), % 5.79/6.11 Or (Eq cn1 False) % 5.79/6.11 (Eq (∀ (R : Iota), is_a_theorem (implies (implies a a_1) (implies (implies a_1 R) (implies a R)))) True) % 5.79/6.11 Clause #920 (by clausification #[919]): ∀ (a a_1 a_2 : Iota), % 5.79/6.11 Or (Eq cn1 False) (Eq (is_a_theorem (implies (implies a a_1) (implies (implies a_1 a_2) (implies a a_2)))) True) % 5.79/6.11 Clause #921 (by forward demodulation #[920, 35]): ∀ (a a_1 a_2 : Iota), % 5.79/6.11 Or (Eq True False) (Eq (is_a_theorem (implies (implies a a_1) (implies (implies a_1 a_2) (implies a a_2)))) True) % 5.79/6.11 Clause #922 (by clausification #[921]): ∀ (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 % 5.79/6.11 Clause #923 (by superposition #[922, 138]): Eq True False % 5.79/6.11 Clause #946 (by clausification #[923]): False % 5.79/6.11 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------