%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL834_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n008.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:46 AM UTC 2026 % Result : Theorem 39.66s 40.03s % Output : Proof 39.89s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL834_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : duper %s % 0.10/0.36 % Computer : n008.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 23:05:53 UTC 2026 % 0.10/0.36 % CPUTime : % 39.66/40.03 SZS status Theorem for theBenchmark.p % 39.66/40.03 SZS output start Proof for theBenchmark.p % 39.66/40.03 Clause #3 (by assumption #[]): Eq % 39.66/40.03 (∀ (T S2 : dB), % 39.66/40.03 pp % 39.66/40.03 (aa dB bool (aa dB (fun dB bool) beta (aa dB dB (aa dB (fun dB dB) app (abs S2)) T)) % 39.66/40.03 (subst S2 T (zero_zero nat)))) % 39.66/40.03 True % 39.66/40.03 Clause #10 (by assumption #[]): Eq % 39.66/40.03 (∀ (Ss1 : list dB) (S Ra : dB), % 39.66/40.03 pp (aa dB bool (aa dB (fun dB bool) beta Ra) S) → % 39.66/40.03 pp (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app Ra Ss1)) (foldl dB dB app S Ss1))) % 39.66/40.03 True % 39.66/40.03 Clause #57 (by assumption #[]): Eq % 39.66/40.03 (∀ (A B : Type) (Xs : list B) (X : B) (Aa : A) (F : fun A (fun B A)), % 39.66/40.03 Eq (foldl A B F Aa (cons B X Xs)) (foldl A B F (aa B A (aa A (fun B A) F Aa) X) Xs)) % 39.66/40.03 True % 39.66/40.03 Clause #103 (by assumption #[]): Eq % 39.66/40.03 (∀ (A C B : Type) (R : A) (Q : B) (P : fun A (fun B C)), % 39.66/40.03 Eq (aa A C (combc A B C P Q) R) (aa B C (aa A (fun B C) P R) Q)) % 39.66/40.03 True % 39.66/40.03 Clause #108 (by assumption #[]): Eq % 39.66/40.03 (Not % 39.66/40.03 (pp % 39.66/40.03 (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app (aa dB dB (aa dB (fun dB dB) app (abs r)) a) as)) % 39.79/40.03 (foldl dB dB app (subst r a (zero_zero nat)) as)))) % 39.79/40.03 True % 39.79/40.03 Clause #133 (by clausification #[3]): ∀ (a : dB), % 39.79/40.03 Eq % 39.79/40.03 (∀ (S2 : dB), % 39.79/40.03 pp % 39.79/40.03 (aa dB bool (aa dB (fun dB bool) beta (aa dB dB (aa dB (fun dB dB) app (abs S2)) a)) % 39.79/40.03 (subst S2 a (zero_zero nat)))) % 39.79/40.03 True % 39.79/40.03 Clause #134 (by clausification #[133]): ∀ (a a_1 : dB), % 39.79/40.03 Eq % 39.79/40.03 (pp % 39.79/40.03 (aa dB bool (aa dB (fun dB bool) beta (aa dB dB (aa dB (fun dB dB) app (abs a)) a_1)) % 39.79/40.03 (subst a a_1 (zero_zero nat)))) % 39.79/40.03 True % 39.79/40.03 Clause #255 (by clausification #[10]): ∀ (a : list dB), % 39.79/40.03 Eq % 39.79/40.03 (∀ (S Ra : dB), % 39.79/40.03 pp (aa dB bool (aa dB (fun dB bool) beta Ra) S) → % 39.79/40.03 pp (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app Ra a)) (foldl dB dB app S a))) % 39.79/40.03 True % 39.79/40.03 Clause #256 (by clausification #[255]): ∀ (a : dB) (a_1 : list dB), % 39.79/40.03 Eq % 39.79/40.03 (∀ (Ra : dB), % 39.79/40.03 pp (aa dB bool (aa dB (fun dB bool) beta Ra) a) → % 39.79/40.03 pp (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app Ra a_1)) (foldl dB dB app a a_1))) % 39.79/40.03 True % 39.79/40.03 Clause #257 (by clausification #[256]): ∀ (a a_1 : dB) (a_2 : list dB), % 39.79/40.03 Eq % 39.79/40.03 (pp (aa dB bool (aa dB (fun dB bool) beta a) a_1) → % 39.79/40.03 pp (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app a a_2)) (foldl dB dB app a_1 a_2))) % 39.79/40.03 True % 39.79/40.03 Clause #258 (by clausification #[257]): ∀ (a a_1 : dB) (a_2 : list dB), % 39.79/40.03 Or (Eq (pp (aa dB bool (aa dB (fun dB bool) beta a) a_1)) False) % 39.79/40.03 (Eq (pp (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app a a_2)) (foldl dB dB app a_1 a_2))) True) % 39.79/40.03 Clause #259 (by superposition #[258, 134]): ∀ (a a_1 : dB) (a_2 : list dB), % 39.79/40.03 Or % 39.79/40.03 (Eq % 39.79/40.03 (pp % 39.79/40.03 (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app (aa dB dB (aa dB (fun dB dB) app (abs a)) a_1) a_2)) % 39.79/40.03 (foldl dB dB app (subst a a_1 (zero_zero nat)) a_2))) % 39.79/40.03 True) % 39.79/40.03 (Eq False True) % 39.79/40.03 Clause #2201 (by clausification #[57]): ∀ (a : Type), % 39.79/40.03 Eq % 39.79/40.03 (∀ (B : Type) (Xs : list B) (X : B) (Aa : a) (F : fun a (fun B a)), % 39.79/40.03 Eq (foldl a B F Aa (cons B X Xs)) (foldl a B F (aa B a (aa a (fun B a) F Aa) X) Xs)) % 39.79/40.03 True % 39.79/40.03 Clause #2202 (by clausification #[2201]): ∀ (a a_1 : Type), % 39.79/40.03 Eq % 39.79/40.03 (∀ (Xs : list a) (X : a) (Aa : a_1) (F : fun a_1 (fun a a_1)), % 39.79/40.03 Eq (foldl a_1 a F Aa (cons a X Xs)) (foldl a_1 a F (aa a a_1 (aa a_1 (fun a a_1) F Aa) X) Xs)) % 39.79/40.03 True % 39.79/40.03 Clause #2203 (by clausification #[2202]): ∀ (a a_1 : Type) (a_2 : list a), % 39.79/40.03 Eq % 39.79/40.03 (∀ (X : a) (Aa : a_1) (F : fun a_1 (fun a a_1)), % 39.79/40.03 Eq (foldl a_1 a F Aa (cons a X a_2)) (foldl a_1 a F (aa a a_1 (aa a_1 (fun a a_1) F Aa) X) a_2)) % 39.79/40.03 True % 39.79/40.03 Clause #2204 (by clausification #[2203]): ∀ (a a_1 : Type) (a_2 : a_1) (a_3 : list a_1), % 39.79/40.03 Eq % 39.79/40.03 (∀ (Aa : a) (F : fun a (fun a_1 a)), % 39.79/40.03 Eq (foldl a a_1 F Aa (cons a_1 a_2 a_3)) (foldl a a_1 F (aa a_1 a (aa a (fun a_1 a) F Aa) a_2) a_3)) % 39.79/40.03 True % 39.79/40.03 Clause #2205 (by clausification #[2204]): ∀ (a a_1 : Type) (a_2 : a) (a_3 : a_1) (a_4 : list a_1), % 39.79/40.03 Eq % 39.79/40.03 (∀ (F : fun a (fun a_1 a)), % 39.79/40.03 Eq (foldl a a_1 F a_2 (cons a_1 a_3 a_4)) (foldl a a_1 F (aa a_1 a (aa a (fun a_1 a) F a_2) a_3) a_4)) % 39.89/40.15 True % 39.89/40.15 Clause #2206 (by clausification #[2205]): ∀ (a a_1 : Type) (a_2 : fun a (fun a_1 a)) (a_3 : a) (a_4 : a_1) (a_5 : list a_1), % 39.89/40.15 Eq (Eq (foldl a a_1 a_2 a_3 (cons a_1 a_4 a_5)) (foldl a a_1 a_2 (aa a_1 a (aa a (fun a_1 a) a_2 a_3) a_4) a_5)) True % 39.89/40.15 Clause #2207 (by clausification #[2206]): ∀ (a a_1 : Type) (a_2 : fun a (fun a_1 a)) (a_3 : a) (a_4 : a_1) (a_5 : list a_1), % 39.89/40.15 Eq (foldl a a_1 a_2 a_3 (cons a_1 a_4 a_5)) (foldl a a_1 a_2 (aa a_1 a (aa a (fun a_1 a) a_2 a_3) a_4) a_5) % 39.89/40.15 Clause #5104 (by clausification #[103]): ∀ (a : Type), % 39.89/40.15 Eq % 39.89/40.15 (∀ (C B : Type) (R : a) (Q : B) (P : fun a (fun B C)), % 39.89/40.15 Eq (aa a C (combc a B C P Q) R) (aa B C (aa a (fun B C) P R) Q)) % 39.89/40.15 True % 39.89/40.15 Clause #5105 (by clausification #[5104]): ∀ (a a_1 : Type), % 39.89/40.15 Eq % 39.89/40.15 (∀ (B : Type) (R : a) (Q : B) (P : fun a (fun B a_1)), % 39.89/40.15 Eq (aa a a_1 (combc a B a_1 P Q) R) (aa B a_1 (aa a (fun B a_1) P R) Q)) % 39.89/40.15 True % 39.89/40.15 Clause #5106 (by clausification #[5105]): ∀ (a a_1 a_2 : Type), % 39.89/40.15 Eq % 39.89/40.15 (∀ (R : a) (Q : a_1) (P : fun a (fun a_1 a_2)), % 39.89/40.16 Eq (aa a a_2 (combc a a_1 a_2 P Q) R) (aa a_1 a_2 (aa a (fun a_1 a_2) P R) Q)) % 39.89/40.16 True % 39.89/40.16 Clause #5107 (by clausification #[5106]): ∀ (a a_1 a_2 : Type) (a_3 : a_1), % 39.89/40.16 Eq % 39.89/40.16 (∀ (Q : a) (P : fun a_1 (fun a a_2)), % 39.89/40.16 Eq (aa a_1 a_2 (combc a_1 a a_2 P Q) a_3) (aa a a_2 (aa a_1 (fun a a_2) P a_3) Q)) % 39.89/40.16 True % 39.89/40.16 Clause #5108 (by clausification #[5107]): ∀ (a a_1 a_2 : Type) (a_3 : a_1) (a_4 : a), % 39.89/40.16 Eq % 39.89/40.16 (∀ (P : fun a (fun a_1 a_2)), Eq (aa a a_2 (combc a a_1 a_2 P a_3) a_4) (aa a_1 a_2 (aa a (fun a_1 a_2) P a_4) a_3)) % 39.89/40.16 True % 39.89/40.16 Clause #5109 (by clausification #[5108]): ∀ (a a_1 a_2 : Type) (a_3 : fun a_1 (fun a_2 a)) (a_4 : a_2) (a_5 : a_1), % 39.89/40.16 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 (fun a_2 a) a_3 a_5) a_4)) True % 39.89/40.16 Clause #5110 (by clausification #[5109]): ∀ (a a_1 a_2 : Type) (a_3 : fun a_1 (fun a_2 a)) (a_4 : a_2) (a_5 : a_1), % 39.89/40.16 Eq (aa a_1 a (combc a_1 a_2 a a_3 a_4) a_5) (aa a_2 a (aa a_1 (fun a_2 a) a_3 a_5) a_4) % 39.89/40.16 Clause #5326 (by clausification #[108]): Eq % 39.89/40.16 (pp % 39.89/40.16 (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app (aa dB dB (aa dB (fun dB dB) app (abs r)) a) as)) % 39.89/40.16 (foldl dB dB app (subst r a (zero_zero nat)) as))) % 39.89/40.16 False % 39.89/40.16 Clause #5327 (by forward demodulation #[5326, 5110]): Eq % 39.89/40.16 (pp % 39.89/40.16 (aa dB bool (combc dB dB bool beta (foldl dB dB app (subst r a (zero_zero nat)) as)) % 39.89/40.16 (foldl dB dB app (aa dB dB (aa dB (fun dB dB) app (abs r)) a) as))) % 39.89/40.16 False % 39.89/40.16 Clause #5328 (by forward demodulation #[5327, 2207]): Eq % 39.89/40.16 (pp % 39.89/40.16 (aa dB bool (combc dB dB bool beta (foldl dB dB app (subst r a (zero_zero nat)) as)) % 39.89/40.16 (foldl dB dB app (abs r) (cons dB a as)))) % 39.89/40.16 False % 39.89/40.16 Clause #7059 (by clausification #[259]): ∀ (a a_1 : dB) (a_2 : list dB), % 39.89/40.16 Eq % 39.89/40.16 (pp % 39.89/40.16 (aa dB bool (aa dB (fun dB bool) beta (foldl dB dB app (aa dB dB (aa dB (fun dB dB) app (abs a)) a_1) a_2)) % 39.89/40.16 (foldl dB dB app (subst a a_1 (zero_zero nat)) a_2))) % 39.89/40.16 True % 39.89/40.16 Clause #7060 (by forward demodulation #[7059, 5110]): ∀ (a a_1 : dB) (a_2 : list dB), % 39.89/40.16 Eq % 39.89/40.16 (pp % 39.89/40.16 (aa dB bool (combc dB dB bool beta (foldl dB dB app (subst a a_1 (zero_zero nat)) a_2)) % 39.89/40.16 (foldl dB dB app (aa dB dB (aa dB (fun dB dB) app (abs a)) a_1) a_2))) % 39.89/40.16 True % 39.89/40.16 Clause #7061 (by forward demodulation #[7060, 2207]): ∀ (a a_1 : dB) (a_2 : list dB), % 39.89/40.16 Eq % 39.89/40.16 (pp % 39.89/40.16 (aa dB bool (combc dB dB bool beta (foldl dB dB app (subst a a_1 (zero_zero nat)) a_2)) % 39.89/40.16 (foldl dB dB app (abs a) (cons dB a_1 a_2)))) % 39.89/40.16 True % 39.89/40.16 Clause #7063 (by superposition #[7061, 5328]): Eq True False % 39.89/40.16 Clause #7143 (by clausification #[7063]): False % 39.89/40.16 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------