%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM088_5 : TPTP v9.2.0. 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 : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Fri Oct 3 07:45:52 PM UTC 2025 % Result : Theorem 27.48s 27.72s % Output : Proof 27.48s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : COM088_5 : TPTP v9.2.0. Released v6.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n016.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 15:54:23 EDT 2025 % 0.13/0.35 % CPUTime : % 27.48/27.72 SZS status Theorem for theBenchmark.p % 27.48/27.72 SZS output start Proof for theBenchmark.p % 27.48/27.72 Clause #1 (by assumption #[]): Eq (∀ (B A : Type) (H : fun A B) (F3 : fun A bool), finite_finite A F3 → finite_finite B (image A B H F3)) True % 27.48/27.72 Clause #2 (by assumption #[]): Eq (∀ (A : Type) (Xsa : list A), finite_finite A (set A Xsa)) True % 27.48/27.72 Clause #129 (by assumption #[]): Eq % 27.48/27.72 (Not % 27.48/27.72 (finite_finite int % 27.48/27.72 (image (product_prod int (list int)) int % 27.48/27.72 (aa (fun int (fun (list int) int)) (fun (product_prod int (list int)) int) % 27.48/27.72 (product_prod_case int (list int) int) % 27.48/27.72 (combc int (fun (list int) int) (fun (list int) int) % 27.48/27.72 (aa (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int))) % 27.48/27.72 (aa (fun (fun int int) (fun (fun (list int) int) (fun (list int) int))) % 27.48/27.72 (fun (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int)))) % 27.48/27.72 (combb (fun int int) (fun (fun (list int) int) (fun (list int) int)) int) (combb int int (list int))) % 27.48/27.72 (minus_minus int)) % 27.48/27.72 (combc (list int) (list int) int (iprod int) xs))) % 27.48/27.72 (set (product_prod int (list int)) (lbounds as))))) % 27.48/27.72 True % 27.48/27.72 Clause #131 (by clausification #[1]): ∀ (a : Type), % 27.48/27.72 Eq (∀ (A : Type) (H : fun A a) (F3 : fun A bool), finite_finite A F3 → finite_finite a (image A a H F3)) True % 27.48/27.72 Clause #132 (by clausification #[131]): ∀ (a a_1 : Type), % 27.48/27.72 Eq (∀ (H : fun a a_1) (F3 : fun a bool), finite_finite a F3 → finite_finite a_1 (image a a_1 H F3)) True % 27.48/27.72 Clause #133 (by clausification #[132]): ∀ (a a_1 : Type) (a_2 : fun a a_1), % 27.48/27.72 Eq (∀ (F3 : fun a bool), finite_finite a F3 → finite_finite a_1 (image a a_1 a_2 F3)) True % 27.48/27.72 Clause #134 (by clausification #[133]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : Type) (a_3 : fun a a_2), % 27.48/27.72 Eq (finite_finite a a_1 → finite_finite a_2 (image a a_2 a_3 a_1)) True % 27.48/27.72 Clause #135 (by clausification #[134]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : Type) (a_3 : fun a a_2), % 27.48/27.72 Or (Eq (finite_finite a a_1) False) (Eq (finite_finite a_2 (image a a_2 a_3 a_1)) True) % 27.48/27.72 Clause #146 (by clausification #[2]): ∀ (a : Type), Eq (∀ (Xsa : list a), finite_finite a (set a Xsa)) True % 27.48/27.72 Clause #147 (by clausification #[146]): ∀ (a : Type) (a_1 : list a), Eq (finite_finite a (set a a_1)) True % 27.48/27.72 Clause #148 (by superposition #[147, 135]): ∀ (a a_1 : Type) (a_2 : fun a_1 a) (a_3 : list a_1), % 27.48/27.72 Or (Eq True False) (Eq (finite_finite a (image a_1 a a_2 (set a_1 a_3))) True) % 27.48/27.72 Clause #457 (by clausification #[148]): ∀ (a a_1 : Type) (a_2 : fun a_1 a) (a_3 : list a_1), Eq (finite_finite a (image a_1 a a_2 (set a_1 a_3))) True % 27.48/27.72 Clause #6894 (by clausification #[129]): Eq % 27.48/27.72 (finite_finite int % 27.48/27.72 (image (product_prod int (list int)) int % 27.48/27.72 (aa (fun int (fun (list int) int)) (fun (product_prod int (list int)) int) (product_prod_case int (list int) int) % 27.48/27.72 (combc int (fun (list int) int) (fun (list int) int) % 27.48/27.72 (aa (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int))) % 27.48/27.72 (aa (fun (fun int int) (fun (fun (list int) int) (fun (list int) int))) % 27.48/27.72 (fun (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int)))) % 27.48/27.72 (combb (fun int int) (fun (fun (list int) int) (fun (list int) int)) int) (combb int int (list int))) % 27.48/27.72 (minus_minus int)) % 27.48/27.72 (combc (list int) (list int) int (iprod int) xs))) % 27.48/27.72 (set (product_prod int (list int)) (lbounds as)))) % 27.48/27.72 False % 27.48/27.72 Clause #6895 (by superposition #[6894, 457]): Eq False True % 27.48/27.72 Clause #6896 (by clausification #[6895]): False % 27.48/27.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------