%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL512+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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:03 AM UTC 2026 % Result : Theorem 5.56s 5.86s % Output : Proof 5.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL512+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : duper %s % 0.11/0.36 % Computer : n015.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % 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 17:16:57 UTC 2026 % 0.11/0.36 % CPUTime : % 5.56/5.86 SZS status Theorem for theBenchmark.p % 5.56/5.86 SZS output start Proof for theBenchmark.p % 5.56/5.86 Clause #12 (by assumption #[]): Eq (Iff equivalence_1 (∀ (X Y : Iota), is_a_theorem (implies (equiv X Y) (implies X Y)))) True % 5.56/5.86 Clause #16 (by assumption #[]): Eq (Iff kn2 (∀ (P Q : Iota), is_a_theorem (implies (and P Q) P))) True % 5.56/5.86 Clause #30 (by assumption #[]): Eq (op_equiv → ∀ (X Y : Iota), Eq (equiv X Y) (and (implies X Y) (implies Y X))) True % 5.56/5.86 Clause #33 (by assumption #[]): Eq op_equiv True % 5.56/5.86 Clause #36 (by assumption #[]): Eq kn2 True % 5.56/5.86 Clause #39 (by assumption #[]): Eq (Not equivalence_1) True % 5.56/5.86 Clause #51 (by clausification #[39]): Eq equivalence_1 False % 5.56/5.86 Clause #141 (by clausification #[16]): Or (Eq kn2 False) (Eq (∀ (P Q : Iota), is_a_theorem (implies (and P Q) P)) True) % 5.56/5.86 Clause #147 (by clausification #[141]): ∀ (a : Iota), Or (Eq kn2 False) (Eq (∀ (Q : Iota), is_a_theorem (implies (and a Q) a)) True) % 5.56/5.86 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), Or (Eq kn2 False) (Eq (is_a_theorem (implies (and a a_1) a)) True) % 5.56/5.86 Clause #149 (by forward demodulation #[148, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (and a a_1) a)) True) % 5.56/5.86 Clause #150 (by clausification #[149]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (and a a_1) a)) True % 5.56/5.86 Clause #199 (by clausification #[12]): Or (Eq equivalence_1 True) (Eq (∀ (X Y : Iota), is_a_theorem (implies (equiv X Y) (implies X Y))) False) % 5.56/5.86 Clause #201 (by clausification #[199]): ∀ (a : Iota), % 5.56/5.86 Or (Eq equivalence_1 True) % 5.56/5.86 (Eq (Not (∀ (Y : Iota), is_a_theorem (implies (equiv (skS.0 34 a) Y) (implies (skS.0 34 a) Y)))) True) % 5.56/5.86 Clause #202 (by clausification #[201]): ∀ (a : Iota), % 5.56/5.86 Or (Eq equivalence_1 True) % 5.56/5.86 (Eq (∀ (Y : Iota), is_a_theorem (implies (equiv (skS.0 34 a) Y) (implies (skS.0 34 a) Y))) False) % 5.56/5.86 Clause #203 (by clausification #[202]): ∀ (a a_1 : Iota), % 5.56/5.86 Or (Eq equivalence_1 True) % 5.56/5.86 (Eq (Not (is_a_theorem (implies (equiv (skS.0 34 a) (skS.0 35 a a_1)) (implies (skS.0 34 a) (skS.0 35 a a_1))))) % 5.56/5.86 True) % 5.56/5.86 Clause #204 (by clausification #[203]): ∀ (a a_1 : Iota), % 5.56/5.86 Or (Eq equivalence_1 True) % 5.56/5.86 (Eq (is_a_theorem (implies (equiv (skS.0 34 a) (skS.0 35 a a_1)) (implies (skS.0 34 a) (skS.0 35 a a_1)))) False) % 5.56/5.86 Clause #205 (by forward demodulation #[204, 51]): ∀ (a a_1 : Iota), % 5.56/5.86 Or (Eq False True) % 5.56/5.86 (Eq (is_a_theorem (implies (equiv (skS.0 34 a) (skS.0 35 a a_1)) (implies (skS.0 34 a) (skS.0 35 a a_1)))) False) % 5.56/5.86 Clause #206 (by clausification #[205]): ∀ (a a_1 : Iota), % 5.56/5.86 Eq (is_a_theorem (implies (equiv (skS.0 34 a) (skS.0 35 a a_1)) (implies (skS.0 34 a) (skS.0 35 a a_1)))) False % 5.56/5.86 Clause #401 (by clausification #[30]): Or (Eq op_equiv False) (Eq (∀ (X Y : Iota), Eq (equiv X Y) (and (implies X Y) (implies Y X))) True) % 5.56/5.86 Clause #402 (by clausification #[401]): ∀ (a : Iota), Or (Eq op_equiv False) (Eq (∀ (Y : Iota), Eq (equiv a Y) (and (implies a Y) (implies Y a))) True) % 5.56/5.86 Clause #403 (by clausification #[402]): ∀ (a a_1 : Iota), Or (Eq op_equiv False) (Eq (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) True) % 5.56/5.86 Clause #404 (by clausification #[403]): ∀ (a a_1 : Iota), Or (Eq op_equiv False) (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) % 5.56/5.86 Clause #405 (by forward demodulation #[404, 33]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) % 5.56/5.86 Clause #406 (by clausification #[405]): ∀ (a a_1 : Iota), Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a)) % 5.56/5.86 Clause #409 (by superposition #[406, 150]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (equiv a a_1) (implies a a_1))) True % 5.56/5.86 Clause #418 (by superposition #[409, 206]): Eq True False % 5.56/5.86 Clause #422 (by clausification #[418]): False % 5.56/5.86 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------