%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL802-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n027.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:52 AM UTC 2026 % Result : Unsatisfiable 0.43s 0.60s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL802-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.34 % Computer : n027.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Sat Sep 5 19:23:43 UTC 2026 % 0.07/0.34 % CPUTime : % 0.26/0.51 start to proof:theBenchmark % 0.43/0.56 %------------------------------------------- % 0.43/0.56 % File :CSE---1.7 % 0.43/0.56 % Problem :theBenchmark % 0.43/0.56 % Transform :cnf % 0.43/0.56 % Format :tptp:raw % 0.43/0.56 % Command :java -jar mcs_scs.jar %d %s % 0.43/0.56 % 0.43/0.56 % Result :Theorem 0.029049s % 0.43/0.56 % Output :CNFRefutation 0.029049s % 0.43/0.56 %------------------------------------------- % 0.43/0.57 %------------------------------------------------------------------------------ % 0.43/0.57 % File : LCL802-1 : TPTP v9.3.1. Released v4.1.0. % 0.43/0.57 % Domain : Logic Calculi % 0.43/0.57 % Problem : Strong normalization of typed lambda calculus 156_15 % 0.43/0.57 % Version : Especial. % 0.43/0.57 % English : % 0.43/0.57 % 0.43/0.57 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.43/0.57 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.43/0.57 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.43/0.57 % Source : [Nip10] % 0.43/0.57 % Names : StrongNorm-156_15 [Nip10] % 0.43/0.57 % 0.43/0.57 % Status : Unsatisfiable % 0.43/0.57 % Rating : 0.17 v9.3.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.00 v6.0.0, 0.10 v5.5.0, 0.20 v5.4.0, 0.15 v5.3.0, 0.17 v5.2.0, 0.12 v5.1.0, 0.24 v5.0.0, 0.21 v4.1.0 % 0.43/0.57 % Syntax : Number of clauses : 329 ( 112 unt; 20 nHn; 188 RR) % 0.43/0.57 % Number of literals : 645 ( 215 equ; 317 neg) % 0.43/0.57 % Maximal clause size : 6 ( 1 avg) % 0.43/0.57 % Maximal term depth : 6 ( 2 avg) % 0.43/0.57 % Number of predicates : 31 ( 30 usr; 0 prp; 1-4 aty) % 0.43/0.57 % Number of functors : 56 ( 56 usr; 23 con; 0-6 aty) % 0.43/0.57 % Number of variables : 978 ( 155 sgn) % 0.43/0.57 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.43/0.57 % 0.43/0.57 % Comments : % 0.43/0.57 %------------------------------------------------------------------------------ % 0.43/0.57 cnf(cls_append__eq__Cons__conv_5,axiom, % 0.43/0.57 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.43/0.57 % 0.43/0.57 cnf(cls_append__Cons_0,axiom, % 0.43/0.57 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.43/0.57 % 0.43/0.57 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.43/0.57 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.57 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.57 | 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.43/0.57 | V_y = V_z ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_add__imp__eq_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.43/0.57 | 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.43/0.57 | V_b = V_c ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_add__left__cancel_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.43/0.57 | 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.43/0.57 | V_b = V_c ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_add__right__cancel_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.43/0.57 | 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.43/0.57 | V_b = V_c ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_Cons__eq__append__conv_5,axiom, % 0.43/0.57 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.43/0.57 % 0.43/0.57 cnf(cls_Cons__eq__appendI_0,axiom, % 0.43/0.57 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.43/0.57 % 0.43/0.57 cnf(cls_neq__Nil__conv_1,axiom, % 0.43/0.57 c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_list_Osimps_I3_J_0,axiom, % 0.43/0.57 c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_Cons__step1__Cons_0,axiom, % 0.43/0.57 ( V_x = V_y % 0.43/0.57 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.43/0.57 | ~ 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.43/0.57 % 0.43/0.57 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.43/0.57 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.57 | 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.43/0.57 % 0.43/0.57 cnf(cls_not__Cons__self2_0,axiom, % 0.43/0.57 c_List_Olist_OCons(V_x,V_t,T_a) != V_t ). % 0.43/0.57 % 0.43/0.57 cnf(cls_not__Cons__self_0,axiom, % 0.43/0.57 V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_Snoc__step1__SnocD_0,axiom, % 0.43/0.57 ( V_ys = V_xs % 0.43/0.57 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.43/0.57 | ~ 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.43/0.57 % 0.43/0.57 cnf(cls_rtranclp__idemp_0,axiom, % 0.43/0.57 c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(V_r,T_a),T_a) = c_Transitive__Closure_Ortranclp(V_r,T_a) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.43/0.57 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_x) = V_x ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.43/0.57 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.57 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.57 | V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_HOL_Ozero__class_Ozero(T_a)) ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_add__0__left_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.43/0.57 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.43/0.57 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.43/0.57 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.57 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.43/0.57 % 0.43/0.57 cnf(cls_Snoc__step1__SnocD_1,axiom, % 0.43/0.57 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.43/0.57 | c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.43/0.57 | ~ 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.43/0.57 % 0.43/0.57 cnf(cls_rtranclp__converseI_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_rtranclp__converseD_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_foldl__Cons_0,axiom, % 0.43/0.58 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.43/0.58 % 0.43/0.58 cnf(cls_lordered__ab__group__add__class_Oadd__sup__inf__distribs_I1_J_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.58 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a)),V_c) = c_Lattices_Olower__semilattice__class_Oinf(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.43/0.58 % 0.43/0.58 cnf(cls_lordered__ab__group__add__class_Oadd__sup__inf__distribs_I2_J_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.58 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_Lattices_Olower__semilattice__class_Oinf(V_b,V_c,T_a)) = c_Lattices_Olower__semilattice__class_Oinf(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),T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__inf__distrib__right_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add__meet(T_a) % 0.43/0.58 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a)),V_c) = c_Lattices_Olower__semilattice__class_Oinf(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.43/0.58 % 0.43/0.58 cnf(cls_add__inf__distrib__left_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add__meet(T_a) % 0.43/0.58 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_Lattices_Olower__semilattice__class_Oinf(V_b,V_c,T_a)) = c_Lattices_Olower__semilattice__class_Oinf(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),T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__cancel__21_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.58 | 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.43/0.58 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) = V_u ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_conversepD_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(V_r,V_b),V_a)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_conversep__iff_1,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_a)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_conversep_Ocases_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(V_r,V_a2),V_a1)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a1),V_a2)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_conversep_Ointros_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_b),V_a)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_add__cancel__21_1,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_double__eq__0__iff_1,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_append__step1I_0,axiom, % 0.43/0.58 ( ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_append__step1I_1,axiom, % 0.43/0.58 ( 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.43/0.58 | ~ c_ListOrder_Ostep1(V_r,V_vs,V_us,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_Cons__step1__Cons_2,axiom, % 0.43/0.58 ( V_x = V_y % 0.43/0.58 | V_xs = V_ys % 0.43/0.58 | ~ 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.43/0.58 % 0.43/0.58 cnf(cls_Cons__step1__Cons_4,axiom, % 0.43/0.58 ( ~ hBOOL(hAPP(hAPP(V_r,V_y),V_xa)) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_rtranclp_Ortrancl__refl_0,axiom, % 0.43/0.58 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_a)) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_Nitpick_Ortranclp__def_1,axiom, % 0.43/0.58 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_x)) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_accp__downwards_0,axiom, % 0.43/0.58 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) % 0.43/0.58 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_accp__downwards__aux_0,axiom, % 0.43/0.58 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.43/0.58 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_rtranclp__trans_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_z)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_z)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_IT__implies__termi_0,axiom, % 0.43/0.58 ( c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_t,tc_Lambda_OdB) % 0.43/0.58 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_termi__implies__IT_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(c_InductTermi_OIT,V_r)) % 0.43/0.58 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_r,tc_Lambda_OdB) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_foldl__assoc_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Osemigroup__add(T_a) % 0.43/0.58 | 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.43/0.58 % 0.43/0.58 cnf(cls_Snoc__step1__SnocD_3,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.43/0.58 | V_y = V_x % 0.43/0.58 | ~ 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.43/0.58 % 0.43/0.58 cnf(cls_of__nat__eq__iff_0,axiom, % 0.43/0.58 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.43/0.58 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.43/0.58 | V_m = V_n ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.43/0.58 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.58 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.58 | V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_a) % 0.43/0.58 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_double__eq__0__iff_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.58 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.58 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_r__into__rtranclp_0,axiom, % 0.43/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) % 0.43/0.58 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_not__Nil__step1_0,axiom, % 0.43/0.58 ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_not__step1__Nil_0,axiom, % 0.43/0.58 ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_conversep__eq_0,axiom, % 0.43/0.58 c_Predicate_Oconversep(c_fequal(T_a),T_a,T_a) = c_fequal(T_a) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_Cons__step1__Cons_3,axiom, % 0.43/0.58 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.43/0.58 | V_xs = V_ys % 0.43/0.58 | ~ 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.43/0.58 % 0.43/0.58 cnf(cls_add__strict__mono_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.43/0.58 | 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.43/0.58 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.43/0.58 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_list_Osimps_I2_J_0,axiom, % 0.43/0.58 c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_Snoc__step1__SnocD_2,axiom, % 0.43/0.58 ( V_ys = V_xs % 0.43/0.58 | V_y = V_x % 0.43/0.58 | ~ 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.43/0.58 % 0.43/0.58 cnf(cls_foldr_Osimps_I2_J_0,axiom, % 0.43/0.58 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.43/0.58 % 0.43/0.58 cnf(cls_conversep__conversep_0,axiom, % 0.43/0.58 c_Predicate_Oconversep(c_Predicate_Oconversep(V_r,T_a,T_b),T_b,T_a) = V_r ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__strict__right__mono_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.43/0.58 | 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.43/0.58 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__less__cancel__right_1,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.43/0.58 | 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.43/0.58 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__less__cancel__right_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.43/0.58 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.43/0.58 | ~ 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.43/0.58 % 0.43/0.58 cnf(cls_add__strict__left__mono_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.43/0.58 | 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.43/0.58 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__less__cancel__left_1,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.43/0.58 | 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.43/0.58 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.43/0.58 % 0.43/0.58 cnf(cls_add__less__cancel__left_0,axiom, % 0.43/0.58 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.43/0.58 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.43/0.58 | ~ 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.43/0.58 % 0.43/0.58 cnf(cls_list_Oinject_0,axiom, % 0.43/0.58 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.43/0.59 | V_a = V_a_H ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_list_Oinject_1,axiom, % 0.43/0.59 ( c_List_Olist_OCons(V_a,V_list,T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) % 0.43/0.59 | V_list = V_list_H ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Cons__step1__Cons_1,axiom, % 0.43/0.59 ( c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) % 0.43/0.59 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_Cons__step1__Cons_5,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ c_ListOrder_Ostep1(V_r,V_ys,V_xs,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_converse__rtranclp__into__rtranclp_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_c)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_c)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_b)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_accp_Ocases_0,axiom, % 0.43/0.59 ( c_Wellfounded_Oaccp(V_r,V_y,T_a) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_y),V_a)) % 0.43/0.59 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_accp__downward_0,axiom, % 0.43/0.59 ( c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) % 0.43/0.59 | ~ c_Wellfounded_Oaccp(V_r,V_b,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.59 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_add__neg__neg_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.59 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.59 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_even__less__0__iff_0,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.43/0.59 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_even__less__0__iff_1,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_add__pos__pos_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.43/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_pos__add__strict_0,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.59 | c_HOL_Oord__class_Oless(V_b,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),T_a) % 0.43/0.59 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.43/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_of__nat__0_0,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.43/0.59 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_of__nat__less__iff_1,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_of__nat__less__iff_0,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.59 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_length__0__conv_1,axiom, % 0.43/0.59 c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_length__0__conv_0,axiom, % 0.43/0.59 ( c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.59 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_foldl__absorb0_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.43/0.59 | 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.43/0.59 % 0.43/0.59 cnf(cls_Cons__eq__append__conv_4,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_append__eq__Cons__conv_4,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_append1__eq__conv_0,axiom, % 0.43/0.59 ( 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.43/0.59 | V_xs = V_ys ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_append1__eq__conv_1,axiom, % 0.43/0.59 ( 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.43/0.59 | V_x = V_y ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_rtrancl__beta__App_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_rtrancl__beta__AppL_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_rtrancl__beta__AppR_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_rtrancl__beta__Abs_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.43/0.59 ( 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.43/0.59 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_subst__preserves__beta2_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_subst__preserves__beta_H_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_subst__preserves__beta2_H_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_head__Var__reduction_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_typing__elims_I2_J_1,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_u),c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u))) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u)),V_T)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_subject__reduction_H_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_t_H),V_T)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_t),V_T)) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_lift__preserves__beta_H_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_foldr__conv__foldl_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.43/0.59 | 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.43/0.59 % 0.43/0.59 cnf(cls_inf__commute_0,axiom, % 0.43/0.59 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.59 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_inf__sup__aci_I1_J_0,axiom, % 0.43/0.59 ( ~ class_Lattices_Olattice(T_a) % 0.43/0.59 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.43/0.59 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.43/0.59 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.43/0.59 ( 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.43/0.59 | V_r = V_s ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Lambda_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.43/0.59 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_appR_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_appL_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_uIT_0,axiom, % 0.43/0.59 hBOOL(hAPP(c_InductTermi_OIT,v_u____)) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_subst__lift_0,axiom, % 0.43/0.59 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.43/0.59 % 0.43/0.59 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.43/0.59 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.43/0.59 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_lift__preserves__beta_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_app__Var__IT_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),c_Lambda_OdB_OVar(V_i)))) % 0.43/0.59 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Nil__is__append__conv_2,axiom, % 0.43/0.59 c_List_Olist_ONil(T_a) = c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_inf1E_1,axiom, % 0.43/0.59 ( hBOOL(hAPP(V_B,V_x)) % 0.43/0.59 | ~ hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_inf1E_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(V_A,V_x)) % 0.43/0.59 | ~ hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_abs_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_foldl__append_0,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.43/0.59 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_var__app__types_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_var__app__typesE_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_Var_I2_J_0,axiom, % 0.43/0.59 hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_list__app__typeE_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_list__app__typeD_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_var__app__typesE_1,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_var__app__types_1,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_Cons_0,axiom, % 0.43/0.59 v_rs____ = c_List_Olist_OCons(v_a____,v_as____,tc_Lambda_OdB) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_list__app__typeD_1,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_list__app__typeE_1,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(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.43/0.59 % 0.43/0.59 cnf(cls_head__Var__reduction_1,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.59 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.43/0.59 | ~ 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.43/0.59 % 0.43/0.59 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.43/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.59 | 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.43/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_typing__elims_I2_J_0,axiom, % 0.43/0.59 ( hBOOL(hAPP(hAPP(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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u)),V_T)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_foldl__foldr1_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.43/0.59 | 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.43/0.59 % 0.43/0.59 cnf(cls_foldl__foldr1__lemma_0,axiom, % 0.43/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.43/0.59 | 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.43/0.59 % 0.43/0.59 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.43/0.59 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.43/0.59 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.43/0.59 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.43/0.59 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.43/0.59 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.43/0.59 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.43/0.59 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.43/0.59 % 0.43/0.59 cnf(cls_apps__preserves__beta2_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_apps__preserves__betas_0,axiom, % 0.43/0.59 ( 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.43/0.59 | ~ c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,V_ss,tc_Lambda_OdB) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_double__induction__lemma_0,axiom, % 0.43/0.59 ( ~ 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.43/0.59 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_s,tc_Lambda_OdB) % 0.43/0.59 | 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.43/0.59 % 0.43/0.59 cnf(cls_length__greater__0__conv_1,axiom, % 0.43/0.59 ( 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.43/0.59 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.43/0.59 % 0.43/0.59 cnf(cls_length__greater__0__conv_0,axiom, % 0.43/0.60 ~ 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.43/0.60 % 0.43/0.60 cnf(cls_Int__commute_0,axiom, % 0.43/0.60 c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_B,V_A,tc_fun(T_a,tc_bool)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_T_0,axiom, % 0.43/0.60 v_T____ = hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.43/0.60 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__Var_1,axiom, % 0.43/0.60 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.43/0.60 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_not__less0_0,axiom, % 0.43/0.60 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_gr__implies__not0_0,axiom, % 0.43/0.60 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_xt1_I10_J_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_order__less__trans_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_list__app__typeI_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(hAPP(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.43/0.60 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(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.43/0.60 % 0.43/0.60 cnf(cls_Var_I3_J_0,axiom, % 0.43/0.60 hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__Var_2,axiom, % 0.43/0.60 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.43/0.60 | V_i = V_k % 0.43/0.60 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__preserves__beta_0,axiom, % 0.43/0.60 ( 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.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__same__eq_0,axiom, % 0.43/0.60 ( c_List_Oappend(V_ys,V_xs,T_a) != c_List_Oappend(V_zs,V_xs,T_a) % 0.43/0.60 | V_ys = V_zs ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_same__append__eq_0,axiom, % 0.43/0.60 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Oappend(V_xs,V_zs,T_a) % 0.43/0.60 | V_ys = V_zs ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__Nil2_0,axiom, % 0.43/0.60 c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) = V_xs ). % 0.43/0.60 % 0.43/0.60 cnf(cls_eq__Nil__appendI_0,axiom, % 0.43/0.60 V_x = c_List_Oappend(c_List_Olist_ONil(T_a),V_x,T_a) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_self__append__conv_1,axiom, % 0.43/0.60 V_xs = c_List_Oappend(V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__Nil_0,axiom, % 0.43/0.60 c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) = V_ys ). % 0.43/0.60 % 0.43/0.60 cnf(cls_self__append__conv2_1,axiom, % 0.43/0.60 V_ys = c_List_Oappend(c_List_Olist_ONil(T_a),V_ys,T_a) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_foldr__append_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_Var__IT_0,axiom, % 0.43/0.60 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.43/0.60 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Beta_0,axiom, % 0.43/0.60 ( 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.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.43/0.60 | ~ 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.43/0.60 % 0.43/0.60 cnf(cls_foldl__Nil_0,axiom, % 0.43/0.60 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.43/0.60 % 0.43/0.60 cnf(cls_lift__IT_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(V_t,V_i))) % 0.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_inf__sup__aci_I2_J_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_inf__sup__aci_I3_J_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_inf__left__commute_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_inf__assoc_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Int__assoc_0,axiom, % 0.43/0.60 c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_C,tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_A,c_Lattices_Olower__semilattice__class_Oinf(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Int__left__commute_0,axiom, % 0.43/0.60 c_Lattices_Olower__semilattice__class_Oinf(V_A,c_Lattices_Olower__semilattice__class_Oinf(V_B,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_B,c_Lattices_Olower__semilattice__class_Oinf(V_A,V_C,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Nil__is__append__conv_0,axiom, % 0.43/0.60 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.43/0.60 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Nil__is__append__conv_1,axiom, % 0.43/0.60 ( c_List_Olist_ONil(T_a) != c_List_Oappend(V_xs,V_ys,T_a) % 0.43/0.60 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.43/0.60 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.43/0.60 | V_dB = V_dB_H ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__is__Nil__conv_0,axiom, % 0.43/0.60 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.43/0.60 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__is__Nil__conv_1,axiom, % 0.43/0.60 ( c_List_Oappend(V_xs,V_ys,T_a) != c_List_Olist_ONil(T_a) % 0.43/0.60 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.43/0.60 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.43/0.60 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.43/0.60 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_apps__preserves__beta_0,axiom, % 0.43/0.60 ( 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.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_uT_H_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(c_Type_Otyping(v_e____),v_u____),hAPP(hAPP(c_Type_Otype_OFun,v_T_H_H____),c_List_Ofoldr(c_Type_Otype_OFun,v_Ts____,v_T_H____,tc_Type_Otype,tc_Type_Otype)))) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_nat__less__le_1,axiom, % 0.43/0.60 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_less__not__refl_0,axiom, % 0.43/0.60 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_order__less__le_1,axiom, % 0.43/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_linorder__neq__iff_1,axiom, % 0.43/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_order__less__irrefl_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_beta_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.43/0.60 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.43/0.60 | V_x = V_y ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.43/0.60 | V_x = V_y % 0.43/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_nat__neq__iff_0,axiom, % 0.43/0.60 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.43/0.60 | V_m = V_n ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_nat__less__cases_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.43/0.60 | V_m = V_n % 0.43/0.60 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_var__app__type__eq_0,axiom, % 0.43/0.60 ( V_T = V_U % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(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.43/0.60 | ~ hBOOL(hAPP(hAPP(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.43/0.60 % 0.43/0.60 cnf(cls_linorder__neqE__nat_0,axiom, % 0.43/0.60 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.43/0.60 | V_x = V_y ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_linorder__neqE_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.43/0.60 | V_x = V_y ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_linorder__less__linear_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.43/0.60 | V_x = V_y % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.43/0.60 | V_x = V_y % 0.43/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.43/0.60 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.43/0.60 | V_dB2 = V_dB2_H ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.43/0.60 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.43/0.60 | V_dB1 = V_dB1_H ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_IT_OVar_0,axiom, % 0.43/0.60 ( 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.43/0.60 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_less__infI2_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_b,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_less__infI1_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.60 | c_HOL_Oord__class_Oless(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_a,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.43/0.60 ( 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.43/0.60 | V_rs = V_ss ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.43/0.60 ( 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.43/0.60 | V_r = V_s ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.43/0.60 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.43/0.60 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_App_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(hAPP(c_Type_Otyping(V_env),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),V_U)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_env),V_t),V_T)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_env),V_s),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U))) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_beta__cases_I1_J_0,axiom, % 0.43/0.60 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_gr0I_0,axiom, % 0.43/0.60 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.43/0.60 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_neq0__conv_1,axiom, % 0.43/0.60 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_inf__sup__aci_I4_J_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_inf__left__idem_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Int__left__absorb_0,axiom, % 0.43/0.60 c_Lattices_Olower__semilattice__class_Oinf(V_A,c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),tc_fun(T_a,tc_bool)) = c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__lt_0,axiom, % 0.43/0.60 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__Var__IT_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j))) % 0.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__self__conv_0,axiom, % 0.43/0.60 ( c_List_Oappend(V_xs,V_ys,T_a) != V_xs % 0.43/0.60 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_self__append__conv_0,axiom, % 0.43/0.60 ( V_xs != c_List_Oappend(V_xs,V_ys,T_a) % 0.43/0.60 | V_ys = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__self__conv2_0,axiom, % 0.43/0.60 ( c_List_Oappend(V_xs,V_ys,T_a) != V_ys % 0.43/0.60 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_self__append__conv2_0,axiom, % 0.43/0.60 ( V_ys != c_List_Oappend(V_xs,V_ys,T_a) % 0.43/0.60 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_type_Osimps_I2_J_1,axiom, % 0.43/0.60 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.43/0.60 | V_type2 = V_type2_H ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_type_Osimps_I2_J_0,axiom, % 0.43/0.60 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.43/0.60 | V_type1 = V_type1_H ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_inf__idem_0,axiom, % 0.43/0.60 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.43/0.60 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_x,T_a) = V_x ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Int__absorb_0,axiom, % 0.43/0.60 c_Lattices_Olower__semilattice__class_Oinf(V_A,V_A,tc_fun(T_a,tc_bool)) = V_A ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__eq_0,axiom, % 0.43/0.60 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.43/0.60 ( 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.43/0.60 | V_rs = V_ss ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.43/0.60 ( 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.43/0.60 | V_m = V_n ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.43/0.60 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.43/0.60 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.43/0.60 | V_nat = V_nat_H ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.43/0.60 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.43/0.60 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__App_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_inf1I_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_x)) % 0.43/0.60 | ~ hBOOL(hAPP(V_B,V_x)) % 0.43/0.60 | ~ hBOOL(hAPP(V_A,V_x)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__is__Nil__conv_2,axiom, % 0.43/0.60 c_List_Oappend(c_List_Olist_ONil(T_a),c_List_Olist_ONil(T_a),T_a) = c_List_Olist_ONil(T_a) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__assoc_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_append__eq__appendI_0,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_append__eq__append__conv2_4,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_append__eq__append__conv2_5,axiom, % 0.43/0.60 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.43/0.60 % 0.43/0.60 cnf(cls_xt1_I9_J_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.43/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_order__less__asym_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_order__less__asym_H_0,axiom, % 0.43/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_lift__type_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(hAPP(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.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_t),V_T)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_uT_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(c_Type_Otyping(v_e____),v_u____),v_T____)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subject__reduction_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_t_H),V_T)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_t),V_T)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_lists__typings_0,axiom, % 0.43/0.60 ( c_List_Olistsp(c_COMBB(c_Ex(tc_Type_Otype),c_Type_Otyping(V_e),tc_fun(tc_Type_Otype,tc_bool),tc_bool,tc_Lambda_OdB),V_ts,tc_Lambda_OdB) % 0.43/0.60 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_image__image_0,axiom, % 0.43/0.60 c_Set_Oimage(V_f,c_Set_Oimage(V_g,V_A,T_c,T_b),T_b,T_a) = c_Set_Oimage(c_COMBB(V_f,V_g,T_b,T_a,T_c),V_A,T_c,T_a) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_shift__gt_0,axiom, % 0.43/0.60 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,V_j) % 0.43/0.60 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__in__listsp__conv_2,axiom, % 0.43/0.60 ( c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) % 0.43/0.60 | ~ c_List_Olistsp(V_A,V_ys,T_a) % 0.43/0.60 | ~ c_List_Olistsp(V_A,V_xs,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_in__listsp__conv__set_2,axiom, % 0.43/0.60 ( c_List_Olistsp(V_A,V_xs,T_a) % 0.43/0.60 | ~ hBOOL(hAPP(V_A,c_List_Osko__List__Xin__listsp__conv__set__1__1(V_A,V_xs,T_a))) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_listsp__infI_0,axiom, % 0.43/0.60 ( c_List_Olistsp(c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,tc_fun(T_a,tc_bool)),V_l,T_a) % 0.43/0.60 | ~ c_List_Olistsp(V_B,V_l,T_a) % 0.43/0.60 | ~ c_List_Olistsp(V_A,V_l,T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_argT_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),v_a____),v_T_H_H____)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_MI2_0,axiom, % 0.43/0.60 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.43/0.60 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_u),V_T2)) % 0.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T2,tc_Type_Otype)),V_t),V_Ta)) % 0.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_MI1_0,axiom, % 0.43/0.60 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.43/0.60 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),V_u),V_T1)) % 0.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T1,tc_Type_Otype)),V_t),V_Ta)) % 0.43/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_shift__eq_0,axiom, % 0.43/0.60 hAPP(c_Type_Oshift(V_e,V_x,V_T,T_a),V_x) = V_T ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Abs_0,axiom, % 0.43/0.60 ( hBOOL(hAPP(hAPP(c_Type_Otyping(V_env),c_Lambda_OdB_OAbs(V_t)),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U))) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(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.43/0.60 % 0.43/0.60 cnf(cls_True_0,axiom, % 0.43/0.60 v_n____ = v_i____ ). % 0.43/0.60 % 0.43/0.60 cnf(cls_typing__elims_I1_J_0,axiom, % 0.43/0.60 ( hAPP(V_e,V_i) = V_T % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e),c_Lambda_OdB_OVar(V_i)),V_T)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_varT_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(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.43/0.60 % 0.43/0.60 cnf(cls_headT_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(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.43/0.60 % 0.43/0.60 cnf(cls_argsT_0,axiom, % 0.43/0.60 c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_Var_I4_J_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(c_Type_Otyping(v_ea______),v_ua______),v_T____)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_listsp_ONil_0,axiom, % 0.43/0.60 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__in__listsp__conv_1,axiom, % 0.43/0.60 ( c_List_Olistsp(V_A,V_ys,T_a) % 0.43/0.60 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_append__in__listsp__conv_0,axiom, % 0.43/0.60 ( c_List_Olistsp(V_A,V_xs,T_a) % 0.43/0.60 | ~ c_List_Olistsp(V_A,c_List_Oappend(V_xs,V_ys,T_a),T_a) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_nT_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(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.43/0.60 % 0.43/0.60 cnf(cls_COMBB__def_0,axiom, % 0.43/0.60 hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_typing_OVar_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(c_Type_Otyping(V_env),c_Lambda_OdB_OVar(V_x)),hAPP(V_env,V_x))) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_subst__lemma_0,axiom, % 0.43/0.60 ( ~ hBOOL(hAPP(hAPP(c_Type_Otyping(V_e_H),V_u),V_U)) % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_Type_Otyping(c_Type_Oshift(V_e_H,V_i,V_U,tc_Type_Otype)),V_t),V_T)) % 0.43/0.60 | hBOOL(hAPP(hAPP(c_Type_Otyping(V_e_H),c_Lambda_Osubst(V_t,V_u,V_i)),V_T)) ) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_CHAINED_0,axiom, % 0.43/0.60 c_Type_Otypings(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_as____,v_Ts____) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_conjecture_0,negated_conjecture, % 0.43/0.60 ~ c_List_Olistsp(c_COMBB(c_Ex(tc_Type_Otype),c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype)),tc_fun(tc_Type_Otype,tc_bool),tc_bool,tc_Lambda_OdB),v_as____,tc_Lambda_OdB) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_fun__Lattices_Olower__semilattice,axiom, % 0.43/0.60 ( class_Lattices_Olower__semilattice(tc_fun(T_2,T_1)) % 0.43/0.60 | ~ class_Lattices_Olattice(T_1) ) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.43/0.60 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.43/0.60 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_fun__Lattices_Olattice,axiom, % 0.43/0.60 ( class_Lattices_Olattice(tc_fun(T_2,T_1)) % 0.43/0.60 | ~ class_Lattices_Olattice(T_1) ) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.43/0.60 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.43/0.60 | ~ class_Orderings_Oorder(T_1) ) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.43/0.60 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.43/0.60 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.43/0.60 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.43/0.60 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.43/0.60 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.43/0.60 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.43/0.60 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.43/0.60 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.43/0.60 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Osemigroup__add,axiom, % 0.43/0.60 class_OrderedGroup_Osemigroup__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Lattices_Olower__semilattice,axiom, % 0.43/0.60 class_Lattices_Olower__semilattice(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.43/0.60 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.43/0.60 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.43/0.60 class_Nat_Osemiring__char__0(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.43/0.60 class_Orderings_Opreorder(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.43/0.60 class_Orderings_Olinorder(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Lattices_Olattice,axiom, % 0.43/0.60 class_Lattices_Olattice(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.43/0.60 class_Orderings_Oorder(tc_nat) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_bool__Lattices_Olower__semilattice,axiom, % 0.43/0.60 class_Lattices_Olower__semilattice(tc_bool) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_bool__Orderings_Opreorder,axiom, % 0.43/0.60 class_Orderings_Opreorder(tc_bool) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_bool__Lattices_Olattice,axiom, % 0.43/0.60 class_Lattices_Olattice(tc_bool) ). % 0.43/0.60 % 0.43/0.60 cnf(clsarity_bool__Orderings_Oorder,axiom, % 0.43/0.60 class_Orderings_Oorder(tc_bool) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_ATP__Linkup_OCOMBC__def_0,axiom, % 0.43/0.60 c_COMBC(V_P,V_Q,V_R,T_b,T_c,T_a) = hAPP(hAPP(V_P,V_R),V_Q) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_ATP__Linkup_OCOMBB__def_0,axiom, % 0.43/0.60 hAPP(c_COMBB(V_P,V_Q,T_b,T_a,T_c),V_R) = hAPP(V_P,hAPP(V_Q,V_R)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.43/0.60 hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)) ). % 0.43/0.60 % 0.43/0.60 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.43/0.60 ( V_X = V_Y % 0.43/0.60 | ~ hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y)) ) ). % 0.43/0.60 % 0.43/0.60 %------------------------------------------------------------------------------ % 0.43/0.60 %------------------------------------------- % 0.43/0.60 % Proof found % 0.43/0.60 % SZS status Theorem for theBenchmark % 0.43/0.60 % SZS output start Proof % 0.43/0.60 %ClaNum:457(EqnAxiom:129) % 0.43/0.60 %VarNum:1942(SingletonVarNum:845) % 0.43/0.60 %MaxLitNum:6 % 0.43/0.60 %MaxfuncDepth:5 % 0.43/0.60 %SharedTerms:99 % 0.43/0.60 %goalClause: 240 % 0.43/0.60 %singleGoalClaCount:1 % 0.43/0.60 [130]E(a1,a51) % 0.43/0.60 [131]P1(a2) % 0.43/0.60 [132]P13(a2) % 0.43/0.60 [133]P14(a2) % 0.43/0.60 [134]P15(a2) % 0.43/0.60 [135]P16(a2) % 0.43/0.60 [136]P2(a2) % 0.43/0.60 [137]P19(a2) % 0.43/0.60 [138]P3(a2) % 0.43/0.60 [139]P20(a2) % 0.43/0.60 [140]P21(a2) % 0.43/0.60 [141]P26(a2) % 0.43/0.60 [142]P22(a2) % 0.43/0.60 [143]P29(a2) % 0.43/0.60 [144]P4(a2) % 0.43/0.60 [145]P4(a3) % 0.43/0.60 [146]P5(a2) % 0.43/0.60 [147]P5(a3) % 0.43/0.60 [148]P23(a2) % 0.43/0.60 [149]P23(a3) % 0.43/0.60 [150]P25(a2) % 0.43/0.60 [151]P25(a3) % 0.43/0.60 [152]P24(a2) % 0.43/0.60 [153]P30(f9(a4,a53)) % 0.43/0.60 [154]P30(f9(a4,a55)) % 0.43/0.60 [157]E(f15(a42,a48,a39),a54) % 0.43/0.60 [196]P9(f31(a50,a1,a43,a40),a48,a47) % 0.43/0.60 [204]E(f9(f9(a32,a44),f22(a32,a47,a45,a40,a40)),a43) % 0.43/0.60 [213]P30(f9(f9(f30(f31(a50,a1,a43,a40)),f9(f9(a12,f11(a51)),a42)),f22(a32,a47,a45,a40,a40))) % 0.43/0.60 [240]~P6(f6(f7(a40),f30(f31(a50,a1,a43,a40)),f41(a40,a3),a3,a39),a48,a39) % 0.43/0.60 [171]P30(f9(f9(f30(a49),a55),a43)) % 0.43/0.60 [172]P30(f9(f9(f30(a50),a53),a43)) % 0.43/0.60 [214]P30(f9(f9(f30(a50),a53),f9(f9(a32,a44),f22(a32,a47,a45,a40,a40)))) % 0.43/0.60 [217]P30(f9(f9(f30(f31(a50,a1,a43,a40)),f11(a51)),f9(f9(a32,a44),f22(a32,a47,a45,a40,a40)))) % 0.43/0.60 [210]P30(f9(f9(f30(f31(a50,a1,a43,a40)),a42),a44)) % 0.43/0.60 [215]P30(f9(f9(f30(f31(a49,a52,a43,a40)),f21(a12,f11(a51),a54,a39,a39)),a46)) % 0.43/0.60 [216]P30(f9(f9(f30(f31(a50,a1,a43,a40)),f21(a12,f11(a51),a54,a39,a39)),a45)) % 0.43/0.60 [225]~P7(x2251,x2251,a2) % 0.43/0.60 [229]~P7(x2291,f5(a2),a2) % 0.43/0.60 [155]E(f23(f10(x1551),f38(x1551)),f5(a2)) % 0.43/0.60 [156]P30(f9(a4,f11(x1561))) % 0.43/0.60 [166]E(f27(f29(x1661),x1661,x1661),f29(x1661)) % 0.43/0.61 [235]~P7(f5(a2),f23(f10(x2351),f38(x2351)),a2) % 0.43/0.61 [159]P6(x1591,f10(x1592),x1592) % 0.43/0.61 [219]~E(f11(x2191),f14(x2192)) % 0.43/0.61 [158]E(f26(f26(x1581,x1582),x1582),f26(x1581,x1582)) % 0.43/0.61 [163]E(f16(x1631,f10(x1632),x1632),x1631) % 0.43/0.61 [164]E(f16(f10(x1641),x1642,x1641),x1642) % 0.43/0.61 [165]E(f17(f11(x1651),x1652,x1651),x1652) % 0.43/0.61 [169]E(f19(x1691,x1691,f41(x1692,a3)),x1691) % 0.43/0.61 [176]P30(f9(f9(f30(x1761),f11(x1762)),f9(x1761,x1762))) % 0.43/0.61 [173]P30(f9(f9(f29(x1731),x1732),x1732)) % 0.43/0.61 [197]P30(f9(f9(a13,f9(f9(a12,f14(x1971)),x1972)),f17(x1971,x1972,f5(a2)))) % 0.43/0.61 [234]~P30(f9(f9(a13,f11(x2341)),x2342)) % 0.43/0.61 [227]~E(f15(x2271,x2272,x2273),x2272) % 0.43/0.61 [232]~E(f15(x2321,x2322,x2323),f10(x2323)) % 0.43/0.61 [236]~P8(x2361,x2362,f10(x2363),x2363) % 0.43/0.61 [237]~P8(x2371,f10(x2372),x2373,x2372) % 0.43/0.61 [170]E(f17(f18(x1701,x1702),x1703,x1702),x1701) % 0.43/0.61 [174]E(f19(x1741,x1742,f41(x1743,a3)),f19(x1742,x1741,f41(x1743,a3))) % 0.43/0.61 [175]E(f27(f27(x1751,x1752,x1753),x1753,x1752),x1751) % 0.43/0.61 [182]E(f19(x1821,f19(x1821,x1822,f41(x1823,a3)),f41(x1823,a3)),f19(x1821,x1822,f41(x1823,a3))) % 0.43/0.61 [220]~E(f14(x2201),f9(f9(a12,x2202),x2203)) % 0.43/0.61 [221]~E(f11(x2211),f9(f9(a12,x2212),x2213)) % 0.43/0.61 [222]~E(f9(f9(a12,x2221),x2222),f14(x2223)) % 0.43/0.61 [223]~E(f9(f9(a12,x2231),x2232),f11(x2233)) % 0.43/0.61 [178]P30(f9(f9(f26(x1781,x1782),x1783),x1783)) % 0.43/0.61 [179]E(f9(f9(a12,f18(x1791,x1792)),f18(x1793,x1792)),f18(f9(f9(a12,x1791),x1793),x1792)) % 0.43/0.61 [188]E(f15(x1881,f16(x1882,x1883,x1884),x1884),f16(f15(x1881,x1882,x1884),x1883,x1884)) % 0.43/0.61 [190]E(f16(f16(x1901,x1902,x1903),x1904,x1903),f16(x1901,f16(x1902,x1904,x1903),x1903)) % 0.43/0.61 [191]E(f19(x1911,f19(x1912,x1913,f41(x1914,a3)),f41(x1914,a3)),f19(x1912,f19(x1911,x1913,f41(x1914,a3)),f41(x1914,a3))) % 0.43/0.61 [192]E(f19(f19(x1921,x1922,f41(x1923,a3)),x1924,f41(x1923,a3)),f19(x1921,f19(x1922,x1924,f41(x1923,a3)),f41(x1923,a3))) % 0.43/0.61 [194]E(f9(f31(x1941,x1942,x1943,x1944),x1942),x1943) % 0.43/0.61 [198]E(f21(x1981,x1982,f10(x1983),x1984,x1983),x1982) % 0.43/0.61 [199]E(f22(x1991,f10(x1992),x1993,x1992,x1994),x1993) % 0.43/0.61 [239]~E(f21(a12,f11(x2391),x2392,a39,a39),f21(a12,f14(x2393),x2394,a39,a39)) % 0.43/0.61 [193]E(f9(f9(a12,f17(x1931,x1932,x1933)),f17(x1934,x1932,x1933)),f17(f9(f9(a12,x1931),x1934),x1932,x1933)) % 0.43/0.61 [238]~E(f9(f9(a12,f14(x2381)),x2382),f21(a12,f11(x2383),x2384,a39,a39)) % 0.43/0.61 [206]E(f9(f6(x2061,x2062,x2063,x2064,x2065),x2066),f9(x2061,f9(x2062,x2066))) % 0.43/0.61 [208]E(f28(x2081,f28(x2082,x2083,x2084,x2085),x2085,x2086),f28(f6(x2081,x2082,x2085,x2086,x2084),x2083,x2084,x2086)) % 0.43/0.61 [209]E(f22(x2091,f15(x2092,x2093,x2094),x2095,x2094,x2096),f9(f9(x2091,x2092),f22(x2091,x2093,x2095,x2094,x2096))) % 0.43/0.61 [211]E(f21(x2111,f21(x2111,x2112,x2113,x2114,x2115),x2116,x2114,x2115),f21(x2111,x2112,f16(x2113,x2116,x2115),x2114,x2115)) % 0.43/0.61 [212]E(f22(x2121,x2122,f22(x2121,x2123,x2124,x2125,x2126),x2125,x2126),f22(x2121,f16(x2122,x2123,x2125),x2124,x2125,x2126)) % 0.43/0.61 [207]E(f21(x2071,x2072,f15(x2073,x2074,x2075),x2076,x2075),f21(x2071,f9(f9(x2071,x2072),x2073),x2074,x2076,x2075)) % 0.43/0.61 [250]E(x2501,f5(a2))+P7(f5(a2),x2501,a2) % 0.43/0.61 [313]P11(f27(a13,a39,a39),x3131,a39)+~P30(f9(a4,x3131)) % 0.43/0.61 [326]~P11(f27(a13,a39,a39),x3261,a39)+P30(f9(a4,x3261)) % 0.43/0.61 [243]~P29(x2431)+E(f24(f5(a2),x2431),f5(x2431)) % 0.43/0.61 [260]~P17(x2601)+E(f9(f9(f8(x2601),f5(x2601)),f5(x2601)),f5(x2601)) % 0.43/0.61 [261]~P30(f9(a4,x2611))+P30(f9(a4,f14(x2611))) % 0.43/0.61 [266]~P7(x2662,x2662,x2661)+~P23(x2661) % 0.43/0.61 [267]~P7(x2672,x2672,x2671)+~P25(x2671) % 0.43/0.61 [268]~P7(x2682,x2682,x2681)+~P24(x2681) % 0.43/0.61 [241]E(x2411,x2412)+~E(f14(x2411),f14(x2412)) % 0.43/0.61 [242]E(x2421,x2422)+~E(f11(x2421),f11(x2422)) % 0.43/0.61 [244]~P5(x2442)+P4(f41(x2441,x2442)) % 0.43/0.61 [245]~P5(x2452)+P5(f41(x2451,x2452)) % 0.43/0.61 [246]~P23(x2462)+P23(f41(x2461,x2462)) % 0.43/0.61 [247]~P25(x2472)+P25(f41(x2471,x2472)) % 0.43/0.61 [251]~P4(x2512)+E(f19(x2511,x2511,x2512),x2511) % 0.43/0.61 [296]~P26(x2961)+~P7(f24(x2962,x2961),f5(x2961),x2961) % 0.43/0.61 [248]E(x2481,f10(x2482))+~E(f23(x2481,f38(x2482)),f5(a2)) % 0.43/0.61 [252]~P14(x2521)+E(f9(f9(f8(x2521),x2522),f5(x2521)),x2522) % 0.43/0.61 [253]~P15(x2531)+E(f9(f9(f8(x2531),x2532),f5(x2531)),x2532) % 0.43/0.61 [254]~P16(x2541)+E(f9(f9(f8(x2541),x2542),f5(x2541)),x2542) % 0.43/0.61 [273]E(x2731,f10(x2732))+P7(f5(a2),f23(x2731,f38(x2732)),a2) % 0.43/0.61 [276]~P7(x2761,x2762,a2)+E(f18(f11(x2761),x2762),f11(x2761)) % 0.43/0.61 [295]~P30(f9(a4,x2951))+P30(f9(a4,f18(x2951,x2952))) % 0.43/0.61 [320]~P30(f9(f9(a13,x3201),x3202))+P30(f9(f9(a13,f14(x3201)),f14(x3202))) % 0.43/0.61 [424]~P16(x4241)+E(f22(f8(x4241),x4242,f5(x4241),x4241,x4241),f21(f8(x4241),f5(x4241),x4242,x4241,x4241)) % 0.43/0.61 [256]~P14(x2561)+E(f9(f9(f8(x2561),f5(x2561)),x2562),x2562) % 0.43/0.61 [257]~P15(x2571)+E(f9(f9(f8(x2571),f5(x2571)),x2572),x2572) % 0.43/0.61 [258]~P16(x2581)+E(f9(f9(f8(x2581),f5(x2581)),x2582),x2582) % 0.43/0.61 [323]~P30(f9(a4,x3231))+P30(f9(a4,f9(f9(a12,x3231),f11(x3232)))) % 0.43/0.61 [370]P30(f9(f9(f26(a13,a39),f14(x3701)),f14(x3702)))+~P30(f9(f9(f26(a13,a39),x3701),x3702)) % 0.43/0.61 [436]~P6(a4,x4362,a39)+P30(f9(a4,f21(a12,f11(x4361),x4362,a39,a39))) % 0.43/0.61 [264]~E(f16(x2643,x2641,x2642),x2643)+E(x2641,f10(x2642)) % 0.43/0.61 [265]~E(f16(x2651,x2653,x2652),x2653)+E(x2651,f10(x2652)) % 0.43/0.61 [271]~E(f16(x2713,x2711,x2712),f10(x2712))+E(x2711,f10(x2712)) % 0.43/0.61 [272]~E(f16(x2721,x2723,x2722),f10(x2722))+E(x2721,f10(x2722)) % 0.43/0.61 [283]~P4(x2833)+E(f19(x2831,x2832,x2833),f19(x2832,x2831,x2833)) % 0.43/0.61 [284]~P5(x2843)+E(f19(x2841,x2842,x2843),f19(x2842,x2841,x2843)) % 0.43/0.61 [416]~E(f14(x4162),f21(a12,x4163,x4161,a39,a39))+E(x4161,f10(a39)) % 0.43/0.61 [417]~E(f11(x4172),f21(a12,x4173,x4171,a39,a39))+E(x4171,f10(a39)) % 0.43/0.61 [418]~E(f21(a12,x4182,x4181,a39,a39),f14(x4183))+E(x4181,f10(a39)) % 0.43/0.61 [419]E(x4191,f14(x4192))+~E(f21(a12,x4191,x4193,a39,a39),f14(x4192)) % 0.43/0.61 [420]E(f14(x4201),x4202)+~E(f14(x4201),f21(a12,x4202,x4203,a39,a39)) % 0.43/0.61 [421]E(f11(x4211),x4212)+~E(f11(x4211),f21(a12,x4212,x4213,a39,a39)) % 0.43/0.61 [428]E(x4281,x4282)+~E(f21(a12,x4281,x4283,a39,a39),f21(a12,x4282,x4283,a39,a39)) % 0.43/0.61 [297]~P7(x2971,x2973,a2)+E(f17(f11(x2971),x2972,x2973),f11(x2971)) % 0.43/0.61 [317]~P4(x3173)+E(f19(x3171,f19(x3171,x3172,x3173),x3173),f19(x3171,x3172,x3173)) % 0.43/0.61 [318]~P5(x3183)+E(f19(x3181,f19(x3181,x3182,x3183),x3183),f19(x3181,x3182,x3183)) % 0.43/0.61 [348]~P30(f9(f9(a13,x3481),x3483))+P30(f9(f9(a13,f18(x3481,x3482)),f18(x3483,x3482))) % 0.43/0.61 [368]P6(x3681,x3682,x3683)+~P30(f9(x3681,f25(x3681,x3682,x3683))) % 0.43/0.61 [422]E(f9(f9(a12,x4221),x4222),x4223)+~E(f9(f9(a12,x4221),x4222),f21(a12,x4223,f10(a39),a39,a39)) % 0.43/0.61 [423]~P2(x4231)+E(f22(f8(x4231),x4232,x4233,x4231,x4231),f21(f8(x4231),x4233,x4232,x4231,x4231)) % 0.43/0.61 [425]~P9(x4251,x4252,x4253)+P6(f6(f7(a40),f30(x4251),f41(a40,a3),a3,a39),x4252,a39) % 0.43/0.61 [443]~P30(f9(f9(a13,x4431),x4433))+P30(f9(f9(a13,f21(a12,x4431,x4432,a39,a39)),f21(a12,x4433,x4432,a39,a39))) % 0.43/0.61 [445]~P8(a13,x4452,x4453,a39)+P30(f9(f9(a13,f21(a12,x4451,x4452,a39,a39)),f21(a12,x4451,x4453,a39,a39))) % 0.43/0.61 [280]~P14(x2801)+E(f9(f9(f8(x2801),x2802),x2803),f9(f9(f8(x2801),x2803),x2802)) % 0.43/0.61 [281]~P15(x2811)+E(f9(f9(f8(x2811),x2812),x2813),f9(f9(f8(x2811),x2813),x2812)) % 0.43/0.61 [298]E(x2981,x2982)+~P30(f9(f9(f29(x2983),x2981),x2982)) % 0.43/0.61 [316]E(f9(x3161,x3162),x3163)+~P30(f9(f9(f30(x3161),f11(x3162)),x3163)) % 0.43/0.61 [332]~P30(f9(a4,x3321))+P30(f9(a4,f17(x3321,f11(x3322),x3323))) % 0.43/0.61 [381]P30(f9(f9(f26(a13,a39),f18(x3811,x3812)),f18(x3813,x3812)))+~P30(f9(f9(f26(a13,a39),x3811),x3813)) % 0.43/0.61 [386]~P30(f9(f9(a13,x3861),x3863))+P30(f9(f9(a13,f9(f9(a12,x3861),x3862)),f9(f9(a12,x3863),x3862))) % 0.43/0.61 [387]~P30(f9(f9(a13,x3872),x3873))+P30(f9(f9(a13,f9(f9(a12,x3871),x3872)),f9(f9(a12,x3871),x3873))) % 0.43/0.61 [395]~P30(f9(f9(f26(a13,a39),x3951),x3953))+P30(f9(f9(f26(a13,a39),f9(f9(a12,x3951),x3952)),f9(f9(a12,x3953),x3952))) % 0.43/0.61 [396]~P30(f9(f9(f26(a13,a39),x3962),x3963))+P30(f9(f9(f26(a13,a39),f9(f9(a12,x3961),x3962)),f9(f9(a12,x3961),x3963))) % 0.43/0.61 [426]~P16(x4261)+E(f9(f9(f8(x4261),x4262),f22(f8(x4261),x4263,f5(x4261),x4261,x4261)),f21(f8(x4261),x4262,x4263,x4261,x4261)) % 0.43/0.61 [427]~P16(x4271)+E(f9(f9(f8(x4271),x4272),f21(f8(x4271),f5(x4271),x4273,x4271,x4271)),f21(f8(x4271),x4272,x4273,x4271,x4271)) % 0.43/0.61 [444]P30(f9(f9(f26(a13,a39),f21(a12,x4441,x4442,a39,a39)),f21(a12,x4443,x4442,a39,a39)))+~P30(f9(f9(f26(a13,a39),x4441),x4443)) % 0.43/0.61 [446]P8(a13,x4461,f20(x4462,x4461,x4463),a39)+~P30(f9(f9(a13,f21(a12,f11(x4462),x4461,a39,a39)),x4463)) % 0.43/0.61 [450]E(f21(a12,f11(x4501),f20(x4501,x4502,x4503),a39,a39),x4503)+~P30(f9(f9(a13,f21(a12,f11(x4501),x4502,a39,a39)),x4503)) % 0.43/0.61 [300]E(x3001,x3002)+~E(f16(x3003,x3001,x3004),f16(x3003,x3002,x3004)) % 0.43/0.61 [302]E(x3021,x3022)+~E(f16(x3021,x3023,x3024),f16(x3022,x3023,x3024)) % 0.43/0.61 [333]P6(x3331,x3332,x3333)+~P6(x3331,f16(x3334,x3332,x3333),x3333) % 0.43/0.61 [334]P6(x3341,x3342,x3343)+~P6(x3341,f16(x3342,x3344,x3343),x3343) % 0.43/0.61 [285]E(x2851,x2852)+~E(f9(f9(a12,x2853),x2851),f9(f9(a12,x2854),x2852)) % 0.43/0.61 [286]E(x2861,x2862)+~E(f9(f9(a32,x2863),x2861),f9(f9(a32,x2864),x2862)) % 0.43/0.61 [287]E(x2871,x2872)+~E(f9(f9(a12,x2871),x2873),f9(f9(a12,x2872),x2874)) % 0.43/0.61 [288]E(x2881,x2882)+~E(f9(f9(a32,x2881),x2883),f9(f9(a32,x2882),x2884)) % 0.43/0.61 [342]~P4(x3424)+E(f19(x3421,f19(x3422,x3423,x3424),x3424),f19(x3422,f19(x3421,x3423,x3424),x3424)) % 0.43/0.61 [343]~P5(x3434)+E(f19(x3431,f19(x3432,x3433,x3434),x3434),f19(x3432,f19(x3431,x3433,x3434),x3434)) % 0.43/0.61 [344]~P4(x3443)+E(f19(f19(x3441,x3442,x3443),x3444,x3443),f19(x3441,f19(x3442,x3444,x3443),x3443)) % 0.43/0.61 [345]~P5(x3453)+E(f19(f19(x3451,x3452,x3453),x3454,x3453),f19(x3451,f19(x3452,x3454,x3453),x3453)) % 0.43/0.61 [394]~P30(f9(f9(a13,x3941),x3944))+P30(f9(f9(a13,f17(x3941,x3942,x3943)),f17(x3944,x3942,x3943))) % 0.43/0.61 [402]P30(f9(f9(f26(a13,a39),f17(x4021,x4022,x4023)),f17(x4021,x4024,x4023)))+~P30(f9(f9(a13,x4022),x4024)) % 0.43/0.61 [430]E(x4301,x4302)+~E(f21(a12,f14(x4303),x4301,a39,a39),f21(a12,f14(x4304),x4302,a39,a39)) % 0.43/0.61 [431]E(x4311,x4312)+~E(f21(a12,f11(x4313),x4311,a39,a39),f21(a12,f11(x4314),x4312,a39,a39)) % 0.43/0.61 [432]E(x4321,x4322)+~E(f21(a12,f14(x4321),x4323,a39,a39),f21(a12,f14(x4322),x4324,a39,a39)) % 0.43/0.61 [433]E(x4331,x4332)+~E(f21(a12,f11(x4331),x4333,a39,a39),f21(a12,f11(x4332),x4334,a39,a39)) % 0.43/0.61 [335]~P30(f9(f9(x3351,x3353),x3354))+P30(f9(f9(f26(x3351,x3352),x3353),x3354)) % 0.43/0.61 [379]P30(f9(x3791,x3792))+~P30(f9(f19(x3793,x3791,f41(x3794,a3)),x3792)) % 0.43/0.61 [380]P30(f9(x3801,x3802))+~P30(f9(f19(x3801,x3803,f41(x3804,a3)),x3802)) % 0.43/0.61 [406]P30(f9(f9(f26(a13,a39),f17(x4061,x4062,x4063)),f17(x4064,x4062,x4063)))+~P30(f9(f9(f26(a13,a39),x4061),x4064)) % 0.43/0.61 [407]P30(f9(f9(f26(a13,a39),f17(x4071,x4072,x4073)),f17(x4071,x4074,x4073)))+~P30(f9(f9(f26(a13,a39),x4072),x4074)) % 0.43/0.61 [447]P9(x4471,x4472,f34(x4473,x4471,x4474,x4472))+~P30(f9(f9(f30(x4471),f21(a12,x4474,x4472,a39,a39)),x4473)) % 0.43/0.61 [448]P9(x4481,x4482,f35(x4483,x4481,x4484,x4482))+~P30(f9(f9(f30(x4481),f21(a12,x4484,x4482,a39,a39)),x4483)) % 0.43/0.61 [452]~P30(f9(f9(f30(x4521),f21(a12,x4522,x4524,a39,a39)),x4523))+P30(f9(f9(f30(x4521),x4522),f22(a32,f34(x4523,x4521,x4522,x4524),x4523,a40,a40))) % 0.43/0.61 [453]~P30(f9(f9(f30(x4531),f21(a12,x4532,x4534,a39,a39)),x4533))+P30(f9(f9(f30(x4531),x4532),f22(a32,f35(x4533,x4531,x4532,x4534),x4533,a40,a40))) % 0.43/0.61 [336]~P14(x3361)+E(f9(f9(f8(x3361),x3362),f9(f9(f8(x3361),x3363),x3364)),f9(f9(f8(x3361),x3363),f9(f9(f8(x3361),x3362),x3364))) % 0.43/0.61 [337]~P15(x3371)+E(f9(f9(f8(x3371),x3372),f9(f9(f8(x3371),x3373),x3374)),f9(f9(f8(x3371),x3373),f9(f9(f8(x3371),x3372),x3374))) % 0.43/0.61 [338]~P12(x3381)+E(f9(f9(f8(x3381),x3382),f9(f9(f8(x3381),x3383),x3384)),f9(f9(f8(x3381),x3383),f9(f9(f8(x3381),x3382),x3384))) % 0.43/0.61 [363]~P17(x3631)+E(f19(f9(f9(f8(x3631),x3632),x3633),f9(f9(f8(x3631),x3632),x3634),x3631),f9(f9(f8(x3631),x3632),f19(x3633,x3634,x3631))) % 0.43/0.61 [364]~P18(x3641)+E(f19(f9(f9(f8(x3641),x3642),x3643),f9(f9(f8(x3641),x3642),x3644),x3641),f9(f9(f8(x3641),x3642),f19(x3643,x3644,x3641))) % 0.43/0.61 [375]~P17(x3751)+E(f19(f9(f9(f8(x3751),x3752),x3753),f9(f9(f8(x3751),x3754),x3753),x3751),f9(f9(f8(x3751),f19(x3752,x3754,x3751)),x3753)) % 0.43/0.61 [376]~P18(x3761)+E(f19(f9(f9(f8(x3761),x3762),x3763),f9(f9(f8(x3761),x3764),x3763),x3761),f9(f9(f8(x3761),f19(x3762,x3764,x3761)),x3763)) % 0.43/0.61 [409]~P30(f9(f9(f26(x4091,x4092),x4094),x4093))+P30(f9(f9(f26(f27(x4091,x4092,x4092),x4092),x4093),x4094)) % 0.43/0.61 [412]P30(f9(f9(f30(x4121),x4122),f33(x4123,x4121,x4124,x4122)))+~P30(f9(f9(f30(x4121),f9(f9(a12,x4124),x4122)),x4123)) % 0.43/0.61 [415]P30(f9(f9(f26(x4151,x4152),x4153),x4154))+~P30(f9(f9(f26(f27(x4151,x4152,x4152),x4152),x4154),x4153)) % 0.43/0.61 [429]~P19(x4291)+E(f21(f8(x4291),f9(f9(f8(x4291),x4292),x4293),x4294,x4291,x4291),f9(f9(f8(x4291),x4292),f21(f8(x4291),x4293,x4294,x4291,x4291))) % 0.43/0.61 [435]~P30(f9(f9(f30(x4351),f9(f9(a12,x4352),x4354)),x4353))+P30(f9(f9(f30(x4351),x4352),f9(f9(a32,f33(x4353,x4351,x4352,x4354)),x4353))) % 0.43/0.61 [449]P9(x4491,x4492,f36(x4493,x4491,x4494,x4492))+~P30(f9(f9(f30(x4491),f21(a12,f11(x4494),x4492,a39,a39)),x4493)) % 0.43/0.61 [454]P30(f9(f9(f30(x4541),f11(x4542)),f22(a32,f36(x4543,x4541,x4542,x4544),x4543,a40,a40)))+~P30(f9(f9(f30(x4541),f21(a12,f11(x4542),x4544,a39,a39)),x4543)) % 0.43/0.61 [360]~P14(x3601)+E(f9(f9(f8(x3601),f9(f9(f8(x3601),x3602),x3603)),x3604),f9(f9(f8(x3601),x3602),f9(f9(f8(x3601),x3603),x3604))) % 0.43/0.61 [361]~P15(x3611)+E(f9(f9(f8(x3611),f9(f9(f8(x3611),x3612),x3613)),x3614),f9(f9(f8(x3611),x3612),f9(f9(f8(x3611),x3613),x3614))) % 0.43/0.61 [362]~P2(x3621)+E(f9(f9(f8(x3621),f9(f9(f8(x3621),x3622),x3623)),x3624),f9(f9(f8(x3621),x3622),f9(f9(f8(x3621),x3623),x3624))) % 0.43/0.61 [373]~P14(x3731)+E(f9(f9(f8(x3731),f9(f9(f8(x3731),x3732),x3733)),x3734),f9(f9(f8(x3731),f9(f9(f8(x3731),x3732),x3734)),x3733)) % 0.43/0.61 [437]P30(f9(f9(f30(x4371),f14(x4372)),f9(f9(a32,x4373),x4374)))+~P30(f9(f9(f30(f31(x4371,f5(a2),x4373,a40)),x4372),x4374)) % 0.43/0.61 [299]E(x2991,x2992)+~E(f15(x2993,x2991,x2994),f15(x2995,x2992,x2994)) % 0.43/0.61 [301]E(x3011,x3012)+~E(f15(x3011,x3013,x3014),f15(x3012,x3015,x3014)) % 0.43/0.61 [397]~P8(x3971,x3973,x3975,x3974)+P8(x3971,f15(x3972,x3973,x3974),f15(x3972,x3975,x3974),x3974) % 0.43/0.61 [398]~P8(x3981,x3982,x3985,x3984)+P8(x3981,f16(x3982,x3983,x3984),f16(x3985,x3983,x3984),x3984) % 0.43/0.61 [399]~P8(x3991,x3993,x3995,x3994)+P8(x3991,f16(x3992,x3993,x3994),f16(x3992,x3995,x3994),x3994) % 0.43/0.61 [382]P8(x3821,f15(x3822,x3823,x3824),f15(x3825,x3823,x3824),x3824)+~P30(f9(f9(x3821,x3822),x3825)) % 0.43/0.61 [383]~P7(x3835,x3832,a2)+E(f9(f31(x3831,x3832,x3833,x3834),x3835),f9(x3831,x3835)) % 0.43/0.61 [377]E(x3771,x3772)+~E(f16(x3773,f15(x3771,f10(x3774),x3774),x3774),f16(x3775,f15(x3772,f10(x3774),x3774),x3774)) % 0.43/0.61 [378]E(x3781,x3782)+~E(f16(x3781,f15(x3783,f10(x3784),x3784),x3784),f16(x3782,f15(x3785,f10(x3784),x3784),x3784)) % 0.43/0.61 [389]~P30(f9(f9(x3891,x3895),x3894))+P30(f9(f9(f27(x3891,x3892,x3893),x3894),x3895)) % 0.43/0.61 [401]P30(f9(f9(x4011,x4012),x4013))+~P30(f9(f9(f27(x4011,x4014,x4015),x4013),x4012)) % 0.43/0.61 [434]~P30(f9(f9(f30(x4341),x4344),x4345))+P30(f9(f9(f30(f31(x4341,x4342,x4343,a40)),f18(x4344,x4342)),x4345)) % 0.43/0.61 [390]~P14(x3901)+E(f9(f9(f8(x3901),f9(f9(f8(x3901),x3902),x3903)),f9(f9(f8(x3901),x3904),x3905)),f9(f9(f8(x3901),f9(f9(f8(x3901),x3902),x3904)),f9(f9(f8(x3901),x3903),x3905))) % 0.43/0.61 [278]E(x2781,x2782)+P7(x2782,x2781,a2)+P7(x2781,x2782,a2) % 0.43/0.61 [311]~P26(x3111)+P7(f5(x3111),f24(x3112,x3111),x3111)+~P7(f5(a2),x3112,a2) % 0.43/0.61 [315]~P26(x3152)+~P7(f5(x3152),f24(x3151,x3152),x3152)+P7(f5(a2),x3151,a2) % 0.43/0.61 [259]~P27(x2591)+~P10(x2591)+E(f9(f9(f8(x2591),x2592),f5(x2591)),x2592) % 0.43/0.61 [274]~P17(x2742)+E(x2741,f5(x2742))+~E(f9(f9(f8(x2742),x2741),x2741),f5(x2742)) % 0.43/0.61 [327]~P17(x3271)+~P7(f5(x3271),x3272,x3271)+P7(f5(x3271),f9(f9(f8(x3271),x3272),x3272),x3271) % 0.43/0.61 [328]~P17(x3281)+~P7(x3282,f5(x3281),x3281)+P7(f9(f9(f8(x3281),x3282),x3282),f5(x3281),x3281) % 0.43/0.61 [329]~P28(x3291)+~P7(x3292,f5(x3291),x3291)+P7(f9(f9(f8(x3291),x3292),x3292),f5(x3291),x3291) % 0.43/0.61 [339]~P17(x3392)+P7(x3391,f5(x3392),x3392)+~P7(f9(f9(f8(x3392),x3391),x3391),f5(x3392),x3392) % 0.43/0.61 [340]~P28(x3402)+P7(x3401,f5(x3402),x3402)+~P7(f9(f9(f8(x3402),x3401),x3401),f5(x3402),x3402) % 0.43/0.61 [341]~P17(x3411)+P7(f5(x3411),x3412,x3411)+~P7(f5(x3411),f9(f9(f8(x3411),x3412),x3412),x3411) % 0.43/0.61 [306]~P7(x3063,x3062,x3061)+~P23(x3061)+~P7(x3062,x3063,x3061) % 0.43/0.61 [308]~P7(x3083,x3082,x3081)+~P25(x3081)+~P7(x3082,x3083,x3081) % 0.43/0.61 [309]~P7(x3093,x3092,x3091)+~P24(x3091)+~P7(x3092,x3093,x3091) % 0.43/0.61 [249]~P3(x2493)+E(x2491,x2492)+~E(f24(x2491,x2493),f24(x2492,x2493)) % 0.43/0.61 [314]~P26(x3142)+~P7(x3141,x3143,a2)+P7(f24(x3141,x3142),f24(x3143,x3142),x3142) % 0.43/0.61 [319]~P26(x3193)+~P7(f24(x3191,x3193),f24(x3192,x3193),x3193)+P7(x3191,x3192,a2) % 0.43/0.61 [294]E(x2941,x2942)+P7(x2942,x2941,a2)+E(f17(f11(x2941),x2943,x2942),f11(x2941)) % 0.43/0.61 [441]~P11(f27(a13,a39,a39),x4412,a39)+~P11(f27(a13,a39,a39),f21(a12,f17(x4411,x4412,f5(a2)),x4413,a39,a39),a39)+P11(f27(a13,a39,a39),f21(a12,f9(f9(a12,f14(x4411)),x4412),x4413,a39,a39),a39) % 0.43/0.61 [442]~P30(f9(a4,x4422))+~P30(f9(a4,f21(a12,f17(x4421,x4422,f5(a2)),x4423,a39,a39)))+P30(f9(a4,f21(a12,f9(f9(a12,f14(x4421)),x4422),x4423,a39,a39))) % 0.43/0.61 [324]~P4(x3243)+~P7(x3242,x3244,x3243)+P7(f19(x3241,x3242,x3243),x3244,x3243) % 0.43/0.61 [325]~P4(x3253)+~P7(x3251,x3254,x3253)+P7(f19(x3251,x3252,x3253),x3254,x3253) % 0.43/0.61 [346]~P6(x3461,x3463,x3464)+~P6(x3461,x3462,x3464)+P6(x3461,f16(x3462,x3463,x3464),x3464) % 0.43/0.61 [331]P11(x3311,x3312,x3313)+~P11(x3311,x3314,x3313)+~P30(f9(f9(x3311,x3312),x3314)) % 0.43/0.61 [355]~P6(x3552,x3554,x3553)+~P6(x3551,x3554,x3553)+P6(f19(x3551,x3552,f41(x3553,a3)),x3554,x3553) % 0.43/0.61 [303]~P1(x3033)+E(x3031,x3032)+~E(f9(f9(f8(x3033),x3034),x3031),f9(f9(f8(x3033),x3034),x3032)) % 0.43/0.61 [304]~P13(x3043)+E(x3041,x3042)+~E(f9(f9(f8(x3043),x3044),x3041),f9(f9(f8(x3043),x3044),x3042)) % 0.43/0.61 [305]~P13(x3053)+E(x3051,x3052)+~E(f9(f9(f8(x3053),x3051),x3054),f9(f9(f8(x3053),x3052),x3054)) % 0.43/0.61 [349]~P20(x3491)+~P7(x3492,x3494,x3491)+P7(f9(f9(f8(x3491),x3492),x3493),f9(f9(f8(x3491),x3494),x3493),x3491) % 0.43/0.61 [350]~P21(x3501)+~P7(x3502,x3504,x3501)+P7(f9(f9(f8(x3501),x3502),x3503),f9(f9(f8(x3501),x3504),x3503),x3501) % 0.43/0.61 [351]~P20(x3511)+~P7(x3513,x3514,x3511)+P7(f9(f9(f8(x3511),x3512),x3513),f9(f9(f8(x3511),x3512),x3514),x3511) % 0.43/0.61 [352]~P21(x3521)+~P7(x3523,x3524,x3521)+P7(f9(f9(f8(x3521),x3522),x3523),f9(f9(f8(x3521),x3522),x3524),x3521) % 0.43/0.61 [357]~P30(f9(f9(a13,x3574),x3572))+~P30(f9(f9(f30(x3571),x3574),x3573))+P30(f9(f9(f30(x3571),x3572),x3573)) % 0.43/0.61 [365]~P30(f9(x3652,x3654))+~P30(f9(x3651,x3654))+P30(f9(f19(x3651,x3652,f41(x3653,a3)),x3654)) % 0.43/0.61 [367]P11(x3671,x3672,x3673)+~P11(x3671,x3674,x3673)+~P30(f9(f9(f26(x3671,x3673),x3672),x3674)) % 0.43/0.61 [371]~P21(x3713)+P7(x3711,x3712,x3713)+~P7(f9(f9(f8(x3713),x3714),x3711),f9(f9(f8(x3713),x3714),x3712),x3713) % 0.43/0.61 [372]~P21(x3723)+P7(x3721,x3722,x3723)+~P7(f9(f9(f8(x3723),x3721),x3724),f9(f9(f8(x3723),x3722),x3724),x3723) % 0.43/0.61 [374]P30(f9(f9(f30(x3741),x3742),x3743))+~P30(f9(f9(f30(x3741),x3744),x3743))+~P30(f9(f9(f26(a13,a39),x3744),x3742)) % 0.43/0.61 [408]~P30(f9(f9(f26(a13,a39),x4081),x4083))+~P30(f9(f9(f26(a13,a39),x4082),x4084))+P30(f9(f9(f26(a13,a39),f9(f9(a12,x4081),x4082)),f9(f9(a12,x4083),x4084))) % 0.43/0.61 [384]~P30(f9(f9(x3841,x3845),x3844))+~P30(f9(f9(f26(x3841,x3842),x3843),x3845))+P30(f9(f9(f26(x3841,x3842),x3843),x3844)) % 0.43/0.61 [385]~P30(f9(f9(x3851,x3853),x3855))+~P30(f9(f9(f26(x3851,x3852),x3855),x3854))+P30(f9(f9(f26(x3851,x3852),x3853),x3854)) % 0.43/0.61 [392]~P30(f9(f9(f26(x3921,x3922),x3923),x3925))+P30(f9(f9(f26(x3921,x3922),x3923),x3924))+~P30(f9(f9(f26(x3921,x3922),x3925),x3924)) % 0.43/0.61 [451]~P9(x4511,x4513,x4515)+~P30(f9(f9(f30(x4511),x4512),f22(a32,x4515,x4514,a40,a40)))+P30(f9(f9(f30(x4511),f21(a12,x4512,x4513,a39,a39)),x4514)) % 0.43/0.61 [356]~P12(x3561)+E(f9(f9(f8(x3561),x3562),x3563),x3564)+~E(f9(f9(f8(x3561),x3562),f9(f9(f8(x3561),x3565),x3563)),f9(f9(f8(x3561),x3565),x3564)) % 0.43/0.61 [403]~P30(f9(f9(f30(x4031),x4033),x4035))+~P30(f9(f9(f30(x4031),x4032),f9(f9(a32,x4035),x4034)))+P30(f9(f9(f30(x4031),f9(f9(a12,x4032),x4033)),x4034)) % 0.43/0.61 [455]E(x4551,x4552)+~P30(f9(f9(f30(x4553),f21(a12,f11(x4554),x4555,a39,a39)),x4551))+~P30(f9(f9(f30(x4553),f21(a12,f11(x4554),x4555,a39,a39)),x4552)) % 0.43/0.61 [391]E(x3911,x3912)+E(x3913,x3914)+~P8(x3915,f15(x3914,x3912,x3916),f15(x3913,x3911,x3916),x3916) % 0.43/0.61 [404]E(x4041,x4042)+P8(x4043,x4041,x4042,x4044)+~P8(x4043,f15(x4045,x4041,x4044),f15(x4046,x4042,x4044),x4044) % 0.43/0.61 [393]E(x3931,x3932)+~P8(x3933,f15(x3932,x3934,x3935),f15(x3931,x3936,x3935),x3935)+P30(f9(f9(x3933,x3932),x3931)) % 0.43/0.61 [405]P8(x4051,x4052,x4053,x4054)+~P8(x4051,f15(x4055,x4052,x4054),f15(x4056,x4053,x4054),x4054)+P30(f9(f9(x4051,x4055),x4056)) % 0.43/0.61 [410]E(x4101,x4102)+E(x4103,x4104)+~P8(x4105,f16(x4103,f15(x4101,f10(x4106),x4106),x4106),f16(x4104,f15(x4102,f10(x4106),x4106),x4106),x4106) % 0.43/0.61 [411]E(x4111,x4112)+~P8(x4113,f16(x4114,f15(x4111,f10(x4115),x4115),x4115),f16(x4116,f15(x4112,f10(x4115),x4115),x4115),x4115)+P30(f9(f9(x4113,x4111),x4112)) % 0.43/0.61 [413]E(x4131,x4132)+P8(x4133,x4131,x4132,x4134)+~P8(x4133,f16(x4131,f15(x4135,f10(x4134),x4134),x4134),f16(x4132,f15(x4136,f10(x4134),x4134),x4134),x4134) % 0.43/0.61 [414]P8(x4141,x4142,x4143,x4144)+~P8(x4141,f16(x4142,f15(x4145,f10(x4144),x4144),x4144),f16(x4143,f15(x4146,f10(x4144),x4144),x4144),x4144)+P30(f9(f9(x4141,x4145),x4146)) % 0.43/0.61 [440]P30(f9(f9(f30(x4401),f17(x4402,x4403,x4404)),x4405))+~P30(f9(f9(f30(x4401),x4403),x4406))+~P30(f9(f9(f30(f31(x4401,x4404,x4406,a40)),x4402),x4405)) % 0.43/0.61 [289]P7(x2891,x2892,x2893)+~P28(x2893)+E(x2891,x2892)+P7(x2892,x2891,x2893) % 0.43/0.61 [293]P7(x2931,x2932,x2933)+~P24(x2933)+E(x2931,x2932)+P7(x2932,x2931,x2933) % 0.43/0.61 [275]~P27(x2752)+~P10(x2752)+E(x2751,f5(x2752))+~E(f9(f9(f8(x2752),x2753),x2751),x2753) % 0.43/0.61 [353]~P22(x3531)+~P7(f5(x3531),x3533,x3531)+~P7(f5(x3531),x3532,x3531)+P7(f5(x3531),f9(f9(f8(x3531),x3532),x3533),x3531) % 0.43/0.61 [354]~P22(x3541)+~P7(x3543,f5(x3541),x3541)+~P7(x3542,f5(x3541),x3541)+P7(f9(f9(f8(x3541),x3542),x3543),f5(x3541),x3541) % 0.43/0.61 [321]~P23(x3213)+~P7(x3211,x3214,x3213)+P7(x3211,x3212,x3213)+~P7(x3214,x3212,x3213) % 0.43/0.61 [322]~P25(x3223)+~P7(x3221,x3224,x3223)+P7(x3221,x3222,x3223)+~P7(x3224,x3222,x3223) % 0.43/0.61 [310]~P27(x3103)+~P10(x3103)+E(x3101,x3102)+~E(f9(f9(f8(x3103),x3104),x3101),f9(f9(f8(x3103),x3104),x3102)) % 0.43/0.61 [347]~P26(x3472)+~P7(x3471,x3474,x3472)+~P7(f5(x3472),x3473,x3472)+P7(x3471,f9(f9(f8(x3472),x3473),x3474),x3472) % 0.43/0.61 [369]~P20(x3691)+~P7(x3693,x3695,x3691)+~P7(x3692,x3694,x3691)+P7(f9(f9(f8(x3691),x3692),x3693),f9(f9(f8(x3691),x3694),x3695),x3691) % 0.43/0.61 [456]~P9(x4561,x4565,x4566)+P9(x4561,x4562,f37(x4563,x4564,x4561,x4562))+~P30(f9(f9(f30(x4561),f21(a12,f11(x4567),x4565,a39,a39)),x4564))+~P30(f9(f9(f30(x4561),f21(a12,f21(a12,f11(x4567),x4565,a39,a39),x4562,a39,a39)),x4563)) % 0.43/0.61 [457]~P9(x4573,x4575,x4576)+E(f22(a32,f37(x4571,x4572,x4573,x4574),x4571,a40,a40),x4572)+~P30(f9(f9(f30(x4573),f21(a12,f11(x4577),x4575,a39,a39)),x4572))+~P30(f9(f9(f30(x4573),f21(a12,f21(a12,f11(x4577),x4575,a39,a39),x4574,a39,a39)),x4571)) % 0.43/0.61 [438]~P30(f9(a4,x4382))+~P30(f9(a4,x4381))+~E(f9(f9(a32,x4384),x4385),a43)+P30(f9(a4,f17(x4381,x4382,x4383)))+~P30(f9(f9(f30(x4386),x4382),x4385))+~P30(f9(f9(f30(f31(x4386,x4383,x4385,a40)),x4381),x4387)) % 0.43/0.61 [439]~P30(f9(a4,x4392))+~P30(f9(a4,x4391))+~E(f9(f9(a32,x4394),x4395),a43)+P30(f9(a4,f17(x4391,x4392,x4393)))+~P30(f9(f9(f30(x4396),x4392),x4394))+~P30(f9(f9(f30(f31(x4396,x4393,x4394,a40)),x4391),x4397)) % 0.43/0.61 %EqnAxiom % 0.43/0.61 [1]E(x11,x11) % 0.43/0.61 [2]E(x22,x21)+~E(x21,x22) % 0.43/0.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.43/0.61 [4]~E(x41,x42)+E(f9(x41,x43),f9(x42,x43)) % 0.43/0.61 [5]~E(x51,x52)+E(f9(x53,x51),f9(x53,x52)) % 0.43/0.61 [6]~E(x61,x62)+E(f21(x61,x63,x64,x65,x66),f21(x62,x63,x64,x65,x66)) % 0.43/0.61 [7]~E(x71,x72)+E(f21(x73,x71,x74,x75,x76),f21(x73,x72,x74,x75,x76)) % 0.43/0.61 [8]~E(x81,x82)+E(f21(x83,x84,x81,x85,x86),f21(x83,x84,x82,x85,x86)) % 0.43/0.61 [9]~E(x91,x92)+E(f21(x93,x94,x95,x91,x96),f21(x93,x94,x95,x92,x96)) % 0.43/0.61 [10]~E(x101,x102)+E(f21(x103,x104,x105,x106,x101),f21(x103,x104,x105,x106,x102)) % 0.43/0.61 [11]~E(x111,x112)+E(f10(x111),f10(x112)) % 0.43/0.61 [12]~E(x121,x122)+E(f38(x121),f38(x122)) % 0.43/0.61 [13]~E(x131,x132)+E(f23(x131,x133),f23(x132,x133)) % 0.43/0.61 [14]~E(x141,x142)+E(f23(x143,x141),f23(x143,x142)) % 0.43/0.61 [15]~E(x151,x152)+E(f5(x151),f5(x152)) % 0.43/0.61 [16]~E(x161,x162)+E(f11(x161),f11(x162)) % 0.43/0.61 [17]~E(x171,x172)+E(f14(x171),f14(x172)) % 0.43/0.61 [18]~E(x181,x182)+E(f15(x181,x183,x184),f15(x182,x183,x184)) % 0.43/0.61 [19]~E(x191,x192)+E(f15(x193,x191,x194),f15(x193,x192,x194)) % 0.43/0.61 [20]~E(x201,x202)+E(f15(x203,x204,x201),f15(x203,x204,x202)) % 0.43/0.61 [21]~E(x211,x212)+E(f26(x211,x213),f26(x212,x213)) % 0.43/0.61 [22]~E(x221,x222)+E(f26(x223,x221),f26(x223,x222)) % 0.43/0.61 [23]~E(x231,x232)+E(f27(x231,x233,x234),f27(x232,x233,x234)) % 0.43/0.61 [24]~E(x241,x242)+E(f27(x243,x241,x244),f27(x243,x242,x244)) % 0.43/0.61 [25]~E(x251,x252)+E(f27(x253,x254,x251),f27(x253,x254,x252)) % 0.43/0.61 [26]~E(x261,x262)+E(f8(x261),f8(x262)) % 0.43/0.61 [27]~E(x271,x272)+E(f29(x271),f29(x272)) % 0.43/0.61 [28]~E(x281,x282)+E(f16(x281,x283,x284),f16(x282,x283,x284)) % 0.43/0.61 [29]~E(x291,x292)+E(f16(x293,x291,x294),f16(x293,x292,x294)) % 0.43/0.61 [30]~E(x301,x302)+E(f16(x303,x304,x301),f16(x303,x304,x302)) % 0.43/0.61 [31]~E(x311,x312)+E(f19(x311,x313,x314),f19(x312,x313,x314)) % 0.43/0.61 [32]~E(x321,x322)+E(f19(x323,x321,x324),f19(x323,x322,x324)) % 0.43/0.61 [33]~E(x331,x332)+E(f19(x333,x334,x331),f19(x333,x334,x332)) % 0.43/0.61 [34]~E(x341,x342)+E(f41(x341,x343),f41(x342,x343)) % 0.43/0.61 [35]~E(x351,x352)+E(f41(x353,x351),f41(x353,x352)) % 0.43/0.61 [36]~E(x361,x362)+E(f30(x361),f30(x362)) % 0.43/0.61 [37]~E(x371,x372)+E(f22(x371,x373,x374,x375,x376),f22(x372,x373,x374,x375,x376)) % 0.43/0.61 [38]~E(x381,x382)+E(f22(x383,x381,x384,x385,x386),f22(x383,x382,x384,x385,x386)) % 0.43/0.61 [39]~E(x391,x392)+E(f22(x393,x394,x391,x395,x396),f22(x393,x394,x392,x395,x396)) % 0.43/0.61 [40]~E(x401,x402)+E(f22(x403,x404,x405,x401,x406),f22(x403,x404,x405,x402,x406)) % 0.43/0.61 [41]~E(x411,x412)+E(f22(x413,x414,x415,x416,x411),f22(x413,x414,x415,x416,x412)) % 0.43/0.61 [42]~E(x421,x422)+E(f17(x421,x423,x424),f17(x422,x423,x424)) % 0.43/0.61 [43]~E(x431,x432)+E(f17(x433,x431,x434),f17(x433,x432,x434)) % 0.43/0.61 [44]~E(x441,x442)+E(f17(x443,x444,x441),f17(x443,x444,x442)) % 0.43/0.61 [45]~E(x451,x452)+E(f24(x451,x453),f24(x452,x453)) % 0.43/0.61 [46]~E(x461,x462)+E(f24(x463,x461),f24(x463,x462)) % 0.43/0.61 [47]~E(x471,x472)+E(f31(x471,x473,x474,x475),f31(x472,x473,x474,x475)) % 0.43/0.61 [48]~E(x481,x482)+E(f31(x483,x481,x484,x485),f31(x483,x482,x484,x485)) % 0.43/0.61 [49]~E(x491,x492)+E(f31(x493,x494,x491,x495),f31(x493,x494,x492,x495)) % 0.43/0.61 [50]~E(x501,x502)+E(f31(x503,x504,x505,x501),f31(x503,x504,x505,x502)) % 0.43/0.61 [51]~E(x511,x512)+E(f18(x511,x513),f18(x512,x513)) % 0.43/0.61 [52]~E(x521,x522)+E(f18(x523,x521),f18(x523,x522)) % 0.43/0.61 [53]~E(x531,x532)+E(f36(x531,x533,x534,x535),f36(x532,x533,x534,x535)) % 0.43/0.61 [54]~E(x541,x542)+E(f36(x543,x541,x544,x545),f36(x543,x542,x544,x545)) % 0.43/0.61 [55]~E(x551,x552)+E(f36(x553,x554,x551,x555),f36(x553,x554,x552,x555)) % 0.43/0.61 [56]~E(x561,x562)+E(f36(x563,x564,x565,x561),f36(x563,x564,x565,x562)) % 0.43/0.61 [57]~E(x571,x572)+E(f37(x571,x573,x574,x575),f37(x572,x573,x574,x575)) % 0.43/0.61 [58]~E(x581,x582)+E(f37(x583,x581,x584,x585),f37(x583,x582,x584,x585)) % 0.43/0.61 [59]~E(x591,x592)+E(f37(x593,x594,x591,x595),f37(x593,x594,x592,x595)) % 0.43/0.61 [60]~E(x601,x602)+E(f37(x603,x604,x605,x601),f37(x603,x604,x605,x602)) % 0.43/0.61 [61]~E(x611,x612)+E(f28(x611,x613,x614,x615),f28(x612,x613,x614,x615)) % 0.43/0.61 [62]~E(x621,x622)+E(f28(x623,x621,x624,x625),f28(x623,x622,x624,x625)) % 0.43/0.61 [63]~E(x631,x632)+E(f28(x633,x634,x631,x635),f28(x633,x634,x632,x635)) % 0.43/0.61 [64]~E(x641,x642)+E(f28(x643,x644,x645,x641),f28(x643,x644,x645,x642)) % 0.43/0.61 [65]~E(x651,x652)+E(f34(x651,x653,x654,x655),f34(x652,x653,x654,x655)) % 0.43/0.61 [66]~E(x661,x662)+E(f34(x663,x661,x664,x665),f34(x663,x662,x664,x665)) % 0.43/0.61 [67]~E(x671,x672)+E(f34(x673,x674,x671,x675),f34(x673,x674,x672,x675)) % 0.43/0.61 [68]~E(x681,x682)+E(f34(x683,x684,x685,x681),f34(x683,x684,x685,x682)) % 0.43/0.61 [69]~E(x691,x692)+E(f33(x691,x693,x694,x695),f33(x692,x693,x694,x695)) % 0.43/0.61 [70]~E(x701,x702)+E(f33(x703,x701,x704,x705),f33(x703,x702,x704,x705)) % 0.43/0.61 [71]~E(x711,x712)+E(f33(x713,x714,x711,x715),f33(x713,x714,x712,x715)) % 0.43/0.61 [72]~E(x721,x722)+E(f33(x723,x724,x725,x721),f33(x723,x724,x725,x722)) % 0.43/0.61 [73]~E(x731,x732)+E(f25(x731,x733,x734),f25(x732,x733,x734)) % 0.43/0.61 [74]~E(x741,x742)+E(f25(x743,x741,x744),f25(x743,x742,x744)) % 0.43/0.61 [75]~E(x751,x752)+E(f25(x753,x754,x751),f25(x753,x754,x752)) % 0.43/0.61 [76]~E(x761,x762)+E(f7(x761),f7(x762)) % 0.43/0.61 [77]~E(x771,x772)+E(f6(x771,x773,x774,x775,x776),f6(x772,x773,x774,x775,x776)) % 0.43/0.61 [78]~E(x781,x782)+E(f6(x783,x781,x784,x785,x786),f6(x783,x782,x784,x785,x786)) % 0.43/0.61 [79]~E(x791,x792)+E(f6(x793,x794,x791,x795,x796),f6(x793,x794,x792,x795,x796)) % 0.43/0.61 [80]~E(x801,x802)+E(f6(x803,x804,x805,x801,x806),f6(x803,x804,x805,x802,x806)) % 0.43/0.61 [81]~E(x811,x812)+E(f6(x813,x814,x815,x816,x811),f6(x813,x814,x815,x816,x812)) % 0.43/0.61 [82]~E(x821,x822)+E(f35(x821,x823,x824,x825),f35(x822,x823,x824,x825)) % 0.43/0.61 [83]~E(x831,x832)+E(f35(x833,x831,x834,x835),f35(x833,x832,x834,x835)) % 0.43/0.61 [84]~E(x841,x842)+E(f35(x843,x844,x841,x845),f35(x843,x844,x842,x845)) % 0.43/0.61 [85]~E(x851,x852)+E(f35(x853,x854,x855,x851),f35(x853,x854,x855,x852)) % 0.43/0.61 [86]~E(x861,x862)+E(f20(x861,x863,x864),f20(x862,x863,x864)) % 0.43/0.61 [87]~E(x871,x872)+E(f20(x873,x871,x874),f20(x873,x872,x874)) % 0.43/0.61 [88]~E(x881,x882)+E(f20(x883,x884,x881),f20(x883,x884,x882)) % 0.43/0.61 [89]~P1(x891)+P1(x892)+~E(x891,x892) % 0.43/0.61 [90]~P13(x901)+P13(x902)+~E(x901,x902) % 0.43/0.61 [91]~P14(x911)+P14(x912)+~E(x911,x912) % 0.43/0.61 [92]~P15(x921)+P15(x922)+~E(x921,x922) % 0.43/0.61 [93]~P16(x931)+P16(x932)+~E(x931,x932) % 0.43/0.61 [94]~P2(x941)+P2(x942)+~E(x941,x942) % 0.43/0.61 [95]~P19(x951)+P19(x952)+~E(x951,x952) % 0.43/0.61 [96]~P3(x961)+P3(x962)+~E(x961,x962) % 0.43/0.61 [97]~P20(x971)+P20(x972)+~E(x971,x972) % 0.43/0.61 [98]~P21(x981)+P21(x982)+~E(x981,x982) % 0.43/0.61 [99]~P26(x991)+P26(x992)+~E(x991,x992) % 0.43/0.61 [100]~P22(x1001)+P22(x1002)+~E(x1001,x1002) % 0.43/0.61 [101]~P29(x1011)+P29(x1012)+~E(x1011,x1012) % 0.43/0.61 [102]~P4(x1021)+P4(x1022)+~E(x1021,x1022) % 0.43/0.61 [103]~P30(x1031)+P30(x1032)+~E(x1031,x1032) % 0.43/0.61 [104]~P5(x1041)+P5(x1042)+~E(x1041,x1042) % 0.43/0.61 [105]P7(x1052,x1053,x1054)+~E(x1051,x1052)+~P7(x1051,x1053,x1054) % 0.43/0.61 [106]P7(x1063,x1062,x1064)+~E(x1061,x1062)+~P7(x1063,x1061,x1064) % 0.43/0.61 [107]P7(x1073,x1074,x1072)+~E(x1071,x1072)+~P7(x1073,x1074,x1071) % 0.43/0.61 [108]~P23(x1081)+P23(x1082)+~E(x1081,x1082) % 0.43/0.61 [109]P9(x1092,x1093,x1094)+~E(x1091,x1092)+~P9(x1091,x1093,x1094) % 0.43/0.61 [110]P9(x1103,x1102,x1104)+~E(x1101,x1102)+~P9(x1103,x1101,x1104) % 0.43/0.61 [111]P9(x1113,x1114,x1112)+~E(x1111,x1112)+~P9(x1113,x1114,x1111) % 0.43/0.61 [112]~P25(x1121)+P25(x1122)+~E(x1121,x1122) % 0.43/0.61 [113]P11(x1132,x1133,x1134)+~E(x1131,x1132)+~P11(x1131,x1133,x1134) % 0.43/0.61 [114]P11(x1143,x1142,x1144)+~E(x1141,x1142)+~P11(x1143,x1141,x1144) % 0.43/0.61 [115]P11(x1153,x1154,x1152)+~E(x1151,x1152)+~P11(x1153,x1154,x1151) % 0.43/0.61 [116]~P24(x1161)+P24(x1162)+~E(x1161,x1162) % 0.43/0.61 [117]P6(x1172,x1173,x1174)+~E(x1171,x1172)+~P6(x1171,x1173,x1174) % 0.43/0.61 [118]P6(x1183,x1182,x1184)+~E(x1181,x1182)+~P6(x1183,x1181,x1184) % 0.43/0.61 [119]P6(x1193,x1194,x1192)+~E(x1191,x1192)+~P6(x1193,x1194,x1191) % 0.43/0.61 [120]P8(x1202,x1203,x1204,x1205)+~E(x1201,x1202)+~P8(x1201,x1203,x1204,x1205) % 0.43/0.61 [121]P8(x1213,x1212,x1214,x1215)+~E(x1211,x1212)+~P8(x1213,x1211,x1214,x1215) % 0.43/0.61 [122]P8(x1223,x1224,x1222,x1225)+~E(x1221,x1222)+~P8(x1223,x1224,x1221,x1225) % 0.43/0.61 [123]P8(x1233,x1234,x1235,x1232)+~E(x1231,x1232)+~P8(x1233,x1234,x1235,x1231) % 0.43/0.61 [124]~P27(x1241)+P27(x1242)+~E(x1241,x1242) % 0.43/0.61 [125]~P17(x1251)+P17(x1252)+~E(x1251,x1252) % 0.43/0.61 [126]~P10(x1261)+P10(x1262)+~E(x1261,x1262) % 0.43/0.61 [127]~P18(x1271)+P18(x1272)+~E(x1271,x1272) % 0.43/0.61 [128]~P12(x1281)+P12(x1282)+~E(x1281,x1282) % 0.43/0.61 [129]~P28(x1291)+P28(x1292)+~E(x1291,x1292) % 0.43/0.61 % 0.43/0.61 %------------------------------------------- % 0.43/0.61 cnf(481,plain, % 0.43/0.61 ($false), % 0.43/0.61 inference(scs_inference,[],[196,240,425]), % 0.43/0.61 ['proof']). % 0.43/0.61 % SZS output end Proof % 0.43/0.61 % Total time :0.029049s %------------------------------------------------------------------------------