%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL771-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:19:48 AM UTC 2026 % Result : Unsatisfiable 0.47s 0.65s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL771-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.34 % Computer : n019.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Fri Sep 4 20:15:23 UTC 2026 % 0.08/0.34 % CPUTime : % 0.30/0.50 start to proof:theBenchmark % 0.30/0.59 %------------------------------------------- % 0.30/0.59 % File :CSE---1.7 % 0.30/0.59 % Problem :theBenchmark % 0.30/0.59 % Transform :cnf % 0.30/0.59 % Format :tptp:raw % 0.30/0.59 % Command :java -jar mcs_scs.jar %d %s % 0.30/0.59 % 0.30/0.59 % Result :Theorem 0.046789s % 0.30/0.59 % Output :CNFRefutation 0.046789s % 0.30/0.59 %------------------------------------------- % 0.30/0.60 %------------------------------------------------------------------------------ % 0.30/0.60 % File : LCL771-1 : TPTP v9.3.1. Released v4.1.0. % 0.30/0.60 % Domain : Logic Calculi % 0.30/0.60 % Problem : Strong normalization of typed lambda calculus 078_5 % 0.30/0.60 % Version : Especial. % 0.30/0.60 % English : % 0.30/0.60 % 0.30/0.60 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.30/0.60 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.30/0.60 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.30/0.60 % Source : [Nip10] % 0.30/0.60 % Names : StrongNorm-078_5 [Nip10] % 0.30/0.60 % 0.30/0.60 % Status : Unsatisfiable % 0.30/0.60 % Rating : 0.17 v9.3.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.00 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.06 v5.1.0, 0.12 v5.0.0, 0.14 v4.1.0 % 0.30/0.60 % Syntax : Number of clauses : 428 ( 184 unt; 72 nHn; 190 RR) % 0.30/0.60 % Number of literals : 780 ( 369 equ; 308 neg) % 0.30/0.60 % Maximal clause size : 4 ( 1 avg) % 0.30/0.60 % Maximal term depth : 6 ( 1 avg) % 0.30/0.60 % Number of predicates : 17 ( 16 usr; 0 prp; 1-4 aty) % 0.30/0.60 % Number of functors : 80 ( 80 usr; 10 con; 0-5 aty) % 0.30/0.60 % Number of variables : 1327 ( 257 sgn) % 0.30/0.60 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.30/0.60 % 0.30/0.60 % Comments : % 0.30/0.60 %------------------------------------------------------------------------------ % 0.30/0.60 cnf(cls_length__remdups__eq_0,axiom, % 0.30/0.60 ( c_Nat_Osize__class_Osize(c_List_Oremdups(V_xs,T_a),tc_List_Olist(T_a)) != c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) % 0.30/0.60 | c_List_Oremdups(V_xs,T_a) = V_xs ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Zero__neq__Suc_0,axiom, % 0.30/0.60 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_nat_Osimps_I2_J_0,axiom, % 0.30/0.60 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_rtranclp__trans_0,axiom, % 0.30/0.60 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_z)) % 0.30/0.60 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_z)) % 0.30/0.60 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Nitpick_Ortranclp__def_1,axiom, % 0.30/0.60 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_x)) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_rtranclp_Ortrancl__refl_0,axiom, % 0.30/0.60 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_a)) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_replicate__eq__replicate_0,axiom, % 0.30/0.60 ( c_List_Oreplicate(V_m,V_x,T_a) != c_List_Oreplicate(V_n,V_y,T_a) % 0.30/0.60 | V_m = V_n ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Cons__step1__Cons_4,axiom, % 0.30/0.60 ( ~ hBOOL(hAPP(hAPP(V_r,V_y),V_xa)) % 0.30/0.60 | c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_x,T_a),c_List_Olist_OCons(V_xa,V_x,T_a),T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Cons__step1__Cons_2,axiom, % 0.30/0.60 ( V_x = V_y % 0.30/0.60 | V_xs = V_ys % 0.30/0.60 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_less__Suc0_0,axiom, % 0.30/0.60 ( V_n = c_HOL_Ozero__class_Ozero(tc_nat) % 0.30/0.60 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Suc__length__conv_2,axiom, % 0.30/0.60 c_Suc(c_Nat_Osize__class_Osize(V_xa,tc_List_Olist(T_a))) = c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_xa,T_a),tc_List_Olist(T_a)) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_append__step1I_1,axiom, % 0.30/0.60 ( c_ListOrder_Ostep1(V_r,c_List_Oappend(V_x,V_vs,T_a),c_List_Oappend(V_x,V_us,T_a),T_a) % 0.30/0.60 | ~ c_ListOrder_Ostep1(V_r,V_vs,V_us,T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_append__step1I_0,axiom, % 0.30/0.60 ( ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.30/0.60 | c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,V_x,T_a),c_List_Oappend(V_xs,V_x,T_a),T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_length__Suc__conv_2,axiom, % 0.30/0.60 c_Nat_Osize__class_Osize(c_List_Olist_OCons(V_x,V_xa,T_a),tc_List_Olist(T_a)) = c_Suc(c_Nat_Osize__class_Osize(V_xa,tc_List_Olist(T_a))) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_order__less__trans_0,axiom, % 0.30/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.30/0.60 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.30/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.30/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_xt1_I10_J_0,axiom, % 0.30/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.30/0.60 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.30/0.60 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.30/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_gr__implies__not0_0,axiom, % 0.30/0.60 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_not__less0_0,axiom, % 0.30/0.60 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_replicate__Suc_0,axiom, % 0.30/0.60 c_List_Oreplicate(c_Suc(V_n),V_x,T_a) = c_List_Olist_OCons(V_x,c_List_Oreplicate(V_n,V_x,T_a),T_a) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_zero__less__Suc_0,axiom, % 0.30/0.60 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_n),tc_nat) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_gr0__conv__Suc_1,axiom, % 0.30/0.60 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_x),tc_nat) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Suc__lessI_0,axiom, % 0.30/0.60 ( c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) % 0.30/0.60 | c_Suc(V_m) = V_n % 0.30/0.60 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_length__greater__0__conv_1,axiom, % 0.30/0.60 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),tc_nat) % 0.30/0.60 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_Cons__step1__Cons_0,axiom, % 0.30/0.60 ( V_x = V_y % 0.30/0.60 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.30/0.60 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_rotate__Suc_0,axiom, % 0.30/0.60 c_List_Orotate(c_Suc(V_n),V_xs,T_a) = c_List_Orotate1(c_List_Orotate(V_n,V_xs,T_a),T_a) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_last__replicate_0,axiom, % 0.30/0.60 ( c_List_Olast(c_List_Oreplicate(V_n,V_x,T_a),T_a) = V_x % 0.30/0.60 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.30/0.60 % 0.30/0.60 cnf(cls_replicate__eq__replicate_2,axiom, % 0.47/0.60 c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) = c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_y,T_a) ). % 0.47/0.60 % 0.47/0.60 cnf(cls_replicate__empty_1,axiom, % 0.47/0.60 c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.60 % 0.47/0.60 cnf(cls_length__list__update_0,axiom, % 0.47/0.60 c_Nat_Osize__class_Osize(c_List_Olist__update(V_xs,V_i,V_x,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ). % 0.47/0.60 % 0.47/0.60 cnf(cls_not__less__less__Suc__eq_1,axiom, % 0.47/0.60 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.47/0.60 | c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ) ). % 0.47/0.60 % 0.47/0.60 cnf(cls_not__less__eq_1,axiom, % 0.47/0.60 ( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.47/0.60 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) ) ). % 0.47/0.60 % 0.47/0.60 cnf(cls_not__less__eq_0,axiom, % 0.47/0.61 ( c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_replicate__eq__replicate_1,axiom, % 0.47/0.61 ( c_List_Oreplicate(V_m,V_x,T_a) != c_List_Oreplicate(V_n,V_y,T_a) % 0.47/0.61 | V_x = V_y % 0.47/0.61 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_rtranclp__idemp_0,axiom, % 0.47/0.61 c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(V_r,T_a),T_a) = c_Transitive__Closure_Ortranclp(V_r,T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_length__greater__0__conv_0,axiom, % 0.47/0.61 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__Suc__eq__0__disj_3,axiom, % 0.47/0.61 ( c_HOL_Oord__class_Oless(c_Suc(V_x),c_Suc(V_n),tc_nat) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_n,tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_Suc__less__eq_0,axiom, % 0.47/0.61 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_Suc__mono_0,axiom, % 0.47/0.61 ( c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_butlast_Osimps_I1_J_0,axiom, % 0.47/0.61 c_List_Obutlast(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_not__step1__Nil_0,axiom, % 0.47/0.61 ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_not__Nil__step1_0,axiom, % 0.47/0.61 ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_rotate1__is__Nil__conv_0,axiom, % 0.47/0.61 ( c_List_Orotate1(V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.61 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_rotate__simps_0,axiom, % 0.47/0.61 c_List_Orotate1(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_length__remdups__eq_1,axiom, % 0.47/0.61 ( c_List_Oremdups(V_xs,T_a) != V_xs % 0.47/0.61 | c_Nat_Osize__class_Osize(c_List_Oremdups(V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_length__map_0,axiom, % 0.47/0.61 c_Nat_Osize__class_Osize(c_List_Omap(V_f,V_xs,T_b,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_b)) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_map__replicate_0,axiom, % 0.47/0.61 c_List_Omap(V_f,c_List_Oreplicate(V_n,V_x,T_b),T_b,T_a) = c_List_Oreplicate(V_n,hAPP(V_f,V_x),T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_rev__replicate_0,axiom, % 0.47/0.61 c_List_Orev(c_List_Oreplicate(V_n,V_x,T_a),T_a) = c_List_Oreplicate(V_n,V_x,T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_Suc__inject_0,axiom, % 0.47/0.61 ( c_Suc(V_x) != c_Suc(V_y) % 0.47/0.61 | V_x = V_y ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_nat_Oinject_0,axiom, % 0.47/0.61 ( c_Suc(V_nat) != c_Suc(V_nat_H) % 0.47/0.61 | V_nat = V_nat_H ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_r__into__rtranclp_0,axiom, % 0.47/0.61 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) % 0.47/0.61 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__Suc0_1,axiom, % 0.47/0.61 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_filter__replicate_0,axiom, % 0.47/0.61 ( c_List_Ofilter(V_P,c_List_Oreplicate(V_n,V_x,T_a),T_a) = c_List_Oreplicate(V_n,V_x,T_a) % 0.47/0.61 | ~ hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_map__eq__imp__length__eq_0,axiom, % 0.47/0.61 ( c_List_Omap(V_f,V_xs,T_b,T_a) != c_List_Omap(V_f,V_ys,T_b,T_a) % 0.47/0.61 | c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_b)) = c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_b)) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_length__0__conv_1,axiom, % 0.47/0.61 c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__SucE_0,axiom, % 0.47/0.61 ( V_m = V_n % 0.47/0.61 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__antisym_0,axiom, % 0.47/0.61 ( V_m = V_n % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_not__less__less__Suc__eq_0,axiom, % 0.47/0.61 ( V_n = V_m % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_list__update__append_0,axiom, % 0.47/0.61 ( c_List_Olist__update(c_List_Oappend(V_xs,V_ys,T_a),V_n,V_x,T_a) = c_List_Oappend(c_List_Olist__update(V_xs,V_n,V_x,T_a),V_ys,T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_n,c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_list__update__append1_0,axiom, % 0.47/0.61 ( c_List_Olist__update(c_List_Oappend(V_xs,V_ys,T_a),V_i,V_x,T_a) = c_List_Oappend(c_List_Olist__update(V_xs,V_i,V_x,T_a),V_ys,T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_i,c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_length__rotate_0,axiom, % 0.47/0.61 c_Nat_Osize__class_Osize(c_List_Orotate(V_n,V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_empty__replicate_1,axiom, % 0.47/0.61 c_List_Olist_ONil(T_a) = c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_length__rotate1_0,axiom, % 0.47/0.61 c_Nat_Osize__class_Osize(c_List_Orotate1(V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_nat__less__le_1,axiom, % 0.47/0.61 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__not__refl_0,axiom, % 0.47/0.61 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_order__less__le_1,axiom, % 0.47/0.61 ( ~ class_Orderings_Oorder(T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_linorder__neq__iff_1,axiom, % 0.47/0.61 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_order__less__irrefl_0,axiom, % 0.47/0.61 ( ~ class_Orderings_Opreorder(T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_Cons__step1__Cons_3,axiom, % 0.47/0.61 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.47/0.61 | V_xs = V_ys % 0.47/0.61 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.47/0.61 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.47/0.61 | V_x = V_y ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.47/0.61 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.61 | V_x = V_y % 0.47/0.61 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_nat__neq__iff_0,axiom, % 0.47/0.61 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.47/0.61 | V_m = V_n ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_nat__less__cases_0,axiom, % 0.47/0.61 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.47/0.61 | V_m = V_n % 0.47/0.61 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_linorder__neqE__nat_0,axiom, % 0.47/0.61 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.47/0.61 | V_x = V_y ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_linorder__neqE_0,axiom, % 0.47/0.61 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.47/0.61 | V_x = V_y ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_append__replicate__commute_0,axiom, % 0.47/0.61 c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),c_List_Oreplicate(V_k,V_x,T_a),T_a) = c_List_Oappend(c_List_Oreplicate(V_k,V_x,T_a),c_List_Oreplicate(V_n,V_x,T_a),T_a) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_linorder__less__linear_0,axiom, % 0.47/0.61 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.47/0.61 | V_x = V_y % 0.47/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.47/0.61 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.61 | V_x = V_y % 0.47/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__infI2_0,axiom, % 0.47/0.61 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_b,V_x,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_less__infI1_0,axiom, % 0.47/0.61 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.61 | c_HOL_Oord__class_Oless(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.47/0.61 | ~ c_HOL_Oord__class_Oless(V_a,V_x,T_a) ) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_nat_Osimps_I3_J_0,axiom, % 0.47/0.61 c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_Suc__neq__Zero_0,axiom, % 0.47/0.61 c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.47/0.61 % 0.47/0.61 cnf(cls_lessI_0,axiom, % 0.47/0.62 c_HOL_Oord__class_Oless(V_n,c_Suc(V_n),tc_nat) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_less__Suc__eq_2,axiom, % 0.47/0.62 c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_less__trans__Suc_0,axiom, % 0.47/0.62 ( c_HOL_Oord__class_Oless(c_Suc(V_i),V_k,tc_nat) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_replicate__empty_0,axiom, % 0.47/0.62 ( c_List_Oreplicate(V_n,V_x,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_gr0I_0,axiom, % 0.47/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.47/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_liftn__0_0,axiom, % 0.47/0.62 c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t ). % 0.47/0.62 % 0.47/0.62 cnf(cls_neq0__conv_1,axiom, % 0.47/0.62 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_length__replicate_0,axiom, % 0.47/0.62 c_Nat_Osize__class_Osize(c_List_Oreplicate(V_n,V_x,T_a),tc_List_Olist(T_a)) = V_n ). % 0.47/0.62 % 0.47/0.62 cnf(cls_empty__replicate_0,axiom, % 0.47/0.62 ( c_List_Olist_ONil(T_a) != c_List_Oreplicate(V_n,V_x,T_a) % 0.47/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_length__0__conv_0,axiom, % 0.47/0.62 ( c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.47/0.62 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_Suc__n__not__n_0,axiom, % 0.47/0.62 c_Suc(V_n) != V_n ). % 0.47/0.62 % 0.47/0.62 cnf(cls_n__not__Suc__n_0,axiom, % 0.47/0.62 V_n != c_Suc(V_n) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_Cons__step1__Cons_1,axiom, % 0.47/0.62 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.47/0.62 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.47/0.62 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_Cons__step1__Cons_5,axiom, % 0.47/0.62 ( c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_x,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) % 0.47/0.62 | ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_Suc__lessD_0,axiom, % 0.47/0.62 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_less__SucI_0,axiom, % 0.47/0.62 ( c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_length__rev_0,axiom, % 0.47/0.62 c_Nat_Osize__class_Osize(c_List_Orev(V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_rotate1__rotate__swap_0,axiom, % 0.47/0.62 c_List_Orotate1(c_List_Orotate(V_n,V_xs,T_a),T_a) = c_List_Orotate(V_n,c_List_Orotate1(V_xs,T_a),T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_xt1_I9_J_0,axiom, % 0.47/0.62 ( ~ class_Orderings_Oorder(T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_converse__rtranclp__into__rtranclp_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_c)) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_c)) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_b)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.47/0.62 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_order__less__asym_0,axiom, % 0.47/0.62 ( ~ class_Orderings_Opreorder(T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_order__less__asym_H_0,axiom, % 0.47/0.62 ( ~ class_Orderings_Opreorder(T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_append__butlast__last__id_0,axiom, % 0.47/0.62 ( c_List_Oappend(c_List_Obutlast(V_xs,T_a),c_List_Olist_OCons(c_List_Olast(V_xs,T_a),c_List_Olist_ONil(T_a),T_a),T_a) = V_xs % 0.47/0.62 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_App__eq__foldl__conv_5,axiom, % 0.47/0.62 ( V_r != c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s),V_xa,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.62 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s),c_List_Oappend(V_xa,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_app__last_0,axiom, % 0.47/0.62 hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_u) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_ts,c_List_Olist_OCons(V_u,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_App__eq__foldl__conv_3,axiom, % 0.47/0.62 ( c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) = c_List_Olist_ONil(tc_Lambda_OdB) % 0.47/0.62 | hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_x,tc_Lambda_OdB,tc_Lambda_OdB)),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_substn_Osimps_I1_J_1,axiom, % 0.47/0.62 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.47/0.62 | c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_x),V_s,V_x) = c_Lambda_Oliftn(V_x,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_last_Osimps_1,axiom, % 0.47/0.62 ( c_List_Olast(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olast(V_xs,T_a) % 0.47/0.62 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_butlast_Osimps_I2_J_0,axiom, % 0.47/0.62 c_List_Obutlast(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_last_Osimps_0,axiom, % 0.47/0.62 c_List_Olast(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = V_x ). % 0.47/0.62 % 0.47/0.62 cnf(cls_butlast_Osimps_I2_J_1,axiom, % 0.47/0.62 ( c_List_Obutlast(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Obutlast(V_xs,T_a),T_a) % 0.47/0.62 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_append__eq__Cons__conv_3,axiom, % 0.47/0.62 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.47/0.62 | c_List_Oappend(c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) = V_xs % 0.47/0.62 | V_zs = c_List_Olist_OCons(V_x,V_xs,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_Cons__eq__append__conv_2,axiom, % 0.47/0.62 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.47/0.62 | c_List_Olist_OCons(V_x,c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) = V_ys % 0.47/0.62 | c_List_Olist_OCons(V_x,V_xs,T_a) = V_zs ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_append__eq__Cons__conv_2,axiom, % 0.47/0.62 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.47/0.62 | V_ys = c_List_Olist_OCons(V_x,c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) % 0.47/0.62 | V_zs = c_List_Olist_OCons(V_x,V_xs,T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_Cons__eq__append__conv_3,axiom, % 0.47/0.62 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.47/0.62 | V_xs = c_List_Oappend(c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) % 0.47/0.62 | c_List_Olist_OCons(V_x,V_xs,T_a) = V_zs ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_replicate__app__Cons__same_0,axiom, % 0.47/0.62 c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),V_xs,T_a),T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_butlast__append_0,axiom, % 0.47/0.62 c_List_Obutlast(c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Obutlast(V_xs,T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_last__append_1,axiom, % 0.47/0.62 ( c_List_Olast(c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Olast(V_ys,T_a) % 0.47/0.62 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_last__append_0,axiom, % 0.47/0.62 c_List_Olast(c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olast(V_xs,T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_butlast__append_1,axiom, % 0.47/0.62 ( c_List_Obutlast(c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Oappend(V_xs,c_List_Obutlast(V_ys,T_a),T_a) % 0.47/0.62 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_rtrancl__beta__App_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),hAPP(hAPP(c_Lambda_OdB_OApp,V_s_H),V_t_H))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_rtrancl__beta__AppL_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),hAPP(hAPP(c_Lambda_OdB_OApp,V_s_H),V_t))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_rtrancl__beta__AppR_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t_H))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_rtrancl__beta__Abs_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_s_H))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_filter__replicate_1,axiom, % 0.47/0.62 ( c_List_Ofilter(V_P,c_List_Oreplicate(V_n,V_x,T_a),T_a) = c_List_Olist_ONil(T_a) % 0.47/0.62 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subst__preserves__beta2_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_t,V_r,V_i)),c_Lambda_Osubst(V_t,V_s,V_i))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subst__preserves__beta_H_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_r,V_t,V_i)),c_Lambda_Osubst(V_s,V_t,V_i))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subst__preserves__beta2_H_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_t,V_r,V_i)),c_Lambda_Osubst(V_t,V_s,V_i))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_head__Var__reduction_0,axiom, % 0.47/0.62 ( c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(V_n,V_rs,V_v),tc_Lambda_OdB) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_rs,tc_Lambda_OdB,tc_Lambda_OdB)),V_v)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_list__update__code_I2_J_0,axiom, % 0.47/0.62 c_List_Olist__update(c_List_Olist_OCons(V_x,V_xs,T_a),c_HOL_Ozero__class_Ozero(tc_nat),V_y,T_a) = c_List_Olist_OCons(V_y,V_xs,T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_list__update__code_I3_J_0,axiom, % 0.47/0.62 c_List_Olist__update(c_List_Olist_OCons(V_x,V_xs,T_a),c_Suc(V_i),V_y,T_a) = c_List_Olist_OCons(V_x,c_List_Olist__update(V_xs,V_i,V_y,T_a),T_a) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subst__Var_1,axiom, % 0.47/0.62 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.47/0.62 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subst__Var_2,axiom, % 0.47/0.62 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.47/0.62 | V_i = V_k % 0.47/0.62 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subst__lt_0,axiom, % 0.47/0.62 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.47/0.62 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_subject__reduction_H_0,axiom, % 0.47/0.62 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.47/0.62 | ~ c_Type_Otyping(V_e,V_t,V_T) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_lift__preserves__beta_H_0,axiom, % 0.47/0.62 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.47/0.62 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_fun__upds__append__drop_0,axiom, % 0.47/0.62 ( c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) != c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_b)) % 0.47/0.62 | c_Map_Omap__upds(V_m,c_List_Oappend(V_xs,V_zs,T_a),V_ys,T_a,T_b) = c_Map_Omap__upds(V_m,V_xs,V_ys,T_a,T_b) ) ). % 0.47/0.62 % 0.47/0.62 cnf(cls_fun__upds__append2__drop_0,axiom, % 0.47/0.62 ( c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) != c_Nat_Osize__class_Osize(V_ys,tc_List_Olist(T_b)) % 0.47/0.63 | c_Map_Omap__upds(V_m,V_xs,c_List_Oappend(V_ys,V_zs,T_b),T_a,T_b) = c_Map_Omap__upds(V_m,V_xs,V_ys,T_a,T_b) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.47/0.63 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.47/0.63 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_liftn_Osimps_I1_J_0,axiom, % 0.47/0.63 ( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.47/0.63 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_inf1E_0,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_A,V_x)) % 0.47/0.63 | ~ hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_sorted_Osimps_I2_J_0,axiom, % 0.47/0.63 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.63 | c_List_Olinorder__class_Osorted(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_abs_0,axiom, % 0.47/0.63 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.47/0.63 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_rev__append_0,axiom, % 0.47/0.63 c_List_Orev(c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Oappend(c_List_Orev(V_ys,T_a),c_List_Orev(V_xs,T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_foldl__append_0,axiom, % 0.47/0.63 c_List_Ofoldl(V_f,V_a,c_List_Oappend(V_xs,V_ys,T_b),T_a,T_b) = c_List_Ofoldl(V_f,c_List_Ofoldl(V_f,V_a,V_xs,T_a,T_b),V_ys,T_a,T_b) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_filter__append_0,axiom, % 0.47/0.63 c_List_Ofilter(V_P,c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Oappend(c_List_Ofilter(V_P,V_xs,T_a),c_List_Ofilter(V_P,V_ys,T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__is__Nil__conv_2,axiom, % 0.47/0.63 c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_map__is__Nil__conv_0,axiom, % 0.47/0.63 ( c_List_Omap(V_f,V_xs,T_b,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_b) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_empty__null_1,axiom, % 0.47/0.63 ( V_xs = c_List_Olist_ONil(T_a) % 0.47/0.63 | ~ c_List_Onull(V_xs,T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Nil__is__rev__conv_1,axiom, % 0.47/0.63 c_List_Olist_ONil(T_a) = c_List_Orev(c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_remdups__eq__nil__right__iff_1,axiom, % 0.47/0.63 c_List_Olist_ONil(T_a) = c_List_Oremdups(c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_self__append__conv2_0,axiom, % 0.47/0.63 ( V_ys != c_List_Oappend(V_xs,V_ys,T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__self__conv2_0,axiom, % 0.47/0.63 ( c_List_Oappend(V_xs,V_ys,T_a) != V_ys % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_self__append__conv_0,axiom, % 0.47/0.63 ( V_xs != c_List_Oappend(V_xs,V_ys,T_a) % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__self__conv_0,axiom, % 0.47/0.63 ( c_List_Oappend(V_xs,V_ys,T_a) != V_xs % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_remdups__eq__nil__iff_0,axiom, % 0.47/0.63 ( c_List_Oremdups(V_x,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.63 | V_x = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_rotate__is__Nil__conv_0,axiom, % 0.47/0.63 ( c_List_Orotate(V_n,V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Nil__is__rev__conv_0,axiom, % 0.47/0.63 ( c_List_Olist_ONil(T_a) != c_List_Orev(V_xs,T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_list_Osimps_I2_J_0,axiom, % 0.47/0.63 c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__is__Nil__conv_1,axiom, % 0.47/0.63 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__is__Nil__conv_0,axiom, % 0.47/0.63 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Nil__is__append__conv_1,axiom, % 0.47/0.63 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Nil__is__append__conv_0,axiom, % 0.47/0.63 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_foldl__Nil_0,axiom, % 0.47/0.63 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.47/0.63 % 0.47/0.63 cnf(cls_remdups__eq__nil__iff_1,axiom, % 0.47/0.63 c_List_Oremdups(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Nil__is__map__conv_0,axiom, % 0.47/0.63 ( c_List_Olist_ONil(T_a) != c_List_Omap(V_f,V_xs,T_b,T_a) % 0.47/0.63 | V_xs = c_List_Olist_ONil(T_b) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_self__append__conv2_1,axiom, % 0.47/0.63 V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__Nil_0,axiom, % 0.47/0.63 c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) = V_ys ). % 0.47/0.63 % 0.47/0.63 cnf(cls_self__append__conv_1,axiom, % 0.47/0.63 V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_eq__Nil__appendI_0,axiom, % 0.47/0.63 V_x = c_List_Oappend(c_List_Olist_ONil(T_a),V_x,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__Nil2_0,axiom, % 0.47/0.63 c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) = V_xs ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Beta_0,axiom, % 0.47/0.63 ( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r)),V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.47/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.47/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_head__Var__reduction_1,axiom, % 0.47/0.63 ( V_v = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(V_n,V_rs,V_v),tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.63 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_rs,tc_Lambda_OdB,tc_Lambda_OdB)),V_v)) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_beta_0,axiom, % 0.47/0.63 hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t)),c_Lambda_Osubst(V_s,V_t,c_HOL_Ozero__class_Ozero(tc_nat)))) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_concat_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xconcat__Xinduct__1(V_P),v_sko__List__Xconcat__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_take_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xtake__Xinduct__1(V_P),v_sko__List__Xtake__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_map_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xmap__Xinduct__1(V_P),v_sko__List__Xmap__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_list_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xlist__Xinduct__1(V_P),v_sko__List__Xlist__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_dropWhile_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__XdropWhile__Xinduct__1(V_P),v_sko__List__XdropWhile__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_zip_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xzip__Xinduct__1(V_P),v_sko__List__Xzip__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_listset_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xlistset__Xinduct__1(V_P),v_sko__List__Xlistset__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_remove1_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xremove1__Xinduct__1(V_P),v_sko__List__Xremove1__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_distinct_Oinduct_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xdistinct__Xinduct__1(V_P),v_sko__List__Xdistinct__Xinduct__2(V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_substn__subst__n_0,axiom, % 0.47/0.63 c_Lambda_Osubstn(V_t,V_s,V_n) = c_Lambda_Osubst(V_t,c_Lambda_Oliftn(V_n,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_n) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_list__update__length_0,axiom, % 0.47/0.63 c_List_Olist__update(c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,V_ys,T_a),T_a),c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),V_y,T_a) = c_List_Oappend(V_xs,c_List_Olist_OCons(V_y,V_ys,T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_apps__preserves__beta2_0,axiom, % 0.47/0.63 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,V_r,V_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.47/0.63 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_apps__preserves__betas_0,axiom, % 0.47/0.63 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,V_r,V_rs,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,V_r,V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.47/0.63 | ~ c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,V_ss,tc_Lambda_OdB) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Cons__eq__filter__iff_5,axiom, % 0.47/0.63 ( ~ hBOOL(hAPP(V_P,V_x)) % 0.47/0.63 | hBOOL(hAPP(V_P,c_List_Osko__List__XCons__eq__filter__iff__1__3(V_P,V_xa,T_a))) % 0.47/0.63 | c_List_Olist_OCons(V_x,c_List_Ofilter(V_P,V_xb,T_a),T_a) = c_List_Ofilter(V_P,c_List_Oappend(V_xa,c_List_Olist_OCons(V_x,V_xb,T_a),T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_filter__eq__Cons__iff_5,axiom, % 0.47/0.63 ( ~ hBOOL(hAPP(V_P,V_x)) % 0.47/0.63 | hBOOL(hAPP(V_P,c_List_Osko__List__Xfilter__eq__Cons__iff__1__3(V_P,V_xa,T_a))) % 0.47/0.63 | c_List_Ofilter(V_P,c_List_Oappend(V_xa,c_List_Olist_OCons(V_x,V_xb,T_a),T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Ofilter(V_P,V_xb,T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Cons__eq__append__conv_1,axiom, % 0.47/0.63 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.47/0.63 | V_xs = c_List_Oappend(c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__eq__Cons__conv_0,axiom, % 0.47/0.63 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.47/0.63 | V_ys = c_List_Olist_OCons(V_x,c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_last__snoc_0,axiom, % 0.47/0.63 c_List_Olast(c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) = V_x ). % 0.47/0.63 % 0.47/0.63 cnf(cls_butlast__snoc_0,axiom, % 0.47/0.63 c_List_Obutlast(c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) = V_xs ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Snoc__step1__SnocD_2,axiom, % 0.47/0.63 ( V_ys = V_xs % 0.47/0.63 | V_y = V_x % 0.47/0.63 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Snoc__step1__SnocD_3,axiom, % 0.47/0.63 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.47/0.63 | V_y = V_x % 0.47/0.63 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_append__eq__Cons__conv_1,axiom, % 0.47/0.63 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.47/0.63 | c_List_Oappend(c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) = V_xs % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Cons__eq__append__conv_0,axiom, % 0.47/0.63 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.47/0.63 | c_List_Olist_OCons(V_x,c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) = V_ys % 0.47/0.63 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Snoc__step1__SnocD_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.47/0.63 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.47/0.63 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_rotate__simps_1,axiom, % 0.47/0.63 c_List_Orotate1(c_List_Olist_OCons(V_x,V_xs,T_b),T_b) = c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_b),T_b),T_b) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Snoc__step1__SnocD_0,axiom, % 0.47/0.63 ( V_ys = V_xs % 0.47/0.63 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.47/0.63 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_replicate__append__same_0,axiom, % 0.47/0.63 c_List_Oappend(c_List_Oreplicate(V_i,V_x,T_a),c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Oreplicate(V_i,V_x,T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_App__eq__foldl__conv_1,axiom, % 0.47/0.63 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.63 | V_ts = c_List_Oappend(c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(V_r,V_s,V_t,V_ts),c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) % 0.47/0.63 | V_ts = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_liftn__lift_0,axiom, % 0.47/0.63 c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = c_Lambda_Olift(c_Lambda_Oliftn(V_n,V_t,V_k),V_k) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_substn_Osimps_I1_J_2,axiom, % 0.47/0.63 ( c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.47/0.63 | V_i = V_k % 0.47/0.63 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_substn__subst__0_0,axiom, % 0.47/0.63 c_Lambda_Osubstn(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) = c_Lambda_Osubst(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_inf1E_1,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_B,V_x)) % 0.47/0.63 | ~ hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_foldl__foldr_0,axiom, % 0.47/0.63 c_List_Ofoldl(V_f,V_a,V_xs,T_a,T_b) = c_List_Ofoldr(c_COMBC(V_f,T_a,T_b,T_a),c_List_Orev(V_xs,T_b),V_a,T_b,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_singleton__rev__conv_1,axiom, % 0.47/0.63 c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) = c_List_Orev(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_map__update_0,axiom, % 0.47/0.63 c_List_Omap(V_f,c_List_Olist__update(V_xs,V_k,V_y,T_b),T_b,T_a) = c_List_Olist__update(c_List_Omap(V_f,V_xs,T_b,T_a),V_k,hAPP(V_f,V_y),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Cons__eq__append__conv_4,axiom, % 0.47/0.63 c_List_Olist_OCons(V_x,V_xs,T_a) = c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_not__Cons__self_0,axiom, % 0.47/0.63 V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_not__Cons__self2_0,axiom, % 0.47/0.63 c_List_Olist_OCons(V_x,V_t,T_a) != V_t ). % 0.47/0.63 % 0.47/0.63 cnf(cls_lift__preserves__beta_0,axiom, % 0.47/0.63 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.47/0.63 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_listsp_Oinducts_3,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xlistsp__Xinducts__1(V_A,V_P),v_sko__List__Xlistsp__Xinducts__2(V_A,V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.63 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_subst__lift_0,axiom, % 0.47/0.63 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.47/0.63 % 0.47/0.63 cnf(cls_listsp_Oinduct_3,axiom, % 0.47/0.63 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_OCons(v_sko__List__Xlistsp__Xinduct__1(V_A,V_P),v_sko__List__Xlistsp__Xinduct__2(V_A,V_P),t_a))) % 0.47/0.63 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.63 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_rev__eq__Cons__iff_1,axiom, % 0.47/0.63 c_List_Orev(c_List_Oappend(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),T_a) = c_List_Olist_OCons(V_y,V_ys,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_sorted__Cons_0,axiom, % 0.47/0.63 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.63 | c_List_Olinorder__class_Osorted(V_xs,T_a) % 0.47/0.63 | ~ c_List_Olinorder__class_Osorted(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Cons__eq__appendI_0,axiom, % 0.47/0.63 c_List_Olist_OCons(V_x,c_List_Oappend(V_xs1,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xs1,T_a),V_zs,T_a) ). % 0.47/0.63 % 0.47/0.63 cnf(cls_Cons__eq__append__conv_5,axiom, % 0.47/0.64 c_List_Olist_OCons(V_x,c_List_Oappend(V_xa,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xa,T_a),V_zs,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remove1_Osimps_I2_J_0,axiom, % 0.47/0.64 c_List_Oremove1(V_x,c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = V_xs ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Osimps_I5_J_0,axiom, % 0.47/0.64 c_List_Olist_Olist__case(V_f1,V_f2,c_List_Olist_OCons(V_a,V_list,T_b),T_a,T_b) = hAPP(hAPP(V_f2,V_a),V_list) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map_Osimps_I2_J_0,axiom, % 0.47/0.64 c_List_Omap(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),T_b,T_a) = c_List_Olist_OCons(hAPP(V_f,V_x),c_List_Omap(V_f,V_xs,T_b,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Cons__eq__map__conv_3,axiom, % 0.47/0.64 c_List_Olist_OCons(hAPP(V_f,V_xa),c_List_Omap(V_f,V_xb,T_b,T_a),T_a) = c_List_Omap(V_f,c_List_Olist_OCons(V_xa,V_xb,T_b),T_b,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map__eq__Cons__conv_3,axiom, % 0.47/0.64 c_List_Omap(V_f,c_List_Olist_OCons(V_x,V_xa,T_b),T_b,T_a) = c_List_Olist_OCons(hAPP(V_f,V_x),c_List_Omap(V_f,V_xa,T_b,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__Cons_0,axiom, % 0.47/0.64 c_List_Oappend(c_List_Olist_OCons(V_x,V_xs,T_a),V_ys,T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(V_xs,V_ys,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__eq__Cons__conv_5,axiom, % 0.47/0.64 c_List_Oappend(c_List_Olist_OCons(V_x,V_xa,T_a),V_zs,T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(V_xa,V_zs,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.47/0.64 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sorted_Osimps_I3_J_1,axiom, % 0.47/0.64 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.64 | c_List_Olinorder__class_Osorted(c_List_Olist_OCons(V_y,V_zs,T_a),T_a) % 0.47/0.64 | ~ c_List_Olinorder__class_Osorted(c_List_Olist_OCons(V_x,c_List_Olist_OCons(V_y,V_zs,T_a),T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__sup__aci_I1_J_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__commute_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Int__commute_0,axiom, % 0.47/0.64 c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_B,V_A,tc_fun(T_a,tc_bool)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__eq__Cons__iff_0,axiom, % 0.47/0.64 ( c_List_Orev(V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) % 0.47/0.64 | V_xs = c_List_Oappend(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__singleton__conv_1,axiom, % 0.47/0.64 c_List_Orev(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_foldl__Cons_0,axiom, % 0.47/0.64 c_List_Ofoldl(V_f,V_a,c_List_Olist_OCons(V_x,V_xs,T_b),T_a,T_b) = c_List_Ofoldl(V_f,hAPP(hAPP(V_f,V_a),V_x),V_xs,T_a,T_b) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev_Osimps_I2_J_0,axiom, % 0.47/0.64 c_List_Orev(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Oappend(c_List_Orev(V_xs,T_a),c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Cons__eq__filterD_2,axiom, % 0.47/0.64 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Ofilter(V_P,V_ys,T_a) % 0.47/0.64 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remdups__filter_0,axiom, % 0.47/0.64 c_List_Oremdups(c_List_Ofilter(V_P,V_xs,T_a),T_a) = c_List_Ofilter(V_P,c_List_Oremdups(V_xs,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_filter_Osimps_I2_J_0,axiom, % 0.47/0.64 ( c_List_Ofilter(V_P,c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Ofilter(V_P,V_xs,T_a),T_a) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_singleton__rev__conv_0,axiom, % 0.47/0.64 ( c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) != c_List_Orev(V_xs,T_a) % 0.47/0.64 | V_xs = c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I12_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),T_a) = hAPP(V_f3,V_dB) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_subst__preserves__beta_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Osubst(V_r,V_t,V_i)),c_Lambda_Osubst(V_s,V_t,V_i))) % 0.47/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__map_0,axiom, % 0.47/0.64 c_List_Orev(c_List_Omap(V_f,V_xs,T_b,T_a),T_a) = c_List_Omap(V_f,c_List_Orev(V_xs,T_b),T_b,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__same__eq_0,axiom, % 0.47/0.64 ( c_List_Oappend(V_ys,V_xs,T_a) != c_List_Oappend(V_zs,V_xs,T_a) % 0.47/0.64 | V_ys = V_zs ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_same__append__eq_0,axiom, % 0.47/0.64 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Oappend(V_xs,V_zs,T_a) % 0.47/0.64 | V_ys = V_zs ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_filter__eq__ConsD_2,axiom, % 0.47/0.64 ( c_List_Ofilter(V_P,V_ys,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.47/0.64 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rotate__map_0,axiom, % 0.47/0.64 c_List_Orotate(V_n,c_List_Omap(V_f,V_xs,T_b,T_a),T_a) = c_List_Omap(V_f,c_List_Orotate(V_n,V_xs,T_b),T_b,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__swap_0,axiom, % 0.47/0.64 V_xs = c_List_Orev(c_List_Orev(V_xs,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__swap_1,axiom, % 0.47/0.64 c_List_Orev(c_List_Orev(V_ys,T_a),T_a) = V_ys ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__rev__ident_0,axiom, % 0.47/0.64 c_List_Orev(c_List_Orev(V_xs,T_a),T_a) = V_xs ). % 0.47/0.64 % 0.47/0.64 cnf(cls_foldr__append_0,axiom, % 0.47/0.64 c_List_Ofoldr(V_f,c_List_Oappend(V_xs,V_ys,T_b),V_a,T_b,T_a) = c_List_Ofoldr(V_f,V_xs,c_List_Ofoldr(V_f,V_ys,V_a,T_b,T_a),T_b,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__ex_Osimps_I2_J_1,axiom, % 0.47/0.64 ( c_List_Olist__ex(V_P,c_List_Olist_OCons(V_x,V_xs,T_a),T_a) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__singleton__conv_0,axiom, % 0.47/0.64 ( c_List_Orev(V_xs,T_a) != c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) % 0.47/0.64 | V_xs = c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__ex_Osimps_I2_J_2,axiom, % 0.47/0.64 ( c_List_Olist__ex(V_P,c_List_Olist_OCons(V_x,V_xs,T_a),T_a) % 0.47/0.64 | ~ c_List_Olist__ex(V_P,V_xs,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__ex_Osimps_I2_J_0,axiom, % 0.47/0.64 ( c_List_Olist__ex(V_P,V_xs,T_a) % 0.47/0.64 | hBOOL(hAPP(V_P,V_x)) % 0.47/0.64 | ~ c_List_Olist__ex(V_P,c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_listrelp_OCons_0,axiom, % 0.47/0.64 ( c_List_Olistrelp(V_r,c_List_Olist_OCons(V_x,V_xs,T_a),c_List_Olist_OCons(V_y,V_ys,T_a),T_a) % 0.47/0.64 | ~ c_List_Olistrelp(V_r,V_xs,V_ys,T_a) % 0.47/0.64 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__sup__aci_I2_J_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__sup__aci_I3_J_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__left__commute_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__assoc_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Int__assoc_0,axiom, % 0.47/0.64 c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_A,c_Lattices_Olower__semilattice__class_Oinf(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Int__left__commute_0,axiom, % 0.47/0.64 c_Lattices_Olower__semilattice__class_Oinf(V_A,c_Lattices_Olower__semilattice__class_Oinf(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_B,c_Lattices_Olower__semilattice__class_Oinf(V_A,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.47/0.64 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.47/0.64 | V_dB = V_dB_H ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remove1_Osimps_I2_J_1,axiom, % 0.47/0.64 ( c_List_Oremove1(V_x,c_List_Olist_OCons(V_y,V_xs,T_a),T_a) = c_List_Olist_OCons(V_y,c_List_Oremove1(V_x,V_xs,T_a),T_a) % 0.47/0.64 | V_x = V_y ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_apps__preserves__beta_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,V_r,V_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.47/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map__append_0,axiom, % 0.47/0.64 c_List_Omap(V_f,c_List_Oappend(V_xs,V_ys,T_b),T_b,T_a) = c_List_Oappend(c_List_Omap(V_f,V_xs,T_b,T_a),c_List_Omap(V_f,V_ys,T_b,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_listsp_Ocases_0,axiom, % 0.47/0.64 ( V_a = c_List_Olist_OCons(v_sko__List__Xlistsp__Xcases__1(V_A,V_a),v_sko__List__Xlistsp__Xcases__2(V_A,V_a),t_a) % 0.47/0.64 | V_a = c_List_Olist_ONil(t_a) % 0.47/0.64 | ~ c_List_Olistsp(V_A,V_a,t_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.47/0.64 ( c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_rs,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | V_rs = V_ss ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.47/0.64 ( c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_rs,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | V_r = V_s ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.47/0.64 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.47/0.64 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remove1__filter__not_0,axiom, % 0.47/0.64 ( c_List_Oremove1(V_x,c_List_Ofilter(V_P,V_xs,T_a),T_a) = c_List_Ofilter(V_P,V_xs,T_a) % 0.47/0.64 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Orecs_I2_J_0,axiom, % 0.47/0.64 c_List_Olist_Olist__rec(V_f1,V_f2,c_List_Olist_OCons(V_a,V_list,T_b),T_a,T_b) = hAPP(hAPP(hAPP(V_f2,V_a),V_list),c_List_Olist_Olist__rec(V_f1,V_f2,V_list,T_a,T_b)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__is__rev__conv_0,axiom, % 0.47/0.64 ( c_List_Orev(V_xs,T_a) != c_List_Orev(V_ys,T_a) % 0.47/0.64 | V_xs = V_ys ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_foldr__foldl_0,axiom, % 0.47/0.64 c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a) = c_List_Ofoldl(c_COMBC(V_f,T_b,T_a,T_a),V_a,c_List_Orev(V_xs,T_b),T_a,T_b) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Orecs_I3_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),T_a) = hAPP(hAPP(V_f3,V_dB),c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,V_dB,T_a)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_List_Onull_Osimps_I2_J_0,axiom, % 0.47/0.64 ~ c_List_Onull(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__sup__aci_I4_J_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__left__idem_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Int__left__absorb_0,axiom, % 0.47/0.64 c_Lattices_Olower__semilattice__class_Oinf(V_A,c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_foldr_Osimps_I2_J_0,axiom, % 0.47/0.64 c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osplit_2,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),t_a))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(V_f3,V_dB))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osplit__asm_2,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_xa),t_a))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(V_f3,V_xa))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__eq__Cons__conv_4,axiom, % 0.47/0.64 c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf__idem_0,axiom, % 0.47/0.64 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.47/0.64 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_x,T_a) = V_x ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Int__absorb_0,axiom, % 0.47/0.64 c_Lattices_Olower__semilattice__class_Oinf(V_A,V_A,tc_fun(T_a,tc_bool)) = V_A ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Oinject_0,axiom, % 0.47/0.64 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.47/0.64 | V_a = V_a_H ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Oinject_1,axiom, % 0.47/0.64 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.47/0.64 | V_list = V_list_H ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_subject__reduction_0,axiom, % 0.47/0.64 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.47/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.47/0.64 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sorted__append_0,axiom, % 0.47/0.64 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.64 | c_List_Olinorder__class_Osorted(V_xs,T_a) % 0.47/0.64 | ~ c_List_Olinorder__class_Osorted(c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sorted__append_1,axiom, % 0.47/0.64 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.64 | c_List_Olinorder__class_Osorted(V_ys,T_a) % 0.47/0.64 | ~ c_List_Olinorder__class_Osorted(c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__update__swap_0,axiom, % 0.47/0.64 ( c_List_Olist__update(c_List_Olist__update(V_xs,V_i,V_x,T_a),V_i_H,V_x_H,T_a) = c_List_Olist__update(c_List_Olist__update(V_xs,V_i_H,V_x_H,T_a),V_i,V_x,T_a) % 0.47/0.64 | V_i = V_i_H ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sorted__remdups_0,axiom, % 0.47/0.64 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.64 | c_List_Olinorder__class_Osorted(c_List_Oremdups(V_l,T_a),T_a) % 0.47/0.64 | ~ c_List_Olinorder__class_Osorted(V_l,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_filter_Osimps_I2_J_1,axiom, % 0.47/0.64 ( c_List_Ofilter(V_P,c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Ofilter(V_P,V_xs,T_a) % 0.47/0.64 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_inf1I_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) % 0.47/0.64 | ~ hBOOL(hAPP(V_B,V_x)) % 0.47/0.64 | ~ hBOOL(hAPP(V_A,V_x)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__filter_0,axiom, % 0.47/0.64 c_List_Orev(c_List_Ofilter(V_P,V_xs,T_a),T_a) = c_List_Ofilter(V_P,c_List_Orev(V_xs,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append1__eq__conv_0,axiom, % 0.47/0.64 ( c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) != c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a) % 0.47/0.64 | V_xs = V_ys ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append1__eq__conv_1,axiom, % 0.47/0.64 ( c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) != c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a) % 0.47/0.64 | V_x = V_y ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Osplit_1,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_List_Olist_Olist__case(V_f1,V_f2,c_List_Olist_OCons(V_a,V_list,t_b),t_a,t_b))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_a),V_list))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Osplit__asm_1,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_List_Olist_Olist__case(V_f1,V_f2,c_List_Olist_OCons(V_xa,V_xb,t_b),t_a,t_b))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_xa),V_xb))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__update__overwrite_0,axiom, % 0.47/0.64 c_List_Olist__update(c_List_Olist__update(V_xs,V_i,V_x,T_a),V_i,V_y,T_a) = c_List_Olist__update(V_xs,V_i,V_y,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__assoc_0,axiom, % 0.47/0.64 c_List_Oappend(c_List_Oappend(V_xs,V_ys,T_a),V_zs,T_a) = c_List_Oappend(V_xs,c_List_Oappend(V_ys,V_zs,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__eq__appendI_0,axiom, % 0.47/0.64 c_List_Oappend(V_xs,c_List_Oappend(V_xs1,V_us,T_a),T_a) = c_List_Oappend(c_List_Oappend(V_xs,V_xs1,T_a),V_us,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__eq__append__conv2_4,axiom, % 0.47/0.64 c_List_Oappend(c_List_Oappend(V_zs,V_x,T_a),V_ys,T_a) = c_List_Oappend(V_zs,c_List_Oappend(V_x,V_ys,T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_append__eq__append__conv2_5,axiom, % 0.47/0.64 c_List_Oappend(V_xs,c_List_Oappend(V_x,V_ts,T_a),T_a) = c_List_Oappend(c_List_Oappend(V_xs,V_x,T_a),V_ts,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sorted__remove1_0,axiom, % 0.47/0.64 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.64 | c_List_Olinorder__class_Osorted(c_List_Oremove1(V_a,V_xs,T_a),T_a) % 0.47/0.64 | ~ c_List_Olinorder__class_Osorted(V_xs,T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__ex_Osimps_I1_J_0,axiom, % 0.47/0.64 ~ c_List_Olist__ex(V_P,c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_empty__null_0,axiom, % 0.47/0.64 c_List_Onull(c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Osplit_0,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_List_Olist_Olist__case(V_f1,V_f2,c_List_Olist_ONil(t_b),t_a,t_b))) % 0.47/0.64 | hBOOL(hAPP(V_P,V_f1)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.47/0.64 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.47/0.64 % 0.47/0.64 cnf(cls_zip_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xzip__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map__is__Nil__conv_1,axiom, % 0.47/0.64 c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sublist__nil_0,axiom, % 0.47/0.64 c_List_Osublist(c_List_Olist_ONil(T_a),V_A,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_listset_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xlistset__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Orecs_I1_J_0,axiom, % 0.47/0.64 c_List_Olist_Olist__rec(V_f1,V_f2,c_List_Olist_ONil(T_b),T_a,T_b) = V_f1 ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dropWhile_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__XdropWhile__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_take_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xtake__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_sorted_Osimps_I1_J_0,axiom, % 0.47/0.64 ( ~ class_Orderings_Olinorder(T_a) % 0.47/0.64 | c_List_Olinorder__class_Osorted(c_List_Olist_ONil(T_a),T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_filtermap_Osimps_I1_J_0,axiom, % 0.47/0.64 c_List_Ofiltermap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remdups__eq__nil__right__iff_0,axiom, % 0.47/0.64 ( c_List_Olist_ONil(T_a) != c_List_Oremdups(V_x,T_a) % 0.47/0.64 | V_x = c_List_Olist_ONil(T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_filter_Osimps_I1_J_0,axiom, % 0.47/0.64 c_List_Ofilter(V_P,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__update__nonempty_1,axiom, % 0.47/0.64 c_List_Olist__update(c_List_Olist_ONil(T_a),V_k,V_x,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__update__code_I1_J_0,axiom, % 0.47/0.64 c_List_Olist__update(c_List_Olist_ONil(T_a),V_i,V_y,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__update_Osimps_I1_J_0,axiom, % 0.47/0.64 c_List_Olist__update(c_List_Olist_ONil(T_a),V_i,V_v,T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_concat_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xconcat__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_neq__Nil__conv_1,axiom, % 0.47/0.64 c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Osimps_I3_J_0,axiom, % 0.47/0.64 c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remove1_Osimps_I1_J_0,axiom, % 0.47/0.64 c_List_Oremove1(V_x,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_distinct_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xdistinct__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map__upds__Nil2_0,axiom, % 0.47/0.64 c_Map_Omap__upds(V_m,V_as,c_List_Olist_ONil(T_b),T_a,T_b) = V_m ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map__upds__Nil1_0,axiom, % 0.47/0.64 c_Map_Omap__upds(V_m,c_List_Olist_ONil(T_a),V_bs,T_a,T_b) = V_m ). % 0.47/0.64 % 0.47/0.64 cnf(cls_remove1_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xremove1__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Osimps_I4_J_0,axiom, % 0.47/0.64 c_List_Olist_Olist__case(V_f1,V_f2,c_List_Olist_ONil(T_b),T_a,T_b) = V_f1 ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__is__Nil__conv_0,axiom, % 0.47/0.64 ( c_List_Orev(V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.64 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rotate__is__Nil__conv_1,axiom, % 0.47/0.64 c_List_Orotate(V_n,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xlist__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Nil__is__map__conv_1,axiom, % 0.47/0.64 c_List_Olist_ONil(T_a) = c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Nil__is__append__conv_2,axiom, % 0.47/0.64 c_List_Olist_ONil(T_a) = c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_listrelp_ONil_0,axiom, % 0.47/0.64 c_List_Olistrelp(V_r,c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_map_Oinduct_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(V_P,V_list)) % 0.47/0.64 | hBOOL(hAPP(V_P,v_sko__List__Xmap__Xinduct__2(V_P))) % 0.47/0.64 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_rev__is__Nil__conv_1,axiom, % 0.47/0.64 c_List_Orev(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_list__update__nonempty_0,axiom, % 0.47/0.64 ( c_List_Olist__update(V_xs,V_k,V_x,T_a) != c_List_Olist_ONil(T_a) % 0.47/0.64 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_subst__App_0,axiom, % 0.47/0.64 c_Lambda_Osubst(hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_s,V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_t,V_s,V_k)),c_Lambda_Osubst(V_u,V_s,V_k)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.47/0.64 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osplit__asm_1,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_xb),V_xc),t_a))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_xb),V_xc))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osplit_1,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),t_a))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_dB1),V_dB2))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.47/0.64 c_Lambda_Olift(hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Olift(V_s,V_k)),c_Lambda_Olift(V_t,V_k)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I11_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),T_a) = hAPP(hAPP(V_f2,V_dB1),V_dB2) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Orecs_I2_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),T_a) = hAPP(hAPP(hAPP(hAPP(V_f2,V_dB1),V_dB2),c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,V_dB1,T_a)),c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,V_dB2,T_a)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.47/0.64 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_r,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | V_r = V_s ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_appR_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,V_u),V_s)),hAPP(hAPP(c_Lambda_OdB_OApp,V_u),V_t))) % 0.47/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_appL_0,axiom, % 0.47/0.64 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_u)),hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u))) % 0.47/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_liftn_Osimps_I2_J_0,axiom, % 0.47/0.64 c_Lambda_Oliftn(V_n,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Oliftn(V_n,V_s,V_k)),c_Lambda_Oliftn(V_n,V_t,V_k)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_substn_Osimps_I2_J_0,axiom, % 0.47/0.64 c_Lambda_Osubstn(hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_s,V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Osubstn(V_t,V_s,V_k)),c_Lambda_Osubstn(V_u,V_s,V_k)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_var__app__type__eq_0,axiom, % 0.47/0.64 ( V_T = V_U % 0.47/0.64 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_U) % 0.47/0.64 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.47/0.64 c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ts,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),V_ss,tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.47/0.64 hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osplit__asm_0,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_xd),t_a))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(V_f1,V_xd))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osplit_0,axiom, % 0.47/0.64 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),t_a))) % 0.47/0.64 | hBOOL(hAPP(V_P,hAPP(V_f1,V_nat))) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_subst__eq_0,axiom, % 0.47/0.64 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.47/0.64 % 0.47/0.64 cnf(cls_beta__cases_I1_J_0,axiom, % 0.47/0.64 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Orecs_I1_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_typing__elims_I1_J_0,axiom, % 0.47/0.64 ( hAPP(V_e,V_i) = V_T % 0.47/0.64 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OVar(V_i),V_T) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_dB_Osimps_I10_J_0,axiom, % 0.47/0.64 c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_typing_OVar_0,axiom, % 0.47/0.64 c_Type_Otyping(V_env,c_Lambda_OdB_OVar(V_x),hAPP(V_env,V_x)) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.47/0.64 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.47/0.64 c_Lambda_OdB_OAbs(V_r) = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_App__eq__foldl__conv_2,axiom, % 0.47/0.64 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | V_r = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(V_r,V_s,V_t,V_ts),tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.64 | V_ts = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.47/0.64 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.47/0.64 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.47/0.64 % 0.47/0.64 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.47/0.65 c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) = c_Lambda_OdB_OAbs(V_r) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_append__in__listsp__conv_2,axiom, % 0.47/0.65 ( c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_ys,T_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_xs,T_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_in__listsp__conv__set_2,axiom, % 0.47/0.65 ( c_List_Olistsp(V_A,V_xs,T_a) % 0.47/0.65 | ~ hBOOL(hAPP(V_A,c_List_Osko__List__Xin__listsp__conv__set__1__1(V_A,V_xs,T_a))) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp__infI_0,axiom, % 0.47/0.65 ( c_List_Olistsp(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_l,T_a) % 0.47/0.65 | ~ c_List_Olistsp(V_B,V_l,T_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_l,T_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_append__in__listsp__conv_1,axiom, % 0.47/0.65 ( c_List_Olistsp(V_A,V_ys,T_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_append__in__listsp__conv_0,axiom, % 0.47/0.65 ( c_List_Olistsp(V_A,V_xs,T_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_lift__IT_0,axiom, % 0.47/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(V_t,V_i))) % 0.47/0.65 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Lambda_0,axiom, % 0.47/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.47/0.65 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.47/0.65 ( c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_m),V_rs,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.65 | V_m = V_n ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.47/0.65 ( c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_m),V_rs,tc_Lambda_OdB,tc_Lambda_OdB) != c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.65 | V_rs = V_ss ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.47/0.65 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.65 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Oinducts_0,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.65 | hBOOL(hAPP(V_A,v_sko__List__Xlistsp__Xinducts__1(V_A,V_P))) % 0.47/0.65 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Oinducts_2,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.65 | hBOOL(hAPP(V_P,v_sko__List__Xlistsp__Xinducts__2(V_A,V_P))) % 0.47/0.65 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Oinduct_0,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.65 | hBOOL(hAPP(V_A,v_sko__List__Xlistsp__Xinduct__1(V_A,V_P))) % 0.47/0.65 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Oinduct_2,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.65 | hBOOL(hAPP(V_P,v_sko__List__Xlistsp__Xinduct__2(V_A,V_P))) % 0.47/0.65 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Ocases_2,axiom, % 0.47/0.65 ( c_List_Olistsp(V_A,v_sko__List__Xlistsp__Xcases__2(V_A,V_a),t_a) % 0.47/0.65 | V_a = c_List_Olist_ONil(t_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_a,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Ocases_1,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_A,v_sko__List__Xlistsp__Xcases__1(V_A,V_a))) % 0.47/0.65 | V_a = c_List_Olist_ONil(t_a) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_a,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Oinducts_1,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.65 | c_List_Olistsp(V_A,v_sko__List__Xlistsp__Xinducts__2(V_A,V_P),t_a) % 0.47/0.65 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_Oinduct_1,axiom, % 0.47/0.65 ( hBOOL(hAPP(V_P,V_x)) % 0.47/0.65 | c_List_Olistsp(V_A,v_sko__List__Xlistsp__Xinduct__2(V_A,V_P),t_a) % 0.47/0.65 | ~ hBOOL(hAPP(V_P,c_List_Olist_ONil(t_a))) % 0.47/0.65 | ~ c_List_Olistsp(V_A,V_x,t_a) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.47/0.65 hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.47/0.65 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.65 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_subst__Var__IT_0,axiom, % 0.47/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j))) % 0.47/0.65 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.47/0.65 c_Lambda_OdB_OVar(V_m) = c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_m),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.47/0.65 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.47/0.65 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_IT_OVar_0,axiom, % 0.47/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_rs,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.47/0.65 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.47/0.65 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.47/0.65 | V_nat = V_nat_H ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.47/0.65 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.47/0.65 | V_dB1 = V_dB1_H ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.47/0.65 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.47/0.65 | V_dB2 = V_dB2_H ) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.47/0.65 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_Var__IT_0,axiom, % 0.47/0.65 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_listsp_ONil_0,axiom, % 0.47/0.65 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_COMBB__def_0,axiom, % 0.47/0.65 hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_COMBC__def_0,axiom, % 0.47/0.65 hAPP(hAPP(c_COMBC(V_P,T_b,T_c,T_a),V_Q),V_R) = hAPP(hAPP(V_P,V_R),V_Q) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.47/0.65 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_conjecture_0,negated_conjecture, % 0.47/0.65 c_List_Olistsp(c_InductTermi_OIT,v_rs,tc_Lambda_OdB) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_conjecture_1,negated_conjecture, % 0.47/0.65 c_List_Olistsp(c_COMBB(c_InductTermi_OIT,hAPP(c_COMBC(c_Lambda_OdB_OApp,tc_Lambda_OdB,tc_Lambda_OdB,tc_Lambda_OdB),c_Lambda_OdB_OVar(v_i)),tc_Lambda_OdB,tc_bool,tc_Lambda_OdB),v_rs,tc_Lambda_OdB) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_conjecture_2,negated_conjecture, % 0.47/0.65 ~ c_List_Olistsp(c_InductTermi_OIT,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_fun__Lattices_Olower__semilattice,axiom, % 0.47/0.65 ( class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) % 0.47/0.65 | ~ class_Lattices_Olattice(T_1) ) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.47/0.65 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.47/0.65 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_fun__Lattices_Olattice,axiom, % 0.47/0.65 ( class_Lattices_Olattice(tc_fun(T_2,T_1)) % 0.47/0.65 | ~ class_Lattices_Olattice(T_1) ) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.47/0.65 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.47/0.65 | ~ class_Orderings_Oorder(T_1) ) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_nat__Lattices_Olower__semilattice,axiom, % 0.47/0.65 class_Lattices_Olower__semilattice(tc_nat) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.47/0.65 class_Orderings_Opreorder(tc_nat) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.47/0.65 class_Orderings_Olinorder(tc_nat) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_nat__Lattices_Olattice,axiom, % 0.47/0.65 class_Lattices_Olattice(tc_nat) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.47/0.65 class_Orderings_Oorder(tc_nat) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_bool__Lattices_Olower__semilattice,axiom, % 0.47/0.65 class_Lattices_Olower__semilattice(tc_bool) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_bool__Orderings_Opreorder,axiom, % 0.47/0.65 class_Orderings_Opreorder(tc_bool) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_bool__Lattices_Olattice,axiom, % 0.47/0.65 class_Lattices_Olattice(tc_bool) ). % 0.47/0.65 % 0.47/0.65 cnf(clsarity_bool__Orderings_Oorder,axiom, % 0.47/0.65 class_Orderings_Oorder(tc_bool) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_ATP__Linkup_OCOMBC__def_0,axiom, % 0.47/0.65 hAPP(hAPP(c_COMBC(V_P,T_b,T_c,T_a),V_Q),V_R) = hAPP(hAPP(V_P,V_R),V_Q) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_ATP__Linkup_OCOMBB__def_0,axiom, % 0.47/0.65 hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.47/0.65 c_fequal(V_x,V_x,T_a) ). % 0.47/0.65 % 0.47/0.65 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.47/0.65 ( V_X = V_Y % 0.47/0.65 | ~ c_fequal(V_X,V_Y,T_a) ) ). % 0.47/0.65 % 0.47/0.65 %------------------------------------------------------------------------------ % 0.47/0.65 %------------------------------------------- % 0.47/0.65 % Proof found % 0.47/0.65 % SZS status Theorem for theBenchmark % 0.47/0.65 % SZS output start Proof % 0.47/0.65 %ClaNum:625(EqnAxiom:200) % 0.47/0.65 %VarNum:2572(SingletonVarNum:1117) % 0.47/0.65 %MaxLitNum:4 % 0.47/0.65 %MaxfuncDepth:5 % 0.47/0.65 %SharedTerms:34 % 0.47/0.65 %goalClause: 222 346 366 % 0.47/0.65 %singleGoalClaCount:3 % 0.47/0.65 [201]P1(a1) % 0.47/0.65 [202]P1(a2) % 0.47/0.65 [203]P2(a1) % 0.47/0.65 [204]P2(a2) % 0.47/0.65 [205]P3(a1) % 0.47/0.65 [206]P4(a1) % 0.47/0.65 [207]P4(a2) % 0.47/0.65 [208]P5(a1) % 0.47/0.65 [209]P5(a2) % 0.47/0.65 [222]P7(a8,a53,a49) % 0.47/0.65 [366]~P7(a8,f3(a49),a49) % 0.47/0.65 [346]P7(f7(a8,f46(f6(a10,a49,a49,a49),f9(a54)),a49,a2,a49),a53,a49) % 0.47/0.65 [365]~P8(x3651,x3651,a1) % 0.47/0.65 [210]P6(f3(x2101),x2101) % 0.47/0.65 [227]P8(x2271,f48(x2271),a1) % 0.47/0.65 [238]P8(f5(a1),f48(x2381),a1) % 0.47/0.65 [353]~E(f48(x3531),x3531) % 0.47/0.65 [357]~E(f48(x3571),f5(a1)) % 0.47/0.65 [370]~P8(x3701,f5(a1),a1) % 0.47/0.65 [213]E(f27(f3(x2131),x2131),f3(x2131)) % 0.47/0.65 [214]E(f35(f3(x2141),x2141),f3(x2141)) % 0.47/0.65 [215]E(f4(f3(x2151),x2151),f3(x2151)) % 0.47/0.65 [216]E(f32(f3(x2161),x2161),f3(x2161)) % 0.47/0.65 [217]E(f38(f3(x2171),f37(x2171)),f5(a1)) % 0.47/0.65 [218]P15(f46(a8,f9(x2181))) % 0.47/0.65 [377]~P8(f5(a1),f38(f3(x3771),f37(x3771)),a1) % 0.47/0.65 [224]P13(x2241,x2241,x2242) % 0.47/0.65 [228]P7(x2281,f3(x2282),x2282) % 0.47/0.65 [250]P14(x2501,f9(x2502),f46(x2501,x2502)) % 0.47/0.65 [284]P9(x2841,f3(x2842),f3(x2842),x2842) % 0.47/0.65 [359]~E(f12(x3591),f9(x3592)) % 0.47/0.65 [375]~P10(x3751,f3(x3752),x3752) % 0.47/0.65 [221]E(f32(f32(x2211,x2212),x2212),x2211) % 0.47/0.65 [223]E(f47(f47(x2231,x2232),x2232),f47(x2231,x2232)) % 0.47/0.65 [225]E(f13(f5(a1),x2251,x2252),x2251) % 0.47/0.65 [232]E(f17(x2321,f3(x2322),x2322),x2321) % 0.47/0.65 [233]E(f17(f3(x2331),x2332,x2331),x2332) % 0.47/0.65 [234]E(f18(f9(x2341),x2342,x2341),x2342) % 0.47/0.65 [236]E(f33(f5(a1),x2361,x2362),f3(x2362)) % 0.47/0.65 [239]E(f36(x2391,f3(x2392),x2392),f3(x2392)) % 0.47/0.65 [240]E(f22(x2401,f3(x2402),x2402),f3(x2402)) % 0.47/0.65 [241]E(f34(x2411,f3(x2412),x2412),f3(x2412)) % 0.47/0.65 [242]E(f39(f3(x2421),x2422,x2421),f3(x2421)) % 0.47/0.65 [243]E(f38(f35(x2431,x2432),f37(x2432)),f38(x2431,f37(x2432))) % 0.47/0.65 [244]E(f38(f32(x2441,x2442),f37(x2442)),f38(x2441,f37(x2442))) % 0.47/0.65 [248]E(f19(x2481,x2481,f52(x2482,a2)),x2481) % 0.47/0.65 [277]E(f18(x2771,f13(f5(a1),x2772,f5(a1)),f5(a1)),f18(x2771,x2772,f5(a1))) % 0.47/0.65 [253]E(f24(f23(x2531,f3(x2532),x2532),x2532),x2531) % 0.47/0.65 [254]E(f4(f23(x2541,f3(x2542),x2542),x2542),f3(x2542)) % 0.47/0.65 [255]E(f24(f17(x2551,f3(x2552),x2552),x2552),f24(x2551,x2552)) % 0.47/0.65 [256]E(f4(f17(x2561,f3(x2562),x2562),x2562),f4(x2561,x2562)) % 0.47/0.65 [268]E(f32(f23(x2681,f3(x2682),x2682),x2682),f23(x2681,f3(x2682),x2682)) % 0.47/0.65 [311]P15(f46(f46(a11,f46(f46(a10,f12(x3111)),x3112)),f18(x3111,x3112,f5(a1)))) % 0.47/0.65 [376]~P15(f46(f46(a11,f9(x3761)),x3762)) % 0.47/0.65 [368]~E(f23(x3681,x3682,x3683),x3682) % 0.47/0.65 [373]~E(f23(x3731,x3732,x3733),f3(x3733)) % 0.47/0.65 [378]~P6(f23(x3781,x3782,x3783),x3783) % 0.47/0.65 [379]~P11(x3791,x3792,f3(x3793),x3793) % 0.47/0.65 [380]~P11(x3801,f3(x3802),x3803,x3802) % 0.47/0.65 [249]E(f18(f14(x2491,x2492),x2493,x2492),x2491) % 0.47/0.65 [251]E(f33(f5(a1),x2511,x2512),f33(f5(a1),x2513,x2512)) % 0.47/0.65 [252]E(f38(f33(x2521,x2522,x2523),f37(x2523)),x2521) % 0.47/0.65 [257]E(f38(f36(x2571,x2572,x2573),f37(x2573)),f38(x2572,f37(x2573))) % 0.47/0.65 [258]E(f19(x2581,x2582,f52(x2583,a2)),f19(x2582,x2581,f52(x2583,a2))) % 0.47/0.65 [259]E(f34(x2591,f23(x2591,x2592,x2593),x2593),x2592) % 0.47/0.65 [262]E(f32(f33(x2621,x2622,x2623),x2623),f33(x2621,x2622,x2623)) % 0.47/0.65 [263]E(f35(f36(x2631,x2632,x2633),x2633),f36(f48(x2631),x2632,x2633)) % 0.47/0.65 [264]E(f14(f13(x2641,x2642,x2643),x2643),f13(f48(x2641),x2642,x2643)) % 0.47/0.65 [270]E(f22(x2701,f27(x2702,x2703),x2703),f27(f22(x2701,x2702,x2703),x2703)) % 0.47/0.65 [271]E(f36(x2711,f35(x2712,x2713),x2713),f35(f36(x2711,x2712,x2713),x2713)) % 0.47/0.65 [272]E(f22(x2721,f32(x2722,x2723),x2723),f32(f22(x2721,x2722,x2723),x2723)) % 0.47/0.65 [274]E(f23(x2741,f33(x2742,x2741,x2743),x2743),f33(f48(x2742),x2741,x2743)) % 0.47/0.65 [276]E(f17(f32(x2761,x2762),f32(x2763,x2762),x2762),f32(f17(x2763,x2761,x2762),x2762)) % 0.47/0.65 [279]E(f28(x2791,f3(x2792),x2792,x2793),f3(x2793)) % 0.47/0.65 [280]E(f25(x2801,f3(x2802),x2802,x2803),f3(x2803)) % 0.47/0.65 [283]E(f29(f3(x2831),x2832,x2833,x2831),f3(x2831)) % 0.47/0.65 [286]E(f19(x2861,f19(x2861,x2862,f52(x2863,a2)),f52(x2863,a2)),f19(x2861,x2862,f52(x2863,a2))) % 0.47/0.65 [360]~E(f9(x3601),f46(f46(a10,x3602),x3603)) % 0.47/0.65 [361]~E(f12(x3611),f46(f46(a10,x3612),x3613)) % 0.47/0.65 [362]~E(f46(f46(a10,x3621),x3622),f9(x3623)) % 0.47/0.65 [363]~E(f46(f46(a10,x3631),x3632),f12(x3633)) % 0.47/0.65 [261]E(f38(f23(x2611,x2612,x2613),f37(x2613)),f48(f38(x2612,f37(x2613)))) % 0.47/0.65 [266]P15(f46(f46(f47(x2661,x2662),x2663),x2663)) % 0.47/0.65 [269]E(f46(f46(a10,f14(x2691,x2692)),f14(x2693,x2692)),f14(f46(f46(a10,x2691),x2693),x2692)) % 0.47/0.65 [285]E(f17(x2851,f23(x2852,f3(x2853),x2853),x2853),f35(f23(x2852,x2851,x2853),x2853)) % 0.47/0.65 [287]E(f17(f32(x2871,x2872),f23(x2873,f3(x2872),x2872),x2872),f32(f23(x2873,x2871,x2872),x2872)) % 0.47/0.65 [301]E(f17(f33(x3011,x3012,x3013),f23(x3012,f3(x3013),x3013),x3013),f23(x3012,f33(x3011,x3012,x3013),x3013)) % 0.47/0.65 [296]E(f24(f17(x2961,f23(x2962,f3(x2963),x2963),x2963),x2963),x2962) % 0.47/0.65 [297]E(f4(f17(x2971,f23(x2972,f3(x2973),x2973),x2973),x2973),x2971) % 0.47/0.65 [304]E(f32(f17(f32(x3041,x3042),f23(x3043,f3(x3042),x3042),x3042),x3042),f23(x3043,x3041,x3042)) % 0.47/0.65 [349]E(f26(a10,x3491,f17(x3492,f23(x3493,f3(a49),a49),a49),a49,a49),f46(f46(a10,f26(a10,x3491,x3492,a49,a49)),x3493)) % 0.47/0.65 [293]E(f23(x2931,f17(x2932,x2933,x2934),x2934),f17(f23(x2931,x2932,x2934),x2933,x2934)) % 0.47/0.65 [295]E(f17(f17(x2951,x2952,x2953),x2954,x2953),f17(x2951,f17(x2952,x2954,x2953),x2953)) % 0.47/0.65 [298]E(f29(f23(x2981,x2982,x2983),f5(a1),x2984,x2983),f23(x2984,x2982,x2983)) % 0.47/0.65 [299]E(f17(f22(x2991,x2992,x2993),f22(x2991,x2994,x2993),x2993),f22(x2991,f17(x2992,x2994,x2993),x2993)) % 0.47/0.65 [302]E(f19(x3021,f19(x3022,x3023,f52(x3024,a2)),f52(x3024,a2)),f19(x3022,f19(x3021,x3023,f52(x3024,a2)),f52(x3024,a2))) % 0.47/0.65 [303]E(f19(f19(x3031,x3032,f52(x3033,a2)),x3034,f52(x3033,a2)),f19(x3031,f19(x3032,x3034,f52(x3033,a2)),f52(x3033,a2))) % 0.47/0.65 [307]E(f38(f29(x3071,x3072,x3073,x3074),f37(x3074)),f38(x3071,f37(x3074))) % 0.47/0.65 [308]E(f38(f28(x3081,x3082,x3083,x3084),f37(x3084)),f38(x3082,f37(x3083))) % 0.47/0.65 [309]E(f17(f33(x3091,x3092,x3093),f33(x3094,x3092,x3093),x3093),f17(f33(x3094,x3092,x3093),f33(x3091,x3092,x3093),x3093)) % 0.47/0.65 [313]E(f32(f28(x3131,x3132,x3133,x3134),x3134),f28(x3131,f32(x3132,x3133),x3133,x3134)) % 0.47/0.65 [322]E(f26(x3221,x3222,f3(x3223),x3224,x3223),x3222) % 0.47/0.65 [323]E(f45(x3231,x3232,f3(x3233),x3234,x3233),x3231) % 0.47/0.65 [324]E(f30(x3241,x3242,f3(x3243),x3244,x3243),x3241) % 0.47/0.65 [325]E(f31(x3251,x3252,f3(x3253),x3254,x3253),x3251) % 0.47/0.65 [326]E(f45(x3261,f3(x3262),x3263,x3262,x3264),x3261) % 0.47/0.65 [382]~E(f26(a10,f12(x3821),x3822,a49,a49),f26(a10,f9(x3823),x3824,a49,a49)) % 0.47/0.65 [305]E(f46(f46(a10,f13(x3051,x3052,x3053)),f13(x3051,x3054,x3053)),f13(x3051,f46(f46(a10,x3052),x3054),x3053)) % 0.47/0.65 [306]E(f46(f46(a10,f18(x3061,x3062,x3063)),f18(x3064,x3062,x3063)),f18(f46(f46(a10,x3061),x3064),x3062,x3063)) % 0.47/0.65 [310]E(f23(x3101,f17(f33(x3102,x3101,x3103),x3104,x3103),x3103),f17(f33(x3102,x3101,x3103),f23(x3101,x3104,x3103),x3103)) % 0.47/0.65 [339]E(f26(f6(x3391,x3392,x3393,x3393),x3394,f32(f3(x3392),x3392),x3393,x3392),x3394) % 0.47/0.65 [381]~E(f46(f46(a10,f12(x3811)),x3812),f26(a10,f9(x3813),x3814,a49,a49)) % 0.47/0.65 [300]E(f28(x3001,f33(x3002,x3003,x3004),x3004,x3005),f33(x3002,f46(x3001,x3003),x3005)) % 0.47/0.65 [314]E(f36(x3141,f28(x3142,x3143,x3144,x3145),x3145),f28(x3142,f36(x3141,x3143,x3144),x3144,x3145)) % 0.47/0.65 [315]E(f29(f23(x3151,x3152,x3153),f48(x3154),x3155,x3153),f23(x3151,f29(x3152,x3154,x3155,x3153),x3153)) % 0.47/0.65 [317]E(f28(x3171,f23(x3172,x3173,x3174),x3174,x3175),f23(f46(x3171,x3172),f28(x3171,x3173,x3174,x3175),x3175)) % 0.47/0.65 [318]E(f23(f46(x3181,x3182),f28(x3181,x3183,x3184,x3185),x3185),f28(x3181,f23(x3182,x3183,x3184),x3184,x3185)) % 0.47/0.65 [319]E(f29(f29(x3191,x3192,x3193,x3194),x3192,x3195,x3194),f29(x3191,x3192,x3195,x3194)) % 0.47/0.65 [330]E(f15(x3301,x3302,x3303,f9(x3304),x3305),f46(x3301,x3304)) % 0.47/0.65 [331]E(f15(x3311,x3312,x3313,f12(x3314),x3315),f46(x3313,x3314)) % 0.47/0.65 [332]E(f16(x3321,x3322,x3323,f9(x3324),x3325),f46(x3321,x3324)) % 0.47/0.65 [337]E(f17(f28(x3371,x3372,x3373,x3374),f28(x3371,x3375,x3373,x3374),x3374),f28(x3371,f17(x3372,x3375,x3373),x3373,x3374)) % 0.47/0.65 [343]E(f46(f46(x3431,x3432),f16(x3433,x3434,x3431,x3432,x3435)),f16(x3433,x3434,x3431,f12(x3432),x3435)) % 0.47/0.65 [312]E(f29(f17(x3121,f23(x3122,x3123,x3124),x3124),f38(x3121,f37(x3124)),x3125,x3124),f17(x3121,f23(x3125,x3123,x3124),x3124)) % 0.47/0.65 [345]E(f26(f6(f6(x3451,x3452,x3453,x3452),x3453,x3452,x3452),x3454,f32(f32(x3455,x3453),x3453),x3452,x3453),f26(x3451,x3454,x3455,x3452,x3453)) % 0.47/0.65 [336]E(f30(x3361,x3362,f23(x3363,x3364,x3365),x3366,x3365),f46(f46(x3362,x3363),x3364)) % 0.47/0.65 [338]E(f28(x3381,f29(x3382,x3383,x3384,x3385),x3385,x3386),f29(f28(x3381,x3382,x3385,x3386),x3383,f46(x3381,x3384),x3386)) % 0.47/0.65 [341]E(f46(f7(x3411,x3412,x3413,x3414,x3415),x3416),f46(x3411,f46(x3412,x3416))) % 0.47/0.65 [344]E(f31(x3441,x3442,f23(x3443,x3444,x3445),x3446,x3445),f46(f46(f46(x3442,x3443),x3444),f31(x3441,x3442,x3444,x3446,x3445))) % 0.47/0.65 [347]E(f26(x3471,f26(x3471,x3472,x3473,x3474,x3475),x3476,x3474,x3475),f26(x3471,x3472,f17(x3473,x3476,x3475),x3474,x3475)) % 0.47/0.65 [321]E(f46(f46(f6(x3211,x3212,x3213,x3214),x3215),x3216),f46(f46(x3211,x3216),x3215)) % 0.47/0.65 [335]E(f15(x3351,x3352,x3353,f46(f46(a10,x3354),x3355),x3356),f46(f46(x3352,x3354),x3355)) % 0.47/0.65 [342]E(f26(x3421,x3422,f23(x3423,x3424,x3425),x3426,x3425),f26(x3421,f46(f46(x3421,x3422),x3423),x3424,x3426,x3425)) % 0.47/0.65 [348]E(f26(f6(x3481,x3482,x3483,x3483),x3484,f32(f23(x3485,x3486,x3482),x3482),x3483,x3482),f46(f46(x3481,x3485),f26(f6(x3481,x3482,x3483,x3483),x3484,f32(x3486,x3482),x3483,x3482))) % 0.47/0.65 [350]E(f26(f6(x3501,x3502,x3503,x3503),f26(f6(x3501,x3502,x3503,x3503),x3504,f32(x3505,x3502),x3503,x3502),f32(x3506,x3502),x3503,x3502),f26(f6(x3501,x3502,x3503,x3503),x3504,f32(f17(x3506,x3505,x3502),x3502),x3503,x3502)) % 0.47/0.65 [351]E(f46(f46(f46(f46(x3511,x3512),x3513),f16(x3514,x3511,x3515,x3512,x3516)),f16(x3514,x3511,x3515,x3513,x3516)),f16(x3514,x3511,x3515,f46(f46(a10,x3512),x3513),x3516)) % 0.47/0.65 [387]~P3(x3871)+P12(f3(x3871),x3871) % 0.47/0.65 [400]E(x4001,f5(a1))+P8(f5(a1),x4001,a1) % 0.47/0.65 [403]~P15(f46(a8,x4031))+P15(f46(a8,f12(x4031))) % 0.47/0.65 [420]E(x4201,f5(a1))+~P8(x4201,f48(f5(a1)),a1) % 0.47/0.65 [409]~P8(x4092,x4092,x4091)+~P1(x4091) % 0.47/0.65 [410]~P8(x4102,x4102,x4101)+~P2(x4101) % 0.47/0.65 [411]~P8(x4112,x4112,x4111)+~P3(x4111) % 0.47/0.65 [384]E(x3841,x3842)+~E(f48(x3841),f48(x3842)) % 0.47/0.65 [385]E(x3851,x3852)+~E(f9(x3851),f9(x3852)) % 0.47/0.65 [386]E(x3861,x3862)+~E(f12(x3861),f12(x3862)) % 0.47/0.65 [388]~P6(x3881,x3882)+E(x3881,f3(x3882)) % 0.47/0.65 [391]~E(f27(x3911,x3912),f3(x3912))+E(x3911,f3(x3912)) % 0.47/0.65 [392]~E(f35(x3921,x3922),f3(x3922))+E(x3921,f3(x3922)) % 0.47/0.65 [393]~E(f32(x3931,x3932),f3(x3932))+E(x3931,f3(x3932)) % 0.47/0.65 [394]~P1(x3942)+P1(f52(x3941,x3942)) % 0.47/0.65 [395]~P2(x3952)+P2(f52(x3951,x3952)) % 0.47/0.65 [396]~P5(x3962)+P4(f52(x3961,x3962)) % 0.47/0.65 [397]~P5(x3972)+P5(f52(x3971,x3972)) % 0.47/0.65 [401]~P4(x4012)+E(f19(x4011,x4011,x4012),x4011) % 0.47/0.65 [425]P8(x4251,x4252,a1)+P8(x4252,f48(x4251),a1) % 0.47/0.65 [453]~P8(x4531,x4532,a1)+P8(x4531,f48(x4532),a1) % 0.47/0.65 [454]P8(x4541,x4542,a1)+~P8(f48(x4541),x4542,a1) % 0.47/0.65 [462]~P8(x4621,x4622,a1)+P8(f48(x4621),f48(x4622),a1) % 0.47/0.65 [464]P8(x4641,x4642,a1)+~P8(f48(x4641),f48(x4642),a1) % 0.47/0.65 [472]~P8(x4721,x4722,a1)+~P8(x4722,f48(x4721),a1) % 0.47/0.65 [398]E(x3981,f3(x3982))+~E(f38(x3981,f37(x3982)),f5(a1)) % 0.47/0.65 [419]E(x4191,f3(x4192))+P8(f5(a1),f38(x4191,f37(x4192)),a1) % 0.47/0.65 [421]~P8(x4211,x4212,a1)+E(f14(f9(x4211),x4212),f9(x4211)) % 0.47/0.65 [437]E(f27(x4371,x4372),x4371)+~E(f38(f27(x4371,x4372),f37(x4372)),f38(x4371,f37(x4372))) % 0.47/0.65 [439]~P15(f46(a8,x4391))+P15(f46(a8,f14(x4391,x4392))) % 0.47/0.65 [452]~P3(x4522)+P12(f23(x4521,f3(x4522),x4522),x4522) % 0.47/0.65 [494]~P15(f46(f46(a11,x4941),x4942))+P15(f46(f46(a11,f12(x4941)),f12(x4942))) % 0.47/0.65 [509]E(x5091,f3(x5092))+E(f17(f4(x5091,x5092),f23(f24(x5091,x5092),f3(x5092),x5092),x5092),x5091) % 0.47/0.65 [534]P15(f46(f46(f47(a11,a49),f12(x5341)),f12(x5342)))+~P15(f46(f46(f47(a11,a49),x5341),x5342)) % 0.47/0.65 [608]~P7(a8,x6082,a49)+P15(f46(a8,f26(a10,f9(x6081),x6082,a49,a49))) % 0.47/0.65 [404]E(x4041,x4042)+~P13(x4041,x4042,x4043) % 0.47/0.65 [399]E(x3991,x3992)+~E(f32(x3991,x3993),f32(x3992,x3993)) % 0.47/0.65 [407]~E(f17(x4073,x4071,x4072),x4073)+E(x4071,f3(x4072)) % 0.47/0.65 [408]~E(f17(x4081,x4083,x4082),x4083)+E(x4081,f3(x4082)) % 0.47/0.65 [413]~E(f33(x4131,x4132,x4133),f3(x4133))+E(x4131,f5(a1)) % 0.47/0.65 [416]~E(f17(x4163,x4161,x4162),f3(x4162))+E(x4161,f3(x4162)) % 0.47/0.65 [417]~E(f36(x4173,x4171,x4172),f3(x4172))+E(x4171,f3(x4172)) % 0.47/0.65 [418]~E(f17(x4181,x4183,x4182),f3(x4182))+E(x4181,f3(x4182)) % 0.47/0.65 [424]~P14(x4241,f9(x4242),x4243)+E(f46(x4241,x4242),x4243) % 0.47/0.65 [428]~P4(x4283)+E(f19(x4281,x4282,x4283),f19(x4282,x4281,x4283)) % 0.47/0.65 [429]~P5(x4293)+E(f19(x4291,x4292,x4293),f19(x4292,x4291,x4293)) % 0.47/0.65 [583]~E(f9(x5832),f26(a10,x5833,x5831,a49,a49))+E(x5831,f3(a49)) % 0.47/0.65 [584]~E(f12(x5842),f26(a10,x5843,x5841,a49,a49))+E(x5841,f3(a49)) % 0.47/0.65 [585]~E(f26(a10,x5852,x5851,a49,a49),f12(x5853))+E(x5851,f3(a49)) % 0.47/0.65 [586]E(x5861,f12(x5862))+~E(f26(a10,x5861,x5863,a49,a49),f12(x5862)) % 0.47/0.65 [587]E(f9(x5871),x5872)+~E(f9(x5871),f26(a10,x5872,x5873,a49,a49)) % 0.47/0.65 [588]E(f12(x5881),x5882)+~E(f12(x5881),f26(a10,x5882,x5883,a49,a49)) % 0.47/0.65 [603]E(x6031,x6032)+~E(f26(a10,x6031,x6033,a49,a49),f26(a10,x6032,x6033,a49,a49)) % 0.47/0.65 [440]E(x4401,f5(a1))+E(f24(f33(x4401,x4402,x4403),x4403),x4402) % 0.47/0.65 [450]E(x4501,f3(x4502))+E(f24(f23(x4503,x4501,x4502),x4502),f24(x4501,x4502)) % 0.47/0.65 [451]E(x4511,f3(x4512))+E(f24(f17(x4513,x4511,x4512),x4512),f24(x4511,x4512)) % 0.47/0.65 [455]~P8(x4552,x4553,a1)+E(f13(x4551,f9(x4552),x4553),f9(x4552)) % 0.47/0.65 [456]~P8(x4561,x4563,a1)+E(f18(f9(x4561),x4562,x4563),f9(x4561)) % 0.47/0.65 [474]~E(f32(x4741,x4743),f23(x4742,f3(x4743),x4743))+E(x4741,f23(x4742,f3(x4743),x4743)) % 0.47/0.65 [475]~E(f23(x4752,f3(x4753),x4753),f32(x4751,x4753))+E(x4751,f23(x4752,f3(x4753),x4753)) % 0.47/0.65 [485]E(x4851,f3(x4852))+E(f23(x4853,f4(x4851,x4852),x4852),f4(f23(x4853,x4851,x4852),x4852)) % 0.47/0.65 [486]E(x4861,f3(x4862))+E(f17(x4863,f4(x4861,x4862),x4862),f4(f17(x4863,x4861,x4862),x4862)) % 0.47/0.65 [491]~P4(x4913)+E(f19(x4911,f19(x4911,x4912,x4913),x4913),f19(x4911,x4912,x4913)) % 0.47/0.65 [492]~P5(x4923)+E(f19(x4921,f19(x4921,x4922,x4923),x4923),f19(x4921,x4922,x4923)) % 0.47/0.65 [525]~P15(f46(f46(a11,x5251),x5253))+P15(f46(f46(a11,f14(x5251,x5252)),f14(x5253,x5252))) % 0.47/0.65 [533]P7(x5331,x5332,x5333)+~P15(f46(x5331,f40(x5331,x5332,x5333))) % 0.47/0.65 [589]E(f46(f46(a10,x5891),x5892),x5893)+~E(f46(f46(a10,x5891),x5892),f26(a10,x5893,f3(a49),a49,a49)) % 0.47/0.65 [621]~P15(f46(f46(a11,x6211),x6213))+P15(f46(f46(a11,f26(a10,x6211,x6212,a49,a49)),f26(a10,x6213,x6212,a49,a49))) % 0.47/0.65 [623]~P11(a11,x6232,x6233,a49)+P15(f46(f46(a11,f26(a10,x6231,x6232,a49,a49)),f26(a10,x6231,x6233,a49,a49))) % 0.47/0.65 [514]~P15(f46(a8,x5141))+P15(f46(a8,f18(x5141,f9(x5142),x5143))) % 0.47/0.65 [548]P15(f46(f46(f47(a11,a49),f14(x5481,x5482)),f14(x5483,x5482)))+~P15(f46(f46(f47(a11,a49),x5481),x5483)) % 0.47/0.65 [552]~P15(f46(f46(a11,x5521),x5523))+P15(f46(f46(a11,f46(f46(a10,x5521),x5522)),f46(f46(a10,x5523),x5522))) % 0.47/0.65 [553]~P15(f46(f46(a11,x5532),x5533))+P15(f46(f46(a11,f46(f46(a10,x5531),x5532)),f46(f46(a10,x5531),x5533))) % 0.47/0.65 [562]~P15(f46(f46(f47(a11,a49),x5621),x5623))+P15(f46(f46(f47(a11,a49),f46(f46(a10,x5621),x5622)),f46(f46(a10,x5623),x5622))) % 0.47/0.65 [563]~P15(f46(f46(f47(a11,a49),x5632),x5633))+P15(f46(f46(f47(a11,a49),f46(f46(a10,x5631),x5632)),f46(f46(a10,x5631),x5633))) % 0.47/0.65 [610]P15(f46(x6101,x6102))+~P15(f46(x6101,f30(x6102,x6103,f3(a51),a50,a51))) % 0.47/0.65 [622]P15(f46(f46(f47(a11,a49),f26(a10,x6221,x6222,a49,a49)),f26(a10,x6223,x6222,a49,a49)))+~P15(f46(f46(f47(a11,a49),x6221),x6223)) % 0.47/0.65 [601]~E(f26(a10,f46(f46(a10,x6011),x6012),x6013,a49,a49),x6011)+E(f26(a10,f46(f46(a10,x6011),x6012),f17(x6013,f23(x6012,f3(a49),a49),a49),a49,a49),f46(f46(a10,x6011),x6012)) % 0.47/0.65 [624]P11(a11,x6241,f21(x6242,x6241,x6243),a49)+~P15(f46(f46(a11,f26(a10,f9(x6242),x6241,a49,a49)),x6243)) % 0.47/0.65 [625]E(f26(a10,f9(x6251),f21(x6251,x6252,x6253),a49,a49),x6253)+~P15(f46(f46(a11,f26(a10,f9(x6251),x6252,a49,a49)),x6253)) % 0.47/0.65 [468]E(x4681,x4682)+~E(f17(x4683,x4681,x4684),f17(x4683,x4682,x4684)) % 0.47/0.65 [471]E(x4711,x4712)+~E(f17(x4711,x4713,x4714),f17(x4712,x4713,x4714)) % 0.47/0.65 [487]P10(x4871,f23(x4872,x4873,x4874),x4874)+~P15(f46(x4871,x4872)) % 0.47/0.65 [500]~P10(x5001,x5003,x5004)+P10(x5001,f23(x5002,x5003,x5004),x5004) % 0.47/0.65 [515]P7(x5151,x5152,x5153)+~P7(x5151,f17(x5154,x5152,x5153),x5153) % 0.47/0.65 [516]P7(x5161,x5162,x5163)+~P7(x5161,f17(x5162,x5164,x5163),x5163) % 0.47/0.65 [530]~E(f28(x5303,x5301,x5302,x5304),f3(x5304))+E(x5301,f3(x5302)) % 0.47/0.65 [531]~E(f29(x5311,x5313,x5314,x5312),f3(x5312))+E(x5311,f3(x5312)) % 0.47/0.65 [430]E(x4301,x4302)+~E(f46(f46(a10,x4303),x4301),f46(f46(a10,x4304),x4302)) % 0.47/0.65 [431]E(x4311,x4312)+~E(f46(f46(a10,x4311),x4313),f46(f46(a10,x4312),x4314)) % 0.47/0.65 [482]P15(f46(x4821,x4823))+E(f22(x4821,f33(x4822,x4823,x4824),x4824),f3(x4824)) % 0.47/0.65 [498]P15(f46(x4981,x4982))+E(f22(x4981,f23(x4982,x4983,x4984),x4984),f22(x4981,x4983,x4984)) % 0.47/0.65 [499]P15(f46(x4992,x4991))+E(f34(x4991,f22(x4992,x4993,x4994),x4994),f22(x4992,x4993,x4994)) % 0.47/0.65 [511]~P15(f46(x5111,x5113))+E(f22(x5111,f33(x5112,x5113,x5114),x5114),f33(x5112,x5113,x5114)) % 0.47/0.65 [518]E(x5181,x5182)+E(f23(x5182,f34(x5181,x5183,x5184),x5184),f34(x5181,f23(x5182,x5183,x5184),x5184)) % 0.47/0.65 [519]~P4(x5194)+E(f19(x5191,f19(x5192,x5193,x5194),x5194),f19(x5192,f19(x5191,x5193,x5194),x5194)) % 0.47/0.65 [520]~P5(x5204)+E(f19(x5201,f19(x5202,x5203,x5204),x5204),f19(x5202,f19(x5201,x5203,x5204),x5204)) % 0.47/0.65 [521]~P4(x5213)+E(f19(f19(x5211,x5212,x5213),x5214,x5213),f19(x5211,f19(x5212,x5214,x5213),x5213)) % 0.47/0.65 [522]~P5(x5223)+E(f19(f19(x5221,x5222,x5223),x5224,x5223),f19(x5221,f19(x5222,x5224,x5223),x5223)) % 0.47/0.65 [526]~P15(f46(x5262,x5261))+E(f23(x5261,f22(x5262,x5263,x5264),x5264),f22(x5262,f23(x5261,x5263,x5264),x5264)) % 0.47/0.65 [561]~P15(f46(f46(a11,x5611),x5614))+P15(f46(f46(a11,f18(x5611,x5612,x5613)),f18(x5614,x5612,x5613))) % 0.47/0.65 [569]P15(f46(f46(f47(a11,a49),f18(x5691,x5692,x5693)),f18(x5691,x5694,x5693)))+~P15(f46(f46(a11,x5692),x5694)) % 0.47/0.65 [604]E(x6041,x6042)+~E(f26(a10,f9(x6043),x6041,a49,a49),f26(a10,f9(x6044),x6042,a49,a49)) % 0.47/0.65 [605]E(x6051,x6052)+~E(f26(a10,f12(x6053),x6051,a49,a49),f26(a10,f12(x6054),x6052,a49,a49)) % 0.47/0.65 [606]E(x6061,x6062)+~E(f26(a10,f9(x6061),x6063,a49,a49),f26(a10,f9(x6062),x6064,a49,a49)) % 0.47/0.65 [607]E(x6071,x6072)+~E(f26(a10,f12(x6071),x6073,a49,a49),f26(a10,f12(x6072),x6074,a49,a49)) % 0.47/0.65 [513]~E(f32(x5131,x5133),f23(x5134,x5132,x5133))+E(x5131,f17(f32(x5132,x5133),f23(x5134,f3(x5133),x5133),x5133)) % 0.47/0.65 [517]~P15(f46(f46(x5171,x5173),x5174))+P15(f46(f46(f47(x5171,x5172),x5173),x5174)) % 0.47/0.65 [546]P15(f46(x5461,x5462))+~P15(f46(f19(x5463,x5461,f52(x5464,a2)),x5462)) % 0.47/0.65 [547]P15(f46(x5471,x5472))+~P15(f46(f19(x5471,x5473,f52(x5474,a2)),x5472)) % 0.47/0.65 [575]P15(f46(f46(f47(a11,a49),f18(x5751,x5752,x5753)),f18(x5754,x5752,x5753)))+~P15(f46(f46(f47(a11,a49),x5751),x5754)) % 0.47/0.65 [576]P15(f46(f46(f47(a11,a49),f18(x5761,x5762,x5763)),f18(x5761,x5764,x5763)))+~P15(f46(f46(f47(a11,a49),x5762),x5764)) % 0.47/0.65 [467]E(x4671,x4672)+~E(f23(x4673,x4671,x4674),f23(x4675,x4672,x4674)) % 0.47/0.65 [469]E(x4691,x4692)+~E(f33(x4691,x4693,x4694),f33(x4692,x4695,x4694)) % 0.47/0.65 [470]E(x4701,x4702)+~E(f23(x4701,x4703,x4704),f23(x4702,x4705,x4704)) % 0.47/0.65 [484]~E(f22(x4841,x4843,x4844),f23(x4842,x4845,x4844))+P15(f46(x4841,x4842)) % 0.47/0.65 [564]~P11(x5641,x5643,x5645,x5644)+P11(x5641,f23(x5642,x5643,x5644),f23(x5642,x5645,x5644),x5644) % 0.47/0.65 [565]~P11(x5651,x5652,x5655,x5654)+P11(x5651,f17(x5652,x5653,x5654),f17(x5655,x5653,x5654),x5654) % 0.47/0.65 [566]~P11(x5661,x5663,x5665,x5664)+P11(x5661,f17(x5662,x5663,x5664),f17(x5662,x5665,x5664),x5664) % 0.47/0.65 [549]P11(x5491,f23(x5492,x5493,x5494),f23(x5495,x5493,x5494),x5494)+~P15(f46(f46(x5491,x5492),x5495)) % 0.47/0.65 [558]~E(f28(x5584,x5581,x5582,x5585),f28(x5584,x5583,x5582,x5585))+E(f38(x5581,f37(x5582)),f38(x5583,f37(x5582))) % 0.65/0.65 [573]~P8(x5734,f38(x5731,f37(x5733)),a1)+E(f29(f17(x5731,x5732,x5733),x5734,x5735,x5733),f17(f29(x5731,x5734,x5735,x5733),x5732,x5733)) % 0.65/0.65 [544]E(x5441,x5442)+~E(f17(x5443,f23(x5441,f3(x5444),x5444),x5444),f17(x5445,f23(x5442,f3(x5444),x5444),x5444)) % 0.65/0.65 [545]E(x5451,x5452)+~E(f17(x5451,f23(x5453,f3(x5454),x5454),x5454),f17(x5452,f23(x5455,f3(x5454),x5454),x5454)) % 0.65/0.65 [612]P15(f46(x6121,f46(x6122,x6123)))+~P15(f46(x6121,f15(x6124,x6125,x6122,f12(x6123),a50))) % 0.65/0.65 [614]P15(f46(x6141,f46(x6142,x6143)))+~P15(f46(x6141,f15(x6142,x6144,x6145,f9(x6143),a50))) % 0.65/0.65 [619]P15(f46(x6191,f46(f46(x6192,x6193),x6194)))+~P15(f46(x6191,f30(x6195,x6192,f23(x6193,x6194,a51),a50,a51))) % 0.65/0.65 [579]E(x5791,x5792)+E(f29(f29(x5793,x5791,x5794,x5795),x5792,x5796,x5795),f29(f29(x5793,x5792,x5796,x5795),x5791,x5794,x5795)) % 0.65/0.65 [590]~E(f38(x5902,f37(x5906)),f38(x5903,f37(x5905)))+E(f45(x5901,x5902,f17(x5903,x5904,x5905),x5906,x5905),f45(x5901,x5902,x5903,x5906,x5905)) % 0.65/0.65 [591]~E(f38(x5912,f37(x5914)),f38(x5915,f37(x5916)))+E(f45(x5911,f17(x5912,x5913,x5914),x5915,x5914,x5916),f45(x5911,x5912,x5915,x5914,x5916)) % 0.65/0.65 [617]P15(f46(x6171,f46(f46(x6172,x6173),x6174)))+~P15(f46(x6171,f15(x6175,x6172,x6176,f46(f46(a10,x6173),x6174),a50))) % 0.65/0.65 [423]E(x4231,x4232)+P8(x4232,x4231,a1)+P8(x4231,x4232,a1) % 0.65/0.65 [402]~P3(x4022)+~P12(x4021,x4022)+P12(f27(x4021,x4022),x4022) % 0.65/0.65 [457]~P8(x4571,x4572,a1)+E(f48(x4571),x4572)+P8(f48(x4571),x4572,a1) % 0.65/0.65 [458]E(x4581,x4582)+P8(x4582,x4581,a1)+~P8(x4582,f48(x4581),a1) % 0.65/0.65 [460]E(x4601,x4602)+P8(x4601,x4602,a1)+~P8(x4601,f48(x4602),a1) % 0.65/0.65 [465]~P7(x4652,x4651,a50)+P7(x4652,f67(x4652,x4651),a50)+E(x4651,f3(a50)) % 0.65/0.65 [441]P15(f46(x4411,x4412))+P15(f46(x4411,f55(x4411)))+~P15(f46(x4411,f3(a50))) % 0.65/0.65 [442]P15(f46(x4421,x4422))+P15(f46(x4421,f57(x4421)))+~P15(f46(x4421,f3(a50))) % 0.65/0.65 [443]P15(f46(x4431,x4432))+P15(f46(x4431,f58(x4431)))+~P15(f46(x4431,f3(a50))) % 0.65/0.65 [444]P15(f46(x4441,x4442))+P15(f46(x4441,f59(x4441)))+~P15(f46(x4441,f3(a50))) % 0.65/0.65 [445]P15(f46(x4451,x4452))+P15(f46(x4451,f60(x4451)))+~P15(f46(x4451,f3(a50))) % 0.65/0.65 [446]P15(f46(x4461,x4462))+P15(f46(x4461,f77(x4461)))+~P15(f46(x4461,f3(a50))) % 0.65/0.65 [447]P15(f46(x4471,x4472))+P15(f46(x4471,f65(x4471)))+~P15(f46(x4471,f3(a50))) % 0.65/0.65 [448]P15(f46(x4481,x4482))+P15(f46(x4481,f74(x4481)))+~P15(f46(x4481,f3(a50))) % 0.65/0.65 [449]P15(f46(x4491,x4492))+P15(f46(x4491,f61(x4491)))+~P15(f46(x4491,f3(a50))) % 0.65/0.65 [466]~P7(x4662,x4661,a50)+E(x4661,f3(a50))+P15(f46(x4662,f68(x4662,x4661))) % 0.65/0.65 [481]~P7(x4812,x4811,a50)+E(x4811,f3(a50))+E(f23(f68(x4812,x4811),f67(x4812,x4811),a50),x4811) % 0.65/0.65 [535]P15(f46(x5351,x5352))+~P15(f46(x5351,f3(a50)))+~P15(f46(x5351,f23(f56(x5351),f55(x5351),a50))) % 0.65/0.65 [536]P15(f46(x5361,x5362))+~P15(f46(x5361,f3(a50)))+~P15(f46(x5361,f23(f76(x5361),f57(x5361),a50))) % 0.65/0.65 [537]P15(f46(x5371,x5372))+~P15(f46(x5371,f3(a50)))+~P15(f46(x5371,f23(f73(x5371),f58(x5371),a50))) % 0.65/0.65 [538]P15(f46(x5381,x5382))+~P15(f46(x5381,f3(a50)))+~P15(f46(x5381,f23(f64(x5381),f59(x5381),a50))) % 0.65/0.65 [539]P15(f46(x5391,x5392))+~P15(f46(x5391,f3(a50)))+~P15(f46(x5391,f23(f63(x5391),f60(x5391),a50))) % 0.65/0.65 [540]P15(f46(x5401,x5402))+~P15(f46(x5401,f3(a50)))+~P15(f46(x5401,f23(f78(x5401),f77(x5401),a50))) % 0.65/0.65 [541]P15(f46(x5411,x5412))+~P15(f46(x5411,f3(a50)))+~P15(f46(x5411,f23(f66(x5411),f65(x5411),a50))) % 0.65/0.65 [542]P15(f46(x5421,x5422))+~P15(f46(x5421,f3(a50)))+~P15(f46(x5421,f23(f75(x5421),f74(x5421),a50))) % 0.65/0.65 [543]P15(f46(x5431,x5432))+~P15(f46(x5431,f3(a50)))+~P15(f46(x5431,f23(f62(x5431),f61(x5431),a50))) % 0.65/0.65 [477]~P8(x4773,x4772,x4771)+~P1(x4771)+~P8(x4772,x4773,x4771) % 0.65/0.65 [478]~P8(x4783,x4782,x4781)+~P2(x4781)+~P8(x4782,x4783,x4781) % 0.65/0.65 [479]~P8(x4793,x4792,x4791)+~P3(x4791)+~P8(x4792,x4793,x4791) % 0.65/0.65 [463]~P3(x4633)+~P12(x4632,x4633)+P12(f34(x4631,x4632,x4633),x4633) % 0.65/0.65 [488]~P3(x4882)+P12(x4881,x4882)+~P12(f23(x4883,x4881,x4882),x4882) % 0.65/0.65 [489]~P3(x4892)+P12(x4891,x4892)+~P12(f17(x4893,x4891,x4892),x4892) % 0.65/0.65 [490]~P3(x4902)+P12(x4901,x4902)+~P12(f17(x4901,x4903,x4902),x4902) % 0.65/0.65 [493]~P8(x4931,x4933,a1)+~P8(x4933,x4932,a1)+P8(f48(x4931),x4932,a1) % 0.65/0.65 [438]E(x4381,x4382)+P8(x4382,x4381,a1)+E(f18(f9(x4381),x4383,x4382),f9(x4381)) % 0.65/0.65 [620]~P15(f46(a8,x6202))+~P15(f46(a8,f26(a10,f18(x6201,x6202,f5(a1)),x6203,a49,a49)))+P15(f46(a8,f26(a10,f46(f46(a10,f12(x6201)),x6202),x6203,a49,a49))) % 0.65/0.65 [507]~P4(x5073)+~P8(x5072,x5074,x5073)+P8(f19(x5071,x5072,x5073),x5074,x5073) % 0.65/0.65 [508]~P4(x5083)+~P8(x5081,x5084,x5083)+P8(f19(x5081,x5082,x5083),x5084,x5083) % 0.65/0.65 [523]~P7(x5231,x5233,x5234)+~P7(x5231,x5232,x5234)+P7(x5231,f17(x5232,x5233,x5234),x5234) % 0.65/0.65 [524]P10(x5241,x5242,x5243)+~P10(x5241,f23(x5244,x5242,x5243),x5243)+P15(f46(x5241,x5244)) % 0.65/0.65 [510]P14(x5101,x5102,x5103)+~P14(x5101,x5104,x5103)+~P15(f46(f46(a11,x5104),x5102)) % 0.65/0.65 [527]~P7(x5272,x5274,x5273)+~P7(x5271,x5274,x5273)+P7(f19(x5271,x5272,f52(x5273,a2)),x5274,x5273) % 0.65/0.65 [602]E(x6021,f3(a49))+E(f26(a10,x6022,f20(x6023,x6024,x6022,x6021),a49,a49),x6023)+~E(f46(f46(a10,x6023),x6024),f26(a10,x6022,x6021,a49,a49)) % 0.65/0.65 [528]P14(x5281,x5282,x5283)+~P14(x5281,x5284,x5283)+~P15(f46(f46(f47(a11,a49),x5284),x5282)) % 0.65/0.65 [532]~P15(f46(x5322,x5324))+~P15(f46(x5321,x5324))+P15(f46(f19(x5321,x5322,f52(x5323,a2)),x5324)) % 0.65/0.65 [577]~P15(f46(f46(f47(a11,a49),x5771),x5773))+~P15(f46(f46(f47(a11,a49),x5772),x5774))+P15(f46(f46(f47(a11,a49),f46(f46(a10,x5771),x5772)),f46(f46(a10,x5773),x5774))) % 0.65/0.65 [592]E(x5921,f3(a49))+~E(f46(f46(a10,x5922),x5923),f26(a10,x5924,x5921,a49,a49))+E(f17(f20(x5922,x5923,x5924,x5921),f23(x5923,f3(a49),a49),a49),x5921) % 0.65/0.65 [473]E(x4731,x4732)+~E(f33(x4733,x4731,x4734),f33(x4735,x4732,x4734))+E(x4733,f5(a1)) % 0.65/0.65 [593]~E(f17(x5931,x5935,x5932),f23(x5933,x5934,x5932))+E(x5931,f3(x5932))+E(f23(x5933,f44(x5933,x5934,x5931,x5935,x5932),x5932),x5931) % 0.65/0.65 [594]~E(f17(x5941,x5945,x5942),f23(x5943,x5944,x5942))+E(x5941,f3(x5942))+E(f17(f42(x5943,x5944,x5941,x5945,x5942),x5945,x5942),x5944) % 0.65/0.65 [595]~E(f17(x5951,x5955,x5952),f23(x5953,x5954,x5952))+E(x5951,f3(x5952))+E(f23(x5953,f42(x5953,x5954,x5951,x5955,x5952),x5952),x5951) % 0.65/0.65 [596]~E(f17(x5961,x5965,x5962),f23(x5963,x5964,x5962))+E(x5961,f3(x5962))+E(f17(f44(x5963,x5964,x5961,x5965,x5962),x5965,x5962),x5964) % 0.65/0.65 [597]~E(f17(x5975,x5971,x5974),f23(x5972,x5973,x5974))+E(x5971,f23(x5972,x5973,x5974))+E(f23(x5972,f44(x5972,x5973,x5975,x5971,x5974),x5974),x5975) % 0.65/0.65 [598]~E(f17(x5985,x5981,x5984),f23(x5982,x5983,x5984))+E(x5981,f23(x5982,x5983,x5984))+E(f17(f44(x5982,x5983,x5985,x5981,x5984),x5981,x5984),x5983) % 0.65/0.65 [599]~E(f17(x5995,x5994,x5993),f23(x5991,x5992,x5993))+E(f23(x5991,x5992,x5993),x5994)+E(f17(f42(x5991,x5992,x5995,x5994,x5993),x5994,x5993),x5992) % 0.65/0.65 [600]~E(f17(x6005,x6004,x6003),f23(x6001,x6002,x6003))+E(f23(x6001,x6002,x6003),x6004)+E(f23(x6001,f42(x6001,x6002,x6005,x6004,x6003),x6003),x6005) % 0.65/0.65 [615]E(x6151,x6152)+~P14(x6153,f26(a10,f9(x6154),x6155,a49,a49),x6151)+~P14(x6153,f26(a10,f9(x6154),x6155,a49,a49),x6152) % 0.65/0.65 [550]~P15(f46(f46(x5501,x5505),x5504))+~P15(f46(f46(f47(x5501,x5502),x5503),x5505))+P15(f46(f46(f47(x5501,x5502),x5503),x5504)) % 0.65/0.65 [551]~P15(f46(f46(x5511,x5513),x5515))+~P15(f46(f46(f47(x5511,x5512),x5515),x5514))+P15(f46(f46(f47(x5511,x5512),x5513),x5514)) % 0.65/0.65 [556]~P15(f46(f46(f47(x5561,x5562),x5563),x5565))+P15(f46(f46(f47(x5561,x5562),x5563),x5564))+~P15(f46(f46(f47(x5561,x5562),x5565),x5564)) % 0.65/0.65 [559]~P15(f46(x5591,x5593))+E(f22(x5591,f17(x5592,f23(x5593,x5594,x5595),x5595),x5595),f23(x5593,f22(x5591,x5594,x5595),x5595))+P15(f46(x5591,f41(x5591,x5592,x5595))) % 0.65/0.65 [560]~P15(f46(x5601,x5603))+E(f22(x5601,f17(x5602,f23(x5603,x5604,x5605),x5605),x5605),f23(x5603,f22(x5601,x5604,x5605),x5605))+P15(f46(x5601,f43(x5601,x5602,x5605))) % 0.65/0.65 [555]E(x5551,x5552)+E(x5553,x5554)+~P11(x5555,f23(x5554,x5552,x5556),f23(x5553,x5551,x5556),x5556) % 0.65/0.65 [570]E(x5701,x5702)+P11(x5703,x5701,x5702,x5704)+~P11(x5703,f23(x5705,x5701,x5704),f23(x5706,x5702,x5704),x5704) % 0.65/0.65 [557]E(x5571,x5572)+~P11(x5573,f23(x5572,x5574,x5575),f23(x5571,x5576,x5575),x5575)+P15(f46(f46(x5573,x5572),x5571)) % 0.65/0.65 [571]~P9(x5711,x5713,x5716,x5714)+P9(x5711,f23(x5712,x5713,x5714),f23(x5715,x5716,x5714),x5714)+~P15(f46(f46(x5711,x5712),x5715)) % 0.65/0.65 [574]P11(x5741,x5742,x5743,x5744)+~P11(x5741,f23(x5745,x5742,x5744),f23(x5746,x5743,x5744),x5744)+P15(f46(f46(x5741,x5745),x5746)) % 0.65/0.65 [578]E(x5781,x5782)+E(x5783,x5784)+~P11(x5785,f17(x5783,f23(x5781,f3(x5786),x5786),x5786),f17(x5784,f23(x5782,f3(x5786),x5786),x5786),x5786) % 0.65/0.65 [580]E(x5801,x5802)+~P11(x5803,f17(x5804,f23(x5801,f3(x5805),x5805),x5805),f17(x5806,f23(x5802,f3(x5805),x5805),x5805),x5805)+P15(f46(f46(x5803,x5801),x5802)) % 0.65/0.65 [581]E(x5811,x5812)+P11(x5813,x5811,x5812,x5814)+~P11(x5813,f17(x5811,f23(x5815,f3(x5814),x5814),x5814),f17(x5812,f23(x5816,f3(x5814),x5814),x5814),x5814) % 0.65/0.65 [582]P11(x5821,x5822,x5823,x5824)+~P11(x5821,f17(x5822,f23(x5825,f3(x5824),x5824),x5824),f17(x5823,f23(x5826,f3(x5824),x5824),x5824),x5824)+P15(f46(f46(x5821,x5825),x5826)) % 0.65/0.65 [435]P8(x4351,x4352,x4353)+~P3(x4353)+E(x4351,x4352)+P8(x4352,x4351,x4353) % 0.65/0.65 [436]P8(x4361,x4362,x4363)+~P16(x4363)+E(x4361,x4362)+P8(x4362,x4361,x4363) % 0.65/0.65 [501]~P7(x5013,x5012,a50)+P7(x5013,f69(x5013,x5011),a50)+P15(f46(x5011,x5012))+~P15(f46(x5011,f3(a50))) % 0.65/0.65 [502]~P7(x5023,x5022,a50)+P7(x5023,f70(x5023,x5021),a50)+P15(f46(x5021,x5022))+~P15(f46(x5021,f3(a50))) % 0.65/0.65 [503]~P7(x5033,x5032,a50)+P15(f46(x5031,x5032))+P15(f46(x5033,f72(x5033,x5031)))+~P15(f46(x5031,f3(a50))) % 0.65/0.65 [504]~P7(x5043,x5042,a50)+P15(f46(x5041,x5042))+P15(f46(x5043,f71(x5043,x5041)))+~P15(f46(x5041,f3(a50))) % 0.65/0.65 [505]~P7(x5053,x5052,a50)+P15(f46(x5051,x5052))+P15(f46(x5051,f69(x5053,x5051)))+~P15(f46(x5051,f3(a50))) % 0.65/0.65 [506]~P7(x5063,x5062,a50)+P15(f46(x5061,x5062))+P15(f46(x5061,f70(x5063,x5061)))+~P15(f46(x5061,f3(a50))) % 0.65/0.65 [567]~P7(x5673,x5672,a50)+P15(f46(x5671,x5672))+~P15(f46(x5671,f3(a50)))+~P15(f46(x5671,f23(f72(x5673,x5671),f69(x5673,x5671),a50))) % 0.65/0.65 [568]~P7(x5683,x5682,a50)+P15(f46(x5681,x5682))+~P15(f46(x5681,f3(a50)))+~P15(f46(x5681,f23(f71(x5683,x5681),f70(x5683,x5681),a50))) % 0.65/0.65 [496]~P1(x4963)+~P8(x4961,x4964,x4963)+P8(x4961,x4962,x4963)+~P8(x4964,x4962,x4963) % 0.65/0.65 [497]~P2(x4973)+~P8(x4971,x4974,x4973)+P8(x4971,x4972,x4973)+~P8(x4974,x4972,x4973) % 0.65/0.65 %EqnAxiom % 0.65/0.65 [1]E(x11,x11) % 0.65/0.65 [2]E(x22,x21)+~E(x21,x22) % 0.65/0.65 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.65/0.65 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.65/0.65 [5]~E(x51,x52)+E(f46(x51,x53),f46(x52,x53)) % 0.65/0.65 [6]~E(x61,x62)+E(f46(x63,x61),f46(x63,x62)) % 0.65/0.65 [7]~E(x71,x72)+E(f27(x71,x73),f27(x72,x73)) % 0.65/0.65 [8]~E(x81,x82)+E(f27(x83,x81),f27(x83,x82)) % 0.65/0.65 [9]~E(x91,x92)+E(f38(x91,x93),f38(x92,x93)) % 0.65/0.65 [10]~E(x101,x102)+E(f38(x103,x101),f38(x103,x102)) % 0.65/0.65 [11]~E(x111,x112)+E(f26(x111,x113,x114,x115,x116),f26(x112,x113,x114,x115,x116)) % 0.65/0.65 [12]~E(x121,x122)+E(f26(x123,x121,x124,x125,x126),f26(x123,x122,x124,x125,x126)) % 0.65/0.65 [13]~E(x131,x132)+E(f26(x133,x134,x131,x135,x136),f26(x133,x134,x132,x135,x136)) % 0.65/0.65 [14]~E(x141,x142)+E(f26(x143,x144,x145,x141,x146),f26(x143,x144,x145,x142,x146)) % 0.65/0.65 [15]~E(x151,x152)+E(f26(x153,x154,x155,x156,x151),f26(x153,x154,x155,x156,x152)) % 0.65/0.65 [16]~E(x161,x162)+E(f32(x161,x163),f32(x162,x163)) % 0.65/0.65 [17]~E(x171,x172)+E(f32(x173,x171),f32(x173,x172)) % 0.65/0.65 [18]~E(x181,x182)+E(f9(x181),f9(x182)) % 0.65/0.65 [19]~E(x191,x192)+E(f13(x191,x193,x194),f13(x192,x193,x194)) % 0.65/0.65 [20]~E(x201,x202)+E(f13(x203,x201,x204),f13(x203,x202,x204)) % 0.65/0.65 [21]~E(x211,x212)+E(f13(x213,x214,x211),f13(x213,x214,x212)) % 0.65/0.65 [22]~E(x221,x222)+E(f19(x221,x223,x224),f19(x222,x223,x224)) % 0.65/0.65 [23]~E(x231,x232)+E(f19(x233,x231,x234),f19(x233,x232,x234)) % 0.65/0.65 [24]~E(x241,x242)+E(f19(x243,x244,x241),f19(x243,x244,x242)) % 0.65/0.65 [25]~E(x251,x252)+E(f21(x251,x253,x254),f21(x252,x253,x254)) % 0.65/0.65 [26]~E(x261,x262)+E(f21(x263,x261,x264),f21(x263,x262,x264)) % 0.65/0.65 [27]~E(x271,x272)+E(f21(x273,x274,x271),f21(x273,x274,x272)) % 0.65/0.65 [28]~E(x281,x282)+E(f22(x281,x283,x284),f22(x282,x283,x284)) % 0.65/0.65 [29]~E(x291,x292)+E(f22(x293,x291,x294),f22(x293,x292,x294)) % 0.65/0.65 [30]~E(x301,x302)+E(f22(x303,x304,x301),f22(x303,x304,x302)) % 0.65/0.65 [31]~E(x311,x312)+E(f35(x311,x313),f35(x312,x313)) % 0.65/0.65 [32]~E(x321,x322)+E(f35(x323,x321),f35(x323,x322)) % 0.65/0.65 [33]~E(x331,x332)+E(f37(x331),f37(x332)) % 0.65/0.65 [34]~E(x341,x342)+E(f20(x341,x343,x344,x345),f20(x342,x343,x344,x345)) % 0.65/0.65 [35]~E(x351,x352)+E(f20(x353,x351,x354,x355),f20(x353,x352,x354,x355)) % 0.65/0.65 [36]~E(x361,x362)+E(f20(x363,x364,x361,x365),f20(x363,x364,x362,x365)) % 0.65/0.65 [37]~E(x371,x372)+E(f20(x373,x374,x375,x371),f20(x373,x374,x375,x372)) % 0.65/0.65 [38]~E(x381,x382)+E(f4(x381,x383),f4(x382,x383)) % 0.65/0.65 [39]~E(x391,x392)+E(f4(x393,x391),f4(x393,x392)) % 0.65/0.65 [40]~E(x401,x402)+E(f5(x401),f5(x402)) % 0.65/0.65 [41]~E(x411,x412)+E(f33(x411,x413,x414),f33(x412,x413,x414)) % 0.65/0.65 [42]~E(x421,x422)+E(f33(x423,x421,x424),f33(x423,x422,x424)) % 0.65/0.65 [43]~E(x431,x432)+E(f33(x433,x434,x431),f33(x433,x434,x432)) % 0.65/0.65 [44]~E(x441,x442)+E(f23(x441,x443,x444),f23(x442,x443,x444)) % 0.65/0.65 [45]~E(x451,x452)+E(f23(x453,x451,x454),f23(x453,x452,x454)) % 0.65/0.65 [46]~E(x461,x462)+E(f23(x463,x464,x461),f23(x463,x464,x462)) % 0.65/0.65 [47]~E(x471,x472)+E(f17(x471,x473,x474),f17(x472,x473,x474)) % 0.65/0.65 [48]~E(x481,x482)+E(f17(x483,x481,x484),f17(x483,x482,x484)) % 0.65/0.65 [49]~E(x491,x492)+E(f17(x493,x494,x491),f17(x493,x494,x492)) % 0.65/0.65 [50]~E(x501,x502)+E(f14(x501,x503),f14(x502,x503)) % 0.65/0.65 [51]~E(x511,x512)+E(f14(x513,x511),f14(x513,x512)) % 0.65/0.65 [52]~E(x521,x522)+E(f7(x521,x523,x524,x525,x526),f7(x522,x523,x524,x525,x526)) % 0.65/0.65 [53]~E(x531,x532)+E(f7(x533,x531,x534,x535,x536),f7(x533,x532,x534,x535,x536)) % 0.65/0.65 [54]~E(x541,x542)+E(f7(x543,x544,x541,x545,x546),f7(x543,x544,x542,x545,x546)) % 0.65/0.65 [55]~E(x551,x552)+E(f7(x553,x554,x555,x551,x556),f7(x553,x554,x555,x552,x556)) % 0.65/0.65 [56]~E(x561,x562)+E(f7(x563,x564,x565,x566,x561),f7(x563,x564,x565,x566,x562)) % 0.65/0.65 [57]~E(x571,x572)+E(f24(x571,x573),f24(x572,x573)) % 0.65/0.65 [58]~E(x581,x582)+E(f24(x583,x581),f24(x583,x582)) % 0.65/0.65 [59]~E(x591,x592)+E(f12(x591),f12(x592)) % 0.65/0.65 [60]~E(x601,x602)+E(f36(x601,x603,x604),f36(x602,x603,x604)) % 0.65/0.65 [61]~E(x611,x612)+E(f36(x613,x611,x614),f36(x613,x612,x614)) % 0.65/0.65 [62]~E(x621,x622)+E(f36(x623,x624,x621),f36(x623,x624,x622)) % 0.65/0.65 [63]~E(x631,x632)+E(f45(x631,x633,x634,x635,x636),f45(x632,x633,x634,x635,x636)) % 0.65/0.65 [64]~E(x641,x642)+E(f45(x643,x641,x644,x645,x646),f45(x643,x642,x644,x645,x646)) % 0.65/0.65 [65]~E(x651,x652)+E(f45(x653,x654,x651,x655,x656),f45(x653,x654,x652,x655,x656)) % 0.65/0.65 [66]~E(x661,x662)+E(f45(x663,x664,x665,x661,x666),f45(x663,x664,x665,x662,x666)) % 0.65/0.65 [67]~E(x671,x672)+E(f45(x673,x674,x675,x676,x671),f45(x673,x674,x675,x676,x672)) % 0.65/0.65 [68]~E(x681,x682)+E(f67(x681,x683),f67(x682,x683)) % 0.65/0.65 [69]~E(x691,x692)+E(f67(x693,x691),f67(x693,x692)) % 0.65/0.65 [70]~E(x701,x702)+E(f47(x701,x703),f47(x702,x703)) % 0.65/0.65 [71]~E(x711,x712)+E(f47(x713,x711),f47(x713,x712)) % 0.65/0.65 [72]~E(x721,x722)+E(f56(x721),f56(x722)) % 0.65/0.65 [73]~E(x731,x732)+E(f55(x731),f55(x732)) % 0.65/0.65 [74]~E(x741,x742)+E(f28(x741,x743,x744,x745),f28(x742,x743,x744,x745)) % 0.65/0.65 [75]~E(x751,x752)+E(f28(x753,x751,x754,x755),f28(x753,x752,x754,x755)) % 0.65/0.65 [76]~E(x761,x762)+E(f28(x763,x764,x761,x765),f28(x763,x764,x762,x765)) % 0.65/0.65 [77]~E(x771,x772)+E(f28(x773,x774,x775,x771),f28(x773,x774,x775,x772)) % 0.65/0.65 [78]~E(x781,x782)+E(f15(x781,x783,x784,x785,x786),f15(x782,x783,x784,x785,x786)) % 0.65/0.65 [79]~E(x791,x792)+E(f15(x793,x791,x794,x795,x796),f15(x793,x792,x794,x795,x796)) % 0.65/0.65 [80]~E(x801,x802)+E(f15(x803,x804,x801,x805,x806),f15(x803,x804,x802,x805,x806)) % 0.65/0.65 [81]~E(x811,x812)+E(f15(x813,x814,x815,x811,x816),f15(x813,x814,x815,x812,x816)) % 0.65/0.65 [82]~E(x821,x822)+E(f15(x823,x824,x825,x826,x821),f15(x823,x824,x825,x826,x822)) % 0.65/0.65 [83]~E(x831,x832)+E(f29(x831,x833,x834,x835),f29(x832,x833,x834,x835)) % 0.65/0.65 [84]~E(x841,x842)+E(f29(x843,x841,x844,x845),f29(x843,x842,x844,x845)) % 0.65/0.65 [85]~E(x851,x852)+E(f29(x853,x854,x851,x855),f29(x853,x854,x852,x855)) % 0.65/0.65 [86]~E(x861,x862)+E(f29(x863,x864,x865,x861),f29(x863,x864,x865,x862)) % 0.65/0.65 [87]~E(x871,x872)+E(f6(x871,x873,x874,x875),f6(x872,x873,x874,x875)) % 0.65/0.65 [88]~E(x881,x882)+E(f6(x883,x881,x884,x885),f6(x883,x882,x884,x885)) % 0.65/0.65 [89]~E(x891,x892)+E(f6(x893,x894,x891,x895),f6(x893,x894,x892,x895)) % 0.65/0.65 [90]~E(x901,x902)+E(f6(x903,x904,x905,x901),f6(x903,x904,x905,x902)) % 0.65/0.65 [91]~E(x911,x912)+E(f48(x911),f48(x912)) % 0.65/0.65 [92]~E(x921,x922)+E(f30(x921,x923,x924,x925,x926),f30(x922,x923,x924,x925,x926)) % 0.65/0.65 [93]~E(x931,x932)+E(f30(x933,x931,x934,x935,x936),f30(x933,x932,x934,x935,x936)) % 0.65/0.65 [94]~E(x941,x942)+E(f30(x943,x944,x941,x945,x946),f30(x943,x944,x942,x945,x946)) % 0.65/0.65 [95]~E(x951,x952)+E(f30(x953,x954,x955,x951,x956),f30(x953,x954,x955,x952,x956)) % 0.65/0.65 [96]~E(x961,x962)+E(f30(x963,x964,x965,x966,x961),f30(x963,x964,x965,x966,x962)) % 0.65/0.65 [97]~E(x971,x972)+E(f18(x971,x973,x974),f18(x972,x973,x974)) % 0.65/0.65 [98]~E(x981,x982)+E(f18(x983,x981,x984),f18(x983,x982,x984)) % 0.65/0.65 [99]~E(x991,x992)+E(f18(x993,x994,x991),f18(x993,x994,x992)) % 0.65/0.65 [100]~E(x1001,x1002)+E(f42(x1001,x1003,x1004,x1005,x1006),f42(x1002,x1003,x1004,x1005,x1006)) % 0.65/0.65 [101]~E(x1011,x1012)+E(f42(x1013,x1011,x1014,x1015,x1016),f42(x1013,x1012,x1014,x1015,x1016)) % 0.65/0.65 [102]~E(x1021,x1022)+E(f42(x1023,x1024,x1021,x1025,x1026),f42(x1023,x1024,x1022,x1025,x1026)) % 0.65/0.65 [103]~E(x1031,x1032)+E(f42(x1033,x1034,x1035,x1031,x1036),f42(x1033,x1034,x1035,x1032,x1036)) % 0.65/0.65 [104]~E(x1041,x1042)+E(f42(x1043,x1044,x1045,x1046,x1041),f42(x1043,x1044,x1045,x1046,x1042)) % 0.65/0.65 [105]~E(x1051,x1052)+E(f52(x1051,x1053),f52(x1052,x1053)) % 0.65/0.65 [106]~E(x1061,x1062)+E(f52(x1063,x1061),f52(x1063,x1062)) % 0.65/0.65 [107]~E(x1071,x1072)+E(f16(x1071,x1073,x1074,x1075,x1076),f16(x1072,x1073,x1074,x1075,x1076)) % 0.65/0.65 [108]~E(x1081,x1082)+E(f16(x1083,x1081,x1084,x1085,x1086),f16(x1083,x1082,x1084,x1085,x1086)) % 0.65/0.65 [109]~E(x1091,x1092)+E(f16(x1093,x1094,x1091,x1095,x1096),f16(x1093,x1094,x1092,x1095,x1096)) % 0.65/0.65 [110]~E(x1101,x1102)+E(f16(x1103,x1104,x1105,x1101,x1106),f16(x1103,x1104,x1105,x1102,x1106)) % 0.65/0.65 [111]~E(x1111,x1112)+E(f16(x1113,x1114,x1115,x1116,x1111),f16(x1113,x1114,x1115,x1116,x1112)) % 0.65/0.65 [112]~E(x1121,x1122)+E(f25(x1121,x1123,x1124,x1125),f25(x1122,x1123,x1124,x1125)) % 0.65/0.65 [113]~E(x1131,x1132)+E(f25(x1133,x1131,x1134,x1135),f25(x1133,x1132,x1134,x1135)) % 0.65/0.65 [114]~E(x1141,x1142)+E(f25(x1143,x1144,x1141,x1145),f25(x1143,x1144,x1142,x1145)) % 0.65/0.66 [115]~E(x1151,x1152)+E(f25(x1153,x1154,x1155,x1151),f25(x1153,x1154,x1155,x1152)) % 0.65/0.66 [116]~E(x1161,x1162)+E(f34(x1161,x1163,x1164),f34(x1162,x1163,x1164)) % 0.65/0.66 [117]~E(x1171,x1172)+E(f34(x1173,x1171,x1174),f34(x1173,x1172,x1174)) % 0.65/0.66 [118]~E(x1181,x1182)+E(f34(x1183,x1184,x1181),f34(x1183,x1184,x1182)) % 0.65/0.66 [119]~E(x1191,x1192)+E(f44(x1191,x1193,x1194,x1195,x1196),f44(x1192,x1193,x1194,x1195,x1196)) % 0.65/0.66 [120]~E(x1201,x1202)+E(f44(x1203,x1201,x1204,x1205,x1206),f44(x1203,x1202,x1204,x1205,x1206)) % 0.65/0.66 [121]~E(x1211,x1212)+E(f44(x1213,x1214,x1211,x1215,x1216),f44(x1213,x1214,x1212,x1215,x1216)) % 0.65/0.66 [122]~E(x1221,x1222)+E(f44(x1223,x1224,x1225,x1221,x1226),f44(x1223,x1224,x1225,x1222,x1226)) % 0.65/0.66 [123]~E(x1231,x1232)+E(f44(x1233,x1234,x1235,x1236,x1231),f44(x1233,x1234,x1235,x1236,x1232)) % 0.65/0.66 [124]~E(x1241,x1242)+E(f31(x1241,x1243,x1244,x1245,x1246),f31(x1242,x1243,x1244,x1245,x1246)) % 0.65/0.66 [125]~E(x1251,x1252)+E(f31(x1253,x1251,x1254,x1255,x1256),f31(x1253,x1252,x1254,x1255,x1256)) % 0.65/0.66 [126]~E(x1261,x1262)+E(f31(x1263,x1264,x1261,x1265,x1266),f31(x1263,x1264,x1262,x1265,x1266)) % 0.65/0.66 [127]~E(x1271,x1272)+E(f31(x1273,x1274,x1275,x1271,x1276),f31(x1273,x1274,x1275,x1272,x1276)) % 0.65/0.66 [128]~E(x1281,x1282)+E(f31(x1283,x1284,x1285,x1286,x1281),f31(x1283,x1284,x1285,x1286,x1282)) % 0.65/0.66 [129]~E(x1291,x1292)+E(f59(x1291),f59(x1292)) % 0.65/0.66 [130]~E(x1301,x1302)+E(f70(x1301,x1303),f70(x1302,x1303)) % 0.65/0.66 [131]~E(x1311,x1312)+E(f70(x1313,x1311),f70(x1313,x1312)) % 0.65/0.66 [132]~E(x1321,x1322)+E(f57(x1321),f57(x1322)) % 0.65/0.66 [133]~E(x1331,x1332)+E(f58(x1331),f58(x1332)) % 0.65/0.66 [134]~E(x1341,x1342)+E(f77(x1341),f77(x1342)) % 0.65/0.66 [135]~E(x1351,x1352)+E(f71(x1351,x1353),f71(x1352,x1353)) % 0.65/0.66 [136]~E(x1361,x1362)+E(f71(x1363,x1361),f71(x1363,x1362)) % 0.65/0.66 [137]~E(x1371,x1372)+E(f68(x1371,x1373),f68(x1372,x1373)) % 0.65/0.66 [138]~E(x1381,x1382)+E(f68(x1383,x1381),f68(x1383,x1382)) % 0.65/0.66 [139]~E(x1391,x1392)+E(f60(x1391),f60(x1392)) % 0.65/0.66 [140]~E(x1401,x1402)+E(f62(x1401),f62(x1402)) % 0.65/0.66 [141]~E(x1411,x1412)+E(f61(x1411),f61(x1412)) % 0.65/0.66 [142]~E(x1421,x1422)+E(f73(x1421),f73(x1422)) % 0.65/0.66 [143]~E(x1431,x1432)+E(f69(x1431,x1433),f69(x1432,x1433)) % 0.65/0.66 [144]~E(x1441,x1442)+E(f69(x1443,x1441),f69(x1443,x1442)) % 0.65/0.66 [145]~E(x1451,x1452)+E(f74(x1451),f74(x1452)) % 0.65/0.66 [146]~E(x1461,x1462)+E(f72(x1461,x1463),f72(x1462,x1463)) % 0.65/0.66 [147]~E(x1471,x1472)+E(f72(x1473,x1471),f72(x1473,x1472)) % 0.65/0.66 [148]~E(x1481,x1482)+E(f66(x1481),f66(x1482)) % 0.65/0.66 [149]~E(x1491,x1492)+E(f78(x1491),f78(x1492)) % 0.65/0.66 [150]~E(x1501,x1502)+E(f39(x1501,x1503,x1504),f39(x1502,x1503,x1504)) % 0.65/0.66 [151]~E(x1511,x1512)+E(f39(x1513,x1511,x1514),f39(x1513,x1512,x1514)) % 0.65/0.66 [152]~E(x1521,x1522)+E(f39(x1523,x1524,x1521),f39(x1523,x1524,x1522)) % 0.65/0.66 [153]~E(x1531,x1532)+E(f43(x1531,x1533,x1534),f43(x1532,x1533,x1534)) % 0.65/0.66 [154]~E(x1541,x1542)+E(f43(x1543,x1541,x1544),f43(x1543,x1542,x1544)) % 0.65/0.66 [155]~E(x1551,x1552)+E(f43(x1553,x1554,x1551),f43(x1553,x1554,x1552)) % 0.65/0.66 [156]~E(x1561,x1562)+E(f63(x1561),f63(x1562)) % 0.65/0.66 [157]~E(x1571,x1572)+E(f40(x1571,x1573,x1574),f40(x1572,x1573,x1574)) % 0.65/0.66 [158]~E(x1581,x1582)+E(f40(x1583,x1581,x1584),f40(x1583,x1582,x1584)) % 0.65/0.66 [159]~E(x1591,x1592)+E(f40(x1593,x1594,x1591),f40(x1593,x1594,x1592)) % 0.65/0.66 [160]~E(x1601,x1602)+E(f41(x1601,x1603,x1604),f41(x1602,x1603,x1604)) % 0.65/0.66 [161]~E(x1611,x1612)+E(f41(x1613,x1611,x1614),f41(x1613,x1612,x1614)) % 0.65/0.66 [162]~E(x1621,x1622)+E(f41(x1623,x1624,x1621),f41(x1623,x1624,x1622)) % 0.65/0.66 [163]~E(x1631,x1632)+E(f76(x1631),f76(x1632)) % 0.65/0.66 [164]~E(x1641,x1642)+E(f75(x1641),f75(x1642)) % 0.65/0.66 [165]~E(x1651,x1652)+E(f64(x1651),f64(x1652)) % 0.65/0.66 [166]~E(x1661,x1662)+E(f65(x1661),f65(x1662)) % 0.65/0.66 [167]~P1(x1671)+P1(x1672)+~E(x1671,x1672) % 0.65/0.66 [168]~P15(x1681)+P15(x1682)+~E(x1681,x1682) % 0.65/0.66 [169]~P2(x1691)+P2(x1692)+~E(x1691,x1692) % 0.65/0.66 [170]P7(x1702,x1703,x1704)+~E(x1701,x1702)+~P7(x1701,x1703,x1704) % 0.65/0.66 [171]P7(x1713,x1712,x1714)+~E(x1711,x1712)+~P7(x1713,x1711,x1714) % 0.65/0.66 [172]P7(x1723,x1724,x1722)+~E(x1721,x1722)+~P7(x1723,x1724,x1721) % 0.65/0.66 [173]~P3(x1731)+P3(x1732)+~E(x1731,x1732) % 0.65/0.66 [174]~P4(x1741)+P4(x1742)+~E(x1741,x1742) % 0.65/0.66 [175]~P5(x1751)+P5(x1752)+~E(x1751,x1752) % 0.65/0.66 [176]P8(x1762,x1763,x1764)+~E(x1761,x1762)+~P8(x1761,x1763,x1764) % 0.65/0.66 [177]P8(x1773,x1772,x1774)+~E(x1771,x1772)+~P8(x1773,x1771,x1774) % 0.65/0.66 [178]P8(x1783,x1784,x1782)+~E(x1781,x1782)+~P8(x1783,x1784,x1781) % 0.65/0.66 [179]P10(x1792,x1793,x1794)+~E(x1791,x1792)+~P10(x1791,x1793,x1794) % 0.65/0.66 [180]P10(x1803,x1802,x1804)+~E(x1801,x1802)+~P10(x1803,x1801,x1804) % 0.65/0.66 [181]P10(x1813,x1814,x1812)+~E(x1811,x1812)+~P10(x1813,x1814,x1811) % 0.65/0.66 [182]P6(x1822,x1823)+~E(x1821,x1822)+~P6(x1821,x1823) % 0.65/0.66 [183]P6(x1833,x1832)+~E(x1831,x1832)+~P6(x1833,x1831) % 0.65/0.66 [184]P14(x1842,x1843,x1844)+~E(x1841,x1842)+~P14(x1841,x1843,x1844) % 0.65/0.66 [185]P14(x1853,x1852,x1854)+~E(x1851,x1852)+~P14(x1853,x1851,x1854) % 0.65/0.66 [186]P14(x1863,x1864,x1862)+~E(x1861,x1862)+~P14(x1863,x1864,x1861) % 0.65/0.66 [187]P12(x1872,x1873)+~E(x1871,x1872)+~P12(x1871,x1873) % 0.65/0.66 [188]P12(x1883,x1882)+~E(x1881,x1882)+~P12(x1883,x1881) % 0.65/0.66 [189]P13(x1892,x1893,x1894)+~E(x1891,x1892)+~P13(x1891,x1893,x1894) % 0.65/0.66 [190]P13(x1903,x1902,x1904)+~E(x1901,x1902)+~P13(x1903,x1901,x1904) % 0.65/0.66 [191]P13(x1913,x1914,x1912)+~E(x1911,x1912)+~P13(x1913,x1914,x1911) % 0.65/0.66 [192]P11(x1922,x1923,x1924,x1925)+~E(x1921,x1922)+~P11(x1921,x1923,x1924,x1925) % 0.65/0.66 [193]P11(x1933,x1932,x1934,x1935)+~E(x1931,x1932)+~P11(x1933,x1931,x1934,x1935) % 0.65/0.66 [194]P11(x1943,x1944,x1942,x1945)+~E(x1941,x1942)+~P11(x1943,x1944,x1941,x1945) % 0.65/0.66 [195]P11(x1953,x1954,x1955,x1952)+~E(x1951,x1952)+~P11(x1953,x1954,x1955,x1951) % 0.65/0.66 [196]P9(x1962,x1963,x1964,x1965)+~E(x1961,x1962)+~P9(x1961,x1963,x1964,x1965) % 0.65/0.66 [197]P9(x1973,x1972,x1974,x1975)+~E(x1971,x1972)+~P9(x1973,x1971,x1974,x1975) % 0.65/0.66 [198]P9(x1983,x1984,x1982,x1985)+~E(x1981,x1982)+~P9(x1983,x1984,x1981,x1985) % 0.65/0.66 [199]P9(x1993,x1994,x1995,x1992)+~E(x1991,x1992)+~P9(x1993,x1994,x1995,x1991) % 0.65/0.66 [200]~P16(x2001)+P16(x2002)+~E(x2001,x2002) % 0.65/0.66 % 0.65/0.66 %------------------------------------------- % 0.65/0.66 cnf(648,plain, % 0.65/0.66 ($false), % 0.65/0.66 inference(scs_inference,[],[366,228]), % 0.65/0.66 ['proof']). % 0.65/0.66 % SZS output end Proof % 0.65/0.66 % Total time :0.046789s %------------------------------------------------------------------------------