%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL802_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:41 AM UTC 2026 % Result : Theorem 85.34s 85.61s % Output : Proof 85.44s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL802_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.04 % Command : duper %s % 0.10/0.37 % Computer : n016.cluster.edu % 0.10/0.37 % Model : x86_64 x86_64 % 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.37 % Memory : 8046.5625MB % 0.10/0.37 % OS : Linux 6.8.0-71-generic % 0.10/0.37 % CPULimit : 300 % 0.10/0.37 % WCLimit : 300 % 0.10/0.37 % DateTime : Fri Sep 4 19:40:13 UTC 2026 % 0.10/0.37 % CPUTime : % 85.34/85.61 SZS status Theorem for theBenchmark.p % 85.34/85.61 SZS output start Proof for theBenchmark.p % 85.34/85.61 Clause #2 (by assumption #[]): Eq (pp (aa (list type) bool (typings (shift type e i t) as) ts)) True % 85.34/85.61 Clause #7 (by assumption #[]): Eq % 85.34/85.61 (∀ (Tsa : list type) (Ts : list dB) (Eb : fun nat type), % 85.34/85.61 pp (aa (list type) bool (typings Eb Ts) Tsa) → % 85.34/85.61 listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing Eb)) % 85.34/85.61 Ts) % 85.34/85.61 True % 85.34/85.61 Clause #104 (by assumption #[]): Eq % 85.34/85.61 (∀ (A C B : Type) (R : A) (Q : B) (P : fun A (fun B C)), % 85.34/85.61 Eq (aa A C (combc A B C P Q) R) (aa B C (aa A (fun B C) P R) Q)) % 85.34/85.61 True % 85.34/85.61 Clause #112 (by assumption #[]): Eq % 85.34/85.61 (Not % 85.34/85.61 (listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing (shift type e i t))) % 85.34/85.61 as)) % 85.34/85.61 True % 85.34/85.61 Clause #212 (by clausification #[7]): ∀ (a : list type), % 85.34/85.61 Eq % 85.34/85.61 (∀ (Ts : list dB) (Eb : fun nat type), % 85.34/85.61 pp (aa (list type) bool (typings Eb Ts) a) → % 85.34/85.61 listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing Eb)) % 85.34/85.61 Ts) % 85.34/85.61 True % 85.34/85.61 Clause #213 (by clausification #[212]): ∀ (a : list dB) (a_1 : list type), % 85.34/85.61 Eq % 85.34/85.61 (∀ (Eb : fun nat type), % 85.34/85.61 pp (aa (list type) bool (typings Eb a) a_1) → % 85.34/85.61 listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing Eb)) % 85.34/85.61 a) % 85.34/85.61 True % 85.34/85.61 Clause #214 (by clausification #[213]): ∀ (a : fun nat type) (a_1 : list dB) (a_2 : list type), % 85.34/85.61 Eq % 85.34/85.61 (pp (aa (list type) bool (typings a a_1) a_2) → % 85.34/85.61 listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing a)) % 85.34/85.61 a_1) % 85.34/85.61 True % 85.34/85.61 Clause #215 (by clausification #[214]): ∀ (a : fun nat type) (a_1 : list dB) (a_2 : list type), % 85.34/85.61 Or (Eq (pp (aa (list type) bool (typings a a_1) a_2)) False) % 85.34/85.61 (Eq % 85.34/85.61 (listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing a)) % 85.34/85.61 a_1) % 85.34/85.61 True) % 85.34/85.61 Clause #216 (by superposition #[215, 2]): Or % 85.34/85.61 (Eq % 85.34/85.61 (listsp dB % 85.34/85.61 (aa (fun dB (fun type bool)) (fun dB bool) % 85.34/85.61 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.34/85.61 (fEx type)) % 85.34/85.61 (typing (shift type e i t))) % 85.34/85.61 as) % 85.34/85.61 True) % 85.34/85.61 (Eq False True) % 85.34/85.61 Clause #6548 (by clausification #[104]): ∀ (a : Type), % 85.34/85.61 Eq % 85.34/85.61 (∀ (C B : Type) (R : a) (Q : B) (P : fun a (fun B C)), % 85.34/85.61 Eq (aa a C (combc a B C P Q) R) (aa B C (aa a (fun B C) P R) Q)) % 85.34/85.61 True % 85.34/85.61 Clause #6549 (by clausification #[6548]): ∀ (a a_1 : Type), % 85.34/85.61 Eq % 85.34/85.61 (∀ (B : Type) (R : a) (Q : B) (P : fun a (fun B a_1)), % 85.34/85.61 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)) % 85.34/85.61 True % 85.34/85.61 Clause #6550 (by clausification #[6549]): ∀ (a a_1 a_2 : Type), % 85.34/85.61 Eq % 85.34/85.61 (∀ (R : a) (Q : a_1) (P : fun a (fun a_1 a_2)), % 85.34/85.61 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)) % 85.34/85.61 True % 85.34/85.61 Clause #6551 (by clausification #[6550]): ∀ (a a_1 a_2 : Type) (a_3 : a_1), % 85.34/85.61 Eq % 85.34/85.61 (∀ (Q : a) (P : fun a_1 (fun a a_2)), % 85.34/85.61 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)) % 85.34/85.61 True % 85.34/85.61 Clause #6552 (by clausification #[6551]): ∀ (a a_1 a_2 : Type) (a_3 : a_1) (a_4 : a), % 85.34/85.61 Eq % 85.34/85.61 (∀ (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)) % 85.44/85.73 True % 85.44/85.73 Clause #6553 (by clausification #[6552]): ∀ (a a_1 a_2 : Type) (a_3 : fun a_1 (fun a_2 a)) (a_4 : a_2) (a_5 : a_1), % 85.44/85.73 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 % 85.44/85.73 Clause #6554 (by clausification #[6553]): ∀ (a a_1 a_2 : Type) (a_3 : fun a_1 (fun a_2 a)) (a_4 : a_2) (a_5 : a_1), % 85.44/85.73 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) % 85.44/85.73 Clause #7775 (by clausification #[112]): Eq % 85.44/85.73 (listsp dB % 85.44/85.73 (aa (fun dB (fun type bool)) (fun dB bool) % 85.44/85.73 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.44/85.73 (fEx type)) % 85.44/85.73 (typing (shift type e i t))) % 85.44/85.73 as) % 85.44/85.73 False % 85.44/85.73 Clause #7776 (by forward demodulation #[7775, 6554]): Eq % 85.44/85.73 (listsp dB % 85.44/85.73 (aa (fun (fun type bool) bool) (fun dB bool) % 85.44/85.73 (combc (fun (fun type bool) bool) (fun dB (fun type bool)) (fun dB bool) (combb (fun type bool) bool dB) % 85.44/85.73 (typing (shift type e i t))) % 85.44/85.73 (fEx type)) % 85.44/85.73 as) % 85.44/85.73 False % 85.44/85.73 Clause #9775 (by clausification #[216]): Eq % 85.44/85.73 (listsp dB % 85.44/85.73 (aa (fun dB (fun type bool)) (fun dB bool) % 85.44/85.73 (aa (fun (fun type bool) bool) (fun (fun dB (fun type bool)) (fun dB bool)) (combb (fun type bool) bool dB) % 85.44/85.73 (fEx type)) % 85.44/85.73 (typing (shift type e i t))) % 85.44/85.73 as) % 85.44/85.73 True % 85.44/85.73 Clause #9776 (by forward demodulation #[9775, 6554]): Eq % 85.44/85.73 (listsp dB % 85.44/85.73 (aa (fun (fun type bool) bool) (fun dB bool) % 85.44/85.73 (combc (fun (fun type bool) bool) (fun dB (fun type bool)) (fun dB bool) (combb (fun type bool) bool dB) % 85.44/85.73 (typing (shift type e i t))) % 85.44/85.73 (fEx type)) % 85.44/85.73 as) % 85.44/85.73 True % 85.44/85.73 Clause #9777 (by superposition #[9776, 7776]): Eq True False % 85.44/85.73 Clause #9779 (by clausification #[9777]): False % 85.44/85.73 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------