%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM047_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:45:50 PM UTC 2025 % Result : Theorem 44.02s 44.20s % Output : Proof 44.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.13 % Problem : COM047_5 : TPTP v9.2.0. Released v6.0.0. % 0.10/0.14 % Command : duper %s % 0.14/0.35 % Computer : n009.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu Oct 2 15:56:08 EDT 2025 % 0.14/0.35 % CPUTime : % 44.02/44.20 SZS status Theorem for theBenchmark.p % 44.02/44.20 SZS output start Proof for theBenchmark.p % 44.02/44.20 Clause #0 (by assumption #[]): Eq (Eq a (c_PresArith_Oatom_OLe int1 list1)) True % 44.02/44.20 Clause #3 (by assumption #[]): Eq % 44.02/44.20 (pp % 44.02/44.20 (atom_case bool % 44.02/44.20 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.20 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 44.02/44.20 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 44.02/44.20 (combk (fun int (fun (list int) bool)) int) % 44.02/44.20 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.20 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 44.02/44.20 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 44.02/44.20 (combk (fun int (fun (list int) bool)) int) % 44.02/44.20 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.20 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 44.02/44.20 a)) % 44.02/44.20 True % 44.02/44.20 Clause #16 (by assumption #[]): Eq % 44.02/44.20 (∀ (A : Type) (Lista : list int) (Inta : int) (F3 F2 : fun int (fun int (fun (list int) A))) % 44.02/44.20 (F1 : fun int (fun (list int) A)), % 44.02/44.20 Eq (atom_case A F1 F2 F3 (c_PresArith_Oatom_OLe Inta Lista)) % 44.02/44.20 (aa (list int) A (aa int (fun (list int) A) F1 Inta) Lista)) % 44.02/44.20 True % 44.02/44.20 Clause #107 (by assumption #[]): Eq (Not (pp fFalse)) True % 44.02/44.20 Clause #108 (by assumption #[]): Eq (pp fTrue) True % 44.02/44.20 Clause #112 (by assumption #[]): Eq (∀ (B A : Type) (Q : B) (P : A), Eq (aa B A (aa A (fun B A) (combk A B) P) Q) P) True % 44.02/44.20 Clause #114 (by assumption #[]): Eq (∀ (P : bool), Or (Eq P fTrue) (Eq P fFalse)) True % 44.02/44.20 Clause #121 (by clausification #[0]): Eq a (c_PresArith_Oatom_OLe int1 list1) % 44.02/44.20 Clause #123 (by clausification #[107]): Eq (pp fFalse) False % 44.02/44.20 Clause #193 (by clausification #[114]): ∀ (a : bool), Eq (Or (Eq a fTrue) (Eq a fFalse)) True % 44.02/44.20 Clause #194 (by clausification #[193]): ∀ (a : bool), Or (Eq (Eq a fTrue) True) (Eq (Eq a fFalse) True) % 44.02/44.20 Clause #195 (by clausification #[194]): ∀ (a : bool), Or (Eq (Eq a fFalse) True) (Eq a fTrue) % 44.02/44.20 Clause #196 (by clausification #[195]): ∀ (a : bool), Or (Eq a fTrue) (Eq a fFalse) % 44.02/44.20 Clause #197 (by superposition #[196, 108]): ∀ (a : bool), Or (Eq a fFalse) (Eq (pp a) True) % 44.02/44.20 Clause #223 (by superposition #[197, 196]): ∀ (a a_1 : bool), Or (Eq (pp a) True) (Or (Eq a_1 fTrue) (Eq a_1 a)) % 44.02/44.20 Clause #403 (by clausification #[16]): ∀ (a : Type), % 44.02/44.20 Eq % 44.02/44.20 (∀ (Lista : list int) (Inta : int) (F3 F2 : fun int (fun int (fun (list int) a))) (F1 : fun int (fun (list int) a)), % 44.02/44.20 Eq (atom_case a F1 F2 F3 (c_PresArith_Oatom_OLe Inta Lista)) % 44.02/44.20 (aa (list int) a (aa int (fun (list int) a) F1 Inta) Lista)) % 44.02/44.20 True % 44.02/44.20 Clause #404 (by clausification #[403]): ∀ (a : Type) (a_1 : list int), % 44.02/44.20 Eq % 44.02/44.20 (∀ (Inta : int) (F3 F2 : fun int (fun int (fun (list int) a))) (F1 : fun int (fun (list int) a)), % 44.02/44.20 Eq (atom_case a F1 F2 F3 (c_PresArith_Oatom_OLe Inta a_1)) % 44.02/44.20 (aa (list int) a (aa int (fun (list int) a) F1 Inta) a_1)) % 44.02/44.20 True % 44.02/44.20 Clause #405 (by clausification #[404]): ∀ (a : Type) (a_1 : int) (a_2 : list int), % 44.02/44.20 Eq % 44.02/44.20 (∀ (F3 F2 : fun int (fun int (fun (list int) a))) (F1 : fun int (fun (list int) a)), % 44.02/44.20 Eq (atom_case a F1 F2 F3 (c_PresArith_Oatom_OLe a_1 a_2)) % 44.02/44.20 (aa (list int) a (aa int (fun (list int) a) F1 a_1) a_2)) % 44.02/44.20 True % 44.02/44.20 Clause #406 (by clausification #[405]): ∀ (a : Type) (a_1 : fun int (fun int (fun (list int) a))) (a_2 : int) (a_3 : list int), % 44.02/44.20 Eq % 44.02/44.20 (∀ (F2 : fun int (fun int (fun (list int) a))) (F1 : fun int (fun (list int) a)), % 44.02/44.20 Eq (atom_case a F1 F2 a_1 (c_PresArith_Oatom_OLe a_2 a_3)) % 44.02/44.20 (aa (list int) a (aa int (fun (list int) a) F1 a_2) a_3)) % 44.02/44.20 True % 44.02/44.20 Clause #407 (by clausification #[406]): ∀ (a : Type) (a_1 a_2 : fun int (fun int (fun (list int) a))) (a_3 : int) (a_4 : list int), % 44.02/44.20 Eq % 44.02/44.20 (∀ (F1 : fun int (fun (list int) a)), % 44.02/44.20 Eq (atom_case a F1 a_1 a_2 (c_PresArith_Oatom_OLe a_3 a_4)) % 44.02/44.20 (aa (list int) a (aa int (fun (list int) a) F1 a_3) a_4)) % 44.02/44.20 True % 44.02/44.20 Clause #408 (by clausification #[407]): ∀ (a : Type) (a_1 : fun int (fun (list int) a)) (a_2 a_3 : fun int (fun int (fun (list int) a))) (a_4 : int) % 44.02/44.22 (a_5 : list int), % 44.02/44.22 Eq % 44.02/44.22 (Eq (atom_case a a_1 a_2 a_3 (c_PresArith_Oatom_OLe a_4 a_5)) % 44.02/44.22 (aa (list int) a (aa int (fun (list int) a) a_1 a_4) a_5)) % 44.02/44.22 True % 44.02/44.22 Clause #409 (by clausification #[408]): ∀ (a : Type) (a_1 : fun int (fun (list int) a)) (a_2 a_3 : fun int (fun int (fun (list int) a))) (a_4 : int) % 44.02/44.22 (a_5 : list int), % 44.02/44.22 Eq (atom_case a a_1 a_2 a_3 (c_PresArith_Oatom_OLe a_4 a_5)) (aa (list int) a (aa int (fun (list int) a) a_1 a_4) a_5) % 44.02/44.22 Clause #415 (by superposition #[409, 121]): ∀ (a_1 : Type) (a_2 : fun int (fun (list int) a_1)) (a_3 a_4 : fun int (fun int (fun (list int) a_1))), % 44.02/44.22 Eq (atom_case a_1 a_2 a_3 a_4 a) (aa (list int) a_1 (aa int (fun (list int) a_1) a_2 int1) list1) % 44.02/44.22 Clause #430 (by superposition #[223, 3]): ∀ (a_1 a_2 : bool), % 44.02/44.22 Or (Eq (pp a_1) True) % 44.02/44.22 (Or (Eq a_2 a_1) % 44.02/44.22 (Eq % 44.02/44.22 (pp % 44.02/44.22 (atom_case bool % 44.02/44.22 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.22 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 44.02/44.22 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 44.02/44.22 (combk (fun int (fun (list int) bool)) int) % 44.02/44.22 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.22 (aa bool (fun (list int) bool) (combk bool (list int)) a_2))) % 44.02/44.22 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 44.02/44.22 (combk (fun int (fun (list int) bool)) int) % 44.02/44.22 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.22 (aa bool (fun (list int) bool) (combk bool (list int)) a_2))) % 44.02/44.22 a)) % 44.02/44.22 True)) % 44.02/44.22 Clause #2705 (by clausification #[112]): ∀ (a : Type), Eq (∀ (A : Type) (Q : a) (P : A), Eq (aa a A (aa A (fun a A) (combk A a) P) Q) P) True % 44.02/44.22 Clause #2706 (by clausification #[2705]): ∀ (a a_1 : Type), Eq (∀ (Q : a) (P : a_1), Eq (aa a a_1 (aa a_1 (fun a a_1) (combk a_1 a) P) Q) P) True % 44.02/44.22 Clause #2707 (by clausification #[2706]): ∀ (a a_1 : Type) (a_2 : a_1), Eq (∀ (P : a), Eq (aa a_1 a (aa a (fun a_1 a) (combk a a_1) P) a_2) P) True % 44.02/44.22 Clause #2708 (by clausification #[2707]): ∀ (a a_1 : Type) (a_2 : a) (a_3 : a_1), Eq (Eq (aa a_1 a (aa a (fun a_1 a) (combk a a_1) a_2) a_3) a_2) True % 44.02/44.22 Clause #2709 (by clausification #[2708]): ∀ (a a_1 : Type) (a_2 : a) (a_3 : a_1), Eq (aa a_1 a (aa a (fun a_1 a) (combk a a_1) a_2) a_3) a_2 % 44.02/44.22 Clause #10700 (by forward demodulation #[430, 415]): ∀ (a a_1 : bool), % 44.02/44.22 Or (Eq (pp a) True) % 44.02/44.22 (Or (Eq a_1 a) % 44.02/44.22 (Eq % 44.02/44.22 (pp % 44.02/44.22 (aa (list int) bool % 44.02/44.22 (aa int (fun (list int) bool) % 44.02/44.22 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 44.02/44.22 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 44.02/44.22 int1) % 44.02/44.22 list1)) % 44.02/44.22 True)) % 44.02/44.22 Clause #10701 (by forward demodulation #[10700, 2709]): ∀ (a a_1 : bool), % 44.02/44.22 Or (Eq (pp a) True) % 44.02/44.22 (Or (Eq a_1 a) % 44.02/44.22 (Eq (pp (aa (list int) bool (aa bool (fun (list int) bool) (combk bool (list int)) fFalse) list1)) True)) % 44.02/44.22 Clause #10702 (by forward demodulation #[10701, 2709]): ∀ (a a_1 : bool), Or (Eq (pp a) True) (Or (Eq a_1 a) (Eq (pp fFalse) True)) % 44.02/44.22 Clause #10981 (by equality factoring #[10702]): ∀ (a : bool), Or (Eq a fFalse) (Or (Ne True True) (Eq (pp fFalse) True)) % 44.02/44.22 Clause #10982 (by clausification #[10981]): ∀ (a : bool), Or (Eq a fFalse) (Or (Eq (pp fFalse) True) (Or (Eq True False) (Eq True False))) % 44.02/44.22 Clause #10984 (by clausification #[10982]): ∀ (a : bool), Or (Eq a fFalse) (Or (Eq (pp fFalse) True) (Eq True False)) % 44.02/44.22 Clause #10985 (by clausification #[10984]): ∀ (a : bool), Or (Eq a fFalse) (Eq (pp fFalse) True) % 44.02/44.22 Clause #11063 (by superposition #[10985, 123]): ∀ (a : bool), Or (Eq a fFalse) (Eq True False) % 44.02/44.22 Clause #11143 (by clausification #[11063]): ∀ (a : bool), Eq a fFalse % 44.02/44.22 Clause #11201 (by superposition #[11143, 11143]): ∀ (a a_1 : bool), Eq a a_1 % 44.14/44.31 Clause #11202 (by superposition #[11201, 108]): ∀ (a : bool), Eq (pp a) True % 44.14/44.31 Clause #11247 (by superposition #[11202, 123]): Eq True False % 44.14/44.31 Clause #11250 (by clausification #[11247]): False % 44.14/44.31 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------