%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL769_5 : TPTP v9.3.1. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:36 AM UTC 2026 % Result : Theorem 68.26s 68.51s % Output : Proof 68.26s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL769_5 : TPTP v9.3.1. Released v6.0.0. % 0.00/0.05 % Command : duper %s % 0.10/0.36 % Computer : n002.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 22:10:06 UTC 2026 % 0.10/0.36 % CPUTime : % 68.26/68.51 SZS status Theorem for theBenchmark.p % 68.26/68.51 SZS output start Proof for theBenchmark.p % 68.26/68.51 Clause #0 (by assumption #[]): Eq (∀ (N2 : nat), pp (aa dB bool it (var N2))) True % 68.26/68.51 Clause #1 (by assumption #[]): Eq (∀ (A : Type) (A1 : fun A bool), listsp A A1 (nil A)) True % 68.26/68.51 Clause #10 (by assumption #[]): Eq % 68.26/68.51 (∀ (A : Type) (A2 : list A) (A1 : fun A bool), % 68.26/68.51 Iff (listsp A A1 A2) % 68.26/68.51 (Or (Eq A2 (nil A)) % 68.26/68.51 (Exists fun A4 => % 68.26/68.51 Exists fun L => % 68.26/68.51 And (And (Eq A2 (aa (list A) (list A) (aa A (fun (list A) (list A)) (cons A) A4) L)) (pp (aa A bool A1 A4))) % 68.26/68.51 (listsp A A1 L)))) % 68.26/68.51 True % 68.26/68.51 Clause #21 (by assumption #[]): Eq % 68.26/68.51 (∀ (A : Type) (X : A), % 68.26/68.51 Eq (insert A X (nil A)) (aa (list A) (list A) (aa A (fun (list A) (list A)) (cons A) X) (nil A))) % 68.26/68.51 True % 68.26/68.51 Clause #115 (by assumption #[]): Eq (Not (listsp dB it (aa (list dB) (list dB) (aa dB (fun (list dB) (list dB)) (cons dB) (var i)) (nil dB)))) True % 68.26/68.51 Clause #119 (by clausification #[1]): ∀ (a : Type), Eq (∀ (A1 : fun a bool), listsp a A1 (nil a)) True % 68.26/68.51 Clause #120 (by clausification #[119]): ∀ (a : Type) (a_1 : fun a bool), Eq (listsp a a_1 (nil a)) True % 68.26/68.51 Clause #121 (by clausification #[0]): ∀ (a : nat), Eq (pp (aa dB bool it (var a))) True % 68.26/68.51 Clause #361 (by clausification #[10]): ∀ (a : Type), % 68.26/68.51 Eq % 68.26/68.51 (∀ (A2 : list a) (A1 : fun a bool), % 68.26/68.51 Iff (listsp a A1 A2) % 68.26/68.51 (Or (Eq A2 (nil a)) % 68.26/68.51 (Exists fun A4 => % 68.26/68.51 Exists fun L => % 68.26/68.51 And % 68.26/68.51 (And (Eq A2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) A4) L)) (pp (aa a bool A1 A4))) % 68.26/68.51 (listsp a A1 L)))) % 68.26/68.51 True % 68.26/68.51 Clause #362 (by clausification #[361]): ∀ (a : Type) (a_1 : list a), % 68.26/68.51 Eq % 68.26/68.51 (∀ (A1 : fun a bool), % 68.26/68.51 Iff (listsp a A1 a_1) % 68.26/68.51 (Or (Eq a_1 (nil a)) % 68.26/68.51 (Exists fun A4 => % 68.26/68.51 Exists fun L => % 68.26/68.51 And % 68.26/68.51 (And (Eq a_1 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) A4) L)) % 68.26/68.51 (pp (aa a bool A1 A4))) % 68.26/68.51 (listsp a A1 L)))) % 68.26/68.51 True % 68.26/68.51 Clause #363 (by clausification #[362]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : list a), % 68.26/68.51 Eq % 68.26/68.51 (Iff (listsp a a_1 a_2) % 68.26/68.51 (Or (Eq a_2 (nil a)) % 68.26/68.51 (Exists fun A4 => % 68.26/68.51 Exists fun L => % 68.26/68.51 And % 68.26/68.51 (And (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) A4) L)) (pp (aa a bool a_1 A4))) % 68.26/68.51 (listsp a a_1 L)))) % 68.26/68.51 True % 68.26/68.51 Clause #364 (by clausification #[363]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : list a), % 68.26/68.51 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.51 (Eq % 68.26/68.51 (Or (Eq a_2 (nil a)) % 68.26/68.51 (Exists fun A4 => % 68.26/68.51 Exists fun L => % 68.26/68.51 And % 68.26/68.51 (And (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) A4) L)) (pp (aa a bool a_1 A4))) % 68.26/68.51 (listsp a a_1 L))) % 68.26/68.51 False) % 68.26/68.51 Clause #366 (by clausification #[364]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : list a), % 68.26/68.51 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.51 (Eq % 68.26/68.51 (Exists fun A4 => % 68.26/68.51 Exists fun L => % 68.26/68.51 And (And (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) A4) L)) (pp (aa a bool a_1 A4))) % 68.26/68.51 (listsp a a_1 L)) % 68.26/68.51 False) % 68.26/68.51 Clause #368 (by clausification #[366]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : list a) (a_3 : a), % 68.26/68.51 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.51 (Eq % 68.26/68.51 (Exists fun L => % 68.26/68.51 And (And (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_3) L)) (pp (aa a bool a_1 a_3))) % 68.26/68.51 (listsp a a_1 L)) % 68.26/68.51 False) % 68.26/68.51 Clause #369 (by clausification #[368]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : list a) (a_3 : a) (a_4 : list a), % 68.26/68.51 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.51 (Eq % 68.26/68.51 (And % 68.26/68.51 (And (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_3) a_4)) (pp (aa a bool a_1 a_3))) % 68.26/68.51 (listsp a a_1 a_4)) % 68.26/68.51 False) % 68.26/68.51 Clause #370 (by clausification #[369]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : list a) (a_3 : a) (a_4 : list a), % 68.26/68.51 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.51 (Or % 68.26/68.51 (Eq (And (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_3) a_4)) (pp (aa a bool a_1 a_3))) % 68.26/68.59 False) % 68.26/68.59 (Eq (listsp a a_1 a_4) False)) % 68.26/68.59 Clause #371 (by clausification #[370]): ∀ (a : Type) (a_1 : fun a bool) (a_2 a_3 : list a) (a_4 : a), % 68.26/68.59 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.59 (Or (Eq (listsp a a_1 a_3) False) % 68.26/68.59 (Or (Eq (Eq a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_4) a_3)) False) % 68.26/68.59 (Eq (pp (aa a bool a_1 a_4)) False))) % 68.26/68.59 Clause #372 (by clausification #[371]): ∀ (a : Type) (a_1 : fun a bool) (a_2 a_3 : list a) (a_4 : a), % 68.26/68.59 Or (Eq (listsp a a_1 a_2) True) % 68.26/68.59 (Or (Eq (listsp a a_1 a_3) False) % 68.26/68.59 (Or (Eq (pp (aa a bool a_1 a_4)) False) % 68.26/68.59 (Ne a_2 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_4) a_3)))) % 68.26/68.59 Clause #373 (by destructive equality resolution #[372]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : a) (a_3 : list a), % 68.26/68.59 Or (Eq (listsp a a_1 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_2) a_3)) True) % 68.26/68.59 (Or (Eq (listsp a a_1 a_3) False) (Eq (pp (aa a bool a_1 a_2)) False)) % 68.26/68.59 Clause #374 (by superposition #[373, 120]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : a), % 68.26/68.59 Or (Eq (listsp a a_1 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_2) (nil a))) True) % 68.26/68.59 (Or (Eq (pp (aa a bool a_1 a_2)) False) (Eq False True)) % 68.26/68.59 Clause #642 (by clausification #[21]): ∀ (a : Type), % 68.26/68.59 Eq (∀ (X : a), Eq (insert a X (nil a)) (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) X) (nil a))) True % 68.26/68.59 Clause #643 (by clausification #[642]): ∀ (a : Type) (a_1 : a), % 68.26/68.59 Eq (Eq (insert a a_1 (nil a)) (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_1) (nil a))) True % 68.26/68.59 Clause #644 (by clausification #[643]): ∀ (a : Type) (a_1 : a), % 68.26/68.59 Eq (insert a a_1 (nil a)) (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_1) (nil a)) % 68.26/68.59 Clause #2743 (by clausification #[115]): Eq (listsp dB it (aa (list dB) (list dB) (aa dB (fun (list dB) (list dB)) (cons dB) (var i)) (nil dB))) False % 68.26/68.59 Clause #2744 (by forward demodulation #[2743, 644]): Eq (listsp dB it (insert dB (var i) (nil dB))) False % 68.26/68.59 Clause #3445 (by clausification #[374]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : a), % 68.26/68.59 Or (Eq (listsp a a_1 (aa (list a) (list a) (aa a (fun (list a) (list a)) (cons a) a_2) (nil a))) True) % 68.26/68.59 (Eq (pp (aa a bool a_1 a_2)) False) % 68.26/68.59 Clause #3446 (by forward demodulation #[3445, 644]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : a), % 68.26/68.59 Or (Eq (listsp a a_1 (insert a a_2 (nil a))) True) (Eq (pp (aa a bool a_1 a_2)) False) % 68.26/68.59 Clause #3447 (by superposition #[3446, 121]): ∀ (a : nat), Or (Eq (listsp dB it (insert dB (var a) (nil dB))) True) (Eq False True) % 68.26/68.59 Clause #3501 (by clausification #[3447]): ∀ (a : nat), Eq (listsp dB it (insert dB (var a) (nil dB))) True % 68.26/68.59 Clause #3502 (by superposition #[3501, 2744]): Eq True False % 68.26/68.59 Clause #3513 (by clausification #[3502]): False % 68.26/68.59 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------