%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL821-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 : n020.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:55 AM UTC 2026 % Result : Unsatisfiable 0.49s 0.66s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL821-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.07/0.34 % Computer : n020.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Fri Sep 4 20:49:42 UTC 2026 % 0.07/0.34 % CPUTime : % 0.24/0.50 start to proof:theBenchmark % 0.39/0.61 %------------------------------------------- % 0.39/0.61 % File :CSE---1.7 % 0.39/0.61 % Problem :theBenchmark % 0.39/0.61 % Transform :cnf % 0.39/0.61 % Format :tptp:raw % 0.39/0.61 % Command :java -jar mcs_scs.jar %d %s % 0.39/0.61 % 0.39/0.61 % Result :Theorem 0.033512s % 0.39/0.61 % Output :CNFRefutation 0.033512s % 0.39/0.61 %------------------------------------------- % 0.39/0.61 %------------------------------------------------------------------------------ % 0.39/0.61 % File : LCL821-1 : TPTP v9.3.1. Released v4.1.0. % 0.39/0.61 % Domain : Logic Calculi % 0.39/0.61 % Problem : Strong normalization of typed lambda calculus 195_11 % 0.39/0.61 % Version : Especial. % 0.39/0.61 % English : % 0.39/0.61 % 0.39/0.61 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.39/0.61 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.39/0.61 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.39/0.61 % Source : [Nip10] % 0.39/0.61 % Names : StrongNorm-195_11 [Nip10] % 0.39/0.61 % 0.39/0.61 % Status : Unsatisfiable % 0.39/0.61 % Rating : 0.25 v9.3.0, 0.09 v9.1.0, 0.15 v9.0.0, 0.10 v8.2.0, 0.14 v8.1.0, 0.11 v7.5.0, 0.16 v7.4.0, 0.18 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.13 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.14 v6.0.0, 0.20 v5.5.0, 0.40 v5.3.0, 0.39 v5.2.0, 0.31 v5.1.0, 0.41 v5.0.0, 0.29 v4.1.0 % 0.39/0.61 % Syntax : Number of clauses : 367 ( 122 unt; 32 nHn; 205 RR) % 0.39/0.61 % Number of literals : 723 ( 277 equ; 351 neg) % 0.39/0.61 % Maximal clause size : 6 ( 1 avg) % 0.39/0.61 % Maximal term depth : 8 ( 2 avg) % 0.39/0.61 % Number of predicates : 33 ( 32 usr; 1 prp; 0-4 aty) % 0.39/0.61 % Number of functors : 45 ( 45 usr; 20 con; 0-5 aty) % 0.39/0.61 % Number of variables : 916 ( 136 sgn) % 0.39/0.61 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.39/0.61 % 0.39/0.61 % Comments : % 0.39/0.61 %------------------------------------------------------------------------------ % 0.39/0.61 cnf(cls_less__eqI_0,axiom, % 0.39/0.61 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.39/0.61 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a) % 0.39/0.61 | c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) % 0.39/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.39/0.61 % 0.39/0.61 cnf(cls_less__eqI_1,axiom, % 0.39/0.61 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.39/0.61 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a) % 0.39/0.61 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.39/0.61 | ~ c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) ) ). % 0.39/0.61 % 0.39/0.61 cnf(cls_add__diff__inverse_0,axiom, % 0.39/0.61 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat)) = V_m % 0.39/0.61 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.39/0.61 % 0.39/0.61 cnf(cls_diff__Suc__less_0,axiom, % 0.39/0.61 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_n,c_Suc(V_i),tc_nat),V_n,tc_nat) % 0.39/0.61 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.39/0.61 % 0.39/0.61 cnf(cls_add__is__1_1,axiom, % 0.39/0.61 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.39/0.61 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.39/0.61 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.39/0.61 % 0.39/0.61 cnf(cls_add__is__1_2,axiom, % 0.39/0.61 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.39/0.62 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.39/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__less_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_m,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__pred_0,axiom, % 0.39/0.62 ( c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = V_n % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__SucI_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__lessD_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_zero__less__diff_1,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat),tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_zero__less__diff_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat),tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_add__is__1_5,axiom, % 0.39/0.62 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_nat__diff__split_0,axiom, % 0.39/0.62 ( hBOOL(hAPP(V_P,c_HOL_Ozero__class_Ozero(tc_nat))) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_a,V_b,tc_nat) % 0.39/0.62 | ~ hBOOL(hAPP(V_P,c_HOL_Ominus__class_Ominus(V_a,V_b,tc_nat))) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_n__not__Suc__n_0,axiom, % 0.39/0.62 V_n != c_Suc(V_n) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__n__not__n_0,axiom, % 0.39/0.62 c_Suc(V_n) != V_n ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__diff__conv_1,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(V_i,c_HOL_Ominus__class_Ominus(V_j,V_k,tc_nat),tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),V_j,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__diff__conv_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),V_j,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_i,c_HOL_Ominus__class_Ominus(V_j,V_k,tc_nat),tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_of__nat__aux_Osimps_I1_J_0,axiom, % 0.39/0.62 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.39/0.62 | c_Nat_Osemiring__1__class_Oof__nat__aux(V_inc,c_HOL_Ozero__class_Ozero(tc_nat),V_i,T_a) = V_i ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__trans__Suc_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(c_Suc(V_i),V_k,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__Suc__eq_2,axiom, % 0.39/0.62 c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_lessI_0,axiom, % 0.39/0.62 c_HOL_Oord__class_Oless(V_n,c_Suc(V_n),tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__iff__diff__less__0_0,axiom, % 0.39/0.62 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.39/0.62 | c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__iff__diff__less__0_1,axiom, % 0.39/0.62 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.39/0.62 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__neq__Zero_0,axiom, % 0.39/0.62 c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_nat_Osimps_I3_J_0,axiom, % 0.39/0.62 c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__pred_H_0,axiom, % 0.39/0.62 ( V_n = c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__diff__1_0,axiom, % 0.39/0.62 ( c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) = V_n % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diffs0__imp__equal_0,axiom, % 0.39/0.62 ( c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.39/0.62 | c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.39/0.62 | V_m = V_n ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_one__is__add_4,axiom, % 0.39/0.62 c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__imp__diff__less_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_j,V_n,tc_nat),V_k,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_add__eq__if_1,axiom, % 0.39/0.62 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ominus__class_Ominus(V_m,c_HOL_Oone__class_Oone(tc_nat),tc_nat)),V_n)) % 0.39/0.62 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_not__less__less__Suc__eq_0,axiom, % 0.39/0.62 ( V_n = V_m % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.39/0.62 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__antisym_0,axiom, % 0.39/0.62 ( V_m = V_n % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.39/0.62 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__SucE_0,axiom, % 0.39/0.62 ( V_m = V_n % 0.39/0.62 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__Suc__Suc_0,axiom, % 0.39/0.62 c_HOL_Ominus__class_Ominus(c_Suc(V_m),c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_one__is__add_2,axiom, % 0.39/0.62 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.39/0.62 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.39/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_one__is__add_1,axiom, % 0.39/0.62 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.39/0.62 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.39/0.62 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__Suc0_1,axiom, % 0.39/0.62 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_not__step1__Nil_0,axiom, % 0.39/0.62 ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_not__Nil__step1_0,axiom, % 0.39/0.62 ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_One__nat__def_0,axiom, % 0.39/0.62 c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_nat_Oinject_0,axiom, % 0.39/0.62 ( c_Suc(V_nat) != c_Suc(V_nat_H) % 0.39/0.62 | V_nat = V_nat_H ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_Suc__inject_0,axiom, % 0.39/0.62 ( c_Suc(V_x) != c_Suc(V_y) % 0.39/0.62 | V_x = V_y ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_shift__commute_0,axiom, % 0.39/0.62 c_Type_Oshift(c_Type_Oshift(V_e,V_i,V_U,T_a),c_HOL_Ozero__class_Ozero(tc_nat),V_T,T_a) = c_Type_Oshift(c_Type_Oshift(V_e,c_HOL_Ozero__class_Ozero(tc_nat),V_T,T_a),c_Suc(V_i),V_U,T_a) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_minus__nat_Odiff__0_0,axiom, % 0.39/0.62 c_HOL_Ominus__class_Ominus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__self__eq__0_0,axiom, % 0.39/0.62 c_HOL_Ominus__class_Ominus(V_m,V_m,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_class__ringb_Osubr0__iff_1,axiom, % 0.39/0.62 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.39/0.62 | ~ class_Int_Onumber__ring(T_a) % 0.39/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__self_0,axiom, % 0.39/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.39/0.62 | c_HOL_Ominus__class_Ominus(V_a,V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__0__right_0,axiom, % 0.39/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.39/0.62 | c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_right__minus__eq_1,axiom, % 0.39/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.39/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_eq__iff__diff__eq__0_0,axiom, % 0.39/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.39/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__less__mono2_0,axiom, % 0.39/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_l,V_n,tc_nat),c_HOL_Ominus__class_Ominus(V_l,V_m,tc_nat),tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_m,V_l,tc_nat) % 0.39/0.62 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_diff__Suc__1_0,axiom, % 0.39/0.62 c_HOL_Ominus__class_Ominus(c_Suc(V_n),c_HOL_Oone__class_Oone(tc_nat),tc_nat) = V_n ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__iff__Suc__add_1,axiom, % 0.39/0.62 c_HOL_Oord__class_Oless(V_m,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_x)),tc_nat) ). % 0.39/0.62 % 0.39/0.62 cnf(cls_less__add__Suc2_0,axiom, % 0.39/0.62 c_HOL_Oord__class_Oless(V_i,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_i)),tc_nat) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_less__add__Suc1_0,axiom, % 0.39/0.63 c_HOL_Oord__class_Oless(V_i,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_m)),tc_nat) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_Zero__neq__Suc_0,axiom, % 0.39/0.63 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_nat_Osimps_I2_J_0,axiom, % 0.39/0.63 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_add__Suc_0,axiom, % 0.39/0.63 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(V_m)),V_n) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_add__Suc__right_0,axiom, % 0.39/0.63 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_Suc(V_n)) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_add__is__1_4,axiom, % 0.39/0.63 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_Suc__eq__plus1__left_0,axiom, % 0.39/0.63 c_Suc(V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),V_n) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_Suc__eq__plus1_0,axiom, % 0.39/0.63 c_Suc(V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),c_HOL_Oone__class_Oone(tc_nat)) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_less__Suc0_0,axiom, % 0.39/0.63 ( V_n = c_HOL_Ozero__class_Ozero(tc_nat) % 0.39/0.63 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_Var_I3_J_0,axiom, % 0.39/0.63 hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_diff__add__cancel_0,axiom, % 0.39/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.39/0.63 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ominus__class_Ominus(V_a,V_b,T_a)),V_b) = V_a ) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_nat__diff__split__asm_1,axiom, % 0.39/0.63 ( ~ hBOOL(hAPP(V_P,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_b),V_x),V_b,tc_nat))) % 0.39/0.63 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_nat__diff__split_1,axiom, % 0.39/0.63 ( ~ hBOOL(hAPP(V_P,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_b),V_d),V_b,tc_nat))) % 0.39/0.63 | hBOOL(hAPP(V_P,V_d)) ) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_diff__less__Suc_0,axiom, % 0.39/0.63 c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),c_Suc(V_m),tc_nat) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_of__nat__aux_Osimps_I2_J_0,axiom, % 0.39/0.63 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.39/0.63 | c_Nat_Osemiring__1__class_Oof__nat__aux(V_inc,c_Suc(V_n),V_i,T_a) = c_Nat_Osemiring__1__class_Oof__nat__aux(V_inc,V_n,hAPP(V_inc,V_i),T_a) ) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_one__is__add_5,axiom, % 0.39/0.63 c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_diff__add__0_0,axiom, % 0.39/0.63 c_HOL_Ominus__class_Ominus(V_n,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_diff__diff__left_0,axiom, % 0.39/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_i,V_j,tc_nat),V_k,tc_nat) = c_HOL_Ominus__class_Ominus(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_k),tc_nat) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_eq__eqI_1,axiom, % 0.39/0.63 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.39/0.63 | c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) % 0.39/0.63 | V_xa = V_y ) ). % 0.39/0.63 % 0.39/0.63 cnf(cls_eq__eqI_0,axiom, % 0.39/0.63 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.39/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a) % 0.49/0.63 | V_x_H = V_y_H ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_one__is__add_3,axiom, % 0.49/0.63 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.49/0.63 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.49/0.63 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_one__is__add_0,axiom, % 0.49/0.63 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.49/0.63 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.49/0.63 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__Suc__shift_0,axiom, % 0.49/0.63 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(V_m)),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_Suc(V_n)) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__0__eq__0_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__cancel2_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_k),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_k),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__cancel_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_zero__less__Suc_0,axiom, % 0.49/0.63 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_n),tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_gr0__conv__Suc_1,axiom, % 0.49/0.63 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_x),tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_class__ringb_Osubr0__iff_0,axiom, % 0.49/0.63 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.49/0.63 | ~ class_Int_Onumber__ring(T_a) % 0.49/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.49/0.63 | V_x = V_y ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_right__minus__eq_0,axiom, % 0.49/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.49/0.63 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.49/0.63 | V_a = V_b ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_eq__iff__diff__eq__0_1,axiom, % 0.49/0.63 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.49/0.63 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.49/0.63 | V_a = V_b ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__commute_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_i,V_j,tc_nat),V_k,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_i,V_k,tc_nat),V_j,tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Suc__lessI_0,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) % 0.49/0.63 | c_Suc(V_m) = V_n % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__is__1_3,axiom, % 0.49/0.63 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.49/0.63 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.49/0.63 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__is__1_0,axiom, % 0.49/0.63 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.49/0.63 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.49/0.63 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Suc__diff__diff_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(c_Suc(V_m),V_n,tc_nat),c_Suc(V_k),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_k,tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__Suc__eq__diff__pred_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(V_m,c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_m,c_HOL_Oone__class_Oone(tc_nat),tc_nat),V_n,tc_nat) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_not__less__less__Suc__eq_1,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.49/0.63 | c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_not__less__eq_1,axiom, % 0.49/0.63 ( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_not__less__eq_0,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.49/0.63 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__add__inverse2_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),V_n,tc_nat) = V_m ). % 0.49/0.63 % 0.49/0.63 cnf(cls_diff__add__inverse_0,axiom, % 0.49/0.63 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m),V_n,tc_nat) = V_m ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__diff__cancel_0,axiom, % 0.49/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.49/0.63 | c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b),V_b,T_a) = V_a ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_less__Suc__eq__0__disj_3,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(c_Suc(V_x),c_Suc(V_n),tc_nat) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_x,V_n,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Suc__less__eq_0,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Suc__mono_0,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_liftn__lift_0,axiom, % 0.49/0.63 c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = hAPP(hAPP(c_Lambda_Olift,c_Lambda_Oliftn(V_n,V_t,V_k)),V_k) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_of__nat__Suc_0,axiom, % 0.49/0.63 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.49/0.63 | c_Nat_Osemiring__1__class_Oof__nat(c_Suc(V_m),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Oone__class_Oone(T_a)),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_apps__preserves__betas_0,axiom, % 0.49/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.49/0.63 | ~ c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,V_ss,tc_Lambda_OdB) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_shift__lt_0,axiom, % 0.49/0.63 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,c_HOL_Ominus__class_Ominus(V_j,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Abs_0,axiom, % 0.49/0.63 ( c_Type_Otyping(V_env,c_Lambda_OdB_OAbs(V_t),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) % 0.49/0.63 | ~ c_Type_Otyping(c_Type_Oshift(V_env,c_HOL_Ozero__class_Ozero(tc_nat),V_T,tc_Type_Otype),V_t,V_U) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Beta_0,axiom, % 0.49/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.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),V_s),c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_foldl__Nil_0,axiom, % 0.49/0.63 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.49/0.63 % 0.49/0.63 cnf(cls_MI1_0,axiom, % 0.49/0.63 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.49/0.63 | hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i))) % 0.49/0.63 | ~ c_Type_Otyping(V_e,V_u,V_T1) % 0.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.49/0.63 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T1,tc_Type_Otype),V_t,V_Ta) % 0.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_MI2_0,axiom, % 0.49/0.63 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.49/0.63 | hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i))) % 0.49/0.63 | ~ c_Type_Otyping(V_e,V_u,V_T2) % 0.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.49/0.63 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T2,tc_Type_Otype),V_t,V_Ta) % 0.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_not__one__less__zero_0,axiom, % 0.49/0.63 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_lift__IT_0,axiom, % 0.49/0.63 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_Olift,V_t),V_i))) % 0.49/0.63 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_one__neq__zero_0,axiom, % 0.49/0.63 ( ~ class_Ring__and__Field_Ozero__neq__one(T_a) % 0.49/0.63 | c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.49/0.63 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.49/0.63 | V_dB = V_dB_H ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.49/0.63 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.49/0.63 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_liftn_Osimps_I1_J_1,axiom, % 0.49/0.63 ( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_n)) % 0.49/0.63 | c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_beta_0,axiom, % 0.49/0.63 hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_s),V_t),c_HOL_Ozero__class_Ozero(tc_nat)))) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__pos__pos_0,axiom, % 0.49/0.63 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.49/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b),T_a) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_liftn_Osimps_I3_J_0,axiom, % 0.49/0.63 c_Lambda_Oliftn(V_n,c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Oliftn(V_n,V_s,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__strict__mono_0,axiom, % 0.49/0.63 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.49/0.63 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_d),T_a) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_add__less__mono_0,axiom, % 0.49/0.63 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_l),tc_nat) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.49/0.63 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_beta__cases_I1_J_0,axiom, % 0.49/0.63 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_foldl__foldr1_0,axiom, % 0.49/0.63 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.49/0.63 | c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a),V_xs,T_a,T_a) = c_List_Ofoldr(c_HOL_Oplus__class_Oplus(T_a),V_xs,c_HOL_Ozero__class_Ozero(T_a),T_a,T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_zero__less__one_0,axiom, % 0.49/0.63 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oone__class_Oone(T_a),T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_less__add__one_0,axiom, % 0.49/0.63 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.63 | c_HOL_Oord__class_Oless(V_a,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Oone__class_Oone(T_a)),T_a) ) ). % 0.49/0.63 % 0.49/0.63 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_gr0I_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.49/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_liftn__0_0,axiom, % 0.49/0.64 c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t ). % 0.49/0.64 % 0.49/0.64 cnf(cls_neq0__conv_1,axiom, % 0.49/0.64 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_substn__subst__0_0,axiom, % 0.49/0.64 c_Lambda_Osubstn(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_pos__add__strict_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(V_b,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subst__Var__IT_0,axiom, % 0.49/0.64 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),c_Lambda_OdB_OVar(V_i)),V_j))) % 0.49/0.64 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_not__add__less1_0,axiom, % 0.49/0.64 ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_i,tc_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_not__add__less2_0,axiom, % 0.49/0.64 ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),V_i,tc_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_type_Osimps_I2_J_1,axiom, % 0.49/0.64 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.49/0.64 | V_type2 = V_type2_H ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_type_Osimps_I2_J_0,axiom, % 0.49/0.64 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.49/0.64 | V_type1 = V_type1_H ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__strict__right__mono_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__less__cancel__right_1,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__less__cancel__right_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__strict__left__mono_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_b),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__less__cancel__left_1,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_b),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__less__cancel__left_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_b),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__less__mono1_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_k),tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_nat__add__left__cancel__less_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n),tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_nat__add__left__cancel__less_1,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n),tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subst__eq_0,axiom, % 0.49/0.64 hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_k)),V_u),V_k) = V_u ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subject__reduction_0,axiom, % 0.49/0.64 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.49/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.49/0.64 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.49/0.64 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.49/0.64 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.49/0.64 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subst__App_0,axiom, % 0.49/0.64 hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u)),V_s),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),V_k)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_u),V_s),V_k)) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_of__nat__add_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.49/0.64 | c_Nat_Osemiring__1__class_Oof__nat(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_map__is__Nil__conv_0,axiom, % 0.49/0.64 ( c_List_Omap(V_f,V_xs,T_b,T_a) != c_List_Olist_ONil(T_a) % 0.49/0.64 | V_xs = c_List_Olist_ONil(T_b) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_lift_Osimps_I3_J_0,axiom, % 0.49/0.64 hAPP(hAPP(c_Lambda_Olift,c_Lambda_OdB_OAbs(V_s)),V_k) = c_Lambda_OdB_OAbs(hAPP(hAPP(c_Lambda_Olift,V_s),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_head__Var__reduction_0,axiom, % 0.49/0.64 ( 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.49/0.64 | ~ 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.49/0.64 % 0.49/0.64 cnf(cls_subst__subst_0,axiom, % 0.49/0.64 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),hAPP(hAPP(c_Lambda_Olift,V_v),V_i)),c_Suc(V_j))),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_u),V_v),V_j)),V_i) = hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i)),V_v),V_j) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_semiring__1__class_Oof__nat__code_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.49/0.64 | c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) = c_Nat_Osemiring__1__class_Oof__nat__aux(c_COMBC(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Oone__class_Oone(T_a),T_a,T_a,T_a),V_n,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_Var_I4_J_0,axiom, % 0.49/0.64 c_Type_Otyping(v_ea______,v_ua______,v_T____) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_substn_Osimps_I1_J_0,axiom, % 0.49/0.64 ( c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_i,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_lift__lift_0,axiom, % 0.49/0.64 ( hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(c_Lambda_Olift,V_t),V_i)),c_Suc(V_k)) = hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(c_Lambda_Olift,V_t),V_k)),V_i) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subst__gt_0,axiom, % 0.49/0.64 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_j)),V_u),V_i) = c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_j,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subst__Var_0,axiom, % 0.49/0.64 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_i)),V_s),V_k) = c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_i,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_foldl__absorb0_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a),V_zs,T_a,T_a)) = c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),V_x,V_zs,T_a,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_even__less__0__iff_1,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_even__less__0__iff_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.49/0.64 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_foldr__conv__foldl_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.49/0.64 | c_List_Ofoldr(c_HOL_Oplus__class_Oplus(T_a),V_xs,V_a,T_a,T_a) = c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),V_a,V_xs,T_a,T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_double__eq__0__iff_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.49/0.64 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__is__0_1,axiom, % 0.49/0.64 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.49/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__is__0_0,axiom, % 0.49/0.64 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.49/0.64 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_Var__IT_0,axiom, % 0.49/0.64 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_Nil__is__map__conv_0,axiom, % 0.49/0.64 ( c_List_Olist_ONil(T_a) != c_List_Omap(V_f,V_xs,T_b,T_a) % 0.49/0.64 | V_xs = c_List_Olist_ONil(T_b) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_natgb_Oadd__r0__iff_0,axiom, % 0.49/0.64 ( V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a) % 0.49/0.64 | V_a = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__eq__self__zero_0,axiom, % 0.49/0.64 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != V_m % 0.49/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.49/0.64 | ~ class_Int_Onumber__ring(T_a) % 0.49/0.64 | V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_a) % 0.49/0.64 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_of__nat__eq__iff_0,axiom, % 0.49/0.64 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.49/0.64 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.49/0.64 | V_m = V_n ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_foldl__assoc_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Osemigroup__add(T_a) % 0.49/0.64 | c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_y),V_zs,T_a,T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),V_y,V_zs,T_a,T_a)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_y) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),V_x) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_less__add__eq__less_0,axiom, % 0.49/0.64 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_l) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.49/0.64 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_nat__add__commute_0,axiom, % 0.49/0.64 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_substn_Osimps_I3_J_0,axiom, % 0.49/0.64 c_Lambda_Osubstn(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubstn(V_t,V_s,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_trans__less__add2_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_j),tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_trans__less__add1_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_m),tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__lessD1_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_k,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_termination__basic__simps_I2_J_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(V_x,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z),tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_x,V_z,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_termination__basic__simps_I1_J_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(V_x,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z),tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_list__app__typeE_0,axiom, % 0.49/0.64 ( c_Type_Otyping(V_e,V_t,c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xlist__app__typeE__1__1(V_T,V_e,V_t,V_ts),V_T,tc_Type_Otype,tc_Type_Otype)) % 0.49/0.64 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_listsp_ONil_0,axiom, % 0.49/0.64 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_subst__preserves__beta_0,axiom, % 0.49/0.64 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),V_t),V_i)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_s),V_t),V_i))) % 0.49/0.64 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_var__app__typesE_0,axiom, % 0.49/0.64 ( c_Type_Otyping(V_e,c_Lambda_OdB_OVar(V_i),c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xvar__app__typesE__1__1(V_T,V_e,V_i,V_ts),V_T,tc_Type_Otype,tc_Type_Otype)) % 0.49/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.49/0.64 % 0.49/0.64 cnf(cls_substn__subst__n_0,axiom, % 0.49/0.64 c_Lambda_Osubstn(V_t,V_s,V_n) = hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),c_Lambda_Oliftn(V_n,V_s,c_HOL_Ozero__class_Ozero(tc_nat))),V_n) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_double__eq__0__iff_1,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),c_HOL_Ozero__class_Ozero(T_a)) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__is__0_2,axiom, % 0.49/0.64 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),V_z)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_y)),V_z) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__cancel__21_1,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),V_z)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_nat__add__left__commute_0,axiom, % 0.49/0.64 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_z)) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_nat__add__assoc_0,axiom, % 0.49/0.64 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)),V_k) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_k)) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b)),V_c) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b)),V_c) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_d)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c)),V_d) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b)),V_c) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c)),V_b) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_d)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_d)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b)),V_c) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c)) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__gr__0_0,axiom, % 0.49/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.49/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_gr__implies__not0_0,axiom, % 0.49/0.64 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_not__less0_0,axiom, % 0.49/0.64 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__cancel__21_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),V_z)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),V_u) % 0.49/0.64 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) = V_u ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.49/0.64 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.49/0.64 % 0.49/0.64 cnf(cls_map__is__Nil__conv_1,axiom, % 0.49/0.64 c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) = c_List_Olist_ONil(T_a) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_of__nat__1_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.49/0.64 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oone__class_Oone(tc_nat),T_a) = c_HOL_Oone__class_Oone(T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_zero__neq__one_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Ozero__neq__one(T_a) % 0.49/0.64 | c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.49/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.49/0.64 % 0.49/0.64 cnf(cls_of__nat__0_0,axiom, % 0.49/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.49/0.64 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_lift__subst__lt_0,axiom, % 0.49/0.64 ( hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),V_j)),V_i) = hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,V_t),V_i)),hAPP(hAPP(c_Lambda_Olift,V_s),V_i)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),c_HOL_Oone__class_Oone(tc_nat))) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.49/0.64 % 0.49/0.64 cnf(cls_add__neg__neg_0,axiom, % 0.49/0.64 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.49/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.49/0.64 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_foldl__foldr1__lemma_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.49/0.65 | c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),V_a,V_xs,T_a,T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_List_Ofoldr(c_HOL_Oplus__class_Oplus(T_a),V_xs,c_HOL_Ozero__class_Ozero(T_a),T_a,T_a)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_natgb_Oadd__cancel_0,axiom, % 0.49/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_y) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_z) % 0.49/0.65 | V_y = V_z ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_nat__add__right__cancel_0,axiom, % 0.49/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_k) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_k) % 0.49/0.65 | V_m = V_n ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_nat__add__left__cancel_0,axiom, % 0.49/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n) % 0.49/0.65 | V_m = V_n ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.49/0.65 | ~ class_Int_Onumber__ring(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_y) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) % 0.49/0.65 | V_y = V_z ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_add__imp__eq_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c) % 0.49/0.65 | V_b = V_c ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_add__left__cancel_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c) % 0.49/0.65 | V_b = V_c ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_add__right__cancel_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_a) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a) % 0.49/0.65 | V_b = V_c ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_subst__Abs_0,axiom, % 0.49/0.65 hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OAbs(V_t)),V_s),V_k) = c_Lambda_OdB_OAbs(hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),hAPP(hAPP(c_Lambda_Olift,V_s),c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.49/0.65 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.49/0.65 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Lambda_0,axiom, % 0.49/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.49/0.65 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_d)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_d)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_appR_0,axiom, % 0.49/0.65 ( 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.49/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_appL_0,axiom, % 0.49/0.65 ( 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.49/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_liftn_Osimps_I2_J_0,axiom, % 0.49/0.65 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.49/0.65 % 0.49/0.65 cnf(cls_subst__lift_0,axiom, % 0.49/0.65 hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,V_t),V_k)),V_s),V_k) = V_t ). % 0.49/0.65 % 0.49/0.65 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.49/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.49/0.65 % 0.49/0.65 cnf(cls_lift__preserves__beta_0,axiom, % 0.49/0.65 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_Olift,V_r),V_i)),hAPP(hAPP(c_Lambda_Olift,V_s),V_i))) % 0.49/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_substn_Osimps_I1_J_1,axiom, % 0.49/0.65 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.49/0.65 | 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.49/0.65 % 0.49/0.65 cnf(cls_list__app__typeD_0,axiom, % 0.49/0.65 ( c_Type_Otyping(V_e,V_t,c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xlist__app__typeD__1__1(V_T,V_e,V_t,V_ts),V_T,tc_Type_Otype,tc_Type_Otype)) % 0.49/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift__subst_0,axiom, % 0.49/0.65 ( hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),V_j)),V_i) = hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,V_t),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat)))),hAPP(hAPP(c_Lambda_Olift,V_s),V_i)),V_j) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_j,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Nil__is__map__conv_1,axiom, % 0.49/0.65 c_List_Olist_ONil(T_a) = c_List_Omap(V_f,c_List_Olist_ONil(T_b),T_b,T_a) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_zero__less__two_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Oone__class_Oone(T_a)),c_HOL_Oone__class_Oone(T_a)),T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_x) = V_x ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_natgb_Oadd__r0__iff_1,axiom, % 0.49/0.65 V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_plus__nat_Oadd__0_0,axiom, % 0.49/0.65 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = V_n ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Nat_Oadd__0__right_0,axiom, % 0.49/0.65 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat)) = V_m ). % 0.49/0.65 % 0.49/0.65 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.49/0.65 | ~ class_Int_Onumber__ring(T_a) % 0.49/0.65 | V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_HOL_Ozero__class_Ozero(T_a)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_add__0__left_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.49/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_abs_0,axiom, % 0.49/0.65 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.49/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_substn_Osimps_I2_J_0,axiom, % 0.49/0.65 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.49/0.65 % 0.49/0.65 cnf(cls_typing__elims_I2_J_0,axiom, % 0.49/0.65 ( c_Type_Otyping(V_e,V_t,hAPP(hAPP(c_Type_Otype_OFun,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u)),V_T)) % 0.49/0.65 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_add__gr__0_2,axiom, % 0.49/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),tc_nat) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_add__gr__0_1,axiom, % 0.49/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),tc_nat) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.49/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.49/0.65 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.49/0.65 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.49/0.65 % 0.49/0.65 cnf(cls_subst__lemma_0,axiom, % 0.49/0.65 ( ~ c_Type_Otyping(V_e_H,V_u,V_U) % 0.49/0.65 | ~ c_Type_Otyping(c_Type_Oshift(V_e_H,V_i,V_U,tc_Type_Otype),V_t,V_T) % 0.49/0.65 | c_Type_Otyping(V_e_H,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_app__Var__IT_0,axiom, % 0.49/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),c_Lambda_OdB_OVar(V_i)))) % 0.49/0.65 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.49/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.49/0.65 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.49/0.65 ( hAPP(hAPP(c_Lambda_Olift,c_Lambda_OdB_OVar(V_i)),V_k) = c_Lambda_OdB_OVar(V_i) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_liftn_Osimps_I1_J_0,axiom, % 0.49/0.65 ( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_uIT_0,axiom, % 0.49/0.65 hBOOL(hAPP(c_InductTermi_OIT,v_u____)) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_var__app__types_1,axiom, % 0.49/0.65 ( c_Type_Otypings(V_e,V_us,c_Type_Osko__Type__Xvar__app__types__1__1(V_T,V_U,V_e,V_us)) % 0.49/0.65 | ~ 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.49/0.65 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.49/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_us,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.49/0.65 ( 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.49/0.65 | V_r = V_s ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.49/0.65 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.49/0.65 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_typing_OVar_0,axiom, % 0.49/0.65 c_Type_Otyping(V_env,c_Lambda_OdB_OVar(V_x),hAPP(V_env,V_x)) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_substs__lemma_0,axiom, % 0.49/0.65 ( c_Type_Otypings(V_e,c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,V_u,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),V_i,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) % 0.49/0.65 | ~ c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_T,tc_Type_Otype),V_ts,V_Ts) % 0.49/0.65 | ~ c_Type_Otyping(V_e,V_u,V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_subst__Var_1,axiom, % 0.49/0.65 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.49/0.65 | hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_x)),V_s),V_x) = V_s ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_list__app__typeE_1,axiom, % 0.49/0.65 ( c_Type_Otypings(V_e,V_ts,c_Type_Osko__Type__Xlist__app__typeE__1__1(V_T,V_e,V_t,V_ts)) % 0.49/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_COMBC__def_0,axiom, % 0.49/0.65 hAPP(c_COMBC(V_P,V_Q,T_b,T_c,T_a),V_R) = hAPP(hAPP(V_P,V_R),V_Q) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift_Osimps_I1_J_1,axiom, % 0.49/0.65 ( hAPP(hAPP(c_Lambda_Olift,c_Lambda_OdB_OVar(V_i)),V_k) = c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat))) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.49/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.49/0.65 % 0.49/0.65 cnf(cls_typing__elims_I2_J_1,axiom, % 0.49/0.65 ( c_Type_Otyping(V_e,V_u,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u)) % 0.49/0.65 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_xt1_I10_J_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Oorder(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_order__less__trans_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_head__Var__reduction_1,axiom, % 0.49/0.65 ( 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.49/0.65 | ~ 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.49/0.65 % 0.49/0.65 cnf(cls_list__app__typeI_0,axiom, % 0.49/0.65 ( c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) % 0.49/0.65 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.49/0.65 | ~ c_Type_Otyping(V_e,V_t,c_List_Ofoldr(c_Type_Otype_OFun,V_Ts,V_T,tc_Type_Otype,tc_Type_Otype)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_subst__Var_2,axiom, % 0.49/0.65 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_i)),V_s),V_k) = c_Lambda_OdB_OVar(V_i) % 0.49/0.65 | V_i = V_k % 0.49/0.65 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var_I2_J_0,axiom, % 0.49/0.65 c_Type_Otyping(c_Type_Oshift(v_ea______,v_ia______,v_T____,tc_Type_Otype),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB),v_T_Ha______) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_subst__map_0,axiom, % 0.49/0.65 hAPP(hAPP(hAPP(c_Lambda_Osubst,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_u),V_i) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i),c_List_Omap(c_COMBC(c_COMBC(c_Lambda_Osubst,V_u,tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),V_i,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.49/0.65 hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_Olift,V_s),V_k)),hAPP(hAPP(c_Lambda_Olift,V_t),V_k)) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_typing__elims_I1_J_0,axiom, % 0.49/0.65 ( hAPP(V_e,V_i) = V_T % 0.49/0.65 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OVar(V_i),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_substn_Osimps_I1_J_2,axiom, % 0.49/0.65 ( c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.49/0.65 | V_i = V_k % 0.49/0.65 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.49/0.65 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.49/0.65 % 0.49/0.65 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.49/0.65 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.49/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.49/0.65 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_apps__preserves__beta_0,axiom, % 0.49/0.65 ( 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.49/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_nat__less__le_1,axiom, % 0.49/0.65 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_less__not__refl_0,axiom, % 0.49/0.65 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_order__less__le_1,axiom, % 0.49/0.65 ( ~ class_Orderings_Oorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_linorder__neq__iff_1,axiom, % 0.49/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_order__less__irrefl_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.49/0.65 | V_x = V_y ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.49/0.65 | V_x = V_y % 0.49/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_nat__neq__iff_0,axiom, % 0.49/0.65 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.49/0.65 | V_m = V_n ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_nat__less__cases_0,axiom, % 0.49/0.65 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.49/0.65 | V_m = V_n % 0.49/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_var__app__type__eq_0,axiom, % 0.49/0.65 ( V_T = V_U % 0.49/0.65 | ~ 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.49/0.65 | ~ 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.49/0.65 % 0.49/0.65 cnf(cls_linorder__neqE__nat_0,axiom, % 0.49/0.65 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.49/0.65 | V_x = V_y ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_linorder__neqE_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.49/0.65 | V_x = V_y ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_linorder__less__linear_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.49/0.65 | V_x = V_y % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.49/0.65 | V_x = V_y % 0.49/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.49/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.49/0.65 | V_dB2 = V_dB2_H ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.49/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.49/0.65 | V_dB1 = V_dB1_H ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_IT_OVar_0,axiom, % 0.49/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.49/0.65 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.49/0.65 ( 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.49/0.65 | V_rs = V_ss ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.49/0.65 ( 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.49/0.65 | V_r = V_s ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.49/0.65 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.49/0.65 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_App_0,axiom, % 0.49/0.65 ( c_Type_Otyping(V_env,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_U) % 0.49/0.65 | ~ c_Type_Otyping(V_env,V_t,V_T) % 0.49/0.65 | ~ c_Type_Otyping(V_env,V_s,hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_of__nat__less__iff_1,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_of__nat__less__iff_0,axiom, % 0.49/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.49/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.49/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.49/0.65 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift__map_0,axiom, % 0.49/0.65 hAPP(hAPP(c_Lambda_Olift,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_i) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_Olift,V_t),V_i),c_List_Omap(c_COMBC(c_Lambda_Olift,V_i,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_var__app__types_0,axiom, % 0.49/0.65 ( V_U = c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xvar__app__types__1__1(V_T,V_U,V_e,V_us),V_T,tc_Type_Otype,tc_Type_Otype) % 0.49/0.65 | ~ 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.49/0.65 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.49/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_us,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_list__app__typeD_1,axiom, % 0.49/0.65 ( c_Type_Otypings(V_e,V_ts,c_Type_Osko__Type__Xlist__app__typeD__1__1(V_T,V_e,V_t,V_ts)) % 0.49/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_subst__lt_0,axiom, % 0.49/0.65 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_j)),V_u),V_i) = c_Lambda_OdB_OVar(V_j) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.49/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.49/0.65 | V_rs = V_ss ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.49/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.49/0.65 | V_m = V_n ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.49/0.65 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.49/0.65 | V_nat = V_nat_H ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_var__app__typesE_1,axiom, % 0.49/0.65 ( c_Type_Otypings(V_e,V_ts,c_Type_Osko__Type__Xvar__app__typesE__1__1(V_T,V_e,V_i,V_ts)) % 0.49/0.65 | ~ 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.49/0.65 % 0.49/0.65 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.49/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.49/0.65 % 0.49/0.65 cnf(cls_lifts__IT_0,axiom, % 0.49/0.65 ( c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(c_COMBC(c_Lambda_Olift,c_HOL_Ozero__class_Ozero(tc_nat),tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) % 0.49/0.65 | ~ c_List_Olistsp(c_InductTermi_OIT,V_ts,tc_Lambda_OdB) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift__type_0,axiom, % 0.49/0.65 ( c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),hAPP(hAPP(c_Lambda_Olift,V_t),V_i),V_T) % 0.49/0.65 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_xt1_I9_J_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Oorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.49/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_order__less__asym_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_order__less__asym_H_0,axiom, % 0.49/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_uT_0,axiom, % 0.49/0.65 c_Type_Otyping(v_e____,v_u____,v_T____) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_shift__gt_0,axiom, % 0.49/0.65 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,V_j) % 0.49/0.65 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_shift__eq_0,axiom, % 0.49/0.65 hAPP(c_Type_Oshift(V_e,V_x,V_T,T_a),V_x) = V_T ). % 0.49/0.65 % 0.49/0.65 cnf(cls_False_0,axiom, % 0.49/0.65 v_n____ != v_i____ ). % 0.49/0.65 % 0.49/0.65 cnf(cls_that_0,axiom, % 0.49/0.65 ( v_thesis____ % 0.49/0.65 | ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_rs____,V_Ts) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_nT_0,axiom, % 0.49/0.65 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB),v_T_H____) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_lift__types_0,axiom, % 0.49/0.65 ( c_Type_Otypings(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_List_Omap(c_COMBC(c_Lambda_Olift,V_i,tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_Ts) % 0.49/0.65 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) ) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_CHAINED_0,axiom, % 0.49/0.65 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____),v_rs____,tc_Lambda_OdB,tc_Lambda_OdB),v_T_H____) ). % 0.49/0.65 % 0.49/0.65 cnf(cls_conjecture_0,negated_conjecture, % 0.49/0.65 ~ v_thesis____ ). % 0.49/0.65 % 0.49/0.65 cnf(cls_conjecture_1,negated_conjecture, % 0.49/0.65 ( v_thesis____ % 0.49/0.65 | ~ c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_rs____,V_x) ) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.49/0.65 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.49/0.65 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.49/0.65 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.49/0.65 | ~ class_Orderings_Oorder(T_1) ) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.49/0.65 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.49/0.65 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.49/0.65 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.49/0.65 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.49/0.65 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.49/0.65 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.49/0.65 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.49/0.65 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.49/0.65 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__Ring__and__Field_Ozero__neq__one,axiom, % 0.49/0.65 class_Ring__and__Field_Ozero__neq__one(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Osemigroup__add,axiom, % 0.49/0.65 class_OrderedGroup_Osemigroup__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.49/0.65 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.49/0.65 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.49/0.65 class_Nat_Osemiring__char__0(tc_nat) ). % 0.49/0.65 % 0.49/0.65 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.49/0.66 class_Orderings_Opreorder(tc_nat) ). % 0.49/0.66 % 0.49/0.66 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.49/0.66 class_Orderings_Olinorder(tc_nat) ). % 0.49/0.66 % 0.49/0.66 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.49/0.66 class_Orderings_Oorder(tc_nat) ). % 0.49/0.66 % 0.49/0.66 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.49/0.66 c_fequal(V_x,V_x,T_a) ). % 0.49/0.66 % 0.49/0.66 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.49/0.66 ( V_X = V_Y % 0.49/0.66 | ~ c_fequal(V_X,V_Y,T_a) ) ). % 0.49/0.66 % 0.49/0.66 %------------------------------------------------------------------------------ % 0.49/0.66 %------------------------------------------- % 0.49/0.66 % Proof found % 0.49/0.66 % SZS status Theorem for theBenchmark % 0.49/0.66 % SZS output start Proof % 0.49/0.66 %ClaNum:481(EqnAxiom:116) % 0.49/0.66 %VarNum:1809(SingletonVarNum:796) % 0.49/0.66 %MaxLitNum:6 % 0.49/0.66 %MaxfuncDepth:6 % 0.49/0.66 %SharedTerms:72 % 0.49/0.66 %goalClause: 212 432 % 0.49/0.66 %singleGoalClaCount:1 % 0.49/0.66 [117]P1(a1) % 0.49/0.66 [118]P2(a1) % 0.49/0.66 [119]P30(a1) % 0.49/0.66 [120]P3(a1) % 0.49/0.66 [121]P4(a1) % 0.49/0.66 [122]P5(a1) % 0.49/0.66 [123]P21(a1) % 0.49/0.66 [124]P6(a1) % 0.49/0.66 [125]P7(a1) % 0.49/0.66 [126]P23(a1) % 0.49/0.66 [127]P24(a1) % 0.49/0.66 [128]P16(a1) % 0.49/0.66 [129]P17(a1) % 0.49/0.66 [130]P18(a1) % 0.49/0.66 [131]P25(a1) % 0.49/0.66 [132]P27(a1) % 0.49/0.66 [133]P26(a1) % 0.49/0.66 [137]P8(a35,a33,a36) % 0.49/0.66 [138]P8(a39,a34,a36) % 0.49/0.66 [211]~E(a41,a42) % 0.49/0.66 [212]~P32(a5000) % 0.49/0.66 [134]P31(f8(a2,a33)) % 0.49/0.66 [135]P31(f8(a2,a34)) % 0.49/0.66 [206]P8(f21(a35,a40,a36,a31),f17(a12,f9(a42),a43,a30,a30),a37) % 0.49/0.66 [208]P8(f21(a39,a41,a36,a31),f17(a12,f9(a42),a43,a30,a30),a38) % 0.49/0.66 [226]~P10(x2261,x2261,a1) % 0.49/0.66 [143]E(f4(x1431,x1431,a1),f7(a1)) % 0.49/0.66 [228]~P10(x2281,f7(a1),a1) % 0.49/0.66 [136]P31(f8(a2,f9(x1361))) % 0.49/0.66 [140]E(f8(f8(f3(a1),x1401),f7(a1)),x1401) % 0.49/0.66 [144]E(f4(x1441,f7(a1),a1),x1441) % 0.49/0.66 [148]E(f4(f7(a1),x1481,a1),f7(a1)) % 0.49/0.66 [158]P10(x1581,f8(f8(f3(a1),x1581),f6(a1)),a1) % 0.49/0.66 [160]P10(f7(a1),f8(f8(f3(a1),x1601),f6(a1)),a1) % 0.49/0.66 [220]~E(f8(f8(f3(a1),x2201),f6(a1)),x2201) % 0.49/0.66 [224]~E(f8(f8(f3(a1),x2241),f6(a1)),f7(a1)) % 0.49/0.66 [141]E(f8(f8(f3(a1),f7(a1)),x1411),x1411) % 0.49/0.66 [142]P12(x1421,x1421,x1422) % 0.49/0.66 [149]P9(x1491,f15(x1492),x1492) % 0.49/0.66 [150]P8(x1501,f9(x1502),f8(x1501,x1502)) % 0.49/0.66 [214]~E(f9(x2141),f10(x2142)) % 0.49/0.66 [147]E(f13(f7(a1),x1471,x1472),x1471) % 0.49/0.66 [165]P10(f4(x1651,x1652,a1),f8(f8(f3(a1),x1651),f6(a1)),a1) % 0.49/0.66 [184]E(f8(f8(f8(a16,x1841),f13(f7(a1),x1842,f7(a1))),f7(a1)),f8(f8(f8(a16,x1841),x1842),f7(a1))) % 0.49/0.66 [189]P10(x1891,f8(f8(f3(a1),f8(f8(f3(a1),x1892),x1891)),f6(a1)),a1) % 0.49/0.66 [191]P10(x1911,f8(f8(f3(a1),f8(f8(f3(a1),x1911),x1912)),f6(a1)),a1) % 0.49/0.66 [151]E(f8(f8(f3(a1),x1511),x1512),f8(f8(f3(a1),x1512),x1511)) % 0.49/0.66 [173]E(f4(x1731,f8(f8(f3(a1),x1732),f6(a1)),a1),f4(f4(x1731,f6(a1),a1),x1732,a1)) % 0.49/0.66 [194]P31(f8(f8(a11,f8(f8(a12,f10(x1941)),x1942)),f8(f8(f8(a16,x1941),x1942),f7(a1)))) % 0.49/0.66 [230]~P31(f8(f8(a11,f9(x2301)),x2302)) % 0.49/0.66 [231]~P10(f8(f8(f3(a1),x2311),x2312),x2312,a1) % 0.49/0.66 [232]~P10(f8(f8(f3(a1),x2321),x2322),x2321,a1) % 0.49/0.66 [153]E(f8(f8(f8(a16,f9(x1531)),x1532),x1531),x1532) % 0.49/0.66 [154]E(f4(f8(f8(f3(a1),x1541),x1542),x1542,a1),x1541) % 0.49/0.66 [155]E(f4(f8(f8(f3(a1),x1551),x1552),x1551,a1),x1552) % 0.49/0.66 [156]E(f4(x1561,f8(f8(f3(a1),x1561),x1562),a1),f7(a1)) % 0.49/0.66 [175]E(f10(f8(f8(a14,x1751),f8(f8(f3(a1),x1752),f6(a1)))),f8(f8(a14,f10(x1751)),x1752)) % 0.49/0.66 [182]E(f8(f8(f3(a1),f8(f8(f3(a1),x1821),f6(a1))),x1822),f8(f8(f3(a1),x1821),f8(f8(f3(a1),x1822),f6(a1)))) % 0.49/0.66 [186]E(f8(f8(f3(a1),f8(f8(f3(a1),x1861),f6(a1))),x1862),f8(f8(f3(a1),f8(f8(f3(a1),x1861),x1862)),f6(a1))) % 0.49/0.66 [233]~P11(x2331,x2332,f15(x2333),x2333) % 0.49/0.66 [234]~P11(x2341,f15(x2342),x2343,x2342) % 0.49/0.66 [167]E(f20(x1671,f15(x1672),x1672,x1673),f15(x1673)) % 0.49/0.66 [174]E(f4(f4(x1741,x1742,a1),x1743,a1),f4(f4(x1741,x1743,a1),x1742,a1)) % 0.49/0.66 [215]~E(f10(x2151),f8(f8(a12,x2152),x2153)) % 0.49/0.66 [216]~E(f9(x2161),f8(f8(a12,x2162),x2163)) % 0.49/0.66 [217]~E(f8(f8(a12,x2171),x2172),f10(x2173)) % 0.49/0.66 [218]~E(f8(f8(a12,x2181),x2182),f9(x2183)) % 0.49/0.66 [183]E(f13(f8(f8(f3(a1),x1831),f6(a1)),x1832,x1833),f8(f8(a14,f13(x1831,x1832,x1833)),x1833)) % 0.49/0.66 [192]E(f4(f4(f8(f8(f3(a1),x1921),f6(a1)),x1922,a1),f8(f8(f3(a1),x1923),f6(a1)),a1),f4(f4(x1921,x1922,a1),x1923,a1)) % 0.49/0.66 [209]E(f17(a12,f8(f8(a14,x2091),x2092),f20(f5(a14,x2092,a30,a1,a30),x2093,a30,a30),a30,a30),f8(f8(a14,f17(a12,x2091,x2093,a30,a30)),x2092)) % 0.49/0.66 [168]E(f8(f8(f3(a1),x1681),f8(f8(f3(a1),x1682),x1683)),f8(f8(f3(a1),x1682),f8(f8(f3(a1),x1681),x1683))) % 0.49/0.66 [169]E(f4(f8(f8(f3(a1),x1691),x1692),f8(f8(f3(a1),x1693),x1692),a1),f4(x1691,x1693,a1)) % 0.49/0.66 [170]E(f4(f8(f8(f3(a1),x1701),x1702),f8(f8(f3(a1),x1701),x1703),a1),f4(x1702,x1703,a1)) % 0.49/0.66 [172]E(f4(x1721,f8(f8(f3(a1),x1722),x1723),a1),f4(f4(x1721,x1722,a1),x1723,a1)) % 0.49/0.66 [179]E(f10(f13(x1791,x1792,f8(f8(f3(a1),x1793),f6(a1)))),f13(x1791,f10(x1792),x1793)) % 0.49/0.66 [185]E(f8(f8(a12,f8(f8(a14,x1851),x1852)),f8(f8(a14,x1853),x1852)),f8(f8(a14,f8(f8(a12,x1851),x1853)),x1852)) % 0.49/0.66 [193]E(f10(f8(f8(f8(a16,x1931),f8(f8(a14,x1932),f7(a1))),f8(f8(f3(a1),x1933),f6(a1)))),f8(f8(f8(a16,f10(x1931)),x1932),x1933)) % 0.49/0.66 [203]E(f10(f8(f8(f8(a16,x2031),f13(f8(f8(f3(a1),x2032),f6(a1)),x2033,f7(a1))),f8(f8(f3(a1),x2032),f6(a1)))),f8(f8(f8(a16,f10(x2031)),f13(x2032,x2033,f7(a1))),x2032)) % 0.49/0.66 [178]E(f8(f8(f3(a1),f8(f8(f3(a1),x1781),x1782)),x1783),f8(f8(f3(a1),x1781),f8(f8(f3(a1),x1782),x1783))) % 0.49/0.66 [181]E(f8(f8(f8(a16,f8(f8(a14,x1811),x1812)),x1813),x1812),x1811) % 0.49/0.66 [188]E(f8(f21(x1881,x1882,x1883,x1884),x1882),x1883) % 0.49/0.66 [196]E(f17(x1961,x1962,f15(x1963),x1964,x1963),x1962) % 0.49/0.66 [197]E(f19(x1971,f15(x1972),x1973,x1972,x1974),x1973) % 0.49/0.66 [236]~E(f17(a12,f9(x2361),x2362,a30,a30),f17(a12,f10(x2363),x2364,a30,a30)) % 0.49/0.66 [187]E(f8(f8(a12,f13(x1871,x1872,x1873)),f13(x1871,x1874,x1873)),f13(x1871,f8(f8(a12,x1872),x1874),x1873)) % 0.49/0.66 [235]~E(f8(f8(a12,f10(x2351)),x2352),f17(a12,f9(x2353),x2354,a30,a30)) % 0.49/0.66 [195]E(f8(f8(a12,f8(f8(f8(a16,x1951),x1952),x1953)),f8(f8(f8(a16,x1954),x1952),x1953)),f8(f8(f8(a16,f8(f8(a12,x1951),x1954)),x1952),x1953)) % 0.49/0.66 [210]E(f17(a12,f8(f8(f8(a16,x2101),x2102),x2103),f20(f5(f5(a16,x2102,a30,a30,f32(a1,a30)),x2103,a30,a1,a30),x2104,a30,a30),a30,a30),f8(f8(f8(a16,f17(a12,x2101,x2104,a30,a30)),x2102),x2103)) % 0.49/0.66 [202]E(f21(f21(x2021,f7(a1),x2022,x2023),f8(f8(f3(a1),x2024),f6(a1)),x2025,x2023),f21(f21(x2021,x2024,x2025,x2023),f7(a1),x2022,x2023)) % 0.49/0.66 [204]E(f8(f5(x2041,x2042,x2043,x2044,x2045),x2046),f8(f8(x2041,x2046),x2042)) % 0.49/0.66 [240]~P30(x2401)+~E(f6(x2401),f7(x2401)) % 0.49/0.66 [246]E(x2461,f7(a1))+P10(f7(a1),x2461,a1) % 0.49/0.66 [260]~P2(x2601)+P10(f7(x2601),f6(x2601),x2601) % 0.49/0.66 [282]~P2(x2821)+~P10(f6(x2821),f7(x2821),x2821) % 0.49/0.66 [432]~P13(f21(a39,a41,a36,a31),a43,x4321)+P32(a5000) % 0.49/0.66 [241]~P1(x2411)+E(f22(f7(a1),x2411),f7(x2411)) % 0.49/0.66 [242]~P1(x2421)+E(f22(f6(a1),x2421),f6(x2421)) % 0.49/0.66 [265]~P20(x2651)+E(f8(f8(f3(x2651),f7(x2651)),f7(x2651)),f7(x2651)) % 0.49/0.66 [266]~P31(f8(a2,x2661))+P31(f8(a2,f10(x2661))) % 0.49/0.66 [326]~P2(x3261)+P10(f7(x3261),f8(f8(f3(x3261),f6(x3261)),f6(x3261)),x3261) % 0.49/0.66 [349]E(x3491,f7(a1))+~P10(x3491,f8(f8(f3(a1),f7(a1)),f6(a1)),a1) % 0.49/0.66 [392]~P10(f7(a1),x3921,a1)+E(f8(f8(f3(a1),f4(x3921,f6(a1),a1)),f6(a1)),x3921) % 0.49/0.66 [430]~P10(f7(a1),x4301,a1)+E(f8(f8(f3(a1),f4(x4301,f8(f8(f3(a1),f7(a1)),f6(a1)),a1)),f6(a1)),x4301) % 0.49/0.66 [467]~P9(a2,x4671,a30)+P9(a2,f20(f5(a14,f7(a1),a30,a1,a30),x4671,a30,a30),a30) % 0.49/0.66 [268]~P10(x2682,x2682,x2681)+~P25(x2681) % 0.49/0.66 [269]~P10(x2692,x2692,x2691)+~P27(x2691) % 0.49/0.66 [270]~P10(x2702,x2702,x2701)+~P26(x2701) % 0.49/0.66 [237]E(x2371,x2372)+~E(f10(x2371),f10(x2372)) % 0.49/0.66 [238]E(x2381,x2382)+~E(f9(x2381),f9(x2382)) % 0.49/0.66 [243]~P25(x2432)+P25(f32(x2431,x2432)) % 0.49/0.66 [244]~P27(x2442)+P27(f32(x2441,x2442)) % 0.49/0.66 [248]~P19(x2482)+E(f4(x2481,x2481,x2482),f7(x2482)) % 0.49/0.66 [249]~P15(x2492)+E(f4(x2491,x2491,x2492),f7(x2492)) % 0.49/0.66 [293]~P2(x2931)+~P10(f22(x2932,x2931),f7(x2931),x2931) % 0.49/0.66 [348]~P10(x3482,x3481,a1)+P10(f7(a1),f4(x3481,x3482,a1),a1) % 0.49/0.66 [366]P10(x3661,x3662,a1)+~P10(f7(a1),f4(x3662,x3661,a1),a1) % 0.49/0.66 [250]~P5(x2501)+E(f8(f8(f3(x2501),x2502),f7(x2501)),x2502) % 0.49/0.66 [251]~P24(x2511)+E(f8(f8(f3(x2511),x2512),f7(x2511)),x2512) % 0.49/0.66 [252]~P16(x2521)+E(f8(f8(f3(x2521),x2522),f7(x2521)),x2522) % 0.49/0.66 [253]~P19(x2532)+E(f4(x2531,f7(x2532),x2532),x2531) % 0.49/0.66 [308]~P2(x3082)+P10(x3081,f8(f8(f3(x3082),x3081),f6(x3082)),x3082) % 0.49/0.66 [322]P10(x3221,x3222,a1)+P10(x3222,f8(f8(f3(a1),x3221),f6(a1)),a1) % 0.49/0.66 [325]P10(x3252,x3251,a1)+E(f8(f8(f3(a1),x3251),f4(x3252,x3251,a1)),x3252) % 0.49/0.66 [339]~P31(f8(f8(a11,x3391),x3392))+P31(f8(f8(a11,f10(x3391)),f10(x3392))) % 0.49/0.66 [375]~P10(x3751,x3752,a1)+~P10(x3752,f8(f8(f3(a1),x3751),f6(a1)),a1) % 0.49/0.66 [412]P10(x4121,x4122,a1)+~P10(f8(f8(f3(a1),x4121),f6(a1)),f8(f8(f3(a1),x4122),f6(a1)),a1) % 0.49/0.66 [452]~P5(x4521)+E(f19(f3(x4521),x4522,f7(x4521),x4521,x4521),f17(f3(x4521),f7(x4521),x4522,x4521,x4521)) % 0.49/0.66 [453]~P1(x4531)+E(f23(f5(f3(x4531),f6(x4531),x4531,x4531,x4531),x4532,f7(x4531),x4531),f22(x4532,x4531)) % 0.49/0.66 [254]~P5(x2541)+E(f8(f8(f3(x2541),f7(x2541)),x2542),x2542) % 0.49/0.66 [256]~P24(x2561)+E(f8(f8(f3(x2561),f7(x2561)),x2562),x2562) % 0.49/0.66 [257]~P16(x2571)+E(f8(f8(f3(x2571),f7(x2571)),x2572),x2572) % 0.49/0.66 [262]E(x2621,f7(a1))+~E(f8(f8(f3(a1),x2622),x2621),x2622) % 0.49/0.66 [263]E(x2631,f7(a1))+~E(f8(f8(f3(a1),x2632),x2631),f7(a1)) % 0.49/0.66 [264]E(x2641,f7(a1))+~E(f8(f8(f3(a1),x2641),x2642),f7(a1)) % 0.49/0.66 [292]~P10(x2921,x2922,a1)+E(f8(f8(a14,f9(x2921)),x2922),f9(x2921)) % 0.49/0.66 [324]P10(x3241,x3242,a1)+E(f8(f8(a14,f9(x3241)),x3242),f9(f8(f8(f3(a1),x3241),f6(a1)))) % 0.49/0.66 [327]~P1(x3272)+E(f22(f8(f8(f3(a1),x3271),f6(a1)),x3272),f8(f8(f3(x3272),f6(x3272)),f22(x3271,x3272))) % 0.49/0.66 [329]~P31(f8(a2,x3291))+P31(f8(a2,f8(f8(a14,x3291),x3292))) % 0.49/0.66 [345]~P31(f8(a2,x3451))+P31(f8(a2,f8(f8(a12,x3451),f9(x3452)))) % 0.49/0.66 [410]~P10(f7(a1),x4101,a1)+P10(f4(x4101,f8(f8(f3(a1),x4102),f6(a1)),a1),x4101,a1) % 0.49/0.66 [436]E(x4361,f7(a1))+E(f8(f8(f3(a1),f8(f8(f3(a1),f4(x4361,f6(a1),a1)),x4362)),f6(a1)),f8(f8(f3(a1),x4361),x4362)) % 0.49/0.66 [466]~P9(a2,x4662,a30)+P31(f8(a2,f17(a12,f9(x4661),x4662,a30,a30))) % 0.49/0.66 [267]E(x2671,x2672)+~P12(x2671,x2672,x2673) % 0.49/0.66 [278]~P8(x2781,f9(x2782),x2783)+E(f8(x2781,x2782),x2783) % 0.49/0.66 [346]~P10(x3461,x3463,a1)+P10(f4(x3461,x3462,a1),x3463,a1) % 0.49/0.66 [442]~E(f10(x4422),f17(a12,x4423,x4421,a30,a30))+E(x4421,f15(a30)) % 0.49/0.66 [443]~E(f9(x4432),f17(a12,x4433,x4431,a30,a30))+E(x4431,f15(a30)) % 0.49/0.66 [444]~E(f17(a12,x4442,x4441,a30,a30),f10(x4443))+E(x4441,f15(a30)) % 0.49/0.66 [446]E(x4461,f10(x4462))+~E(f17(a12,x4461,x4463,a30,a30),f10(x4462)) % 0.49/0.66 [447]E(f10(x4471),x4472)+~E(f10(x4471),f17(a12,x4472,x4473,a30,a30)) % 0.49/0.66 [448]E(f9(x4481),x4482)+~E(f9(x4481),f17(a12,x4482,x4483,a30,a30)) % 0.49/0.66 [456]E(x4561,x4562)+~E(f17(a12,x4561,x4563,a30,a30),f17(a12,x4562,x4563,a30,a30)) % 0.49/0.66 [297]~P10(x2972,x2973,a1)+E(f13(x2971,f9(x2972),x2973),f9(x2972)) % 0.49/0.66 [350]~P1(x3503)+E(f23(x3501,f7(a1),x3502,x3503),x3502) % 0.49/0.66 [449]E(f8(f8(a12,x4491),x4492),x4493)+~E(f8(f8(a12,x4491),x4492),f17(a12,x4493,f15(a30),a30,a30)) % 0.49/0.66 [451]~P6(x4511)+E(f19(f3(x4511),x4512,x4513,x4511,x4511),f17(f3(x4511),x4513,x4512,x4511,x4511)) % 0.49/0.66 [475]~P31(f8(f8(a11,x4751),x4753))+P31(f8(f8(a11,f17(a12,x4751,x4752,a30,a30)),f17(a12,x4753,x4752,a30,a30))) % 0.49/0.66 [476]~P11(a11,x4762,x4763,a30)+P31(f8(f8(a11,f17(a12,x4761,x4762,a30,a30)),f17(a12,x4761,x4763,a30,a30))) % 0.49/0.66 [280]~P24(x2801)+E(f8(f8(f3(x2801),x2802),x2803),f8(f8(f3(x2801),x2803),x2802)) % 0.49/0.66 [281]~P16(x2811)+E(f8(f8(f3(x2811),x2812),x2813),f8(f8(f3(x2811),x2813),x2812)) % 0.49/0.66 [295]E(x2951,x2952)+~E(f8(f8(f3(a1),x2953),x2951),f8(f8(f3(a1),x2953),x2952)) % 0.49/0.66 [296]E(x2961,x2962)+~E(f8(f8(f3(a1),x2961),x2963),f8(f8(f3(a1),x2962),x2963)) % 0.49/0.66 [335]~P10(x3351,x3353,a1)+P10(x3351,f8(f8(f3(a1),x3352),x3353),a1) % 0.49/0.66 [337]~P10(x3371,x3372,a1)+P10(x3371,f8(f8(f3(a1),x3372),x3373),a1) % 0.49/0.66 [358]~P19(x3581)+E(f8(f8(f3(x3581),f4(x3582,x3583,x3581)),x3583),x3582) % 0.49/0.66 [359]P10(x3591,x3592,a1)+~P10(f8(f8(f3(a1),x3591),x3593),x3592,a1) % 0.49/0.66 [372]~P10(x3721,x3723,a1)+P10(f8(f8(f3(a1),x3721),x3722),f8(f8(f3(a1),x3723),x3722),a1) % 0.49/0.66 [373]~P10(x3732,x3733,a1)+P10(f8(f8(f3(a1),x3731),x3732),f8(f8(f3(a1),x3731),x3733),a1) % 0.49/0.66 [395]P10(x3951,f4(x3952,x3953,a1),a1)+~P10(f8(f8(f3(a1),x3951),x3953),x3952,a1) % 0.49/0.66 [397]~P10(x3971,f4(x3973,x3972,a1),a1)+P10(f8(f8(f3(a1),x3971),x3972),x3973,a1) % 0.49/0.66 [408]P10(x4081,x4082,a1)+~P10(f8(f8(f3(a1),x4083),x4081),f8(f8(f3(a1),x4083),x4082),a1) % 0.49/0.66 [422]~P31(f8(f8(a11,x4221),x4223))+P31(f8(f8(a11,f8(f8(a14,x4221),x4222)),f8(f8(a14,x4223),x4222))) % 0.49/0.66 [423]~P31(f8(f8(a11,x4231),x4233))+P31(f8(f8(a11,f8(f8(a12,x4231),x4232)),f8(f8(a12,x4233),x4232))) % 0.49/0.66 [424]~P31(f8(f8(a11,x4242),x4243))+P31(f8(f8(a11,f8(f8(a12,x4241),x4242)),f8(f8(a12,x4241),x4243))) % 0.49/0.66 [454]~P5(x4541)+E(f8(f8(f3(x4541),x4542),f19(f3(x4541),x4543,f7(x4541),x4541,x4541)),f17(f3(x4541),x4542,x4543,x4541,x4541)) % 0.49/0.66 [455]~P5(x4551)+E(f8(f8(f3(x4551),x4552),f17(f3(x4551),f7(x4551),x4553,x4551,x4551)),f17(f3(x4551),x4552,x4553,x4551,x4551)) % 0.49/0.66 [301]~P19(x3011)+E(f4(f8(f8(f3(x3011),x3012),x3013),x3013,x3011),x3012) % 0.49/0.66 [320]~P10(x3201,x3203,a1)+E(f8(f8(f8(a16,f9(x3201)),x3202),x3203),f9(x3201)) % 0.49/0.66 [328]P10(x3282,x3283,a1)+E(f13(x3281,f9(x3282),x3283),f9(f8(f8(f3(a1),x3282),x3281))) % 0.49/0.66 [347]~P1(x3471)+E(f8(f8(f3(x3471),f22(x3472,x3471)),f22(x3473,x3471)),f22(f8(f8(f3(a1),x3472),x3473),x3471)) % 0.49/0.66 [368]~P10(x3683,x3681,a1)+E(f8(f8(f8(a16,f9(x3681)),x3682),x3683),f9(f4(x3681,f6(a1),a1))) % 0.49/0.66 [414]~P31(f8(a2,x4141))+P31(f8(a2,f8(f8(f8(a16,x4141),f9(x4142)),x4143))) % 0.49/0.66 [425]~P10(x4252,f8(f8(f3(a1),x4253),f6(a1)),a1)+E(f8(f8(a14,f8(f8(a14,x4251),x4252)),f8(f8(f3(a1),x4253),f6(a1))),f8(f8(a14,f8(f8(a14,x4251),x4253)),x4252)) % 0.49/0.66 [477]P11(a11,x4771,f18(x4772,x4771,x4773),a30)+~P31(f8(f8(a11,f17(a12,f9(x4772),x4771,a30,a30)),x4773)) % 0.49/0.66 [480]E(f17(a12,f9(x4801),f18(x4801,x4802,x4803),a30,a30),x4803)+~P31(f8(f8(a11,f17(a12,f9(x4801),x4802,a30,a30)),x4803)) % 0.49/0.66 [434]P31(f8(x4341,x4342))+~P31(f8(x4341,f4(f8(f8(f3(a1),x4343),x4342),x4343,a1))) % 0.49/0.66 [400]~E(f20(x4003,x4001,x4002,x4004),f15(x4004))+E(x4001,f15(x4002)) % 0.49/0.66 [463]P13(x4631,x4632,f26(x4633,x4631,x4634,x4632))+~P8(x4631,f17(a12,x4634,x4632,a30,a30),x4633) % 0.49/0.66 [464]P13(x4641,x4642,f27(x4643,x4641,x4644,x4642))+~P8(x4641,f17(a12,x4644,x4642,a30,a30),x4643) % 0.49/0.66 [283]E(x2831,x2832)+~E(f8(f8(a12,x2833),x2831),f8(f8(a12,x2834),x2832)) % 0.49/0.66 [284]E(x2841,x2842)+~E(f8(f8(a24,x2843),x2841),f8(f8(a24,x2844),x2842)) % 0.49/0.66 [285]E(x2851,x2852)+~E(f8(f8(a12,x2851),x2853),f8(f8(a12,x2852),x2854)) % 0.49/0.66 [286]E(x2861,x2862)+~E(f8(f8(a24,x2861),x2863),f8(f8(a24,x2862),x2864)) % 0.49/0.66 [429]P8(x4291,x4292,f25(x4293,x4291,x4294,x4292))+~P8(x4291,f8(f8(a12,x4294),x4292),x4293) % 0.49/0.66 [435]P8(x4351,f10(x4352),f8(f8(a24,x4353),x4354))+~P8(f21(x4351,f7(a1),x4353,a31),x4352,x4354) % 0.49/0.66 [458]E(x4581,x4582)+~E(f17(a12,f10(x4583),x4581,a30,a30),f17(a12,f10(x4584),x4582,a30,a30)) % 0.49/0.66 [459]E(x4591,x4592)+~E(f17(a12,f9(x4593),x4591,a30,a30),f17(a12,f9(x4594),x4592,a30,a30)) % 0.49/0.66 [460]E(x4601,x4602)+~E(f17(a12,f10(x4601),x4603,a30,a30),f17(a12,f10(x4602),x4604,a30,a30)) % 0.49/0.66 [461]E(x4611,x4612)+~E(f17(a12,f9(x4611),x4613,a30,a30),f17(a12,f9(x4612),x4614,a30,a30)) % 0.49/0.66 [465]P13(x4651,x4652,f28(x4653,x4651,x4654,x4652))+~P8(x4651,f17(a12,f9(x4654),x4652,a30,a30),x4653) % 0.49/0.66 [470]~P8(x4701,f17(a12,x4702,x4704,a30,a30),x4703)+P8(x4701,x4702,f19(a24,f26(x4703,x4701,x4702,x4704),x4703,a31,a31)) % 0.49/0.66 [471]~P8(x4711,f17(a12,x4712,x4714,a30,a30),x4713)+P8(x4711,x4712,f19(a24,f27(x4713,x4711,x4712,x4714),x4713,a31,a31)) % 0.49/0.66 [472]~P8(x4721,f17(a12,f9(x4722),x4724,a30,a30),x4723)+P8(x4721,f9(x4722),f19(a24,f28(x4723,x4721,x4722,x4724),x4723,a31,a31)) % 0.49/0.66 [421]~P1(x4214)+E(f23(x4211,f8(f8(f3(a1),x4212),f6(a1)),x4213,x4214),f23(x4211,x4212,f8(x4211,x4213),x4214)) % 0.49/0.66 [450]~P8(x4501,f8(f8(a12,x4502),x4504),x4503)+P8(x4501,x4502,f8(f8(a24,f25(x4503,x4501,x4502,x4504)),x4503)) % 0.49/0.66 [369]~P15(x3691)+E(f8(f8(f3(x3691),x3692),f8(f8(f3(x3691),x3693),x3694)),f8(f8(f3(x3691),x3693),f8(f8(f3(x3691),x3692),x3694))) % 0.49/0.66 [370]~P24(x3701)+E(f8(f8(f3(x3701),x3702),f8(f8(f3(x3701),x3703),x3704)),f8(f8(f3(x3701),x3703),f8(f8(f3(x3701),x3702),x3704))) % 0.49/0.66 [371]~P16(x3711)+E(f8(f8(f3(x3711),x3712),f8(f8(f3(x3711),x3713),x3714)),f8(f8(f3(x3711),x3713),f8(f8(f3(x3711),x3712),x3714))) % 0.49/0.66 [438]~P31(f8(f8(a11,x4381),x4384))+P31(f8(f8(a11,f8(f8(f8(a16,x4381),x4382),x4383)),f8(f8(f8(a16,x4384),x4382),x4383))) % 0.49/0.66 [457]~P23(x4571)+E(f17(f3(x4571),f8(f8(f3(x4571),x4572),x4573),x4574,x4571,x4571),f8(f8(f3(x4571),x4572),f17(f3(x4571),x4573,x4574,x4571,x4571))) % 0.49/0.66 [405]~P6(x4051)+E(f8(f8(f3(x4051),f8(f8(f3(x4051),x4052),x4053)),x4054),f8(f8(f3(x4051),x4052),f8(f8(f3(x4051),x4053),x4054))) % 0.49/0.66 [406]~P24(x4061)+E(f8(f8(f3(x4061),f8(f8(f3(x4061),x4062),x4063)),x4064),f8(f8(f3(x4061),x4062),f8(f8(f3(x4061),x4063),x4064))) % 0.49/0.66 [407]~P16(x4071)+E(f8(f8(f3(x4071),f8(f8(f3(x4071),x4072),x4073)),x4074),f8(f8(f3(x4071),x4072),f8(f8(f3(x4071),x4073),x4074))) % 0.49/0.66 [418]~P24(x4181)+E(f8(f8(f3(x4181),f8(f8(f3(x4181),x4182),x4183)),x4184),f8(f8(f3(x4181),f8(f8(f3(x4181),x4182),x4184)),x4183)) % 0.49/0.66 [439]~P10(x4392,f8(f8(f3(a1),x4394),f6(a1)),a1)+E(f8(f8(f8(a16,f8(f8(a14,x4391),x4392)),f8(f8(a14,x4393),x4392)),f8(f8(f3(a1),x4394),f6(a1))),f8(f8(a14,f8(f8(f8(a16,x4391),x4393),x4394)),x4392)) % 0.49/0.66 [445]~P10(x4454,f8(f8(f3(a1),x4452),f6(a1)),a1)+E(f8(f8(f8(a16,f8(f8(a14,x4451),f8(f8(f3(a1),x4452),f6(a1)))),f8(f8(a14,x4453),x4452)),x4454),f8(f8(a14,f8(f8(f8(a16,x4451),x4453),x4454)),x4452)) % 0.49/0.66 [420]~P10(x4205,x4202,a1)+E(f8(f21(x4201,x4202,x4203,x4204),x4205),f8(x4201,x4205)) % 0.49/0.66 [426]~P8(x4261,x4264,x4265)+P8(f21(x4261,x4262,x4263,a31),f8(f8(a14,x4264),x4262),x4265) % 0.49/0.66 [468]~P13(x4681,x4684,x4685)+P13(f21(x4681,x4682,x4683,a31),f20(f5(a14,x4682,a30,a1,a30),x4684,a30,a30),x4685) % 0.49/0.66 [427]~P10(x4272,x4275,a1)+E(f8(f21(x4271,x4272,x4273,x4274),x4275),f8(x4271,f4(x4275,f6(a1),a1))) % 0.49/0.66 [428]~P24(x4281)+E(f8(f8(f3(x4281),f8(f8(f3(x4281),x4282),x4283)),f8(f8(f3(x4281),x4284),x4285)),f8(f8(f3(x4281),f8(f8(f3(x4281),x4282),x4284)),f8(f8(f3(x4281),x4283),x4285))) % 0.49/0.66 [462]~P10(x4623,f8(f8(f3(a1),x4624),f6(a1)),a1)+E(f8(f8(f8(a16,f8(f8(f8(a16,x4621),f8(f8(a14,x4622),x4623)),f8(f8(f3(a1),x4624),f6(a1)))),f8(f8(f8(a16,x4625),x4622),x4624)),x4623),f8(f8(f8(a16,f8(f8(f8(a16,x4621),x4625),x4623)),x4622),x4624)) % 0.49/0.66 [277]E(x2771,x2772)+P10(x2772,x2771,a1)+P10(x2771,x2772,a1) % 0.49/0.66 [258]~P28(x2582)+~P14(x2582)+E(f4(x2581,x2581,x2582),f7(x2582)) % 0.49/0.66 [309]E(x3091,x3092)+~E(f4(x3092,x3091,a1),f7(a1))+~E(f4(x3091,x3092,a1),f7(a1)) % 0.49/0.66 [317]~P2(x3171)+P10(f7(x3171),f22(x3172,x3171),x3171)+~P10(f7(a1),x3172,a1) % 0.49/0.66 [321]~P2(x3212)+~P10(f7(x3212),f22(x3211,x3212),x3212)+P10(f7(a1),x3211,a1) % 0.49/0.66 [384]P10(f4(x3841,x3842,a1),x3841,a1)+~P10(f7(a1),x3842,a1)+~P10(f7(a1),x3841,a1) % 0.49/0.66 [259]~P28(x2591)+~P14(x2591)+E(f8(f8(f3(x2591),x2592),f7(x2591)),x2592) % 0.49/0.66 [361]~P10(x3611,x3612,a1)+P10(f8(f8(f3(a1),x3611),f6(a1)),x3612,a1)+E(f8(f8(f3(a1),x3611),f6(a1)),x3612) % 0.49/0.66 [363]E(x3631,x3632)+P10(x3632,x3631,a1)+~P10(x3632,f8(f8(f3(a1),x3631),f6(a1)),a1) % 0.49/0.66 [365]E(x3651,x3652)+P10(x3651,x3652,a1)+~P10(x3651,f8(f8(f3(a1),x3652),f6(a1)),a1) % 0.49/0.66 [271]~P20(x2712)+E(x2711,f7(x2712))+~E(f8(f8(f3(x2712),x2711),x2711),f7(x2712)) % 0.49/0.66 [302]E(x3021,f7(a1))+E(x3022,f7(a1))+~E(f8(f8(f3(a1),x3022),x3021),f8(f8(f3(a1),f7(a1)),f6(a1))) % 0.49/0.66 [303]E(x3031,f7(a1))+E(x3032,f7(a1))+~E(f8(f8(f3(a1),f7(a1)),f6(a1)),f8(f8(f3(a1),x3032),x3031)) % 0.49/0.66 [330]E(x3301,f7(a1))+E(x3301,f8(f8(f3(a1),f7(a1)),f6(a1)))+~E(f8(f8(f3(a1),x3302),x3301),f8(f8(f3(a1),f7(a1)),f6(a1))) % 0.49/0.66 [331]E(x3311,f7(a1))+E(x3311,f8(f8(f3(a1),f7(a1)),f6(a1)))+~E(f8(f8(f3(a1),x3311),x3312),f8(f8(f3(a1),f7(a1)),f6(a1))) % 0.49/0.66 [332]E(x3321,f7(a1))+E(x3321,f8(f8(f3(a1),f7(a1)),f6(a1)))+~E(f8(f8(f3(a1),f7(a1)),f6(a1)),f8(f8(f3(a1),x3322),x3321)) % 0.49/0.66 [333]E(x3331,f7(a1))+E(x3331,f8(f8(f3(a1),f7(a1)),f6(a1)))+~E(f8(f8(f3(a1),f7(a1)),f6(a1)),f8(f8(f3(a1),x3331),x3332)) % 0.49/0.66 [353]~P20(x3531)+~P10(f7(x3531),x3532,x3531)+P10(f7(x3531),f8(f8(f3(x3531),x3532),x3532),x3531) % 0.49/0.66 [354]~P29(x3541)+~P10(x3542,f7(x3541),x3541)+P10(f8(f8(f3(x3541),x3542),x3542),f7(x3541),x3541) % 0.49/0.66 [355]~P20(x3551)+~P10(x3552,f7(x3551),x3551)+P10(f8(f8(f3(x3551),x3552),x3552),f7(x3551),x3551) % 0.49/0.66 [356]E(x3561,f8(f8(f3(a1),f7(a1)),f6(a1)))+E(x3562,f8(f8(f3(a1),f7(a1)),f6(a1)))+~E(f8(f8(f3(a1),x3562),x3561),f8(f8(f3(a1),f7(a1)),f6(a1))) % 0.49/0.66 [357]E(x3571,f8(f8(f3(a1),f7(a1)),f6(a1)))+E(x3572,f8(f8(f3(a1),f7(a1)),f6(a1)))+~E(f8(f8(f3(a1),f7(a1)),f6(a1)),f8(f8(f3(a1),x3572),x3571)) % 0.49/0.66 [378]~P29(x3782)+P10(x3781,f7(x3782),x3782)+~P10(f8(f8(f3(x3782),x3781),x3781),f7(x3782),x3782) % 0.49/0.66 [379]~P20(x3792)+P10(x3791,f7(x3792),x3792)+~P10(f8(f8(f3(x3792),x3791),x3791),f7(x3792),x3792) % 0.49/0.66 [380]~P20(x3801)+P10(f7(x3801),x3802,x3801)+~P10(f7(x3801),f8(f8(f3(x3801),x3802),x3802),x3801) % 0.49/0.66 [385]P10(f7(a1),x3851,a1)+P10(f7(a1),x3852,a1)+~P10(f7(a1),f8(f8(f3(a1),x3851),x3852),a1) % 0.49/0.66 [310]~P10(x3103,x3102,x3101)+~P25(x3101)+~P10(x3102,x3103,x3101) % 0.49/0.66 [312]~P10(x3123,x3122,x3121)+~P27(x3121)+~P10(x3122,x3123,x3121) % 0.49/0.66 [313]~P10(x3133,x3132,x3131)+~P26(x3131)+~P10(x3132,x3133,x3131) % 0.49/0.66 [245]~P7(x2453)+E(x2451,x2452)+~E(f22(x2451,x2453),f22(x2452,x2453)) % 0.49/0.66 [272]~P19(x2723)+E(x2721,x2722)+~E(f4(x2721,x2722,x2723),f7(x2723)) % 0.49/0.66 [273]~P15(x2733)+E(x2731,x2732)+~E(f4(x2731,x2732,x2733),f7(x2733)) % 0.49/0.66 [319]~P2(x3192)+~P10(x3191,x3193,a1)+P10(f22(x3191,x3192),f22(x3193,x3192),x3192) % 0.49/0.66 [338]~P2(x3383)+~P10(f22(x3381,x3383),f22(x3382,x3383),x3383)+P10(x3381,x3382,a1) % 0.49/0.66 [352]~P22(x3523)+~P10(x3521,x3522,x3523)+P10(f4(x3521,x3522,x3523),f7(x3523),x3523) % 0.49/0.66 [381]~P22(x3813)+P10(x3811,x3812,x3813)+~P10(f4(x3811,x3812,x3813),f7(x3813),x3813) % 0.49/0.66 [409]~P10(x4093,x4092,a1)+~P10(x4093,x4091,a1)+P10(f4(x4091,x4092,a1),f4(x4091,x4093,a1),a1) % 0.49/0.66 [374]~P10(x3741,x3743,a1)+~P10(x3743,x3742,a1)+P10(f8(f8(f3(a1),x3741),f6(a1)),x3742,a1) % 0.49/0.66 [417]~P10(x4172,x4173,a1)+~P31(f8(x4171,f4(x4172,x4173,a1)))+P31(f8(x4171,f7(a1))) % 0.49/0.66 [304]E(x3041,x3042)+P10(x3042,x3041,a1)+E(f8(f8(f8(a16,f9(x3041)),x3043),x3042),f9(x3041)) % 0.49/0.66 [474]~P31(f8(a2,x4742))+~P31(f8(a2,f17(a12,f8(f8(f8(a16,x4741),x4742),f7(a1)),x4743,a30,a30)))+P31(f8(a2,f17(a12,f8(f8(a12,f10(x4741)),x4742),x4743,a30,a30))) % 0.49/0.66 [314]~P15(x3144)+E(x3141,x3142)+~E(f4(x3143,x3143,x3144),f4(x3141,x3142,x3144)) % 0.49/0.66 [315]~P15(x3153)+E(x3151,x3152)+~E(f4(x3151,x3152,x3153),f4(x3154,x3154,x3153)) % 0.49/0.66 [351]P8(x3511,x3512,x3513)+~P8(x3511,x3514,x3513)+~P31(f8(f8(a11,x3514),x3512)) % 0.49/0.66 [305]~P17(x3053)+E(x3051,x3052)+~E(f8(f8(f3(x3053),x3054),x3051),f8(f8(f3(x3053),x3054),x3052)) % 0.49/0.66 [306]~P18(x3063)+E(x3061,x3062)+~E(f8(f8(f3(x3063),x3064),x3061),f8(f8(f3(x3063),x3064),x3062)) % 0.49/0.66 [307]~P18(x3073)+E(x3071,x3072)+~E(f8(f8(f3(x3073),x3071),x3074),f8(f8(f3(x3073),x3072),x3074)) % 0.49/0.66 [360]~P10(x3604,x3603,a1)+P10(x3601,x3602,a1)+~E(f8(f8(f3(a1),x3601),x3603),f8(f8(f3(a1),x3604),x3602)) % 0.49/0.66 [387]~P4(x3871)+~P10(x3872,x3874,x3871)+P10(f8(f8(f3(x3871),x3872),x3873),f8(f8(f3(x3871),x3874),x3873),x3871) % 0.49/0.66 [388]~P21(x3881)+~P10(x3882,x3884,x3881)+P10(f8(f8(f3(x3881),x3882),x3883),f8(f8(f3(x3881),x3884),x3883),x3881) % 0.49/0.66 [389]~P4(x3891)+~P10(x3893,x3894,x3891)+P10(f8(f8(f3(x3891),x3892),x3893),f8(f8(f3(x3891),x3892),x3894),x3891) % 0.49/0.66 [390]~P21(x3901)+~P10(x3903,x3904,x3901)+P10(f8(f8(f3(x3901),x3902),x3903),f8(f8(f3(x3901),x3902),x3904),x3901) % 0.49/0.66 [401]~P10(x4012,x4014,a1)+~P10(x4011,x4013,a1)+P10(f8(f8(f3(a1),x4011),x4012),f8(f8(f3(a1),x4013),x4014),a1) % 0.49/0.66 [415]~P21(x4153)+P10(x4151,x4152,x4153)+~P10(f8(f8(f3(x4153),x4154),x4151),f8(f8(f3(x4153),x4154),x4152),x4153) % 0.49/0.66 [416]~P21(x4163)+P10(x4161,x4162,x4163)+~P10(f8(f8(f3(x4163),x4161),x4164),f8(f8(f3(x4163),x4162),x4164),x4163) % 0.49/0.66 [469]~P13(x4691,x4693,x4695)+~P8(x4691,x4692,f19(a24,x4695,x4694,a31,a31))+P8(x4691,f17(a12,x4692,x4693,a30,a30),x4694) % 0.49/0.66 [402]~P8(x4021,x4023,x4025)+~P8(x4021,x4022,f8(f8(a24,x4025),x4024))+P8(x4021,f8(f8(a12,x4022),x4023),x4024) % 0.49/0.66 [473]E(x4731,x4732)+~P8(x4733,f17(a12,f9(x4734),x4735,a30,a30),x4731)+~P8(x4733,f17(a12,f9(x4734),x4735,a30,a30),x4732) % 0.49/0.66 [396]~P15(x3961)+E(f8(f8(f3(x3961),x3962),x3963),x3964)+~E(f8(f8(f3(x3961),x3962),f8(f8(f3(x3961),x3965),x3963)),f8(f8(f3(x3961),x3965),x3964)) % 0.49/0.66 [437]~P8(x4371,x4373,x4376)+~P8(f21(x4371,x4374,x4376,a31),x4372,x4375)+P8(x4371,f8(f8(f8(a16,x4372),x4373),x4374),x4375) % 0.49/0.66 [479]~P8(x4791,x4792,x4796)+~P13(f21(x4791,x4793,x4796,a31),x4794,x4795)+P13(x4791,f20(f5(f5(a16,x4792,a30,a30,f32(a1,a30)),x4793,a30,a1,a30),x4794,a30,a30),x4795) % 0.49/0.66 [287]P10(x2871,x2872,x2873)+~P29(x2873)+E(x2871,x2872)+P10(x2872,x2871,x2873) % 0.49/0.66 [291]P10(x2911,x2912,x2913)+~P26(x2913)+E(x2911,x2912)+P10(x2912,x2911,x2913) % 0.49/0.66 [275]~P28(x2753)+~P14(x2753)+E(x2751,x2752)+~E(f4(x2751,x2752,x2753),f7(x2753)) % 0.49/0.66 [274]~P28(x2742)+~P14(x2742)+E(x2741,f7(x2742))+~E(f8(f8(f3(x2742),x2743),x2741),x2743) % 0.49/0.66 [393]~P3(x3931)+~P10(f7(x3931),x3933,x3931)+~P10(f7(x3931),x3932,x3931)+P10(f7(x3931),f8(f8(f3(x3931),x3932),x3933),x3931) % 0.49/0.66 [394]~P3(x3941)+~P10(x3943,f7(x3941),x3941)+~P10(x3942,f7(x3941),x3941)+P10(f8(f8(f3(x3941),x3942),x3943),f7(x3941),x3941) % 0.49/0.66 [341]~P25(x3413)+~P10(x3411,x3414,x3413)+P10(x3411,x3412,x3413)+~P10(x3414,x3412,x3413) % 0.49/0.66 [342]~P27(x3423)+~P10(x3421,x3424,x3423)+P10(x3421,x3422,x3423)+~P10(x3424,x3422,x3423) % 0.49/0.66 [316]~P28(x3163)+~P14(x3163)+E(x3161,x3162)+~E(f8(f8(f3(x3163),x3164),x3161),f8(f8(f3(x3163),x3164),x3162)) % 0.49/0.66 [386]~P2(x3862)+~P10(x3861,x3864,x3862)+~P10(f7(x3862),x3863,x3862)+P10(x3861,f8(f8(f3(x3862),x3863),x3864),x3862) % 0.49/0.66 [376]~P22(x3763)+~P10(x3764,x3765,x3763)+P10(x3761,x3762,x3763)+~E(f4(x3764,x3765,x3763),f4(x3761,x3762,x3763)) % 0.49/0.66 [377]~P22(x3773)+~P10(x3774,x3775,x3773)+P10(x3771,x3772,x3773)+~E(f4(x3771,x3772,x3773),f4(x3774,x3775,x3773)) % 0.49/0.66 [411]~P4(x4111)+~P10(x4113,x4115,x4111)+~P10(x4112,x4114,x4111)+P10(f8(f8(f3(x4111),x4112),x4113),f8(f8(f3(x4111),x4114),x4115),x4111) % 0.49/0.66 [478]~P13(x4781,x4785,x4786)+P13(x4781,x4782,f29(x4783,x4784,x4781,x4782))+~P8(x4781,f17(a12,f9(x4787),x4785,a30,a30),x4784)+~P8(x4781,f17(a12,f17(a12,f9(x4787),x4785,a30,a30),x4782,a30,a30),x4783) % 0.49/0.66 [481]~P13(x4813,x4815,x4816)+~P8(x4813,f17(a12,f9(x4817),x4815,a30,a30),x4812)+~P8(x4813,f17(a12,f17(a12,f9(x4817),x4815,a30,a30),x4814,a30,a30),x4811)+E(f19(a24,f29(x4811,x4812,x4813,x4814),x4811,a31,a31),x4812) % 0.49/0.66 [440]~P8(x4406,x4402,x4405)+~P8(f21(x4406,x4403,x4405,a31),x4401,x4407)+~P31(f8(a2,x4402))+~P31(f8(a2,x4401))+~E(f8(f8(a24,x4404),x4405),a36)+P31(f8(a2,f8(f8(f8(a16,x4401),x4402),x4403))) % 0.49/0.66 [441]~P8(x4416,x4412,x4414)+~P8(f21(x4416,x4413,x4414,a31),x4411,x4417)+~P31(f8(a2,x4412))+~P31(f8(a2,x4411))+~E(f8(f8(a24,x4414),x4415),a36)+P31(f8(a2,f8(f8(f8(a16,x4411),x4412),x4413))) % 0.49/0.66 %EqnAxiom % 0.49/0.66 [1]E(x11,x11) % 0.49/0.66 [2]E(x22,x21)+~E(x21,x22) % 0.49/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.49/0.66 [4]~E(x41,x42)+E(f8(x41,x43),f8(x42,x43)) % 0.49/0.66 [5]~E(x51,x52)+E(f8(x53,x51),f8(x53,x52)) % 0.49/0.66 [6]~E(x61,x62)+E(f17(x61,x63,x64,x65,x66),f17(x62,x63,x64,x65,x66)) % 0.49/0.66 [7]~E(x71,x72)+E(f17(x73,x71,x74,x75,x76),f17(x73,x72,x74,x75,x76)) % 0.49/0.66 [8]~E(x81,x82)+E(f17(x83,x84,x81,x85,x86),f17(x83,x84,x82,x85,x86)) % 0.49/0.66 [9]~E(x91,x92)+E(f17(x93,x94,x95,x91,x96),f17(x93,x94,x95,x92,x96)) % 0.49/0.66 [10]~E(x101,x102)+E(f17(x103,x104,x105,x106,x101),f17(x103,x104,x105,x106,x102)) % 0.49/0.66 [11]~E(x111,x112)+E(f9(x111),f9(x112)) % 0.49/0.66 [12]~E(x121,x122)+E(f7(x121),f7(x122)) % 0.49/0.66 [13]~E(x131,x132)+E(f3(x131),f3(x132)) % 0.49/0.66 [14]~E(x141,x142)+E(f6(x141),f6(x142)) % 0.49/0.66 [15]~E(x151,x152)+E(f4(x151,x153,x154),f4(x152,x153,x154)) % 0.49/0.66 [16]~E(x161,x162)+E(f4(x163,x161,x164),f4(x163,x162,x164)) % 0.49/0.66 [17]~E(x171,x172)+E(f4(x173,x174,x171),f4(x173,x174,x172)) % 0.49/0.66 [18]~E(x181,x182)+E(f13(x181,x183,x184),f13(x182,x183,x184)) % 0.49/0.66 [19]~E(x191,x192)+E(f13(x193,x191,x194),f13(x193,x192,x194)) % 0.49/0.66 [20]~E(x201,x202)+E(f13(x203,x204,x201),f13(x203,x204,x202)) % 0.49/0.66 [21]~E(x211,x212)+E(f10(x211),f10(x212)) % 0.49/0.66 [22]~E(x221,x222)+E(f5(x221,x223,x224,x225,x226),f5(x222,x223,x224,x225,x226)) % 0.49/0.66 [23]~E(x231,x232)+E(f5(x233,x231,x234,x235,x236),f5(x233,x232,x234,x235,x236)) % 0.49/0.66 [24]~E(x241,x242)+E(f5(x243,x244,x241,x245,x246),f5(x243,x244,x242,x245,x246)) % 0.49/0.66 [25]~E(x251,x252)+E(f5(x253,x254,x255,x251,x256),f5(x253,x254,x255,x252,x256)) % 0.49/0.66 [26]~E(x261,x262)+E(f5(x263,x264,x265,x266,x261),f5(x263,x264,x265,x266,x262)) % 0.49/0.66 [27]~E(x271,x272)+E(f21(x271,x273,x274,x275),f21(x272,x273,x274,x275)) % 0.49/0.66 [28]~E(x281,x282)+E(f21(x283,x281,x284,x285),f21(x283,x282,x284,x285)) % 0.49/0.66 [29]~E(x291,x292)+E(f21(x293,x294,x291,x295),f21(x293,x294,x292,x295)) % 0.49/0.66 [30]~E(x301,x302)+E(f21(x303,x304,x305,x301),f21(x303,x304,x305,x302)) % 0.49/0.66 [31]~E(x311,x312)+E(f19(x311,x313,x314,x315,x316),f19(x312,x313,x314,x315,x316)) % 0.49/0.66 [32]~E(x321,x322)+E(f19(x323,x321,x324,x325,x326),f19(x323,x322,x324,x325,x326)) % 0.49/0.66 [33]~E(x331,x332)+E(f19(x333,x334,x331,x335,x336),f19(x333,x334,x332,x335,x336)) % 0.49/0.66 [34]~E(x341,x342)+E(f19(x343,x344,x345,x341,x346),f19(x343,x344,x345,x342,x346)) % 0.49/0.66 [35]~E(x351,x352)+E(f19(x353,x354,x355,x356,x351),f19(x353,x354,x355,x356,x352)) % 0.49/0.66 [36]~E(x361,x362)+E(f15(x361),f15(x362)) % 0.49/0.66 [37]~E(x371,x372)+E(f23(x371,x373,x374,x375),f23(x372,x373,x374,x375)) % 0.49/0.66 [38]~E(x381,x382)+E(f23(x383,x381,x384,x385),f23(x383,x382,x384,x385)) % 0.49/0.66 [39]~E(x391,x392)+E(f23(x393,x394,x391,x395),f23(x393,x394,x392,x395)) % 0.49/0.66 [40]~E(x401,x402)+E(f23(x403,x404,x405,x401),f23(x403,x404,x405,x402)) % 0.49/0.66 [41]~E(x411,x412)+E(f29(x411,x413,x414,x415),f29(x412,x413,x414,x415)) % 0.49/0.66 [42]~E(x421,x422)+E(f29(x423,x421,x424,x425),f29(x423,x422,x424,x425)) % 0.49/0.66 [43]~E(x431,x432)+E(f29(x433,x434,x431,x435),f29(x433,x434,x432,x435)) % 0.49/0.66 [44]~E(x441,x442)+E(f29(x443,x444,x445,x441),f29(x443,x444,x445,x442)) % 0.49/0.66 [45]~E(x451,x452)+E(f20(x451,x453,x454,x455),f20(x452,x453,x454,x455)) % 0.49/0.66 [46]~E(x461,x462)+E(f20(x463,x461,x464,x465),f20(x463,x462,x464,x465)) % 0.49/0.66 [47]~E(x471,x472)+E(f20(x473,x474,x471,x475),f20(x473,x474,x472,x475)) % 0.49/0.66 [48]~E(x481,x482)+E(f20(x483,x484,x485,x481),f20(x483,x484,x485,x482)) % 0.49/0.66 [49]~E(x491,x492)+E(f27(x491,x493,x494,x495),f27(x492,x493,x494,x495)) % 0.49/0.66 [50]~E(x501,x502)+E(f27(x503,x501,x504,x505),f27(x503,x502,x504,x505)) % 0.49/0.66 [51]~E(x511,x512)+E(f27(x513,x514,x511,x515),f27(x513,x514,x512,x515)) % 0.49/0.66 [52]~E(x521,x522)+E(f27(x523,x524,x525,x521),f27(x523,x524,x525,x522)) % 0.49/0.66 [53]~E(x531,x532)+E(f25(x531,x533,x534,x535),f25(x532,x533,x534,x535)) % 0.49/0.66 [54]~E(x541,x542)+E(f25(x543,x541,x544,x545),f25(x543,x542,x544,x545)) % 0.49/0.66 [55]~E(x551,x552)+E(f25(x553,x554,x551,x555),f25(x553,x554,x552,x555)) % 0.49/0.66 [56]~E(x561,x562)+E(f25(x563,x564,x565,x561),f25(x563,x564,x565,x562)) % 0.49/0.66 [57]~E(x571,x572)+E(f22(x571,x573),f22(x572,x573)) % 0.49/0.66 [58]~E(x581,x582)+E(f22(x583,x581),f22(x583,x582)) % 0.49/0.66 [59]~E(x591,x592)+E(f32(x591,x593),f32(x592,x593)) % 0.49/0.66 [60]~E(x601,x602)+E(f32(x603,x601),f32(x603,x602)) % 0.49/0.66 [61]~E(x611,x612)+E(f18(x611,x613,x614),f18(x612,x613,x614)) % 0.49/0.66 [62]~E(x621,x622)+E(f18(x623,x621,x624),f18(x623,x622,x624)) % 0.49/0.66 [63]~E(x631,x632)+E(f18(x633,x634,x631),f18(x633,x634,x632)) % 0.49/0.66 [64]~E(x641,x642)+E(f28(x641,x643,x644,x645),f28(x642,x643,x644,x645)) % 0.49/0.66 [65]~E(x651,x652)+E(f28(x653,x651,x654,x655),f28(x653,x652,x654,x655)) % 0.49/0.66 [66]~E(x661,x662)+E(f28(x663,x664,x661,x665),f28(x663,x664,x662,x665)) % 0.49/0.66 [67]~E(x671,x672)+E(f28(x673,x674,x675,x671),f28(x673,x674,x675,x672)) % 0.49/0.66 [68]~E(x681,x682)+E(f26(x681,x683,x684,x685),f26(x682,x683,x684,x685)) % 0.49/0.66 [69]~E(x691,x692)+E(f26(x693,x691,x694,x695),f26(x693,x692,x694,x695)) % 0.49/0.66 [70]~E(x701,x702)+E(f26(x703,x704,x701,x705),f26(x703,x704,x702,x705)) % 0.49/0.66 [71]~E(x711,x712)+E(f26(x713,x714,x715,x711),f26(x713,x714,x715,x712)) % 0.49/0.66 [72]~P1(x721)+P1(x722)+~E(x721,x722) % 0.49/0.66 [73]~P2(x731)+P2(x732)+~E(x731,x732) % 0.49/0.66 [74]~P30(x741)+P30(x742)+~E(x741,x742) % 0.49/0.66 [75]~P3(x751)+P3(x752)+~E(x751,x752) % 0.49/0.66 [76]~P4(x761)+P4(x762)+~E(x761,x762) % 0.49/0.66 [77]~P5(x771)+P5(x772)+~E(x771,x772) % 0.49/0.66 [78]~P21(x781)+P21(x782)+~E(x781,x782) % 0.49/0.66 [79]~P6(x791)+P6(x792)+~E(x791,x792) % 0.49/0.66 [80]~P7(x801)+P7(x802)+~E(x801,x802) % 0.49/0.66 [81]~P23(x811)+P23(x812)+~E(x811,x812) % 0.49/0.66 [82]~P24(x821)+P24(x822)+~E(x821,x822) % 0.49/0.66 [83]~P16(x831)+P16(x832)+~E(x831,x832) % 0.49/0.66 [84]~P17(x841)+P17(x842)+~E(x841,x842) % 0.49/0.66 [85]~P18(x851)+P18(x852)+~E(x851,x852) % 0.49/0.66 [86]~P25(x861)+P25(x862)+~E(x861,x862) % 0.49/0.66 [87]~P27(x871)+P27(x872)+~E(x871,x872) % 0.49/0.66 [88]~P26(x881)+P26(x882)+~E(x881,x882) % 0.49/0.66 [89]~P31(x891)+P31(x892)+~E(x891,x892) % 0.49/0.66 [90]P13(x902,x903,x904)+~E(x901,x902)+~P13(x901,x903,x904) % 0.49/0.66 [91]P13(x913,x912,x914)+~E(x911,x912)+~P13(x913,x911,x914) % 0.49/0.66 [92]P13(x923,x924,x922)+~E(x921,x922)+~P13(x923,x924,x921) % 0.49/0.66 [93]~P32(x931)+P32(x932)+~E(x931,x932) % 0.49/0.66 [94]P8(x942,x943,x944)+~E(x941,x942)+~P8(x941,x943,x944) % 0.49/0.66 [95]P8(x953,x952,x954)+~E(x951,x952)+~P8(x953,x951,x954) % 0.49/0.66 [96]P8(x963,x964,x962)+~E(x961,x962)+~P8(x963,x964,x961) % 0.49/0.66 [97]P10(x972,x973,x974)+~E(x971,x972)+~P10(x971,x973,x974) % 0.49/0.66 [98]P10(x983,x982,x984)+~E(x981,x982)+~P10(x983,x981,x984) % 0.49/0.66 [99]P10(x993,x994,x992)+~E(x991,x992)+~P10(x993,x994,x991) % 0.49/0.66 [100]P12(x1002,x1003,x1004)+~E(x1001,x1002)+~P12(x1001,x1003,x1004) % 0.49/0.66 [101]P12(x1013,x1012,x1014)+~E(x1011,x1012)+~P12(x1013,x1011,x1014) % 0.49/0.66 [102]P12(x1023,x1024,x1022)+~E(x1021,x1022)+~P12(x1023,x1024,x1021) % 0.49/0.66 [103]P9(x1032,x1033,x1034)+~E(x1031,x1032)+~P9(x1031,x1033,x1034) % 0.49/0.66 [104]P9(x1043,x1042,x1044)+~E(x1041,x1042)+~P9(x1043,x1041,x1044) % 0.49/0.66 [105]P9(x1053,x1054,x1052)+~E(x1051,x1052)+~P9(x1053,x1054,x1051) % 0.49/0.66 [106]~P22(x1061)+P22(x1062)+~E(x1061,x1062) % 0.49/0.66 [107]~P20(x1071)+P20(x1072)+~E(x1071,x1072) % 0.49/0.66 [108]~P19(x1081)+P19(x1082)+~E(x1081,x1082) % 0.49/0.66 [109]~P29(x1091)+P29(x1092)+~E(x1091,x1092) % 0.49/0.66 [110]~P28(x1101)+P28(x1102)+~E(x1101,x1102) % 0.49/0.66 [111]~P15(x1111)+P15(x1112)+~E(x1111,x1112) % 0.49/0.66 [112]~P14(x1121)+P14(x1122)+~E(x1121,x1122) % 0.49/0.66 [113]P11(x1132,x1133,x1134,x1135)+~E(x1131,x1132)+~P11(x1131,x1133,x1134,x1135) % 0.49/0.66 [114]P11(x1143,x1142,x1144,x1145)+~E(x1141,x1142)+~P11(x1143,x1141,x1144,x1145) % 0.49/0.66 [115]P11(x1153,x1154,x1152,x1155)+~E(x1151,x1152)+~P11(x1153,x1154,x1151,x1155) % 0.49/0.66 [116]P11(x1163,x1164,x1165,x1162)+~E(x1161,x1162)+~P11(x1163,x1164,x1165,x1161) % 0.49/0.66 % 0.49/0.66 %------------------------------------------- % 0.49/0.66 cnf(514,plain, % 0.49/0.66 ($false), % 0.49/0.66 inference(scs_inference,[],[212,208,432,463]), % 0.49/0.66 ['proof']). % 0.49/0.66 % SZS output end Proof % 0.49/0.66 % Total time :0.033512s %------------------------------------------------------------------------------