%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SCT171+5 : TPTP v9.2.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n012.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:59:13 PM UTC 2025 % Result : Theorem 199.47s 199.68s % Output : Proof 199.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SCT171+5 : TPTP v9.2.0. Released v5.3.0. % 0.10/0.13 % Command : duper %s % 0.14/0.34 % Computer : n012.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 21:16:38 EDT 2025 % 0.14/0.34 % CPUTime : % 199.47/199.68 SZS status Theorem for theBenchmark.p % 199.47/199.68 SZS output start Proof for theBenchmark.p % 199.47/199.68 Clause #29 (by assumption #[]): Eq (∀ (X_c X_a B_1_1 B_2_1 : Iota), Eq (ti X_c (hAPP X_a X_c B_1_1 B_2_1)) (hAPP X_a X_c B_1_1 B_2_1)) True % 199.47/199.68 Clause #30 (by assumption #[]): Eq (∀ (B_1_1 : Iota), Iff (hBOOL (ti bool B_1_1)) (hBOOL B_1_1)) True % 199.47/199.68 Clause #56 (by assumption #[]): Eq % 199.47/199.68 (hBOOL % 199.47/199.68 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.47/199.68 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.47/199.68 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.47/199.68 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.47/199.68 (hAPP arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.47/199.68 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.47/199.68 d)) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (fun % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi bool) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun bool % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (fun (fun arrow_1384031255e_indi bool) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.47/199.68 (combb bool % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 arrow_1384031255e_indi) % 199.47/199.68 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.47/199.68 (combc arrow_1384031255e_indi nat bool) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.47/199.68 (hAPP (fun nat (fun nat bool)) % 199.47/199.68 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.47/199.68 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.47/199.68 h)) % 199.47/199.68 n))) % 199.47/199.68 (hAPP arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (fun % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 arrow_1384031255e_indi) % 199.47/199.68 arrow_992993526_mktop) % 199.47/199.68 p)) % 199.47/199.68 e))) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (fun % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi bool) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun bool % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (fun (fun arrow_1384031255e_indi bool) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.47/199.68 (combb bool % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 arrow_1384031255e_indi) % 199.47/199.68 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.47/199.68 (combc arrow_1384031255e_indi nat bool) % 199.47/199.68 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.47/199.68 (hAPP (fun nat (fun nat bool)) % 199.47/199.68 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.47/199.68 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.47/199.68 h)) % 199.47/199.68 n))) % 199.47/199.68 (hAPP arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (hAPP arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (hAPP % 199.47/199.68 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.47/199.68 (fun % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.47/199.68 (fun arrow_1384031255e_indi % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.47/199.68 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1212486748le_alt % 199.47/199.68 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.47/199.68 arrow_1384031255e_indi) % 199.47/199.68 arrow_1726925404_above) % 199.47/199.68 p)) % 199.47/199.68 c)) % 199.47/199.68 e))) % 199.47/199.68 (hAPP arrow_1212486748le_alt % 199.47/199.68 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 arrow_1384031255e_indi) % 199.55/199.71 arrow_844286440_mkbot) % 199.55/199.71 p)) % 199.55/199.71 e)))))) % 199.55/199.71 True % 199.55/199.71 Clause #57 (by assumption #[]): Eq % 199.55/199.71 (Iff % 199.55/199.71 (hBOOL % 199.55/199.71 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.55/199.71 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.55/199.71 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.71 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.71 (hAPP arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.71 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.55/199.71 d)) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f p))) % 199.55/199.71 (hBOOL % 199.55/199.71 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.55/199.71 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.55/199.71 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.71 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.71 (hAPP arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.71 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.55/199.71 d)) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (fun % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi bool) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun bool % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (fun (fun arrow_1384031255e_indi bool) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.55/199.71 (combb bool % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 arrow_1384031255e_indi) % 199.55/199.71 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.55/199.71 (combc arrow_1384031255e_indi nat bool) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.55/199.71 (hAPP (fun nat (fun nat bool)) % 199.55/199.71 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.55/199.71 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.55/199.71 h)) % 199.55/199.71 n))) % 199.55/199.71 (hAPP arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 arrow_1384031255e_indi) % 199.55/199.71 arrow_992993526_mktop) % 199.55/199.71 p)) % 199.55/199.71 e))) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (fun % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (combs arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi bool) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun bool % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (fun (fun arrow_1384031255e_indi bool) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.55/199.71 (combb bool % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 arrow_1384031255e_indi) % 199.55/199.71 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.55/199.71 (combc arrow_1384031255e_indi nat bool) % 199.55/199.71 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.55/199.71 (hAPP (fun nat (fun nat bool)) % 199.55/199.71 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.55/199.71 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.55/199.71 h)) % 199.55/199.71 n))) % 199.55/199.71 (hAPP arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.71 (fun % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.55/199.71 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 arrow_1384031255e_indi) % 199.55/199.71 arrow_1726925404_above) % 199.55/199.71 p)) % 199.55/199.71 c)) % 199.55/199.71 e))) % 199.55/199.71 (hAPP arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (hAPP % 199.55/199.71 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.71 (fun arrow_1384031255e_indi % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.71 (hAPP % 199.55/199.71 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.71 (fun arrow_1212486748le_alt % 199.55/199.71 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.73 (fun % 199.55/199.73 (fun arrow_1384031255e_indi % 199.55/199.73 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.73 (fun arrow_1384031255e_indi % 199.55/199.73 (fun arrow_1212486748le_alt % 199.55/199.73 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.73 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.73 (fun arrow_1212486748le_alt % 199.55/199.73 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.73 arrow_1384031255e_indi) % 199.55/199.73 arrow_844286440_mkbot) % 199.55/199.73 p)) % 199.55/199.73 e))))))) % 199.55/199.73 True % 199.55/199.73 Clause #84 (by assumption #[]): Eq % 199.55/199.73 (∀ (X_a : Iota), % 199.55/199.73 order X_a → ∀ (X Y : Iota), hBOOL (hAPP X_a bool (hAPP X_a (fun X_a bool) (ord_less X_a) X) Y) → Ne X Y) % 199.55/199.73 True % 199.55/199.73 Clause #144 (by assumption #[]): Eq (order nat) True % 199.55/199.73 Clause #150 (by assumption #[]): Eq (∀ (T A : Iota), Eq (ti T (ti T A)) (ti T A)) True % 199.55/199.73 Clause #153 (by assumption #[]): Eq (∀ (P : Iota), Or (Eq (ti bool P) fTrue) (Eq (ti bool P) fFalse)) True % 199.55/199.73 Clause #159 (by assumption #[]): Eq (hBOOL fTrue) True % 199.55/199.73 Clause #162 (by assumption #[]): Eq % 199.55/199.73 (Not % 199.55/199.73 (hBOOL % 199.55/199.73 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.55/199.73 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.73 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.55/199.73 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.73 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.73 (hAPP arrow_1212486748le_alt % 199.55/199.73 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.73 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.55/199.73 d)) % 199.55/199.73 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.73 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f p)))) % 199.55/199.73 True % 199.55/199.73 Clause #227 (by clausification #[30]): ∀ (a : Iota), Eq (Iff (hBOOL (ti bool a)) (hBOOL a)) True % 199.55/199.73 Clause #229 (by clausification #[227]): ∀ (a : Iota), Or (Eq (hBOOL (ti bool a)) False) (Eq (hBOOL a) True) % 199.55/199.73 Clause #243 (by clausification #[84]): ∀ (a : Iota), Eq (order a → ∀ (X Y : Iota), hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) X) Y) → Ne X Y) True % 199.55/199.73 Clause #244 (by clausification #[243]): ∀ (a : Iota), % 199.55/199.73 Or (Eq (order a) False) % 199.55/199.73 (Eq (∀ (X Y : Iota), hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) X) Y) → Ne X Y) True) % 199.55/199.73 Clause #245 (by clausification #[244]): ∀ (a a_1 : Iota), % 199.55/199.73 Or (Eq (order a) False) % 199.55/199.73 (Eq (∀ (Y : Iota), hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) a_1) Y) → Ne a_1 Y) True) % 199.55/199.73 Clause #246 (by clausification #[245]): ∀ (a a_1 a_2 : Iota), % 199.55/199.73 Or (Eq (order a) False) (Eq (hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) a_1) a_2) → Ne a_1 a_2) True) % 199.55/199.73 Clause #247 (by clausification #[246]): ∀ (a a_1 a_2 : Iota), % 199.55/199.73 Or (Eq (order a) False) % 199.55/199.73 (Or (Eq (hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) a_1) a_2)) False) (Eq (Ne a_1 a_2) True)) % 199.55/199.73 Clause #248 (by clausification #[247]): ∀ (a a_1 a_2 : Iota), % 199.55/199.73 Or (Eq (order a) False) (Or (Eq (hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) a_1) a_2)) False) (Ne a_1 a_2)) % 199.55/199.73 Clause #249 (by destructive equality resolution #[248]): ∀ (a a_1 : Iota), Or (Eq (order a) False) (Eq (hBOOL (hAPP a bool (hAPP a (fun a bool) (ord_less a) a_1) a_1)) False) % 199.55/199.73 Clause #251 (by superposition #[249, 144]): ∀ (a : Iota), Or (Eq (hBOOL (hAPP nat bool (hAPP nat (fun nat bool) (ord_less nat) a) a)) False) (Eq False True) % 199.55/199.73 Clause #320 (by clausification #[150]): ∀ (a : Iota), Eq (∀ (A : Iota), Eq (ti a (ti a A)) (ti a A)) True % 199.55/199.73 Clause #321 (by clausification #[320]): ∀ (a a_1 : Iota), Eq (Eq (ti a (ti a a_1)) (ti a a_1)) True % 199.55/199.78 Clause #322 (by clausification #[321]): ∀ (a a_1 : Iota), Eq (ti a (ti a a_1)) (ti a a_1) % 199.55/199.78 Clause #390 (by clausification #[153]): ∀ (a : Iota), Eq (Or (Eq (ti bool a) fTrue) (Eq (ti bool a) fFalse)) True % 199.55/199.78 Clause #391 (by clausification #[390]): ∀ (a : Iota), Or (Eq (Eq (ti bool a) fTrue) True) (Eq (Eq (ti bool a) fFalse) True) % 199.55/199.78 Clause #392 (by clausification #[391]): ∀ (a : Iota), Or (Eq (Eq (ti bool a) fFalse) True) (Eq (ti bool a) fTrue) % 199.55/199.78 Clause #393 (by clausification #[392]): ∀ (a : Iota), Or (Eq (ti bool a) fTrue) (Eq (ti bool a) fFalse) % 199.55/199.78 Clause #398 (by superposition #[393, 322]): ∀ (a : Iota), Or (Eq (ti bool (ti bool a)) fTrue) (Eq fFalse (ti bool a)) % 199.55/199.78 Clause #427 (by superposition #[398, 229]): ∀ (a : Iota), Or (Eq fFalse (ti bool a)) (Or (Eq (hBOOL fTrue) False) (Eq (hBOOL (ti bool a)) True)) % 199.55/199.78 Clause #442 (by forward demodulation #[427, 159]): ∀ (a : Iota), Or (Eq fFalse (ti bool a)) (Or (Eq True False) (Eq (hBOOL (ti bool a)) True)) % 199.55/199.78 Clause #443 (by clausification #[442]): ∀ (a : Iota), Or (Eq fFalse (ti bool a)) (Eq (hBOOL (ti bool a)) True) % 199.55/199.78 Clause #475 (by clausification #[29]): ∀ (a : Iota), Eq (∀ (X_a B_1_1 B_2_1 : Iota), Eq (ti a (hAPP X_a a B_1_1 B_2_1)) (hAPP X_a a B_1_1 B_2_1)) True % 199.55/199.78 Clause #476 (by clausification #[475]): ∀ (a a_1 : Iota), Eq (∀ (B_1_1 B_2_1 : Iota), Eq (ti a (hAPP a_1 a B_1_1 B_2_1)) (hAPP a_1 a B_1_1 B_2_1)) True % 199.55/199.78 Clause #477 (by clausification #[476]): ∀ (a a_1 a_2 : Iota), Eq (∀ (B_2_1 : Iota), Eq (ti a (hAPP a_1 a a_2 B_2_1)) (hAPP a_1 a a_2 B_2_1)) True % 199.55/199.78 Clause #478 (by clausification #[477]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (ti a (hAPP a_1 a a_2 a_3)) (hAPP a_1 a a_2 a_3)) True % 199.55/199.78 Clause #479 (by clausification #[478]): ∀ (a a_1 a_2 a_3 : Iota), Eq (ti a (hAPP a_1 a a_2 a_3)) (hAPP a_1 a a_2 a_3) % 199.55/199.78 Clause #481 (by superposition #[479, 393]): ∀ (a a_1 a_2 : Iota), Or (Eq (hAPP a bool a_1 a_2) fTrue) (Eq (hAPP a bool a_1 a_2) fFalse) % 199.55/199.78 Clause #483 (by superposition #[479, 443]): ∀ (a a_1 a_2 : Iota), Or (Eq fFalse (hAPP a bool a_1 a_2)) (Eq (hBOOL (hAPP a bool a_1 a_2)) True) % 199.55/199.78 Clause #854 (by superposition #[56, 481]): Or % 199.55/199.78 (Eq % 199.55/199.78 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.55/199.78 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.55/199.78 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.78 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.55/199.78 (hAPP arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.55/199.78 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.55/199.78 d)) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (fun % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi bool) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun bool % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (fun (fun arrow_1384031255e_indi bool) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.55/199.78 (combb bool % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 arrow_1384031255e_indi) % 199.55/199.78 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.55/199.78 (combc arrow_1384031255e_indi nat bool) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.55/199.78 (hAPP (fun nat (fun nat bool)) % 199.55/199.78 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.55/199.78 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.55/199.78 h)) % 199.55/199.78 n))) % 199.55/199.78 (hAPP arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (fun % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 arrow_1384031255e_indi) % 199.55/199.78 arrow_992993526_mktop) % 199.55/199.78 p)) % 199.55/199.78 e))) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (fun % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi bool) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun bool % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (fun (fun arrow_1384031255e_indi bool) % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.55/199.78 (combb bool % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 arrow_1384031255e_indi) % 199.55/199.78 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.55/199.78 (combc arrow_1384031255e_indi nat bool) % 199.55/199.78 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.55/199.78 (hAPP (fun nat (fun nat bool)) % 199.55/199.78 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.55/199.78 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.55/199.78 h)) % 199.55/199.78 n))) % 199.55/199.78 (hAPP arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.55/199.78 (hAPP arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.55/199.78 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.55/199.78 (fun arrow_1212486748le_alt % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.55/199.78 (hAPP % 199.55/199.78 (fun arrow_1384031255e_indi % 199.55/199.78 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.81 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 arrow_1384031255e_indi) % 199.63/199.81 arrow_1726925404_above) % 199.63/199.81 p)) % 199.63/199.81 c)) % 199.63/199.81 e))) % 199.63/199.81 (hAPP arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 arrow_1384031255e_indi) % 199.63/199.81 arrow_844286440_mkbot) % 199.63/199.81 p)) % 199.63/199.81 e))))) % 199.63/199.81 fTrue) % 199.63/199.81 (Eq (hBOOL fFalse) True) % 199.63/199.81 Clause #886 (by clausification #[57]): Or % 199.63/199.81 (Eq % 199.63/199.81 (hBOOL % 199.63/199.81 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.63/199.81 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.63/199.81 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.81 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.81 (hAPP arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.81 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.63/199.81 d)) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f p))) % 199.63/199.81 True) % 199.63/199.81 (Eq % 199.63/199.81 (hBOOL % 199.63/199.81 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.63/199.81 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.63/199.81 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.81 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.81 (hAPP arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.81 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.63/199.81 d)) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi bool) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun bool % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun (fun arrow_1384031255e_indi bool) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.81 (combb bool % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 arrow_1384031255e_indi) % 199.63/199.81 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.63/199.81 (combc arrow_1384031255e_indi nat bool) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.63/199.81 (hAPP (fun nat (fun nat bool)) % 199.63/199.81 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.63/199.81 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.63/199.81 h)) % 199.63/199.81 n))) % 199.63/199.81 (hAPP arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 arrow_1384031255e_indi) % 199.63/199.81 arrow_992993526_mktop) % 199.63/199.81 p)) % 199.63/199.81 e))) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (combs arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi bool) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun bool % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun (fun arrow_1384031255e_indi bool) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.81 (combb bool % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 arrow_1384031255e_indi) % 199.63/199.81 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.63/199.81 (combc arrow_1384031255e_indi nat bool) % 199.63/199.81 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.63/199.81 (hAPP (fun nat (fun nat bool)) % 199.63/199.81 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.63/199.81 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.63/199.81 h)) % 199.63/199.81 n))) % 199.63/199.81 (hAPP arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (hAPP arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (hAPP % 199.63/199.81 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.81 (fun % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.81 (fun arrow_1384031255e_indi % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun arrow_1212486748le_alt % 199.63/199.81 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.84 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 arrow_1384031255e_indi) % 199.63/199.84 arrow_1726925404_above) % 199.63/199.84 p)) % 199.63/199.84 c)) % 199.63/199.84 e))) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 arrow_1384031255e_indi) % 199.63/199.84 arrow_844286440_mkbot) % 199.63/199.84 p)) % 199.63/199.84 e)))))) % 199.63/199.84 False) % 199.63/199.84 Clause #888 (by superposition #[886, 483]): Or % 199.63/199.84 (Eq % 199.63/199.84 (hBOOL % 199.63/199.84 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.63/199.84 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.63/199.84 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.84 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.84 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.63/199.84 d)) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f p))) % 199.63/199.84 True) % 199.63/199.84 (Or % 199.63/199.84 (Eq fFalse % 199.63/199.84 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.63/199.84 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.63/199.84 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.84 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.63/199.84 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.63/199.84 d)) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (fun % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi bool) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun bool % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (fun (fun arrow_1384031255e_indi bool) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.84 (combb bool % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 arrow_1384031255e_indi) % 199.63/199.84 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.63/199.84 (combc arrow_1384031255e_indi nat bool) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.63/199.84 (hAPP (fun nat (fun nat bool)) % 199.63/199.84 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.63/199.84 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.63/199.84 h)) % 199.63/199.84 n))) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 arrow_1384031255e_indi) % 199.63/199.84 arrow_992993526_mktop) % 199.63/199.84 p)) % 199.63/199.84 e))) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (fun % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (combs arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi bool) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun bool % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (fun (fun arrow_1384031255e_indi bool) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.84 (combb bool % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 arrow_1384031255e_indi) % 199.63/199.84 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.63/199.84 (combc arrow_1384031255e_indi nat bool) % 199.63/199.84 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.63/199.84 (hAPP (fun nat (fun nat bool)) % 199.63/199.84 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.63/199.84 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.63/199.84 h)) % 199.63/199.84 n))) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (hAPP % 199.63/199.84 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.63/199.84 (fun % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.63/199.84 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.63/199.84 arrow_1384031255e_indi) % 199.63/199.84 arrow_1726925404_above) % 199.63/199.84 p)) % 199.63/199.84 c)) % 199.63/199.84 e))) % 199.63/199.84 (hAPP arrow_1212486748le_alt % 199.63/199.84 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.63/199.84 (hAPP % 199.63/199.84 (fun arrow_1384031255e_indi % 199.63/199.84 (fun arrow_1212486748le_alt % 199.63/199.84 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 arrow_1384031255e_indi) % 199.73/199.88 arrow_844286440_mkbot) % 199.73/199.88 p)) % 199.73/199.88 e)))))) % 199.73/199.88 (Eq False True)) % 199.73/199.88 Clause #3744 (by clausification #[162]): Eq % 199.73/199.88 (hBOOL % 199.73/199.88 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.73/199.88 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.73/199.88 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.73/199.88 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.73/199.88 (hAPP arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.73/199.88 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.73/199.88 d)) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f p))) % 199.73/199.88 False % 199.73/199.88 Clause #3785 (by clausification #[251]): ∀ (a : Iota), Eq (hBOOL (hAPP nat bool (hAPP nat (fun nat bool) (ord_less nat) a) a)) False % 199.73/199.88 Clause #3786 (by superposition #[3785, 483]): ∀ (a : Iota), Or (Eq fFalse (hAPP nat bool (hAPP nat (fun nat bool) (ord_less nat) a) a)) (Eq False True) % 199.73/199.88 Clause #3895 (by clausification #[3786]): ∀ (a : Iota), Eq fFalse (hAPP nat bool (hAPP nat (fun nat bool) (ord_less nat) a) a) % 199.73/199.88 Clause #3896 (by backward demodulation #[3895, 3785]): Eq (hBOOL fFalse) False % 199.73/199.88 Clause #11982 (by forward demodulation #[854, 3896]): Or % 199.73/199.88 (Eq % 199.73/199.88 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.73/199.88 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.73/199.88 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.73/199.88 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.73/199.88 (hAPP arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.73/199.88 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.73/199.88 d)) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (fun % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi bool) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun bool % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (fun (fun arrow_1384031255e_indi bool) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.73/199.88 (combb bool % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 arrow_1384031255e_indi) % 199.73/199.88 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.73/199.88 (combc arrow_1384031255e_indi nat bool) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.73/199.88 (hAPP (fun nat (fun nat bool)) % 199.73/199.88 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.73/199.88 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.73/199.88 h)) % 199.73/199.88 n))) % 199.73/199.88 (hAPP arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 arrow_1384031255e_indi) % 199.73/199.88 arrow_992993526_mktop) % 199.73/199.88 p)) % 199.73/199.88 e))) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (fun % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi bool) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun bool % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (fun (fun arrow_1384031255e_indi bool) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.73/199.88 (combb bool % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 arrow_1384031255e_indi) % 199.73/199.88 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.73/199.88 (combc arrow_1384031255e_indi nat bool) % 199.73/199.88 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.73/199.88 (hAPP (fun nat (fun nat bool)) % 199.73/199.88 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.73/199.88 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.73/199.88 h)) % 199.73/199.88 n))) % 199.73/199.88 (hAPP arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.73/199.88 (fun % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.73/199.88 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 arrow_1384031255e_indi) % 199.73/199.88 arrow_1726925404_above) % 199.73/199.88 p)) % 199.73/199.88 c)) % 199.73/199.88 e))) % 199.73/199.88 (hAPP arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (hAPP % 199.73/199.88 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.73/199.88 (fun arrow_1384031255e_indi % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (hAPP % 199.73/199.88 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.73/199.88 (fun arrow_1212486748le_alt % 199.73/199.88 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.73/199.88 (fun % 199.73/199.88 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 arrow_1384031255e_indi) % 199.76/199.91 arrow_844286440_mkbot) % 199.76/199.91 p)) % 199.76/199.91 e))))) % 199.76/199.91 fTrue) % 199.76/199.91 (Eq False True) % 199.76/199.91 Clause #11983 (by clausification #[11982]): Eq % 199.76/199.91 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.76/199.91 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.76/199.91 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.76/199.91 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.76/199.91 (hAPP arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.76/199.91 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.76/199.91 d)) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi bool) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun bool % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (fun (fun arrow_1384031255e_indi bool) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.76/199.91 (combb bool % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 arrow_1384031255e_indi) % 199.76/199.91 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.76/199.91 (combc arrow_1384031255e_indi nat bool) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.76/199.91 (hAPP (fun nat (fun nat bool)) % 199.76/199.91 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.76/199.91 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.76/199.91 h)) % 199.76/199.91 n))) % 199.76/199.91 (hAPP arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (fun % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 arrow_1384031255e_indi) % 199.76/199.91 arrow_992993526_mktop) % 199.76/199.91 p)) % 199.76/199.91 e))) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (fun % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi bool) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun bool % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (fun (fun arrow_1384031255e_indi bool) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.76/199.91 (combb bool % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 arrow_1384031255e_indi) % 199.76/199.91 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.76/199.91 (combc arrow_1384031255e_indi nat bool) % 199.76/199.91 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.76/199.91 (hAPP (fun nat (fun nat bool)) % 199.76/199.91 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.76/199.91 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.76/199.91 h)) % 199.76/199.91 n))) % 199.76/199.91 (hAPP arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (hAPP % 199.76/199.91 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.76/199.91 (fun % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.76/199.91 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1212486748le_alt % 199.76/199.91 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.76/199.91 arrow_1384031255e_indi) % 199.76/199.91 arrow_1726925404_above) % 199.76/199.91 p)) % 199.76/199.91 c)) % 199.76/199.91 e))) % 199.76/199.91 (hAPP arrow_1212486748le_alt % 199.76/199.91 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.76/199.91 (hAPP % 199.76/199.91 (fun arrow_1384031255e_indi % 199.76/199.91 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 arrow_1384031255e_indi) % 199.78/199.95 arrow_844286440_mkbot) % 199.78/199.95 p)) % 199.78/199.95 e))))) % 199.78/199.95 fTrue % 199.78/199.95 Clause #12490 (by clausification #[888]): Or % 199.78/199.95 (Eq % 199.78/199.95 (hBOOL % 199.78/199.95 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.78/199.95 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.78/199.95 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.78/199.95 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.78/199.95 (hAPP arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.78/199.95 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.78/199.95 d)) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f p))) % 199.78/199.95 True) % 199.78/199.95 (Eq fFalse % 199.78/199.95 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.78/199.95 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.78/199.95 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.78/199.95 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.78/199.95 (hAPP arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.78/199.95 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.78/199.95 d)) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (fun % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi bool) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun bool % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (fun (fun arrow_1384031255e_indi bool) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.78/199.95 (combb bool % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 arrow_1384031255e_indi) % 199.78/199.95 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.78/199.95 (combc arrow_1384031255e_indi nat bool) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.78/199.95 (hAPP (fun nat (fun nat bool)) % 199.78/199.95 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.78/199.95 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.78/199.95 h)) % 199.78/199.95 n))) % 199.78/199.95 (hAPP arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 arrow_1384031255e_indi) % 199.78/199.95 arrow_992993526_mktop) % 199.78/199.95 p)) % 199.78/199.95 e))) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (fun % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi bool) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun bool % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (fun (fun arrow_1384031255e_indi bool) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.78/199.95 (combb bool % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 arrow_1384031255e_indi) % 199.78/199.95 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.78/199.95 (combc arrow_1384031255e_indi nat bool) % 199.78/199.95 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.78/199.95 (hAPP (fun nat (fun nat bool)) % 199.78/199.95 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.78/199.95 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.78/199.95 h)) % 199.78/199.95 n))) % 199.78/199.95 (hAPP arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (fun % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.78/199.95 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 arrow_1384031255e_indi) % 199.78/199.95 arrow_1726925404_above) % 199.78/199.95 p)) % 199.78/199.95 c)) % 199.78/199.95 e))) % 199.78/199.95 (hAPP arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (hAPP % 199.78/199.95 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (hAPP % 199.78/199.95 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.95 (fun % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 (fun arrow_1384031255e_indi % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.95 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.95 (fun arrow_1212486748le_alt % 199.78/199.95 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.95 arrow_1384031255e_indi) % 199.78/199.95 arrow_844286440_mkbot) % 199.78/199.95 p)) % 199.78/199.98 e)))))) % 199.78/199.98 Clause #12491 (by forward demodulation #[12490, 3744]): Or (Eq False True) % 199.78/199.98 (Eq fFalse % 199.78/199.98 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.78/199.98 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.78/199.98 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.78/199.98 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.78/199.98 (hAPP arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.78/199.98 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.78/199.98 d)) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (fun % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi bool) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun bool % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (fun (fun arrow_1384031255e_indi bool) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.78/199.98 (combb bool % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 arrow_1384031255e_indi) % 199.78/199.98 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.78/199.98 (combc arrow_1384031255e_indi nat bool) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.78/199.98 (hAPP (fun nat (fun nat bool)) % 199.78/199.98 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.78/199.98 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.78/199.98 h)) % 199.78/199.98 n))) % 199.78/199.98 (hAPP arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (fun % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 arrow_1384031255e_indi) % 199.78/199.98 arrow_992993526_mktop) % 199.78/199.98 p)) % 199.78/199.98 e))) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (fun % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi bool) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun bool % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (fun (fun arrow_1384031255e_indi bool) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.78/199.98 (combb bool % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 arrow_1384031255e_indi) % 199.78/199.98 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.78/199.98 (combc arrow_1384031255e_indi nat bool) % 199.78/199.98 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.78/199.98 (hAPP (fun nat (fun nat bool)) % 199.78/199.98 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.78/199.98 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.78/199.98 h)) % 199.78/199.98 n))) % 199.78/199.98 (hAPP arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (hAPP % 199.78/199.98 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.78/199.98 (fun % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.78/199.98 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1212486748le_alt % 199.78/199.98 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 arrow_1384031255e_indi) % 199.78/199.98 arrow_1726925404_above) % 199.78/199.98 p)) % 199.78/199.98 c)) % 199.78/199.98 e))) % 199.78/199.98 (hAPP arrow_1212486748le_alt % 199.78/199.98 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.78/199.98 (hAPP % 199.78/199.98 (fun arrow_1384031255e_indi % 199.78/199.98 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.78/199.98 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (fun % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 arrow_1384031255e_indi) % 199.85/200.01 arrow_844286440_mkbot) % 199.85/200.01 p)) % 199.85/200.01 e)))))) % 199.85/200.01 Clause #12492 (by clausification #[12491]): Eq fFalse % 199.85/200.01 (hAPP (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool % 199.85/200.01 (hAPP (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) bool) % 199.85/200.01 (member (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.85/200.01 (hAPP arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) % 199.85/200.01 (hAPP arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1212486748le_alt (product_prod arrow_1212486748le_alt arrow_1212486748le_alt)) % 199.85/200.01 (product_Pair arrow_1212486748le_alt arrow_1212486748le_alt) c) % 199.85/200.01 d)) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) f % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi bool) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun bool % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (fun (fun arrow_1384031255e_indi bool) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.85/200.01 (combb bool % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 arrow_1384031255e_indi) % 199.85/200.01 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.85/200.01 (combc arrow_1384031255e_indi nat bool) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.85/200.01 (hAPP (fun nat (fun nat bool)) % 199.85/200.01 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.85/200.01 (combb nat (fun nat bool) arrow_1384031255e_indi) (ord_less nat)) % 199.85/200.01 h)) % 199.85/200.01 n))) % 199.85/200.01 (hAPP arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (fun % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 arrow_1384031255e_indi) % 199.85/200.01 arrow_992993526_mktop) % 199.85/200.01 p)) % 199.85/200.01 e))) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (fun (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (fun % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (combs arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi bool) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun bool % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (fun (fun arrow_1384031255e_indi bool) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.85/200.01 (combb bool % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 arrow_1384031255e_indi) % 199.85/200.01 (if (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP nat (fun arrow_1384031255e_indi bool) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi (fun nat bool)) (fun nat (fun arrow_1384031255e_indi bool)) % 199.85/200.01 (combc arrow_1384031255e_indi nat bool) % 199.85/200.01 (hAPP (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool)) % 199.85/200.01 (hAPP (fun nat (fun nat bool)) % 199.85/200.01 (fun (fun arrow_1384031255e_indi nat) (fun arrow_1384031255e_indi (fun nat bool))) % 199.85/200.01 (combb nat (fun nat bool) arrow_1384031255e_indi) (fequal nat)) % 199.85/200.01 h)) % 199.85/200.01 n))) % 199.85/200.01 (hAPP arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (hAPP arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (hAPP % 199.85/200.01 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun arrow_1212486748le_alt % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.85/200.01 (fun % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.85/200.01 (fun arrow_1384031255e_indi % 199.85/200.01 (fun arrow_1212486748le_alt % 199.91/200.10 (fun arrow_1212486748le_alt % 199.91/200.10 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))))) % 199.91/200.10 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.91/200.10 (fun arrow_1212486748le_alt % 199.91/200.10 (fun arrow_1212486748le_alt % 199.91/200.10 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.91/200.10 arrow_1384031255e_indi) % 199.91/200.10 arrow_1726925404_above) % 199.91/200.10 p)) % 199.91/200.10 c)) % 199.91/200.10 e))) % 199.91/200.10 (hAPP arrow_1212486748le_alt % 199.91/200.10 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.91/200.10 (hAPP % 199.91/200.10 (fun arrow_1384031255e_indi % 199.91/200.10 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.91/200.10 (fun arrow_1212486748le_alt % 199.91/200.10 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.91/200.10 (combc arrow_1384031255e_indi arrow_1212486748le_alt % 199.91/200.10 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.91/200.10 (hAPP (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.91/200.10 (fun arrow_1384031255e_indi % 199.91/200.10 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.91/200.10 (hAPP % 199.91/200.10 (fun (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.91/200.10 (fun arrow_1212486748le_alt % 199.91/200.10 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool))) % 199.91/200.10 (fun % 199.91/200.10 (fun arrow_1384031255e_indi (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.91/200.10 (fun arrow_1384031255e_indi % 199.91/200.10 (fun arrow_1212486748le_alt % 199.91/200.10 (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)))) % 199.91/200.10 (combb (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool) % 199.91/200.10 (fun arrow_1212486748le_alt (fun (product_prod arrow_1212486748le_alt arrow_1212486748le_alt) bool)) % 199.91/200.10 arrow_1384031255e_indi) % 199.91/200.10 arrow_844286440_mkbot) % 199.91/200.10 p)) % 199.91/200.10 e))))) % 199.91/200.10 Clause #12493 (by superposition #[12492, 11983]): Eq fFalse fTrue % 199.91/200.10 Clause #12535 (by backward demodulation #[12493, 3896]): Eq (hBOOL fTrue) False % 199.91/200.10 Clause #12610 (by superposition #[12535, 159]): Eq False True % 199.91/200.10 Clause #12611 (by clausification #[12610]): False % 199.91/200.10 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------