%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL815_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:43 AM UTC 2026 % Result : Theorem 87.56s 87.84s % Output : Proof 87.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL815_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : duper %s % 0.10/0.36 % Computer : n001.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Sat Sep 5 01:19:00 UTC 2026 % 0.10/0.36 % CPUTime : % 87.56/87.84 SZS status Theorem for theBenchmark.p % 87.56/87.84 SZS output start Proof for theBenchmark.p % 87.56/87.84 Clause #3 (by assumption #[]): Eq (pp (aa (list type) bool (typings e (map dB dB (combc dB nat dB (combc dB dB (fun nat dB) subst u) i) as)) ts)) True % 87.56/87.84 Clause #5 (by assumption #[]): Eq % 87.56/87.84 (∀ (Ua : type) (Ib : nat) (Tsa : list type) (Ts : list dB) (Eb : fun nat type), % 87.56/87.84 pp (aa (list type) bool (typings Eb Ts) Tsa) → % 87.56/87.84 pp (aa (list type) bool (typings (shift type Eb Ib Ua) (map dB dB (combc dB nat dB lift Ib) Ts)) Tsa)) % 87.56/87.84 True % 87.56/87.84 Clause #113 (by assumption #[]): Eq % 87.56/87.84 (Not % 87.56/87.84 (pp % 87.56/87.84 (aa (list type) bool % 87.56/87.84 (typings (shift type e (zero_zero nat) (foldr type type fun1 ts t)) % 87.56/87.84 (map dB dB (combc dB nat dB lift (zero_zero nat)) % 87.56/87.84 (map dB dB (combc dB nat dB (combc dB dB (fun nat dB) subst u) i) as))) % 87.56/87.84 ts))) % 87.56/87.84 True % 87.56/87.84 Clause #173 (by clausification #[5]): ∀ (a : type), % 87.56/87.84 Eq % 87.56/87.84 (∀ (Ib : nat) (Tsa : list type) (Ts : list dB) (Eb : fun nat type), % 87.56/87.84 pp (aa (list type) bool (typings Eb Ts) Tsa) → % 87.56/87.85 pp (aa (list type) bool (typings (shift type Eb Ib a) (map dB dB (combc dB nat dB lift Ib) Ts)) Tsa)) % 87.56/87.85 True % 87.56/87.85 Clause #174 (by clausification #[173]): ∀ (a : nat) (a_1 : type), % 87.56/87.85 Eq % 87.56/87.85 (∀ (Tsa : list type) (Ts : list dB) (Eb : fun nat type), % 87.56/87.85 pp (aa (list type) bool (typings Eb Ts) Tsa) → % 87.56/87.85 pp (aa (list type) bool (typings (shift type Eb a a_1) (map dB dB (combc dB nat dB lift a) Ts)) Tsa)) % 87.56/87.85 True % 87.56/87.85 Clause #175 (by clausification #[174]): ∀ (a : list type) (a_1 : nat) (a_2 : type), % 87.56/87.85 Eq % 87.56/87.85 (∀ (Ts : list dB) (Eb : fun nat type), % 87.56/87.85 pp (aa (list type) bool (typings Eb Ts) a) → % 87.56/87.85 pp (aa (list type) bool (typings (shift type Eb a_1 a_2) (map dB dB (combc dB nat dB lift a_1) Ts)) a)) % 87.56/87.85 True % 87.56/87.85 Clause #176 (by clausification #[175]): ∀ (a : list dB) (a_1 : list type) (a_2 : nat) (a_3 : type), % 87.56/87.85 Eq % 87.56/87.85 (∀ (Eb : fun nat type), % 87.56/87.85 pp (aa (list type) bool (typings Eb a) a_1) → % 87.56/87.85 pp (aa (list type) bool (typings (shift type Eb a_2 a_3) (map dB dB (combc dB nat dB lift a_2) a)) a_1)) % 87.56/87.85 True % 87.56/87.85 Clause #177 (by clausification #[176]): ∀ (a : fun nat type) (a_1 : list dB) (a_2 : list type) (a_3 : nat) (a_4 : type), % 87.56/87.85 Eq % 87.56/87.85 (pp (aa (list type) bool (typings a a_1) a_2) → % 87.56/87.85 pp (aa (list type) bool (typings (shift type a a_3 a_4) (map dB dB (combc dB nat dB lift a_3) a_1)) a_2)) % 87.56/87.85 True % 87.56/87.85 Clause #178 (by clausification #[177]): ∀ (a : fun nat type) (a_1 : list dB) (a_2 : list type) (a_3 : nat) (a_4 : type), % 87.56/87.85 Or (Eq (pp (aa (list type) bool (typings a a_1) a_2)) False) % 87.56/87.85 (Eq (pp (aa (list type) bool (typings (shift type a a_3 a_4) (map dB dB (combc dB nat dB lift a_3) a_1)) a_2)) True) % 87.56/87.85 Clause #179 (by superposition #[178, 3]): ∀ (a : nat) (a_1 : type), % 87.56/87.85 Or % 87.56/87.85 (Eq % 87.56/87.85 (pp % 87.56/87.85 (aa (list type) bool % 87.56/87.85 (typings (shift type e a a_1) % 87.56/87.85 (map dB dB (combc dB nat dB lift a) (map dB dB (combc dB nat dB (combc dB dB (fun nat dB) subst u) i) as))) % 87.56/87.85 ts)) % 87.56/87.85 True) % 87.56/87.85 (Eq False True) % 87.56/87.85 Clause #7244 (by clausification #[113]): Eq % 87.56/87.85 (pp % 87.56/87.85 (aa (list type) bool % 87.56/87.85 (typings (shift type e (zero_zero nat) (foldr type type fun1 ts t)) % 87.56/87.85 (map dB dB (combc dB nat dB lift (zero_zero nat)) % 87.56/87.85 (map dB dB (combc dB nat dB (combc dB dB (fun nat dB) subst u) i) as))) % 87.56/87.85 ts)) % 87.56/87.85 False % 87.56/87.85 Clause #8503 (by clausification #[179]): ∀ (a : nat) (a_1 : type), % 87.56/87.85 Eq % 87.56/87.85 (pp % 87.56/87.85 (aa (list type) bool % 87.56/87.85 (typings (shift type e a a_1) % 87.56/87.85 (map dB dB (combc dB nat dB lift a) (map dB dB (combc dB nat dB (combc dB dB (fun nat dB) subst u) i) as))) % 87.56/87.85 ts)) % 87.56/87.85 True % 87.56/87.85 Clause #8508 (by superposition #[8503, 7244]): Eq True False % 87.56/87.85 Clause #8587 (by clausification #[8508]): False % 87.56/87.85 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------