%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : COM069_5 : TPTP v9.2.0. Released v6.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n029.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:51 PM UTC 2025 % Result : Theorem 9.10s 9.29s % Output : Proof 9.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM069_5 : TPTP v9.2.0. Released v6.0.0. % 0.07/0.13 % Command : duper %s % 0.14/0.34 % Computer : n029.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Thu Oct 2 15:49:53 EDT 2025 % 0.14/0.35 % CPUTime : % 9.10/9.29 SZS status Theorem for theBenchmark.p % 9.10/9.29 SZS output start Proof for theBenchmark.p % 9.10/9.29 Clause #75 (by assumption #[]): Eq (∀ (A : Type) (P1 : fun A bool), Eq (collect A P1) P1) True % 9.10/9.29 Clause #81 (by assumption #[]): Eq % 9.10/9.29 (∀ (Y M X : int), % 9.10/9.29 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) (div_mod int X M)) Y) M) % 9.10/9.29 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) Y) M)) % 9.10/9.29 True % 9.10/9.29 Clause #82 (by assumption #[]): Eq % 9.10/9.29 (∀ (M Y X : int), % 9.10/9.29 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) (div_mod int Y M)) M) % 9.10/9.29 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) Y) M)) % 9.10/9.29 True % 9.10/9.29 Clause #130 (by assumption #[]): Eq % 9.10/9.29 (Not % 9.10/9.29 (Eq % 9.10/9.29 (div_mod int % 9.10/9.29 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.10/9.29 (aa int int % 9.10/9.29 (times_times int % 9.10/9.29 (plus_plus int % 9.10/9.29 (div_div int % 9.10/9.29 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.10/9.29 (big_linorder_Min int % 9.10/9.29 (collect int % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.10/9.29 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.10/9.29 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.10/9.29 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.10/9.29 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.10/9.29 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.10/9.29 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.10/9.29 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.10/9.29 (combb (fun int bool) bool (list int)) (fEx int))) % 9.10/9.29 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.10/9.29 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.10/9.29 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.10/9.29 (combs (list int) (fun int bool) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (list int) (fun int (fun bool bool))) % 9.10/9.29 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.10/9.29 (combb (fun (list int) (fun int (fun bool bool))) % 9.10/9.29 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.10/9.29 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int (fun bool bool))) % 9.10/9.29 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.10/9.29 (combs int bool bool))) % 9.10/9.29 (aa (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (fun (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.10/9.29 (combb (fun (list int) (fun int bool)) % 9.10/9.29 (fun (list int) (fun int (fun bool bool))) int) % 9.10/9.29 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) % 9.10/9.29 (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.10/9.29 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.10/9.29 (combb bool (fun bool bool) int) fconj))) % 9.10/9.29 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (aa % 9.10/9.29 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.10/9.29 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (fun int int) (fun int bool))) % 9.10/9.29 (fun int % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (fun int int) (fun int bool)) % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun int (fun (fun int int) (fun int bool))) % 9.10/9.29 (fun int % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.10/9.29 (combb (fun (fun int int) (fun int bool)) % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.10/9.29 int) % 9.10/9.29 (combb (fun int int) (fun int bool) (list int))) % 9.10/9.29 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.10/9.29 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.10/9.29 (fun (fun int (fun int bool)) % 9.10/9.29 (fun int (fun (fun int int) (fun int bool)))) % 9.10/9.29 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.10/9.29 (combb int bool int)) % 9.10/9.29 (fequal int)))) % 9.10/9.29 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.10/9.29 (aa (fun int (fun int int)) % 9.10/9.29 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.10/9.29 (combb int (fun int int) (list int)) (minus_minus int)) % 9.10/9.29 (aa (list int) (fun (list int) int) % 9.10/9.29 (aa (fun (list int) (fun (list int) int)) % 9.10/9.29 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.10/9.29 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.10/9.29 (aa (fun (list int) (fun (list int) int)) % 9.10/9.29 (fun (fun (list int) (list int)) % 9.10/9.29 (fun (list int) (fun (list int) int))) % 9.10/9.29 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.10/9.29 (tl int))) % 9.10/9.29 xs))))))) % 9.10/9.29 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.10/9.29 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.10/9.29 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.10/9.29 (combc (list int) (fun atom bool) (fun int bool)) % 9.10/9.29 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.10/9.29 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.10/9.29 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.10/9.29 (list int)) % 9.10/9.29 (combc int (fun atom bool) bool)) % 9.10/9.29 (aa (fun (list int) (fun int atom)) % 9.10/9.29 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (fun (fun (list int) (fun int atom)) % 9.10/9.29 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.10/9.29 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.10/9.29 (aa (fun atom (fun (fun atom bool) bool)) % 9.10/9.29 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.10/9.29 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.10/9.29 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.10/9.29 (collect atom % 9.10/9.29 (aa (fun atom bool) (fun atom bool) % 9.10/9.29 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.10/9.29 (combs atom bool bool) % 9.10/9.29 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.10/9.29 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.10/9.29 (combb bool (fun bool bool) atom) fconj) % 9.10/9.29 (aa (fun atom bool) (fun atom bool) % 9.10/9.29 (aa (fun atom (fun (fun atom bool) bool)) % 9.10/9.29 (fun (fun atom bool) (fun atom bool)) (combc atom (fun atom bool) bool) % 9.10/9.29 (member atom)) % 9.10/9.29 (set atom as)))) % 9.10/9.29 (atom_case bool % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (list_case bool int fFalse % 9.10/9.29 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.10/9.29 (aa (fun bool (fun (list int) bool)) % 9.10/9.29 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.10/9.29 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.10/9.29 (aa int (fun int bool) % 9.10/9.29 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.10/9.29 (ord_less int)) % 9.10/9.29 (zero_zero int))))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.10/9.29 (zlcms % 9.10/9.29 (map atom int divisor % 9.10/9.29 (filter atom % 9.10/9.29 (atom_case bool % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.10/9.29 as)))) % 9.10/9.29 (one_one int))) % 9.10/9.29 (zlcms % 9.10/9.29 (map atom int divisor % 9.10/9.29 (filter atom % 9.10/9.29 (atom_case bool % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.10/9.29 as))))) % 9.10/9.29 (aa atom int divisor a)) % 9.10/9.29 (div_mod int % 9.10/9.29 (aa int int (aa int (fun int int) (minus_minus int) (div_mod int n (aa atom int divisor a))) % 9.10/9.29 (div_mod int % 9.10/9.29 (aa int int % 9.10/9.29 (times_times int % 9.10/9.29 (plus_plus int % 9.10/9.29 (div_div int % 9.10/9.29 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.10/9.29 (big_linorder_Min int % 9.10/9.29 (collect int % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.10/9.29 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.10/9.29 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.10/9.29 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.10/9.29 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.10/9.29 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.10/9.29 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.10/9.29 (aa (fun (fun int bool) bool) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.10/9.29 (combb (fun int bool) bool (list int)) (fEx int))) % 9.10/9.29 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.10/9.29 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.10/9.29 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.10/9.29 (combs (list int) (fun int bool) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (list int) (fun int (fun bool bool))) % 9.10/9.29 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.10/9.29 (combb (fun (list int) (fun int (fun bool bool))) % 9.10/9.29 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.10/9.29 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int (fun bool bool))) % 9.10/9.29 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.10/9.29 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) % 9.10/9.29 (list int)) % 9.10/9.29 (combs int bool bool))) % 9.10/9.29 (aa (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (list int) (fun int bool)) % 9.10/9.29 (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (fun (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.10/9.29 (combb (fun (list int) (fun int bool)) % 9.10/9.29 (fun (list int) (fun int (fun bool bool))) int) % 9.10/9.29 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.10/9.29 (fun (fun (list int) (fun int bool)) % 9.10/9.29 (fun (list int) (fun int (fun bool bool)))) % 9.10/9.29 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.10/9.29 (aa (fun bool (fun bool bool)) % 9.10/9.29 (fun (fun int bool) (fun int (fun bool bool))) % 9.10/9.29 (combb bool (fun bool bool) int) fconj))) % 9.10/9.29 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.10/9.29 (aa % 9.10/9.29 (fun int % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun (list int) (fun int int)) % 9.10/9.29 (fun int (fun (list int) (fun int bool)))) % 9.10/9.29 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.10/9.29 (aa (fun int (fun (fun int int) (fun int bool))) % 9.10/9.29 (fun int % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun (fun int int) (fun int bool)) % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.10/9.29 (fun (fun int (fun (fun int int) (fun int bool))) % 9.10/9.29 (fun int % 9.10/9.29 (fun (fun (list int) (fun int int)) % 9.10/9.29 (fun (list int) (fun int bool))))) % 9.10/9.29 (combb (fun (fun int int) (fun int bool)) % 9.10/9.29 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.10/9.29 int) % 9.10/9.29 (combb (fun int int) (fun int bool) (list int))) % 9.10/9.29 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.10/9.29 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.10/9.29 (fun (fun int (fun int bool)) % 9.10/9.29 (fun int (fun (fun int int) (fun int bool)))) % 9.10/9.29 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.10/9.29 (combb int bool int)) % 9.10/9.29 (fequal int)))) % 9.10/9.29 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.10/9.29 (aa (fun int (fun int int)) % 9.10/9.29 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.10/9.29 (combb int (fun int int) (list int)) (minus_minus int)) % 9.10/9.29 (aa (list int) (fun (list int) int) % 9.10/9.29 (aa (fun (list int) (fun (list int) int)) % 9.10/9.29 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.10/9.29 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.10/9.29 (aa (fun (list int) (fun (list int) int)) % 9.10/9.29 (fun (fun (list int) (list int)) % 9.10/9.29 (fun (list int) (fun (list int) int))) % 9.10/9.29 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.10/9.29 (tl int))) % 9.10/9.29 xs))))))) % 9.10/9.29 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.10/9.29 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.10/9.29 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.10/9.29 (combc (list int) (fun atom bool) (fun int bool)) % 9.10/9.29 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.10/9.29 (aa % 9.10/9.29 (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.10/9.29 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.10/9.29 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.10/9.29 (list int)) % 9.10/9.29 (combc int (fun atom bool) bool)) % 9.10/9.29 (aa (fun (list int) (fun int atom)) % 9.10/9.29 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (fun (fun (list int) (fun int atom)) % 9.10/9.29 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.10/9.29 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.10/9.29 (aa (fun atom (fun (fun atom bool) bool)) % 9.10/9.29 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.10/9.29 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.10/9.29 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.10/9.29 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.10/9.29 (collect atom % 9.10/9.29 (aa (fun atom bool) (fun atom bool) % 9.10/9.29 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.10/9.29 (combs atom bool bool) % 9.10/9.29 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.10/9.29 (aa (fun bool (fun bool bool)) % 9.10/9.29 (fun (fun atom bool) (fun atom (fun bool bool))) % 9.10/9.29 (combb bool (fun bool bool) atom) fconj) % 9.10/9.29 (aa (fun atom bool) (fun atom bool) % 9.10/9.29 (aa (fun atom (fun (fun atom bool) bool)) % 9.10/9.29 (fun (fun atom bool) (fun atom bool)) (combc atom (fun atom bool) bool) % 9.10/9.29 (member atom)) % 9.10/9.29 (set atom as)))) % 9.10/9.29 (atom_case bool % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (list_case bool int fFalse % 9.10/9.29 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.10/9.29 (aa (fun bool (fun (list int) bool)) % 9.10/9.29 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.10/9.29 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.10/9.29 (aa int (fun int bool) % 9.10/9.29 (aa (fun int (fun int bool)) (fun int (fun int bool)) % 9.10/9.29 (combc int int bool) (ord_less int)) % 9.10/9.29 (zero_zero int))))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.10/9.29 (zlcms % 9.10/9.29 (map atom int divisor % 9.10/9.29 (filter atom % 9.10/9.29 (atom_case bool % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.10/9.29 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.10/9.29 (combk (fun int (fun (list int) bool)) int) % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.10/9.29 (combk (fun (list int) bool) int) % 9.10/9.29 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.10/9.29 as)))) % 9.10/9.29 (one_one int))) % 9.10/9.29 (zlcms % 9.10/9.29 (map atom int divisor % 9.10/9.29 (filter atom % 9.10/9.29 (atom_case bool % 9.10/9.29 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.23/9.41 as)))) % 9.23/9.41 (aa atom int divisor a))) % 9.23/9.41 (aa atom int divisor a)))) % 9.23/9.41 True % 9.23/9.41 Clause #1994 (by clausification #[75]): ∀ (a : Type), Eq (∀ (P1 : fun a bool), Eq (collect a P1) P1) True % 9.23/9.41 Clause #1995 (by clausification #[1994]): ∀ (a : Type) (a_1 : fun a bool), Eq (Eq (collect a a_1) a_1) True % 9.23/9.41 Clause #1996 (by clausification #[1995]): ∀ (a : Type) (a_1 : fun a bool), Eq (collect a a_1) a_1 % 9.23/9.41 Clause #2044 (by clausification #[81]): ∀ (a : int), % 9.23/9.41 Eq % 9.23/9.41 (∀ (M X : int), % 9.23/9.41 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) (div_mod int X M)) a) M) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) a) M)) % 9.23/9.41 True % 9.23/9.41 Clause #2045 (by clausification #[2044]): ∀ (a a_1 : int), % 9.23/9.41 Eq % 9.23/9.41 (∀ (X : int), % 9.23/9.41 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) (div_mod int X a)) a_1) a) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) a_1) a)) % 9.23/9.41 True % 9.23/9.41 Clause #2046 (by clausification #[2045]): ∀ (a a_1 a_2 : int), % 9.23/9.41 Eq % 9.23/9.41 (Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) (div_mod int a a_1)) a_2) a_1) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) a) a_2) a_1)) % 9.23/9.41 True % 9.23/9.41 Clause #2047 (by clausification #[2046]): ∀ (a a_1 a_2 : int), % 9.23/9.41 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) (div_mod int a a_1)) a_2) a_1) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) a) a_2) a_1) % 9.23/9.41 Clause #2325 (by clausification #[82]): ∀ (a : int), % 9.23/9.41 Eq % 9.23/9.41 (∀ (Y X : int), % 9.23/9.41 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) (div_mod int Y a)) a) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) Y) a)) % 9.23/9.41 True % 9.23/9.41 Clause #2326 (by clausification #[2325]): ∀ (a a_1 : int), % 9.23/9.41 Eq % 9.23/9.41 (∀ (X : int), % 9.23/9.41 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) (div_mod int a a_1)) a_1) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) X) a) a_1)) % 9.23/9.41 True % 9.23/9.41 Clause #2327 (by clausification #[2326]): ∀ (a a_1 a_2 : int), % 9.23/9.41 Eq % 9.23/9.41 (Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) a) (div_mod int a_1 a_2)) a_2) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) a) a_1) a_2)) % 9.23/9.41 True % 9.23/9.41 Clause #2328 (by clausification #[2327]): ∀ (a a_1 a_2 : int), % 9.23/9.41 Eq (div_mod int (aa int int (aa int (fun int int) (minus_minus int) a) (div_mod int a_1 a_2)) a_2) % 9.23/9.41 (div_mod int (aa int int (aa int (fun int int) (minus_minus int) a) a_1) a_2) % 9.23/9.41 Clause #3504 (by clausification #[130]): Eq % 9.23/9.41 (Eq % 9.23/9.41 (div_mod int % 9.23/9.41 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.23/9.41 (aa int int % 9.23/9.41 (times_times int % 9.23/9.41 (plus_plus int % 9.23/9.41 (div_div int % 9.23/9.41 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.23/9.41 (big_linorder_Min int % 9.23/9.41 (collect int % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.23/9.41 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.23/9.41 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.23/9.41 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.23/9.41 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.23/9.41 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.23/9.41 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.23/9.41 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.23/9.41 (combb (fun int bool) bool (list int)) (fEx int))) % 9.23/9.41 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.23/9.41 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.23/9.41 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.23/9.41 (combs (list int) (fun int bool) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.23/9.41 (combb (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.23/9.41 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.23/9.41 (combs int bool bool))) % 9.23/9.41 (aa (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (fun (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.23/9.41 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 int) % 9.23/9.41 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.23/9.41 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.23/9.41 (combb bool (fun bool bool) int) fconj))) % 9.23/9.41 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.23/9.41 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (fun int int) (fun int bool))) % 9.23/9.41 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (fun int int) (fun int bool)) % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun int (fun (fun int int) (fun int bool))) % 9.23/9.41 (fun int % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.23/9.41 (combb (fun (fun int int) (fun int bool)) % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.23/9.41 (combb (fun int int) (fun int bool) (list int))) % 9.23/9.41 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.23/9.41 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.23/9.41 (fun (fun int (fun int bool)) % 9.23/9.41 (fun int (fun (fun int int) (fun int bool)))) % 9.23/9.41 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.23/9.41 (combb int bool int)) % 9.23/9.41 (fequal int)))) % 9.23/9.41 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.23/9.41 (aa (fun int (fun int int)) % 9.23/9.41 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.23/9.41 (combb int (fun int int) (list int)) (minus_minus int)) % 9.23/9.41 (aa (list int) (fun (list int) int) % 9.23/9.41 (aa (fun (list int) (fun (list int) int)) % 9.23/9.41 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.23/9.41 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.23/9.41 (aa (fun (list int) (fun (list int) int)) % 9.23/9.41 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.23/9.41 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.23/9.41 (tl int))) % 9.23/9.41 xs))))))) % 9.23/9.41 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.23/9.41 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.23/9.41 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.23/9.41 (combc (list int) (fun atom bool) (fun int bool)) % 9.23/9.41 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.23/9.41 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.23/9.41 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.23/9.41 (list int)) % 9.23/9.41 (combc int (fun atom bool) bool)) % 9.23/9.41 (aa (fun (list int) (fun int atom)) % 9.23/9.41 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (fun (fun (list int) (fun int atom)) % 9.23/9.41 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.23/9.41 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.23/9.41 (aa (fun atom (fun (fun atom bool) bool)) % 9.23/9.41 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.23/9.41 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.23/9.41 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.23/9.41 (collect atom % 9.23/9.41 (aa (fun atom bool) (fun atom bool) % 9.23/9.41 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.23/9.41 (combs atom bool bool) % 9.23/9.41 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.23/9.41 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.23/9.41 (combb bool (fun bool bool) atom) fconj) % 9.23/9.41 (aa (fun atom bool) (fun atom bool) % 9.23/9.41 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.23/9.41 (combc atom (fun atom bool) bool) (member atom)) % 9.23/9.41 (set atom as)))) % 9.23/9.41 (atom_case bool % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.23/9.41 (combk (fun (list int) bool) int) % 9.23/9.41 (list_case bool int fFalse % 9.23/9.41 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.23/9.41 (aa (fun bool (fun (list int) bool)) % 9.23/9.41 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.23/9.41 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.23/9.41 (aa int (fun int bool) % 9.23/9.41 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.23/9.41 (ord_less int)) % 9.23/9.41 (zero_zero int))))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.23/9.41 (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.23/9.41 (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.23/9.41 (zlcms % 9.23/9.41 (map atom int divisor % 9.23/9.41 (filter atom % 9.23/9.41 (atom_case bool % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.23/9.41 as)))) % 9.23/9.41 (one_one int))) % 9.23/9.41 (zlcms % 9.23/9.41 (map atom int divisor % 9.23/9.41 (filter atom % 9.23/9.41 (atom_case bool % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.23/9.41 as))))) % 9.23/9.41 (aa atom int divisor a)) % 9.23/9.41 (div_mod int % 9.23/9.41 (aa int int (aa int (fun int int) (minus_minus int) (div_mod int n (aa atom int divisor a))) % 9.23/9.41 (div_mod int % 9.23/9.41 (aa int int % 9.23/9.41 (times_times int % 9.23/9.41 (plus_plus int % 9.23/9.41 (div_div int % 9.23/9.41 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.23/9.41 (big_linorder_Min int % 9.23/9.41 (collect int % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.23/9.41 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.23/9.41 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.23/9.41 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.23/9.41 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.23/9.41 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.23/9.41 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.23/9.41 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.23/9.41 (combb (fun int bool) bool (list int)) (fEx int))) % 9.23/9.41 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.23/9.41 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.23/9.41 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.23/9.41 (combs (list int) (fun int bool) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.23/9.41 (combb (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.23/9.41 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int (fun bool bool))) % 9.23/9.41 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.23/9.41 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.23/9.41 (combs int bool bool))) % 9.23/9.41 (aa (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (fun (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.23/9.41 (combb (fun (list int) (fun int bool)) % 9.23/9.41 (fun (list int) (fun int (fun bool bool))) int) % 9.23/9.41 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.23/9.41 (fun (fun (list int) (fun int bool)) % 9.23/9.41 (fun (list int) (fun int (fun bool bool)))) % 9.23/9.41 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.23/9.41 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.23/9.41 (combb bool (fun bool bool) int) fconj))) % 9.23/9.41 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.23/9.41 (aa % 9.23/9.41 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.23/9.41 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.23/9.41 (aa (fun int (fun (fun int int) (fun int bool))) % 9.23/9.41 (fun int % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.23/9.41 (aa % 9.23/9.41 (fun (fun (fun int int) (fun int bool)) % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.23/9.41 (fun (fun int (fun (fun int int) (fun int bool))) % 9.23/9.41 (fun int % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.23/9.41 (combb (fun (fun int int) (fun int bool)) % 9.23/9.41 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.23/9.41 int) % 9.23/9.41 (combb (fun int int) (fun int bool) (list int))) % 9.23/9.41 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.23/9.41 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.23/9.41 (fun (fun int (fun int bool)) % 9.23/9.41 (fun int (fun (fun int int) (fun int bool)))) % 9.23/9.41 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.23/9.41 (combb int bool int)) % 9.23/9.41 (fequal int)))) % 9.23/9.41 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.23/9.41 (aa (fun int (fun int int)) % 9.23/9.41 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.23/9.41 (combb int (fun int int) (list int)) (minus_minus int)) % 9.23/9.41 (aa (list int) (fun (list int) int) % 9.23/9.41 (aa (fun (list int) (fun (list int) int)) % 9.23/9.41 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.23/9.41 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.23/9.41 (aa (fun (list int) (fun (list int) int)) % 9.23/9.41 (fun (fun (list int) (list int)) % 9.23/9.41 (fun (list int) (fun (list int) int))) % 9.23/9.41 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.23/9.41 (tl int))) % 9.23/9.41 xs))))))) % 9.23/9.41 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.23/9.41 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.23/9.41 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.23/9.41 (combc (list int) (fun atom bool) (fun int bool)) % 9.23/9.41 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.23/9.41 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.23/9.41 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.23/9.41 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.23/9.41 (list int)) % 9.23/9.41 (combc int (fun atom bool) bool)) % 9.23/9.41 (aa (fun (list int) (fun int atom)) % 9.23/9.41 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (fun (fun (list int) (fun int atom)) % 9.23/9.41 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.23/9.41 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.23/9.41 (aa (fun atom (fun (fun atom bool) bool)) % 9.23/9.41 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.23/9.41 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.23/9.41 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.23/9.41 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.23/9.41 (collect atom % 9.23/9.41 (aa (fun atom bool) (fun atom bool) % 9.23/9.41 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.23/9.41 (combs atom bool bool) % 9.23/9.41 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.23/9.41 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.23/9.41 (combb bool (fun bool bool) atom) fconj) % 9.23/9.41 (aa (fun atom bool) (fun atom bool) % 9.23/9.41 (aa (fun atom (fun (fun atom bool) bool)) % 9.23/9.41 (fun (fun atom bool) (fun atom bool)) (combc atom (fun atom bool) bool) % 9.23/9.41 (member atom)) % 9.23/9.41 (set atom as)))) % 9.23/9.41 (atom_case bool % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.23/9.41 (combk (fun (list int) bool) int) % 9.23/9.41 (list_case bool int fFalse % 9.23/9.41 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.23/9.41 (aa (fun bool (fun (list int) bool)) % 9.23/9.41 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.23/9.41 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.23/9.41 (aa int (fun int bool) % 9.23/9.41 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.23/9.41 (ord_less int)) % 9.23/9.41 (zero_zero int))))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.23/9.41 (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.23/9.41 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.23/9.41 (combk (fun int (fun (list int) bool)) int) % 9.23/9.41 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.23/9.41 (combk (fun (list int) bool) int) % 9.23/9.41 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.23/9.41 (zlcms % 9.23/9.41 (map atom int divisor % 9.35/9.52 (filter atom % 9.35/9.52 (atom_case bool % 9.35/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.35/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.35/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.35/9.52 (combk (fun int (fun (list int) bool)) int) % 9.35/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.35/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.35/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.35/9.52 (combk (fun int (fun (list int) bool)) int) % 9.35/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.35/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.35/9.52 as)))) % 9.35/9.52 (one_one int))) % 9.35/9.52 (zlcms % 9.35/9.52 (map atom int divisor % 9.35/9.52 (filter atom % 9.35/9.52 (atom_case bool % 9.35/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.35/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.35/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.35/9.52 (combk (fun int (fun (list int) bool)) int) % 9.35/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.35/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.35/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.35/9.52 (combk (fun int (fun (list int) bool)) int) % 9.35/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.35/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.35/9.52 as)))) % 9.35/9.52 (aa atom int divisor a))) % 9.35/9.52 (aa atom int divisor a))) % 9.35/9.52 False % 9.35/9.52 Clause #3505 (by clausification #[3504]): Ne % 9.35/9.52 (div_mod int % 9.35/9.52 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.35/9.52 (aa int int % 9.35/9.52 (times_times int % 9.35/9.52 (plus_plus int % 9.35/9.52 (div_div int % 9.35/9.52 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.35/9.52 (big_linorder_Min int % 9.35/9.52 (collect int % 9.35/9.52 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.35/9.52 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.35/9.52 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.35/9.52 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.35/9.52 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.38/9.52 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.38/9.52 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.38/9.52 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.38/9.52 (combb (fun int bool) bool (list int)) (fEx int))) % 9.38/9.52 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.38/9.52 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.38/9.52 (aa % 9.38/9.52 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.38/9.52 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.38/9.52 (combs (list int) (fun int bool) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (aa % 9.38/9.52 (fun (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.38/9.52 (combb (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.38/9.52 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.38/9.52 (combs int bool bool))) % 9.38/9.52 (aa (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (fun (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.38/9.52 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 int) % 9.38/9.52 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.38/9.52 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.38/9.52 (combb bool (fun bool bool) int) fconj))) % 9.38/9.52 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.38/9.52 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (fun int int) (fun int bool))) % 9.38/9.52 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.38/9.52 (aa % 9.38/9.52 (fun (fun (fun int int) (fun int bool)) % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun int (fun (fun int int) (fun int bool))) % 9.38/9.52 (fun int % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.38/9.52 (combb (fun (fun int int) (fun int bool)) % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.38/9.52 (combb (fun int int) (fun int bool) (list int))) % 9.38/9.52 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.38/9.52 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.38/9.52 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.38/9.52 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.38/9.52 (combb int bool int)) % 9.38/9.52 (fequal int)))) % 9.38/9.52 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.38/9.52 (aa (fun int (fun int int)) % 9.38/9.52 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.38/9.52 (combb int (fun int int) (list int)) (minus_minus int)) % 9.38/9.52 (aa (list int) (fun (list int) int) % 9.38/9.52 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.38/9.52 (combc (list int) (list int) int) % 9.38/9.52 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.38/9.52 (aa (fun (list int) (fun (list int) int)) % 9.38/9.52 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.38/9.52 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.38/9.52 (tl int))) % 9.38/9.52 xs))))))) % 9.38/9.52 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.38/9.52 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.38/9.52 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.38/9.52 (combc (list int) (fun atom bool) (fun int bool)) % 9.38/9.52 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.38/9.52 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.38/9.52 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.38/9.52 (list int)) % 9.38/9.52 (combc int (fun atom bool) bool)) % 9.38/9.52 (aa (fun (list int) (fun int atom)) % 9.38/9.52 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (fun (fun (list int) (fun int atom)) % 9.38/9.52 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.38/9.52 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.38/9.52 (aa (fun atom (fun (fun atom bool) bool)) % 9.38/9.52 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.38/9.52 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.38/9.52 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.38/9.52 (collect atom % 9.38/9.52 (aa (fun atom bool) (fun atom bool) % 9.38/9.52 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.38/9.52 (combs atom bool bool) % 9.38/9.52 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.38/9.52 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.38/9.52 (combb bool (fun bool bool) atom) fconj) % 9.38/9.52 (aa (fun atom bool) (fun atom bool) % 9.38/9.52 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.38/9.52 (combc atom (fun atom bool) bool) (member atom)) % 9.38/9.52 (set atom as)))) % 9.38/9.52 (atom_case bool % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.38/9.52 (combk (fun (list int) bool) int) % 9.38/9.52 (list_case bool int fFalse % 9.38/9.52 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.38/9.52 (aa (fun bool (fun (list int) bool)) % 9.38/9.52 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.38/9.52 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.38/9.52 (aa int (fun int bool) % 9.38/9.52 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.38/9.52 (ord_less int)) % 9.38/9.52 (zero_zero int))))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.38/9.52 (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.38/9.52 (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.38/9.52 (zlcms % 9.38/9.52 (map atom int divisor % 9.38/9.52 (filter atom % 9.38/9.52 (atom_case bool % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.38/9.52 as)))) % 9.38/9.52 (one_one int))) % 9.38/9.52 (zlcms % 9.38/9.52 (map atom int divisor % 9.38/9.52 (filter atom % 9.38/9.52 (atom_case bool % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.38/9.52 as))))) % 9.38/9.52 (aa atom int divisor a)) % 9.38/9.52 (div_mod int % 9.38/9.52 (aa int int (aa int (fun int int) (minus_minus int) (div_mod int n (aa atom int divisor a))) % 9.38/9.52 (div_mod int % 9.38/9.52 (aa int int % 9.38/9.52 (times_times int % 9.38/9.52 (plus_plus int % 9.38/9.52 (div_div int % 9.38/9.52 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.38/9.52 (big_linorder_Min int % 9.38/9.52 (collect int % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.38/9.52 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.38/9.52 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.38/9.52 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.38/9.52 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.38/9.52 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.38/9.52 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.38/9.52 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.38/9.52 (combb (fun int bool) bool (list int)) (fEx int))) % 9.38/9.52 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.38/9.52 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.38/9.52 (aa % 9.38/9.52 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.38/9.52 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.38/9.52 (combs (list int) (fun int bool) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (aa % 9.38/9.52 (fun (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.38/9.52 (combb (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.38/9.52 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.38/9.52 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.38/9.52 (combs int bool bool))) % 9.38/9.52 (aa (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (fun (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.38/9.52 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.38/9.52 int) % 9.38/9.52 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.38/9.52 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.38/9.52 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.38/9.52 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.38/9.52 (combb bool (fun bool bool) int) fconj))) % 9.38/9.52 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.38/9.52 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.38/9.52 (aa (fun int (fun (fun int int) (fun int bool))) % 9.38/9.52 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.38/9.52 (aa % 9.38/9.52 (fun (fun (fun int int) (fun int bool)) % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.38/9.52 (fun (fun int (fun (fun int int) (fun int bool))) % 9.38/9.52 (fun int % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.38/9.52 (combb (fun (fun int int) (fun int bool)) % 9.38/9.52 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.38/9.52 (combb (fun int int) (fun int bool) (list int))) % 9.38/9.52 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.38/9.52 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.38/9.52 (fun (fun int (fun int bool)) % 9.38/9.52 (fun int (fun (fun int int) (fun int bool)))) % 9.38/9.52 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.38/9.52 (combb int bool int)) % 9.38/9.52 (fequal int)))) % 9.38/9.52 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.38/9.52 (aa (fun int (fun int int)) % 9.38/9.52 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.38/9.52 (combb int (fun int int) (list int)) (minus_minus int)) % 9.38/9.52 (aa (list int) (fun (list int) int) % 9.38/9.52 (aa (fun (list int) (fun (list int) int)) % 9.38/9.52 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.38/9.52 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.38/9.52 (aa (fun (list int) (fun (list int) int)) % 9.38/9.52 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.38/9.52 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.38/9.52 (tl int))) % 9.38/9.52 xs))))))) % 9.38/9.52 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.38/9.52 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.38/9.52 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.38/9.52 (combc (list int) (fun atom bool) (fun int bool)) % 9.38/9.52 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.38/9.52 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.38/9.52 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.38/9.52 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.38/9.52 (list int)) % 9.38/9.52 (combc int (fun atom bool) bool)) % 9.38/9.52 (aa (fun (list int) (fun int atom)) % 9.38/9.52 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (fun (fun (list int) (fun int atom)) % 9.38/9.52 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.38/9.52 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.38/9.52 (aa (fun atom (fun (fun atom bool) bool)) % 9.38/9.52 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.38/9.52 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.38/9.52 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.38/9.52 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.38/9.52 (collect atom % 9.38/9.52 (aa (fun atom bool) (fun atom bool) % 9.38/9.52 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.38/9.52 (combs atom bool bool) % 9.38/9.52 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.38/9.52 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.38/9.52 (combb bool (fun bool bool) atom) fconj) % 9.38/9.52 (aa (fun atom bool) (fun atom bool) % 9.38/9.52 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.38/9.52 (combc atom (fun atom bool) bool) (member atom)) % 9.38/9.52 (set atom as)))) % 9.38/9.52 (atom_case bool % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.38/9.52 (combk (fun (list int) bool) int) % 9.38/9.52 (list_case bool int fFalse % 9.38/9.52 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.38/9.52 (aa (fun bool (fun (list int) bool)) % 9.38/9.52 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.38/9.52 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.38/9.52 (aa int (fun int bool) % 9.38/9.52 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.38/9.52 (ord_less int)) % 9.38/9.52 (zero_zero int))))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.38/9.52 (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.38/9.52 (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.38/9.52 (zlcms % 9.38/9.52 (map atom int divisor % 9.38/9.52 (filter atom % 9.38/9.52 (atom_case bool % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.38/9.52 as)))) % 9.38/9.52 (one_one int))) % 9.38/9.52 (zlcms % 9.38/9.52 (map atom int divisor % 9.38/9.52 (filter atom % 9.38/9.52 (atom_case bool % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.38/9.52 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.38/9.52 (combk (fun int (fun (list int) bool)) int) % 9.38/9.52 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.38/9.52 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.38/9.52 as)))) % 9.38/9.52 (aa atom int divisor a))) % 9.38/9.52 (aa atom int divisor a)) % 9.46/9.63 Clause #3506 (by forward demodulation #[3505, 1996]): Ne % 9.46/9.63 (div_mod int % 9.46/9.63 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.46/9.63 (aa int int % 9.46/9.63 (times_times int % 9.46/9.63 (plus_plus int % 9.46/9.63 (div_div int % 9.46/9.63 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.46/9.63 (big_linorder_Min int % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.46/9.63 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.46/9.63 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.46/9.63 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.46/9.63 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.46/9.63 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.46/9.63 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.46/9.63 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.46/9.63 (combb (fun int bool) bool (list int)) (fEx int))) % 9.46/9.63 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.46/9.63 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.46/9.63 (aa % 9.46/9.63 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.46/9.63 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.46/9.63 (combs (list int) (fun int bool) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (aa % 9.46/9.63 (fun (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.46/9.63 (combb (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.46/9.63 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.46/9.63 (combs int bool bool))) % 9.46/9.63 (aa (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (fun (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.46/9.63 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.46/9.63 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.46/9.63 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.46/9.63 (combb bool (fun bool bool) int) fconj))) % 9.46/9.63 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.46/9.63 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (fun int int) (fun int bool))) % 9.46/9.63 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.46/9.63 (aa % 9.46/9.63 (fun (fun (fun int int) (fun int bool)) % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun int (fun (fun int int) (fun int bool))) % 9.46/9.63 (fun int % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.46/9.63 (combb (fun (fun int int) (fun int bool)) % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.46/9.63 (combb (fun int int) (fun int bool) (list int))) % 9.46/9.63 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.46/9.63 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.46/9.63 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.46/9.63 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.46/9.63 (combb int bool int)) % 9.46/9.63 (fequal int)))) % 9.46/9.63 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.46/9.63 (aa (fun int (fun int int)) % 9.46/9.63 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.46/9.63 (combb int (fun int int) (list int)) (minus_minus int)) % 9.46/9.63 (aa (list int) (fun (list int) int) % 9.46/9.63 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.46/9.63 (combc (list int) (list int) int) % 9.46/9.63 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.46/9.63 (aa (fun (list int) (fun (list int) int)) % 9.46/9.63 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.46/9.63 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.46/9.63 (tl int))) % 9.46/9.63 xs))))))) % 9.46/9.63 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.46/9.63 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.46/9.63 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.46/9.63 (combc (list int) (fun atom bool) (fun int bool)) % 9.46/9.63 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.46/9.63 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.46/9.63 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.46/9.63 (list int)) % 9.46/9.63 (combc int (fun atom bool) bool)) % 9.46/9.63 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (fun (fun (list int) (fun int atom)) % 9.46/9.63 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.46/9.63 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.46/9.63 (aa (fun atom (fun (fun atom bool) bool)) % 9.46/9.63 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.46/9.63 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.46/9.63 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.46/9.63 (collect atom % 9.46/9.63 (aa (fun atom bool) (fun atom bool) % 9.46/9.63 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.46/9.63 (combs atom bool bool) % 9.46/9.63 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.46/9.63 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.46/9.63 (combb bool (fun bool bool) atom) fconj) % 9.46/9.63 (aa (fun atom bool) (fun atom bool) % 9.46/9.63 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.46/9.63 (combc atom (fun atom bool) bool) (member atom)) % 9.46/9.63 (set atom as)))) % 9.46/9.63 (atom_case bool % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.46/9.63 (combk (fun (list int) bool) int) % 9.46/9.63 (list_case bool int fFalse % 9.46/9.63 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.46/9.63 (aa (fun bool (fun (list int) bool)) % 9.46/9.63 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.46/9.63 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.46/9.63 (aa int (fun int bool) % 9.46/9.63 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.46/9.63 (ord_less int)) % 9.46/9.63 (zero_zero int))))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.46/9.63 (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.46/9.63 (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)))))))))))) % 9.46/9.63 (zlcms % 9.46/9.63 (map atom int divisor % 9.46/9.63 (filter atom % 9.46/9.63 (atom_case bool % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.46/9.63 as)))) % 9.46/9.63 (one_one int))) % 9.46/9.63 (zlcms % 9.46/9.63 (map atom int divisor % 9.46/9.63 (filter atom % 9.46/9.63 (atom_case bool % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.46/9.63 as))))) % 9.46/9.63 (aa atom int divisor a)) % 9.46/9.63 (div_mod int % 9.46/9.63 (aa int int (aa int (fun int int) (minus_minus int) (div_mod int n (aa atom int divisor a))) % 9.46/9.63 (div_mod int % 9.46/9.63 (aa int int % 9.46/9.63 (times_times int % 9.46/9.63 (plus_plus int % 9.46/9.63 (div_div int % 9.46/9.63 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.46/9.63 (big_linorder_Min int % 9.46/9.63 (collect int % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.46/9.63 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.46/9.63 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.46/9.63 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.46/9.63 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.46/9.63 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.46/9.63 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.46/9.63 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.46/9.63 (combb (fun int bool) bool (list int)) (fEx int))) % 9.46/9.63 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.46/9.63 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.46/9.63 (aa % 9.46/9.63 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.46/9.63 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.46/9.63 (combs (list int) (fun int bool) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (aa % 9.46/9.63 (fun (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.46/9.63 (combb (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.46/9.63 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.46/9.63 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.46/9.63 (combs int bool bool))) % 9.46/9.63 (aa (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (fun (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.46/9.63 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.46/9.63 int) % 9.46/9.63 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.46/9.63 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.46/9.63 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.46/9.63 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.46/9.63 (combb bool (fun bool bool) int) fconj))) % 9.46/9.63 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.46/9.63 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.46/9.63 (aa (fun int (fun (fun int int) (fun int bool))) % 9.46/9.63 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.46/9.63 (aa % 9.46/9.63 (fun (fun (fun int int) (fun int bool)) % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.46/9.63 (fun (fun int (fun (fun int int) (fun int bool))) % 9.46/9.63 (fun int % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.46/9.63 (combb (fun (fun int int) (fun int bool)) % 9.46/9.63 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.46/9.63 (combb (fun int int) (fun int bool) (list int))) % 9.46/9.63 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.46/9.63 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.46/9.63 (fun (fun int (fun int bool)) % 9.46/9.63 (fun int (fun (fun int int) (fun int bool)))) % 9.46/9.63 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.46/9.63 (combb int bool int)) % 9.46/9.63 (fequal int)))) % 9.46/9.63 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.46/9.63 (aa (fun int (fun int int)) % 9.46/9.63 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.46/9.63 (combb int (fun int int) (list int)) (minus_minus int)) % 9.46/9.63 (aa (list int) (fun (list int) int) % 9.46/9.63 (aa (fun (list int) (fun (list int) int)) % 9.46/9.63 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.46/9.63 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.46/9.63 (aa (fun (list int) (fun (list int) int)) % 9.46/9.63 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.46/9.63 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.46/9.63 (tl int))) % 9.46/9.63 xs))))))) % 9.46/9.63 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.46/9.63 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.46/9.63 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.46/9.63 (combc (list int) (fun atom bool) (fun int bool)) % 9.46/9.63 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.46/9.63 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.46/9.63 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.46/9.63 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.46/9.63 (list int)) % 9.46/9.63 (combc int (fun atom bool) bool)) % 9.46/9.63 (aa (fun (list int) (fun int atom)) % 9.46/9.63 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (fun (fun (list int) (fun int atom)) % 9.46/9.63 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.46/9.63 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.46/9.63 (aa (fun atom (fun (fun atom bool) bool)) % 9.46/9.63 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.46/9.63 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.46/9.63 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.46/9.63 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.46/9.63 (collect atom % 9.46/9.63 (aa (fun atom bool) (fun atom bool) % 9.46/9.63 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.46/9.63 (combs atom bool bool) % 9.46/9.63 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.46/9.63 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.46/9.63 (combb bool (fun bool bool) atom) fconj) % 9.46/9.63 (aa (fun atom bool) (fun atom bool) % 9.46/9.63 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.46/9.63 (combc atom (fun atom bool) bool) (member atom)) % 9.46/9.63 (set atom as)))) % 9.46/9.63 (atom_case bool % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.46/9.63 (combk (fun (list int) bool) int) % 9.46/9.63 (list_case bool int fFalse % 9.46/9.63 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.46/9.63 (aa (fun bool (fun (list int) bool)) % 9.46/9.63 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.46/9.63 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.46/9.63 (aa int (fun int bool) % 9.46/9.63 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.46/9.63 (ord_less int)) % 9.46/9.63 (zero_zero int))))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.46/9.63 (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.46/9.63 (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.46/9.63 (zlcms % 9.46/9.63 (map atom int divisor % 9.46/9.63 (filter atom % 9.46/9.63 (atom_case bool % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.46/9.63 (combk (fun int (fun (list int) bool)) int) % 9.46/9.63 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.46/9.63 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.46/9.63 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.53/9.73 as)))) % 9.53/9.73 (one_one int))) % 9.53/9.73 (zlcms % 9.53/9.73 (map atom int divisor % 9.53/9.73 (filter atom % 9.53/9.73 (atom_case bool % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.53/9.73 as)))) % 9.53/9.73 (aa atom int divisor a))) % 9.53/9.73 (aa atom int divisor a)) % 9.53/9.73 Clause #3507 (by forward demodulation #[3506, 1996]): Ne % 9.53/9.73 (div_mod int % 9.53/9.73 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.53/9.73 (aa int int % 9.53/9.73 (times_times int % 9.53/9.73 (plus_plus int % 9.53/9.73 (div_div int % 9.53/9.73 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.53/9.73 (big_linorder_Min int % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.53/9.73 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.53/9.73 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.53/9.73 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.53/9.73 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.53/9.73 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.53/9.73 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.53/9.73 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.53/9.73 (combb (fun int bool) bool (list int)) (fEx int))) % 9.53/9.73 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.53/9.73 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.53/9.73 (aa % 9.53/9.73 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.53/9.73 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.53/9.73 (combs (list int) (fun int bool) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (aa % 9.53/9.73 (fun (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.53/9.73 (combb (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.53/9.73 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.53/9.73 (combs int bool bool))) % 9.53/9.73 (aa (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (fun (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.53/9.73 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.53/9.73 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.53/9.73 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.53/9.73 (combb bool (fun bool bool) int) fconj))) % 9.53/9.73 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.53/9.73 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (fun int int) (fun int bool))) % 9.53/9.73 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.53/9.73 (aa % 9.53/9.73 (fun (fun (fun int int) (fun int bool)) % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun int (fun (fun int int) (fun int bool))) % 9.53/9.73 (fun int % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.53/9.73 (combb (fun (fun int int) (fun int bool)) % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.53/9.73 (combb (fun int int) (fun int bool) (list int))) % 9.53/9.73 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.53/9.73 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.53/9.73 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.53/9.73 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.53/9.73 (combb int bool int)) % 9.53/9.73 (fequal int)))) % 9.53/9.73 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.53/9.73 (aa (fun int (fun int int)) % 9.53/9.73 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.53/9.73 (combb int (fun int int) (list int)) (minus_minus int)) % 9.53/9.73 (aa (list int) (fun (list int) int) % 9.53/9.73 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.53/9.73 (combc (list int) (list int) int) % 9.53/9.73 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.53/9.73 (aa (fun (list int) (fun (list int) int)) % 9.53/9.73 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.53/9.73 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.53/9.73 (tl int))) % 9.53/9.73 xs))))))) % 9.53/9.73 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.53/9.73 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.53/9.73 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.53/9.73 (combc (list int) (fun atom bool) (fun int bool)) % 9.53/9.73 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.53/9.73 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.53/9.73 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.53/9.73 (list int)) % 9.53/9.73 (combc int (fun atom bool) bool)) % 9.53/9.73 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (fun (fun (list int) (fun int atom)) % 9.53/9.73 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.53/9.73 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.53/9.73 (aa (fun atom (fun (fun atom bool) bool)) % 9.53/9.73 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.53/9.73 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.53/9.73 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.53/9.73 (aa (fun atom bool) (fun atom bool) % 9.53/9.73 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) (combs atom bool bool) % 9.53/9.73 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.53/9.73 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.53/9.73 (combb bool (fun bool bool) atom) fconj) % 9.53/9.73 (aa (fun atom bool) (fun atom bool) % 9.53/9.73 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.53/9.73 (combc atom (fun atom bool) bool) (member atom)) % 9.53/9.73 (set atom as)))) % 9.53/9.73 (atom_case bool % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.53/9.73 (combk (fun (list int) bool) int) % 9.53/9.73 (list_case bool int fFalse % 9.53/9.73 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.53/9.73 (aa (fun bool (fun (list int) bool)) % 9.53/9.73 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.53/9.73 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.53/9.73 (aa int (fun int bool) % 9.53/9.73 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.53/9.73 (ord_less int)) % 9.53/9.73 (zero_zero int))))) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.53/9.73 (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.53/9.73 (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))) % 9.53/9.73 (zlcms % 9.53/9.73 (map atom int divisor % 9.53/9.73 (filter atom % 9.53/9.73 (atom_case bool % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.53/9.73 as)))) % 9.53/9.73 (one_one int))) % 9.53/9.73 (zlcms % 9.53/9.73 (map atom int divisor % 9.53/9.73 (filter atom % 9.53/9.73 (atom_case bool % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.53/9.73 as))))) % 9.53/9.73 (aa atom int divisor a)) % 9.53/9.73 (div_mod int % 9.53/9.73 (aa int int (aa int (fun int int) (minus_minus int) (div_mod int n (aa atom int divisor a))) % 9.53/9.73 (div_mod int % 9.53/9.73 (aa int int % 9.53/9.73 (times_times int % 9.53/9.73 (plus_plus int % 9.53/9.73 (div_div int % 9.53/9.73 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.53/9.73 (big_linorder_Min int % 9.53/9.73 (collect int % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.53/9.73 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.53/9.73 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.53/9.73 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.53/9.73 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.53/9.73 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.53/9.73 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.53/9.73 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.53/9.73 (combb (fun int bool) bool (list int)) (fEx int))) % 9.53/9.73 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.53/9.73 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.53/9.73 (aa % 9.53/9.73 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.53/9.73 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.53/9.73 (combs (list int) (fun int bool) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (aa % 9.53/9.73 (fun (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.53/9.73 (combb (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.53/9.73 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.53/9.73 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.53/9.73 (combs int bool bool))) % 9.53/9.73 (aa (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (fun (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.53/9.73 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.53/9.73 int) % 9.53/9.73 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.53/9.73 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.53/9.73 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.53/9.73 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.53/9.73 (combb bool (fun bool bool) int) fconj))) % 9.53/9.73 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.53/9.73 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.53/9.73 (aa (fun int (fun (fun int int) (fun int bool))) % 9.53/9.73 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.53/9.73 (aa % 9.53/9.73 (fun (fun (fun int int) (fun int bool)) % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.53/9.73 (fun (fun int (fun (fun int int) (fun int bool))) % 9.53/9.73 (fun int % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.53/9.73 (combb (fun (fun int int) (fun int bool)) % 9.53/9.73 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.53/9.73 (combb (fun int int) (fun int bool) (list int))) % 9.53/9.73 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.53/9.73 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.53/9.73 (fun (fun int (fun int bool)) % 9.53/9.73 (fun int (fun (fun int int) (fun int bool)))) % 9.53/9.73 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.53/9.73 (combb int bool int)) % 9.53/9.73 (fequal int)))) % 9.53/9.73 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.53/9.73 (aa (fun int (fun int int)) % 9.53/9.73 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.53/9.73 (combb int (fun int int) (list int)) (minus_minus int)) % 9.53/9.73 (aa (list int) (fun (list int) int) % 9.53/9.73 (aa (fun (list int) (fun (list int) int)) % 9.53/9.73 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.53/9.73 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.53/9.73 (aa (fun (list int) (fun (list int) int)) % 9.53/9.73 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.53/9.73 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.53/9.73 (tl int))) % 9.53/9.73 xs))))))) % 9.53/9.73 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.53/9.73 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.53/9.73 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.53/9.73 (combc (list int) (fun atom bool) (fun int bool)) % 9.53/9.73 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.53/9.73 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.53/9.73 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.53/9.73 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.53/9.73 (list int)) % 9.53/9.73 (combc int (fun atom bool) bool)) % 9.53/9.73 (aa (fun (list int) (fun int atom)) % 9.53/9.73 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (fun (fun (list int) (fun int atom)) % 9.53/9.73 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.53/9.73 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.53/9.73 (aa (fun atom (fun (fun atom bool) bool)) % 9.53/9.73 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.53/9.73 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.53/9.73 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.53/9.73 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.53/9.73 (collect atom % 9.53/9.73 (aa (fun atom bool) (fun atom bool) % 9.53/9.73 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.53/9.73 (combs atom bool bool) % 9.53/9.73 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.53/9.73 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.53/9.73 (combb bool (fun bool bool) atom) fconj) % 9.53/9.73 (aa (fun atom bool) (fun atom bool) % 9.53/9.73 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.53/9.73 (combc atom (fun atom bool) bool) (member atom)) % 9.53/9.73 (set atom as)))) % 9.53/9.73 (atom_case bool % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.53/9.73 (combk (fun (list int) bool) int) % 9.53/9.73 (list_case bool int fFalse % 9.53/9.73 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.53/9.73 (aa (fun bool (fun (list int) bool)) % 9.53/9.73 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.53/9.73 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.53/9.73 (aa int (fun int bool) % 9.53/9.73 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.53/9.73 (ord_less int)) % 9.53/9.73 (zero_zero int))))) % 9.53/9.73 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.53/9.73 (combk (fun int (fun (list int) bool)) int) % 9.53/9.73 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.53/9.73 (combk (fun (list int) bool) int) % 9.53/9.73 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.69/9.84 (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.69/9.84 (zlcms % 9.69/9.84 (map atom int divisor % 9.69/9.84 (filter atom % 9.69/9.84 (atom_case bool % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.69/9.84 as)))) % 9.69/9.84 (one_one int))) % 9.69/9.84 (zlcms % 9.69/9.84 (map atom int divisor % 9.69/9.84 (filter atom % 9.69/9.84 (atom_case bool % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.69/9.84 as)))) % 9.69/9.84 (aa atom int divisor a))) % 9.69/9.84 (aa atom int divisor a)) % 9.69/9.84 Clause #3508 (by forward demodulation #[3507, 2047]): Ne % 9.69/9.84 (div_mod int % 9.69/9.84 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.69/9.84 (aa int int % 9.69/9.84 (times_times int % 9.69/9.84 (plus_plus int % 9.69/9.84 (div_div int % 9.69/9.84 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.69/9.84 (big_linorder_Min int % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.69/9.84 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.69/9.84 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.69/9.84 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.69/9.84 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.69/9.84 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.69/9.84 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.69/9.84 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.69/9.84 (combb (fun int bool) bool (list int)) (fEx int))) % 9.69/9.84 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.69/9.84 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.69/9.84 (aa % 9.69/9.84 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.69/9.84 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.69/9.84 (combs (list int) (fun int bool) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (aa % 9.69/9.84 (fun (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.69/9.84 (combb (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.69/9.84 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.69/9.84 (combs int bool bool))) % 9.69/9.84 (aa (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (fun (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.69/9.84 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.69/9.84 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.69/9.84 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.69/9.84 (combb bool (fun bool bool) int) fconj))) % 9.69/9.84 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.69/9.84 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (fun int int) (fun int bool))) % 9.69/9.84 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.69/9.84 (aa % 9.69/9.84 (fun (fun (fun int int) (fun int bool)) % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun int (fun (fun int int) (fun int bool))) % 9.69/9.84 (fun int % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.69/9.84 (combb (fun (fun int int) (fun int bool)) % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.69/9.84 (combb (fun int int) (fun int bool) (list int))) % 9.69/9.84 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.69/9.84 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.69/9.84 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.69/9.84 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.69/9.84 (combb int bool int)) % 9.69/9.84 (fequal int)))) % 9.69/9.84 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.69/9.84 (aa (fun int (fun int int)) % 9.69/9.84 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.69/9.84 (combb int (fun int int) (list int)) (minus_minus int)) % 9.69/9.84 (aa (list int) (fun (list int) int) % 9.69/9.84 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.69/9.84 (combc (list int) (list int) int) % 9.69/9.84 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.69/9.84 (aa (fun (list int) (fun (list int) int)) % 9.69/9.84 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.69/9.84 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.69/9.84 (tl int))) % 9.69/9.84 xs))))))) % 9.69/9.84 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.69/9.84 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.69/9.84 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.69/9.84 (combc (list int) (fun atom bool) (fun int bool)) % 9.69/9.84 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.69/9.84 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.69/9.84 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.69/9.84 (list int)) % 9.69/9.84 (combc int (fun atom bool) bool)) % 9.69/9.84 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (fun (fun (list int) (fun int atom)) % 9.69/9.84 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.69/9.84 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.69/9.84 (aa (fun atom (fun (fun atom bool) bool)) % 9.69/9.84 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.69/9.84 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.69/9.84 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.69/9.84 (aa (fun atom bool) (fun atom bool) % 9.69/9.84 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) (combs atom bool bool) % 9.69/9.84 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.69/9.84 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.69/9.84 (combb bool (fun bool bool) atom) fconj) % 9.69/9.84 (aa (fun atom bool) (fun atom bool) % 9.69/9.84 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.69/9.84 (combc atom (fun atom bool) bool) (member atom)) % 9.69/9.84 (set atom as)))) % 9.69/9.84 (atom_case bool % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.69/9.84 (combk (fun (list int) bool) int) % 9.69/9.84 (list_case bool int fFalse % 9.69/9.84 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.69/9.84 (aa (fun bool (fun (list int) bool)) % 9.69/9.84 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.69/9.84 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.69/9.84 (aa int (fun int bool) % 9.69/9.84 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.69/9.84 (ord_less int)) % 9.69/9.84 (zero_zero int))))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.69/9.84 (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.69/9.84 (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))) % 9.69/9.84 (zlcms % 9.69/9.84 (map atom int divisor % 9.69/9.84 (filter atom % 9.69/9.84 (atom_case bool % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.69/9.84 as)))) % 9.69/9.84 (one_one int))) % 9.69/9.84 (zlcms % 9.69/9.84 (map atom int divisor % 9.69/9.84 (filter atom % 9.69/9.84 (atom_case bool % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.69/9.84 (combk (fun int (fun (list int) bool)) int) % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.69/9.84 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.69/9.84 as))))) % 9.69/9.84 (aa atom int divisor a)) % 9.69/9.84 (div_mod int % 9.69/9.84 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.69/9.84 (div_mod int % 9.69/9.84 (aa int int % 9.69/9.84 (times_times int % 9.69/9.84 (plus_plus int % 9.69/9.84 (div_div int % 9.69/9.84 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.69/9.84 (big_linorder_Min int % 9.69/9.84 (collect int % 9.69/9.84 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.69/9.84 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.69/9.84 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.69/9.84 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.69/9.84 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.69/9.84 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.69/9.84 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.69/9.84 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.69/9.84 (combb (fun int bool) bool (list int)) (fEx int))) % 9.69/9.84 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.69/9.84 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.69/9.84 (aa % 9.69/9.84 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.69/9.84 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.69/9.84 (combs (list int) (fun int bool) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (aa % 9.69/9.84 (fun (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.69/9.84 (combb (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.69/9.84 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.69/9.84 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.69/9.84 (combs int bool bool))) % 9.69/9.84 (aa (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (fun (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.69/9.84 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.69/9.84 int) % 9.69/9.84 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.69/9.84 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.69/9.84 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.69/9.84 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.69/9.84 (combb bool (fun bool bool) int) fconj))) % 9.69/9.84 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.69/9.84 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.69/9.84 (aa (fun int (fun (fun int int) (fun int bool))) % 9.69/9.84 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.69/9.84 (aa % 9.69/9.84 (fun (fun (fun int int) (fun int bool)) % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.69/9.84 (fun (fun int (fun (fun int int) (fun int bool))) % 9.69/9.84 (fun int % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.69/9.84 (combb (fun (fun int int) (fun int bool)) % 9.69/9.84 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.69/9.84 (combb (fun int int) (fun int bool) (list int))) % 9.69/9.84 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.69/9.84 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.69/9.84 (fun (fun int (fun int bool)) % 9.69/9.84 (fun int (fun (fun int int) (fun int bool)))) % 9.69/9.84 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.69/9.84 (combb int bool int)) % 9.69/9.84 (fequal int)))) % 9.69/9.84 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.69/9.84 (aa (fun int (fun int int)) % 9.69/9.84 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.69/9.84 (combb int (fun int int) (list int)) (minus_minus int)) % 9.69/9.84 (aa (list int) (fun (list int) int) % 9.69/9.84 (aa (fun (list int) (fun (list int) int)) % 9.69/9.84 (fun (list int) (fun (list int) int)) (combc (list int) (list int) int) % 9.69/9.84 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.69/9.84 (aa (fun (list int) (fun (list int) int)) % 9.69/9.84 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.69/9.84 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.69/9.84 (tl int))) % 9.69/9.84 xs))))))) % 9.69/9.84 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.69/9.84 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.69/9.84 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.69/9.84 (combc (list int) (fun atom bool) (fun int bool)) % 9.69/9.84 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.69/9.84 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.69/9.84 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.69/9.84 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.69/9.84 (list int)) % 9.69/9.84 (combc int (fun atom bool) bool)) % 9.69/9.84 (aa (fun (list int) (fun int atom)) % 9.69/9.84 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (fun (fun (list int) (fun int atom)) % 9.69/9.84 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.69/9.84 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.69/9.84 (aa (fun atom (fun (fun atom bool) bool)) % 9.69/9.84 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.69/9.84 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.69/9.84 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.69/9.84 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.69/9.84 (collect atom % 9.69/9.84 (aa (fun atom bool) (fun atom bool) % 9.69/9.84 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.69/9.84 (combs atom bool bool) % 9.69/9.84 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.69/9.84 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.69/9.84 (combb bool (fun bool bool) atom) fconj) % 9.69/9.84 (aa (fun atom bool) (fun atom bool) % 9.69/9.84 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.69/9.84 (combc atom (fun atom bool) bool) (member atom)) % 9.69/9.84 (set atom as)))) % 9.69/9.84 (atom_case bool % 9.69/9.84 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (list_case bool int fFalse % 9.77/9.95 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.77/9.95 (aa (fun bool (fun (list int) bool)) % 9.77/9.95 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.77/9.95 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.77/9.95 (aa int (fun int bool) % 9.77/9.95 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.77/9.95 (ord_less int)) % 9.77/9.95 (zero_zero int))))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.77/9.95 (zlcms % 9.77/9.95 (map atom int divisor % 9.77/9.95 (filter atom % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.77/9.95 as)))) % 9.77/9.95 (one_one int))) % 9.77/9.95 (zlcms % 9.77/9.95 (map atom int divisor % 9.77/9.95 (filter atom % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.77/9.95 as)))) % 9.77/9.95 (aa atom int divisor a))) % 9.77/9.95 (aa atom int divisor a)) % 9.77/9.95 Clause #3509 (by forward demodulation #[3508, 2328]): Ne % 9.77/9.95 (div_mod int % 9.77/9.95 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.77/9.95 (aa int int % 9.77/9.95 (times_times int % 9.77/9.95 (plus_plus int % 9.77/9.95 (div_div int % 9.77/9.95 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.77/9.95 (big_linorder_Min int % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.77/9.95 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.77/9.95 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.77/9.95 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.77/9.95 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.77/9.95 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.77/9.95 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.77/9.95 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.77/9.95 (combb (fun int bool) bool (list int)) (fEx int))) % 9.77/9.95 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.77/9.95 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.77/9.95 (aa % 9.77/9.95 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.77/9.95 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.77/9.95 (combs (list int) (fun int bool) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (aa % 9.77/9.95 (fun (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.77/9.95 (combb (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.77/9.95 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.77/9.95 (combs int bool bool))) % 9.77/9.95 (aa (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (fun (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.77/9.95 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.77/9.95 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.77/9.95 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.77/9.95 (combb bool (fun bool bool) int) fconj))) % 9.77/9.95 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.77/9.95 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (fun int int) (fun int bool))) % 9.77/9.95 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.77/9.95 (aa % 9.77/9.95 (fun (fun (fun int int) (fun int bool)) % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun int (fun (fun int int) (fun int bool))) % 9.77/9.95 (fun int % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.77/9.95 (combb (fun (fun int int) (fun int bool)) % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.77/9.95 (combb (fun int int) (fun int bool) (list int))) % 9.77/9.95 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.77/9.95 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.77/9.95 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.77/9.95 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.77/9.95 (combb int bool int)) % 9.77/9.95 (fequal int)))) % 9.77/9.95 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.77/9.95 (aa (fun int (fun int int)) % 9.77/9.95 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.77/9.95 (combb int (fun int int) (list int)) (minus_minus int)) % 9.77/9.95 (aa (list int) (fun (list int) int) % 9.77/9.95 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.77/9.95 (combc (list int) (list int) int) % 9.77/9.95 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.77/9.95 (aa (fun (list int) (fun (list int) int)) % 9.77/9.95 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.77/9.95 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.77/9.95 (tl int))) % 9.77/9.95 xs))))))) % 9.77/9.95 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.77/9.95 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.77/9.95 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.77/9.95 (combc (list int) (fun atom bool) (fun int bool)) % 9.77/9.95 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.77/9.95 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.77/9.95 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.77/9.95 (list int)) % 9.77/9.95 (combc int (fun atom bool) bool)) % 9.77/9.95 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (fun (fun (list int) (fun int atom)) % 9.77/9.95 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.77/9.95 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.77/9.95 (aa (fun atom (fun (fun atom bool) bool)) % 9.77/9.95 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.77/9.95 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.77/9.95 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.77/9.95 (aa (fun atom bool) (fun atom bool) % 9.77/9.95 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) (combs atom bool bool) % 9.77/9.95 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.77/9.95 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.77/9.95 (combb bool (fun bool bool) atom) fconj) % 9.77/9.95 (aa (fun atom bool) (fun atom bool) % 9.77/9.95 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.77/9.95 (combc atom (fun atom bool) bool) (member atom)) % 9.77/9.95 (set atom as)))) % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (list_case bool int fFalse % 9.77/9.95 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.77/9.95 (aa (fun bool (fun (list int) bool)) % 9.77/9.95 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.77/9.95 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.77/9.95 (aa int (fun int bool) % 9.77/9.95 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.77/9.95 (ord_less int)) % 9.77/9.95 (zero_zero int))))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))) % 9.77/9.95 (zlcms % 9.77/9.95 (map atom int divisor % 9.77/9.95 (filter atom % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.77/9.95 as)))) % 9.77/9.95 (one_one int))) % 9.77/9.95 (zlcms % 9.77/9.95 (map atom int divisor % 9.77/9.95 (filter atom % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.77/9.95 as))))) % 9.77/9.95 (aa atom int divisor a)) % 9.77/9.95 (div_mod int % 9.77/9.95 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.77/9.95 (aa int int % 9.77/9.95 (times_times int % 9.77/9.95 (plus_plus int % 9.77/9.95 (div_div int % 9.77/9.95 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.77/9.95 (big_linorder_Min int % 9.77/9.95 (collect int % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.77/9.95 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.77/9.95 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.77/9.95 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.77/9.95 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.77/9.95 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.77/9.95 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.77/9.95 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.77/9.95 (combb (fun int bool) bool (list int)) (fEx int))) % 9.77/9.95 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.77/9.95 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.77/9.95 (aa % 9.77/9.95 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.77/9.95 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.77/9.95 (combs (list int) (fun int bool) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (aa % 9.77/9.95 (fun (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.77/9.95 (combb (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.77/9.95 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.77/9.95 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.77/9.95 (combs int bool bool))) % 9.77/9.95 (aa (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (fun (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.77/9.95 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) % 9.77/9.95 int) % 9.77/9.95 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.77/9.95 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.77/9.95 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.77/9.95 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.77/9.95 (combb bool (fun bool bool) int) fconj))) % 9.77/9.95 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.77/9.95 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.77/9.95 (aa (fun int (fun (fun int int) (fun int bool))) % 9.77/9.95 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.77/9.95 (aa % 9.77/9.95 (fun (fun (fun int int) (fun int bool)) % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.77/9.95 (fun (fun int (fun (fun int int) (fun int bool))) % 9.77/9.95 (fun int % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.77/9.95 (combb (fun (fun int int) (fun int bool)) % 9.77/9.95 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.77/9.95 (combb (fun int int) (fun int bool) (list int))) % 9.77/9.95 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.77/9.95 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.77/9.95 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.77/9.95 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.77/9.95 (combb int bool int)) % 9.77/9.95 (fequal int)))) % 9.77/9.95 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.77/9.95 (aa (fun int (fun int int)) % 9.77/9.95 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.77/9.95 (combb int (fun int int) (list int)) (minus_minus int)) % 9.77/9.95 (aa (list int) (fun (list int) int) % 9.77/9.95 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.77/9.95 (combc (list int) (list int) int) % 9.77/9.95 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.77/9.95 (aa (fun (list int) (fun (list int) int)) % 9.77/9.95 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.77/9.95 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.77/9.95 (tl int))) % 9.77/9.95 xs))))))) % 9.77/9.95 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.77/9.95 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.77/9.95 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.77/9.95 (combc (list int) (fun atom bool) (fun int bool)) % 9.77/9.95 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.77/9.95 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.77/9.95 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.77/9.95 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.77/9.95 (list int)) % 9.77/9.95 (combc int (fun atom bool) bool)) % 9.77/9.95 (aa (fun (list int) (fun int atom)) % 9.77/9.95 (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (fun (fun (list int) (fun int atom)) % 9.77/9.95 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.77/9.95 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.77/9.95 (aa (fun atom (fun (fun atom bool) bool)) % 9.77/9.95 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.77/9.95 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.77/9.95 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.77/9.95 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.77/9.95 (collect atom % 9.77/9.95 (aa (fun atom bool) (fun atom bool) % 9.77/9.95 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.77/9.95 (combs atom bool bool) % 9.77/9.95 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.77/9.95 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.77/9.95 (combb bool (fun bool bool) atom) fconj) % 9.77/9.95 (aa (fun atom bool) (fun atom bool) % 9.77/9.95 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.77/9.95 (combc atom (fun atom bool) bool) (member atom)) % 9.77/9.95 (set atom as)))) % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (list_case bool int fFalse % 9.77/9.95 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.77/9.95 (aa (fun bool (fun (list int) bool)) % 9.77/9.95 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.77/9.95 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.77/9.95 (aa int (fun int bool) % 9.77/9.95 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.77/9.95 (ord_less int)) % 9.77/9.95 (zero_zero int))))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.77/9.95 (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))))) % 9.77/9.95 (zlcms % 9.77/9.95 (map atom int divisor % 9.77/9.95 (filter atom % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.77/9.95 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.77/9.95 (combk (fun int (fun (list int) bool)) int) % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.77/9.95 as)))) % 9.77/9.95 (one_one int))) % 9.77/9.95 (zlcms % 9.77/9.95 (map atom int divisor % 9.77/9.95 (filter atom % 9.77/9.95 (atom_case bool % 9.77/9.95 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.77/9.95 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.84/10.05 as))))) % 9.84/10.05 (aa atom int divisor a)) % 9.84/10.05 Clause #3510 (by forward demodulation #[3509, 1996]): Ne % 9.84/10.05 (div_mod int % 9.84/10.05 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.84/10.05 (aa int int % 9.84/10.05 (times_times int % 9.84/10.05 (plus_plus int % 9.84/10.05 (div_div int % 9.84/10.05 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.84/10.05 (big_linorder_Min int % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.84/10.05 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.84/10.05 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.84/10.05 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.84/10.05 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.84/10.05 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.84/10.05 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.84/10.05 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.84/10.05 (combb (fun int bool) bool (list int)) (fEx int))) % 9.84/10.05 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.84/10.05 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.84/10.05 (aa % 9.84/10.05 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.84/10.05 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.84/10.05 (combs (list int) (fun int bool) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (aa % 9.84/10.05 (fun (fun (list int) (fun int (fun bool bool))) % 9.84/10.05 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.84/10.05 (combb (fun (list int) (fun int (fun bool bool))) % 9.84/10.05 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.84/10.05 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int (fun bool bool))) % 9.84/10.05 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.84/10.05 (combs int bool bool))) % 9.84/10.05 (aa (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (fun (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.84/10.05 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.84/10.05 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.84/10.05 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.84/10.05 (combb bool (fun bool bool) int) fconj))) % 9.84/10.05 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.84/10.05 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (fun int int) (fun int bool))) % 9.84/10.05 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.84/10.05 (aa % 9.84/10.05 (fun (fun (fun int int) (fun int bool)) % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun int (fun (fun int int) (fun int bool))) % 9.84/10.05 (fun int % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.84/10.05 (combb (fun (fun int int) (fun int bool)) % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.84/10.05 (combb (fun int int) (fun int bool) (list int))) % 9.84/10.05 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.84/10.05 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.84/10.05 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.84/10.05 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.84/10.05 (combb int bool int)) % 9.84/10.05 (fequal int)))) % 9.84/10.05 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.84/10.05 (aa (fun int (fun int int)) % 9.84/10.05 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.84/10.05 (combb int (fun int int) (list int)) (minus_minus int)) % 9.84/10.05 (aa (list int) (fun (list int) int) % 9.84/10.05 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.84/10.05 (combc (list int) (list int) int) % 9.84/10.05 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.84/10.05 (aa (fun (list int) (fun (list int) int)) % 9.84/10.05 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.84/10.05 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.84/10.05 (tl int))) % 9.84/10.05 xs))))))) % 9.84/10.05 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.84/10.05 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.84/10.05 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.84/10.05 (combc (list int) (fun atom bool) (fun int bool)) % 9.84/10.05 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.84/10.05 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.84/10.05 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.84/10.05 (list int)) % 9.84/10.05 (combc int (fun atom bool) bool)) % 9.84/10.05 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (fun (fun (list int) (fun int atom)) % 9.84/10.05 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.84/10.05 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.84/10.05 (aa (fun atom (fun (fun atom bool) bool)) % 9.84/10.05 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.84/10.05 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.84/10.05 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.84/10.05 (aa (fun atom bool) (fun atom bool) % 9.84/10.05 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) (combs atom bool bool) % 9.84/10.05 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.84/10.05 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.84/10.05 (combb bool (fun bool bool) atom) fconj) % 9.84/10.05 (aa (fun atom bool) (fun atom bool) % 9.84/10.05 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.84/10.05 (combc atom (fun atom bool) bool) (member atom)) % 9.84/10.05 (set atom as)))) % 9.84/10.05 (atom_case bool % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.84/10.05 (combk (fun (list int) bool) int) % 9.84/10.05 (list_case bool int fFalse % 9.84/10.05 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.84/10.05 (aa (fun bool (fun (list int) bool)) % 9.84/10.05 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.84/10.05 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.84/10.05 (aa int (fun int bool) % 9.84/10.05 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.84/10.05 (ord_less int)) % 9.84/10.05 (zero_zero int))))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.84/10.05 (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.84/10.05 (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))) % 9.84/10.05 (zlcms % 9.84/10.05 (map atom int divisor % 9.84/10.05 (filter atom % 9.84/10.05 (atom_case bool % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.84/10.05 as)))) % 9.84/10.05 (one_one int))) % 9.84/10.05 (zlcms % 9.84/10.05 (map atom int divisor % 9.84/10.05 (filter atom % 9.84/10.05 (atom_case bool % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.84/10.05 as))))) % 9.84/10.05 (aa atom int divisor a)) % 9.84/10.05 (div_mod int % 9.84/10.05 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.84/10.05 (aa int int % 9.84/10.05 (times_times int % 9.84/10.05 (plus_plus int % 9.84/10.05 (div_div int % 9.84/10.05 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.84/10.05 (big_linorder_Min int % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.84/10.05 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.84/10.05 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.84/10.05 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.84/10.05 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.84/10.05 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.84/10.05 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.84/10.05 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.84/10.05 (combb (fun int bool) bool (list int)) (fEx int))) % 9.84/10.05 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.84/10.05 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.84/10.05 (aa % 9.84/10.05 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.84/10.05 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.84/10.05 (combs (list int) (fun int bool) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (aa % 9.84/10.05 (fun (fun (list int) (fun int (fun bool bool))) % 9.84/10.05 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.84/10.05 (combb (fun (list int) (fun int (fun bool bool))) % 9.84/10.05 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.84/10.05 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int (fun bool bool))) % 9.84/10.05 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.84/10.05 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.84/10.05 (combs int bool bool))) % 9.84/10.05 (aa (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (fun (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.84/10.05 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.84/10.05 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.84/10.05 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.84/10.05 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.84/10.05 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.84/10.05 (combb bool (fun bool bool) int) fconj))) % 9.84/10.05 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.84/10.05 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.84/10.05 (aa (fun int (fun (fun int int) (fun int bool))) % 9.84/10.05 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.84/10.05 (aa % 9.84/10.05 (fun (fun (fun int int) (fun int bool)) % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.84/10.05 (fun (fun int (fun (fun int int) (fun int bool))) % 9.84/10.05 (fun int % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.84/10.05 (combb (fun (fun int int) (fun int bool)) % 9.84/10.05 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.84/10.05 (combb (fun int int) (fun int bool) (list int))) % 9.84/10.05 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.84/10.05 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.84/10.05 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.84/10.05 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.84/10.05 (combb int bool int)) % 9.84/10.05 (fequal int)))) % 9.84/10.05 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.84/10.05 (aa (fun int (fun int int)) % 9.84/10.05 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.84/10.05 (combb int (fun int int) (list int)) (minus_minus int)) % 9.84/10.05 (aa (list int) (fun (list int) int) % 9.84/10.05 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.84/10.05 (combc (list int) (list int) int) % 9.84/10.05 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.84/10.05 (aa (fun (list int) (fun (list int) int)) % 9.84/10.05 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.84/10.05 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.84/10.05 (tl int))) % 9.84/10.05 xs))))))) % 9.84/10.05 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.84/10.05 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.84/10.05 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.84/10.05 (combc (list int) (fun atom bool) (fun int bool)) % 9.84/10.05 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.84/10.05 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.84/10.05 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.84/10.05 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.84/10.05 (list int)) % 9.84/10.05 (combc int (fun atom bool) bool)) % 9.84/10.05 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (fun (fun (list int) (fun int atom)) % 9.84/10.05 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.84/10.05 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.84/10.05 (aa (fun atom (fun (fun atom bool) bool)) % 9.84/10.05 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.84/10.05 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.84/10.05 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.84/10.05 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.84/10.05 (collect atom % 9.84/10.05 (aa (fun atom bool) (fun atom bool) % 9.84/10.05 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) % 9.84/10.05 (combs atom bool bool) % 9.84/10.05 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.84/10.05 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.84/10.05 (combb bool (fun bool bool) atom) fconj) % 9.84/10.05 (aa (fun atom bool) (fun atom bool) % 9.84/10.05 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.84/10.05 (combc atom (fun atom bool) bool) (member atom)) % 9.84/10.05 (set atom as)))) % 9.84/10.05 (atom_case bool % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.84/10.05 (combk (fun (list int) bool) int) % 9.84/10.05 (list_case bool int fFalse % 9.84/10.05 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.84/10.05 (aa (fun bool (fun (list int) bool)) % 9.84/10.05 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.84/10.05 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.84/10.05 (aa int (fun int bool) % 9.84/10.05 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.84/10.05 (ord_less int)) % 9.84/10.05 (zero_zero int))))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.84/10.05 (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.84/10.05 (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)))))))))))) % 9.84/10.05 (zlcms % 9.84/10.05 (map atom int divisor % 9.84/10.05 (filter atom % 9.84/10.05 (atom_case bool % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.84/10.05 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.84/10.05 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.84/10.05 (combk (fun int (fun (list int) bool)) int) % 9.84/10.05 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.15 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.98/10.15 as)))) % 9.98/10.15 (one_one int))) % 9.98/10.15 (zlcms % 9.98/10.15 (map atom int divisor % 9.98/10.15 (filter atom % 9.98/10.15 (atom_case bool % 9.98/10.15 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.15 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.98/10.15 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.15 (combk (fun int (fun (list int) bool)) int) % 9.98/10.15 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.15 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.98/10.15 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.15 (combk (fun int (fun (list int) bool)) int) % 9.98/10.15 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.15 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.98/10.15 as))))) % 9.98/10.15 (aa atom int divisor a)) % 9.98/10.15 Clause #3511 (by forward demodulation #[3510, 1996]): Ne % 9.98/10.15 (div_mod int % 9.98/10.15 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.98/10.15 (aa int int % 9.98/10.15 (times_times int % 9.98/10.15 (plus_plus int % 9.98/10.15 (div_div int % 9.98/10.15 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.98/10.15 (big_linorder_Min int % 9.98/10.15 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.98/10.15 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.98/10.15 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.98/10.15 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.98/10.15 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.98/10.15 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.98/10.15 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.98/10.15 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.98/10.15 (combb (fun int bool) bool (list int)) (fEx int))) % 9.98/10.15 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.98/10.15 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.98/10.15 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.98/10.15 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.98/10.15 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.15 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.98/10.15 (aa % 9.98/10.15 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.98/10.15 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.98/10.15 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.15 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.98/10.15 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.98/10.15 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.98/10.15 (combs (list int) (fun int bool) (fun int bool))) % 9.98/10.15 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.98/10.15 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.15 (aa % 9.98/10.15 (fun (fun (list int) (fun int (fun bool bool))) % 9.98/10.15 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.15 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.98/10.15 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.98/10.15 (combb (fun (list int) (fun int (fun bool bool))) % 9.98/10.15 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.98/10.15 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.98/10.15 (fun (fun (list int) (fun int (fun bool bool))) % 9.98/10.15 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.15 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.98/10.15 (combs int bool bool))) % 9.98/10.15 (aa (fun int (fun (list int) (fun int bool))) % 9.98/10.15 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.98/10.15 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.98/10.15 (fun (fun int (fun (list int) (fun int bool))) % 9.98/10.15 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.98/10.15 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.98/10.15 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.98/10.15 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.98/10.15 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.98/10.15 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.98/10.15 (combb bool (fun bool bool) int) fconj))) % 9.98/10.15 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.98/10.15 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.98/10.15 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.98/10.15 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.98/10.15 (aa (fun int (fun (fun int int) (fun int bool))) % 9.98/10.15 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.98/10.15 (aa % 9.98/10.15 (fun (fun (fun int int) (fun int bool)) % 9.98/10.15 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.98/10.15 (fun (fun int (fun (fun int int) (fun int bool))) % 9.98/10.15 (fun int % 9.98/10.15 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.98/10.15 (combb (fun (fun int int) (fun int bool)) % 9.98/10.15 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.98/10.15 (combb (fun int int) (fun int bool) (list int))) % 9.98/10.15 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.98/10.15 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.98/10.15 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.98/10.15 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.98/10.15 (combb int bool int)) % 9.98/10.15 (fequal int)))) % 9.98/10.15 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.98/10.15 (aa (fun int (fun int int)) % 9.98/10.15 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.98/10.16 (combb int (fun int int) (list int)) (minus_minus int)) % 9.98/10.16 (aa (list int) (fun (list int) int) % 9.98/10.16 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.98/10.16 (combc (list int) (list int) int) % 9.98/10.16 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.98/10.16 (aa (fun (list int) (fun (list int) int)) % 9.98/10.16 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.98/10.16 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.98/10.16 (tl int))) % 9.98/10.16 xs))))))) % 9.98/10.16 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.98/10.16 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.98/10.16 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.98/10.16 (combc (list int) (fun atom bool) (fun int bool)) % 9.98/10.16 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.98/10.16 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.98/10.16 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.98/10.16 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.98/10.16 (list int)) % 9.98/10.16 (combc int (fun atom bool) bool)) % 9.98/10.16 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (fun (fun (list int) (fun int atom)) % 9.98/10.16 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.98/10.16 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.98/10.16 (aa (fun atom (fun (fun atom bool) bool)) % 9.98/10.16 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.98/10.16 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.98/10.16 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.98/10.16 (aa (fun atom bool) (fun atom bool) % 9.98/10.16 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) (combs atom bool bool) % 9.98/10.16 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.98/10.16 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.98/10.16 (combb bool (fun bool bool) atom) fconj) % 9.98/10.16 (aa (fun atom bool) (fun atom bool) % 9.98/10.16 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.98/10.16 (combc atom (fun atom bool) bool) (member atom)) % 9.98/10.16 (set atom as)))) % 9.98/10.16 (atom_case bool % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.98/10.16 (combk (fun (list int) bool) int) % 9.98/10.16 (list_case bool int fFalse % 9.98/10.16 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.98/10.16 (aa (fun bool (fun (list int) bool)) % 9.98/10.16 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.98/10.16 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.98/10.16 (aa int (fun int bool) % 9.98/10.16 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.98/10.16 (ord_less int)) % 9.98/10.16 (zero_zero int))))) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.98/10.16 (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.98/10.16 (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))) % 9.98/10.16 (zlcms % 9.98/10.16 (map atom int divisor % 9.98/10.16 (filter atom % 9.98/10.16 (atom_case bool % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.98/10.16 as)))) % 9.98/10.16 (one_one int))) % 9.98/10.16 (zlcms % 9.98/10.16 (map atom int divisor % 9.98/10.16 (filter atom % 9.98/10.16 (atom_case bool % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.98/10.16 as))))) % 9.98/10.16 (aa atom int divisor a)) % 9.98/10.16 (div_mod int % 9.98/10.16 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.98/10.16 (aa int int % 9.98/10.16 (times_times int % 9.98/10.16 (plus_plus int % 9.98/10.16 (div_div int % 9.98/10.16 (aa int int (aa int (fun int int) (minus_minus int) n) % 9.98/10.16 (big_linorder_Min int % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int bool) % 9.98/10.16 (aa (fun (fun (list int) bool) bool) (fun (fun int (fun (list int) bool)) (fun int bool)) % 9.98/10.16 (combb (fun (list int) bool) bool int) (fEx (list int))) % 9.98/10.16 (aa (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool)) % 9.98/10.16 (aa (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.98/10.16 (fun (fun int (fun (list int) (fun int bool))) (fun int (fun (list int) bool))) % 9.98/10.16 (combb (fun (list int) (fun int bool)) (fun (list int) bool) int) % 9.98/10.16 (aa (fun (fun int bool) bool) (fun (fun (list int) (fun int bool)) (fun (list int) bool)) % 9.98/10.16 (combb (fun int bool) bool (list int)) (fEx int))) % 9.98/10.16 (aa (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool))) % 9.98/10.16 (aa (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.98/10.16 (fun (fun (list int) (fun int bool)) (fun int (fun (list int) (fun int bool)))) % 9.98/10.16 (combc int (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) % 9.98/10.16 (aa (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.16 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.98/10.16 (aa % 9.98/10.16 (fun (fun (list int) (fun (fun int bool) (fun int bool))) % 9.98/10.16 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool)))) % 9.98/10.16 (fun (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.16 (fun int (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))))) % 9.98/10.16 (combb (fun (list int) (fun (fun int bool) (fun int bool))) % 9.98/10.16 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int bool))) int) % 9.98/10.16 (combs (list int) (fun int bool) (fun int bool))) % 9.98/10.16 (aa (fun int (fun (list int) (fun int (fun bool bool)))) % 9.98/10.16 (fun int (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.16 (aa % 9.98/10.16 (fun (fun (list int) (fun int (fun bool bool))) % 9.98/10.16 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.16 (fun (fun int (fun (list int) (fun int (fun bool bool)))) % 9.98/10.16 (fun int (fun (list int) (fun (fun int bool) (fun int bool))))) % 9.98/10.16 (combb (fun (list int) (fun int (fun bool bool))) % 9.98/10.16 (fun (list int) (fun (fun int bool) (fun int bool))) int) % 9.98/10.16 (aa (fun (fun int (fun bool bool)) (fun (fun int bool) (fun int bool))) % 9.98/10.16 (fun (fun (list int) (fun int (fun bool bool))) % 9.98/10.16 (fun (list int) (fun (fun int bool) (fun int bool)))) % 9.98/10.16 (combb (fun int (fun bool bool)) (fun (fun int bool) (fun int bool)) (list int)) % 9.98/10.16 (combs int bool bool))) % 9.98/10.16 (aa (fun int (fun (list int) (fun int bool))) % 9.98/10.16 (fun int (fun (list int) (fun int (fun bool bool)))) % 9.98/10.16 (aa (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.98/10.16 (fun (fun int (fun (list int) (fun int bool))) % 9.98/10.16 (fun int (fun (list int) (fun int (fun bool bool))))) % 9.98/10.16 (combb (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool))) int) % 9.98/10.16 (aa (fun (fun int bool) (fun int (fun bool bool))) % 9.98/10.16 (fun (fun (list int) (fun int bool)) (fun (list int) (fun int (fun bool bool)))) % 9.98/10.16 (combb (fun int bool) (fun int (fun bool bool)) (list int)) % 9.98/10.16 (aa (fun bool (fun bool bool)) (fun (fun int bool) (fun int (fun bool bool))) % 9.98/10.16 (combb bool (fun bool bool) int) fconj))) % 9.98/10.16 (aa (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool))) % 9.98/10.16 (aa (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.98/10.16 (fun (fun (list int) (fun int int)) (fun int (fun (list int) (fun int bool)))) % 9.98/10.16 (combc int (fun (list int) (fun int int)) (fun (list int) (fun int bool))) % 9.98/10.16 (aa (fun int (fun (fun int int) (fun int bool))) % 9.98/10.16 (fun int (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.98/10.16 (aa % 9.98/10.16 (fun (fun (fun int int) (fun int bool)) % 9.98/10.16 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool)))) % 9.98/10.16 (fun (fun int (fun (fun int int) (fun int bool))) % 9.98/10.16 (fun int % 9.98/10.16 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))))) % 9.98/10.16 (combb (fun (fun int int) (fun int bool)) % 9.98/10.16 (fun (fun (list int) (fun int int)) (fun (list int) (fun int bool))) int) % 9.98/10.16 (combb (fun int int) (fun int bool) (list int))) % 9.98/10.16 (aa (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool))) % 9.98/10.16 (aa (fun (fun int bool) (fun (fun int int) (fun int bool))) % 9.98/10.16 (fun (fun int (fun int bool)) (fun int (fun (fun int int) (fun int bool)))) % 9.98/10.16 (combb (fun int bool) (fun (fun int int) (fun int bool)) int) % 9.98/10.16 (combb int bool int)) % 9.98/10.16 (fequal int)))) % 9.98/10.16 (aa (fun (list int) int) (fun (list int) (fun int int)) % 9.98/10.16 (aa (fun int (fun int int)) % 9.98/10.16 (fun (fun (list int) int) (fun (list int) (fun int int))) % 9.98/10.16 (combb int (fun int int) (list int)) (minus_minus int)) % 9.98/10.16 (aa (list int) (fun (list int) int) % 9.98/10.16 (aa (fun (list int) (fun (list int) int)) (fun (list int) (fun (list int) int)) % 9.98/10.16 (combc (list int) (list int) int) % 9.98/10.16 (aa (fun (list int) (list int)) (fun (list int) (fun (list int) int)) % 9.98/10.16 (aa (fun (list int) (fun (list int) int)) % 9.98/10.16 (fun (fun (list int) (list int)) (fun (list int) (fun (list int) int))) % 9.98/10.16 (combb (list int) (fun (list int) int) (list int)) (iprod int)) % 9.98/10.16 (tl int))) % 9.98/10.16 xs))))))) % 9.98/10.16 (aa (fun atom bool) (fun (list int) (fun int bool)) % 9.98/10.16 (aa (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.98/10.16 (fun (fun atom bool) (fun (list int) (fun int bool))) % 9.98/10.16 (combc (list int) (fun atom bool) (fun int bool)) % 9.98/10.16 (aa (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (fun (list int) (fun (fun atom bool) (fun int bool))) % 9.98/10.16 (aa (fun (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool))) % 9.98/10.16 (fun (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (fun (list int) (fun (fun atom bool) (fun int bool)))) % 9.98/10.16 (combb (fun int (fun (fun atom bool) bool)) (fun (fun atom bool) (fun int bool)) % 9.98/10.16 (list int)) % 9.98/10.16 (combc int (fun atom bool) bool)) % 9.98/10.16 (aa (fun (list int) (fun int atom)) (fun (list int) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (aa (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (fun (fun (list int) (fun int atom)) % 9.98/10.16 (fun (list int) (fun int (fun (fun atom bool) bool)))) % 9.98/10.16 (combb (fun int atom) (fun int (fun (fun atom bool) bool)) (list int)) % 9.98/10.16 (aa (fun atom (fun (fun atom bool) bool)) % 9.98/10.16 (fun (fun int atom) (fun int (fun (fun atom bool) bool))) % 9.98/10.16 (combb atom (fun (fun atom bool) bool) int) (member atom))) % 9.98/10.16 (aa (fun int (fun (list int) atom)) (fun (list int) (fun int atom)) % 9.98/10.16 (combc int (list int) atom) c_PresArith_Oatom_OLe)))) % 9.98/10.16 (aa (fun atom bool) (fun atom bool) % 9.98/10.16 (aa (fun atom (fun bool bool)) (fun (fun atom bool) (fun atom bool)) (combs atom bool bool) % 9.98/10.16 (aa (fun atom bool) (fun atom (fun bool bool)) % 9.98/10.16 (aa (fun bool (fun bool bool)) (fun (fun atom bool) (fun atom (fun bool bool))) % 9.98/10.16 (combb bool (fun bool bool) atom) fconj) % 9.98/10.16 (aa (fun atom bool) (fun atom bool) % 9.98/10.16 (aa (fun atom (fun (fun atom bool) bool)) (fun (fun atom bool) (fun atom bool)) % 9.98/10.16 (combc atom (fun atom bool) bool) (member atom)) % 9.98/10.16 (set atom as)))) % 9.98/10.16 (atom_case bool % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.98/10.16 (combk (fun (list int) bool) int) % 9.98/10.16 (list_case bool int fFalse % 9.98/10.16 (aa (fun int bool) (fun int (fun (list int) bool)) % 9.98/10.16 (aa (fun bool (fun (list int) bool)) % 9.98/10.16 (fun (fun int bool) (fun int (fun (list int) bool))) % 9.98/10.16 (combb bool (fun (list int) bool) int) (combk bool (list int))) % 9.98/10.16 (aa int (fun int bool) % 9.98/10.16 (aa (fun int (fun int bool)) (fun int (fun int bool)) (combc int int bool) % 9.98/10.16 (ord_less int)) % 9.98/10.16 (zero_zero int))))) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.98/10.16 (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) % 9.98/10.16 (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse))))))))))) % 9.98/10.16 (zlcms % 9.98/10.16 (map atom int divisor % 9.98/10.16 (filter atom % 9.98/10.16 (atom_case bool % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.98/10.16 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.16 (combk (fun int (fun (list int) bool)) int) % 9.98/10.16 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.16 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.98/10.17 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.17 (combk (fun int (fun (list int) bool)) int) % 9.98/10.17 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.17 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.98/10.17 as)))) % 9.98/10.17 (one_one int))) % 9.98/10.17 (zlcms % 9.98/10.17 (map atom int divisor % 9.98/10.17 (filter atom % 9.98/10.17 (atom_case bool % 9.98/10.17 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.17 (aa bool (fun (list int) bool) (combk bool (list int)) fFalse)) % 9.98/10.17 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.17 (combk (fun int (fun (list int) bool)) int) % 9.98/10.17 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.17 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue))) % 9.98/10.17 (aa (fun int (fun (list int) bool)) (fun int (fun int (fun (list int) bool))) % 9.98/10.17 (combk (fun int (fun (list int) bool)) int) % 9.98/10.17 (aa (fun (list int) bool) (fun int (fun (list int) bool)) (combk (fun (list int) bool) int) % 9.98/10.17 (aa bool (fun (list int) bool) (combk bool (list int)) fTrue)))) % 9.98/10.17 as))))) % 9.98/10.17 (aa atom int divisor a)) % 9.98/10.17 Clause #3512 (by eliminate resolved literals #[3511]): False % 9.98/10.17 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------