%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL787-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n017.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:50 AM UTC 2026 % Result : Unsatisfiable 0.55s 0.76s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL787-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.06/0.33 % Computer : n017.cluster.edu % 0.06/0.33 % Model : x86_64 x86_64 % 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.33 % Memory : 8046.5625MB % 0.06/0.33 % OS : Linux 6.8.0-71-generic % 0.06/0.33 % CPULimit : 300 % 0.06/0.33 % WCLimit : 300 % 0.06/0.33 % DateTime : Fri Sep 4 14:51:20 UTC 2026 % 0.06/0.34 % CPUTime : % 0.24/0.50 start to proof:theBenchmark % 0.55/0.71 %------------------------------------------- % 0.55/0.71 % File :CSE---1.7 % 0.55/0.71 % Problem :theBenchmark % 0.55/0.71 % Transform :cnf % 0.55/0.71 % Format :tptp:raw % 0.55/0.71 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.71 % 0.55/0.71 % Result :Theorem 0.169129s % 0.55/0.71 % Output :CNFRefutation 0.169129s % 0.55/0.71 %------------------------------------------- % 0.55/0.71 %------------------------------------------------------------------------------ % 0.55/0.71 % File : LCL787-1 : TPTP v9.3.1. Released v4.1.0. % 0.55/0.71 % Domain : Logic Calculi % 0.55/0.71 % Problem : Strong normalization of typed lambda calculus 129_13 % 0.55/0.71 % Version : Especial. % 0.55/0.71 % English : % 0.55/0.71 % 0.55/0.71 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.55/0.71 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.55/0.71 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.55/0.71 % Source : [Nip10] % 0.55/0.71 % Names : StrongNorm-129_13 [Nip10] % 0.55/0.71 % 0.55/0.71 % Status : Unsatisfiable % 0.55/0.71 % Rating : 0.17 v9.3.0, 0.09 v9.1.0, 0.10 v8.2.0, 0.19 v8.1.0, 0.26 v7.4.0, 0.24 v7.3.0, 0.17 v7.0.0, 0.33 v6.3.0, 0.18 v6.2.0, 0.30 v6.1.0, 0.43 v6.0.0, 0.60 v5.5.0, 0.75 v5.3.0, 0.78 v5.2.0, 0.69 v5.1.0, 0.71 v5.0.0, 0.57 v4.1.0 % 0.55/0.71 % Syntax : Number of clauses : 378 ( 140 unt; 38 nHn; 212 RR) % 0.55/0.71 % Number of literals : 724 ( 305 equ; 331 neg) % 0.55/0.71 % Maximal clause size : 6 ( 1 avg) % 0.55/0.71 % Maximal term depth : 6 ( 2 avg) % 0.55/0.71 % Number of predicates : 30 ( 29 usr; 1 prp; 0-4 aty) % 0.55/0.71 % Number of functors : 65 ( 65 usr; 23 con; 0-5 aty) % 0.55/0.71 % Number of variables : 1159 ( 200 sgn) % 0.55/0.71 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.55/0.71 % 0.55/0.71 % Comments : % 0.55/0.71 %------------------------------------------------------------------------------ % 0.55/0.71 cnf(cls_accp__downwards_0,axiom, % 0.55/0.71 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.55/0.71 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) % 0.55/0.71 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_Nitpick_Ortranclp__def_1,axiom, % 0.55/0.71 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_x)) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_rtranclp_Ortrancl__refl_0,axiom, % 0.55/0.71 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_a)) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_replicate__eq__replicate_0,axiom, % 0.55/0.71 ( c_List_Oreplicate(V_m,V_x,T_a) != c_List_Oreplicate(V_n,V_y,T_a) % 0.55/0.71 | V_m = V_n ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_listsp_ONil_0,axiom, % 0.55/0.71 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_Cons__step1__Cons_4,axiom, % 0.55/0.71 ( ~ hBOOL(hAPP(hAPP(V_r,V_y),V_xa)) % 0.55/0.71 | 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.55/0.71 % 0.55/0.71 cnf(cls_Cons__step1__Cons_2,axiom, % 0.55/0.72 ( V_x = V_y % 0.55/0.72 | V_xs = V_ys % 0.55/0.72 | ~ 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.55/0.72 % 0.55/0.72 cnf(cls_append__in__listsp__conv_1,axiom, % 0.55/0.72 ( c_List_Olistsp(V_A,V_ys,T_a) % 0.55/0.72 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_append__in__listsp__conv_0,axiom, % 0.55/0.72 ( c_List_Olistsp(V_A,V_xs,T_a) % 0.55/0.72 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_rotate__simps_0,axiom, % 0.55/0.72 c_List_Orotate1(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_append__step1I_1,axiom, % 0.55/0.72 ( 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.55/0.72 | ~ c_ListOrder_Ostep1(V_r,V_vs,V_us,T_a) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_append__step1I_0,axiom, % 0.55/0.72 ( ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_double__eq__0__iff_1,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_add__cancel__21_1,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_conversep_Ointros_0,axiom, % 0.55/0.72 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_b),V_a)) % 0.55/0.72 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_conversep_Ocases_0,axiom, % 0.55/0.72 ( hBOOL(hAPP(hAPP(V_r,V_a2),V_a1)) % 0.55/0.72 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a1),V_a2)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_conversep__iff_1,axiom, % 0.55/0.72 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) % 0.55/0.72 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_a)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_conversepD_0,axiom, % 0.55/0.72 ( hBOOL(hAPP(hAPP(V_r,V_b),V_a)) % 0.55/0.72 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_add__cancel__21_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.72 | 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.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) = V_u ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_rtranclp__converseD_0,axiom, % 0.55/0.72 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) % 0.55/0.72 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_rtranclp__converseI_0,axiom, % 0.55/0.72 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) % 0.55/0.72 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.55/0.72 | ~ class_Int_Onumber__ring(T_a) % 0.55/0.72 | 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.55/0.72 | V_y = V_z ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_add__imp__eq_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.55/0.72 | 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.55/0.72 | V_b = V_c ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_add__left__cancel_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.55/0.72 | 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.55/0.72 | V_b = V_c ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_add__right__cancel_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.55/0.72 | 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.55/0.72 | V_b = V_c ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_Cons__step1__Cons_0,axiom, % 0.55/0.72 ( V_x = V_y % 0.55/0.72 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.55/0.72 | ~ 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.55/0.72 % 0.55/0.72 cnf(cls_last__replicate_0,axiom, % 0.55/0.72 ( c_List_Olast(c_List_Oreplicate(V_n,V_x,T_a),T_a) = V_x % 0.55/0.72 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | 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.55/0.72 % 0.55/0.72 cnf(cls_replicate__eq__replicate_2,axiom, % 0.55/0.72 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.55/0.72 % 0.55/0.72 cnf(cls_rev__is__Nil__conv_0,axiom, % 0.55/0.72 ( c_List_Orev(V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.55/0.72 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_replicate__eq__replicate_1,axiom, % 0.55/0.72 ( c_List_Oreplicate(V_m,V_x,T_a) != c_List_Oreplicate(V_n,V_y,T_a) % 0.55/0.72 | V_x = V_y % 0.55/0.72 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_rtranclp__idemp_0,axiom, % 0.55/0.72 c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(V_r,T_a),T_a) = c_Transitive__Closure_Ortranclp(V_r,T_a) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_x) = V_x ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.55/0.72 | ~ class_Int_Onumber__ring(T_a) % 0.55/0.72 | V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_HOL_Ozero__class_Ozero(T_a)) ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_add__0__left_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.55/0.72 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.55/0.72 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.72 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_rev__is__Nil__conv_1,axiom, % 0.55/0.72 c_List_Orev(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_rev__append_0,axiom, % 0.55/0.72 c_List_Orev(c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Oappend(c_List_Orev(V_ys,T_a),c_List_Orev(V_xs,T_a),T_a) ). % 0.55/0.72 % 0.55/0.72 cnf(cls_accp__downwards__aux_0,axiom, % 0.55/0.72 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.55/0.73 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rtranclp__trans_0,axiom, % 0.55/0.73 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_z)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_z)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_IT__implies__termi_0,axiom, % 0.55/0.73 ( c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_t,tc_Lambda_OdB) % 0.55/0.73 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_termi__implies__IT_0,axiom, % 0.55/0.73 ( hBOOL(hAPP(c_InductTermi_OIT,V_r)) % 0.55/0.73 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_r,tc_Lambda_OdB) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_take__eq__Nil_2,axiom, % 0.55/0.73 c_List_Otake(V_n,c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rotate1__is__Nil__conv_0,axiom, % 0.55/0.73 ( c_List_Orotate1(V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.55/0.73 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rev__swap_0,axiom, % 0.55/0.73 V_xs = c_List_Orev(c_List_Orev(V_xs,T_a),T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rev__swap_1,axiom, % 0.55/0.73 c_List_Orev(c_List_Orev(V_ys,T_a),T_a) = V_ys ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rev__rev__ident_0,axiom, % 0.55/0.73 c_List_Orev(c_List_Orev(V_xs,T_a),T_a) = V_xs ). % 0.55/0.73 % 0.55/0.73 cnf(cls_append__eq__conv__conj_0,axiom, % 0.55/0.73 V_xs = c_List_Otake(c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),c_List_Oappend(V_xs,V_ys,T_a),T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.73 | 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.55/0.73 % 0.55/0.73 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.73 | 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.55/0.73 % 0.55/0.73 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.73 | 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.55/0.73 % 0.55/0.73 cnf(cls_foldl__assoc_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Osemigroup__add(T_a) % 0.55/0.73 | 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.55/0.73 % 0.55/0.73 cnf(cls_rev__replicate_0,axiom, % 0.55/0.73 c_List_Orev(c_List_Oreplicate(V_n,V_x,T_a),T_a) = c_List_Oreplicate(V_n,V_x,T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_of__nat__eq__iff_0,axiom, % 0.55/0.73 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.55/0.73 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.55/0.73 | V_m = V_n ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.55/0.73 | ~ class_Int_Onumber__ring(T_a) % 0.55/0.73 | V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_a) % 0.55/0.73 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_double__eq__0__iff_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.73 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.55/0.73 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_r__into__rtranclp_0,axiom, % 0.55/0.73 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_not__Nil__step1_0,axiom, % 0.55/0.73 ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_not__step1__Nil_0,axiom, % 0.55/0.73 ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_take__butlast_0,axiom, % 0.55/0.73 ( c_List_Otake(V_n,c_List_Obutlast(V_xs,T_a),T_a) = c_List_Otake(V_n,V_xs,T_a) % 0.55/0.73 | ~ c_HOL_Oord__class_Oless(V_n,c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),tc_nat) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_conversep__eq_0,axiom, % 0.55/0.73 c_Predicate_Oconversep(c_fequal(T_a),T_a,T_a) = c_fequal(T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_length__rotate1_0,axiom, % 0.55/0.73 c_Nat_Osize__class_Osize(c_List_Orotate1(V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_Cons__step1__Cons_3,axiom, % 0.55/0.73 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.55/0.73 | V_xs = V_ys % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_append__replicate__commute_0,axiom, % 0.55/0.73 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.55/0.73 % 0.55/0.73 cnf(cls_add__strict__mono_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rev__is__rev__conv_0,axiom, % 0.55/0.73 ( c_List_Orev(V_xs,T_a) != c_List_Orev(V_ys,T_a) % 0.55/0.73 | V_xs = V_ys ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_append__in__listsp__conv_2,axiom, % 0.55/0.73 ( c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) % 0.55/0.73 | ~ c_List_Olistsp(V_A,V_ys,T_a) % 0.55/0.73 | ~ c_List_Olistsp(V_A,V_xs,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_length__replicate_0,axiom, % 0.55/0.73 c_Nat_Osize__class_Osize(c_List_Oreplicate(V_n,V_x,T_a),tc_List_Olist(T_a)) = V_n ). % 0.55/0.73 % 0.55/0.73 cnf(cls_Nil__is__rev__conv_0,axiom, % 0.55/0.73 ( c_List_Olist_ONil(T_a) != c_List_Orev(V_xs,T_a) % 0.55/0.73 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_conversep__conversep_0,axiom, % 0.55/0.73 c_Predicate_Oconversep(c_Predicate_Oconversep(V_r,T_a,T_b),T_b,T_a) = V_r ). % 0.55/0.73 % 0.55/0.73 cnf(cls_add__strict__right__mono_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_add__less__cancel__right_1,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_add__less__cancel__right_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_add__strict__left__mono_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_add__less__cancel__left_1,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_add__less__cancel__left_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_Cons__step1__Cons_1,axiom, % 0.55/0.73 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.55/0.73 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_Cons__step1__Cons_5,axiom, % 0.55/0.73 ( 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.55/0.73 | ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_butlast_Osimps_I1_J_0,axiom, % 0.55/0.73 c_List_Obutlast(c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_Nil__is__rev__conv_1,axiom, % 0.55/0.73 c_List_Olist_ONil(T_a) = c_List_Orev(c_List_Olist_ONil(T_a),T_a) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_length__rev_0,axiom, % 0.55/0.73 c_Nat_Osize__class_Osize(c_List_Orev(V_xs,T_a),tc_List_Olist(T_a)) = c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_converse__rtranclp__into__rtranclp_0,axiom, % 0.55/0.73 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_c)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom, % 0.55/0.73 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_c)) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_b)) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_accp_Ocases_0,axiom, % 0.55/0.73 ( c_Wellfounded_Oaccp(V_r,V_y,T_a) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(V_r,V_y),V_a)) % 0.55/0.73 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_accp__downward_0,axiom, % 0.55/0.73 ( c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.55/0.73 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) % 0.55/0.73 | ~ c_Wellfounded_Oaccp(V_r,V_b,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_append__butlast__last__id_0,axiom, % 0.55/0.73 ( c_List_Oappend(c_List_Obutlast(V_xs,T_a),c_List_Olist_OCons(c_List_Olast(V_xs,T_a),c_List_Olist_ONil(T_a),T_a),T_a) = V_xs % 0.55/0.73 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_add__neg__neg_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_even__less__0__iff_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_even__less__0__iff_1,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_add__pos__pos_0,axiom, % 0.55/0.73 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.55/0.73 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_pos__add__strict_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(V_b,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),T_a) % 0.55/0.73 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.55/0.73 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_of__nat__0_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.55/0.73 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_of__nat__less__iff_1,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.55/0.73 | 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.55/0.73 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.55/0.73 % 0.55/0.73 cnf(cls_of__nat__less__iff_0,axiom, % 0.55/0.73 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.55/0.73 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.55/0.73 | ~ 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.55/0.73 % 0.55/0.73 cnf(cls_replicate__empty_1,axiom, % 0.55/0.74 c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_take__eq__Nil_0,axiom, % 0.55/0.74 ( c_List_Otake(V_n,V_xs,T_a) != c_List_Olist_ONil(T_a) % 0.55/0.74 | V_xs = c_List_Olist_ONil(T_a) % 0.55/0.74 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_length__0__conv_1,axiom, % 0.55/0.74 c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_empty__replicate_1,axiom, % 0.55/0.74 c_List_Olist_ONil(T_a) = c_List_Oreplicate(c_HOL_Ozero__class_Ozero(tc_nat),V_x,T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_take__0_0,axiom, % 0.55/0.74 c_List_Otake(c_HOL_Ozero__class_Ozero(tc_nat),V_xs,T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_replicate__empty_0,axiom, % 0.55/0.74 ( c_List_Oreplicate(V_n,V_x,T_a) != c_List_Olist_ONil(T_a) % 0.55/0.74 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_empty__replicate_0,axiom, % 0.55/0.74 ( c_List_Olist_ONil(T_a) != c_List_Oreplicate(V_n,V_x,T_a) % 0.55/0.74 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_length__0__conv_0,axiom, % 0.55/0.74 ( c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.55/0.74 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_singleton__rev__conv_1,axiom, % 0.55/0.74 c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) = c_List_Orev(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_last_Osimps_1,axiom, % 0.55/0.74 ( c_List_Olast(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olast(V_xs,T_a) % 0.55/0.74 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_rev__singleton__conv_1,axiom, % 0.55/0.74 c_List_Orev(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_singleton__rev__conv_0,axiom, % 0.55/0.74 ( c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) != c_List_Orev(V_xs,T_a) % 0.55/0.74 | V_xs = c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_rev__singleton__conv_0,axiom, % 0.55/0.74 ( c_List_Orev(V_xs,T_a) != c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) % 0.55/0.74 | V_xs = c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_butlast_Osimps_I2_J_0,axiom, % 0.55/0.74 c_List_Obutlast(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_last_Osimps_0,axiom, % 0.55/0.74 c_List_Olast(c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) = V_x ). % 0.55/0.74 % 0.55/0.74 cnf(cls_butlast_Osimps_I2_J_1,axiom, % 0.55/0.74 ( c_List_Obutlast(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_OCons(V_x,c_List_Obutlast(V_xs,T_a),T_a) % 0.55/0.74 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_foldl__absorb0_0,axiom, % 0.55/0.74 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.55/0.74 | 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.55/0.74 % 0.55/0.74 cnf(cls_append__eq__Cons__conv_3,axiom, % 0.55/0.74 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.55/0.74 | c_List_Oappend(c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) = V_xs % 0.55/0.74 | V_zs = c_List_Olist_OCons(V_x,V_xs,T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Cons__eq__append__conv_2,axiom, % 0.55/0.74 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.55/0.74 | c_List_Olist_OCons(V_x,c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) = V_ys % 0.55/0.74 | c_List_Olist_OCons(V_x,V_xs,T_a) = V_zs ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_append__eq__Cons__conv_2,axiom, % 0.55/0.74 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.55/0.74 | V_ys = c_List_Olist_OCons(V_x,c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) % 0.55/0.74 | V_zs = c_List_Olist_OCons(V_x,V_xs,T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Cons__eq__append__conv_3,axiom, % 0.55/0.74 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.55/0.74 | V_xs = c_List_Oappend(c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) % 0.55/0.74 | c_List_Olist_OCons(V_x,V_xs,T_a) = V_zs ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_replicate__app__Cons__same_0,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_butlast__append_0,axiom, % 0.55/0.74 c_List_Obutlast(c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Obutlast(V_xs,T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_last__append_1,axiom, % 0.55/0.74 ( c_List_Olast(c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Olast(V_ys,T_a) % 0.55/0.74 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_last__append_0,axiom, % 0.55/0.74 c_List_Olast(c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a),T_a) = c_List_Olast(V_xs,T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_butlast__append_1,axiom, % 0.55/0.74 ( c_List_Obutlast(c_List_Oappend(V_xs,V_ys,T_a),T_a) = c_List_Oappend(V_xs,c_List_Obutlast(V_ys,T_a),T_a) % 0.55/0.74 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_rtrancl__beta__App_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) % 0.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_rtrancl__beta__AppL_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_rtrancl__beta__AppR_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_rtrancl__beta__Abs_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.55/0.74 ( 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.55/0.74 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_subst__preserves__beta2_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_subst__preserves__beta_H_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_subst__preserves__beta2_H_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_head__Var__reduction_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ 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.55/0.74 % 0.55/0.74 cnf(cls_subject__reduction_H_0,axiom, % 0.55/0.74 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.55/0.74 | ~ c_Type_Otyping(V_e,V_t,V_T) % 0.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_lift__preserves__beta_H_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_foldr__conv__foldl_0,axiom, % 0.55/0.74 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.55/0.74 | 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.55/0.74 % 0.55/0.74 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.55/0.74 ( 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.55/0.74 | V_r = V_s ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_var__app__types_1,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ 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.55/0.74 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.55/0.74 | ~ 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.55/0.74 % 0.55/0.74 cnf(cls_Lambda_0,axiom, % 0.55/0.74 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.55/0.74 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_appR_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_appL_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_uIT_0,axiom, % 0.55/0.74 hBOOL(hAPP(c_InductTermi_OIT,v_u____)) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_subst__lift_0,axiom, % 0.55/0.74 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.55/0.74 % 0.55/0.74 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.55/0.74 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.55/0.74 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_lift__preserves__beta_0,axiom, % 0.55/0.74 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_not__Cons__self2_0,axiom, % 0.55/0.74 c_List_Olist_OCons(V_x,V_t,T_a) != V_t ). % 0.55/0.74 % 0.55/0.74 cnf(cls_not__Cons__self_0,axiom, % 0.55/0.74 V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Cons__eq__append__conv_4,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_app__Var__IT_0,axiom, % 0.55/0.74 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),c_Lambda_OdB_OVar(V_i)))) % 0.55/0.74 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Nil__is__append__conv_2,axiom, % 0.55/0.74 c_List_Olist_ONil(T_a) = c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_abs_0,axiom, % 0.55/0.74 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_foldl__append_0,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_type_Osimps_I5_J_0,axiom, % 0.55/0.74 c_Type_Otype_Otype__case(V_f1,V_f2,c_Type_Otype_OAtom(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Cons_0,axiom, % 0.55/0.74 v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_IT_OVar_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_head__Var__reduction_1,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ 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.55/0.74 % 0.55/0.74 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.55/0.74 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.55/0.74 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.55/0.74 | ~ 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.55/0.74 % 0.55/0.74 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.55/0.74 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.55/0.74 | 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.55/0.74 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_foldl__foldr1_0,axiom, % 0.55/0.74 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.55/0.74 | 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.55/0.74 % 0.55/0.74 cnf(cls_foldl__foldr1__lemma_0,axiom, % 0.55/0.74 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.55/0.74 | 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.55/0.74 % 0.55/0.74 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.55/0.74 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.55/0.74 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.55/0.74 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.55/0.74 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.55/0.74 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.55/0.74 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.55/0.74 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.55/0.74 % 0.55/0.74 cnf(cls_apps__preserves__beta2_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_apps__preserves__betas_0,axiom, % 0.55/0.74 ( 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.55/0.74 | ~ c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,V_ss,tc_Lambda_OdB) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_double__induction__lemma_0,axiom, % 0.55/0.74 ( ~ 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.55/0.74 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_s,tc_Lambda_OdB) % 0.55/0.74 | 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.55/0.74 % 0.55/0.74 cnf(cls_Cons__eq__append__conv_1,axiom, % 0.55/0.74 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.55/0.74 | V_xs = c_List_Oappend(c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) % 0.55/0.74 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_append__eq__Cons__conv_0,axiom, % 0.55/0.74 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.55/0.74 | V_ys = c_List_Olist_OCons(V_x,c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) % 0.55/0.74 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.74 % 0.55/0.74 cnf(cls_last__snoc_0,axiom, % 0.55/0.74 c_List_Olast(c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) = V_x ). % 0.55/0.74 % 0.55/0.74 cnf(cls_butlast__snoc_0,axiom, % 0.55/0.74 c_List_Obutlast(c_List_Oappend(V_xs,c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a),T_a) = V_xs ). % 0.55/0.74 % 0.55/0.74 cnf(cls_Snoc__step1__SnocD_2,axiom, % 0.55/0.74 ( V_ys = V_xs % 0.55/0.74 | V_y = V_x % 0.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_Snoc__step1__SnocD_3,axiom, % 0.55/0.75 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.55/0.75 | V_y = V_x % 0.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_append__eq__Cons__conv_1,axiom, % 0.55/0.75 ( c_List_Oappend(V_ys,V_zs,T_a) != c_List_Olist_OCons(V_x,V_xs,T_a) % 0.55/0.75 | c_List_Oappend(c_List_Osko__List__Xappend__eq__Cons__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),V_zs,T_a) = V_xs % 0.55/0.75 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Cons__eq__append__conv_0,axiom, % 0.55/0.75 ( c_List_Olist_OCons(V_x,V_xs,T_a) != c_List_Oappend(V_ys,V_zs,T_a) % 0.55/0.75 | c_List_Olist_OCons(V_x,c_List_Osko__List__XCons__eq__append__conv__1__1(V_x,V_xs,V_ys,V_zs,T_a),T_a) = V_ys % 0.55/0.75 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_rev_Osimps_I2_J_0,axiom, % 0.55/0.75 c_List_Orev(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Oappend(c_List_Orev(V_xs,T_a),c_List_Olist_OCons(V_x,c_List_Olist_ONil(T_a),T_a),T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Snoc__step1__SnocD_1,axiom, % 0.55/0.75 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.55/0.75 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_rev__eq__Cons__iff_0,axiom, % 0.55/0.75 ( c_List_Orev(V_xs,T_a) != c_List_Olist_OCons(V_y,V_ys,T_a) % 0.55/0.75 | V_xs = c_List_Oappend(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_rev__eq__Cons__iff_1,axiom, % 0.55/0.75 c_List_Orev(c_List_Oappend(c_List_Orev(V_ys,T_a),c_List_Olist_OCons(V_y,c_List_Olist_ONil(T_a),T_a),T_a),T_a) = c_List_Olist_OCons(V_y,V_ys,T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_rotate__simps_1,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_Snoc__step1__SnocD_0,axiom, % 0.55/0.75 ( V_ys = V_xs % 0.55/0.75 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_replicate__append__same_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_length__greater__0__conv_1,axiom, % 0.55/0.75 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)),tc_nat) % 0.55/0.75 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_length__greater__0__conv_0,axiom, % 0.55/0.75 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)),tc_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_take__Cons_H_0,axiom, % 0.55/0.75 c_List_Otake(c_HOL_Ozero__class_Ozero(tc_nat),c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Osplit_0,axiom, % 0.55/0.75 ( ~ hBOOL(hAPP(V_P,c_Type_Otype_Otype__case(V_f1,V_f2,c_Type_Otype_OAtom(V_nat),t_a))) % 0.55/0.75 | hBOOL(hAPP(V_P,hAPP(V_f1,V_nat))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Osplit__asm_0,axiom, % 0.55/0.75 ( ~ hBOOL(hAPP(V_P,c_Type_Otype_Otype__case(V_f1,V_f2,c_Type_Otype_OAtom(V_xc),t_a))) % 0.55/0.75 | hBOOL(hAPP(V_P,hAPP(V_f1,V_xc))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_list_Osimps_I3_J_0,axiom, % 0.55/0.75 c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_neq__Nil__conv_1,axiom, % 0.55/0.75 c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Cons__eq__appendI_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_Cons__eq__append__conv_5,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_dB_Orecs_I2_J_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_append__Cons_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_append__eq__Cons__conv_5,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.55/0.75 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.55/0.75 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_foldl__Cons_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_type__induct_2,axiom, % 0.55/0.75 ( hBOOL(hAPP(V_P,V_T)) % 0.55/0.75 | ~ hBOOL(hAPP(V_P,c_Type_Osko__Type__Xtype__induct__1__1(V_P))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_subst__Var_1,axiom, % 0.55/0.75 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.55/0.75 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_list__app__typeE_1,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_not__less0_0,axiom, % 0.55/0.75 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_gr__implies__not0_0,axiom, % 0.55/0.75 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_typing__elims_I2_J_1,axiom, % 0.55/0.75 ( c_Type_Otyping(V_e,V_u,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u)) % 0.55/0.75 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_xt1_I10_J_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_order__less__trans_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_typing__elims_I3_J_1,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I11_J_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_Var_I3_J_0,axiom, % 0.55/0.75 hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_subst__Var_2,axiom, % 0.55/0.75 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.55/0.75 | V_i = V_k % 0.55/0.75 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I12_J_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_subst__preserves__beta_0,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__same__eq_0,axiom, % 0.55/0.75 ( c_List_Oappend(V_ys,V_xs,T_a) != c_List_Oappend(V_zs,V_xs,T_a) % 0.55/0.75 | V_ys = V_zs ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_same__append__eq_0,axiom, % 0.55/0.75 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Oappend(V_xs,V_zs,T_a) % 0.55/0.75 | V_ys = V_zs ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__Nil2_0,axiom, % 0.55/0.75 c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) = V_xs ). % 0.55/0.75 % 0.55/0.75 cnf(cls_eq__Nil__appendI_0,axiom, % 0.55/0.75 V_x = c_List_Oappend(c_List_Olist_ONil(T_a),V_x,T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_self__append__conv_1,axiom, % 0.55/0.75 V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__Nil_0,axiom, % 0.55/0.75 c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) = V_ys ). % 0.55/0.75 % 0.55/0.75 cnf(cls_self__append__conv2_1,axiom, % 0.55/0.75 V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Osimps_I1_J_0,axiom, % 0.55/0.75 ( c_Type_Otype_OAtom(V_nat) != c_Type_Otype_OAtom(V_nat_H) % 0.55/0.75 | V_nat = V_nat_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_Beta_0,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_foldl__Nil_0,axiom, % 0.55/0.75 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.55/0.75 % 0.55/0.75 cnf(cls_lift__IT_0,axiom, % 0.55/0.75 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(V_t,V_i))) % 0.55/0.75 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_Nil__is__append__conv_0,axiom, % 0.55/0.75 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.55/0.75 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Nil__is__append__conv_1,axiom, % 0.55/0.75 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.55/0.75 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.55/0.75 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.55/0.75 | V_dB = V_dB_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__is__Nil__conv_0,axiom, % 0.55/0.75 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.55/0.75 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__is__Nil__conv_1,axiom, % 0.55/0.75 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.55/0.75 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.55/0.75 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.55/0.75 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Orecs_I1_J_0,axiom, % 0.55/0.75 c_Type_Otype_Otype__rec(V_f1,V_f2,c_Type_Otype_OAtom(V_nat),T_a) = hAPP(V_f1,V_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_apps__preserves__beta_0,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_nat__less__le_1,axiom, % 0.55/0.75 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_less__not__refl_0,axiom, % 0.55/0.75 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_order__less__le_1,axiom, % 0.55/0.75 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_linorder__neq__iff_1,axiom, % 0.55/0.75 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_order__less__irrefl_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_beta_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.55/0.75 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.75 | V_x = V_y ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.75 | V_x = V_y % 0.55/0.75 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_nat__neq__iff_0,axiom, % 0.55/0.75 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.55/0.75 | V_m = V_n ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_nat__less__cases_0,axiom, % 0.55/0.75 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.55/0.75 | V_m = V_n % 0.55/0.75 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_linorder__neqE__nat_0,axiom, % 0.55/0.75 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.55/0.75 | V_x = V_y ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_linorder__neqE_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.75 | V_x = V_y ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_linorder__less__linear_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.75 | V_x = V_y % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.75 | V_x = V_y % 0.55/0.75 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.75 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.55/0.75 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.55/0.75 | V_dB2 = V_dB2_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.55/0.75 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.55/0.75 | V_dB1 = V_dB1_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.55/0.75 ( 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.55/0.75 | V_rs = V_ss ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.55/0.75 ( 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.55/0.75 | V_r = V_s ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.55/0.75 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.55/0.75 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_list_Osimps_I2_J_0,axiom, % 0.55/0.75 c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_gr0I_0,axiom, % 0.55/0.75 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.55/0.75 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Orecs_I3_J_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_neq0__conv_1,axiom, % 0.55/0.75 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_list__app__typeD_1,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_subst__lt_0,axiom, % 0.55/0.75 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osplit_2,axiom, % 0.55/0.75 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_dB),t_a))) % 0.55/0.75 | hBOOL(hAPP(V_P,hAPP(V_f3,V_dB))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osplit__asm_2,axiom, % 0.55/0.75 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OAbs(V_xa),t_a))) % 0.55/0.75 | hBOOL(hAPP(V_P,hAPP(V_f3,V_xa))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_subst__Var__IT_0,axiom, % 0.55/0.75 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j))) % 0.55/0.75 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__self__conv_0,axiom, % 0.55/0.75 ( c_List_Oappend(V_xs,V_ys,T_a) != V_xs % 0.55/0.75 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_self__append__conv_0,axiom, % 0.55/0.75 ( V_xs != c_List_Oappend(V_xs,V_ys,T_a) % 0.55/0.75 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__self__conv2_0,axiom, % 0.55/0.75 ( c_List_Oappend(V_xs,V_ys,T_a) != V_ys % 0.55/0.75 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_self__append__conv2_0,axiom, % 0.55/0.75 ( V_ys != c_List_Oappend(V_xs,V_ys,T_a) % 0.55/0.75 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__eq__Cons__conv_4,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_dB_Osplit_1,axiom, % 0.55/0.75 ( ~ 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.55/0.75 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_dB1),V_dB2))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osplit__asm_1,axiom, % 0.55/0.75 ( ~ 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.55/0.75 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_xb),V_xc))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_list_Oinject_0,axiom, % 0.55/0.75 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.55/0.75 | V_a = V_a_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_list_Oinject_1,axiom, % 0.55/0.75 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.55/0.75 | V_list = V_list_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.55/0.75 ( 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.55/0.75 | V_rs = V_ss ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.55/0.75 ( 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.55/0.75 | V_m = V_n ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.55/0.75 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_var__app__typesE_1,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ 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.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.55/0.75 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_subst__App_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_append1__eq__conv_0,axiom, % 0.55/0.75 ( 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.55/0.75 | V_xs = V_ys ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append1__eq__conv_1,axiom, % 0.55/0.75 ( 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.55/0.75 | V_x = V_y ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__is__Nil__conv_2,axiom, % 0.55/0.75 c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_append__assoc_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_append__eq__appendI_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_append__eq__append__conv2_4,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_append__eq__append__conv2_5,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_xt1_I9_J_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.55/0.75 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_order__less__asym_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_order__less__asym_H_0,axiom, % 0.55/0.75 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.55/0.75 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_lift__type_0,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Osimps_I4_J_0,axiom, % 0.55/0.75 hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) != c_Type_Otype_OAtom(V_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_uT_0,axiom, % 0.55/0.75 c_Type_Otyping(v_e____,v_u____,v_T____) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.55/0.75 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.55/0.75 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.55/0.75 | V_nat = V_nat_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osplit__asm_0,axiom, % 0.55/0.75 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_xd),t_a))) % 0.55/0.75 | hBOOL(hAPP(V_P,hAPP(V_f1,V_xd))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_dB_Osplit_0,axiom, % 0.55/0.75 ( ~ hBOOL(hAPP(V_P,c_Lambda_OdB_OdB__case(V_f1,V_f2,V_f3,c_Lambda_OdB_OVar(V_nat),t_a))) % 0.55/0.75 | hBOOL(hAPP(V_P,hAPP(V_f1,V_nat))) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_typing__elims_I3_J_0,axiom, % 0.55/0.75 ( 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.55/0.75 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_subject__reduction_0,axiom, % 0.55/0.75 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.55/0.75 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.55/0.75 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_subst__eq_0,axiom, % 0.55/0.75 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Osimps_I2_J_0,axiom, % 0.55/0.75 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.55/0.75 | V_type1 = V_type1_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_type_Osimps_I2_J_1,axiom, % 0.55/0.75 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.55/0.75 | V_type2 = V_type2_H ) ). % 0.55/0.75 % 0.55/0.75 cnf(cls_foldr_Osimps_I2_J_0,axiom, % 0.55/0.75 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.55/0.75 % 0.55/0.75 cnf(cls_var__app__types_0,axiom, % 0.55/0.76 ( 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.55/0.76 | ~ 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.55/0.76 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_shift__gt_0,axiom, % 0.55/0.76 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,V_j) % 0.55/0.76 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_type__induct_1,axiom, % 0.55/0.76 ( c_Type_Osko__Type__Xtype__induct__1__1(V_P) != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.55/0.76 | hBOOL(hAPP(V_P,V_T)) % 0.55/0.76 | hBOOL(hAPP(V_P,V_T2)) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_type__induct_0,axiom, % 0.55/0.76 ( c_Type_Osko__Type__Xtype__induct__1__1(V_P) != hAPP(hAPP(c_Type_Otype_OFun,V_T1a),V_x) % 0.55/0.76 | hBOOL(hAPP(V_P,V_T)) % 0.55/0.76 | hBOOL(hAPP(V_P,V_T1a)) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_beta__cases_I1_J_0,axiom, % 0.55/0.76 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_App_0,axiom, % 0.55/0.76 ( c_Type_Otyping(V_env,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_U) % 0.55/0.76 | ~ c_Type_Otyping(V_env,V_t,V_T) % 0.55/0.76 | ~ c_Type_Otyping(V_env,V_s,hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_var__app__type__eq_0,axiom, % 0.55/0.76 ( V_T = V_U % 0.55/0.76 | ~ 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.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_dB_Orecs_I1_J_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.55/0.76 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_MI2_0,axiom, % 0.55/0.76 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.55/0.76 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.55/0.76 | ~ c_Type_Otyping(V_e,V_u,V_T2) % 0.55/0.76 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.55/0.76 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T2,tc_Type_Otype),V_t,V_Ta) % 0.55/0.76 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_MI1_0,axiom, % 0.55/0.76 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.55/0.76 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.55/0.76 | ~ c_Type_Otyping(V_e,V_u,V_T1) % 0.55/0.76 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.55/0.76 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T1,tc_Type_Otype),V_t,V_Ta) % 0.55/0.76 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_shift__eq_0,axiom, % 0.55/0.76 hAPP(c_Type_Oshift(V_e,V_x,V_T,T_a),V_x) = V_T ). % 0.55/0.76 % 0.55/0.76 cnf(cls_Abs_0,axiom, % 0.55/0.76 ( c_Type_Otyping(V_env,c_Lambda_OdB_OAbs(V_t),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) % 0.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_True_0,axiom, % 0.55/0.76 v_n____ = v_i____ ). % 0.55/0.76 % 0.55/0.76 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.55/0.76 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_Var__IT_0,axiom, % 0.55/0.76 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_typing__elims_I1_J_0,axiom, % 0.55/0.76 ( hAPP(V_e,V_i) = V_T % 0.55/0.76 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OVar(V_i),V_T) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_foldr__append_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_Var_I2_J_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_headT_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_argsT_0,axiom, % 0.55/0.76 c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_list__app__typeE_0,axiom, % 0.55/0.76 ( 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.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_Var_I4_J_0,axiom, % 0.55/0.76 c_Type_Otyping(v_ea______,v_ua______,v_T____) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_var__app__typesE_0,axiom, % 0.55/0.76 ( 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.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_nT_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_list__app__typeI_0,axiom, % 0.55/0.76 ( 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.55/0.76 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_dB_Osimps_I10_J_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.55/0.76 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.55/0.76 % 0.55/0.76 cnf(cls_type_Orecs_I2_J_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_type_Osimps_I6_J_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_that_0,axiom, % 0.55/0.76 ( v_thesis____ % 0.55/0.76 | ~ c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,V_T_H_H) % 0.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_typing_OVar_0,axiom, % 0.55/0.76 c_Type_Otyping(V_env,c_Lambda_OdB_OVar(V_x),hAPP(V_env,V_x)) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_type_Osplit__asm_1,axiom, % 0.55/0.76 ( ~ 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.55/0.76 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_xa),V_xb))) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_type_Osplit_1,axiom, % 0.55/0.76 ( ~ 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.55/0.76 | hBOOL(hAPP(V_P,hAPP(hAPP(V_f2,V_type1),V_type2))) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_type_Osimps_I3_J_0,axiom, % 0.55/0.76 c_Type_Otype_OAtom(V_nat) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_list__app__typeD_0,axiom, % 0.55/0.76 ( 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.55/0.76 | ~ 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.55/0.76 % 0.55/0.76 cnf(cls_subst__lemma_0,axiom, % 0.55/0.76 ( ~ c_Type_Otyping(V_e_H,V_u,V_U) % 0.55/0.76 | ~ c_Type_Otyping(c_Type_Oshift(V_e_H,V_i,V_U,tc_Type_Otype),V_t,V_T) % 0.55/0.76 | c_Type_Otyping(V_e_H,c_Lambda_Osubst(V_t,V_u,V_i),V_T) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_typing__elims_I2_J_0,axiom, % 0.55/0.76 ( 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.55/0.76 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.55/0.76 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_CHAINED_0,axiom, % 0.55/0.76 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.55/0.76 % 0.55/0.76 cnf(cls_conjecture_0,negated_conjecture, % 0.55/0.76 ~ v_thesis____ ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.55/0.76 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.55/0.76 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.55/0.76 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.55/0.76 | ~ class_Orderings_Oorder(T_1) ) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.55/0.76 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.55/0.76 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.55/0.76 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.55/0.76 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.55/0.76 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.55/0.76 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.55/0.76 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.55/0.76 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.55/0.76 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Osemigroup__add,axiom, % 0.55/0.76 class_OrderedGroup_Osemigroup__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.55/0.76 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.55/0.76 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.55/0.76 class_Nat_Osemiring__char__0(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.55/0.76 class_Orderings_Opreorder(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.55/0.76 class_Orderings_Olinorder(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.55/0.76 class_Orderings_Oorder(tc_nat) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_bool__Orderings_Opreorder,axiom, % 0.55/0.76 class_Orderings_Opreorder(tc_bool) ). % 0.55/0.76 % 0.55/0.76 cnf(clsarity_bool__Orderings_Oorder,axiom, % 0.55/0.76 class_Orderings_Oorder(tc_bool) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.55/0.76 hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)) ). % 0.55/0.76 % 0.55/0.76 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.55/0.76 ( V_X = V_Y % 0.55/0.76 | ~ hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y)) ) ). % 0.55/0.76 % 0.55/0.76 %------------------------------------------------------------------------------ % 0.55/0.76 %------------------------------------------- % 0.55/0.76 % Proof found % 0.55/0.76 % SZS status Theorem for theBenchmark % 0.55/0.76 % SZS output start Proof % 0.55/0.76 %ClaNum:541(EqnAxiom:163) % 0.55/0.76 %VarNum:2320(SingletonVarNum:996) % 0.55/0.76 %MaxLitNum:6 % 0.55/0.76 %MaxfuncDepth:5 % 0.55/0.76 %SharedTerms:69 % 0.55/0.76 %goalClause: 279 % 0.55/0.76 %singleGoalClaCount:1 % 0.55/0.76 [164]E(a1,a61) % 0.55/0.76 [165]P1(a2) % 0.55/0.76 [166]P2(a2) % 0.55/0.76 [167]P3(a2) % 0.55/0.76 [168]P13(a2) % 0.55/0.76 [169]P14(a2) % 0.55/0.76 [170]P15(a2) % 0.55/0.76 [171]P17(a2) % 0.55/0.76 [172]P4(a2) % 0.55/0.76 [173]P18(a2) % 0.55/0.76 [174]P19(a2) % 0.55/0.76 [175]P24(a2) % 0.55/0.76 [176]P20(a2) % 0.55/0.76 [177]P27(a2) % 0.55/0.76 [178]P21(a2) % 0.55/0.76 [179]P21(a3) % 0.55/0.76 [180]P23(a2) % 0.55/0.76 [181]P23(a3) % 0.55/0.76 [182]P22(a2) % 0.55/0.76 [195]P5(a59,a63,a54) % 0.55/0.76 [196]P5(a60,a65,a54) % 0.55/0.76 [279]~P29(a5000) % 0.55/0.76 [187]P28(f26(a6,a63)) % 0.55/0.76 [188]P28(f26(a6,a65)) % 0.55/0.76 [194]E(f19(a53,a58,a49),a64) % 0.55/0.76 [254]P9(f36(a59,a1,a54,a51),a58,a57) % 0.55/0.76 [270]P5(f36(a59,a1,a54,a51),f21(a10,f9(a61),a64,a49,a49),a55) % 0.55/0.76 [271]P5(f36(a60,a62,a54,a51),f21(a10,f9(a61),a64,a49,a49),a56) % 0.55/0.76 [273]P5(f36(a59,a1,a54,a51),f26(f26(a10,f9(a61)),a53),f22(a46,a57,a55,a51,a51)) % 0.55/0.76 [289]~P7(x2891,x2891,a2) % 0.55/0.76 [293]~P7(x2931,f7(a2),a2) % 0.55/0.76 [184]E(f25(f4(x1841),x1841),f4(x1841)) % 0.55/0.76 [185]E(f23(f4(x1851),x1851),f4(x1851)) % 0.55/0.76 [186]E(f5(f4(x1861),x1861),f4(x1861)) % 0.55/0.76 [189]E(f27(f4(x1891),f48(x1891)),f7(a2)) % 0.55/0.76 [190]P28(f26(a6,f9(x1901))) % 0.55/0.76 [209]E(f33(f34(x2091),x2091,x2091),f34(x2091)) % 0.55/0.76 [299]~P7(f7(a2),f27(f4(x2991),f48(x2991)),a2) % 0.55/0.76 [198]P6(x1981,f4(x1982),x1982) % 0.55/0.76 [215]P5(x2151,f9(x2152),f26(x2151,x2152)) % 0.55/0.76 [281]~E(f9(x2811),f12(x2812)) % 0.55/0.76 [193]E(f23(f23(x1931,x1932),x1932),x1931) % 0.55/0.76 [197]E(f32(f32(x1971,x1972),x1972),f32(x1971,x1972)) % 0.55/0.76 [202]E(f13(x2021,f4(x2022),x2022),x2021) % 0.55/0.76 [203]E(f13(f4(x2031),x2032,x2031),x2032) % 0.55/0.76 [204]E(f14(f9(x2041),x2042,x2041),x2042) % 0.55/0.76 [206]E(f24(f7(a2),x2061,x2062),f4(x2062)) % 0.55/0.76 [207]E(f28(f7(a2),x2071,x2072),f4(x2072)) % 0.55/0.76 [208]E(f28(x2081,f4(x2082),x2082),f4(x2082)) % 0.55/0.76 [210]E(f27(f25(x2101,x2102),f48(x2102)),f27(x2101,f48(x2102))) % 0.55/0.76 [211]E(f27(f23(x2111,x2112),f48(x2112)),f27(x2111,f48(x2112))) % 0.55/0.76 [216]P28(f26(f26(f34(x2161),x2162),x2162)) % 0.55/0.76 [219]E(f20(f19(x2191,f4(x2192),x2192),x2192),x2191) % 0.55/0.76 [220]E(f5(f19(x2201,f4(x2202),x2202),x2202),f4(x2202)) % 0.55/0.76 [221]E(f20(f13(x2211,f4(x2212),x2212),x2212),f20(x2211,x2212)) % 0.55/0.76 [222]E(f5(f13(x2221,f4(x2222),x2222),x2222),f5(x2221,x2222)) % 0.55/0.76 [229]E(f23(f19(x2291,f4(x2292),x2292),x2292),f19(x2291,f4(x2292),x2292)) % 0.55/0.76 [257]P28(f26(f26(a11,f26(f26(a10,f12(x2571)),x2572)),f14(x2571,x2572,f7(a2)))) % 0.55/0.76 [298]~P28(f26(f26(a11,f9(x2981)),x2982)) % 0.55/0.76 [291]~E(f19(x2911,x2912,x2913),x2912) % 0.55/0.76 [296]~E(f19(x2961,x2962,x2963),f4(x2963)) % 0.55/0.76 [300]~P8(x3001,x3002,f4(x3003),x3003) % 0.55/0.76 [301]~P8(x3011,f4(x3012),x3013,x3012) % 0.55/0.76 [214]E(f14(f15(x2141,x2142),x2143,x2142),x2141) % 0.55/0.76 [217]E(f24(f7(a2),x2171,x2172),f24(f7(a2),x2173,x2172)) % 0.55/0.76 [218]E(f27(f24(x2181,x2182,x2183),f48(x2183)),x2181) % 0.55/0.76 [223]E(f33(f33(x2231,x2232,x2233),x2233,x2232),x2231) % 0.55/0.76 [225]E(f23(f24(x2251,x2252,x2253),x2253),f24(x2251,x2252,x2253)) % 0.55/0.76 [230]E(f28(f27(x2301,f48(x2302)),f13(x2301,x2303,x2302),x2302),x2301) % 0.55/0.76 [234]E(f13(f23(x2341,x2342),f23(x2343,x2342),x2342),f23(f13(x2343,x2341,x2342),x2342)) % 0.55/0.76 [282]~E(f12(x2821),f26(f26(a10,x2822),x2823)) % 0.55/0.76 [283]~E(f9(x2831),f26(f26(a10,x2832),x2833)) % 0.55/0.76 [284]~E(f35(x2841),f26(f26(a46,x2842),x2843)) % 0.55/0.76 [285]~E(f26(f26(a10,x2851),x2852),f12(x2853)) % 0.55/0.76 [286]~E(f26(f26(a10,x2861),x2862),f9(x2863)) % 0.55/0.76 [287]~E(f26(f26(a46,x2871),x2872),f35(x2873)) % 0.55/0.76 [227]P28(f26(f26(f32(x2271,x2272),x2273),x2273)) % 0.55/0.76 [231]E(f26(f26(a10,f15(x2311,x2312)),f15(x2313,x2312)),f15(f26(f26(a10,x2311),x2313),x2312)) % 0.55/0.76 [237]E(f13(x2371,f19(x2372,f4(x2373),x2373),x2373),f25(f19(x2372,x2371,x2373),x2373)) % 0.55/0.76 [238]E(f13(f23(x2381,x2382),f19(x2383,f4(x2382),x2382),x2382),f23(f19(x2383,x2381,x2382),x2382)) % 0.55/0.76 [250]E(f13(f24(x2501,x2502,x2503),f19(x2502,f4(x2503),x2503),x2503),f19(x2502,f24(x2501,x2502,x2503),x2503)) % 0.55/0.76 [248]E(f20(f13(x2481,f19(x2482,f4(x2483),x2483),x2483),x2483),x2482) % 0.55/0.76 [249]E(f5(f13(x2491,f19(x2492,f4(x2493),x2493),x2493),x2493),x2491) % 0.55/0.76 [251]E(f23(f13(f23(x2511,x2512),f19(x2513,f4(x2512),x2512),x2512),x2512),f19(x2513,x2511,x2512)) % 0.55/0.76 [235]E(f45(x2351,x2352,f35(x2353),x2354),f26(x2351,x2353)) % 0.55/0.76 [236]E(f47(x2361,x2362,f35(x2363),x2364),f26(x2361,x2363)) % 0.55/0.76 [244]E(f19(x2441,f13(x2442,x2443,x2444),x2444),f13(f19(x2441,x2442,x2444),x2443,x2444)) % 0.55/0.76 [246]E(f13(f13(x2461,x2462,x2463),x2464,x2463),f13(x2461,f13(x2462,x2464,x2463),x2463)) % 0.55/0.76 [253]E(f26(f36(x2531,x2532,x2533,x2534),x2532),x2533) % 0.55/0.76 [255]E(f13(f24(x2551,x2552,x2553),f24(x2554,x2552,x2553),x2553),f13(f24(x2554,x2552,x2553),f24(x2551,x2552,x2553),x2553)) % 0.55/0.76 [258]E(f21(x2581,x2582,f4(x2583),x2584,x2583),x2582) % 0.55/0.76 [259]E(f22(x2591,f4(x2592),x2593,x2592,x2594),x2593) % 0.55/0.76 [303]~E(f21(a10,f9(x3031),x3032,a49,a49),f21(a10,f12(x3033),x3034,a49,a49)) % 0.55/0.76 [252]E(f26(f26(a10,f14(x2521,x2522,x2523)),f14(x2524,x2522,x2523)),f14(f26(f26(a10,x2521),x2524),x2522,x2523)) % 0.55/0.76 [256]E(f19(x2561,f13(f24(x2562,x2561,x2563),x2564,x2563),x2563),f13(f24(x2562,x2561,x2563),f19(x2561,x2564,x2563),x2563)) % 0.55/0.76 [302]~E(f26(f26(a10,f12(x3021)),x3022),f21(a10,f9(x3023),x3024,a49,a49)) % 0.55/0.76 [263]E(f16(x2631,x2632,x2633,f9(x2634),x2635),f26(x2631,x2634)) % 0.55/0.76 [264]E(f17(x2641,x2642,x2643,f12(x2644),x2645),f26(x2643,x2644)) % 0.55/0.76 [265]E(f17(x2651,x2652,x2653,f9(x2654),x2655),f26(x2651,x2654)) % 0.55/0.76 [274]E(f26(f26(x2741,x2742),f16(x2743,x2744,x2741,x2742,x2745)),f16(x2743,x2744,x2741,f12(x2742),x2745)) % 0.55/0.76 [247]E(f45(x2471,x2472,f26(f26(a46,x2473),x2474),x2475),f26(f26(x2472,x2473),x2474)) % 0.55/0.76 [268]E(f26(f26(f26(f26(x2681,x2682),x2683),f47(x2684,x2681,x2682,x2685)),f47(x2684,x2681,x2683,x2685)),f47(x2684,x2681,f26(f26(a46,x2682),x2683),x2685)) % 0.55/0.76 [275]E(f22(x2751,f19(x2752,x2753,x2754),x2755,x2754,x2756),f26(f26(x2751,x2752),f22(x2751,x2753,x2755,x2754,x2756))) % 0.55/0.76 [276]E(f21(x2761,f21(x2761,x2762,x2763,x2764,x2765),x2766,x2764,x2765),f21(x2761,x2762,f13(x2763,x2766,x2765),x2764,x2765)) % 0.55/0.76 [277]E(f22(x2771,x2772,f22(x2771,x2773,x2774,x2775,x2776),x2775,x2776),f22(x2771,f13(x2772,x2773,x2775),x2774,x2775,x2776)) % 0.55/0.76 [267]E(f17(x2671,x2672,x2673,f26(f26(a10,x2674),x2675),x2676),f26(f26(x2672,x2674),x2675)) % 0.55/0.76 [269]E(f21(x2691,x2692,f19(x2693,x2694,x2695),x2696,x2695),f21(x2691,f26(f26(x2691,x2692),x2693),x2694,x2696,x2695)) % 0.55/0.76 [278]E(f26(f26(f26(f26(x2781,x2782),x2783),f16(x2784,x2781,x2785,x2782,x2786)),f16(x2784,x2781,x2785,x2783,x2786)),f16(x2784,x2781,x2785,f26(f26(a10,x2782),x2783),x2786)) % 0.55/0.76 [316]E(x3161,f7(a2))+P7(f7(a2),x3161,a2) % 0.55/0.76 [390]P11(f33(a11,a49,a49),x3901,a49)+~P28(f26(a6,x3901)) % 0.55/0.76 [402]~P11(f33(a11,a49,a49),x4021,a49)+P28(f26(a6,x4021)) % 0.55/0.76 [307]~P27(x3071)+E(f31(f7(a2),x3071),f7(x3071)) % 0.55/0.76 [325]~P16(x3251)+E(f26(f26(f8(x3251),f7(x3251)),f7(x3251)),f7(x3251)) % 0.55/0.76 [326]~P28(f26(a6,x3261))+P28(f26(a6,f12(x3261))) % 0.55/0.76 [331]~P7(x3312,x3312,x3311)+~P21(x3311) % 0.55/0.76 [332]~P7(x3322,x3322,x3321)+~P23(x3321) % 0.55/0.76 [333]~P7(x3332,x3332,x3331)+~P22(x3331) % 0.55/0.76 [304]E(x3041,x3042)+~E(f12(x3041),f12(x3042)) % 0.55/0.76 [305]E(x3051,x3052)+~E(f9(x3051),f9(x3052)) % 0.55/0.76 [306]E(x3061,x3062)+~E(f35(x3061),f35(x3062)) % 0.55/0.76 [309]~E(f25(x3091,x3092),f4(x3092))+E(x3091,f4(x3092)) % 0.55/0.76 [310]~E(f23(x3101,x3102),f4(x3102))+E(x3101,f4(x3102)) % 0.55/0.76 [311]~P21(x3112)+P21(f52(x3111,x3112)) % 0.55/0.76 [312]~P23(x3122)+P23(f52(x3121,x3122)) % 0.55/0.76 [369]~P24(x3691)+~P7(f31(x3692,x3691),f7(x3691),x3691) % 0.55/0.76 [313]E(x3131,f4(x3132))+~E(f27(x3131,f48(x3132)),f7(a2)) % 0.55/0.76 [317]~P1(x3171)+E(f26(f26(f8(x3171),x3172),f7(x3171)),x3172) % 0.55/0.76 [318]~P2(x3181)+E(f26(f26(f8(x3181),x3182),f7(x3181)),x3182) % 0.55/0.76 [319]~P15(x3191)+E(f26(f26(f8(x3191),x3192),f7(x3191)),x3192) % 0.55/0.76 [340]P28(f26(x3401,x3402))+~P28(f26(x3401,f37(x3401))) % 0.55/0.76 [341]E(x3411,f4(x3412))+P7(f7(a2),f27(x3411,f48(x3412)),a2) % 0.55/0.76 [345]~P7(x3451,x3452,a2)+E(f15(f9(x3451),x3452),f9(x3451)) % 0.55/0.76 [363]~P28(f26(a6,x3631))+P28(f26(a6,f15(x3631,x3632))) % 0.55/0.76 [396]~P28(f26(f26(a11,x3961),x3962))+P28(f26(f26(a11,f12(x3961)),f12(x3962))) % 0.55/0.76 [500]~P15(x5001)+E(f22(f8(x5001),x5002,f7(x5001),x5001,x5001),f21(f8(x5001),f7(x5001),x5002,x5001,x5001)) % 0.55/0.76 [321]~P1(x3211)+E(f26(f26(f8(x3211),f7(x3211)),x3212),x3212) % 0.55/0.76 [322]~P2(x3221)+E(f26(f26(f8(x3221),f7(x3221)),x3222),x3222) % 0.55/0.76 [323]~P15(x3231)+E(f26(f26(f8(x3231),f7(x3231)),x3232),x3232) % 0.55/0.76 [399]~P28(f26(a6,x3991))+P28(f26(a6,f26(f26(a10,x3991),f9(x3992)))) % 0.55/0.76 [400]E(x4001,f4(x4002))+E(f13(f5(x4001,x4002),f19(f20(x4001,x4002),f4(x4002),x4002),x4002),x4001) % 0.55/0.76 [440]P28(f26(f26(f32(a11,a49),f12(x4401)),f12(x4402)))+~P28(f26(f26(f32(a11,a49),x4401),x4402)) % 0.55/0.76 [520]~P6(a6,x5202,a49)+P28(f26(a6,f21(a10,f9(x5201),x5202,a49,a49))) % 0.55/0.76 [314]E(x3141,x3142)+~E(f23(x3141,x3143),f23(x3142,x3143)) % 0.55/0.76 [329]~E(f13(x3293,x3291,x3292),x3293)+E(x3291,f4(x3292)) % 0.55/0.76 [330]~E(f13(x3301,x3303,x3302),x3303)+E(x3301,f4(x3302)) % 0.55/0.76 [335]~E(f24(x3351,x3352,x3353),f4(x3353))+E(x3351,f7(a2)) % 0.55/0.76 [338]~E(f13(x3383,x3381,x3382),f4(x3382))+E(x3381,f4(x3382)) % 0.55/0.76 [339]~E(f13(x3391,x3393,x3392),f4(x3392))+E(x3391,f4(x3392)) % 0.55/0.76 [348]~P5(x3481,f9(x3482),x3483)+E(f26(x3481,x3482),x3483) % 0.55/0.76 [489]~E(f12(x4892),f21(a10,x4893,x4891,a49,a49))+E(x4891,f4(a49)) % 0.55/0.76 [490]~E(f9(x4902),f21(a10,x4903,x4901,a49,a49))+E(x4901,f4(a49)) % 0.55/0.76 [491]~E(f21(a10,x4912,x4911,a49,a49),f12(x4913))+E(x4911,f4(a49)) % 0.55/0.76 [492]E(x4921,f12(x4922))+~E(f21(a10,x4921,x4923,a49,a49),f12(x4922)) % 0.55/0.76 [493]E(f12(x4931),x4932)+~E(f12(x4931),f21(a10,x4932,x4933,a49,a49)) % 0.55/0.76 [494]E(f9(x4941),x4942)+~E(f9(x4941),f21(a10,x4942,x4943,a49,a49)) % 0.55/0.76 [511]E(x5111,x5112)+~E(f21(a10,x5111,x5113,a49,a49),f21(a10,x5112,x5113,a49,a49)) % 0.55/0.76 [366]E(x3661,f7(a2))+E(f20(f24(x3661,x3662,x3663),x3663),x3662) % 0.55/0.76 [367]E(x3671,f4(x3672))+E(f20(f19(x3673,x3671,x3672),x3672),f20(x3671,x3672)) % 0.55/0.76 [368]E(x3681,f4(x3682))+E(f20(f13(x3683,x3681,x3682),x3682),f20(x3681,x3682)) % 0.55/0.76 [370]~P7(x3701,x3703,a2)+E(f14(f9(x3701),x3702,x3703),f9(x3701)) % 0.55/0.76 [381]~E(f23(x3811,x3813),f19(x3812,f4(x3813),x3813))+E(x3811,f19(x3812,f4(x3813),x3813)) % 0.55/0.76 [382]~E(f19(x3822,f4(x3823),x3823),f23(x3821,x3823))+E(x3821,f19(x3822,f4(x3823),x3823)) % 0.55/0.76 [393]E(x3931,f4(x3932))+E(f19(x3933,f5(x3931,x3932),x3932),f5(f19(x3933,x3931,x3932),x3932)) % 0.55/0.76 [394]E(x3941,f4(x3942))+E(f13(x3943,f5(x3941,x3942),x3942),f5(f13(x3943,x3941,x3942),x3942)) % 0.55/0.76 [408]~P7(x4081,f27(x4082,f48(x4083)),a2)+E(f28(x4081,f5(x4082,x4083),x4083),f28(x4081,x4082,x4083)) % 0.55/0.76 [422]~P28(f26(f26(a11,x4221),x4223))+P28(f26(f26(a11,f15(x4221,x4222)),f15(x4223,x4222))) % 0.55/0.76 [441]~P5(x4412,f12(x4413),x4411)+E(f26(f26(a46,f40(x4411,x4412,x4413)),f42(x4411,x4412,x4413)),x4411) % 0.55/0.76 [471]~P5(x4711,f12(x4713),x4712)+P5(f36(x4711,f7(a2),f40(x4712,x4711,x4713),a51),x4713,f42(x4712,x4711,x4713)) % 0.55/0.76 [495]E(f26(f26(a10,x4951),x4952),x4953)+~E(f26(f26(a10,x4951),x4952),f21(a10,x4953,f4(a49),a49,a49)) % 0.55/0.76 [499]~P3(x4991)+E(f22(f8(x4991),x4992,x4993,x4991,x4991),f21(f8(x4991),x4993,x4992,x4991,x4991)) % 0.55/0.76 [535]~P28(f26(f26(a11,x5351),x5353))+P28(f26(f26(a11,f21(a10,x5351,x5352,a49,a49)),f21(a10,x5353,x5352,a49,a49))) % 0.55/0.76 [537]~P8(a11,x5372,x5373,a49)+P28(f26(f26(a11,f21(a10,x5371,x5372,a49,a49)),f21(a10,x5371,x5373,a49,a49))) % 0.55/0.76 [350]~P1(x3501)+E(f26(f26(f8(x3501),x3502),x3503),f26(f26(f8(x3501),x3503),x3502)) % 0.55/0.76 [351]~P2(x3511)+E(f26(f26(f8(x3511),x3512),x3513),f26(f26(f8(x3511),x3513),x3512)) % 0.55/0.76 [371]E(x3711,x3712)+~P28(f26(f26(f34(x3713),x3711),x3712)) % 0.55/0.76 [410]~P28(f26(a6,x4101))+P28(f26(a6,f14(x4101,f9(x4102),x4103))) % 0.55/0.76 [447]P28(f26(f26(f32(a11,a49),f15(x4471,x4472)),f15(x4473,x4472)))+~P28(f26(f26(f32(a11,a49),x4471),x4473)) % 0.55/0.76 [452]~P28(f26(f26(a11,x4521),x4523))+P28(f26(f26(a11,f26(f26(a10,x4521),x4522)),f26(f26(a10,x4523),x4522))) % 0.55/0.76 [453]~P28(f26(f26(a11,x4532),x4533))+P28(f26(f26(a11,f26(f26(a10,x4531),x4532)),f26(f26(a10,x4531),x4533))) % 0.55/0.76 [463]~P28(f26(f26(f32(a11,a49),x4631),x4633))+P28(f26(f26(f32(a11,a49),f26(f26(a10,x4631),x4632)),f26(f26(a10,x4633),x4632))) % 0.55/0.76 [464]~P28(f26(f26(f32(a11,a49),x4642),x4643))+P28(f26(f26(f32(a11,a49),f26(f26(a10,x4641),x4642)),f26(f26(a10,x4641),x4643))) % 0.55/0.76 [509]~P15(x5091)+E(f26(f26(f8(x5091),x5092),f22(f8(x5091),x5093,f7(x5091),x5091,x5091)),f21(f8(x5091),x5092,x5093,x5091,x5091)) % 0.55/0.76 [510]~P15(x5101)+E(f26(f26(f8(x5101),x5102),f21(f8(x5101),f7(x5101),x5103,x5101,x5101)),f21(f8(x5101),x5102,x5103,x5101,x5101)) % 0.55/0.76 [536]P28(f26(f26(f32(a11,a49),f21(a10,x5361,x5362,a49,a49)),f21(a10,x5363,x5362,a49,a49)))+~P28(f26(f26(f32(a11,a49),x5361),x5363)) % 0.55/0.76 [538]P8(a11,x5381,f18(x5382,x5381,x5383),a49)+~P28(f26(f26(a11,f21(a10,f9(x5382),x5381,a49,a49)),x5383)) % 0.55/0.76 [540]E(f21(a10,f9(x5401),f18(x5401,x5402,x5403),a49,a49),x5403)+~P28(f26(f26(a11,f21(a10,f9(x5401),x5402,a49,a49)),x5403)) % 0.55/0.76 [373]E(x3731,x3732)+~E(f13(x3733,x3731,x3734),f13(x3733,x3732,x3734)) % 0.55/0.76 [376]E(x3761,x3762)+~E(f13(x3761,x3763,x3764),f13(x3762,x3763,x3764)) % 0.55/0.76 [411]P6(x4111,x4112,x4113)+~P6(x4111,f13(x4114,x4112,x4113),x4113) % 0.55/0.76 [412]P6(x4121,x4122,x4123)+~P6(x4121,f13(x4122,x4124,x4123),x4123) % 0.55/0.76 [517]P9(x5171,x5172,f38(x5173,x5171,x5174,x5172))+~P5(x5171,f21(a10,x5174,x5172,a49,a49),x5173) % 0.55/0.76 [518]P9(x5181,x5182,f39(x5183,x5181,x5184,x5182))+~P5(x5181,f21(a10,x5184,x5182,a49,a49),x5183) % 0.55/0.76 [353]E(x3531,x3532)+~E(f26(f26(a10,x3533),x3531),f26(f26(a10,x3534),x3532)) % 0.55/0.76 [354]E(x3541,x3542)+~E(f26(f26(a46,x3543),x3541),f26(f26(a46,x3544),x3542)) % 0.55/0.76 [355]E(x3551,x3552)+~E(f26(f26(a10,x3551),x3553),f26(f26(a10,x3552),x3554)) % 0.55/0.76 [356]E(x3561,x3562)+~E(f26(f26(a46,x3561),x3563),f26(f26(a46,x3562),x3564)) % 0.55/0.76 [459]P5(x4591,x4592,f41(x4593,x4591,x4594,x4592))+~P5(x4591,f26(f26(a10,x4594),x4592),x4593) % 0.55/0.76 [462]~P28(f26(f26(a11,x4621),x4624))+P28(f26(f26(a11,f14(x4621,x4622,x4623)),f14(x4624,x4622,x4623))) % 0.55/0.76 [470]P28(f26(f26(f32(a11,a49),f14(x4701,x4702,x4703)),f14(x4701,x4704,x4703)))+~P28(f26(f26(a11,x4702),x4704)) % 0.55/0.76 [473]P5(x4731,f12(x4732),f26(f26(a46,x4733),x4734))+~P5(f36(x4731,f7(a2),x4733,a51),x4732,x4734) % 0.55/0.76 [513]E(x5131,x5132)+~E(f21(a10,f12(x5133),x5131,a49,a49),f21(a10,f12(x5134),x5132,a49,a49)) % 0.55/0.76 [514]E(x5141,x5142)+~E(f21(a10,f9(x5143),x5141,a49,a49),f21(a10,f9(x5144),x5142,a49,a49)) % 0.55/0.76 [515]E(x5151,x5152)+~E(f21(a10,f12(x5151),x5153,a49,a49),f21(a10,f12(x5152),x5154,a49,a49)) % 0.55/0.76 [516]E(x5161,x5162)+~E(f21(a10,f9(x5161),x5163,a49,a49),f21(a10,f9(x5162),x5164,a49,a49)) % 0.55/0.76 [519]P9(x5191,x5192,f43(x5193,x5191,x5194,x5192))+~P5(x5191,f21(a10,f9(x5194),x5192,a49,a49),x5193) % 0.55/0.76 [522]~P5(x5221,f21(a10,x5222,x5224,a49,a49),x5223)+P5(x5221,x5222,f22(a46,f38(x5223,x5221,x5222,x5224),x5223,a51,a51)) % 0.55/0.76 [523]~P5(x5231,f21(a10,x5232,x5234,a49,a49),x5233)+P5(x5231,x5232,f22(a46,f39(x5233,x5231,x5232,x5234),x5233,a51,a51)) % 0.55/0.76 [524]~P5(x5241,f21(a10,f9(x5242),x5244,a49,a49),x5243)+P5(x5241,f9(x5242),f22(a46,f43(x5243,x5241,x5242,x5244),x5243,a51,a51)) % 0.55/0.76 [409]~E(f23(x4091,x4093),f19(x4094,x4092,x4093))+E(x4091,f13(f23(x4092,x4093),f19(x4094,f4(x4093),x4093),x4093)) % 0.55/0.76 [413]~P28(f26(f26(x4131,x4133),x4134))+P28(f26(f26(f32(x4131,x4132),x4133),x4134)) % 0.55/0.76 [475]P28(f26(f26(f32(a11,a49),f14(x4751,x4752,x4753)),f14(x4754,x4752,x4753)))+~P28(f26(f26(f32(a11,a49),x4751),x4754)) % 0.55/0.76 [476]P28(f26(f26(f32(a11,a49),f14(x4761,x4762,x4763)),f14(x4761,x4764,x4763)))+~P28(f26(f26(f32(a11,a49),x4762),x4764)) % 0.55/0.76 [485]P28(f26(x4851,f26(x4852,x4853)))+~P28(f26(x4851,f45(x4852,x4854,f35(x4853),a50))) % 0.55/0.76 [498]~P5(x4981,f26(f26(a10,x4982),x4984),x4983)+P5(x4981,x4982,f26(f26(a46,f41(x4983,x4981,x4982,x4984)),x4983)) % 0.55/0.76 [414]~P1(x4141)+E(f26(f26(f8(x4141),x4142),f26(f26(f8(x4141),x4143),x4144)),f26(f26(f8(x4141),x4143),f26(f26(f8(x4141),x4142),x4144))) % 0.55/0.76 [415]~P12(x4151)+E(f26(f26(f8(x4151),x4152),f26(f26(f8(x4151),x4153),x4154)),f26(f26(f8(x4151),x4153),f26(f26(f8(x4151),x4152),x4154))) % 0.55/0.76 [416]~P2(x4161)+E(f26(f26(f8(x4161),x4162),f26(f26(f8(x4161),x4163),x4164)),f26(f26(f8(x4161),x4163),f26(f26(f8(x4161),x4162),x4164))) % 0.55/0.76 [481]~P28(f26(f26(f32(x4811,x4812),x4814),x4813))+P28(f26(f26(f32(f33(x4811,x4812,x4812),x4812),x4813),x4814)) % 0.55/0.76 [488]P28(f26(f26(f32(x4881,x4882),x4883),x4884))+~P28(f26(f26(f32(f33(x4881,x4882,x4882),x4882),x4884),x4883)) % 0.55/0.76 [512]~P17(x5121)+E(f21(f8(x5121),f26(f26(f8(x5121),x5122),x5123),x5124,x5121,x5121),f26(f26(f8(x5121),x5122),f21(f8(x5121),x5123,x5124,x5121,x5121))) % 0.55/0.76 [434]~P1(x4341)+E(f26(f26(f8(x4341),f26(f26(f8(x4341),x4342),x4343)),x4344),f26(f26(f8(x4341),x4342),f26(f26(f8(x4341),x4343),x4344))) % 0.55/0.76 [435]~P2(x4351)+E(f26(f26(f8(x4351),f26(f26(f8(x4351),x4352),x4353)),x4354),f26(f26(f8(x4351),x4352),f26(f26(f8(x4351),x4353),x4354))) % 0.55/0.76 [436]~P3(x4361)+E(f26(f26(f8(x4361),f26(f26(f8(x4361),x4362),x4363)),x4364),f26(f26(f8(x4361),x4362),f26(f26(f8(x4361),x4363),x4364))) % 0.55/0.76 [444]~P1(x4441)+E(f26(f26(f8(x4441),f26(f26(f8(x4441),x4442),x4443)),x4444),f26(f26(f8(x4441),f26(f26(f8(x4441),x4442),x4444)),x4443)) % 0.55/0.76 [372]E(x3721,x3722)+~E(f19(x3723,x3721,x3724),f19(x3725,x3722,x3724)) % 0.55/0.76 [374]E(x3741,x3742)+~E(f24(x3741,x3743,x3744),f24(x3742,x3745,x3744)) % 0.55/0.76 [375]E(x3751,x3752)+~E(f19(x3751,x3753,x3754),f19(x3752,x3755,x3754)) % 0.55/0.76 [456]~P5(x4561,x4564,x4565)+P5(f36(x4561,x4562,x4563,a51),f15(x4564,x4562),x4565) % 0.55/0.76 [465]~P8(x4651,x4653,x4655,x4654)+P8(x4651,f19(x4652,x4653,x4654),f19(x4652,x4655,x4654),x4654) % 0.55/0.76 [466]~P8(x4661,x4662,x4665,x4664)+P8(x4661,f13(x4662,x4663,x4664),f13(x4665,x4663,x4664),x4664) % 0.55/0.76 [467]~P8(x4671,x4673,x4675,x4674)+P8(x4671,f13(x4672,x4673,x4674),f13(x4672,x4675,x4674),x4674) % 0.55/0.76 [448]P8(x4481,f19(x4482,x4483,x4484),f19(x4485,x4483,x4484),x4484)+~P28(f26(f26(x4481,x4482),x4485)) % 0.55/0.76 [449]~P7(x4495,x4492,a2)+E(f26(f36(x4491,x4492,x4493,x4494),x4495),f26(x4491,x4495)) % 0.55/0.76 [445]E(x4451,x4452)+~E(f13(x4453,f19(x4451,f4(x4454),x4454),x4454),f13(x4455,f19(x4452,f4(x4454),x4454),x4454)) % 0.55/0.76 [446]E(x4461,x4462)+~E(f13(x4461,f19(x4463,f4(x4464),x4464),x4464),f13(x4462,f19(x4465,f4(x4464),x4464),x4464)) % 0.55/0.76 [455]~P28(f26(f26(x4551,x4555),x4554))+P28(f26(f26(f33(x4551,x4552,x4553),x4554),x4555)) % 0.55/0.76 [469]P28(f26(f26(x4691,x4692),x4693))+~P28(f26(f26(f33(x4691,x4694,x4695),x4693),x4692)) % 0.55/0.76 [527]P28(f26(x5271,f26(x5272,x5273)))+~P28(f26(x5271,f17(x5274,x5275,x5272,f12(x5273),a50))) % 0.55/0.76 [529]P28(f26(x5291,f26(x5292,x5293)))+~P28(f26(x5291,f17(x5292,x5294,x5295,f9(x5293),a50))) % 0.55/0.76 [457]~P1(x4571)+E(f26(f26(f8(x4571),f26(f26(f8(x4571),x4572),x4573)),f26(f26(f8(x4571),x4574),x4575)),f26(f26(f8(x4571),f26(f26(f8(x4571),x4572),x4574)),f26(f26(f8(x4571),x4573),x4575))) % 0.55/0.76 [497]P28(f26(x4971,f26(f26(x4972,x4973),x4974)))+~P28(f26(x4971,f45(x4975,x4972,f26(f26(a46,x4973),x4974),a50))) % 0.55/0.76 [532]P28(f26(x5321,f26(f26(x5322,x5323),x5324)))+~P28(f26(x5321,f17(x5325,x5322,x5326,f26(f26(a10,x5323),x5324),a50))) % 0.55/0.76 [533]~P5(f36(a59,a1,a54,a51),a53,x5331)+~P5(f36(a59,a1,a54,a51),f9(a61),f26(f26(a46,x5331),f22(a46,a57,a55,a51,a51)))+P29(a5000) % 0.55/0.76 [347]E(x3471,x3472)+P7(x3472,x3471,a2)+P7(x3471,x3472,a2) % 0.55/0.76 [388]~P24(x3881)+P7(f7(x3881),f31(x3882,x3881),x3881)+~P7(f7(a2),x3882,a2) % 0.55/0.76 [392]~P24(x3922)+~P7(f7(x3922),f31(x3921,x3922),x3922)+P7(f7(a2),x3921,a2) % 0.55/0.76 [324]~P25(x3241)+~P10(x3241)+E(f26(f26(f8(x3241),x3242),f7(x3241)),x3242) % 0.55/0.76 [342]~P16(x3422)+E(x3421,f7(x3422))+~E(f26(f26(f8(x3422),x3421),x3421),f7(x3422)) % 0.55/0.76 [403]~P16(x4031)+~P7(f7(x4031),x4032,x4031)+P7(f7(x4031),f26(f26(f8(x4031),x4032),x4032),x4031) % 0.55/0.76 [404]~P16(x4041)+~P7(x4042,f7(x4041),x4041)+P7(f26(f26(f8(x4041),x4042),x4042),f7(x4041),x4041) % 0.55/0.76 [405]~P26(x4051)+~P7(x4052,f7(x4051),x4051)+P7(f26(f26(f8(x4051),x4052),x4052),f7(x4051),x4051) % 0.55/0.76 [417]~P16(x4172)+P7(x4171,f7(x4172),x4172)+~P7(f26(f26(f8(x4172),x4171),x4171),f7(x4172),x4172) % 0.55/0.76 [418]~P26(x4182)+P7(x4181,f7(x4182),x4182)+~P7(f26(f26(f8(x4182),x4181),x4181),f7(x4182),x4182) % 0.55/0.76 [419]~P16(x4191)+P7(f7(x4191),x4192,x4191)+~P7(f7(x4191),f26(f26(f8(x4191),x4192),x4192),x4191) % 0.55/0.76 [383]~P7(x3833,x3832,x3831)+~P21(x3831)+~P7(x3832,x3833,x3831) % 0.55/0.76 [385]~P7(x3853,x3852,x3851)+~P23(x3851)+~P7(x3852,x3853,x3851) % 0.55/0.76 [386]~P7(x3863,x3862,x3861)+~P22(x3861)+~P7(x3862,x3863,x3861) % 0.55/0.76 [315]~P4(x3153)+E(x3151,x3152)+~E(f31(x3151,x3153),f31(x3152,x3153)) % 0.55/0.76 [343]~E(f28(x3433,x3431,x3432),f4(x3432))+E(x3431,f4(x3432))+E(x3433,f7(a2)) % 0.55/0.76 [391]~P24(x3912)+~P7(x3911,x3913,a2)+P7(f31(x3911,x3912),f31(x3913,x3912),x3912) % 0.55/0.76 [395]~P24(x3953)+~P7(f31(x3951,x3953),f31(x3952,x3953),x3953)+P7(x3951,x3952,a2) % 0.55/0.76 [362]E(x3621,x3622)+P7(x3622,x3621,a2)+E(f14(f9(x3621),x3623,x3622),f9(x3621)) % 0.55/0.76 [525]~P11(f33(a11,a49,a49),x5252,a49)+~P11(f33(a11,a49,a49),f21(a10,f14(x5251,x5252,f7(a2)),x5253,a49,a49),a49)+P11(f33(a11,a49,a49),f21(a10,f26(f26(a10,f12(x5251)),x5252),x5253,a49,a49),a49) % 0.55/0.76 [534]~P28(f26(a6,x5342))+~P28(f26(a6,f21(a10,f14(x5341,x5342,f7(a2)),x5343,a49,a49)))+P28(f26(a6,f21(a10,f26(f26(a10,f12(x5341)),x5342),x5343,a49,a49))) % 0.55/0.76 [420]~P6(x4201,x4203,x4204)+~P6(x4201,x4202,x4204)+P6(x4201,f13(x4202,x4203,x4204),x4204) % 0.55/0.76 [364]P28(f26(x3641,x3642))+P28(f26(x3641,x3643))+~E(f37(x3641),f26(f26(a46,x3644),x3643)) % 0.55/0.76 [365]P28(f26(x3651,x3652))+P28(f26(x3651,x3653))+~E(f37(x3651),f26(f26(a46,x3653),x3654)) % 0.55/0.76 [401]P5(x4011,x4012,x4013)+~P5(x4011,x4014,x4013)+~P28(f26(f26(a11,x4014),x4012)) % 0.55/0.76 [407]P11(x4071,x4072,x4073)+~P11(x4071,x4074,x4073)+~P28(f26(f26(x4071,x4072),x4074)) % 0.55/0.76 [377]~P13(x3773)+E(x3771,x3772)+~E(f26(f26(f8(x3773),x3774),x3771),f26(f26(f8(x3773),x3774),x3772)) % 0.55/0.76 [378]~P14(x3783)+E(x3781,x3782)+~E(f26(f26(f8(x3783),x3784),x3781),f26(f26(f8(x3783),x3784),x3782)) % 0.55/0.76 [379]~P14(x3793)+E(x3791,x3792)+~E(f26(f26(f8(x3793),x3791),x3794),f26(f26(f8(x3793),x3792),x3794)) % 0.55/0.76 [423]~P18(x4231)+~P7(x4232,x4234,x4231)+P7(f26(f26(f8(x4231),x4232),x4233),f26(f26(f8(x4231),x4234),x4233),x4231) % 0.55/0.76 [424]~P19(x4241)+~P7(x4242,x4244,x4241)+P7(f26(f26(f8(x4241),x4242),x4243),f26(f26(f8(x4241),x4244),x4243),x4241) % 0.55/0.76 [425]~P18(x4251)+~P7(x4253,x4254,x4251)+P7(f26(f26(f8(x4251),x4252),x4253),f26(f26(f8(x4251),x4252),x4254),x4251) % 0.55/0.76 [426]~P19(x4261)+~P7(x4263,x4264,x4261)+P7(f26(f26(f8(x4261),x4262),x4263),f26(f26(f8(x4261),x4262),x4264),x4261) % 0.55/0.76 [430]P5(x4301,x4302,x4303)+~P5(x4301,x4304,x4303)+~P28(f26(f26(f32(a11,a49),x4304),x4302)) % 0.55/0.76 [438]P11(x4381,x4382,x4383)+~P11(x4381,x4384,x4383)+~P28(f26(f26(f32(x4381,x4383),x4382),x4384)) % 0.55/0.76 [442]~P19(x4423)+P7(x4421,x4422,x4423)+~P7(f26(f26(f8(x4423),x4424),x4421),f26(f26(f8(x4423),x4424),x4422),x4423) % 0.55/0.76 [443]~P19(x4433)+P7(x4431,x4432,x4433)+~P7(f26(f26(f8(x4433),x4431),x4434),f26(f26(f8(x4433),x4432),x4434),x4433) % 0.55/0.76 [477]~P28(f26(f26(f32(a11,a49),x4771),x4773))+~P28(f26(f26(f32(a11,a49),x4772),x4774))+P28(f26(f26(f32(a11,a49),f26(f26(a10,x4771),x4772)),f26(f26(a10,x4773),x4774))) % 0.55/0.76 [380]E(x3801,x3802)+~E(f24(x3803,x3801,x3804),f24(x3805,x3802,x3804))+E(x3803,f7(a2)) % 0.55/0.76 [521]~P9(x5211,x5213,x5215)+~P5(x5211,x5212,f22(a46,x5215,x5214,a51,a51))+P5(x5211,f21(a10,x5212,x5213,a49,a49),x5214) % 0.55/0.76 [431]~P5(x4311,x4313,x4315)+~P5(x4311,x4312,f26(f26(a46,x4315),x4314))+P5(x4311,f26(f26(a10,x4312),x4313),x4314) % 0.55/0.76 [501]~E(f13(x5011,x5015,x5012),f19(x5013,x5014,x5012))+E(x5011,f4(x5012))+E(f19(x5013,f29(x5013,x5014,x5011,x5015,x5012),x5012),x5011) % 0.55/0.76 [502]~E(f13(x5021,x5025,x5022),f19(x5023,x5024,x5022))+E(x5021,f4(x5022))+E(f13(f30(x5023,x5024,x5021,x5025,x5022),x5025,x5022),x5024) % 0.55/0.76 [503]~E(f13(x5031,x5035,x5032),f19(x5033,x5034,x5032))+E(x5031,f4(x5032))+E(f19(x5033,f30(x5033,x5034,x5031,x5035,x5032),x5032),x5031) % 0.55/0.76 [504]~E(f13(x5041,x5045,x5042),f19(x5043,x5044,x5042))+E(x5041,f4(x5042))+E(f13(f29(x5043,x5044,x5041,x5045,x5042),x5045,x5042),x5044) % 0.55/0.76 [505]~E(f13(x5055,x5051,x5054),f19(x5052,x5053,x5054))+E(x5051,f19(x5052,x5053,x5054))+E(f19(x5052,f29(x5052,x5053,x5055,x5051,x5054),x5054),x5055) % 0.55/0.76 [506]~E(f13(x5065,x5061,x5064),f19(x5062,x5063,x5064))+E(x5061,f19(x5062,x5063,x5064))+E(f13(f29(x5062,x5063,x5065,x5061,x5064),x5061,x5064),x5063) % 0.55/0.76 [507]~E(f13(x5075,x5074,x5073),f19(x5071,x5072,x5073))+E(f19(x5071,x5072,x5073),x5074)+E(f13(f30(x5071,x5072,x5075,x5074,x5073),x5074,x5073),x5072) % 0.55/0.76 [508]~E(f13(x5085,x5084,x5083),f19(x5081,x5082,x5083))+E(f19(x5081,x5082,x5083),x5084)+E(f19(x5081,f30(x5081,x5082,x5085,x5084,x5083),x5083),x5085) % 0.55/0.76 [530]E(x5301,x5302)+~P5(x5303,f21(a10,f9(x5304),x5305,a49,a49),x5301)+~P5(x5303,f21(a10,f9(x5304),x5305,a49,a49),x5302) % 0.55/0.76 [450]~P28(f26(f26(x4501,x4505),x4504))+~P28(f26(f26(f32(x4501,x4502),x4503),x4505))+P28(f26(f26(f32(x4501,x4502),x4503),x4504)) % 0.55/0.76 [451]~P28(f26(f26(x4511,x4513),x4515))+~P28(f26(f26(f32(x4511,x4512),x4515),x4514))+P28(f26(f26(f32(x4511,x4512),x4513),x4514)) % 0.55/0.76 [460]~P28(f26(f26(f32(x4601,x4602),x4603),x4605))+P28(f26(f26(f32(x4601,x4602),x4603),x4604))+~P28(f26(f26(f32(x4601,x4602),x4605),x4604)) % 0.55/0.76 [429]~P12(x4291)+E(f26(f26(f8(x4291),x4292),x4293),x4294)+~E(f26(f26(f8(x4291),x4292),f26(f26(f8(x4291),x4295),x4293)),f26(f26(f8(x4291),x4295),x4294)) % 0.55/0.76 [458]E(x4581,x4582)+E(x4583,x4584)+~P8(x4585,f19(x4584,x4582,x4586),f19(x4583,x4581,x4586),x4586) % 0.55/0.76 [472]E(x4721,x4722)+P8(x4723,x4721,x4722,x4724)+~P8(x4723,f19(x4725,x4721,x4724),f19(x4726,x4722,x4724),x4724) % 0.55/0.76 [478]~P5(x4781,x4783,x4786)+P5(x4781,f14(x4782,x4783,x4784),x4785)+~P5(f36(x4781,x4784,x4786,a51),x4782,x4785) % 0.55/0.76 [461]E(x4611,x4612)+~P8(x4613,f19(x4612,x4614,x4615),f19(x4611,x4616,x4615),x4615)+P28(f26(f26(x4613,x4612),x4611)) % 0.55/0.76 [474]P8(x4741,x4742,x4743,x4744)+~P8(x4741,f19(x4745,x4742,x4744),f19(x4746,x4743,x4744),x4744)+P28(f26(f26(x4741,x4745),x4746)) % 0.55/0.76 [482]E(x4821,x4822)+E(x4823,x4824)+~P8(x4825,f13(x4823,f19(x4821,f4(x4826),x4826),x4826),f13(x4824,f19(x4822,f4(x4826),x4826),x4826),x4826) % 0.55/0.76 [483]E(x4831,x4832)+~P8(x4833,f13(x4834,f19(x4831,f4(x4835),x4835),x4835),f13(x4836,f19(x4832,f4(x4835),x4835),x4835),x4835)+P28(f26(f26(x4833,x4831),x4832)) % 0.55/0.76 [486]E(x4861,x4862)+P8(x4863,x4861,x4862,x4864)+~P8(x4863,f13(x4861,f19(x4865,f4(x4864),x4864),x4864),f13(x4862,f19(x4866,f4(x4864),x4864),x4864),x4864) % 0.55/0.76 [487]P8(x4871,x4872,x4873,x4874)+~P8(x4871,f13(x4872,f19(x4875,f4(x4874),x4874),x4874),f13(x4873,f19(x4876,f4(x4874),x4874),x4874),x4874)+P28(f26(f26(x4871,x4875),x4876)) % 0.55/0.76 [357]P7(x3571,x3572,x3573)+~P26(x3573)+E(x3571,x3572)+P7(x3572,x3571,x3573) % 0.55/0.76 [361]P7(x3611,x3612,x3613)+~P22(x3613)+E(x3611,x3612)+P7(x3612,x3611,x3613) % 0.55/0.76 [344]~P25(x3442)+~P10(x3442)+E(x3441,f7(x3442))+~E(f26(f26(f8(x3442),x3443),x3441),x3443) % 0.55/0.76 [427]~P20(x4271)+~P7(f7(x4271),x4273,x4271)+~P7(f7(x4271),x4272,x4271)+P7(f7(x4271),f26(f26(f8(x4271),x4272),x4273),x4271) % 0.55/0.76 [428]~P20(x4281)+~P7(x4283,f7(x4281),x4281)+~P7(x4282,f7(x4281),x4281)+P7(f26(f26(f8(x4281),x4282),x4283),f7(x4281),x4281) % 0.55/0.76 [397]~P21(x3973)+~P7(x3971,x3974,x3973)+P7(x3971,x3972,x3973)+~P7(x3974,x3972,x3973) % 0.55/0.76 [398]~P23(x3983)+~P7(x3981,x3984,x3983)+P7(x3981,x3982,x3983)+~P7(x3984,x3982,x3983) % 0.55/0.76 [387]~P25(x3873)+~P10(x3873)+E(x3871,x3872)+~E(f26(f26(f8(x3873),x3874),x3871),f26(f26(f8(x3873),x3874),x3872)) % 0.55/0.76 [421]~P24(x4212)+~P7(x4211,x4214,x4212)+~P7(f7(x4212),x4213,x4212)+P7(x4211,f26(f26(f8(x4212),x4213),x4214),x4212) % 0.55/0.76 [439]~P18(x4391)+~P7(x4393,x4395,x4391)+~P7(x4392,x4394,x4391)+P7(f26(f26(f8(x4391),x4392),x4393),f26(f26(f8(x4391),x4394),x4395),x4391) % 0.55/0.76 [539]~P9(x5391,x5395,x5396)+P9(x5391,x5392,f44(x5393,x5394,x5391,x5392))+~P5(x5391,f21(a10,f9(x5397),x5395,a49,a49),x5394)+~P5(x5391,f21(a10,f21(a10,f9(x5397),x5395,a49,a49),x5392,a49,a49),x5393) % 0.55/0.76 [541]~P9(x5413,x5415,x5416)+~P5(x5413,f21(a10,f9(x5417),x5415,a49,a49),x5412)+~P5(x5413,f21(a10,f21(a10,f9(x5417),x5415,a49,a49),x5414,a49,a49),x5411)+E(f22(a46,f44(x5411,x5412,x5413,x5414),x5411,a51,a51),x5412) % 0.55/0.76 [479]~P5(x4796,x4792,x4795)+~P5(f36(x4796,x4793,x4795,a51),x4791,x4797)+~P28(f26(a6,x4792))+~P28(f26(a6,x4791))+~E(f26(f26(a46,x4794),x4795),a54)+P28(f26(a6,f14(x4791,x4792,x4793))) % 0.55/0.76 [480]~P5(x4806,x4802,x4804)+~P5(f36(x4806,x4803,x4804,a51),x4801,x4807)+~P28(f26(a6,x4802))+~P28(f26(a6,x4801))+~E(f26(f26(a46,x4804),x4805),a54)+P28(f26(a6,f14(x4801,x4802,x4803))) % 0.55/0.76 %EqnAxiom % 0.55/0.76 [1]E(x11,x11) % 0.55/0.76 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.76 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.76 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 0.55/0.76 [5]~E(x51,x52)+E(f23(x51,x53),f23(x52,x53)) % 0.55/0.76 [6]~E(x61,x62)+E(f23(x63,x61),f23(x63,x62)) % 0.55/0.76 [7]~E(x71,x72)+E(f21(x71,x73,x74,x75,x76),f21(x72,x73,x74,x75,x76)) % 0.55/0.76 [8]~E(x81,x82)+E(f21(x83,x81,x84,x85,x86),f21(x83,x82,x84,x85,x86)) % 0.55/0.76 [9]~E(x91,x92)+E(f21(x93,x94,x91,x95,x96),f21(x93,x94,x92,x95,x96)) % 0.55/0.76 [10]~E(x101,x102)+E(f21(x103,x104,x105,x101,x106),f21(x103,x104,x105,x102,x106)) % 0.55/0.76 [11]~E(x111,x112)+E(f21(x113,x114,x115,x116,x111),f21(x113,x114,x115,x116,x112)) % 0.55/0.76 [12]~E(x121,x122)+E(f12(x121),f12(x122)) % 0.55/0.76 [13]~E(x131,x132)+E(f25(x131,x133),f25(x132,x133)) % 0.55/0.76 [14]~E(x141,x142)+E(f25(x143,x141),f25(x143,x142)) % 0.55/0.76 [15]~E(x151,x152)+E(f9(x151),f9(x152)) % 0.55/0.76 [16]~E(x161,x162)+E(f26(x161,x163),f26(x162,x163)) % 0.55/0.76 [17]~E(x171,x172)+E(f26(x173,x171),f26(x173,x172)) % 0.55/0.77 [18]~E(x181,x182)+E(f43(x181,x183,x184,x185),f43(x182,x183,x184,x185)) % 0.55/0.77 [19]~E(x191,x192)+E(f43(x193,x191,x194,x195),f43(x193,x192,x194,x195)) % 0.55/0.77 [20]~E(x201,x202)+E(f43(x203,x204,x201,x205),f43(x203,x204,x202,x205)) % 0.55/0.77 [21]~E(x211,x212)+E(f43(x213,x214,x215,x211),f43(x213,x214,x215,x212)) % 0.55/0.77 [22]~E(x221,x222)+E(f19(x221,x223,x224),f19(x222,x223,x224)) % 0.55/0.77 [23]~E(x231,x232)+E(f19(x233,x231,x234),f19(x233,x232,x234)) % 0.55/0.77 [24]~E(x241,x242)+E(f19(x243,x244,x241),f19(x243,x244,x242)) % 0.55/0.77 [25]~E(x251,x252)+E(f22(x251,x253,x254,x255,x256),f22(x252,x253,x254,x255,x256)) % 0.55/0.77 [26]~E(x261,x262)+E(f22(x263,x261,x264,x265,x266),f22(x263,x262,x264,x265,x266)) % 0.55/0.77 [27]~E(x271,x272)+E(f22(x273,x274,x271,x275,x276),f22(x273,x274,x272,x275,x276)) % 0.55/0.77 [28]~E(x281,x282)+E(f22(x283,x284,x285,x281,x286),f22(x283,x284,x285,x282,x286)) % 0.55/0.77 [29]~E(x291,x292)+E(f22(x293,x294,x295,x296,x291),f22(x293,x294,x295,x296,x292)) % 0.55/0.77 [30]~E(x301,x302)+E(f5(x301,x303),f5(x302,x303)) % 0.55/0.77 [31]~E(x311,x312)+E(f5(x313,x311),f5(x313,x312)) % 0.55/0.77 [32]~E(x321,x322)+E(f44(x321,x323,x324,x325),f44(x322,x323,x324,x325)) % 0.55/0.77 [33]~E(x331,x332)+E(f44(x333,x331,x334,x335),f44(x333,x332,x334,x335)) % 0.55/0.77 [34]~E(x341,x342)+E(f44(x343,x344,x341,x345),f44(x343,x344,x342,x345)) % 0.55/0.77 [35]~E(x351,x352)+E(f44(x353,x354,x355,x351),f44(x353,x354,x355,x352)) % 0.55/0.77 [36]~E(x361,x362)+E(f45(x361,x363,x364,x365),f45(x362,x363,x364,x365)) % 0.55/0.77 [37]~E(x371,x372)+E(f45(x373,x371,x374,x375),f45(x373,x372,x374,x375)) % 0.55/0.77 [38]~E(x381,x382)+E(f45(x383,x384,x381,x385),f45(x383,x384,x382,x385)) % 0.55/0.77 [39]~E(x391,x392)+E(f45(x393,x394,x395,x391),f45(x393,x394,x395,x392)) % 0.55/0.77 [40]~E(x401,x402)+E(f35(x401),f35(x402)) % 0.55/0.77 [41]~E(x411,x412)+E(f13(x411,x413,x414),f13(x412,x413,x414)) % 0.55/0.77 [42]~E(x421,x422)+E(f13(x423,x421,x424),f13(x423,x422,x424)) % 0.55/0.77 [43]~E(x431,x432)+E(f13(x433,x434,x431),f13(x433,x434,x432)) % 0.55/0.77 [44]~E(x441,x442)+E(f48(x441),f48(x442)) % 0.55/0.77 [45]~E(x451,x452)+E(f27(x451,x453),f27(x452,x453)) % 0.55/0.77 [46]~E(x461,x462)+E(f27(x463,x461),f27(x463,x462)) % 0.55/0.77 [47]~E(x471,x472)+E(f7(x471),f7(x472)) % 0.55/0.77 [48]~E(x481,x482)+E(f31(x481,x483),f31(x482,x483)) % 0.55/0.77 [49]~E(x491,x492)+E(f31(x493,x491),f31(x493,x492)) % 0.55/0.77 [50]~E(x501,x502)+E(f8(x501),f8(x502)) % 0.55/0.77 [51]~E(x511,x512)+E(f29(x511,x513,x514,x515,x516),f29(x512,x513,x514,x515,x516)) % 0.55/0.77 [52]~E(x521,x522)+E(f29(x523,x521,x524,x525,x526),f29(x523,x522,x524,x525,x526)) % 0.55/0.77 [53]~E(x531,x532)+E(f29(x533,x534,x531,x535,x536),f29(x533,x534,x532,x535,x536)) % 0.55/0.77 [54]~E(x541,x542)+E(f29(x543,x544,x545,x541,x546),f29(x543,x544,x545,x542,x546)) % 0.55/0.77 [55]~E(x551,x552)+E(f29(x553,x554,x555,x556,x551),f29(x553,x554,x555,x556,x552)) % 0.55/0.77 [56]~E(x561,x562)+E(f36(x561,x563,x564,x565),f36(x562,x563,x564,x565)) % 0.55/0.77 [57]~E(x571,x572)+E(f36(x573,x571,x574,x575),f36(x573,x572,x574,x575)) % 0.55/0.77 [58]~E(x581,x582)+E(f36(x583,x584,x581,x585),f36(x583,x584,x582,x585)) % 0.55/0.77 [59]~E(x591,x592)+E(f36(x593,x594,x595,x591),f36(x593,x594,x595,x592)) % 0.55/0.77 [60]~E(x601,x602)+E(f30(x601,x603,x604,x605,x606),f30(x602,x603,x604,x605,x606)) % 0.55/0.77 [61]~E(x611,x612)+E(f30(x613,x611,x614,x615,x616),f30(x613,x612,x614,x615,x616)) % 0.55/0.77 [62]~E(x621,x622)+E(f30(x623,x624,x621,x625,x626),f30(x623,x624,x622,x625,x626)) % 0.55/0.77 [63]~E(x631,x632)+E(f30(x633,x634,x635,x631,x636),f30(x633,x634,x635,x632,x636)) % 0.55/0.77 [64]~E(x641,x642)+E(f30(x643,x644,x645,x646,x641),f30(x643,x644,x645,x646,x642)) % 0.55/0.77 [65]~E(x651,x652)+E(f39(x651,x653,x654,x655),f39(x652,x653,x654,x655)) % 0.55/0.77 [66]~E(x661,x662)+E(f39(x663,x661,x664,x665),f39(x663,x662,x664,x665)) % 0.55/0.77 [67]~E(x671,x672)+E(f39(x673,x674,x671,x675),f39(x673,x674,x672,x675)) % 0.55/0.77 [68]~E(x681,x682)+E(f39(x683,x684,x685,x681),f39(x683,x684,x685,x682)) % 0.55/0.77 [69]~E(x691,x692)+E(f32(x691,x693),f32(x692,x693)) % 0.55/0.77 [70]~E(x701,x702)+E(f32(x703,x701),f32(x703,x702)) % 0.55/0.77 [71]~E(x711,x712)+E(f14(x711,x713,x714),f14(x712,x713,x714)) % 0.55/0.77 [72]~E(x721,x722)+E(f14(x723,x721,x724),f14(x723,x722,x724)) % 0.55/0.77 [73]~E(x731,x732)+E(f14(x733,x734,x731),f14(x733,x734,x732)) % 0.55/0.77 [74]~E(x741,x742)+E(f33(x741,x743,x744),f33(x742,x743,x744)) % 0.55/0.77 [75]~E(x751,x752)+E(f33(x753,x751,x754),f33(x753,x752,x754)) % 0.55/0.77 [76]~E(x761,x762)+E(f33(x763,x764,x761),f33(x763,x764,x762)) % 0.55/0.77 [77]~E(x771,x772)+E(f28(x771,x773,x774),f28(x772,x773,x774)) % 0.55/0.77 [78]~E(x781,x782)+E(f28(x783,x781,x784),f28(x783,x782,x784)) % 0.55/0.77 [79]~E(x791,x792)+E(f28(x793,x794,x791),f28(x793,x794,x792)) % 0.55/0.77 [80]~E(x801,x802)+E(f16(x801,x803,x804,x805,x806),f16(x802,x803,x804,x805,x806)) % 0.55/0.77 [81]~E(x811,x812)+E(f16(x813,x811,x814,x815,x816),f16(x813,x812,x814,x815,x816)) % 0.55/0.77 [82]~E(x821,x822)+E(f16(x823,x824,x821,x825,x826),f16(x823,x824,x822,x825,x826)) % 0.55/0.77 [83]~E(x831,x832)+E(f16(x833,x834,x835,x831,x836),f16(x833,x834,x835,x832,x836)) % 0.55/0.77 [84]~E(x841,x842)+E(f16(x843,x844,x845,x846,x841),f16(x843,x844,x845,x846,x842)) % 0.55/0.77 [85]~E(x851,x852)+E(f15(x851,x853),f15(x852,x853)) % 0.55/0.77 [86]~E(x861,x862)+E(f15(x863,x861),f15(x863,x862)) % 0.55/0.77 [87]~E(x871,x872)+E(f20(x871,x873),f20(x872,x873)) % 0.55/0.77 [88]~E(x881,x882)+E(f20(x883,x881),f20(x883,x882)) % 0.55/0.77 [89]~E(x891,x892)+E(f24(x891,x893,x894),f24(x892,x893,x894)) % 0.55/0.77 [90]~E(x901,x902)+E(f24(x903,x901,x904),f24(x903,x902,x904)) % 0.55/0.77 [91]~E(x911,x912)+E(f24(x913,x914,x911),f24(x913,x914,x912)) % 0.55/0.77 [92]~E(x921,x922)+E(f37(x921),f37(x922)) % 0.55/0.77 [93]~E(x931,x932)+E(f41(x931,x933,x934,x935),f41(x932,x933,x934,x935)) % 0.55/0.77 [94]~E(x941,x942)+E(f41(x943,x941,x944,x945),f41(x943,x942,x944,x945)) % 0.55/0.77 [95]~E(x951,x952)+E(f41(x953,x954,x951,x955),f41(x953,x954,x952,x955)) % 0.55/0.77 [96]~E(x961,x962)+E(f41(x963,x964,x965,x961),f41(x963,x964,x965,x962)) % 0.55/0.77 [97]~E(x971,x972)+E(f40(x971,x973,x974),f40(x972,x973,x974)) % 0.55/0.77 [98]~E(x981,x982)+E(f40(x983,x981,x984),f40(x983,x982,x984)) % 0.55/0.77 [99]~E(x991,x992)+E(f40(x993,x994,x991),f40(x993,x994,x992)) % 0.55/0.77 [100]~E(x1001,x1002)+E(f17(x1001,x1003,x1004,x1005,x1006),f17(x1002,x1003,x1004,x1005,x1006)) % 0.55/0.77 [101]~E(x1011,x1012)+E(f17(x1013,x1011,x1014,x1015,x1016),f17(x1013,x1012,x1014,x1015,x1016)) % 0.55/0.77 [102]~E(x1021,x1022)+E(f17(x1023,x1024,x1021,x1025,x1026),f17(x1023,x1024,x1022,x1025,x1026)) % 0.55/0.77 [103]~E(x1031,x1032)+E(f17(x1033,x1034,x1035,x1031,x1036),f17(x1033,x1034,x1035,x1032,x1036)) % 0.55/0.77 [104]~E(x1041,x1042)+E(f17(x1043,x1044,x1045,x1046,x1041),f17(x1043,x1044,x1045,x1046,x1042)) % 0.55/0.77 [105]~E(x1051,x1052)+E(f42(x1051,x1053,x1054),f42(x1052,x1053,x1054)) % 0.55/0.77 [106]~E(x1061,x1062)+E(f42(x1063,x1061,x1064),f42(x1063,x1062,x1064)) % 0.55/0.77 [107]~E(x1071,x1072)+E(f42(x1073,x1074,x1071),f42(x1073,x1074,x1072)) % 0.55/0.77 [108]~E(x1081,x1082)+E(f18(x1081,x1083,x1084),f18(x1082,x1083,x1084)) % 0.55/0.77 [109]~E(x1091,x1092)+E(f18(x1093,x1091,x1094),f18(x1093,x1092,x1094)) % 0.55/0.77 [110]~E(x1101,x1102)+E(f18(x1103,x1104,x1101),f18(x1103,x1104,x1102)) % 0.55/0.77 [111]~E(x1111,x1112)+E(f47(x1111,x1113,x1114,x1115),f47(x1112,x1113,x1114,x1115)) % 0.55/0.77 [112]~E(x1121,x1122)+E(f47(x1123,x1121,x1124,x1125),f47(x1123,x1122,x1124,x1125)) % 0.55/0.77 [113]~E(x1131,x1132)+E(f47(x1133,x1134,x1131,x1135),f47(x1133,x1134,x1132,x1135)) % 0.55/0.77 [114]~E(x1141,x1142)+E(f47(x1143,x1144,x1145,x1141),f47(x1143,x1144,x1145,x1142)) % 0.55/0.77 [115]~E(x1151,x1152)+E(f52(x1151,x1153),f52(x1152,x1153)) % 0.55/0.77 [116]~E(x1161,x1162)+E(f52(x1163,x1161),f52(x1163,x1162)) % 0.55/0.77 [117]~E(x1171,x1172)+E(f38(x1171,x1173,x1174,x1175),f38(x1172,x1173,x1174,x1175)) % 0.55/0.77 [118]~E(x1181,x1182)+E(f38(x1183,x1181,x1184,x1185),f38(x1183,x1182,x1184,x1185)) % 0.55/0.77 [119]~E(x1191,x1192)+E(f38(x1193,x1194,x1191,x1195),f38(x1193,x1194,x1192,x1195)) % 0.55/0.77 [120]~E(x1201,x1202)+E(f38(x1203,x1204,x1205,x1201),f38(x1203,x1204,x1205,x1202)) % 0.55/0.77 [121]~E(x1211,x1212)+E(f34(x1211),f34(x1212)) % 0.55/0.77 [122]~P1(x1221)+P1(x1222)+~E(x1221,x1222) % 0.55/0.77 [123]~P2(x1231)+P2(x1232)+~E(x1231,x1232) % 0.55/0.77 [124]~P3(x1241)+P3(x1242)+~E(x1241,x1242) % 0.55/0.77 [125]~P13(x1251)+P13(x1252)+~E(x1251,x1252) % 0.55/0.77 [126]~P14(x1261)+P14(x1262)+~E(x1261,x1262) % 0.55/0.77 [127]~P15(x1271)+P15(x1272)+~E(x1271,x1272) % 0.55/0.77 [128]~P17(x1281)+P17(x1282)+~E(x1281,x1282) % 0.55/0.77 [129]~P4(x1291)+P4(x1292)+~E(x1291,x1292) % 0.55/0.77 [130]~P18(x1301)+P18(x1302)+~E(x1301,x1302) % 0.55/0.77 [131]~P19(x1311)+P19(x1312)+~E(x1311,x1312) % 0.55/0.77 [132]~P24(x1321)+P24(x1322)+~E(x1321,x1322) % 0.55/0.77 [133]~P20(x1331)+P20(x1332)+~E(x1331,x1332) % 0.55/0.77 [134]~P27(x1341)+P27(x1342)+~E(x1341,x1342) % 0.55/0.77 [135]~P21(x1351)+P21(x1352)+~E(x1351,x1352) % 0.55/0.77 [136]P5(x1362,x1363,x1364)+~E(x1361,x1362)+~P5(x1361,x1363,x1364) % 0.55/0.77 [137]P5(x1373,x1372,x1374)+~E(x1371,x1372)+~P5(x1373,x1371,x1374) % 0.55/0.77 [138]P5(x1383,x1384,x1382)+~E(x1381,x1382)+~P5(x1383,x1384,x1381) % 0.55/0.77 [139]~P23(x1391)+P23(x1392)+~E(x1391,x1392) % 0.55/0.77 [140]~P28(x1401)+P28(x1402)+~E(x1401,x1402) % 0.55/0.77 [141]~P22(x1411)+P22(x1412)+~E(x1411,x1412) % 0.55/0.77 [142]P8(x1422,x1423,x1424,x1425)+~E(x1421,x1422)+~P8(x1421,x1423,x1424,x1425) % 0.55/0.77 [143]P8(x1433,x1432,x1434,x1435)+~E(x1431,x1432)+~P8(x1433,x1431,x1434,x1435) % 0.55/0.77 [144]P8(x1443,x1444,x1442,x1445)+~E(x1441,x1442)+~P8(x1443,x1444,x1441,x1445) % 0.55/0.77 [145]P8(x1453,x1454,x1455,x1452)+~E(x1451,x1452)+~P8(x1453,x1454,x1455,x1451) % 0.55/0.77 [146]P6(x1462,x1463,x1464)+~E(x1461,x1462)+~P6(x1461,x1463,x1464) % 0.55/0.77 [147]P6(x1473,x1472,x1474)+~E(x1471,x1472)+~P6(x1473,x1471,x1474) % 0.55/0.77 [148]P6(x1483,x1484,x1482)+~E(x1481,x1482)+~P6(x1483,x1484,x1481) % 0.55/0.77 [149]P7(x1492,x1493,x1494)+~E(x1491,x1492)+~P7(x1491,x1493,x1494) % 0.55/0.77 [150]P7(x1503,x1502,x1504)+~E(x1501,x1502)+~P7(x1503,x1501,x1504) % 0.55/0.77 [151]P7(x1513,x1514,x1512)+~E(x1511,x1512)+~P7(x1513,x1514,x1511) % 0.55/0.77 [152]P9(x1522,x1523,x1524)+~E(x1521,x1522)+~P9(x1521,x1523,x1524) % 0.55/0.77 [153]P9(x1533,x1532,x1534)+~E(x1531,x1532)+~P9(x1533,x1531,x1534) % 0.55/0.77 [154]P9(x1543,x1544,x1542)+~E(x1541,x1542)+~P9(x1543,x1544,x1541) % 0.55/0.77 [155]~P16(x1551)+P16(x1552)+~E(x1551,x1552) % 0.55/0.77 [156]~P29(x1561)+P29(x1562)+~E(x1561,x1562) % 0.55/0.77 [157]~P10(x1571)+P10(x1572)+~E(x1571,x1572) % 0.55/0.77 [158]P11(x1582,x1583,x1584)+~E(x1581,x1582)+~P11(x1581,x1583,x1584) % 0.55/0.77 [159]P11(x1593,x1592,x1594)+~E(x1591,x1592)+~P11(x1593,x1591,x1594) % 0.55/0.77 [160]P11(x1603,x1604,x1602)+~E(x1601,x1602)+~P11(x1603,x1604,x1601) % 0.55/0.77 [161]~P26(x1611)+P26(x1612)+~E(x1611,x1612) % 0.55/0.77 [162]~P25(x1621)+P25(x1622)+~E(x1621,x1622) % 0.55/0.77 [163]~P12(x1631)+P12(x1632)+~E(x1631,x1632) % 0.55/0.77 % 0.55/0.77 %------------------------------------------- % 0.55/0.77 cnf(572,plain, % 0.55/0.77 (~E(f19(x5721,x5722,x5723),x5722)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(575,plain, % 0.55/0.77 (~E(f19(x5751,x5752,x5753),x5752)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(578,plain, % 0.55/0.77 (~E(f19(x5781,x5782,x5783),x5782)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(581,plain, % 0.55/0.77 (~E(f19(x5811,x5812,x5813),x5812)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(584,plain, % 0.55/0.77 (~E(f19(x5841,x5842,x5843),x5842)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(587,plain, % 0.55/0.77 (~E(f19(x5871,x5872,x5873),x5872)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(590,plain, % 0.55/0.77 (~E(f19(x5901,x5902,x5903),x5902)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(598,plain, % 0.55/0.77 (~E(f19(x5981,x5982,x5983),x5982)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(601,plain, % 0.55/0.77 (~E(f19(x6011,x6012,x6013),x6012)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(607,plain, % 0.55/0.77 (~E(f19(x6071,x6072,x6073),x6072)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(610,plain, % 0.55/0.77 (~E(f19(x6101,x6102,x6103),x6102)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(613,plain, % 0.55/0.77 (~E(f19(x6131,x6132,x6133),x6132)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(619,plain, % 0.55/0.77 (P5(x6191,f9(x6192),f26(x6191,x6192))), % 0.55/0.77 inference(rename_variables,[],[215])). % 0.55/0.77 cnf(626,plain, % 0.55/0.77 (P28(f26(f26(f32(x6261,x6262),x6263),x6263))), % 0.55/0.77 inference(rename_variables,[],[227])). % 0.55/0.77 cnf(631,plain, % 0.55/0.77 (P28(f26(f26(f32(x6311,x6312),x6313),x6313))), % 0.55/0.77 inference(rename_variables,[],[227])). % 0.55/0.77 cnf(640,plain, % 0.55/0.77 (P28(f26(f26(f32(x6401,x6402),x6403),x6403))), % 0.55/0.77 inference(rename_variables,[],[227])). % 0.55/0.77 cnf(643,plain, % 0.55/0.77 (P28(f26(f26(f32(x6431,x6432),x6433),x6433))), % 0.55/0.77 inference(rename_variables,[],[227])). % 0.55/0.77 cnf(646,plain, % 0.55/0.77 (P28(f26(f26(f32(x6461,x6462),x6463),x6463))), % 0.55/0.77 inference(rename_variables,[],[227])). % 0.55/0.77 cnf(659,plain, % 0.55/0.77 (E(f28(f27(x6591,f48(x6592)),f13(x6591,x6593,x6592),x6592),x6591)), % 0.55/0.77 inference(rename_variables,[],[230])). % 0.55/0.77 cnf(661,plain, % 0.55/0.77 (~E(f19(x6611,x6612,x6613),x6612)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(664,plain, % 0.55/0.77 (~E(f19(x6641,x6642,x6643),x6642)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(669,plain, % 0.55/0.77 (~P28(f26(f26(a11,f9(x6691)),x6692))), % 0.55/0.77 inference(rename_variables,[],[298])). % 0.55/0.77 cnf(670,plain, % 0.55/0.77 (~E(f19(x6701,x6702,x6703),x6702)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(673,plain, % 0.55/0.77 (~P28(f26(f26(a11,f9(x6731)),x6732))), % 0.55/0.77 inference(rename_variables,[],[298])). % 0.55/0.77 cnf(676,plain, % 0.55/0.77 (~E(f19(x6761,x6762,x6763),x6762)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(679,plain, % 0.55/0.77 (~E(f19(x6791,x6792,x6793),x6792)), % 0.55/0.77 inference(rename_variables,[],[291])). % 0.55/0.77 cnf(681,plain, % 0.55/0.77 (P5(x6811,f9(x6812),f26(x6811,x6812))), % 0.55/0.77 inference(rename_variables,[],[215])). % 0.55/0.77 cnf(686,plain, % 0.55/0.77 (~P8(x6861,x6862,f4(x6863),x6863)), % 0.55/0.77 inference(rename_variables,[],[300])). % 0.55/0.77 cnf(700,plain, % 0.55/0.77 (~P7(x7001,x7001,a2)), % 0.55/0.77 inference(rename_variables,[],[289])). % 0.55/0.77 cnf(713,plain, % 0.55/0.77 ($false), % 0.55/0.77 inference(scs_inference,[],[279,164,230,659,251,215,619,681,195,270,273,227,626,631,640,643,646,257,300,686,289,700,198,291,572,575,578,581,584,587,590,598,601,607,610,613,661,664,670,676,679,296,281,293,175,179,182,285,287,187,298,669,673,459,309,310,329,330,335,338,339,348,381,382,409,441,489,490,491,2,470,473,475,476,485,488,497,517,518,519,527,529,532,536,331,390,448,533,156,343,380,430,461,483,502,3,136,450,474,478,487,140,145,148,392,395,361,421,316,498]), % 0.55/0.77 ['proof']). % 0.55/0.77 % SZS output end Proof % 0.55/0.77 % Total time :0.169129s %------------------------------------------------------------------------------