%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL818-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n011.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.56s 0.71s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL818-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.34 % Computer : n011.cluster.edu % 0.08/0.34 % Model : x86_64 x86_64 % 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.34 % Memory : 8046.5625MB % 0.08/0.34 % OS : Linux 6.8.0-71-generic % 0.08/0.34 % CPULimit : 300 % 0.08/0.34 % WCLimit : 300 % 0.08/0.34 % DateTime : Fri Sep 4 19:19:43 UTC 2026 % 0.08/0.34 % CPUTime : % 0.24/0.50 start to proof:theBenchmark % 0.45/0.66 %------------------------------------------- % 0.45/0.66 % File :CSE---1.7 % 0.45/0.66 % Problem :theBenchmark % 0.45/0.66 % Transform :cnf % 0.45/0.66 % Format :tptp:raw % 0.45/0.66 % Command :java -jar mcs_scs.jar %d %s % 0.45/0.66 % 0.45/0.66 % Result :Theorem 0.073739s % 0.45/0.66 % Output :CNFRefutation 0.073739s % 0.45/0.66 %------------------------------------------- % 0.45/0.67 %------------------------------------------------------------------------------ % 0.45/0.67 % File : LCL818-1 : TPTP v9.3.1. Released v4.1.0. % 0.45/0.67 % Domain : Logic Calculi % 0.45/0.67 % Problem : Strong normalization of typed lambda calculus 186_15 % 0.45/0.67 % Version : Especial. % 0.45/0.67 % English : % 0.45/0.67 % 0.45/0.67 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.45/0.67 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.45/0.67 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.45/0.67 % Source : [Nip10] % 0.45/0.67 % Names : StrongNorm-186_15 [Nip10] % 0.45/0.67 % 0.45/0.67 % Status : Unsatisfiable % 0.45/0.67 % Rating : 0.17 v9.3.0, 0.09 v9.1.0, 0.10 v8.2.0, 0.14 v8.1.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.08 v7.1.0, 0.00 v7.0.0, 0.20 v6.4.0, 0.13 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.14 v6.0.0, 0.20 v5.5.0, 0.45 v5.3.0, 0.44 v5.1.0, 0.53 v5.0.0, 0.36 v4.1.0 % 0.45/0.67 % Syntax : Number of clauses : 398 ( 139 unt; 30 nHn; 226 RR) % 0.45/0.67 % Number of literals : 761 ( 285 equ; 359 neg) % 0.45/0.67 % Maximal clause size : 6 ( 1 avg) % 0.45/0.67 % Maximal term depth : 6 ( 2 avg) % 0.45/0.67 % Number of predicates : 30 ( 29 usr; 0 prp; 1-4 aty) % 0.45/0.67 % Number of functors : 65 ( 65 usr; 24 con; 0-5 aty) % 0.45/0.67 % Number of variables : 1184 ( 203 sgn) % 0.45/0.67 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.45/0.67 % 0.45/0.67 % Comments : % 0.45/0.67 %------------------------------------------------------------------------------ % 0.45/0.67 cnf(cls_lift__subst__lt_0,axiom, % 0.45/0.67 ( c_Lambda_Olift(c_Lambda_Osubst(V_t,V_s,V_j),V_i) = c_Lambda_Osubst(c_Lambda_Olift(V_t,V_i),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.45/0.67 | ~ 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.45/0.67 % 0.45/0.67 cnf(cls_lift__subst_0,axiom, % 0.45/0.67 ( c_Lambda_Olift(c_Lambda_Osubst(V_t,V_s,V_j),V_i) = c_Lambda_Osubst(c_Lambda_Olift(V_t,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat))),c_Lambda_Olift(V_s,V_i),V_j) % 0.45/0.67 | ~ 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.45/0.67 % 0.45/0.67 cnf(cls_lift_Osimps_I3_J_0,axiom, % 0.45/0.67 c_Lambda_Olift(c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Olift(V_s,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_less__add__one_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.67 | 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.45/0.67 % 0.45/0.67 cnf(cls_zero__less__one_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.67 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oone__class_Oone(T_a),T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_liftn_Osimps_I3_J_0,axiom, % 0.45/0.67 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.45/0.67 % 0.45/0.67 cnf(cls_one__neq__zero_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Ozero__neq__one(T_a) % 0.45/0.67 | c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_not__one__less__zero_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.67 | ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_substn_Osimps_I3_J_0,axiom, % 0.45/0.67 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.45/0.67 % 0.45/0.67 cnf(cls_of__nat__1_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.45/0.67 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oone__class_Oone(tc_nat),T_a) = c_HOL_Oone__class_Oone(T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_zero__neq__one_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Ozero__neq__one(T_a) % 0.45/0.67 | c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_zero__less__two_0,axiom, % 0.45/0.67 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.67 | 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.45/0.67 % 0.45/0.67 cnf(cls_lift_Osimps_I1_J_1,axiom, % 0.45/0.67 ( 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.45/0.67 | c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_types__snocE_1,axiom, % 0.45/0.67 ( c_Type_Otypings(V_e,V_ts,c_Type_Osko__Type__Xtypes__snocE__1__1(V_Ts,V_e,V_t,V_ts)) % 0.45/0.67 | ~ c_Type_Otypings(V_e,c_List_Oappend(V_ts,c_List_Olist_OCons(V_t,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),V_Ts) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_subst__Abs_0,axiom, % 0.45/0.67 c_Lambda_Osubst(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(V_t,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.45/0.67 % 0.45/0.67 cnf(cls_types__snocE_2,axiom, % 0.45/0.67 ( c_Type_Otyping(V_e,V_t,c_Type_Osko__Type__Xtypes__snocE__1__2(V_Ts,V_e,V_t,V_ts)) % 0.45/0.67 | ~ c_Type_Otypings(V_e,c_List_Oappend(V_ts,c_List_Olist_OCons(V_t,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),V_Ts) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_Snoc__step1__SnocD_1,axiom, % 0.45/0.67 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.45/0.67 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.45/0.67 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_Snoc__step1__SnocD_3,axiom, % 0.45/0.67 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.45/0.67 | V_y = V_x % 0.45/0.67 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_Snoc__step1__SnocD_2,axiom, % 0.45/0.67 ( V_ys = V_xs % 0.45/0.67 | V_y = V_x % 0.45/0.67 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_listsum_0,axiom, % 0.45/0.67 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.45/0.67 | c_List_Olistsum(V_xs,T_a) = c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a),V_xs,T_a,T_a) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_add__gr__0_1,axiom, % 0.45/0.67 ( 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.45/0.67 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_add__gr__0_2,axiom, % 0.45/0.67 ( 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.45/0.67 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_Nat_Oadd__0__right_0,axiom, % 0.45/0.67 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat)) = V_m ). % 0.45/0.67 % 0.45/0.67 cnf(cls_plus__nat_Oadd__0_0,axiom, % 0.45/0.67 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = V_n ). % 0.45/0.67 % 0.45/0.67 cnf(cls_natgb_Oadd__r0__iff_1,axiom, % 0.45/0.67 V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_rtranclp__idemp_0,axiom, % 0.45/0.67 c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(V_r,T_a),T_a) = c_Transitive__Closure_Ortranclp(V_r,T_a) ). % 0.45/0.67 % 0.45/0.67 cnf(cls_App__eq__foldl__conv_1,axiom, % 0.45/0.67 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) % 0.45/0.67 | V_ts = c_List_Oappend(c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(V_r,V_s,V_t,V_ts),c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) % 0.45/0.67 | V_ts = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.45/0.67 % 0.45/0.68 cnf(cls_replicate__eq__replicate_1,axiom, % 0.45/0.68 ( c_List_Oreplicate(V_m,V_x,T_a) != c_List_Oreplicate(V_n,V_y,T_a) % 0.45/0.68 | V_x = V_y % 0.45/0.68 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_replicate__eq__replicate_2,axiom, % 0.45/0.68 c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) = c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_y,T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.45/0.68 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.68 | ~ 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.45/0.68 % 0.45/0.68 cnf(cls_Cons__step1__Cons_0,axiom, % 0.45/0.68 ( V_x = V_y % 0.45/0.68 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.45/0.68 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_nat__add__left__cancel_0,axiom, % 0.45/0.68 ( 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.45/0.68 | V_m = V_n ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_nat__add__right__cancel_0,axiom, % 0.45/0.68 ( 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.45/0.68 | V_m = V_n ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_natgb_Oadd__cancel_0,axiom, % 0.45/0.68 ( 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.45/0.68 | V_y = V_z ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_rtranclp__converseI_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_rtranclp__converseD_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_conversepD_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(V_r,V_b),V_a)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_conversep__iff_1,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_a)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_conversep_Ocases_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(V_r,V_a2),V_a1)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a1),V_a2)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_conversep_Ointros_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_b),V_a)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__gr__0_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.45/0.68 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.45/0.68 | ~ 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.45/0.68 % 0.45/0.68 cnf(cls_nat__add__assoc_0,axiom, % 0.45/0.68 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.45/0.68 % 0.45/0.68 cnf(cls_nat__add__left__commute_0,axiom, % 0.45/0.68 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.45/0.68 % 0.45/0.68 cnf(cls_add__is__0_2,axiom, % 0.45/0.68 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.45/0.68 % 0.45/0.68 cnf(cls_append__step1I_0,axiom, % 0.45/0.68 ( ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.45/0.68 | c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,V_x,T_a),c_List_Oappend(V_xs,V_x,T_a),T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_append__step1I_1,axiom, % 0.45/0.68 ( c_ListOrder_Ostep1(V_r,c_List_Oappend(V_x,V_vs,T_a),c_List_Oappend(V_x,V_us,T_a),T_a) % 0.45/0.68 | ~ c_ListOrder_Ostep1(V_r,V_vs,V_us,T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Var_I3_J_0,axiom, % 0.45/0.68 hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_rotate__simps_0,axiom, % 0.45/0.68 c_List_Orotate1(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Cons__step1__Cons_2,axiom, % 0.45/0.68 ( V_x = V_y % 0.45/0.68 | V_xs = V_ys % 0.45/0.68 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Cons__step1__Cons_4,axiom, % 0.45/0.68 ( ~ hBOOL(hAPP(hAPP(V_r,V_y),V_xa)) % 0.45/0.68 | c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_x,T_a),c_List_Olist_OCons(V_xa,V_x,T_a),T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_replicate__eq__replicate_0,axiom, % 0.45/0.68 ( c_List_Oreplicate(V_m,V_x,T_a) != c_List_Oreplicate(V_n,V_y,T_a) % 0.45/0.68 | V_m = V_n ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_rtranclp_Ortrancl__refl_0,axiom, % 0.45/0.68 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_a)) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Nitpick_Ortranclp__def_1,axiom, % 0.45/0.68 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_x)) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_accp__downwards_0,axiom, % 0.45/0.68 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) % 0.45/0.68 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_accp__downwards__aux_0,axiom, % 0.45/0.68 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.45/0.68 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_rtranclp__trans_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_z)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_z)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_IT__implies__termi_0,axiom, % 0.45/0.68 ( c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_t,tc_Lambda_OdB) % 0.45/0.68 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_termi__implies__IT_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(c_InductTermi_OIT,V_r)) % 0.45/0.68 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_r,tc_Lambda_OdB) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_rotate1__is__Nil__conv_0,axiom, % 0.45/0.68 ( c_List_Orotate1(V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.45/0.68 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_termination__basic__simps_I1_J_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(V_x,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z),tc_nat) % 0.45/0.68 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_termination__basic__simps_I2_J_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(V_x,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z),tc_nat) % 0.45/0.68 | ~ c_HOL_Oord__class_Oless(V_x,V_z,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__lessD1_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) % 0.45/0.68 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_k,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_trans__less__add1_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_m),tc_nat) % 0.45/0.68 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_trans__less__add2_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_j),tc_nat) % 0.45/0.68 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_nat__add__commute_0,axiom, % 0.45/0.68 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.45/0.68 % 0.45/0.68 cnf(cls_less__add__eq__less_0,axiom, % 0.45/0.68 ( 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.45/0.68 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.45/0.68 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_of__nat__eq__iff_0,axiom, % 0.45/0.68 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.45/0.68 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.45/0.68 | V_m = V_n ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__eq__self__zero_0,axiom, % 0.45/0.68 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != V_m % 0.45/0.68 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_natgb_Oadd__r0__iff_0,axiom, % 0.45/0.68 ( V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a) % 0.45/0.68 | V_a = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__is__0_0,axiom, % 0.45/0.68 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.45/0.68 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__is__0_1,axiom, % 0.45/0.68 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.45/0.68 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_r__into__rtranclp_0,axiom, % 0.45/0.68 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) % 0.45/0.68 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_not__Nil__step1_0,axiom, % 0.45/0.68 ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_not__step1__Nil_0,axiom, % 0.45/0.68 ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_conversep__eq_0,axiom, % 0.45/0.68 c_Predicate_Oconversep(c_fequal(T_a),T_a,T_a) = c_fequal(T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Cons__step1__Cons_3,axiom, % 0.45/0.68 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.45/0.68 | V_xs = V_ys % 0.45/0.68 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_listsum_Osimps_I2_J_0,axiom, % 0.45/0.68 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.45/0.68 | c_List_Olistsum(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_List_Olistsum(V_xs,T_a)) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_append__replicate__commute_0,axiom, % 0.45/0.68 c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),c_List_Oreplicate(V_k,V_x,T_a),T_a) = c_List_Oappend(c_List_Oreplicate(V_k,V_x,T_a),c_List_Oreplicate(V_n,V_x,T_a),T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__less__mono_0,axiom, % 0.45/0.68 ( 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.45/0.68 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.45/0.68 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_of__nat__less__iff_1,axiom, % 0.45/0.68 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.68 | 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.45/0.68 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_of__nat__less__iff_0,axiom, % 0.45/0.68 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.68 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.45/0.68 | ~ 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.45/0.68 % 0.45/0.68 cnf(cls_replicate__add_0,axiom, % 0.45/0.68 c_List_Oreplicate(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m),V_x,T_a) = c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),c_List_Oreplicate(V_m,V_x,T_a),T_a) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_conversep__conversep_0,axiom, % 0.45/0.68 c_Predicate_Oconversep(c_Predicate_Oconversep(V_r,T_a,T_b),T_b,T_a) = V_r ). % 0.45/0.68 % 0.45/0.68 cnf(cls_not__add__less1_0,axiom, % 0.45/0.68 ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_i,tc_nat) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_not__add__less2_0,axiom, % 0.45/0.68 ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),V_i,tc_nat) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_add__less__mono1_0,axiom, % 0.45/0.68 ( 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.45/0.68 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_nat__add__left__cancel__less_0,axiom, % 0.45/0.68 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.45/0.68 | ~ 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.45/0.68 % 0.45/0.68 cnf(cls_nat__add__left__cancel__less_1,axiom, % 0.45/0.68 ( 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.45/0.68 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Cons__step1__Cons_1,axiom, % 0.45/0.68 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.45/0.68 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.45/0.68 | ~ c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_y,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ) ). % 0.45/0.68 % 0.45/0.68 cnf(cls_Cons__step1__Cons_5,axiom, % 0.45/0.69 ( c_ListOrder_Ostep1(V_r,c_List_Olist_OCons(V_x,V_ys,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) % 0.45/0.69 | ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_of__nat__add_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.45/0.69 | 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.45/0.69 % 0.45/0.69 cnf(cls_listsum__append_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.45/0.69 | c_List_Olistsum(c_List_Oappend(V_xs,V_ys,T_a),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_List_Olistsum(V_xs,T_a)),c_List_Olistsum(V_ys,T_a)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_converse__rtranclp__into__rtranclp_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_c)) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_c)) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_b)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_accp_Ocases_0,axiom, % 0.45/0.69 ( c_Wellfounded_Oaccp(V_r,V_y,T_a) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(V_r,V_y),V_a)) % 0.45/0.69 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_accp__downward_0,axiom, % 0.45/0.69 ( c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) % 0.45/0.69 | ~ c_Wellfounded_Oaccp(V_r,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_of__nat__0_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.45/0.69 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_listsum_Osimps_I1_J_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.45/0.69 | c_List_Olistsum(c_List_Olist_ONil(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_replicate__empty_1,axiom, % 0.45/0.69 c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) = c_List_Olist_ONil(T_a) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_empty__replicate_1,axiom, % 0.45/0.69 c_List_Olist_ONil(T_a) = c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_replicate__empty_0,axiom, % 0.45/0.69 ( c_List_Oreplicate(V_n,V_x,T_a) != c_List_Olist_ONil(T_a) % 0.45/0.69 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_empty__replicate_0,axiom, % 0.45/0.69 ( c_List_Olist_ONil(T_a) != c_List_Oreplicate(V_n,V_x,T_a) % 0.45/0.69 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_replicate__app__Cons__same_0,axiom, % 0.45/0.69 c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(c_List_Oreplicate(V_n,V_x,T_a),V_xs,T_a),T_a) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_rtrancl__beta__App_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),hAPP(hAPP(c_Lambda_OdB_OApp,V_s_H),V_t_H))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_rtrancl__beta__AppL_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),hAPP(hAPP(c_Lambda_OdB_OApp,V_s_H),V_t))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_rtrancl__beta__AppR_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t_H))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_rtrancl__beta__Abs_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_s_H))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_subst__preserves__beta2_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_t,V_r,V_i)),c_Lambda_Osubst(V_t,V_s,V_i))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_subst__preserves__beta_H_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_r,V_t,V_i)),c_Lambda_Osubst(V_s,V_t,V_i))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_subst__preserves__beta2_H_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_t,V_r,V_i)),c_Lambda_Osubst(V_t,V_s,V_i))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_subject__reduction_H_0,axiom, % 0.45/0.69 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.45/0.69 | ~ c_Type_Otyping(V_e,V_t,V_T) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_lift__preserves__beta_H_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_rotate__simps_1,axiom, % 0.45/0.69 c_List_Orotate1(c_List_Olist_OCons(V_x,V_xs,T_b),T_b) = c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_b),T_b),T_b) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_Snoc__step1__SnocD_0,axiom, % 0.45/0.69 ( V_ys = V_xs % 0.45/0.69 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.45/0.69 | ~ c_ListOrder_Ostep1(V_r,c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_replicate__append__same_0,axiom, % 0.45/0.69 c_List_Oappend(c_List_Oreplicate(V_i,V_x,T_a),c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Oreplicate(V_i,V_x,T_a),T_a) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_listsum__foldr_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.45/0.69 | c_List_Olistsum(V_xs,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.45/0.69 % 0.45/0.69 cnf(cls_double__induction__lemma_0,axiom, % 0.45/0.69 ( ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) % 0.45/0.69 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_s,tc_Lambda_OdB) % 0.45/0.69 | c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),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),tc_Lambda_OdB) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_apps__preserves__beta2_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,V_r,V_ss,tc_Lambda_OdB,tc_Lambda_OdB)),c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.45/0.69 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_apps__preserves__betas_0,axiom, % 0.45/0.69 ( 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.45/0.69 | ~ c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,V_ss,tc_Lambda_OdB) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_App__eq__foldl__conv_2,axiom, % 0.45/0.69 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) % 0.45/0.69 | V_r = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(V_r,V_s,V_t,V_ts),tc_Lambda_OdB,tc_Lambda_OdB) % 0.45/0.69 | V_ts = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_liftn_Osimps_I1_J_1,axiom, % 0.45/0.69 ( 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.45/0.69 | c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.45/0.69 | ~ 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.45/0.69 % 0.45/0.69 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_App__eq__foldl__conv_3,axiom, % 0.45/0.69 ( c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB) = c_List_Olist_ONil(tc_Lambda_OdB) % 0.45/0.69 | hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_x,tc_Lambda_OdB,tc_Lambda_OdB)),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_x,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_app__last_0,axiom, % 0.45/0.69 hAPP(hAPP(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB)),V_u) = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Oappend(V_ts,c_List_Olist_OCons(V_u,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_App__eq__foldl__conv_5,axiom, % 0.45/0.69 ( V_r != c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s),V_xa,tc_Lambda_OdB,tc_Lambda_OdB) % 0.45/0.69 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s),c_List_Oappend(V_xa,c_List_Olist_OCons(V_s,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_Var_I4_J_0,axiom, % 0.45/0.69 c_Type_Otyping(v_ea______,v_ua______,v_T____) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_head__Var__reduction_0,axiom, % 0.45/0.69 ( 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.45/0.69 | ~ 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.45/0.69 % 0.45/0.69 cnf(cls_substn_Osimps_I1_J_2,axiom, % 0.45/0.69 ( c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.45/0.69 | V_i = V_k % 0.45/0.69 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_liftn_Osimps_I1_J_0,axiom, % 0.45/0.69 ( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.45/0.69 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_foldr__conv__foldl_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.45/0.69 | 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.45/0.69 % 0.45/0.69 cnf(cls_subst__lt_0,axiom, % 0.45/0.69 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_subst__Var_2,axiom, % 0.45/0.69 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.45/0.69 | V_i = V_k % 0.45/0.69 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_subst__Var_1,axiom, % 0.45/0.69 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.45/0.69 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.45/0.69 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.45/0.69 % 0.45/0.69 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.45/0.69 ( 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.45/0.69 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_foldl__absorb0_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.45/0.69 | 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.45/0.69 % 0.45/0.69 cnf(cls_order__less__asym_H_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Opreorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_order__less__asym_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Opreorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.45/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_xt1_I9_J_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Oorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_add__less__cancel__left_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.45/0.69 | ~ 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.45/0.69 % 0.45/0.69 cnf(cls_add__less__cancel__left_1,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_add__strict__left__mono_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_add__less__cancel__right_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.45/0.69 | ~ 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.45/0.69 % 0.45/0.69 cnf(cls_add__less__cancel__right_1,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_add__strict__right__mono_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_pos__add__strict_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_b,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_shift__gt_0,axiom, % 0.45/0.69 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,V_j) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_neq0__conv_1,axiom, % 0.45/0.69 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_append__in__listsp__conv_2,axiom, % 0.45/0.69 ( c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) % 0.45/0.69 | ~ c_List_Olistsp(V_A,V_ys,T_a) % 0.45/0.69 | ~ c_List_Olistsp(V_A,V_xs,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_gr0I_0,axiom, % 0.45/0.69 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.45/0.69 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_add__strict__mono_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.45/0.69 | V_x = V_y % 0.45/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_linorder__less__linear_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.45/0.69 | V_x = V_y % 0.45/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_linorder__neqE_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.45/0.69 | V_x = V_y ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_linorder__neqE__nat_0,axiom, % 0.45/0.69 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.45/0.69 | V_x = V_y ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_nat__less__cases_0,axiom, % 0.45/0.69 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.45/0.69 | V_m = V_n % 0.45/0.69 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_nat__neq__iff_0,axiom, % 0.45/0.69 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.45/0.69 | V_m = V_n ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.45/0.69 | V_x = V_y % 0.45/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.45/0.69 | V_x = V_y ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_add__pos__pos_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_order__less__irrefl_0,axiom, % 0.45/0.69 ( ~ class_Orderings_Opreorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_linorder__neq__iff_1,axiom, % 0.45/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_order__less__le_1,axiom, % 0.45/0.69 ( ~ class_Orderings_Oorder(T_a) % 0.45/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_less__not__refl_0,axiom, % 0.45/0.69 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_nat__less__le_1,axiom, % 0.45/0.69 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_even__less__0__iff_1,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_even__less__0__iff_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.45/0.69 | ~ 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.45/0.69 % 0.45/0.69 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.45/0.69 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.45/0.69 | ~ 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.45/0.69 % 0.45/0.69 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.45/0.69 | 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.45/0.69 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_double__eq__0__iff_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.45/0.69 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.45/0.69 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.45/0.69 | ~ class_Int_Onumber__ring(T_a) % 0.45/0.69 | V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_a) % 0.45/0.69 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.45/0.69 % 0.45/0.69 cnf(cls_foldl__assoc_0,axiom, % 0.45/0.69 ( ~ class_OrderedGroup_Osemigroup__add(T_a) % 0.45/0.69 | 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.45/0.69 % 0.45/0.69 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.45/0.69 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.69 | 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.45/0.69 % 0.45/0.70 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_listsp_ONil_0,axiom, % 0.45/0.70 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_append__in__listsp__conv_1,axiom, % 0.45/0.70 ( c_List_Olistsp(V_A,V_ys,T_a) % 0.45/0.70 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_append__in__listsp__conv_0,axiom, % 0.45/0.70 ( c_List_Olistsp(V_A,V_xs,T_a) % 0.45/0.70 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_double__eq__0__iff_1,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_order__less__trans_0,axiom, % 0.45/0.70 ( ~ class_Orderings_Opreorder(T_a) % 0.45/0.70 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.45/0.70 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.45/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_xt1_I10_J_0,axiom, % 0.45/0.70 ( ~ class_Orderings_Oorder(T_a) % 0.45/0.70 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.45/0.70 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.45/0.70 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_add__cancel__21_1,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.45/0.70 | 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.45/0.70 % 0.45/0.70 cnf(cls_gr__implies__not0_0,axiom, % 0.45/0.70 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_not__less0_0,axiom, % 0.45/0.70 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_add__cancel__21_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.45/0.70 | 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.45/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) = V_u ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_add__neg__neg_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.45/0.70 | 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.45/0.70 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.45/0.70 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.45/0.70 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.45/0.70 | ~ class_Int_Onumber__ring(T_a) % 0.45/0.70 | 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.45/0.70 | V_y = V_z ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_add__imp__eq_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.45/0.70 | 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.45/0.70 | V_b = V_c ) ). % 0.45/0.70 % 0.45/0.70 cnf(cls_add__left__cancel_0,axiom, % 0.45/0.70 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.56/0.70 | 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.56/0.70 | V_b = V_c ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_add__right__cancel_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.56/0.70 | 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.56/0.70 | V_b = V_c ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.56/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.56/0.70 | 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.56/0.70 % 0.56/0.70 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.56/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_x) = V_x ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.56/0.70 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.56/0.70 | ~ class_Int_Onumber__ring(T_a) % 0.56/0.70 | V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_HOL_Ozero__class_Ozero(T_a)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_add__0__left_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.56/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.56/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.56/0.70 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.56/0.70 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.56/0.70 | 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.56/0.70 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.56/0.70 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.56/0.70 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.56/0.70 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.56/0.70 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.56/0.70 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.56/0.70 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_foldl__foldr1__lemma_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.56/0.70 | 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.56/0.70 % 0.56/0.70 cnf(cls_foldl__foldr1_0,axiom, % 0.56/0.70 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.56/0.70 | 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.56/0.70 % 0.56/0.70 cnf(cls_Var_I2_J_0,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_head__Var__reduction_1,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_IT_OVar_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_substn_Osimps_I1_J_1,axiom, % 0.56/0.70 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.56/0.70 | 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.56/0.70 % 0.56/0.70 cnf(cls_Cons_0,axiom, % 0.56/0.70 v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Osimps_I5_J_0,axiom, % 0.56/0.70 c_Type_Otype_Otype__case(V_f1,V_f2,c_Type_Otype_OAtom(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_foldl__append_0,axiom, % 0.56/0.70 c_List_Ofoldl(V_f,V_a,c_List_Oappend(V_xs,V_ys,T_b),T_a,T_b) = c_List_Ofoldl(V_f,c_List_Ofoldl(V_f,V_a,V_xs,T_a,T_b),V_ys,T_a,T_b) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_abs_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.56/0.70 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_Nil__is__append__conv_2,axiom, % 0.56/0.70 c_List_Olist_ONil(T_a) = c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_app__Var__IT_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),c_Lambda_OdB_OVar(V_i)))) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Cons__eq__append__conv_4,axiom, % 0.56/0.70 c_List_Olist_OCons(V_x,V_xs,T_a) = c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_not__Cons__self_0,axiom, % 0.56/0.70 V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_not__Cons__self2_0,axiom, % 0.56/0.70 c_List_Olist_OCons(V_x,V_t,T_a) != V_t ). % 0.56/0.70 % 0.56/0.70 cnf(cls_lift__preserves__beta_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.56/0.70 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Lambda_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_var__app__types_1,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_type_Osplit_0,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Type_Otype_Otype__case(V_f1,V_f2,c_Type_Otype_OAtom(V_nat),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(V_f1,V_nat))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Osplit__asm_0,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Type_Otype_Otype__case(V_f1,V_f2,c_Type_Otype_OAtom(V_xc),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(V_f1,V_xc))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list_Osimps_I3_J_0,axiom, % 0.56/0.70 c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_neq__Nil__conv_1,axiom, % 0.56/0.70 c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Cons__eq__appendI_0,axiom, % 0.56/0.70 c_List_Olist_OCons(V_x,c_List_Oappend(V_xs1,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xs1,T_a),V_zs,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Cons__eq__append__conv_5,axiom, % 0.56/0.70 c_List_Olist_OCons(V_x,c_List_Oappend(V_xa,V_zs,T_a),T_a) = c_List_Oappend(c_List_Olist_OCons(V_x,V_xa,T_a),V_zs,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__Cons_0,axiom, % 0.56/0.70 c_List_Oappend(c_List_Olist_OCons(V_x,V_xs,T_a),V_ys,T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(V_xs,V_ys,T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__eq__Cons__conv_5,axiom, % 0.56/0.70 c_List_Oappend(c_List_Olist_OCons(V_x,V_xa,T_a),V_zs,T_a) = c_List_Olist_OCons(V_x,c_List_Oappend(V_xa,V_zs,T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.56/0.70 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.56/0.70 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_foldl__Cons_0,axiom, % 0.56/0.70 c_List_Ofoldl(V_f,V_a,c_List_Olist_OCons(V_x,V_xs,T_b),T_a,T_b) = c_List_Ofoldl(V_f,hAPP(hAPP(V_f,V_a),V_x),V_xs,T_a,T_b) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type__induct_2,axiom, % 0.56/0.70 ( hBOOL(hAPP(V_P,V_T)) % 0.56/0.70 | ~ hBOOL(hAPP(V_P,c_Type_Osko__Type__Xtype__induct__1__1(V_P))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list__app__typeE_1,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I10_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_typing__elims_I3_J_1,axiom, % 0.56/0.70 ( c_Type_Otyping(c_Type_Oshift(V_e,c_HOL_Ozero__class_Ozero(tc_nat),c_Type_Osko__Type__Xtyping__elims__3__1(V_T,V_e,V_t),tc_Type_Otype),V_t,c_Type_Osko__Type__Xtyping__elims__3__2(V_T,V_e,V_t)) % 0.56/0.70 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_substn__subst__n_0,axiom, % 0.56/0.70 c_Lambda_Osubstn(V_t,V_s,V_n) = c_Lambda_Osubst(V_t,c_Lambda_Oliftn(V_n,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_n) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I12_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),T_a) = hAPP(V_f3,V_dB) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__same__eq_0,axiom, % 0.56/0.70 ( c_List_Oappend(V_ys,V_xs,T_a) != c_List_Oappend(V_zs,V_xs,T_a) % 0.56/0.70 | V_ys = V_zs ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_same__append__eq_0,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Oappend(V_xs,V_zs,T_a) % 0.56/0.70 | V_ys = V_zs ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__Nil2_0,axiom, % 0.56/0.70 c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) = V_xs ). % 0.56/0.70 % 0.56/0.70 cnf(cls_eq__Nil__appendI_0,axiom, % 0.56/0.70 V_x = c_List_Oappend(c_List_Olist_ONil(T_a),V_x,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_self__append__conv_1,axiom, % 0.56/0.70 V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__Nil_0,axiom, % 0.56/0.70 c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) = V_ys ). % 0.56/0.70 % 0.56/0.70 cnf(cls_self__append__conv2_1,axiom, % 0.56/0.70 V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Osimps_I1_J_0,axiom, % 0.56/0.70 ( c_Type_Otype_OAtom(V_nat) != c_Type_Otype_OAtom(V_nat_H) % 0.56/0.70 | V_nat = V_nat_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__IT_0,axiom, % 0.56/0.70 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Beta_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_foldl__Nil_0,axiom, % 0.56/0.70 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.56/0.70 % 0.56/0.70 cnf(cls_shift__eq_0,axiom, % 0.56/0.70 hAPP(c_Type_Oshift(V_e,V_x,V_T,T_a),V_x) = V_T ). % 0.56/0.70 % 0.56/0.70 cnf(cls_lift__IT_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(V_t,V_i))) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_Nil__is__append__conv_0,axiom, % 0.56/0.70 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.56/0.70 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Nil__is__append__conv_1,axiom, % 0.56/0.70 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.56/0.70 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.56/0.70 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.56/0.70 | V_dB = V_dB_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__is__Nil__conv_0,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.56/0.70 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__is__Nil__conv_1,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.56/0.70 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Orecs_I1_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.56/0.70 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.56/0.70 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Orecs_I1_J_0,axiom, % 0.56/0.70 c_Type_Otype_Otype__rec(V_f1,V_f2,c_Type_Otype_OAtom(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_apps__preserves__beta_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_beta_0,axiom, % 0.56/0.70 hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t)),c_Lambda_Osubst(V_s,V_t,c_HOL_Ozero__class_Ozero(tc_nat)))) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.56/0.70 ( 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.56/0.70 | V_rs = V_ss ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.56/0.70 ( 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.56/0.70 | V_r = V_s ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.56/0.70 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.56/0.70 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list_Osimps_I2_J_0,axiom, % 0.56/0.70 c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_beta__cases_I1_J_0,axiom, % 0.56/0.70 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Orecs_I3_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),T_a) = hAPP(hAPP(V_f3,V_dB),c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,V_dB,T_a)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_liftn__0_0,axiom, % 0.56/0.70 c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list__app__typeD_1,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_substn__subst__0_0,axiom, % 0.56/0.70 c_Lambda_Osubstn(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) = c_Lambda_Osubst(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osplit_2,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(V_f3,V_dB))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osplit__asm_2,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_xa),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(V_f3,V_xa))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_subst__Var__IT_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j))) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__self__conv_0,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,V_ys,T_a) != V_xs % 0.56/0.70 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_self__append__conv_0,axiom, % 0.56/0.70 ( V_xs != c_List_Oappend(V_xs,V_ys,T_a) % 0.56/0.70 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__self__conv2_0,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,V_ys,T_a) != V_ys % 0.56/0.70 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_self__append__conv2_0,axiom, % 0.56/0.70 ( V_ys != c_List_Oappend(V_xs,V_ys,T_a) % 0.56/0.70 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__eq__Cons__conv_4,axiom, % 0.56/0.70 c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list_Oinject_0,axiom, % 0.56/0.70 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.56/0.70 | V_a = V_a_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list_Oinject_1,axiom, % 0.56/0.70 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.56/0.70 | V_list = V_list_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.56/0.70 ( 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.56/0.70 | V_rs = V_ss ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.56/0.70 ( 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.56/0.70 | V_m = V_n ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osplit_0,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(V_f1,V_nat))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osplit__asm_0,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_xd),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(V_f1,V_xd))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.56/0.70 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.56/0.70 | V_nat = V_nat_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_var__app__typesE_1,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append1__eq__conv_0,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) != c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a) % 0.56/0.70 | V_xs = V_ys ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append1__eq__conv_1,axiom, % 0.56/0.70 ( c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) != c_List_Oappend(V_ys,c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a) % 0.56/0.70 | V_x = V_y ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__is__Nil__conv_2,axiom, % 0.56/0.70 c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__assoc_0,axiom, % 0.56/0.70 c_List_Oappend(c_List_Oappend(V_xs,V_ys,T_a),V_zs,T_a) = c_List_Oappend(V_xs,c_List_Oappend(V_ys,V_zs,T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__eq__appendI_0,axiom, % 0.56/0.70 c_List_Oappend(V_xs,c_List_Oappend(V_xs1,V_us,T_a),T_a) = c_List_Oappend(c_List_Oappend(V_xs,V_xs1,T_a),V_us,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__eq__append__conv2_4,axiom, % 0.56/0.70 c_List_Oappend(c_List_Oappend(V_zs,V_x,T_a),V_ys,T_a) = c_List_Oappend(V_zs,c_List_Oappend(V_x,V_ys,T_a),T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_append__eq__append__conv2_5,axiom, % 0.56/0.70 c_List_Oappend(V_xs,c_List_Oappend(V_x,V_ts,T_a),T_a) = c_List_Oappend(c_List_Oappend(V_xs,V_x,T_a),V_ts,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_lift__type_0,axiom, % 0.56/0.70 ( c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_Lambda_Olift(V_t,V_i),V_T) % 0.56/0.70 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Osimps_I4_J_0,axiom, % 0.56/0.70 hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_uT_0,axiom, % 0.56/0.70 c_Type_Otyping(v_e____,v_u____,v_T____) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_subst__App_0,axiom, % 0.56/0.70 c_Lambda_Osubst(hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_s,V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_t,V_s,V_k)),c_Lambda_Osubst(V_u,V_s,V_k)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.56/0.70 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_typing__elims_I3_J_0,axiom, % 0.56/0.70 ( V_T = hAPP(hAPP(c_Type_Otype_OFun,c_Type_Osko__Type__Xtyping__elims__3__1(V_T,V_e,V_t)),c_Type_Osko__Type__Xtyping__elims__3__2(V_T,V_e,V_t)) % 0.56/0.70 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_subject__reduction_0,axiom, % 0.56/0.70 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.56/0.70 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.56/0.70 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_subst__eq_0,axiom, % 0.56/0.70 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osplit__asm_1,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_xb),V_xc),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_xb),V_xc))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osplit_1,axiom, % 0.56/0.70 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),t_a))) % 0.56/0.70 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_dB1),V_dB2))) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Osimps_I2_J_0,axiom, % 0.56/0.70 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.56/0.70 | V_type1 = V_type1_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Osimps_I2_J_1,axiom, % 0.56/0.70 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.56/0.70 | V_type2 = V_type2_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_foldr_Osimps_I2_J_0,axiom, % 0.56/0.70 c_List_Ofoldr(V_f,c_List_Olist_OCons(V_x,V_xs,T_b),V_a,T_b,T_a) = hAPP(hAPP(V_f,V_x),c_List_Ofoldr(V_f,V_xs,V_a,T_b,T_a)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_var__app__types_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_type__induct_1,axiom, % 0.56/0.70 ( c_Type_Osko__Type__Xtype__induct__1__1(V_P) != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.56/0.70 | hBOOL(hAPP(V_P,V_T)) % 0.56/0.70 | hBOOL(hAPP(V_P,V_T2)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type__induct_0,axiom, % 0.56/0.70 ( c_Type_Osko__Type__Xtype__induct__1__1(V_P) != hAPP(hAPP(c_Type_Otype_OFun,V_T1a),V_x) % 0.56/0.70 | hBOOL(hAPP(V_P,V_T)) % 0.56/0.70 | hBOOL(hAPP(V_P,V_T1a)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_App_0,axiom, % 0.56/0.70 ( c_Type_Otyping(V_env,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_U) % 0.56/0.70 | ~ c_Type_Otyping(V_env,V_t,V_T) % 0.56/0.70 | ~ c_Type_Otyping(V_env,V_s,hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.56/0.70 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.56/0.70 | V_dB1 = V_dB1_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.56/0.70 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.56/0.70 | V_dB2 = V_dB2_H ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_var__app__type__eq_0,axiom, % 0.56/0.70 ( V_T = V_U % 0.56/0.70 | ~ 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_uT_H_0,axiom, % 0.56/0.70 c_Type_Otyping(v_e____,v_u____,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_argT_0,axiom, % 0.56/0.70 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,v_T_H_H____) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_MI2_0,axiom, % 0.56/0.70 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.56/0.70 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.56/0.70 | ~ c_Type_Otyping(V_e,V_u,V_T2) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.56/0.70 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T2,tc_Type_Otype),V_t,V_Ta) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_MI1_0,axiom, % 0.56/0.70 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.56/0.70 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.56/0.70 | ~ c_Type_Otyping(V_e,V_u,V_T1) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.56/0.70 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T1,tc_Type_Otype),V_t,V_Ta) % 0.56/0.70 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_Abs_0,axiom, % 0.56/0.70 ( c_Type_Otyping(V_env,c_Lambda_OdB_OAbs(V_t),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) % 0.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_True_0,axiom, % 0.56/0.70 v_n____ = v_i____ ). % 0.56/0.70 % 0.56/0.70 cnf(cls_typing__elims_I1_J_0,axiom, % 0.56/0.70 ( hAPP(V_e,V_i) = V_T % 0.56/0.70 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OVar(V_i),V_T) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_foldr__append_0,axiom, % 0.56/0.70 c_List_Ofoldr(V_f,c_List_Oappend(V_xs,V_ys,T_b),V_a,T_b,T_a) = c_List_Ofoldr(V_f,V_xs,c_List_Ofoldr(V_f,V_ys,V_a,T_b,T_a),T_b,T_a) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.56/0.70 c_Lambda_Olift(hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Olift(V_s,V_k)),c_Lambda_Olift(V_t,V_k)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_varT_0,axiom, % 0.56/0.70 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_Lambda_OdB_OVar(v_n____),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_headT_0,axiom, % 0.56/0.70 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(v_n____)),v_a____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_argsT_0,axiom, % 0.56/0.70 c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_list__app__typeE_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_subst__preserves__beta_0,axiom, % 0.56/0.70 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Osubst(V_r,V_t,V_i)),c_Lambda_Osubst(V_s,V_t,V_i))) % 0.56/0.70 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_var__app__typesE_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_nT_0,axiom, % 0.56/0.70 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.56/0.70 % 0.56/0.70 cnf(cls_list__app__typeI_0,axiom, % 0.56/0.70 ( 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.56/0.70 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.56/0.70 | ~ 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.56/0.70 % 0.56/0.70 cnf(cls_dB_Osimps_I11_J_0,axiom, % 0.56/0.70 c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),T_a) = hAPP(hAPP(V_f2,V_dB1),V_dB2) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_typing__elims_I2_J_1,axiom, % 0.56/0.70 ( c_Type_Otyping(V_e,V_u,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u)) % 0.56/0.70 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.56/0.70 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.56/0.70 % 0.56/0.70 cnf(cls_T_0,axiom, % 0.56/0.70 v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) ). % 0.56/0.70 % 0.56/0.70 cnf(cls_type_Orecs_I2_J_0,axiom, % 0.56/0.70 c_Type_Otype_Otype__rec(V_f1,V_f2,hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2),T_a) = hAPP(hAPP(hAPP(hAPP(V_f2,V_type1),V_type2),c_Type_Otype_Otype__rec(V_f1,V_f2,V_type1,T_a)),c_Type_Otype_Otype__rec(V_f1,V_f2,V_type2,T_a)) ). % 0.56/0.70 % 0.56/0.71 cnf(cls_type_Osimps_I6_J_0,axiom, % 0.56/0.71 c_Type_Otype_Otype__case(V_f1,V_f2,hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2),T_a) = hAPP(hAPP(V_f2,V_type1),V_type2) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_typing_OVar_0,axiom, % 0.56/0.71 c_Type_Otyping(V_env,c_Lambda_OdB_OVar(V_x),hAPP(V_env,V_x)) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_type_Osplit__asm_1,axiom, % 0.56/0.71 ( ~ hBOOL(hAPP(V_P,c_Type_Otype_Otype__case(V_f1,V_f2,hAPP(hAPP(c_Type_Otype_OFun,V_xa),V_xb),t_a))) % 0.56/0.71 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_xa),V_xb))) ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_type_Osplit_1,axiom, % 0.56/0.71 ( ~ hBOOL(hAPP(V_P,c_Type_Otype_Otype__case(V_f1,V_f2,hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2),t_a))) % 0.56/0.71 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_type1),V_type2))) ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_dB_Orecs_I2_J_0,axiom, % 0.56/0.71 c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),T_a) = hAPP(hAPP(hAPP(hAPP(V_f2,V_dB1),V_dB2),c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,V_dB1,T_a)),c_Lambda_OdB_OdB__rec(V_f1,V_f2,V_f3,V_dB2,T_a)) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_type_Osimps_I3_J_0,axiom, % 0.56/0.71 c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.56/0.71 ( 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.56/0.71 | V_r = V_s ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_appR_0,axiom, % 0.56/0.71 ( 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.56/0.71 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_appL_0,axiom, % 0.56/0.71 ( 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.56/0.71 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_uIT_0,axiom, % 0.56/0.71 hBOOL(hAPP(c_InductTermi_OIT,v_u____)) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_liftn_Osimps_I2_J_0,axiom, % 0.56/0.71 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.56/0.71 % 0.56/0.71 cnf(cls_subst__lift_0,axiom, % 0.56/0.71 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.56/0.71 % 0.56/0.71 cnf(cls_list__app__typeD_0,axiom, % 0.56/0.71 ( 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.56/0.71 | ~ 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.56/0.71 % 0.56/0.71 cnf(cls_subst__lemma_0,axiom, % 0.56/0.71 ( ~ c_Type_Otyping(V_e_H,V_u,V_U) % 0.56/0.71 | ~ c_Type_Otyping(c_Type_Oshift(V_e_H,V_i,V_U,tc_Type_Otype),V_t,V_T) % 0.56/0.71 | c_Type_Otyping(V_e_H,c_Lambda_Osubst(V_t,V_u,V_i),V_T) ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_substn_Osimps_I2_J_0,axiom, % 0.56/0.71 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.56/0.71 % 0.56/0.71 cnf(cls_typing__elims_I2_J_0,axiom, % 0.56/0.71 ( 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.56/0.71 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.56/0.71 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_CHAINED_0,axiom, % 0.56/0.71 c_Type_Otyping(v_e____,c_Lambda_Osubst(v_a____,v_u____,v_i____),v_T_H_H____) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_CHAINED_0_01,axiom, % 0.56/0.71 c_Type_Otyping(v_e____,v_u____,hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype))) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_conjecture_0,negated_conjecture, % 0.56/0.71 ~ c_Type_Otyping(v_e____,hAPP(hAPP(c_Lambda_OdB_OApp,v_u____),c_Lambda_Osubst(v_a____,v_u____,v_i____)),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.56/0.71 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.56/0.71 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.56/0.71 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.56/0.71 | ~ class_Orderings_Oorder(T_1) ) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.56/0.71 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.56/0.71 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.56/0.71 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.56/0.71 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.56/0.71 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.56/0.71 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.56/0.71 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.56/0.71 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.56/0.71 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Ring__and__Field_Ozero__neq__one,axiom, % 0.56/0.71 class_Ring__and__Field_Ozero__neq__one(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Osemigroup__add,axiom, % 0.56/0.71 class_OrderedGroup_Osemigroup__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.56/0.71 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.56/0.71 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.56/0.71 class_Nat_Osemiring__char__0(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.56/0.71 class_Orderings_Opreorder(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.56/0.71 class_Orderings_Olinorder(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.56/0.71 class_Orderings_Oorder(tc_nat) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_bool__Orderings_Opreorder,axiom, % 0.56/0.71 class_Orderings_Opreorder(tc_bool) ). % 0.56/0.71 % 0.56/0.71 cnf(clsarity_bool__Orderings_Oorder,axiom, % 0.56/0.71 class_Orderings_Oorder(tc_bool) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.56/0.71 hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)) ). % 0.56/0.71 % 0.56/0.71 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.56/0.71 ( V_X = V_Y % 0.56/0.71 | ~ hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y)) ) ). % 0.56/0.71 % 0.56/0.71 %------------------------------------------------------------------------------ % 0.56/0.71 %------------------------------------------- % 0.56/0.71 % Proof found % 0.56/0.71 % SZS status Theorem for theBenchmark % 0.56/0.71 % SZS output start Proof % 0.56/0.71 %ClaNum:556(EqnAxiom:159) % 0.56/0.71 %VarNum:2267(SingletonVarNum:1001) % 0.56/0.71 %MaxLitNum:6 % 0.56/0.71 %MaxfuncDepth:5 % 0.56/0.71 %SharedTerms:84 % 0.56/0.71 %goalClause: 297 % 0.56/0.71 %singleGoalClaCount:1 % 0.56/0.71 [160]E(a1,a60) % 0.56/0.71 [161]P1(a2) % 0.56/0.71 [162]P27(a2) % 0.56/0.71 [163]P28(a2) % 0.56/0.71 [164]P2(a2) % 0.56/0.71 [165]P3(a2) % 0.56/0.71 [166]P11(a2) % 0.56/0.71 [167]P17(a2) % 0.56/0.71 [168]P17(a3) % 0.56/0.71 [169]P18(a2) % 0.56/0.71 [170]P23(a2) % 0.56/0.71 [171]P23(a3) % 0.56/0.71 [172]P19(a2) % 0.56/0.71 [173]P20(a2) % 0.56/0.71 [174]P21(a2) % 0.56/0.71 [175]P22(a2) % 0.56/0.71 [176]P24(a2) % 0.56/0.71 [177]P13(a2) % 0.56/0.71 [178]P14(a2) % 0.56/0.71 [179]P15(a2) % 0.56/0.71 [185]P4(a58,a62,a52) % 0.56/0.71 [186]P4(a59,a63,a52) % 0.56/0.71 [181]P29(f27(a5,a62)) % 0.56/0.71 [182]P29(f27(a5,a63)) % 0.56/0.71 [184]E(f13(a51,a57,a47),a64) % 0.56/0.71 [210]P4(a59,f19(a51,a63,a1),a53) % 0.56/0.71 [240]P8(f33(a59,a1,a52,a49),a57,a56) % 0.56/0.71 [241]P4(f33(a59,a1,a52,a49),a51,a53) % 0.56/0.71 [258]E(f27(f27(a45,a53),f23(a45,a56,a54,a49,a49)),a52) % 0.56/0.71 [260]P4(f33(a58,a61,a52,a49),f22(a10,f9(a60),a64,a47,a47),a55) % 0.56/0.71 [261]P4(f33(a59,a1,a52,a49),f22(a10,f9(a60),a64,a47,a47),a54) % 0.56/0.71 [266]P4(a59,a63,f27(f27(a45,a53),f23(a45,a56,a54,a49,a49))) % 0.56/0.71 [269]P4(f33(a59,a1,a52,a49),f9(a60),f27(f27(a45,a53),f23(a45,a56,a54,a49,a49))) % 0.56/0.71 [297]~P4(a59,f27(f27(a10,a63),f19(a51,a63,a1)),f23(a45,a56,a54,a49,a49)) % 0.56/0.71 [262]P4(f33(a59,a1,a52,a49),f27(f27(a10,f9(a60)),a51),f23(a45,a56,a54,a49,a49)) % 0.56/0.71 [281]~P6(x2811,x2811,a2) % 0.56/0.71 [285]~P6(x2851,f8(a2),a2) % 0.56/0.71 [180]E(f24(f4(x1801),x1801),f4(x1801)) % 0.56/0.71 [183]P29(f27(a5,f9(x1831))) % 0.56/0.71 [188]E(f27(f27(f6(a2),x1881),f8(a2)),x1881) % 0.56/0.71 [202]E(f29(f31(x2021),x2021,x2021),f31(x2021)) % 0.56/0.71 [189]E(f27(f27(f6(a2),f8(a2)),x1891),x1891) % 0.56/0.71 [193]P5(x1931,f4(x1932),x1932) % 0.56/0.71 [206]P4(x2061,f9(x2062),f27(x2061,x2062)) % 0.56/0.71 [273]~E(f9(x2731),f11(x2732)) % 0.56/0.71 [190]E(f28(f28(x1901,x1902),x1902),f28(x1901,x1902)) % 0.56/0.71 [192]E(f14(f8(a2),x1921,x1922),x1921) % 0.56/0.71 [197]E(f18(x1971,f4(x1972),x1972),x1971) % 0.56/0.71 [198]E(f19(f9(x1981),x1982,x1981),x1982) % 0.56/0.71 [199]E(f18(f4(x1991),x1992,x1991),x1992) % 0.56/0.71 [201]E(f25(f8(a2),x2011,x2012),f4(x2012)) % 0.56/0.71 [217]E(f19(x2171,f14(f8(a2),x2172,f8(a2)),f8(a2)),f19(x2171,x2172,f8(a2))) % 0.56/0.71 [207]E(f27(f27(f6(a2),x2071),x2072),f27(f27(f6(a2),x2072),x2071)) % 0.56/0.71 [208]P29(f27(f27(f31(x2081),x2082),x2082)) % 0.56/0.71 [244]P29(f27(f27(a12,f27(f27(a10,f11(x2441)),x2442)),f19(x2441,x2442,f8(a2)))) % 0.56/0.71 [290]~P29(f27(f27(a12,f9(x2901)),x2902)) % 0.56/0.71 [291]~P6(f27(f27(f6(a2),x2911),x2912),x2912,a2) % 0.56/0.71 [292]~P6(f27(f27(f6(a2),x2921),x2922),x2921,a2) % 0.56/0.71 [218]E(f11(f15(x2181,f27(f27(f6(a2),x2182),f7(a2)))),f15(f11(x2181),x2182)) % 0.56/0.71 [283]~E(f13(x2831,x2832,x2833),x2832) % 0.56/0.71 [288]~E(f13(x2881,x2882,x2883),f4(x2883)) % 0.56/0.71 [293]~P7(x2931,x2932,f4(x2933),x2933) % 0.56/0.71 [294]~P7(x2941,f4(x2942),x2943,x2942) % 0.56/0.71 [205]E(f19(f15(x2051,x2052),x2053,x2052),x2051) % 0.56/0.71 [209]E(f25(f8(a2),x2091,x2092),f25(f8(a2),x2093,x2092)) % 0.56/0.71 [211]E(f29(f29(x2111,x2112,x2113),x2113,x2112),x2111) % 0.56/0.71 [274]~E(f11(x2741),f27(f27(a10,x2742),x2743)) % 0.56/0.71 [275]~E(f9(x2751),f27(f27(a10,x2752),x2753)) % 0.56/0.71 [276]~E(f32(x2761),f27(f27(a45,x2762),x2763)) % 0.56/0.71 [277]~E(f27(f27(a10,x2771),x2772),f11(x2773)) % 0.56/0.71 [278]~E(f27(f27(a10,x2781),x2782),f9(x2783)) % 0.56/0.71 [279]~E(f27(f27(a45,x2791),x2792),f32(x2793)) % 0.56/0.71 [213]P29(f27(f27(f28(x2131,x2132),x2133),x2133)) % 0.56/0.71 [214]E(f27(f27(a10,f15(x2141,x2142)),f15(x2143,x2142)),f15(f27(f27(a10,x2141),x2143),x2142)) % 0.56/0.71 [222]E(f18(x2221,f13(x2222,f4(x2223),x2223),x2223),f24(f13(x2222,x2221,x2223),x2223)) % 0.56/0.71 [236]E(f18(f25(x2361,x2362,x2363),f13(x2362,f4(x2363),x2363),x2363),f13(x2362,f25(x2361,x2362,x2363),x2363)) % 0.56/0.71 [221]E(f27(f27(f6(a2),x2211),f27(f27(f6(a2),x2212),x2213)),f27(f27(f6(a2),x2212),f27(f27(f6(a2),x2211),x2213))) % 0.56/0.71 [233]E(f11(f14(x2331,x2332,f27(f27(f6(a2),x2333),f7(a2)))),f14(x2331,f11(x2332),x2333)) % 0.56/0.71 [235]E(f11(f19(x2351,f15(x2352,f8(a2)),f27(f27(f6(a2),x2353),f7(a2)))),f19(f11(x2351),x2352,x2353)) % 0.56/0.71 [245]E(f11(f19(x2451,f14(f27(f27(f6(a2),x2452),f7(a2)),x2453,f8(a2)),f27(f27(f6(a2),x2452),f7(a2)))),f19(f11(x2451),f14(x2452,x2453,f8(a2)),x2452)) % 0.56/0.71 [270]E(f22(a10,x2701,f18(x2702,f13(x2703,f4(a47),a47),a47),a47,a47),f27(f27(a10,f22(a10,x2701,x2702,a47,a47)),x2703)) % 0.56/0.71 [232]E(f27(f27(f6(a2),f27(f27(f6(a2),x2321),x2322)),x2323),f27(f27(f6(a2),x2321),f27(f27(f6(a2),x2322),x2323))) % 0.56/0.71 [219]E(f44(x2191,x2192,f32(x2193),x2194),f27(x2191,x2193)) % 0.56/0.71 [220]E(f46(x2201,x2202,f32(x2203),x2204),f27(x2201,x2203)) % 0.56/0.71 [228]E(f13(x2281,f18(x2282,x2283,x2284),x2284),f18(f13(x2281,x2282,x2284),x2283,x2284)) % 0.56/0.71 [230]E(f18(f18(x2301,x2302,x2303),x2304,x2303),f18(x2301,f18(x2302,x2304,x2303),x2303)) % 0.56/0.71 [239]E(f27(f33(x2391,x2392,x2393,x2394),x2392),x2393) % 0.56/0.71 [242]E(f18(f25(x2421,x2422,x2423),f25(x2424,x2422,x2423),x2423),f18(f25(x2424,x2422,x2423),f25(x2421,x2422,x2423),x2423)) % 0.56/0.71 [246]E(f22(x2461,x2462,f4(x2463),x2464,x2463),x2462) % 0.56/0.71 [247]E(f23(x2471,f4(x2472),x2473,x2472,x2474),x2473) % 0.56/0.71 [296]~E(f22(a10,f9(x2961),x2962,a47,a47),f22(a10,f11(x2963),x2964,a47,a47)) % 0.56/0.71 [237]E(f27(f27(a10,f14(x2371,x2372,x2373)),f14(x2371,x2374,x2373)),f14(x2371,f27(f27(a10,x2372),x2374),x2373)) % 0.56/0.71 [238]E(f27(f27(a10,f19(x2381,x2382,x2383)),f19(x2384,x2382,x2383)),f19(f27(f27(a10,x2381),x2384),x2382,x2383)) % 0.56/0.71 [243]E(f13(x2431,f18(f25(x2432,x2431,x2433),x2434,x2433),x2433),f18(f25(x2432,x2431,x2433),f13(x2431,x2434,x2433),x2433)) % 0.56/0.71 [295]~E(f27(f27(a10,f11(x2951)),x2952),f22(a10,f9(x2953),x2954,a47,a47)) % 0.56/0.71 [234]E(f18(f25(x2341,x2342,x2343),f25(x2344,x2342,x2343),x2343),f25(f27(f27(f6(a2),x2341),x2344),x2342,x2343)) % 0.56/0.71 [251]E(f16(x2511,x2512,x2513,f11(x2514),x2515),f27(x2513,x2514)) % 0.56/0.71 [252]E(f16(x2521,x2522,x2523,f9(x2524),x2525),f27(x2521,x2524)) % 0.56/0.71 [253]E(f17(x2531,x2532,x2533,f9(x2534),x2535),f27(x2531,x2534)) % 0.56/0.71 [263]E(f27(f27(x2631,x2632),f17(x2633,x2634,x2631,x2632,x2635)),f17(x2633,x2634,x2631,f11(x2632),x2635)) % 0.56/0.71 [231]E(f44(x2311,x2312,f27(f27(a45,x2313),x2314),x2315),f27(f27(x2312,x2313),x2314)) % 0.56/0.71 [257]E(f27(f27(f27(f27(x2571,x2572),x2573),f46(x2574,x2571,x2572,x2575)),f46(x2574,x2571,x2573,x2575)),f46(x2574,x2571,f27(f27(a45,x2572),x2573),x2575)) % 0.56/0.71 [264]E(f23(x2641,f13(x2642,x2643,x2644),x2645,x2644,x2646),f27(f27(x2641,x2642),f23(x2641,x2643,x2645,x2644,x2646))) % 0.56/0.71 [267]E(f22(x2671,f22(x2671,x2672,x2673,x2674,x2675),x2676,x2674,x2675),f22(x2671,x2672,f18(x2673,x2676,x2675),x2674,x2675)) % 0.56/0.71 [268]E(f23(x2681,x2682,f23(x2681,x2683,x2684,x2685,x2686),x2685,x2686),f23(x2681,f18(x2682,x2683,x2685),x2684,x2685,x2686)) % 0.56/0.71 [256]E(f16(x2561,x2562,x2563,f27(f27(a10,x2564),x2565),x2566),f27(f27(x2562,x2564),x2565)) % 0.56/0.71 [259]E(f22(x2591,x2592,f13(x2593,x2594,x2595),x2596,x2595),f22(x2591,f27(f27(x2591,x2592),x2593),x2594,x2596,x2595)) % 0.56/0.71 [271]E(f27(f27(f27(f27(x2711,x2712),x2713),f17(x2714,x2711,x2715,x2712,x2716)),f17(x2714,x2711,x2715,x2713,x2716)),f17(x2714,x2711,x2715,f27(f27(a10,x2712),x2713),x2716)) % 0.56/0.71 [302]~P27(x3021)+~E(f7(x3021),f8(x3021)) % 0.56/0.71 [310]E(x3101,f8(a2))+P6(f8(a2),x3101,a2) % 0.56/0.71 [319]~P1(x3191)+P6(f8(x3191),f7(x3191),x3191) % 0.56/0.71 [349]~P1(x3491)+~P6(f7(x3491),f8(x3491),x3491) % 0.56/0.71 [389]P10(f29(a12,a47,a47),x3891,a47)+~P29(f27(a5,x3891)) % 0.56/0.71 [410]~P10(f29(a12,a47,a47),x4101,a47)+P29(f27(a5,x4101)) % 0.56/0.71 [303]~P28(x3031)+E(f30(f7(a2),x3031),f7(x3031)) % 0.56/0.71 [304]~P28(x3041)+E(f30(f8(a2),x3041),f8(x3041)) % 0.56/0.71 [305]~P2(x3051)+E(f26(f4(x3051),x3051),f8(x3051)) % 0.56/0.71 [324]~P16(x3241)+E(f27(f27(f6(x3241),f8(x3241)),f8(x3241)),f8(x3241)) % 0.56/0.71 [325]~P29(f27(a5,x3251))+P29(f27(a5,f11(x3251))) % 0.56/0.71 [393]~P1(x3931)+P6(f8(x3931),f27(f27(f6(x3931),f7(x3931)),f7(x3931)),x3931) % 0.56/0.71 [330]~P6(x3302,x3302,x3301)+~P17(x3301) % 0.56/0.71 [331]~P6(x3312,x3312,x3311)+~P18(x3311) % 0.56/0.71 [332]~P6(x3322,x3322,x3321)+~P23(x3321) % 0.56/0.71 [298]E(x2981,x2982)+~E(f11(x2981),f11(x2982)) % 0.56/0.71 [299]E(x2991,x2992)+~E(f9(x2991),f9(x2992)) % 0.56/0.71 [300]E(x3001,x3002)+~E(f32(x3001),f32(x3002)) % 0.56/0.71 [306]~E(f24(x3061,x3062),f4(x3062))+E(x3061,f4(x3062)) % 0.56/0.71 [307]~P17(x3072)+P17(f50(x3071,x3072)) % 0.56/0.71 [308]~P23(x3082)+P23(f50(x3081,x3082)) % 0.56/0.71 [364]~P1(x3641)+~P6(f30(x3642,x3641),f8(x3641),x3641) % 0.56/0.71 [311]~P2(x3111)+E(f27(f27(f6(x3111),x3112),f8(x3111)),x3112) % 0.56/0.71 [312]~P24(x3121)+E(f27(f27(f6(x3121),x3122),f8(x3121)),x3122) % 0.56/0.71 [313]~P13(x3131)+E(f27(f27(f6(x3131),x3132),f8(x3131)),x3132) % 0.56/0.71 [339]P29(f27(x3391,x3392))+~P29(f27(x3391,f34(x3391))) % 0.56/0.71 [342]~P6(x3421,x3422,a2)+E(f15(f9(x3421),x3422),f9(x3421)) % 0.56/0.71 [361]~P29(f27(a5,x3611))+P29(f27(a5,f15(x3611,x3612))) % 0.56/0.71 [380]~P1(x3802)+P6(x3801,f27(f27(f6(x3802),x3801),f7(x3802)),x3802) % 0.56/0.71 [400]~P29(f27(f27(a12,x4001),x4002))+P29(f27(f27(a12,f11(x4001)),f11(x4002))) % 0.56/0.71 [497]~P2(x4971)+E(f23(f6(x4971),x4972,f8(x4971),x4971,x4971),f26(x4972,x4971)) % 0.56/0.71 [498]~P2(x4981)+E(f22(f6(x4981),f8(x4981),x4982,x4981,x4981),f26(x4982,x4981)) % 0.56/0.71 [520]~P2(x5201)+E(f23(f6(x5201),x5202,f8(x5201),x5201,x5201),f22(f6(x5201),f8(x5201),x5202,x5201,x5201)) % 0.56/0.71 [314]~P2(x3141)+E(f27(f27(f6(x3141),f8(x3141)),x3142),x3142) % 0.56/0.71 [316]~P24(x3161)+E(f27(f27(f6(x3161),f8(x3161)),x3162),x3162) % 0.56/0.71 [317]~P13(x3171)+E(f27(f27(f6(x3171),f8(x3171)),x3172),x3172) % 0.56/0.71 [321]E(x3211,f8(a2))+~E(f27(f27(f6(a2),x3212),x3211),x3212) % 0.56/0.71 [322]E(x3221,f8(a2))+~E(f27(f27(f6(a2),x3222),x3221),f8(a2)) % 0.56/0.71 [323]E(x3231,f8(a2))+~E(f27(f27(f6(a2),x3231),x3232),f8(a2)) % 0.56/0.71 [379]P6(x3791,x3792,a2)+E(f15(f9(x3791),x3792),f9(f27(f27(f6(a2),x3791),f7(a2)))) % 0.56/0.71 [406]~P29(f27(a5,x4061))+P29(f27(a5,f27(f27(a10,x4061),f9(x4062)))) % 0.56/0.71 [454]P29(f27(f27(f28(a12,a47),f11(x4541)),f11(x4542)))+~P29(f27(f27(f28(a12,a47),x4541),x4542)) % 0.56/0.71 [535]~P5(a5,x5352,a47)+P29(f27(a5,f22(a10,f9(x5351),x5352,a47,a47))) % 0.56/0.71 [328]~E(f18(x3283,x3281,x3282),x3283)+E(x3281,f4(x3282)) % 0.56/0.71 [329]~E(f18(x3291,x3293,x3292),x3293)+E(x3291,f4(x3292)) % 0.56/0.71 [334]~E(f25(x3341,x3342,x3343),f4(x3343))+E(x3341,f8(a2)) % 0.56/0.71 [337]~E(f18(x3373,x3371,x3372),f4(x3372))+E(x3371,f4(x3372)) % 0.56/0.71 [338]~E(f18(x3381,x3383,x3382),f4(x3382))+E(x3381,f4(x3382)) % 0.56/0.71 [345]~P4(x3451,f9(x3452),x3453)+E(f27(x3451,x3452),x3453) % 0.56/0.71 [509]~E(f11(x5092),f22(a10,x5093,x5091,a47,a47))+E(x5091,f4(a47)) % 0.56/0.71 [510]~E(f9(x5102),f22(a10,x5103,x5101,a47,a47))+E(x5101,f4(a47)) % 0.56/0.71 [511]~E(f22(a10,x5112,x5111,a47,a47),f11(x5113))+E(x5111,f4(a47)) % 0.56/0.71 [512]E(x5121,f11(x5122))+~E(f22(a10,x5121,x5123,a47,a47),f11(x5122)) % 0.56/0.71 [513]E(f11(x5131),x5132)+~E(f11(x5131),f22(a10,x5132,x5133,a47,a47)) % 0.56/0.71 [514]E(f9(x5141),x5142)+~E(f9(x5141),f22(a10,x5142,x5143,a47,a47)) % 0.56/0.71 [526]E(x5261,x5262)+~E(f22(a10,x5261,x5263,a47,a47),f22(a10,x5262,x5263,a47,a47)) % 0.56/0.71 [368]~P6(x3682,x3683,a2)+E(f14(x3681,f9(x3682),x3683),f9(x3682)) % 0.56/0.71 [369]~P6(x3691,x3693,a2)+E(f19(f9(x3691),x3692,x3693),f9(x3691)) % 0.56/0.71 [392]~P2(x3921)+E(f27(f27(f6(x3921),x3922),f26(x3923,x3921)),f26(f13(x3922,x3923,x3921),x3921)) % 0.56/0.71 [408]~P2(x4081)+E(f27(f27(f6(x4081),f26(x4082,x4081)),f26(x4083,x4081)),f26(f18(x4082,x4083,x4081),x4081)) % 0.56/0.71 [434]~P29(f27(f27(a12,x4341),x4343))+P29(f27(f27(a12,f15(x4341,x4342)),f15(x4343,x4342))) % 0.56/0.71 [455]~P4(x4552,f11(x4553),x4551)+E(f27(f27(a45,f37(x4551,x4552,x4553)),f41(x4551,x4552,x4553)),x4551) % 0.56/0.71 [487]~P4(x4871,f11(x4873),x4872)+P4(f33(x4871,f8(a2),f37(x4872,x4871,x4873),a49),x4873,f41(x4872,x4871,x4873)) % 0.56/0.71 [515]E(f27(f27(a10,x5151),x5152),x5153)+~E(f27(f27(a10,x5151),x5152),f22(a10,x5153,f4(a47),a47,a47)) % 0.56/0.71 [519]~P11(x5191)+E(f23(f6(x5191),x5192,x5193,x5191,x5191),f22(f6(x5191),x5193,x5192,x5191,x5191)) % 0.56/0.71 [550]~P29(f27(f27(a12,x5501),x5503))+P29(f27(f27(a12,f22(a10,x5501,x5502,a47,a47)),f22(a10,x5503,x5502,a47,a47))) % 0.56/0.71 [552]~P7(a12,x5522,x5523,a47)+P29(f27(f27(a12,f22(a10,x5521,x5522,a47,a47)),f22(a10,x5521,x5523,a47,a47))) % 0.56/0.71 [347]~P24(x3471)+E(f27(f27(f6(x3471),x3472),x3473),f27(f27(f6(x3471),x3473),x3472)) % 0.56/0.71 [348]~P13(x3481)+E(f27(f27(f6(x3481),x3482),x3483),f27(f27(f6(x3481),x3483),x3482)) % 0.56/0.71 [366]E(x3661,x3662)+~E(f27(f27(f6(a2),x3663),x3661),f27(f27(f6(a2),x3663),x3662)) % 0.56/0.71 [367]E(x3671,x3672)+~E(f27(f27(f6(a2),x3671),x3673),f27(f27(f6(a2),x3672),x3673)) % 0.56/0.71 [370]E(x3701,x3702)+~P29(f27(f27(f31(x3703),x3701),x3702)) % 0.56/0.71 [396]~P6(x3961,x3963,a2)+P6(x3961,f27(f27(f6(a2),x3962),x3963),a2) % 0.56/0.71 [398]~P6(x3981,x3982,a2)+P6(x3981,f27(f27(f6(a2),x3982),x3983),a2) % 0.56/0.71 [416]P6(x4161,x4162,a2)+~P6(f27(f27(f6(a2),x4161),x4163),x4162,a2) % 0.56/0.71 [419]~P29(f27(a5,x4191))+P29(f27(a5,f19(x4191,f9(x4192),x4193))) % 0.56/0.71 [426]~P6(x4261,x4263,a2)+P6(f27(f27(f6(a2),x4261),x4262),f27(f27(f6(a2),x4263),x4262),a2) % 0.56/0.71 [427]~P6(x4272,x4273,a2)+P6(f27(f27(f6(a2),x4271),x4272),f27(f27(f6(a2),x4271),x4273),a2) % 0.56/0.71 [450]P6(x4501,x4502,a2)+~P6(f27(f27(f6(a2),x4503),x4501),f27(f27(f6(a2),x4503),x4502),a2) % 0.56/0.71 [462]P29(f27(f27(f28(a12,a47),f15(x4621,x4622)),f15(x4623,x4622)))+~P29(f27(f27(f28(a12,a47),x4621),x4623)) % 0.56/0.71 [467]~P29(f27(f27(a12,x4671),x4673))+P29(f27(f27(a12,f27(f27(a10,x4671),x4672)),f27(f27(a10,x4673),x4672))) % 0.56/0.71 [468]~P29(f27(f27(a12,x4682),x4683))+P29(f27(f27(a12,f27(f27(a10,x4681),x4682)),f27(f27(a10,x4681),x4683))) % 0.56/0.71 [479]~P29(f27(f27(f28(a12,a47),x4791),x4793))+P29(f27(f27(f28(a12,a47),f27(f27(a10,x4791),x4792)),f27(f27(a10,x4793),x4792))) % 0.56/0.71 [480]~P29(f27(f27(f28(a12,a47),x4802),x4803))+P29(f27(f27(f28(a12,a47),f27(f27(a10,x4801),x4802)),f27(f27(a10,x4801),x4803))) % 0.56/0.71 [524]~P2(x5241)+E(f27(f27(f6(x5241),x5242),f23(f6(x5241),x5243,f8(x5241),x5241,x5241)),f22(f6(x5241),x5242,x5243,x5241,x5241)) % 0.56/0.71 [525]~P2(x5251)+E(f27(f27(f6(x5251),x5252),f22(f6(x5251),f8(x5251),x5253,x5251,x5251)),f22(f6(x5251),x5252,x5253,x5251,x5251)) % 0.56/0.71 [551]P29(f27(f27(f28(a12,a47),f22(a10,x5511,x5512,a47,a47)),f22(a10,x5513,x5512,a47,a47)))+~P29(f27(f27(f28(a12,a47),x5511),x5513)) % 0.56/0.71 [394]P6(x3942,x3943,a2)+E(f14(x3941,f9(x3942),x3943),f9(f27(f27(f6(a2),x3942),x3941))) % 0.56/0.71 [407]~P28(x4071)+E(f27(f27(f6(x4071),f30(x4072,x4071)),f30(x4073,x4071)),f30(f27(f27(f6(a2),x4072),x4073),x4071)) % 0.56/0.71 [522]~E(f22(a10,f27(f27(a10,x5221),x5222),x5223,a47,a47),x5221)+E(f22(a10,f27(f27(a10,x5221),x5222),f18(x5223,f13(x5222,f4(a47),a47),a47),a47,a47),f27(f27(a10,x5221),x5222)) % 0.56/0.71 [553]P7(a12,x5531,f21(x5532,x5531,x5533),a47)+~P29(f27(f27(a12,f22(a10,f9(x5532),x5531,a47,a47)),x5533)) % 0.56/0.71 [555]E(f22(a10,f9(x5551),f21(x5551,x5552,x5553),a47,a47),x5553)+~P29(f27(f27(a12,f22(a10,f9(x5551),x5552,a47,a47)),x5553)) % 0.56/0.71 [372]E(x3721,x3722)+~E(f18(x3723,x3721,x3724),f18(x3723,x3722,x3724)) % 0.56/0.71 [374]E(x3741,x3742)+~E(f18(x3741,x3743,x3744),f18(x3742,x3743,x3744)) % 0.56/0.71 [420]P5(x4201,x4202,x4203)+~P5(x4201,f18(x4204,x4202,x4203),x4203) % 0.56/0.71 [421]P5(x4211,x4212,x4213)+~P5(x4211,f18(x4212,x4214,x4213),x4213) % 0.56/0.71 [532]P8(x5321,x5322,f35(x5323,x5321,x5324,x5322))+~P4(x5321,f22(a10,x5324,x5322,a47,a47),x5323) % 0.56/0.71 [533]P8(x5331,x5332,f36(x5333,x5331,x5334,x5332))+~P4(x5331,f22(a10,x5334,x5332,a47,a47),x5333) % 0.56/0.71 [351]E(x3511,x3512)+~E(f27(f27(a10,x3513),x3511),f27(f27(a10,x3514),x3512)) % 0.56/0.71 [352]E(x3521,x3522)+~E(f27(f27(a45,x3523),x3521),f27(f27(a45,x3524),x3522)) % 0.56/0.71 [353]E(x3531,x3532)+~E(f27(f27(a10,x3531),x3533),f27(f27(a10,x3532),x3534)) % 0.56/0.71 [354]E(x3541,x3542)+~E(f27(f27(a45,x3541),x3543),f27(f27(a45,x3542),x3544)) % 0.56/0.71 [471]E(f19(f15(x4711,f27(f27(f6(a2),x4712),f7(a2))),f15(x4713,x4712),x4714),f15(f19(x4711,x4713,x4714),x4712))+~P6(x4714,f27(f27(f6(a2),x4712),f7(a2)),a2) % 0.56/0.71 [475]P4(x4751,x4752,f38(x4753,x4751,x4754,x4752))+~P4(x4751,f27(f27(a10,x4754),x4752),x4753) % 0.56/0.71 [478]~P29(f27(f27(a12,x4781),x4784))+P29(f27(f27(a12,f19(x4781,x4782,x4783)),f19(x4784,x4782,x4783))) % 0.56/0.71 [486]P29(f27(f27(f28(a12,a47),f19(x4861,x4862,x4863)),f19(x4861,x4864,x4863)))+~P29(f27(f27(a12,x4862),x4864)) % 0.56/0.71 [489]P4(x4891,f11(x4892),f27(f27(a45,x4893),x4894))+~P4(f33(x4891,f8(a2),x4893,a49),x4892,x4894) % 0.56/0.71 [528]E(x5281,x5282)+~E(f22(a10,f11(x5283),x5281,a47,a47),f22(a10,f11(x5284),x5282,a47,a47)) % 0.56/0.71 [529]E(x5291,x5292)+~E(f22(a10,f9(x5293),x5291,a47,a47),f22(a10,f9(x5294),x5292,a47,a47)) % 0.56/0.71 [530]E(x5301,x5302)+~E(f22(a10,f11(x5301),x5303,a47,a47),f22(a10,f11(x5302),x5304,a47,a47)) % 0.56/0.71 [531]E(x5311,x5312)+~E(f22(a10,f9(x5311),x5313,a47,a47),f22(a10,f9(x5312),x5314,a47,a47)) % 0.56/0.71 [534]P8(x5341,x5342,f42(x5343,x5341,x5344,x5342))+~P4(x5341,f22(a10,f9(x5344),x5342,a47,a47),x5343) % 0.56/0.71 [538]~P4(x5381,f22(a10,x5382,x5384,a47,a47),x5383)+P4(x5381,x5382,f23(a45,f35(x5383,x5381,x5382,x5384),x5383,a49,a49)) % 0.56/0.71 [539]~P4(x5391,f22(a10,x5392,x5394,a47,a47),x5393)+P4(x5391,x5392,f23(a45,f36(x5393,x5391,x5392,x5394),x5393,a49,a49)) % 0.56/0.71 [540]~P4(x5401,f22(a10,f9(x5402),x5404,a47,a47),x5403)+P4(x5401,f9(x5402),f23(a45,f42(x5403,x5401,x5402,x5404),x5403,a49,a49)) % 0.56/0.71 [422]~P29(f27(f27(x4221,x4223),x4224))+P29(f27(f27(f28(x4221,x4222),x4223),x4224)) % 0.56/0.71 [461]~P6(x4612,f27(f27(f6(a2),x4614),f7(a2)),a2)+E(f19(f15(x4611,x4612),f15(x4613,x4612),f27(f27(f6(a2),x4614),f7(a2))),f15(f19(x4611,x4613,x4614),x4612)) % 0.56/0.71 [491]P29(f27(f27(f28(a12,a47),f19(x4911,x4912,x4913)),f19(x4914,x4912,x4913)))+~P29(f27(f27(f28(a12,a47),x4911),x4914)) % 0.56/0.71 [492]P29(f27(f27(f28(a12,a47),f19(x4921,x4922,x4923)),f19(x4921,x4924,x4923)))+~P29(f27(f27(f28(a12,a47),x4922),x4924)) % 0.56/0.71 [495]P8(x4951,x4952,f39(x4953,x4951,x4954,x4952))+~P8(x4951,f18(x4952,f13(x4954,f4(a47),a47),a47),x4953) % 0.56/0.71 [496]P4(x4961,x4962,f40(x4963,x4961,x4962,x4964))+~P8(x4961,f18(x4964,f13(x4962,f4(a47),a47),a47),x4963) % 0.56/0.71 [505]P29(f27(x5051,f27(x5052,x5053)))+~P29(f27(x5051,f44(x5052,x5054,f32(x5053),a48))) % 0.56/0.71 [518]~P4(x5181,f27(f27(a10,x5182),x5184),x5183)+P4(x5181,x5182,f27(f27(a45,f38(x5183,x5181,x5182,x5184)),x5183)) % 0.56/0.71 [423]~P24(x4231)+E(f27(f27(f6(x4231),x4232),f27(f27(f6(x4231),x4233),x4234)),f27(f27(f6(x4231),x4233),f27(f27(f6(x4231),x4232),x4234))) % 0.56/0.71 [424]~P13(x4241)+E(f27(f27(f6(x4241),x4242),f27(f27(f6(x4241),x4243),x4244)),f27(f27(f6(x4241),x4243),f27(f27(f6(x4241),x4242),x4244))) % 0.56/0.71 [425]~P12(x4251)+E(f27(f27(f6(x4251),x4252),f27(f27(f6(x4251),x4253),x4254)),f27(f27(f6(x4251),x4253),f27(f27(f6(x4251),x4252),x4254))) % 0.56/0.71 [501]~P29(f27(f27(f28(x5011,x5012),x5014),x5013))+P29(f27(f27(f28(f29(x5011,x5012,x5012),x5012),x5013),x5014)) % 0.56/0.71 [508]P29(f27(f27(f28(x5081,x5082),x5083),x5084))+~P29(f27(f27(f28(f29(x5081,x5082,x5082),x5082),x5084),x5083)) % 0.56/0.71 [527]~P22(x5271)+E(f22(f6(x5271),f27(f27(f6(x5271),x5272),x5273),x5274,x5271,x5271),f27(f27(f6(x5271),x5272),f22(f6(x5271),x5273,x5274,x5271,x5271))) % 0.56/0.71 [447]~P11(x4471)+E(f27(f27(f6(x4471),f27(f27(f6(x4471),x4472),x4473)),x4474),f27(f27(f6(x4471),x4472),f27(f27(f6(x4471),x4473),x4474))) % 0.56/0.71 [448]~P24(x4481)+E(f27(f27(f6(x4481),f27(f27(f6(x4481),x4482),x4483)),x4484),f27(f27(f6(x4481),x4482),f27(f27(f6(x4481),x4483),x4484))) % 0.56/0.71 [449]~P13(x4491)+E(f27(f27(f6(x4491),f27(f27(f6(x4491),x4492),x4493)),x4494),f27(f27(f6(x4491),x4492),f27(f27(f6(x4491),x4493),x4494))) % 0.56/0.71 [458]~P24(x4581)+E(f27(f27(f6(x4581),f27(f27(f6(x4581),x4582),x4583)),x4584),f27(f27(f6(x4581),f27(f27(f6(x4581),x4582),x4584)),x4583)) % 0.56/0.71 [371]E(x3711,x3712)+~E(f13(x3713,x3711,x3714),f13(x3715,x3712,x3714)) % 0.56/0.71 [373]E(x3731,x3732)+~E(f13(x3731,x3733,x3734),f13(x3732,x3735,x3734)) % 0.56/0.71 [375]E(x3751,x3752)+~E(f25(x3751,x3753,x3754),f25(x3752,x3755,x3754)) % 0.56/0.71 [472]~P4(x4721,x4724,x4725)+P4(f33(x4721,x4722,x4723,a49),f15(x4724,x4722),x4725) % 0.56/0.71 [481]~P7(x4811,x4813,x4815,x4814)+P7(x4811,f13(x4812,x4813,x4814),f13(x4812,x4815,x4814),x4814) % 0.56/0.71 [482]~P7(x4821,x4822,x4825,x4824)+P7(x4821,f18(x4822,x4823,x4824),f18(x4825,x4823,x4824),x4824) % 0.56/0.71 [483]~P7(x4831,x4833,x4835,x4834)+P7(x4831,f18(x4832,x4833,x4834),f18(x4832,x4835,x4834),x4834) % 0.56/0.71 [463]P7(x4631,f13(x4632,x4633,x4634),f13(x4635,x4633,x4634),x4634)+~P29(f27(f27(x4631,x4632),x4635)) % 0.56/0.71 [464]~P6(x4645,x4642,a2)+E(f27(f33(x4641,x4642,x4643,x4644),x4645),f27(x4641,x4645)) % 0.56/0.71 [459]E(x4591,x4592)+~E(f18(x4593,f13(x4591,f4(x4594),x4594),x4594),f18(x4595,f13(x4592,f4(x4594),x4594),x4594)) % 0.56/0.71 [460]E(x4601,x4602)+~E(f18(x4601,f13(x4603,f4(x4604),x4604),x4604),f18(x4602,f13(x4605,f4(x4604),x4604),x4604)) % 0.56/0.71 [470]~P29(f27(f27(x4701,x4705),x4704))+P29(f27(f27(f29(x4701,x4702,x4703),x4704),x4705)) % 0.56/0.71 [485]P29(f27(f27(x4851,x4852),x4853))+~P29(f27(f27(f29(x4851,x4854,x4855),x4853),x4852)) % 0.56/0.71 [543]P29(f27(x5431,f27(x5432,x5433)))+~P29(f27(x5431,f16(x5434,x5435,x5432,f11(x5433),a48))) % 0.56/0.71 [545]P29(f27(x5451,f27(x5452,x5453)))+~P29(f27(x5451,f16(x5452,x5454,x5455,f9(x5453),a48))) % 0.56/0.71 [473]~P24(x4731)+E(f27(f27(f6(x4731),f27(f27(f6(x4731),x4732),x4733)),f27(f27(f6(x4731),x4734),x4735)),f27(f27(f6(x4731),f27(f27(f6(x4731),x4732),x4734)),f27(f27(f6(x4731),x4733),x4735))) % 0.56/0.71 [517]P29(f27(x5171,f27(f27(x5172,x5173),x5174)))+~P29(f27(x5171,f44(x5175,x5172,f27(f27(a45,x5173),x5174),a48))) % 0.56/0.71 [548]P29(f27(x5481,f27(f27(x5482,x5483),x5484)))+~P29(f27(x5481,f16(x5485,x5482,x5486,f27(f27(a10,x5483),x5484),a48))) % 0.56/0.71 [344]E(x3441,x3442)+P6(x3442,x3441,a2)+P6(x3441,x3442,a2) % 0.56/0.71 [387]~P1(x3871)+P6(f8(x3871),f30(x3872,x3871),x3871)+~P6(f8(a2),x3872,a2) % 0.56/0.71 [391]~P1(x3912)+~P6(f8(x3912),f30(x3911,x3912),x3912)+P6(f8(a2),x3911,a2) % 0.56/0.71 [318]~P25(x3181)+~P9(x3181)+E(f27(f27(f6(x3181),x3182),f8(x3181)),x3182) % 0.56/0.71 [340]~P16(x3402)+E(x3401,f8(x3402))+~E(f27(f27(f6(x3402),x3401),x3401),f8(x3402)) % 0.56/0.71 [411]~P16(x4111)+~P6(f8(x4111),x4112,x4111)+P6(f8(x4111),f27(f27(f6(x4111),x4112),x4112),x4111) % 0.56/0.71 [412]~P26(x4121)+~P6(x4122,f8(x4121),x4121)+P6(f27(f27(f6(x4121),x4122),x4122),f8(x4121),x4121) % 0.56/0.71 [413]~P16(x4131)+~P6(x4132,f8(x4131),x4131)+P6(f27(f27(f6(x4131),x4132),x4132),f8(x4131),x4131) % 0.56/0.71 [428]~P26(x4282)+P6(x4281,f8(x4282),x4282)+~P6(f27(f27(f6(x4282),x4281),x4281),f8(x4282),x4282) % 0.56/0.71 [429]~P16(x4292)+P6(x4291,f8(x4292),x4292)+~P6(f27(f27(f6(x4292),x4291),x4291),f8(x4292),x4292) % 0.56/0.71 [430]~P16(x4301)+P6(f8(x4301),x4302,x4301)+~P6(f8(x4301),f27(f27(f6(x4301),x4302),x4302),x4301) % 0.56/0.71 [432]P6(f8(a2),x4321,a2)+P6(f8(a2),x4322,a2)+~P6(f8(a2),f27(f27(f6(a2),x4321),x4322),a2) % 0.56/0.71 [383]~P6(x3833,x3832,x3831)+~P17(x3831)+~P6(x3832,x3833,x3831) % 0.56/0.71 [384]~P6(x3843,x3842,x3841)+~P18(x3841)+~P6(x3842,x3843,x3841) % 0.56/0.71 [385]~P6(x3853,x3852,x3851)+~P23(x3851)+~P6(x3852,x3853,x3851) % 0.56/0.71 [309]~P3(x3093)+E(x3091,x3092)+~E(f30(x3091,x3093),f30(x3092,x3093)) % 0.56/0.71 [390]~P1(x3902)+~P6(x3901,x3903,a2)+P6(f30(x3901,x3902),f30(x3903,x3902),x3902) % 0.56/0.71 [399]~P1(x3993)+~P6(f30(x3991,x3993),f30(x3992,x3993),x3993)+P6(x3991,x3992,a2) % 0.56/0.71 [360]E(x3601,x3602)+P6(x3602,x3601,a2)+E(f19(f9(x3601),x3603,x3602),f9(x3601)) % 0.56/0.71 [541]~P10(f29(a12,a47,a47),x5412,a47)+~P10(f29(a12,a47,a47),f22(a10,f19(x5411,x5412,f8(a2)),x5413,a47,a47),a47)+P10(f29(a12,a47,a47),f22(a10,f27(f27(a10,f11(x5411)),x5412),x5413,a47,a47),a47) % 0.56/0.71 [549]~P29(f27(a5,x5492))+~P29(f27(a5,f22(a10,f19(x5491,x5492,f8(a2)),x5493,a47,a47)))+P29(f27(a5,f22(a10,f27(f27(a10,f11(x5491)),x5492),x5493,a47,a47))) % 0.56/0.71 [431]~P5(x4311,x4313,x4314)+~P5(x4311,x4312,x4314)+P5(x4311,f18(x4312,x4313,x4314),x4314) % 0.56/0.71 [362]P29(f27(x3621,x3622))+P29(f27(x3621,x3623))+~E(f34(x3621),f27(f27(a45,x3624),x3623)) % 0.56/0.71 [363]P29(f27(x3631,x3632))+P29(f27(x3631,x3633))+~E(f34(x3631),f27(f27(a45,x3633),x3634)) % 0.56/0.71 [409]P4(x4091,x4092,x4093)+~P4(x4091,x4094,x4093)+~P29(f27(f27(a12,x4094),x4092)) % 0.56/0.71 [415]P10(x4151,x4152,x4153)+~P10(x4151,x4154,x4153)+~P29(f27(f27(x4151,x4152),x4154)) % 0.56/0.71 [523]E(x5231,f4(a47))+E(f22(a10,x5232,f20(x5233,x5234,x5232,x5231),a47,a47),x5233)+~E(f27(f27(a10,x5233),x5234),f22(a10,x5232,x5231,a47,a47)) % 0.56/0.71 [376]~P14(x3763)+E(x3761,x3762)+~E(f27(f27(f6(x3763),x3764),x3761),f27(f27(f6(x3763),x3764),x3762)) % 0.56/0.71 [377]~P15(x3773)+E(x3771,x3772)+~E(f27(f27(f6(x3773),x3774),x3771),f27(f27(f6(x3773),x3774),x3772)) % 0.56/0.71 [378]~P15(x3783)+E(x3781,x3782)+~E(f27(f27(f6(x3783),x3781),x3784),f27(f27(f6(x3783),x3782),x3784)) % 0.56/0.71 [417]~P6(x4174,x4173,a2)+P6(x4171,x4172,a2)+~E(f27(f27(f6(a2),x4171),x4173),f27(f27(f6(a2),x4174),x4172)) % 0.56/0.71 [435]~P19(x4351)+~P6(x4352,x4354,x4351)+P6(f27(f27(f6(x4351),x4352),x4353),f27(f27(f6(x4351),x4354),x4353),x4351) % 0.56/0.71 [436]~P20(x4361)+~P6(x4362,x4364,x4361)+P6(f27(f27(f6(x4361),x4362),x4363),f27(f27(f6(x4361),x4364),x4363),x4361) % 0.56/0.71 [437]~P19(x4371)+~P6(x4373,x4374,x4371)+P6(f27(f27(f6(x4371),x4372),x4373),f27(f27(f6(x4371),x4372),x4374),x4371) % 0.56/0.71 [438]~P20(x4381)+~P6(x4383,x4384,x4381)+P6(f27(f27(f6(x4381),x4382),x4383),f27(f27(f6(x4381),x4382),x4384),x4381) % 0.56/0.71 [442]P4(x4421,x4422,x4423)+~P4(x4421,x4424,x4423)+~P29(f27(f27(f28(a12,a47),x4424),x4422)) % 0.56/0.71 [443]~P6(x4432,x4434,a2)+~P6(x4431,x4433,a2)+P6(f27(f27(f6(a2),x4431),x4432),f27(f27(f6(a2),x4433),x4434),a2) % 0.56/0.71 [452]P10(x4521,x4522,x4523)+~P10(x4521,x4524,x4523)+~P29(f27(f27(f28(x4521,x4523),x4522),x4524)) % 0.56/0.71 [456]~P19(x4563)+P6(x4561,x4562,x4563)+~P6(f27(f27(f6(x4563),x4564),x4561),f27(f27(f6(x4563),x4564),x4562),x4563) % 0.56/0.71 [457]~P19(x4573)+P6(x4571,x4572,x4573)+~P6(f27(f27(f6(x4573),x4571),x4574),f27(f27(f6(x4573),x4572),x4574),x4573) % 0.56/0.71 [493]~P29(f27(f27(f28(a12,a47),x4931),x4933))+~P29(f27(f27(f28(a12,a47),x4932),x4934))+P29(f27(f27(f28(a12,a47),f27(f27(a10,x4931),x4932)),f27(f27(a10,x4933),x4934))) % 0.56/0.71 [521]E(x5211,f4(a47))+~E(f27(f27(a10,x5212),x5213),f22(a10,x5214,x5211,a47,a47))+E(f18(f20(x5212,x5213,x5214,x5211),f13(x5213,f4(a47),a47),a47),x5211) % 0.56/0.71 [381]E(x3811,x3812)+~E(f25(x3813,x3811,x3814),f25(x3815,x3812,x3814))+E(x3813,f8(a2)) % 0.56/0.71 [536]~P8(x5361,x5363,x5365)+~P4(x5361,x5362,f23(a45,x5365,x5364,a49,a49))+P4(x5361,f22(a10,x5362,x5363,a47,a47),x5364) % 0.56/0.71 [444]~P4(x4441,x4443,x4445)+~P4(x4441,x4442,f27(f27(a45,x4445),x4444))+P4(x4441,f27(f27(a10,x4442),x4443),x4444) % 0.56/0.71 [546]E(x5461,x5462)+~P4(x5463,f22(a10,f9(x5464),x5465,a47,a47),x5461)+~P4(x5463,f22(a10,f9(x5464),x5465,a47,a47),x5462) % 0.56/0.71 [465]~P29(f27(f27(x4651,x4655),x4654))+~P29(f27(f27(f28(x4651,x4652),x4653),x4655))+P29(f27(f27(f28(x4651,x4652),x4653),x4654)) % 0.56/0.71 [466]~P29(f27(f27(x4661,x4663),x4665))+~P29(f27(f27(f28(x4661,x4662),x4665),x4664))+P29(f27(f27(f28(x4661,x4662),x4663),x4664)) % 0.56/0.71 [476]~P29(f27(f27(f28(x4761,x4762),x4763),x4765))+P29(f27(f27(f28(x4761,x4762),x4763),x4764))+~P29(f27(f27(f28(x4761,x4762),x4765),x4764)) % 0.56/0.71 [441]~P12(x4411)+E(f27(f27(f6(x4411),x4412),x4413),x4414)+~E(f27(f27(f6(x4411),x4412),f27(f27(f6(x4411),x4415),x4413)),f27(f27(f6(x4411),x4415),x4414)) % 0.56/0.71 [474]E(x4741,x4742)+E(x4743,x4744)+~P7(x4745,f13(x4744,x4742,x4746),f13(x4743,x4741,x4746),x4746) % 0.56/0.71 [488]E(x4881,x4882)+P7(x4883,x4881,x4882,x4884)+~P7(x4883,f13(x4885,x4881,x4884),f13(x4886,x4882,x4884),x4884) % 0.56/0.71 [494]~P4(x4941,x4943,x4946)+P4(x4941,f19(x4942,x4943,x4944),x4945)+~P4(f33(x4941,x4944,x4946,a49),x4942,x4945) % 0.56/0.71 [477]E(x4771,x4772)+~P7(x4773,f13(x4772,x4774,x4775),f13(x4771,x4776,x4775),x4775)+P29(f27(f27(x4773,x4772),x4771)) % 0.56/0.71 [490]P7(x4901,x4902,x4903,x4904)+~P7(x4901,f13(x4905,x4902,x4904),f13(x4906,x4903,x4904),x4904)+P29(f27(f27(x4901,x4905),x4906)) % 0.56/0.71 [502]E(x5021,x5022)+E(x5023,x5024)+~P7(x5025,f18(x5023,f13(x5021,f4(x5026),x5026),x5026),f18(x5024,f13(x5022,f4(x5026),x5026),x5026),x5026) % 0.56/0.71 [503]E(x5031,x5032)+~P7(x5033,f18(x5034,f13(x5031,f4(x5035),x5035),x5035),f18(x5036,f13(x5032,f4(x5035),x5035),x5035),x5035)+P29(f27(f27(x5033,x5031),x5032)) % 0.56/0.71 [506]E(x5061,x5062)+P7(x5063,x5061,x5062,x5064)+~P7(x5063,f18(x5061,f13(x5065,f4(x5064),x5064),x5064),f18(x5062,f13(x5066,f4(x5064),x5064),x5064),x5064) % 0.56/0.71 [507]P7(x5071,x5072,x5073,x5074)+~P7(x5071,f18(x5072,f13(x5075,f4(x5074),x5074),x5074),f18(x5073,f13(x5076,f4(x5074),x5074),x5074),x5074)+P29(f27(f27(x5071,x5075),x5076)) % 0.56/0.71 [358]P6(x3581,x3582,x3583)+~P18(x3583)+E(x3581,x3582)+P6(x3582,x3581,x3583) % 0.56/0.71 [359]P6(x3591,x3592,x3593)+~P26(x3593)+E(x3591,x3592)+P6(x3592,x3591,x3593) % 0.56/0.71 [341]~P25(x3412)+~P9(x3412)+E(x3411,f8(x3412))+~E(f27(f27(f6(x3412),x3413),x3411),x3413) % 0.56/0.71 [439]~P21(x4391)+~P6(f8(x4391),x4393,x4391)+~P6(f8(x4391),x4392,x4391)+P6(f8(x4391),f27(f27(f6(x4391),x4392),x4393),x4391) % 0.56/0.71 [440]~P21(x4401)+~P6(x4403,f8(x4401),x4401)+~P6(x4402,f8(x4401),x4401)+P6(f27(f27(f6(x4401),x4402),x4403),f8(x4401),x4401) % 0.56/0.71 [402]~P17(x4023)+~P6(x4021,x4024,x4023)+P6(x4021,x4022,x4023)+~P6(x4024,x4022,x4023) % 0.56/0.71 [403]~P23(x4033)+~P6(x4031,x4034,x4033)+P6(x4031,x4032,x4033)+~P6(x4034,x4032,x4033) % 0.56/0.71 [386]~P25(x3863)+~P9(x3863)+E(x3861,x3862)+~E(f27(f27(f6(x3863),x3864),x3861),f27(f27(f6(x3863),x3864),x3862)) % 0.56/0.71 [433]~P1(x4332)+~P6(x4331,x4334,x4332)+~P6(f8(x4332),x4333,x4332)+P6(x4331,f27(f27(f6(x4332),x4333),x4334),x4332) % 0.56/0.71 [453]~P20(x4531)+~P6(x4533,x4535,x4531)+~P6(x4532,x4534,x4531)+P6(f27(f27(f6(x4531),x4532),x4533),f27(f27(f6(x4531),x4534),x4535),x4531) % 0.56/0.71 [554]~P8(x5541,x5545,x5546)+P8(x5541,x5542,f43(x5543,x5544,x5541,x5542))+~P4(x5541,f22(a10,f9(x5547),x5545,a47,a47),x5544)+~P4(x5541,f22(a10,f22(a10,f9(x5547),x5545,a47,a47),x5542,a47,a47),x5543) % 0.56/0.71 [556]~P8(x5563,x5565,x5566)+~P4(x5563,f22(a10,f9(x5567),x5565,a47,a47),x5562)+~P4(x5563,f22(a10,f22(a10,f9(x5567),x5565,a47,a47),x5564,a47,a47),x5561)+E(f23(a45,f43(x5561,x5562,x5563,x5564),x5561,a49,a49),x5562) % 0.56/0.71 [499]~P4(x4996,x4992,x4995)+~P4(f33(x4996,x4993,x4995,a49),x4991,x4997)+~P29(f27(a5,x4992))+~P29(f27(a5,x4991))+~E(f27(f27(a45,x4994),x4995),a52)+P29(f27(a5,f19(x4991,x4992,x4993))) % 0.56/0.71 [500]~P4(x5006,x5002,x5004)+~P4(f33(x5006,x5003,x5004,a49),x5001,x5007)+~P29(f27(a5,x5002))+~P29(f27(a5,x5001))+~E(f27(f27(a45,x5004),x5005),a52)+P29(f27(a5,f19(x5001,x5002,x5003))) % 0.56/0.71 %EqnAxiom % 0.56/0.71 [1]E(x11,x11) % 0.56/0.71 [2]E(x22,x21)+~E(x21,x22) % 0.56/0.71 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.56/0.71 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 0.56/0.71 [5]~E(x51,x52)+E(f24(x51,x53),f24(x52,x53)) % 0.56/0.71 [6]~E(x61,x62)+E(f24(x63,x61),f24(x63,x62)) % 0.56/0.71 [7]~E(x71,x72)+E(f22(x71,x73,x74,x75,x76),f22(x72,x73,x74,x75,x76)) % 0.56/0.71 [8]~E(x81,x82)+E(f22(x83,x81,x84,x85,x86),f22(x83,x82,x84,x85,x86)) % 0.56/0.71 [9]~E(x91,x92)+E(f22(x93,x94,x91,x95,x96),f22(x93,x94,x92,x95,x96)) % 0.56/0.71 [10]~E(x101,x102)+E(f22(x103,x104,x105,x101,x106),f22(x103,x104,x105,x102,x106)) % 0.56/0.71 [11]~E(x111,x112)+E(f22(x113,x114,x115,x116,x111),f22(x113,x114,x115,x116,x112)) % 0.56/0.71 [12]~E(x121,x122)+E(f27(x121,x123),f27(x122,x123)) % 0.56/0.71 [13]~E(x131,x132)+E(f27(x133,x131),f27(x133,x132)) % 0.56/0.71 [14]~E(x141,x142)+E(f6(x141),f6(x142)) % 0.56/0.71 [15]~E(x151,x152)+E(f9(x151),f9(x152)) % 0.56/0.71 [16]~E(x161,x162)+E(f8(x161),f8(x162)) % 0.56/0.71 [17]~E(x171,x172)+E(f13(x171,x173,x174),f13(x172,x173,x174)) % 0.56/0.71 [18]~E(x181,x182)+E(f13(x183,x181,x184),f13(x183,x182,x184)) % 0.56/0.71 [19]~E(x191,x192)+E(f13(x193,x194,x191),f13(x193,x194,x192)) % 0.56/0.71 [20]~E(x201,x202)+E(f30(x201,x203),f30(x202,x203)) % 0.56/0.71 [21]~E(x211,x212)+E(f30(x213,x211),f30(x213,x212)) % 0.56/0.71 [22]~E(x221,x222)+E(f11(x221),f11(x222)) % 0.56/0.71 [23]~E(x231,x232)+E(f15(x231,x233),f15(x232,x233)) % 0.56/0.71 [24]~E(x241,x242)+E(f15(x243,x241),f15(x243,x242)) % 0.56/0.71 [25]~E(x251,x252)+E(f29(x251,x253,x254),f29(x252,x253,x254)) % 0.56/0.71 [26]~E(x261,x262)+E(f29(x263,x261,x264),f29(x263,x262,x264)) % 0.56/0.71 [27]~E(x271,x272)+E(f29(x273,x274,x271),f29(x273,x274,x272)) % 0.56/0.71 [28]~E(x281,x282)+E(f18(x281,x283,x284),f18(x282,x283,x284)) % 0.56/0.71 [29]~E(x291,x292)+E(f18(x293,x291,x294),f18(x293,x292,x294)) % 0.56/0.71 [30]~E(x301,x302)+E(f18(x303,x304,x301),f18(x303,x304,x302)) % 0.56/0.71 [31]~E(x311,x312)+E(f33(x311,x313,x314,x315),f33(x312,x313,x314,x315)) % 0.56/0.71 [32]~E(x321,x322)+E(f33(x323,x321,x324,x325),f33(x323,x322,x324,x325)) % 0.56/0.71 [33]~E(x331,x332)+E(f33(x333,x334,x331,x335),f33(x333,x334,x332,x335)) % 0.56/0.71 [34]~E(x341,x342)+E(f33(x343,x344,x345,x341),f33(x343,x344,x345,x342)) % 0.56/0.71 [35]~E(x351,x352)+E(f23(x351,x353,x354,x355,x356),f23(x352,x353,x354,x355,x356)) % 0.56/0.71 [36]~E(x361,x362)+E(f23(x363,x361,x364,x365,x366),f23(x363,x362,x364,x365,x366)) % 0.56/0.71 [37]~E(x371,x372)+E(f23(x373,x374,x371,x375,x376),f23(x373,x374,x372,x375,x376)) % 0.56/0.71 [38]~E(x381,x382)+E(f23(x383,x384,x385,x381,x386),f23(x383,x384,x385,x382,x386)) % 0.56/0.71 [39]~E(x391,x392)+E(f23(x393,x394,x395,x396,x391),f23(x393,x394,x395,x396,x392)) % 0.56/0.71 [40]~E(x401,x402)+E(f26(x401,x403),f26(x402,x403)) % 0.56/0.71 [41]~E(x411,x412)+E(f26(x413,x411),f26(x413,x412)) % 0.56/0.71 [42]~E(x421,x422)+E(f14(x421,x423,x424),f14(x422,x423,x424)) % 0.56/0.71 [43]~E(x431,x432)+E(f14(x433,x431,x434),f14(x433,x432,x434)) % 0.56/0.71 [44]~E(x441,x442)+E(f14(x443,x444,x441),f14(x443,x444,x442)) % 0.56/0.71 [45]~E(x451,x452)+E(f39(x451,x453,x454,x455),f39(x452,x453,x454,x455)) % 0.56/0.71 [46]~E(x461,x462)+E(f39(x463,x461,x464,x465),f39(x463,x462,x464,x465)) % 0.56/0.71 [47]~E(x471,x472)+E(f39(x473,x474,x471,x475),f39(x473,x474,x472,x475)) % 0.56/0.71 [48]~E(x481,x482)+E(f39(x483,x484,x485,x481),f39(x483,x484,x485,x482)) % 0.56/0.71 [49]~E(x491,x492)+E(f28(x491,x493),f28(x492,x493)) % 0.56/0.71 [50]~E(x501,x502)+E(f28(x503,x501),f28(x503,x502)) % 0.56/0.71 [51]~E(x511,x512)+E(f46(x511,x513,x514,x515),f46(x512,x513,x514,x515)) % 0.56/0.71 [52]~E(x521,x522)+E(f46(x523,x521,x524,x525),f46(x523,x522,x524,x525)) % 0.56/0.71 [53]~E(x531,x532)+E(f46(x533,x534,x531,x535),f46(x533,x534,x532,x535)) % 0.56/0.71 [54]~E(x541,x542)+E(f46(x543,x544,x545,x541),f46(x543,x544,x545,x542)) % 0.56/0.71 [55]~E(x551,x552)+E(f25(x551,x553,x554),f25(x552,x553,x554)) % 0.56/0.71 [56]~E(x561,x562)+E(f25(x563,x561,x564),f25(x563,x562,x564)) % 0.56/0.71 [57]~E(x571,x572)+E(f25(x573,x574,x571),f25(x573,x574,x572)) % 0.56/0.71 [58]~E(x581,x582)+E(f17(x581,x583,x584,x585,x586),f17(x582,x583,x584,x585,x586)) % 0.56/0.71 [59]~E(x591,x592)+E(f17(x593,x591,x594,x595,x596),f17(x593,x592,x594,x595,x596)) % 0.56/0.71 [60]~E(x601,x602)+E(f17(x603,x604,x601,x605,x606),f17(x603,x604,x602,x605,x606)) % 0.56/0.71 [61]~E(x611,x612)+E(f17(x613,x614,x615,x611,x616),f17(x613,x614,x615,x612,x616)) % 0.56/0.71 [62]~E(x621,x622)+E(f17(x623,x624,x625,x626,x621),f17(x623,x624,x625,x626,x622)) % 0.56/0.71 [63]~E(x631,x632)+E(f7(x631),f7(x632)) % 0.56/0.71 [64]~E(x641,x642)+E(f44(x641,x643,x644,x645),f44(x642,x643,x644,x645)) % 0.56/0.71 [65]~E(x651,x652)+E(f44(x653,x651,x654,x655),f44(x653,x652,x654,x655)) % 0.56/0.71 [66]~E(x661,x662)+E(f44(x663,x664,x661,x665),f44(x663,x664,x662,x665)) % 0.56/0.71 [67]~E(x671,x672)+E(f44(x673,x674,x675,x671),f44(x673,x674,x675,x672)) % 0.56/0.71 [68]~E(x681,x682)+E(f34(x681),f34(x682)) % 0.56/0.71 [69]~E(x691,x692)+E(f19(x691,x693,x694),f19(x692,x693,x694)) % 0.56/0.71 [70]~E(x701,x702)+E(f19(x703,x701,x704),f19(x703,x702,x704)) % 0.56/0.71 [71]~E(x711,x712)+E(f19(x713,x714,x711),f19(x713,x714,x712)) % 0.56/0.71 [72]~E(x721,x722)+E(f41(x721,x723,x724),f41(x722,x723,x724)) % 0.56/0.71 [73]~E(x731,x732)+E(f41(x733,x731,x734),f41(x733,x732,x734)) % 0.56/0.71 [74]~E(x741,x742)+E(f41(x743,x744,x741),f41(x743,x744,x742)) % 0.56/0.71 [75]~E(x751,x752)+E(f32(x751),f32(x752)) % 0.56/0.71 [76]~E(x761,x762)+E(f40(x761,x763,x764,x765),f40(x762,x763,x764,x765)) % 0.56/0.71 [77]~E(x771,x772)+E(f40(x773,x771,x774,x775),f40(x773,x772,x774,x775)) % 0.56/0.71 [78]~E(x781,x782)+E(f40(x783,x784,x781,x785),f40(x783,x784,x782,x785)) % 0.56/0.71 [79]~E(x791,x792)+E(f40(x793,x794,x795,x791),f40(x793,x794,x795,x792)) % 0.56/0.71 [80]~E(x801,x802)+E(f38(x801,x803,x804,x805),f38(x802,x803,x804,x805)) % 0.56/0.71 [81]~E(x811,x812)+E(f38(x813,x811,x814,x815),f38(x813,x812,x814,x815)) % 0.56/0.71 [82]~E(x821,x822)+E(f38(x823,x824,x821,x825),f38(x823,x824,x822,x825)) % 0.56/0.71 [83]~E(x831,x832)+E(f38(x833,x834,x835,x831),f38(x833,x834,x835,x832)) % 0.56/0.71 [84]~E(x841,x842)+E(f16(x841,x843,x844,x845,x846),f16(x842,x843,x844,x845,x846)) % 0.56/0.71 [85]~E(x851,x852)+E(f16(x853,x851,x854,x855,x856),f16(x853,x852,x854,x855,x856)) % 0.56/0.71 [86]~E(x861,x862)+E(f16(x863,x864,x861,x865,x866),f16(x863,x864,x862,x865,x866)) % 0.56/0.71 [87]~E(x871,x872)+E(f16(x873,x874,x875,x871,x876),f16(x873,x874,x875,x872,x876)) % 0.56/0.71 [88]~E(x881,x882)+E(f16(x883,x884,x885,x886,x881),f16(x883,x884,x885,x886,x882)) % 0.56/0.71 [89]~E(x891,x892)+E(f31(x891),f31(x892)) % 0.56/0.71 [90]~E(x901,x902)+E(f43(x901,x903,x904,x905),f43(x902,x903,x904,x905)) % 0.56/0.71 [91]~E(x911,x912)+E(f43(x913,x911,x914,x915),f43(x913,x912,x914,x915)) % 0.56/0.71 [92]~E(x921,x922)+E(f43(x923,x924,x921,x925),f43(x923,x924,x922,x925)) % 0.56/0.71 [93]~E(x931,x932)+E(f43(x933,x934,x935,x931),f43(x933,x934,x935,x932)) % 0.56/0.71 [94]~E(x941,x942)+E(f20(x941,x943,x944,x945),f20(x942,x943,x944,x945)) % 0.56/0.71 [95]~E(x951,x952)+E(f20(x953,x951,x954,x955),f20(x953,x952,x954,x955)) % 0.56/0.71 [96]~E(x961,x962)+E(f20(x963,x964,x961,x965),f20(x963,x964,x962,x965)) % 0.56/0.71 [97]~E(x971,x972)+E(f20(x973,x974,x975,x971),f20(x973,x974,x975,x972)) % 0.56/0.71 [98]~E(x981,x982)+E(f35(x981,x983,x984,x985),f35(x982,x983,x984,x985)) % 0.56/0.71 [99]~E(x991,x992)+E(f35(x993,x991,x994,x995),f35(x993,x992,x994,x995)) % 0.56/0.71 [100]~E(x1001,x1002)+E(f35(x1003,x1004,x1001,x1005),f35(x1003,x1004,x1002,x1005)) % 0.56/0.71 [101]~E(x1011,x1012)+E(f35(x1013,x1014,x1015,x1011),f35(x1013,x1014,x1015,x1012)) % 0.56/0.71 [102]~E(x1021,x1022)+E(f42(x1021,x1023,x1024,x1025),f42(x1022,x1023,x1024,x1025)) % 0.56/0.71 [103]~E(x1031,x1032)+E(f42(x1033,x1031,x1034,x1035),f42(x1033,x1032,x1034,x1035)) % 0.56/0.71 [104]~E(x1041,x1042)+E(f42(x1043,x1044,x1041,x1045),f42(x1043,x1044,x1042,x1045)) % 0.56/0.71 [105]~E(x1051,x1052)+E(f42(x1053,x1054,x1055,x1051),f42(x1053,x1054,x1055,x1052)) % 0.56/0.71 [106]~E(x1061,x1062)+E(f50(x1061,x1063),f50(x1062,x1063)) % 0.56/0.71 [107]~E(x1071,x1072)+E(f50(x1073,x1071),f50(x1073,x1072)) % 0.56/0.71 [108]~E(x1081,x1082)+E(f37(x1081,x1083,x1084),f37(x1082,x1083,x1084)) % 0.56/0.71 [109]~E(x1091,x1092)+E(f37(x1093,x1091,x1094),f37(x1093,x1092,x1094)) % 0.56/0.71 [110]~E(x1101,x1102)+E(f37(x1103,x1104,x1101),f37(x1103,x1104,x1102)) % 0.56/0.71 [111]~E(x1111,x1112)+E(f21(x1111,x1113,x1114),f21(x1112,x1113,x1114)) % 0.56/0.71 [112]~E(x1121,x1122)+E(f21(x1123,x1121,x1124),f21(x1123,x1122,x1124)) % 0.56/0.71 [113]~E(x1131,x1132)+E(f21(x1133,x1134,x1131),f21(x1133,x1134,x1132)) % 0.56/0.71 [114]~E(x1141,x1142)+E(f36(x1141,x1143,x1144,x1145),f36(x1142,x1143,x1144,x1145)) % 0.56/0.71 [115]~E(x1151,x1152)+E(f36(x1153,x1151,x1154,x1155),f36(x1153,x1152,x1154,x1155)) % 0.56/0.71 [116]~E(x1161,x1162)+E(f36(x1163,x1164,x1161,x1165),f36(x1163,x1164,x1162,x1165)) % 0.56/0.71 [117]~E(x1171,x1172)+E(f36(x1173,x1174,x1175,x1171),f36(x1173,x1174,x1175,x1172)) % 0.56/0.71 [118]~P1(x1181)+P1(x1182)+~E(x1181,x1182) % 0.56/0.71 [119]~P27(x1191)+P27(x1192)+~E(x1191,x1192) % 0.56/0.71 [120]~P28(x1201)+P28(x1202)+~E(x1201,x1202) % 0.56/0.71 [121]~P2(x1211)+P2(x1212)+~E(x1211,x1212) % 0.56/0.71 [122]~P3(x1221)+P3(x1222)+~E(x1221,x1222) % 0.56/0.71 [123]~P11(x1231)+P11(x1232)+~E(x1231,x1232) % 0.56/0.71 [124]~P17(x1241)+P17(x1242)+~E(x1241,x1242) % 0.56/0.71 [125]~P29(x1251)+P29(x1252)+~E(x1251,x1252) % 0.56/0.71 [126]~P18(x1261)+P18(x1262)+~E(x1261,x1262) % 0.56/0.71 [127]~P23(x1271)+P23(x1272)+~E(x1271,x1272) % 0.56/0.71 [128]P6(x1282,x1283,x1284)+~E(x1281,x1282)+~P6(x1281,x1283,x1284) % 0.56/0.71 [129]P6(x1293,x1292,x1294)+~E(x1291,x1292)+~P6(x1293,x1291,x1294) % 0.56/0.71 [130]P6(x1303,x1304,x1302)+~E(x1301,x1302)+~P6(x1303,x1304,x1301) % 0.56/0.71 [131]~P19(x1311)+P19(x1312)+~E(x1311,x1312) % 0.56/0.71 [132]~P20(x1321)+P20(x1322)+~E(x1321,x1322) % 0.56/0.71 [133]~P21(x1331)+P21(x1332)+~E(x1331,x1332) % 0.56/0.71 [134]~P22(x1341)+P22(x1342)+~E(x1341,x1342) % 0.56/0.71 [135]~P24(x1351)+P24(x1352)+~E(x1351,x1352) % 0.56/0.71 [136]~P13(x1361)+P13(x1362)+~E(x1361,x1362) % 0.56/0.71 [137]~P14(x1371)+P14(x1372)+~E(x1371,x1372) % 0.56/0.71 [138]~P15(x1381)+P15(x1382)+~E(x1381,x1382) % 0.56/0.71 [139]P10(x1392,x1393,x1394)+~E(x1391,x1392)+~P10(x1391,x1393,x1394) % 0.56/0.71 [140]P10(x1403,x1402,x1404)+~E(x1401,x1402)+~P10(x1403,x1401,x1404) % 0.56/0.71 [141]P10(x1413,x1414,x1412)+~E(x1411,x1412)+~P10(x1413,x1414,x1411) % 0.56/0.71 [142]P4(x1422,x1423,x1424)+~E(x1421,x1422)+~P4(x1421,x1423,x1424) % 0.56/0.71 [143]P4(x1433,x1432,x1434)+~E(x1431,x1432)+~P4(x1433,x1431,x1434) % 0.56/0.71 [144]P4(x1443,x1444,x1442)+~E(x1441,x1442)+~P4(x1443,x1444,x1441) % 0.56/0.71 [145]P8(x1452,x1453,x1454)+~E(x1451,x1452)+~P8(x1451,x1453,x1454) % 0.56/0.71 [146]P8(x1463,x1462,x1464)+~E(x1461,x1462)+~P8(x1463,x1461,x1464) % 0.56/0.71 [147]P8(x1473,x1474,x1472)+~E(x1471,x1472)+~P8(x1473,x1474,x1471) % 0.56/0.71 [148]P7(x1482,x1483,x1484,x1485)+~E(x1481,x1482)+~P7(x1481,x1483,x1484,x1485) % 0.56/0.71 [149]P7(x1493,x1492,x1494,x1495)+~E(x1491,x1492)+~P7(x1493,x1491,x1494,x1495) % 0.56/0.71 [150]P7(x1503,x1504,x1502,x1505)+~E(x1501,x1502)+~P7(x1503,x1504,x1501,x1505) % 0.56/0.71 [151]P7(x1513,x1514,x1515,x1512)+~E(x1511,x1512)+~P7(x1513,x1514,x1515,x1511) % 0.56/0.71 [152]~P25(x1521)+P25(x1522)+~E(x1521,x1522) % 0.56/0.71 [153]P5(x1532,x1533,x1534)+~E(x1531,x1532)+~P5(x1531,x1533,x1534) % 0.56/0.71 [154]P5(x1543,x1542,x1544)+~E(x1541,x1542)+~P5(x1543,x1541,x1544) % 0.56/0.71 [155]P5(x1553,x1554,x1552)+~E(x1551,x1552)+~P5(x1553,x1554,x1551) % 0.56/0.71 [156]~P12(x1561)+P12(x1562)+~E(x1561,x1562) % 0.56/0.71 [157]~P26(x1571)+P26(x1572)+~E(x1571,x1572) % 0.56/0.71 [158]~P16(x1581)+P16(x1582)+~E(x1581,x1582) % 0.56/0.71 [159]~P9(x1591)+P9(x1592)+~E(x1591,x1592) % 0.56/0.71 % 0.56/0.71 %------------------------------------------- % 0.56/0.71 cnf(588,plain, % 0.56/0.71 (~E(f13(x5881,x5882,x5883),x5882)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(591,plain, % 0.56/0.71 (~E(f13(x5911,x5912,x5913),x5912)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(594,plain, % 0.56/0.71 (~E(f13(x5941,x5942,x5943),x5942)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(597,plain, % 0.56/0.71 (~E(f13(x5971,x5972,x5973),x5972)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(600,plain, % 0.56/0.71 (~E(f13(x6001,x6002,x6003),x6002)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(603,plain, % 0.56/0.71 (~E(f13(x6031,x6032,x6033),x6032)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(620,plain, % 0.56/0.71 (P29(f27(f27(f28(x6201,x6202),x6203),x6203))), % 0.56/0.71 inference(rename_variables,[],[213])). % 0.56/0.71 cnf(625,plain, % 0.56/0.71 (~E(f13(x6251,x6252,x6253),x6252)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(628,plain, % 0.56/0.71 (~E(f13(x6281,x6282,x6283),x6282)), % 0.56/0.71 inference(rename_variables,[],[283])). % 0.56/0.71 cnf(634,plain, % 0.56/0.71 (P29(f27(f27(f28(x6341,x6342),x6343),x6343))), % 0.56/0.71 inference(rename_variables,[],[213])). % 0.56/0.71 cnf(643,plain, % 0.56/0.71 (P29(f27(f27(f28(x6431,x6432),x6433),x6433))), % 0.56/0.71 inference(rename_variables,[],[213])). % 0.56/0.71 cnf(646,plain, % 0.56/0.71 (P29(f27(f27(f28(x6461,x6462),x6463),x6463))), % 0.56/0.71 inference(rename_variables,[],[213])). % 0.56/0.71 cnf(649,plain, % 0.56/0.71 (P29(f27(f27(f28(x6491,x6492),x6493),x6493))), % 0.56/0.71 inference(rename_variables,[],[213])). % 0.56/0.71 cnf(659,plain, % 0.56/0.71 (~P6(f27(f27(f6(a2),x6591),x6592),x6592,a2)), % 0.56/0.71 inference(rename_variables,[],[291])). % 0.56/0.71 cnf(670,plain, % 0.56/0.71 ($false), % 0.56/0.71 inference(scs_inference,[],[297,206,160,277,261,262,210,266,213,620,634,643,646,649,244,279,283,588,591,594,597,600,603,625,628,168,291,659,181,345,306,328,329,334,337,338,455,475,486,489,491,492,505,508,509,510,511,517,532,533,534,543,545,548,551,2,330,389,396,398,427,463,442,444]), % 0.56/0.71 ['proof']). % 0.56/0.71 % SZS output end Proof % 0.56/0.71 % Total time :0.073739s %------------------------------------------------------------------------------