%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM090_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n007.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:53 PM UTC 2025 % Result : Theorem 92.36s 92.53s % Output : Proof 92.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : COM090_5 : TPTP v9.2.0. Released v6.0.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n007.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:56:53 EDT 2025 % 0.13/0.34 % CPUTime : % 92.36/92.53 SZS status Theorem for theBenchmark.p % 92.36/92.53 SZS output start Proof for theBenchmark.p % 92.36/92.53 Clause #2 (by assumption #[]): Eq (∀ (A : Type) (Xsa : list A), finite_finite A (set A Xsa)) True % 92.36/92.53 Clause #5 (by assumption #[]): Eq % 92.36/92.53 (Eq % 92.36/92.53 (image (product_prod int (list int)) int % 92.36/92.53 (aa (fun int (fun (list int) int)) (fun (product_prod int (list int)) int) (product_prod_case int (list int) int) % 92.36/92.53 (aa (fun (list int) int) (fun int (fun (list int) int)) % 92.36/92.53 (aa (fun int (fun (fun (list int) int) (fun (list int) int))) % 92.36/92.53 (fun (fun (list int) int) (fun int (fun (list int) int))) % 92.36/92.53 (combc int (fun (list int) int) (fun (list int) int)) % 92.36/92.53 (aa (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int))) % 92.36/92.53 (aa (fun (fun int int) (fun (fun (list int) int) (fun (list int) int))) % 92.36/92.53 (fun (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int)))) % 92.36/92.53 (combb (fun int int) (fun (fun (list int) int) (fun (list int) int)) int) (combb int int (list int))) % 92.36/92.53 (minus_minus int))) % 92.36/92.53 (aa (list int) (fun (list int) int) % 92.36/92.53 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.36/92.53 (combc (list int) (list int) int) (iprod int)) % 92.36/92.53 xs))) % 92.36/92.53 (set (product_prod int (list int)) (lbounds as))) % 92.36/92.53 (collect int % 92.36/92.53 (aa (fun int (fun (list int) bool)) (fun int bool) % 92.36/92.53 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 92.36/92.53 (combb (fun (list int) bool) bool int) (fEx (list int))) % 92.36/92.53 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 92.36/92.53 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.36/92.53 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 92.36/92.53 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 92.36/92.53 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.36/92.53 (combb (fun int bool) bool (list int)) (fEx int))) % 92.36/92.53 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 92.36/92.53 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.36/92.53 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 92.36/92.53 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 92.36/92.53 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.53 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.36/92.53 (aa % 92.36/92.53 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 92.36/92.53 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.36/92.53 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.53 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 92.36/92.53 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 92.36/92.53 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 92.36/92.53 (combs (list int) (fun int bool) (fun int bool))) % 92.36/92.53 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 92.36/92.53 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.53 (aa % 92.36/92.53 (fun (fun (list int) (fun int (fun bool bool))) % 92.36/92.53 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.53 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 92.36/92.53 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 92.36/92.53 (combb (fun (list int) (fun int (fun bool bool))) % 92.36/92.53 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 92.36/92.53 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 92.36/92.53 (fun (fun (list int) (fun int (fun bool bool))) % 92.36/92.53 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.53 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 92.36/92.53 (combs int bool bool))) % 92.36/92.53 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) (fun int (fun bool bool)))) % 92.36/92.53 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.36/92.53 (fun (fun int (fun (list int) (fun int bool))) % 92.36/92.53 (fun int (fun (list int) (fun int (fun bool bool))))) % 92.36/92.53 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 92.36/92.53 (aa (fun (fun int bool) (fun int (fun bool bool))) % 92.36/92.53 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.36/92.53 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 92.36/92.53 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 92.36/92.53 (combb bool (fun bool bool) int) fconj))) % 92.36/92.53 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 92.36/92.53 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.36/92.53 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 92.36/92.53 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 92.36/92.53 (aa (fun int (fun (fun int int) (fun int bool))) % 92.36/92.53 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.36/92.53 (aa % 92.36/92.53 (fun (fun (fun int int) (fun int bool)) % 92.36/92.53 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.36/92.53 (fun (fun int (fun (fun int int) (fun int bool))) % 92.36/92.53 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 92.36/92.53 (combb (fun (fun int int) (fun int bool)) % 92.36/92.53 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 92.36/92.53 (combb (fun int int) (fun int bool) (list int))) % 92.36/92.53 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 92.36/92.53 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 92.36/92.53 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 92.36/92.53 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) (combb int bool int)) % 92.36/92.53 (fequal int)))) % 92.36/92.53 (aa (fun (list int) int) (fun (list int) (fun int int)) % 92.36/92.53 (aa (fun int (fun int int)) (fun (fun (list int) int) (fun (list int) (fun int int))) % 92.36/92.53 (combb int (fun int int) (list int)) % 92.36/92.53 (aa (fun int (fun int int)) (fun int (fun int int)) (combc int int int) (minus_minus int))) % 92.36/92.53 (aa (list int) (fun (list int) int) % 92.36/92.53 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.36/92.53 (combc (list int) (list int) int) (iprod int)) % 92.36/92.53 xs))))))) % 92.36/92.53 (aa (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool)) % 92.36/92.53 (aa (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.36/92.53 (fun (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool))) % 92.36/92.53 (combc (list int) (fun (product_prod int (list int)) bool) (fun int bool)) % 92.36/92.53 (aa (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.36/92.53 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.36/92.53 (aa % 92.36/92.53 (fun (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.36/92.57 (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.36/92.57 (fun (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.36/92.57 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool)))) % 92.36/92.57 (combb (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.36/92.57 (fun (fun (product_prod int (list int)) bool) (fun int bool)) (list int)) % 92.36/92.57 (combc int (fun (product_prod int (list int)) bool) bool)) % 92.36/92.57 (aa (fun (list int) (fun int (product_prod int (list int)))) % 92.36/92.57 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.36/92.57 (aa % 92.36/92.57 (fun (fun int (product_prod int (list int))) % 92.36/92.57 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.36/92.57 (fun (fun (list int) (fun int (product_prod int (list int)))) % 92.36/92.57 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool)))) % 92.36/92.57 (combb (fun int (product_prod int (list int))) % 92.36/92.57 (fun int (fun (fun (product_prod int (list int)) bool) bool)) (list int)) % 92.36/92.57 (aa (fun (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool)) % 92.36/92.57 (fun (fun int (product_prod int (list int))) % 92.36/92.57 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.36/92.57 (combb (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool) int) % 92.36/92.57 (member (product_prod int (list int))))) % 92.36/92.57 (aa (fun int (fun (list int) (product_prod int (list int)))) % 92.36/92.57 (fun (list int) (fun int (product_prod int (list int)))) % 92.36/92.57 (combc int (list int) (product_prod int (list int))) (product_Pair int (list int)))))) % 92.36/92.57 (set (product_prod int (list int)) (lbounds as)))))))) % 92.36/92.57 True % 92.36/92.57 Clause #15 (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 % 92.36/92.57 Clause #127 (by assumption #[]): Eq % 92.36/92.57 (Not % 92.36/92.57 (finite_finite int % 92.36/92.57 (collect int % 92.36/92.57 (aa (fun int (fun (list int) bool)) (fun int bool) % 92.36/92.57 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 92.36/92.57 (combb (fun (list int) bool) bool int) (fEx (list int))) % 92.36/92.57 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 92.36/92.57 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.36/92.57 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 92.36/92.57 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 92.36/92.57 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.36/92.57 (combb (fun int bool) bool (list int)) (fEx int))) % 92.36/92.57 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 92.36/92.57 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.36/92.57 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 92.36/92.57 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 92.36/92.57 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.57 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.36/92.57 (aa % 92.36/92.57 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 92.36/92.57 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.36/92.57 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.57 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 92.36/92.57 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 92.36/92.57 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 92.36/92.57 (combs (list int) (fun int bool) (fun int bool))) % 92.36/92.57 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 92.36/92.57 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.57 (aa % 92.36/92.57 (fun (fun (list int) (fun int (fun bool bool))) % 92.36/92.57 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.57 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 92.36/92.57 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 92.36/92.57 (combb (fun (list int) (fun int (fun bool bool))) % 92.36/92.57 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 92.36/92.57 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 92.36/92.57 (fun (fun (list int) (fun int (fun bool bool))) % 92.36/92.57 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.36/92.57 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 92.36/92.57 (combs int bool bool))) % 92.36/92.57 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) (fun int (fun bool bool)))) % 92.36/92.57 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.36/92.57 (fun (fun int (fun (list int) (fun int bool))) % 92.36/92.57 (fun int (fun (list int) (fun int (fun bool bool))))) % 92.36/92.57 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 92.36/92.57 (aa (fun (fun int bool) (fun int (fun bool bool))) % 92.36/92.57 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.36/92.57 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 92.36/92.57 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 92.36/92.57 (combb bool (fun bool bool) int) fconj))) % 92.36/92.57 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 92.36/92.57 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.36/92.57 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 92.36/92.57 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 92.36/92.57 (aa (fun int (fun (fun int int) (fun int bool))) % 92.36/92.57 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.36/92.57 (aa % 92.36/92.57 (fun (fun (fun int int) (fun int bool)) % 92.36/92.57 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.36/92.57 (fun (fun int (fun (fun int int) (fun int bool))) % 92.36/92.57 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 92.36/92.57 (combb (fun (fun int int) (fun int bool)) % 92.36/92.57 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 92.36/92.57 (combb (fun int int) (fun int bool) (list int))) % 92.36/92.57 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 92.36/92.57 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 92.36/92.57 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 92.36/92.57 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) (combb int bool int)) % 92.36/92.57 (fequal int)))) % 92.36/92.57 (aa (fun (list int) int) (fun (list int) (fun int int)) % 92.36/92.57 (aa (fun int (fun int int)) (fun (fun (list int) int) (fun (list int) (fun int int))) % 92.36/92.57 (combb int (fun int int) (list int)) % 92.36/92.57 (aa (fun int (fun int int)) (fun int (fun int int)) (combc int int int) (minus_minus int))) % 92.43/92.61 (aa (list int) (fun (list int) int) % 92.43/92.61 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.43/92.61 (combc (list int) (list int) int) (iprod int)) % 92.43/92.61 xs))))))) % 92.43/92.61 (aa (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool)) % 92.43/92.61 (aa (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.61 (fun (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool))) % 92.43/92.61 (combc (list int) (fun (product_prod int (list int)) bool) (fun int bool)) % 92.43/92.61 (aa (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.61 (fun (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool)))) % 92.43/92.61 (combb (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (fun (fun (product_prod int (list int)) bool) (fun int bool)) (list int)) % 92.43/92.61 (combc int (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (aa (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.61 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun int (product_prod int (list int))) % 92.43/92.61 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (fun (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.61 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool)))) % 92.43/92.61 (combb (fun int (product_prod int (list int))) % 92.43/92.61 (fun int (fun (fun (product_prod int (list int)) bool) bool)) (list int)) % 92.43/92.61 (aa (fun (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (fun (fun int (product_prod int (list int))) % 92.43/92.61 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (combb (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool) int) % 92.43/92.61 (member (product_prod int (list int))))) % 92.43/92.61 (aa (fun int (fun (list int) (product_prod int (list int)))) % 92.43/92.61 (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.61 (combc int (list int) (product_prod int (list int))) (product_Pair int (list int)))))) % 92.43/92.61 (set (product_prod int (list int)) (lbounds as))))))))) % 92.43/92.61 True % 92.43/92.61 Clause #139 (by clausification #[2]): ∀ (a : Type), Eq (∀ (Xsa : list a), finite_finite a (set a Xsa)) True % 92.43/92.61 Clause #140 (by clausification #[139]): ∀ (a : Type) (a_1 : list a), Eq (finite_finite a (set a a_1)) True % 92.43/92.61 Clause #191 (by clausification #[5]): Eq % 92.43/92.61 (image (product_prod int (list int)) int % 92.43/92.61 (aa (fun int (fun (list int) int)) (fun (product_prod int (list int)) int) (product_prod_case int (list int) int) % 92.43/92.61 (aa (fun (list int) int) (fun int (fun (list int) int)) % 92.43/92.61 (aa (fun int (fun (fun (list int) int) (fun (list int) int))) % 92.43/92.61 (fun (fun (list int) int) (fun int (fun (list int) int))) % 92.43/92.61 (combc int (fun (list int) int) (fun (list int) int)) % 92.43/92.61 (aa (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int))) % 92.43/92.61 (aa (fun (fun int int) (fun (fun (list int) int) (fun (list int) int))) % 92.43/92.61 (fun (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int)))) % 92.43/92.61 (combb (fun int int) (fun (fun (list int) int) (fun (list int) int)) int) (combb int int (list int))) % 92.43/92.61 (minus_minus int))) % 92.43/92.61 (aa (list int) (fun (list int) int) % 92.43/92.61 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.43/92.61 (combc (list int) (list int) int) (iprod int)) % 92.43/92.61 xs))) % 92.43/92.61 (set (product_prod int (list int)) (lbounds as))) % 92.43/92.61 (collect int % 92.43/92.61 (aa (fun int (fun (list int) bool)) (fun int bool) % 92.43/92.61 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 92.43/92.61 (combb (fun (list int) bool) bool int) (fEx (list int))) % 92.43/92.61 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 92.43/92.61 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.43/92.61 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 92.43/92.61 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 92.43/92.61 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.43/92.61 (combb (fun int bool) bool (list int)) (fEx int))) % 92.43/92.61 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 92.43/92.61 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.43/92.61 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 92.43/92.61 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 92.43/92.61 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.61 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 92.43/92.61 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.43/92.61 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.61 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 92.43/92.61 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 92.43/92.61 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 92.43/92.61 (combs (list int) (fun int bool) (fun int bool))) % 92.43/92.61 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 92.43/92.61 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun (list int) (fun int (fun bool bool))) (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.61 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 92.43/92.61 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 92.43/92.61 (combb (fun (list int) (fun int (fun bool bool))) (fun (list int) (fun (fun int bool) (fun int bool))) % 92.43/92.61 int) % 92.43/92.61 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 92.43/92.61 (fun (fun (list int) (fun int (fun bool bool))) % 92.43/92.61 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.61 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 92.43/92.61 (combs int bool bool))) % 92.43/92.61 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) (fun int (fun bool bool)))) % 92.43/92.61 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.43/92.61 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) (fun int (fun bool bool))))) % 92.43/92.61 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 92.43/92.61 (aa (fun (fun int bool) (fun int (fun bool bool))) % 92.43/92.61 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.43/92.61 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 92.43/92.61 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 92.43/92.61 (combb bool (fun bool bool) int) fconj))) % 92.43/92.61 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 92.43/92.61 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.43/92.61 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 92.43/92.61 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 92.43/92.61 (aa (fun int (fun (fun int int) (fun int bool))) % 92.43/92.61 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun (fun int int) (fun int bool)) % 92.43/92.61 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.43/92.61 (fun (fun int (fun (fun int int) (fun int bool))) % 92.43/92.61 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 92.43/92.61 (combb (fun (fun int int) (fun int bool)) % 92.43/92.61 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 92.43/92.61 (combb (fun int int) (fun int bool) (list int))) % 92.43/92.61 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 92.43/92.61 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 92.43/92.61 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 92.43/92.61 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) (combb int bool int)) % 92.43/92.61 (fequal int)))) % 92.43/92.61 (aa (fun (list int) int) (fun (list int) (fun int int)) % 92.43/92.61 (aa (fun int (fun int int)) (fun (fun (list int) int) (fun (list int) (fun int int))) % 92.43/92.61 (combb int (fun int int) (list int)) % 92.43/92.61 (aa (fun int (fun int int)) (fun int (fun int int)) (combc int int int) (minus_minus int))) % 92.43/92.61 (aa (list int) (fun (list int) int) % 92.43/92.61 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.43/92.61 (combc (list int) (list int) int) (iprod int)) % 92.43/92.61 xs))))))) % 92.43/92.61 (aa (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool)) % 92.43/92.61 (aa (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.61 (fun (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool))) % 92.43/92.61 (combc (list int) (fun (product_prod int (list int)) bool) (fun int bool)) % 92.43/92.61 (aa (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.61 (fun (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool)))) % 92.43/92.61 (combb (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (fun (fun (product_prod int (list int)) bool) (fun int bool)) (list int)) % 92.43/92.61 (combc int (fun (product_prod int (list int)) bool) bool)) % 92.43/92.61 (aa (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.61 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (aa % 92.43/92.61 (fun (fun int (product_prod int (list int))) % 92.43/92.61 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.61 (fun (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.61 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool)))) % 92.43/92.61 (combb (fun int (product_prod int (list int))) % 92.43/92.66 (fun int (fun (fun (product_prod int (list int)) bool) bool)) (list int)) % 92.43/92.66 (aa (fun (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.66 (fun (fun int (product_prod int (list int))) % 92.43/92.66 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.66 (combb (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool) int) % 92.43/92.66 (member (product_prod int (list int))))) % 92.43/92.66 (aa (fun int (fun (list int) (product_prod int (list int)))) % 92.43/92.66 (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.66 (combc int (list int) (product_prod int (list int))) (product_Pair int (list int)))))) % 92.43/92.66 (set (product_prod int (list int)) (lbounds as))))))) % 92.43/92.66 Clause #539 (by clausification #[15]): ∀ (a : Type), % 92.43/92.66 Eq (∀ (A : Type) (H : fun A a) (F3 : fun A bool), finite_finite A F3 → finite_finite a (image A a H F3)) True % 92.43/92.66 Clause #540 (by clausification #[539]): ∀ (a a_1 : Type), % 92.43/92.66 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 % 92.43/92.66 Clause #541 (by clausification #[540]): ∀ (a a_1 : Type) (a_2 : fun a a_1), % 92.43/92.66 Eq (∀ (F3 : fun a bool), finite_finite a F3 → finite_finite a_1 (image a a_1 a_2 F3)) True % 92.43/92.66 Clause #542 (by clausification #[541]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : Type) (a_3 : fun a a_2), % 92.43/92.66 Eq (finite_finite a a_1 → finite_finite a_2 (image a a_2 a_3 a_1)) True % 92.43/92.66 Clause #543 (by clausification #[542]): ∀ (a : Type) (a_1 : fun a bool) (a_2 : Type) (a_3 : fun a a_2), % 92.43/92.66 Or (Eq (finite_finite a a_1) False) (Eq (finite_finite a_2 (image a a_2 a_3 a_1)) True) % 92.43/92.66 Clause #545 (by superposition #[543, 140]): ∀ (a a_1 : Type) (a_2 : fun a_1 a) (a_3 : list a_1), % 92.43/92.66 Or (Eq (finite_finite a (image a_1 a a_2 (set a_1 a_3))) True) (Eq False True) % 92.43/92.66 Clause #564 (by clausification #[545]): ∀ (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 % 92.43/92.66 Clause #8648 (by clausification #[127]): Eq % 92.43/92.66 (finite_finite int % 92.43/92.66 (collect int % 92.43/92.66 (aa (fun int (fun (list int) bool)) (fun int bool) % 92.43/92.66 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 92.43/92.66 (combb (fun (list int) bool) bool int) (fEx (list int))) % 92.43/92.66 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 92.43/92.66 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.43/92.66 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 92.43/92.66 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 92.43/92.66 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 92.43/92.66 (combb (fun int bool) bool (list int)) (fEx int))) % 92.43/92.66 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 92.43/92.66 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.43/92.66 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 92.43/92.66 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 92.43/92.66 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.66 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.43/92.66 (aa % 92.43/92.66 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 92.43/92.66 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 92.43/92.66 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.66 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 92.43/92.66 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 92.43/92.66 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 92.43/92.66 (combs (list int) (fun int bool) (fun int bool))) % 92.43/92.66 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 92.43/92.66 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.66 (aa % 92.43/92.66 (fun (fun (list int) (fun int (fun bool bool))) % 92.43/92.66 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.66 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 92.43/92.66 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 92.43/92.66 (combb (fun (list int) (fun int (fun bool bool))) % 92.43/92.66 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 92.43/92.66 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 92.43/92.66 (fun (fun (list int) (fun int (fun bool bool))) % 92.43/92.66 (fun (list int) (fun (fun int bool) (fun int bool)))) % 92.43/92.66 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 92.43/92.66 (combs int bool bool))) % 92.43/92.66 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) (fun int (fun bool bool)))) % 92.43/92.66 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.43/92.66 (fun (fun int (fun (list int) (fun int bool))) % 92.43/92.66 (fun int (fun (list int) (fun int (fun bool bool))))) % 92.43/92.66 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 92.43/92.66 (aa (fun (fun int bool) (fun int (fun bool bool))) % 92.43/92.66 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 92.43/92.66 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 92.43/92.66 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 92.43/92.66 (combb bool (fun bool bool) int) fconj))) % 92.43/92.66 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 92.43/92.66 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.43/92.66 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 92.43/92.66 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 92.43/92.66 (aa (fun int (fun (fun int int) (fun int bool))) % 92.43/92.66 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.43/92.66 (aa % 92.43/92.66 (fun (fun (fun int int) (fun int bool)) % 92.43/92.66 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 92.43/92.66 (fun (fun int (fun (fun int int) (fun int bool))) % 92.43/92.66 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 92.43/92.66 (combb (fun (fun int int) (fun int bool)) % 92.43/92.66 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 92.43/92.66 (combb (fun int int) (fun int bool) (list int))) % 92.43/92.66 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 92.43/92.66 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 92.43/92.66 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 92.43/92.66 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) (combb int bool int)) % 92.43/92.66 (fequal int)))) % 92.43/92.66 (aa (fun (list int) int) (fun (list int) (fun int int)) % 92.43/92.66 (aa (fun int (fun int int)) (fun (fun (list int) int) (fun (list int) (fun int int))) % 92.43/92.66 (combb int (fun int int) (list int)) % 92.43/92.66 (aa (fun int (fun int int)) (fun int (fun int int)) (combc int int int) (minus_minus int))) % 92.43/92.66 (aa (list int) (fun (list int) int) % 92.43/92.66 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.43/92.66 (combc (list int) (list int) int) (iprod int)) % 92.43/92.66 xs))))))) % 92.43/92.66 (aa (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool)) % 92.43/92.66 (aa (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.66 (fun (fun (product_prod int (list int)) bool) (fun (list int) (fun int bool))) % 92.43/92.66 (combc (list int) (fun (product_prod int (list int)) bool) (fun int bool)) % 92.43/92.66 (aa (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.66 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.66 (aa % 92.43/92.66 (fun (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.66 (fun (fun (product_prod int (list int)) bool) (fun int bool))) % 92.43/92.66 (fun (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.66 (fun (list int) (fun (fun (product_prod int (list int)) bool) (fun int bool)))) % 92.43/92.66 (combb (fun int (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.66 (fun (fun (product_prod int (list int)) bool) (fun int bool)) (list int)) % 92.43/92.66 (combc int (fun (product_prod int (list int)) bool) bool)) % 92.43/92.66 (aa (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.66 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.66 (aa % 92.43/92.66 (fun (fun int (product_prod int (list int))) % 92.43/92.66 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.66 (fun (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.66 (fun (list int) (fun int (fun (fun (product_prod int (list int)) bool) bool)))) % 92.43/92.66 (combb (fun int (product_prod int (list int))) % 92.43/92.66 (fun int (fun (fun (product_prod int (list int)) bool) bool)) (list int)) % 92.43/92.66 (aa (fun (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool)) % 92.43/92.66 (fun (fun int (product_prod int (list int))) % 92.43/92.66 (fun int (fun (fun (product_prod int (list int)) bool) bool))) % 92.43/92.66 (combb (product_prod int (list int)) (fun (fun (product_prod int (list int)) bool) bool) int) % 92.43/92.66 (member (product_prod int (list int))))) % 92.43/92.66 (aa (fun int (fun (list int) (product_prod int (list int)))) % 92.43/92.66 (fun (list int) (fun int (product_prod int (list int)))) % 92.43/92.66 (combc int (list int) (product_prod int (list int))) (product_Pair int (list int)))))) % 92.43/92.66 (set (product_prod int (list int)) (lbounds as)))))))) % 92.43/92.66 False % 92.43/92.66 Clause #8649 (by forward demodulation #[8648, 191]): Eq % 92.43/92.66 (finite_finite int % 92.43/92.66 (image (product_prod int (list int)) int % 92.43/92.66 (aa (fun int (fun (list int) int)) (fun (product_prod int (list int)) int) (product_prod_case int (list int) int) % 92.43/92.66 (aa (fun (list int) int) (fun int (fun (list int) int)) % 92.43/92.66 (aa (fun int (fun (fun (list int) int) (fun (list int) int))) % 92.43/92.66 (fun (fun (list int) int) (fun int (fun (list int) int))) % 92.43/92.66 (combc int (fun (list int) int) (fun (list int) int)) % 92.43/92.66 (aa (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int))) % 92.43/92.66 (aa (fun (fun int int) (fun (fun (list int) int) (fun (list int) int))) % 92.43/92.66 (fun (fun int (fun int int)) (fun int (fun (fun (list int) int) (fun (list int) int)))) % 92.43/92.66 (combb (fun int int) (fun (fun (list int) int) (fun (list int) int)) int) (combb int int (list int))) % 92.43/92.66 (minus_minus int))) % 92.43/92.66 (aa (list int) (fun (list int) int) % 92.43/92.66 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 92.43/92.66 (combc (list int) (list int) int) (iprod int)) % 92.43/92.66 xs))) % 92.43/92.66 (set (product_prod int (list int)) (lbounds as)))) % 92.56/92.71 False % 92.56/92.71 Clause #8650 (by superposition #[8649, 564]): Eq False True % 92.56/92.71 Clause #8651 (by clausification #[8650]): False % 92.56/92.71 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------