%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL795_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:40 AM UTC 2026 % Result : Theorem 39.06s 39.34s % Output : Proof 39.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL795_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : duper %s % 0.12/0.38 % Computer : n031.cluster.edu % 0.12/0.38 % Model : x86_64 x86_64 % 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.38 % Memory : 8046.5625MB % 0.12/0.38 % OS : Linux 6.8.0-71-generic % 0.12/0.38 % CPULimit : 300 % 0.12/0.38 % WCLimit : 300 % 0.12/0.38 % DateTime : Sat Sep 5 02:22:24 UTC 2026 % 0.12/0.38 % CPUTime : % 39.06/39.34 SZS status Theorem for theBenchmark.p % 39.06/39.34 SZS output start Proof for theBenchmark.p % 39.06/39.34 Clause #3 (by assumption #[]): Eq (pp (aa type bool (typing e u) t2)) True % 39.06/39.34 Clause #4 (by assumption #[]): Eq % 39.06/39.34 (∀ (Ua : type) (Ib : nat) (Ta : type) (Ta1 : dB) (Eb : fun1 nat type), % 39.06/39.34 pp (aa type bool (typing Eb Ta1) Ta) → % 39.06/39.34 pp (aa type bool (typing (shift type Eb Ib Ua) (aa nat dB (aa dB (fun1 nat dB) lift Ta1) Ib)) Ta)) % 39.06/39.34 True % 39.06/39.34 Clause #5 (by assumption #[]): Eq (Eq t2 (aa type type (aa type (fun1 type type) fun t1) (foldr type type fun ts t))) True % 39.06/39.34 Clause #103 (by assumption #[]): Eq % 39.06/39.34 (∀ (A C B : Type) (R : A) (Q : B) (P : fun1 A (fun1 B C)), % 39.06/39.34 Eq (aa A C (combc A B C P Q) R) (aa B C (aa A (fun1 B C) P R) Q)) % 39.06/39.34 True % 39.06/39.34 Clause #110 (by assumption #[]): Eq % 39.06/39.34 (Not % 39.06/39.34 (pp % 39.06/39.34 (aa type bool (typing (shift type e (zero_zero nat) t1) (aa nat dB (aa dB (fun1 nat dB) lift u) (zero_zero nat))) % 39.06/39.34 (aa type type (aa type (fun1 type type) fun t1) (foldr type type fun ts t))))) % 39.06/39.34 True % 39.06/39.34 Clause #131 (by clausification #[4]): ∀ (a : type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (Ib : nat) (Ta : type) (Ta1 : dB) (Eb : fun1 nat type), % 39.06/39.34 pp (aa type bool (typing Eb Ta1) Ta) → % 39.06/39.34 pp (aa type bool (typing (shift type Eb Ib a) (aa nat dB (aa dB (fun1 nat dB) lift Ta1) Ib)) Ta)) % 39.06/39.34 True % 39.06/39.34 Clause #132 (by clausification #[131]): ∀ (a : nat) (a_1 : type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (Ta : type) (Ta1 : dB) (Eb : fun1 nat type), % 39.06/39.34 pp (aa type bool (typing Eb Ta1) Ta) → % 39.06/39.34 pp (aa type bool (typing (shift type Eb a a_1) (aa nat dB (aa dB (fun1 nat dB) lift Ta1) a)) Ta)) % 39.06/39.34 True % 39.06/39.34 Clause #133 (by clausification #[132]): ∀ (a : type) (a_1 : nat) (a_2 : type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (Ta1 : dB) (Eb : fun1 nat type), % 39.06/39.34 pp (aa type bool (typing Eb Ta1) a) → % 39.06/39.34 pp (aa type bool (typing (shift type Eb a_1 a_2) (aa nat dB (aa dB (fun1 nat dB) lift Ta1) a_1)) a)) % 39.06/39.34 True % 39.06/39.34 Clause #134 (by clausification #[133]): ∀ (a : dB) (a_1 : type) (a_2 : nat) (a_3 : type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (Eb : fun1 nat type), % 39.06/39.34 pp (aa type bool (typing Eb a) a_1) → % 39.06/39.34 pp (aa type bool (typing (shift type Eb a_2 a_3) (aa nat dB (aa dB (fun1 nat dB) lift a) a_2)) a_1)) % 39.06/39.34 True % 39.06/39.34 Clause #135 (by clausification #[134]): ∀ (a : fun1 nat type) (a_1 : dB) (a_2 : type) (a_3 : nat) (a_4 : type), % 39.06/39.34 Eq % 39.06/39.34 (pp (aa type bool (typing a a_1) a_2) → % 39.06/39.34 pp (aa type bool (typing (shift type a a_3 a_4) (aa nat dB (aa dB (fun1 nat dB) lift a_1) a_3)) a_2)) % 39.06/39.34 True % 39.06/39.34 Clause #136 (by clausification #[135]): ∀ (a : fun1 nat type) (a_1 : dB) (a_2 : type) (a_3 : nat) (a_4 : type), % 39.06/39.34 Or (Eq (pp (aa type bool (typing a a_1) a_2)) False) % 39.06/39.34 (Eq (pp (aa type bool (typing (shift type a a_3 a_4) (aa nat dB (aa dB (fun1 nat dB) lift a_1) a_3)) a_2)) True) % 39.06/39.34 Clause #137 (by superposition #[136, 3]): ∀ (a : nat) (a_1 : type), % 39.06/39.34 Or (Eq (pp (aa type bool (typing (shift type e a a_1) (aa nat dB (aa dB (fun1 nat dB) lift u) a)) t2)) True) % 39.06/39.34 (Eq False True) % 39.06/39.34 Clause #150 (by clausification #[5]): Eq t2 (aa type type (aa type (fun1 type type) fun t1) (foldr type type fun ts t)) % 39.06/39.34 Clause #7358 (by clausification #[103]): ∀ (a : Type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (C B : Type) (R : a) (Q : B) (P : fun1 a (fun1 B C)), % 39.06/39.34 Eq (aa a C (combc a B C P Q) R) (aa B C (aa a (fun1 B C) P R) Q)) % 39.06/39.34 True % 39.06/39.34 Clause #7359 (by clausification #[7358]): ∀ (a a_1 : Type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (B : Type) (R : a) (Q : B) (P : fun1 a (fun1 B a_1)), % 39.06/39.34 Eq (aa a a_1 (combc a B a_1 P Q) R) (aa B a_1 (aa a (fun1 B a_1) P R) Q)) % 39.06/39.34 True % 39.06/39.34 Clause #7360 (by clausification #[7359]): ∀ (a a_1 a_2 : Type), % 39.06/39.34 Eq % 39.06/39.34 (∀ (R : a) (Q : a_1) (P : fun1 a (fun1 a_1 a_2)), % 39.06/39.34 Eq (aa a a_2 (combc a a_1 a_2 P Q) R) (aa a_1 a_2 (aa a (fun1 a_1 a_2) P R) Q)) % 39.06/39.34 True % 39.06/39.34 Clause #7361 (by clausification #[7360]): ∀ (a a_1 a_2 : Type) (a_3 : a_1), % 39.06/39.34 Eq % 39.06/39.34 (∀ (Q : a) (P : fun1 a_1 (fun1 a a_2)), % 39.06/39.34 Eq (aa a_1 a_2 (combc a_1 a a_2 P Q) a_3) (aa a a_2 (aa a_1 (fun1 a a_2) P a_3) Q)) % 39.06/39.34 True % 39.06/39.34 Clause #7362 (by clausification #[7361]): ∀ (a a_1 a_2 : Type) (a_3 : a_1) (a_4 : a), % 39.06/39.34 Eq % 39.06/39.34 (∀ (P : fun1 a (fun1 a_1 a_2)), % 39.06/39.34 Eq (aa a a_2 (combc a a_1 a_2 P a_3) a_4) (aa a_1 a_2 (aa a (fun1 a_1 a_2) P a_4) a_3)) % 39.16/39.44 True % 39.16/39.44 Clause #7363 (by clausification #[7362]): ∀ (a a_1 a_2 : Type) (a_3 : fun1 a_1 (fun1 a_2 a)) (a_4 : a_2) (a_5 : a_1), % 39.16/39.44 Eq (Eq (aa a_1 a (combc a_1 a_2 a a_3 a_4) a_5) (aa a_2 a (aa a_1 (fun1 a_2 a) a_3 a_5) a_4)) True % 39.16/39.44 Clause #7364 (by clausification #[7363]): ∀ (a a_1 a_2 : Type) (a_3 : fun1 a_1 (fun1 a_2 a)) (a_4 : a_2) (a_5 : a_1), % 39.16/39.44 Eq (aa a_1 a (combc a_1 a_2 a a_3 a_4) a_5) (aa a_2 a (aa a_1 (fun1 a_2 a) a_3 a_5) a_4) % 39.16/39.44 Clause #7781 (by clausification #[110]): Eq % 39.16/39.44 (pp % 39.16/39.44 (aa type bool (typing (shift type e (zero_zero nat) t1) (aa nat dB (aa dB (fun1 nat dB) lift u) (zero_zero nat))) % 39.16/39.44 (aa type type (aa type (fun1 type type) fun t1) (foldr type type fun ts t)))) % 39.16/39.44 False % 39.16/39.44 Clause #7782 (by forward demodulation #[7781, 150]): Eq % 39.16/39.44 (pp % 39.16/39.44 (aa type bool (typing (shift type e (zero_zero nat) t1) (aa nat dB (aa dB (fun1 nat dB) lift u) (zero_zero nat))) % 39.16/39.44 t2)) % 39.16/39.44 False % 39.16/39.44 Clause #7783 (by forward demodulation #[7782, 7364]): Eq (pp (aa type bool (typing (shift type e (zero_zero nat) t1) (aa dB dB (combc dB nat dB lift (zero_zero nat)) u)) t2)) % 39.16/39.44 False % 39.16/39.44 Clause #7855 (by clausification #[137]): ∀ (a : nat) (a_1 : type), % 39.16/39.44 Eq (pp (aa type bool (typing (shift type e a a_1) (aa nat dB (aa dB (fun1 nat dB) lift u) a)) t2)) True % 39.16/39.44 Clause #7856 (by forward demodulation #[7855, 7364]): ∀ (a : nat) (a_1 : type), % 39.16/39.44 Eq (pp (aa type bool (typing (shift type e a a_1) (aa dB dB (combc dB nat dB lift a) u)) t2)) True % 39.16/39.44 Clause #7862 (by superposition #[7856, 7783]): Eq True False % 39.16/39.44 Clause #7931 (by clausification #[7862]): False % 39.16/39.44 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------