%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL807-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n028.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:53 AM UTC 2026 % Result : Unsatisfiable 0.38s 0.60s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL807-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n028.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Sat Sep 5 21:45:30 UTC 2026 % 0.08/0.35 % CPUTime : % 0.13/0.46 start to proof:theBenchmark % 0.38/0.57 %------------------------------------------- % 0.38/0.57 % File :CSE---1.7 % 0.38/0.57 % Problem :theBenchmark % 0.38/0.57 % Transform :cnf % 0.38/0.57 % Format :tptp:raw % 0.38/0.57 % Command :java -jar mcs_scs.jar %d %s % 0.38/0.57 % 0.38/0.57 % Result :Theorem 0.028995s % 0.38/0.57 % Output :CNFRefutation 0.028995s % 0.38/0.57 %------------------------------------------- % 0.38/0.57 %------------------------------------------------------------------------------ % 0.38/0.58 % File : LCL807-1 : TPTP v9.3.1. Released v4.1.0. % 0.38/0.58 % Domain : Logic Calculi % 0.38/0.58 % Problem : Strong normalization of typed lambda calculus 167_57 % 0.38/0.58 % Version : Especial. % 0.38/0.58 % English : % 0.38/0.58 % 0.38/0.58 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.38/0.58 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.38/0.58 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.38/0.58 % Source : [Nip10] % 0.38/0.58 % Names : StrongNorm-167_57 [Nip10] % 0.38/0.58 % 0.38/0.58 % Status : Unsatisfiable % 0.38/0.58 % Rating : 0.17 v9.3.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.13 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.10 v6.1.0, 0.00 v5.5.0, 0.15 v5.3.0, 0.11 v5.2.0, 0.12 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0 % 0.38/0.58 % Syntax : Number of clauses : 273 ( 83 unt; 17 nHn; 173 RR) % 0.38/0.58 % Number of literals : 561 ( 156 equ; 292 neg) % 0.38/0.58 % Maximal clause size : 6 ( 2 avg) % 0.38/0.58 % Maximal term depth : 27 ( 2 avg) % 0.38/0.58 % Number of predicates : 28 ( 27 usr; 1 prp; 0-3 aty) % 0.38/0.58 % Number of functors : 66 ( 66 usr; 30 con; 0-5 aty) % 0.38/0.58 % Number of variables : 762 ( 128 sgn) % 0.38/0.58 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.38/0.58 % 0.38/0.58 % Comments : % 0.38/0.58 %------------------------------------------------------------------------------ % 0.38/0.58 cnf(cls_Cons__step1__Cons_5,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_OCons(V_x,V_ys,T_a)),c_List_Olist_OCons(V_x,V_xs,T_a))) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_ys),V_xs)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_Cons__step1__Cons_1,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_ys),V_xs)) % 0.38/0.58 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_OCons(V_y,V_ys,T_a)),c_List_Olist_OCons(V_x,V_xs,T_a))) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_list_Oinject_1,axiom, % 0.38/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.38/0.58 | V_list = V_list_H ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_list_Oinject_0,axiom, % 0.38/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.38/0.58 | V_a = V_a_H ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_foldr_Osimps_I2_J_0,axiom, % 0.38/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.38/0.58 % 0.38/0.58 cnf(cls_list_Osimps_I2_J_0,axiom, % 0.38/0.58 c_List_Olist_ONil(T_a) != c_List_Olist_OCons(V_a_H,V_list_H,T_a) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_listsum_Osimps_I2_J_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.58 | c_List_Olistsum(c_List_Olist_OCons(V_x,V_xs,T_a),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_List_Olistsum(V_xs,T_a)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_Cons__step1__Cons_3,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_ys),V_xs)) % 0.38/0.58 | V_xs = V_ys % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_OCons(V_y,V_ys,T_a)),c_List_Olist_OCons(V_x,V_xs,T_a))) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_Cons__step1__Cons_4,axiom, % 0.38/0.58 ( ~ hBOOL(hAPP(hAPP(V_r,V_y),V_xa)) % 0.38/0.58 | hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_OCons(V_y,V_x,T_a)),c_List_Olist_OCons(V_xa,V_x,T_a))) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_Cons__step1__Cons_2,axiom, % 0.38/0.58 ( V_x = V_y % 0.38/0.58 | V_xs = V_ys % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_OCons(V_y,V_ys,T_a)),c_List_Olist_OCons(V_x,V_xs,T_a))) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_foldl__Cons_0,axiom, % 0.38/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.38/0.58 % 0.38/0.58 cnf(cls_neq__Nil__conv_1,axiom, % 0.38/0.58 c_List_Olist_OCons(V_x,V_xa,T_a) != c_List_Olist_ONil(T_a) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_list_Osimps_I3_J_0,axiom, % 0.38/0.58 c_List_Olist_OCons(V_a_H,V_list_H,T_a) != c_List_Olist_ONil(T_a) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_Cons__step1__Cons_0,axiom, % 0.38/0.58 ( V_x = V_y % 0.38/0.58 | hBOOL(hAPP(hAPP(V_r,V_y),V_x)) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_OCons(V_y,V_ys,T_a)),c_List_Olist_OCons(V_x,V_xs,T_a))) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_not__Cons__self2_0,axiom, % 0.38/0.58 c_List_Olist_OCons(V_x,V_t,T_a) != V_t ). % 0.38/0.58 % 0.38/0.58 cnf(cls_not__Cons__self_0,axiom, % 0.38/0.58 V_xs != c_List_Olist_OCons(V_x,V_xs,T_a) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_length__greater__0__conv_1,axiom, % 0.38/0.58 ( 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.38/0.58 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_listsum_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.58 | c_List_Olistsum(V_xs,T_a) = c_List_Ofoldl(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a),V_xs,T_a,T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_Cons__acc__step1I_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(V_r,T_a),tc_List_Olist(T_a)),c_List_Olist_OCons(V_x,V_xs,T_a))) % 0.38/0.58 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(V_r,T_a),tc_List_Olist(T_a)),V_xs)) % 0.38/0.58 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_x)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_listsum_Osimps_I1_J_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.58 | c_List_Olistsum(c_List_Olist_ONil(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_length__0__conv_1,axiom, % 0.38/0.58 c_Nat_Osize__class_Osize(c_List_Olist_ONil(T_a),tc_List_Olist(T_a)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_length__0__conv_0,axiom, % 0.38/0.58 ( c_Nat_Osize__class_Osize(V_xs,tc_List_Olist(T_a)) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.38/0.58 | V_xs = c_List_Olist_ONil(T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_length__greater__0__conv_0,axiom, % 0.38/0.58 ~ 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.38/0.58 % 0.38/0.58 cnf(cls_listsum__foldr_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.58 | c_List_Olistsum(V_xs,T_a) = c_List_Ofoldr(c_HOL_Oplus__class_Oplus(T_a),V_xs,c_HOL_Ozero__class_Ozero(T_a),T_a,T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_App__eq__foldl__conv_2,axiom, % 0.38/0.58 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB) % 0.38/0.58 | V_r = c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_ListApplication_Osko__ListApplication__XApp__eq__foldl__conv__1__1(V_r,V_s,V_t,V_ts),tc_Lambda_OdB,tc_Lambda_OdB) % 0.38/0.58 | V_ts = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_lists__accI_0,axiom, % 0.38/0.58 ( c_List_Olistsp(c_Wellfounded_Oaccp(V_r,T_a),V_xs,T_a) % 0.38/0.58 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(V_r,T_a),tc_List_Olist(T_a)),V_xs)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_lists__accD_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_ListOrder_Ostep1(V_r,T_a),tc_List_Olist(T_a)),V_xs)) % 0.38/0.58 | ~ c_List_Olistsp(c_Wellfounded_Oaccp(V_r,T_a),V_xs,T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_foldr__conv__foldl_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.38/0.58 | 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.38/0.58 % 0.38/0.58 cnf(cls_lift__preserves__beta_H_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(c_Lambda_Olift,V_r),V_i)),hAPP(hAPP(c_Lambda_Olift,V_s),V_i))) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_subject__reduction_H_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_t_H),V_T)) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_t),V_T)) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_typing__elims_I2_J_1,axiom, % 0.38/0.58 ( hBOOL(hAPP(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.38/0.58 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u)),V_T)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_head__Var__reduction_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(c_Lambda_Obeta,tc_Lambda_OdB),V_rs),c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(V_n,V_rs,V_v))) % 0.38/0.58 | ~ 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.38/0.58 % 0.38/0.58 cnf(cls_subst__preserves__beta2_H_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_r),V_i)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),V_i))) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_subst__preserves__beta_H_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),V_t),V_i)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_s),V_t),V_i))) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_subst__preserves__beta2_0,axiom, % 0.38/0.58 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_r),V_i)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),V_i))) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.38/0.58 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.38/0.58 % 0.38/0.58 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.38/0.58 ( 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.38/0.58 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_rtrancl__beta__Abs_0,axiom, % 0.38/0.58 ( 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.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_rtrancl__beta__AppR_0,axiom, % 0.38/0.58 ( 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.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_rtrancl__beta__AppL_0,axiom, % 0.38/0.58 ( 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.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_rtrancl__beta__App_0,axiom, % 0.38/0.58 ( 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.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) % 0.38/0.58 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_foldl__absorb0_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.58 | 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.38/0.58 % 0.38/0.58 cnf(cls_of__nat__less__iff_0,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.38/0.58 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.38/0.58 | ~ 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.38/0.58 % 0.38/0.58 cnf(cls_of__nat__less__iff_1,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.38/0.58 | 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.38/0.58 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_of__nat__0_0,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.38/0.58 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_pos__add__strict_0,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.38/0.58 | c_HOL_Oord__class_Oless(V_b,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),T_a) % 0.38/0.58 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.38/0.58 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_add__pos__pos_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.38/0.58 | 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.38/0.58 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.38/0.58 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_even__less__0__iff_1,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.38/0.58 | 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.38/0.58 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_even__less__0__iff_0,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.38/0.58 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.38/0.58 | ~ 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.38/0.58 % 0.38/0.58 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.38/0.58 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.38/0.58 | ~ 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.38/0.58 % 0.38/0.58 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.38/0.58 | 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.38/0.58 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_add__neg__neg_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.38/0.58 | 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.38/0.58 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.38/0.58 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.38/0.58 % 0.38/0.58 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.38/0.58 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.38/0.58 | ~ 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.38/0.58 % 0.38/0.58 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.38/0.58 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.38/0.58 | ~ 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.38/0.58 % 0.38/0.58 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.38/0.58 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.38/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.38/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_accp__downward_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_a)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) % 0.38/0.59 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_b)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_accp_Ocases_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_y)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_y),V_a)) % 0.38/0.59 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_a)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_c)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_b)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_converse__rtranclp__into__rtranclp_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_c)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_ab__semigroup__add_Oadd__commute_0,axiom, % 0.38/0.59 ( hAPP(hAPP(V_plus,V_a),V_b) = hAPP(hAPP(V_plus,V_b),V_a) % 0.38/0.59 | ~ c_OrderedGroup_Oab__semigroup__add(V_plus,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_ab__semigroup__add_Oadd__left__commute_0,axiom, % 0.38/0.59 ( hAPP(hAPP(V_plus,V_a),hAPP(hAPP(V_plus,V_b),V_c)) = hAPP(hAPP(V_plus,V_b),hAPP(hAPP(V_plus,V_a),V_c)) % 0.38/0.59 | ~ c_OrderedGroup_Oab__semigroup__add(V_plus,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_ab__semigroup__add_Oadd__ac_I1_J_0,axiom, % 0.38/0.59 ( hAPP(hAPP(V_plus,hAPP(hAPP(V_plus,V_a),V_b)),V_c) = hAPP(hAPP(V_plus,V_a),hAPP(hAPP(V_plus,V_b),V_c)) % 0.38/0.59 | ~ c_OrderedGroup_Oab__semigroup__add(V_plus,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__less__cancel__left_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.38/0.59 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.38/0.59 | ~ 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.38/0.59 % 0.38/0.59 cnf(cls_add__less__cancel__left_1,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.38/0.59 | 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.38/0.59 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__strict__left__mono_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__less__cancel__right_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.38/0.59 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.38/0.59 | ~ 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.38/0.59 % 0.38/0.59 cnf(cls_add__less__cancel__right_1,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.38/0.59 | 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.38/0.59 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__strict__right__mono_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_conversep__conversep_0,axiom, % 0.38/0.59 c_Predicate_Oconversep(c_Predicate_Oconversep(V_r,T_a,T_b),T_b,T_a) = V_r ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__strict__mono_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.38/0.59 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_conversep__eq_0,axiom, % 0.38/0.59 c_Predicate_Oconversep(c_fequal(T_a),T_a,T_a) = c_fequal(T_a) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_foldl__Nil_0,axiom, % 0.38/0.59 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.38/0.59 % 0.38/0.59 cnf(cls_not__step1__Nil_0,axiom, % 0.38/0.59 ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),V_xs),c_List_Olist_ONil(T_a))) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_not__Nil__step1_0,axiom, % 0.38/0.59 ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(V_r,T_a),c_List_Olist_ONil(T_a)),V_xs)) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_r__into__rtranclp_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_double__eq__0__iff_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.38/0.59 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.38/0.59 | ~ class_Int_Onumber__ring(T_a) % 0.38/0.59 | V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_a) % 0.38/0.59 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_of__nat__eq__iff_0,axiom, % 0.38/0.59 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.38/0.59 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.38/0.59 | V_m = V_n ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_foldl__assoc_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Osemigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_termi__implies__IT_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(c_InductTermi_OIT,V_r)) % 0.38/0.59 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),V_r)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_IT__implies__termi_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),V_t)) % 0.38/0.59 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_rtranclp__trans_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_z)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_z)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_accp__downwards__aux_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_b)) % 0.38/0.59 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_a)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_accp__downwards_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_b)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) % 0.38/0.59 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(V_r,T_a),V_a)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_Nitpick_Ortranclp__def_1,axiom, % 0.38/0.59 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_x)) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_rtranclp_Ortrancl__refl_0,axiom, % 0.38/0.59 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_a)) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_listsp_ONil_0,axiom, % 0.38/0.59 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_double__eq__0__iff_1,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_add__cancel__21_1,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_conversep_Ointros_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_b),V_a)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_conversep_Ocases_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(V_r,V_a2),V_a1)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a1),V_a2)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_conversep__iff_1,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_a)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_conversepD_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(V_r,V_b),V_a)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__cancel__21_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.38/0.59 | 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.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) = V_u ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.38/0.59 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.38/0.59 % 0.38/0.59 cnf(cls_rtranclp__converseD_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_rtranclp__converseI_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.38/0.59 | ~ class_Int_Onumber__ring(T_a) % 0.38/0.59 | 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.38/0.59 | V_y = V_z ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__imp__eq_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 | V_b = V_c ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__left__cancel_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 | V_b = V_c ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__right__cancel_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.38/0.59 | 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.38/0.59 | V_b = V_c ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | 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.38/0.59 % 0.38/0.59 cnf(cls_rtranclp__idemp_0,axiom, % 0.38/0.59 c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(V_r,T_a),T_a) = c_Transitive__Closure_Ortranclp(V_r,T_a) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_x) = V_x ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.38/0.59 | ~ class_Int_Onumber__ring(T_a) % 0.38/0.59 | V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_HOL_Ozero__class_Ozero(T_a)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_add__0__left_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.38/0.59 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_ab__semigroup__add_Ofoldr__conv__foldl_0,axiom, % 0.38/0.59 ( c_List_Ofoldr(V_plus,V_xs,V_a,T_a,T_a) = c_List_Ofoldl(V_plus,V_a,V_xs,T_a,T_a) % 0.38/0.59 | ~ c_OrderedGroup_Oab__semigroup__add(V_plus,T_a) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_double__induction__lemma_0,axiom, % 0.38/0.59 ( ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),V_s),c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) % 0.38/0.59 | ~ hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB),V_s)) % 0.38/0.59 | hBOOL(hAPP(c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,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))) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_apps__preserves__betas_0,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(hAPP(c_ListOrder_Ostep1(c_Lambda_Obeta,tc_Lambda_OdB),V_rs),V_ss)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_apps__preserves__beta2_0,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.38/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.38/0.59 % 0.38/0.59 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.38/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.38/0.59 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.38/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.38/0.59 % 0.38/0.59 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.38/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.38/0.59 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.38/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.38/0.59 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.38/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.38/0.59 % 0.38/0.59 cnf(cls_foldl__foldr1__lemma_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/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.38/0.59 % 0.38/0.59 cnf(cls_foldl__foldr1_0,axiom, % 0.38/0.59 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.38/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.38/0.59 % 0.38/0.59 cnf(cls_typing__elims_I2_J_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(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.38/0.59 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u)),V_T)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.38/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.38/0.59 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.38/0.59 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.38/0.59 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.38/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.38/0.59 % 0.38/0.59 cnf(cls_head__Var__reduction_1,axiom, % 0.38/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.38/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.38/0.59 % 0.38/0.59 cnf(cls_IT_OVar_0,axiom, % 0.38/0.59 ( 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.38/0.59 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_list__app__typeE_1,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_list__app__typeD_1,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_var__app__types_1,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_var__app__typesE_1,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_list__app__typeD_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_list__app__typeE_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_Var_I2_J_0,axiom, % 0.38/0.59 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_ea______),v_ia______),v_T____)),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.38/0.59 % 0.38/0.59 cnf(cls_var__app__typesE_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_var__app__types_0,axiom, % 0.38/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.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.38/0.59 | ~ hBOOL(hAPP(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.38/0.59 % 0.38/0.59 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.38/0.59 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_abs_0,axiom, % 0.38/0.59 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.38/0.59 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.38/0.59 % 0.38/0.59 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.38/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.38/0.60 % 0.38/0.60 cnf(cls_app__Var__IT_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),c_Lambda_OdB_OVar(V_i)))) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_lift__preserves__beta_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_Olift,V_r),V_i)),hAPP(hAPP(c_Lambda_Olift,V_s),V_i))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.38/0.60 ( hAPP(hAPP(c_Lambda_Olift,c_Lambda_OdB_OVar(V_i)),V_k) = c_Lambda_OdB_OVar(V_i) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__lift_0,axiom, % 0.38/0.60 hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_Olift,V_t),V_k)),V_s),V_k) = V_t ). % 0.38/0.60 % 0.38/0.60 cnf(cls_uIT_0,axiom, % 0.38/0.60 hBOOL(hAPP(c_InductTermi_OIT,v_u____)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_appL_0,axiom, % 0.38/0.60 ( 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.38/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_appR_0,axiom, % 0.38/0.60 ( 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.38/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Lambda_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.38/0.60 ( 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.38/0.60 | V_r = V_s ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.38/0.60 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.38/0.60 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_T_0,axiom, % 0.38/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.38/0.60 % 0.38/0.60 cnf(cls_subst__Var_1,axiom, % 0.38/0.60 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.38/0.60 | hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_x)),V_s),V_x) = V_s ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_not__less0_0,axiom, % 0.38/0.60 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_gr__implies__not0_0,axiom, % 0.38/0.60 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_xt1_I10_J_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_order__less__trans_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_list__app__typeI_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(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.38/0.60 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.38/0.60 | ~ hBOOL(hAPP(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.38/0.60 % 0.38/0.60 cnf(cls_Var_I3_J_0,axiom, % 0.38/0.60 hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__Var_2,axiom, % 0.38/0.60 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_i)),V_s),V_k) = c_Lambda_OdB_OVar(V_i) % 0.38/0.60 | V_i = V_k % 0.38/0.60 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__preserves__beta_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),V_t),V_i)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_s),V_t),V_i))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.38/0.60 hAPP(hAPP(c_Lambda_Olift,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_Olift,V_s),V_k)),hAPP(hAPP(c_Lambda_Olift,V_t),V_k)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Var__IT_0,axiom, % 0.38/0.60 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.38/0.60 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Beta_0,axiom, % 0.38/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.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),V_s),c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_lift__IT_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_Olift,V_t),V_i))) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.38/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.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.38/0.60 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.38/0.60 | V_dB = V_dB_H ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.38/0.60 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.38/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.38/0.60 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_apps__preserves__beta_0,axiom, % 0.38/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.38/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_uT_H_0,axiom, % 0.38/0.60 hBOOL(hAPP(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.38/0.60 % 0.38/0.60 cnf(cls_nat__less__le_1,axiom, % 0.38/0.60 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_less__not__refl_0,axiom, % 0.38/0.60 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_order__less__le_1,axiom, % 0.38/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_linorder__neq__iff_1,axiom, % 0.38/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_order__less__irrefl_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_beta_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_s),V_t),c_HOL_Ozero__class_Ozero(tc_nat)))) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.38/0.60 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.38/0.60 | V_x = V_y ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.38/0.60 | V_x = V_y % 0.38/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_nat__neq__iff_0,axiom, % 0.38/0.60 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.38/0.60 | V_m = V_n ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_nat__less__cases_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.38/0.60 | V_m = V_n % 0.38/0.60 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_var__app__type__eq_0,axiom, % 0.38/0.60 ( V_T = V_U % 0.38/0.60 | ~ hBOOL(hAPP(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.38/0.60 | ~ hBOOL(hAPP(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.38/0.60 % 0.38/0.60 cnf(cls_linorder__neqE__nat_0,axiom, % 0.38/0.60 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.38/0.60 | V_x = V_y ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_linorder__neqE_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.38/0.60 | V_x = V_y ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_linorder__less__linear_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.38/0.60 | V_x = V_y % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.38/0.60 | V_x = V_y % 0.38/0.60 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.38/0.60 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.38/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.38/0.60 | V_dB2 = V_dB2_H ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.38/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.38/0.60 | V_dB1 = V_dB1_H ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.38/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.38/0.60 | V_rs = V_ss ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.38/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.38/0.60 | V_r = V_s ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.38/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.38/0.60 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_App_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_env),hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t)),V_U)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_env),V_t),V_T)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_env),V_s),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U))) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_beta__cases_I1_J_0,axiom, % 0.38/0.60 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_gr0I_0,axiom, % 0.38/0.60 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.38/0.60 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_neq0__conv_1,axiom, % 0.38/0.60 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__lt_0,axiom, % 0.38/0.60 ( hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_j)),V_u),V_i) = c_Lambda_OdB_OVar(V_j) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__Var__IT_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_r),c_Lambda_OdB_OVar(V_i)),V_j))) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_type_Osimps_I2_J_1,axiom, % 0.38/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.38/0.60 | V_type2 = V_type2_H ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_type_Osimps_I2_J_0,axiom, % 0.38/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.38/0.60 | V_type1 = V_type1_H ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__eq_0,axiom, % 0.38/0.60 hAPP(hAPP(hAPP(c_Lambda_Osubst,c_Lambda_OdB_OVar(V_k)),V_u),V_k) = V_u ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.38/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.38/0.60 | V_rs = V_ss ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.38/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.38/0.60 | V_m = V_n ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.38/0.60 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.38/0.60 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.38/0.60 | V_nat = V_nat_H ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.38/0.60 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.38/0.60 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__App_0,axiom, % 0.38/0.60 hAPP(hAPP(hAPP(c_Lambda_Osubst,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u)),V_s),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_s),V_k)),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_u),V_s),V_k)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_xt1_I9_J_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Oorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.38/0.60 ( ~ class_Orderings_Olinorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_order__less__asym_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_order__less__asym_H_0,axiom, % 0.38/0.60 ( ~ class_Orderings_Opreorder(T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_lift__type_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_e),V_i),V_U)),hAPP(hAPP(c_Lambda_Olift,V_t),V_i)),V_T)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_t),V_T)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_uT_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,v_e____),v_u____),v_T____)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_I_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_b____),V_ua),V_ia))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_ea),V_ua),v_T____)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_ua)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_ea),V_ia),v_T____)),v_b____),V_T_H)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Cons_I1_J_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_b____),V_u),V_ia))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_ea),V_u),v_T____)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_ea),V_ia),v_T____)),v_b____),V_T_H)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subject__reduction_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_t_H),V_T)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_t),V_T)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_shift__gt_0,axiom, % 0.38/0.60 ( hAPP(hAPP(hAPP(hAPP(c_Type_Oshift(T_a),V_e),V_i),V_T),V_j) = hAPP(V_e,V_j) % 0.38/0.60 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_argT_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),v_a____),v_T_H_H____)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_MI2_0,axiom, % 0.38/0.60 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.38/0.60 | hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_u),V_T2)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_e),V_i),V_T2)),V_t),V_Ta)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_MI1_0,axiom, % 0.38/0.60 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.38/0.60 | hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),V_u),V_T1)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_e),V_i),V_T1)),V_t),V_Ta)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_shift__eq_0,axiom, % 0.38/0.60 hAPP(hAPP(hAPP(hAPP(c_Type_Oshift(T_a),V_e),V_x),V_T),V_x) = V_T ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Abs_0,axiom, % 0.38/0.60 ( hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_env),c_Lambda_OdB_OAbs(V_t)),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_env),c_HOL_Ozero__class_Ozero(tc_nat)),V_T)),V_t),V_U)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_True_0,axiom, % 0.38/0.60 v_n____ = v_i____ ). % 0.38/0.60 % 0.38/0.60 cnf(cls_that_0,axiom, % 0.38/0.60 ( v_thesis____ % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),v_b____),V_U)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_typing__elims_I1_J_0,axiom, % 0.38/0.60 ( hAPP(V_e,V_i) = V_T % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e),c_Lambda_OdB_OVar(V_i)),V_T)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Cons_Ohyps_I1_J_1,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),v_b____),v_sko__local__XCons__Xhyps__1__1(v_T____,v_b____,v_e____,v_i____))) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_varT_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),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.38/0.60 % 0.38/0.60 cnf(cls_headT_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),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.38/0.60 % 0.38/0.60 cnf(cls_argsT_0,axiom, % 0.38/0.60 c_Type_Otypings(hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____),v_as____,v_Ts____) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_Var_I4_J_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,v_ea______),v_ua______),v_T____)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_nT_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),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.38/0.60 % 0.38/0.60 cnf(cls_Cons_I1_J_1,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),v_b____),v_sko__local__XCons__1__1(v_T____,v_b____,v_e____,v_i____))) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_typing_OVar_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_env),c_Lambda_OdB_OVar(V_x)),hAPP(V_env,V_x))) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_subst__lemma_0,axiom, % 0.38/0.60 ( ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e_H),V_u),V_U)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_e_H),V_i),V_U)),V_t),V_T)) % 0.38/0.60 | hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_e_H),hAPP(hAPP(hAPP(c_Lambda_Osubst,V_t),V_u),V_i)),V_T)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_CHAINED_0,axiom, % 0.38/0.60 c_List_Olistsp(c_InductTermi_OIT,c_List_Omap(hAPP(hAPP(c_COMBC(tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),c_Lambda_Olift),c_HOL_Ozero__class_Ozero(tc_nat)),c_List_Omap(hAPP(hAPP(c_COMBC(tc_Lambda_OdB,tc_nat,tc_Lambda_OdB),hAPP(hAPP(c_COMBC(tc_Lambda_OdB,tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),c_Lambda_Osubst),v_u____)),v_i____),v_bs____,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_CHAINED_0_01,axiom, % 0.38/0.60 c_List_Olistsp(hAPP(hAPP(c_COMBS(tc_Lambda_OdB,tc_bool,tc_bool),hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Lambda_OdB),c_and),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_bool),tc_bool,tc_Lambda_OdB),c_All(tc_fun(tc_nat,tc_Type_Otype))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_bool)),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_bool),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_bool),tc_bool,tc_fun(tc_nat,tc_Type_Otype)),c_All(tc_Type_Otype))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_bool))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_bool)),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_bool)),tc_fun(tc_Type_Otype,tc_bool),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_bool),tc_bool,tc_Type_Otype),c_All(tc_Lambda_OdB)))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_bool))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_bool)),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_bool),tc_Type_Otype),hAPP(c_COMBB(tc_fun(tc_nat,tc_bool),tc_bool,tc_Lambda_OdB),c_All(tc_nat))))),hAPP(hAPP(c_COMBS(tc_Lambda_OdB,tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),tc_fun(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),tc_Lambda_OdB),c_COMBS(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)))),tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)))),tc_fun(tc_nat,tc_Type_Otype)),c_COMBC(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool))),tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)))),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)),tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_Type_Otype),c_COMBB(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool),tc_Lambda_OdB)))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_fun(tc_bool,tc_bool)))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_fun(tc_bool,tc_bool))),tc_fun(tc_Type_Otype,tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool))),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_nat,tc_fun(tc_bool,tc_bool)),tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)),tc_Type_Otype),c_COMBS(tc_nat,tc_bool,tc_bool)))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_bool))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_fun(tc_bool,tc_bool)))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_fun(tc_bool,tc_bool))),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_fun(tc_bool,tc_bool)),tc_Type_Otype),hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_nat),c_implies)))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_nat,tc_fun(tc_Type_Otype,tc_bool))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_bool))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_nat,tc_fun(tc_Type_Otype,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_Type_Otype)),c_COMBC(tc_nat,tc_Type_Otype,tc_bool))),hAPP(c_COMBC(tc_fun(tc_nat,tc_Type_Otype),tc_Lambda_OdB,tc_fun(tc_nat,tc_fun(tc_Type_Otype,tc_bool))),hAPP(hAPP(c_COMBB(tc_fun(tc_nat,tc_fun(tc_Lambda_OdB,tc_fun(tc_Type_Otype,tc_bool))),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_fun(tc_Type_Otype,tc_bool))),tc_fun(tc_nat,tc_Type_Otype)),c_COMBC(tc_nat,tc_Lambda_OdB,tc_fun(tc_Type_Otype,tc_bool))),hAPP(hAPP(c_COMBB(tc_fun(tc_nat,tc_fun(tc_nat,tc_Type_Otype)),tc_fun(tc_nat,tc_fun(tc_Lambda_OdB,tc_fun(tc_Type_Otype,tc_bool))),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_Type_Otype,tc_bool)),tc_nat),c_Type_Otyping)),hAPP(hAPP(c_COMBC(tc_fun(tc_nat,tc_Type_Otype),tc_Type_Otype,tc_fun(tc_nat,tc_fun(tc_nat,tc_Type_Otype))),hAPP(hAPP(c_COMBB(tc_fun(tc_nat,tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_Type_Otype))),tc_fun(tc_Type_Otype,tc_fun(tc_nat,tc_fun(tc_nat,tc_Type_Otype))),tc_fun(tc_nat,tc_Type_Otype)),c_COMBC(tc_nat,tc_Type_Otype,tc_fun(tc_nat,tc_Type_Otype))),c_Type_Oshift(tc_Type_Otype))),v_T____))))))))))),hAPP(hAPP(c_COMBB(tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBS(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)),hAPP(hAPP(c_COMBB(tc_fun(tc_bool,tc_bool),tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)),tc_Lambda_OdB),c_COMBB(tc_bool,tc_bool,tc_nat)),hAPP(hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Lambda_OdB),c_implies),c_InductTermi_OIT))))),hAPP(hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_Lambda_OdB),hAPP(c_COMBC(tc_fun(tc_nat,tc_Type_Otype),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),hAPP(hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool))),tc_fun(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool))),tc_fun(tc_nat,tc_Type_Otype)),c_COMBS(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool))),hAPP(hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_bool,tc_bool)),tc_fun(tc_Lambda_OdB,tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool))),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_fun(tc_bool,tc_bool),tc_fun(tc_fun(tc_nat,tc_bool),tc_fun(tc_nat,tc_bool)),tc_Lambda_OdB),c_COMBB(tc_bool,tc_bool,tc_nat))),hAPP(hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_bool),tc_fun(tc_Lambda_OdB,tc_fun(tc_bool,tc_bool)),tc_fun(tc_nat,tc_Type_Otype)),hAPP(c_COMBB(tc_bool,tc_fun(tc_bool,tc_bool),tc_Lambda_OdB),c_implies)),hAPP(hAPP(c_COMBC(tc_fun(tc_nat,tc_Type_Otype),tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_bool)),hAPP(hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_Type_Otype,tc_bool)),tc_fun(tc_Type_Otype,tc_fun(tc_Lambda_OdB,tc_bool)),tc_fun(tc_nat,tc_Type_Otype)),c_COMBC(tc_Lambda_OdB,tc_Type_Otype,tc_bool)),c_Type_Otyping)),v_T____)))))),hAPP(hAPP(c_COMBB(tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_Lambda_OdB)),tc_fun(tc_Lambda_OdB,tc_fun(tc_nat,tc_bool)),tc_Lambda_OdB),hAPP(c_COMBB(tc_fun(tc_nat,tc_Lambda_OdB),tc_fun(tc_nat,tc_bool),tc_Lambda_OdB),hAPP(c_COMBB(tc_Lambda_OdB,tc_bool,tc_nat),c_InductTermi_OIT))),c_Lambda_Osubst)))))))))),hAPP(hAPP(c_COMBB(tc_fun(tc_Type_Otype,tc_bool),tc_bool,tc_Lambda_OdB),c_Ex(tc_Type_Otype)),hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)))),v_bs____,tc_Lambda_OdB) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_CHAINED_1,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),v_b____),v_sko__CHAINED__1(v_T____,v_b____,v_e____,v_i____))) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_CHAINED_0_02,axiom, % 0.38/0.60 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(hAPP(c_Lambda_Osubst,v_b____),V_u),V_ia))) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,V_ea),V_u),v_T____)) % 0.38/0.60 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),V_ea),V_ia),v_T____)),v_b____),V_T_H)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_conjecture_0,negated_conjecture, % 0.38/0.60 ~ v_thesis____ ). % 0.38/0.60 % 0.38/0.60 cnf(cls_conjecture_1,negated_conjecture, % 0.38/0.60 ( v_thesis____ % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(hAPP(c_Type_Otyping,hAPP(hAPP(hAPP(c_Type_Oshift(tc_Type_Otype),v_e____),v_i____),v_T____)),v_b____),V_x)) ) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.38/0.60 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.38/0.60 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.38/0.60 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.38/0.60 | ~ class_Orderings_Oorder(T_1) ) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.38/0.60 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.38/0.60 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.38/0.60 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.38/0.60 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.38/0.60 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.38/0.60 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.38/0.60 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.38/0.60 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.38/0.60 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Osemigroup__add,axiom, % 0.38/0.60 class_OrderedGroup_Osemigroup__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.38/0.60 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.38/0.60 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.38/0.60 class_Nat_Osemiring__char__0(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.38/0.60 class_Orderings_Opreorder(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.38/0.60 class_Orderings_Olinorder(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.38/0.60 class_Orderings_Oorder(tc_nat) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_bool__Orderings_Opreorder,axiom, % 0.38/0.60 class_Orderings_Opreorder(tc_bool) ). % 0.38/0.60 % 0.38/0.60 cnf(clsarity_bool__Orderings_Oorder,axiom, % 0.38/0.60 class_Orderings_Oorder(tc_bool) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.38/0.60 hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)) ). % 0.38/0.60 % 0.38/0.60 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.38/0.60 ( V_X = V_Y % 0.38/0.60 | ~ hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y)) ) ). % 0.38/0.60 % 0.38/0.60 %------------------------------------------------------------------------------ % 0.38/0.60 %------------------------------------------- % 0.38/0.60 % Proof found % 0.38/0.60 % SZS status Theorem for theBenchmark % 0.38/0.60 % SZS output start Proof % 0.38/0.60 %ClaNum:404(EqnAxiom:131) % 0.38/0.61 %VarNum:1557(SingletonVarNum:682) % 0.38/0.61 %MaxLitNum:6 % 0.38/0.61 %MaxfuncDepth:8 % 0.38/0.61 %SharedTerms:301 % 0.38/0.61 %goalClause: 192 369 % 0.38/0.61 %singleGoalClaCount:1 % 0.38/0.61 [132]E(a1,a59) % 0.38/0.61 [133]P1(a2) % 0.38/0.61 [134]P2(a2) % 0.38/0.61 [135]P14(a2) % 0.38/0.61 [136]P25(a2) % 0.38/0.61 [137]P15(a2) % 0.38/0.61 [138]P16(a2) % 0.38/0.61 [139]P17(a2) % 0.38/0.61 [140]P3(a2) % 0.38/0.61 [141]P18(a2) % 0.38/0.61 [142]P19(a2) % 0.38/0.61 [143]P10(a2) % 0.38/0.61 [144]P11(a2) % 0.38/0.61 [145]P12(a2) % 0.38/0.61 [146]P20(a2) % 0.38/0.61 [147]P20(a3) % 0.38/0.61 [148]P22(a2) % 0.38/0.61 [149]P22(a3) % 0.38/0.61 [150]P21(a2) % 0.38/0.61 [192]~P27(a5000) % 0.38/0.61 [151]P26(f12(a4,a61)) % 0.38/0.61 [152]P26(f12(a4,a66)) % 0.38/0.61 [179]E(f12(f12(a35,a50),f24(a35,a55,a51,a46,a46)),a49) % 0.38/0.61 [181]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),a57),f62(a49,a57,a53,a1))) % 0.38/0.61 [182]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),a57),f63(a49,a57,a53,a1))) % 0.38/0.61 [183]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),a57),f64(a49,a57,a53,a1))) % 0.38/0.61 [185]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),f12(f12(a15,f14(a59)),a56)),f24(a35,a55,a51,a46,a46))) % 0.38/0.61 [160]P26(f12(f12(f12(a33,a48),a66),a49)) % 0.38/0.61 [161]P26(f12(f12(f12(a33,a53),a61),a49)) % 0.38/0.61 [186]P26(f12(f12(f12(a33,a53),a61),f12(f12(a35,a50),f24(a35,a55,a51,a46,a46)))) % 0.38/0.61 [189]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),f14(a59)),f12(f12(a35,a50),f24(a35,a55,a51,a46,a46)))) % 0.38/0.61 [165]P6(f12(f12(f12(f34(a46),a53),a1),a49),a54,a55) % 0.38/0.61 [187]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a48),a60),a49)),f20(a15,f14(a59),a65,a45,a45)),a52)) % 0.38/0.61 [188]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),f20(a15,f14(a59),a65,a45,a45)),a51)) % 0.38/0.61 [178]P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),a56),a50)) % 0.38/0.61 [191]P4(f12(f12(f9(a45,a3,a3),f12(f12(f7(a3,f47(a3,a3),a45),a41),f12(f12(f7(f47(f47(a2,a46),a3),a3,a45),f8(f47(a2,a46))),f12(f12(f7(f47(f47(a2,a46),f47(a46,a3)),f47(f47(a2,a46),a3),a45),f12(f7(f47(a46,a3),a3,f47(a2,a46)),f8(a46))),f12(f12(f7(f47(f47(a2,a46),f47(a46,f47(a45,a3))),f47(f47(a2,a46),f47(a46,a3)),a45),f12(f7(f47(a46,f47(a45,a3)),f47(a46,a3),f47(a2,a46)),f12(f7(f47(a45,a3),a3,a46),f8(a45)))),f12(f12(f7(f47(f47(a2,a46),f47(a46,f47(a45,f47(a2,a3)))),f47(f47(a2,a46),f47(a46,f47(a45,a3))),a45),f12(f7(f47(a46,f47(a45,f47(a2,a3))),f47(a46,f47(a45,a3)),f47(a2,a46)),f12(f7(f47(a45,f47(a2,a3)),f47(a45,a3),a46),f12(f7(f47(a2,a3),a3,a45),f8(a2))))),f12(f12(f9(a45,f47(f47(a2,a46),f47(a45,f47(a2,a3))),f47(f47(a2,a46),f47(a46,f47(a45,f47(a2,a3))))),f12(f12(f7(f47(f47(a2,a46),f47(f47(a45,f47(a2,a3)),f47(a46,f47(a45,f47(a2,a3))))),f47(f47(f47(a2,a46),f47(a45,f47(a2,a3))),f47(f47(a2,a46),f47(a46,f47(a45,f47(a2,a3))))),a45),f9(f47(a2,a46),f47(a45,f47(a2,a3)),f47(a46,f47(a45,f47(a2,a3))))),f12(f12(f7(f47(f47(a2,a46),f47(a46,f47(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3))))),f47(f47(a2,a46),f47(f47(a45,f47(a2,a3)),f47(a46,f47(a45,f47(a2,a3))))),a45),f12(f7(f47(a46,f47(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3)))),f47(f47(a45,f47(a2,a3)),f47(a46,f47(a45,f47(a2,a3)))),f47(a2,a46)),f6(a46,f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3))))),f12(f12(f7(f47(f47(a2,a46),f47(a46,f47(f47(a2,a3),f47(a2,a3)))),f47(f47(a2,a46),f47(a46,f47(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3))))),a45),f12(f7(f47(a46,f47(f47(a2,a3),f47(a2,a3))),f47(a46,f47(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3)))),f47(a2,a46)),f12(f7(f47(f47(a2,a3),f47(a2,a3)),f47(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3))),a46),f7(f47(a2,a3),f47(a2,a3),a45)))),f12(f12(f7(f47(f47(a2,a46),f47(a46,f47(a2,f47(a3,a3)))),f47(f47(a2,a46),f47(a46,f47(f47(a2,a3),f47(a2,a3)))),a45),f12(f7(f47(a46,f47(a2,f47(a3,a3))),f47(a46,f47(f47(a2,a3),f47(a2,a3))),f47(a2,a46)),f12(f7(f47(a2,f47(a3,a3)),f47(f47(a2,a3),f47(a2,a3)),a46),f9(a2,a3,a3)))),f12(f12(f7(f47(f47(a2,a46),f47(a46,f47(a2,a3))),f47(f47(a2,a46),f47(a46,f47(a2,f47(a3,a3)))),a45),f12(f7(f47(a46,f47(a2,a3)),f47(a46,f47(a2,f47(a3,a3))),f47(a2,a46)),f12(f7(f47(a2,a3),f47(a2,f47(a3,a3)),a46),f12(f7(a3,f47(a3,a3),a2),a43)))),f12(f12(f7(f47(f47(a2,a46),f47(a2,f47(a46,a3))),f47(f47(a2,a46),f47(a46,f47(a2,a3))),a45),f12(f7(f47(a2,f47(a46,a3)),f47(a46,f47(a2,a3)),f47(a2,a46)),f6(a2,a46,a3))),f12(f6(f47(a2,a46),a45,f47(a2,f47(a46,a3))),f12(f12(f7(f47(a2,f47(a45,f47(a46,a3))),f47(a45,f47(a2,f47(a46,a3))),f47(a2,a46)),f6(a2,a45,f47(a46,a3))),f12(f12(f7(f47(a2,f47(a2,a46)),f47(a2,f47(a45,f47(a46,a3))),f47(a2,a46)),f12(f7(f47(a2,a46),f47(a45,f47(a46,a3)),a2),a33)),f12(f12(f6(f47(a2,a46),a46,f47(a2,f47(a2,a46))),f12(f12(f7(f47(a2,f47(a46,f47(a2,a46))),f47(a46,f47(a2,f47(a2,a46))),f47(a2,a46)),f6(a2,a46,f47(a2,a46))),f34(a46))),a49))))))))))),f12(f12(f7(f47(f47(a2,a46),f47(a45,f47(a2,a3))),f47(f47(a2,a46),f47(a45,f47(a2,a3))),a45),f12(f7(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3)),f47(a2,a46)),f12(f9(a45,f47(a2,a3),f47(a2,a3)),f12(f12(f7(f47(a3,a3),f47(f47(a2,a3),f47(a2,a3)),a45),f7(a3,a3,a2)),f12(f12(f7(a3,f47(a3,a3),a45),a43),a4))))),f12(f12(f7(f47(a45,f47(a2,a3)),f47(f47(a2,a46),f47(a45,f47(a2,a3))),a45),f12(f6(f47(a2,a46),f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3))),f12(f12(f7(f47(a45,f47(f47(a2,a3),f47(a2,a3))),f47(f47(a45,f47(a2,a3)),f47(a45,f47(a2,a3))),f47(a2,a46)),f9(a45,f47(a2,a3),f47(a2,a3))),f12(f12(f7(f47(a45,f47(a3,a3)),f47(a45,f47(f47(a2,a3),f47(a2,a3))),f47(a2,a46)),f12(f7(f47(a3,a3),f47(f47(a2,a3),f47(a2,a3)),a45),f7(a3,a3,a2))),f12(f12(f7(f47(a45,a3),f47(a45,f47(a3,a3)),f47(a2,a46)),f12(f7(a3,f47(a3,a3),a45),a43)),f12(f12(f6(f47(a2,a46),a46,f47(a45,a3)),f12(f12(f7(f47(a45,f47(a46,a3)),f47(a46,f47(a45,a3)),f47(a2,a46)),f6(a45,a46,a3)),a33)),a49)))))),f12(f12(f7(f47(a45,f47(a2,a45)),f47(a45,f47(a2,a3)),a45),f12(f7(f47(a2,a45),f47(a2,a3),a45),f12(f7(a45,a3,a2),a4))),a18)))))))))),f12(f12(f7(f47(a46,a3),a3,a45),f10(a46)),f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)))),a58,a45) % 0.38/0.61 [190]P4(a4,f27(f12(f12(f6(a45,a2,a45),a19),f5(a2)),f27(f12(f12(f6(a45,a2,a45),f12(f12(f6(a45,a45,f47(a2,a45)),a18),a61)),a1),a58,a45,a45),a45,a45),a45) % 0.38/0.61 [200]~P5(x2001,x2001,a2) % 0.38/0.61 [204]~P5(x2041,f5(a2),a2) % 0.38/0.61 [153]E(f26(f13(x1531),f44(x1531)),f5(a2)) % 0.38/0.61 [154]P26(f12(a4,f14(x1541))) % 0.38/0.61 [157]E(f31(f32(x1571),x1571,x1571),f32(x1571)) % 0.38/0.61 [210]~P5(f5(a2),f26(f13(x2101),f44(x2101)),a2) % 0.38/0.61 [156]P4(x1561,f13(x1562),x1562) % 0.38/0.61 [194]~E(f17(x1941),f14(x1942)) % 0.38/0.61 [155]E(f30(f30(x1551,x1552),x1552),f30(x1551,x1552)) % 0.38/0.61 [167]P26(f12(f12(f12(a33,x1671),f14(x1672)),f12(x1671,x1672))) % 0.38/0.61 [158]P26(f12(f12(f32(x1581),x1582),x1582)) % 0.38/0.61 [170]P26(f12(f12(a16,f12(f12(a15,f17(x1701)),x1702)),f12(f12(f12(a18,x1701),x1702),f5(a2)))) % 0.38/0.61 [209]~P26(f12(f12(a16,f14(x2091)),x2092)) % 0.38/0.61 [159]E(f12(f12(f12(a18,f14(x1591)),x1592),x1591),x1592) % 0.38/0.61 [202]~E(f25(x2021,x2022,x2023),x2022) % 0.38/0.61 [207]~E(f25(x2071,x2072,x2073),f13(x2073)) % 0.38/0.61 [162]E(f31(f31(x1621,x1622,x1623),x1623,x1622),x1621) % 0.38/0.61 [195]~E(f14(x1951),f12(f12(a15,x1952),x1953)) % 0.38/0.61 [196]~E(f17(x1961),f12(f12(a15,x1962),x1963)) % 0.38/0.61 [197]~E(f12(f12(a15,x1971),x1972),f14(x1973)) % 0.38/0.61 [198]~E(f12(f12(a15,x1981),x1982),f17(x1983)) % 0.38/0.61 [211]~P26(f12(f12(f21(x2111,x2112),x2113),f13(x2112))) % 0.38/0.61 [164]P26(f12(f12(f30(x1641,x1642),x1643),x1643)) % 0.38/0.61 [212]~P26(f12(f12(f21(x2121,x2122),f13(x2122)),x2123)) % 0.38/0.61 [169]E(f12(f12(a15,f12(f12(a19,x1691),x1692)),f12(f12(a19,x1693),x1692)),f12(f12(a19,f12(f12(a15,x1691),x1693)),x1692)) % 0.38/0.61 [168]E(f12(f12(f12(a18,f12(f12(a19,x1681),x1682)),x1683),x1682),x1681) % 0.38/0.61 [172]E(f20(x1721,x1722,f13(x1723),x1724,x1723),x1722) % 0.38/0.61 [173]E(f24(x1731,f13(x1732),x1733,x1732,x1734),x1733) % 0.38/0.61 [214]~E(f20(a15,f17(x2141),x2142,a45,a45),f20(a15,f14(x2143),x2144,a45,a45)) % 0.38/0.61 [213]~E(f12(f12(a15,f17(x2131)),x2132),f20(a15,f14(x2133),x2134,a45,a45)) % 0.38/0.61 [166]E(f12(f12(f12(f12(f34(x1661),x1662),x1663),x1664),x1663),x1664) % 0.38/0.61 [171]E(f12(f12(a15,f12(f12(f12(a18,x1711),x1712),x1713)),f12(f12(f12(a18,x1714),x1712),x1713)),f12(f12(f12(a18,f12(f12(a15,x1711),x1714)),x1712),x1713)) % 0.38/0.61 [184]E(f24(x1841,f25(x1842,x1843,x1844),x1845,x1844,x1846),f12(f12(x1841,x1842),f24(x1841,x1843,x1845,x1844,x1846))) % 0.38/0.61 [180]E(f20(x1801,x1802,f25(x1803,x1804,x1805),x1806,x1805),f20(x1801,f12(f12(x1801,x1802),x1803),x1804,x1806,x1805)) % 0.38/0.61 [223]E(x2231,f5(a2))+P5(f5(a2),x2231,a2) % 0.38/0.61 [217]~P25(x2171)+E(f29(f5(a2),x2171),f5(x2171)) % 0.38/0.61 [218]~P1(x2181)+E(f28(f13(x2181),x2181),f5(x2181)) % 0.38/0.61 [232]~P13(x2321)+E(f12(f12(f11(x2321),f5(x2321)),f5(x2321)),f5(x2321)) % 0.38/0.61 [233]~P26(f12(a4,x2331))+P26(f12(a4,f17(x2331))) % 0.38/0.61 [320]~P26(f12(a4,x3201))+P26(f12(f42(f31(a16,a45,a45),a45),x3201)) % 0.38/0.61 [332]P26(f12(a4,x3321))+~P26(f12(f42(f31(a16,a45,a45),a45),x3321)) % 0.38/0.61 [369]P27(a5000)+~P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),a53),a1),a49)),a57),x3691)) % 0.38/0.61 [234]~P5(x2342,x2342,x2341)+~P20(x2341) % 0.38/0.61 [235]~P5(x2352,x2352,x2351)+~P22(x2351) % 0.38/0.61 [236]~P5(x2362,x2362,x2361)+~P21(x2361) % 0.38/0.61 [215]E(x2151,x2152)+~E(f14(x2151),f14(x2152)) % 0.38/0.61 [216]E(x2161,x2162)+~E(f17(x2161),f17(x2162)) % 0.38/0.61 [219]~P20(x2192)+P20(f47(x2191,x2192)) % 0.38/0.61 [220]~P22(x2202)+P22(f47(x2201,x2202)) % 0.38/0.61 [256]~P14(x2561)+~P5(f29(x2562,x2561),f5(x2561),x2561) % 0.38/0.61 [221]E(x2211,f13(x2212))+~E(f26(x2211,f44(x2212)),f5(a2)) % 0.38/0.61 [224]~P1(x2241)+E(f12(f12(f11(x2241),x2242),f5(x2241)),x2242) % 0.38/0.61 [225]~P19(x2251)+E(f12(f12(f11(x2251),x2252),f5(x2251)),x2252) % 0.38/0.61 [226]~P10(x2261)+E(f12(f12(f11(x2261),x2262),f5(x2261)),x2262) % 0.38/0.61 [237]E(x2371,f13(x2372))+P5(f5(a2),f26(x2371,f44(x2372)),a2) % 0.38/0.61 [278]~P26(f12(f12(a16,x2781),x2782))+P26(f12(f12(a16,f17(x2781)),f17(x2782))) % 0.38/0.61 [345]~P1(x3451)+E(f24(f11(x3451),x3452,f5(x3451),x3451,x3451),f28(x3452,x3451)) % 0.38/0.61 [346]~P1(x3461)+E(f20(f11(x3461),f5(x3461),x3462,x3461,x3461),f28(x3462,x3461)) % 0.38/0.61 [367]~P1(x3671)+E(f24(f11(x3671),x3672,f5(x3671),x3671,x3671),f20(f11(x3671),f5(x3671),x3672,x3671,x3671)) % 0.38/0.61 [227]~P1(x2271)+E(f12(f12(f11(x2271),f5(x2271)),x2272),x2272) % 0.38/0.61 [229]~P19(x2291)+E(f12(f12(f11(x2291),f5(x2291)),x2292),x2292) % 0.38/0.61 [230]~P10(x2301)+E(f12(f12(f11(x2301),f5(x2301)),x2302),x2302) % 0.38/0.61 [255]~P5(x2551,x2552,a2)+E(f12(f12(a19,f14(x2551)),x2552),f14(x2551)) % 0.38/0.61 [276]~P26(f12(a4,x2761))+P26(f12(a4,f12(f12(a19,x2761),x2762))) % 0.38/0.61 [281]~P26(f12(a4,x2811))+P26(f12(a4,f12(f12(a15,x2811),f14(x2812)))) % 0.38/0.61 [314]P26(f12(f12(f30(a16,a45),f17(x3141)),f17(x3142)))+~P26(f12(f12(f30(a16,a45),x3141),x3142)) % 0.38/0.61 [386]~P4(a4,x3862,a45)+P26(f12(a4,f20(a15,f14(x3861),x3862,a45,a45))) % 0.38/0.61 [357]~E(f14(x3572),f20(a15,x3573,x3571,a45,a45))+E(x3571,f13(a45)) % 0.38/0.61 [358]~E(f17(x3582),f20(a15,x3583,x3581,a45,a45))+E(x3581,f13(a45)) % 0.38/0.61 [359]~E(f20(a15,x3592,x3591,a45,a45),f17(x3593))+E(x3591,f13(a45)) % 0.38/0.61 [360]E(x3601,f17(x3602))+~E(f20(a15,x3601,x3603,a45,a45),f17(x3602)) % 0.38/0.61 [361]E(f14(x3611),x3612)+~E(f14(x3611),f20(a15,x3612,x3613,a45,a45)) % 0.38/0.61 [362]E(f17(x3621),x3622)+~E(f17(x3621),f20(a15,x3622,x3623,a45,a45)) % 0.38/0.61 [379]E(x3791,x3792)+~E(f20(a15,x3791,x3793,a45,a45),f20(a15,x3792,x3793,a45,a45)) % 0.38/0.61 [275]~P1(x2751)+E(f12(f12(f11(x2751),x2752),f28(x2753,x2751)),f28(f25(x2752,x2753,x2751),x2751)) % 0.38/0.61 [363]E(f12(f12(a15,x3631),x3632),x3633)+~E(f12(f12(a15,x3631),x3632),f20(a15,x3633,f13(a45),a45,a45)) % 0.38/0.61 [365]~P2(x3651)+E(f24(f11(x3651),x3652,x3653,x3651,x3651),f20(f11(x3651),x3653,x3652,x3651,x3651)) % 0.38/0.61 [389]~P26(f12(f12(a16,x3891),x3893))+P26(f12(f12(a16,f20(a15,x3891,x3892,a45,a45)),f20(a15,x3893,x3892,a45,a45))) % 0.38/0.61 [244]~P19(x2441)+E(f12(f12(f11(x2441),x2442),x2443),f12(f12(f11(x2441),x2443),x2442)) % 0.38/0.61 [245]~P10(x2451)+E(f12(f12(f11(x2451),x2452),x2453),f12(f12(f11(x2451),x2453),x2452)) % 0.38/0.61 [259]E(x2591,x2592)+~P26(f12(f12(f32(x2593),x2591),x2592)) % 0.38/0.61 [293]E(f12(x2931,x2932),x2933)+~P26(f12(f12(f12(a33,x2931),f14(x2932)),x2933)) % 0.38/0.61 [295]~P4(f42(x2951,x2952),x2953,x2952)+P26(f12(f42(f21(x2951,x2952),f44(x2952)),x2953)) % 0.38/0.61 [307]P4(f42(x3071,x3072),x3073,x3072)+~P26(f12(f42(f21(x3071,x3072),f44(x3072)),x3073)) % 0.38/0.61 [325]~P26(f12(f12(a16,x3251),x3253))+P26(f12(f12(a16,f12(f12(a15,x3251),x3252)),f12(f12(a15,x3253),x3252))) % 0.38/0.61 [326]~P26(f12(f12(a16,x3262),x3263))+P26(f12(f12(a16,f12(f12(a15,x3261),x3262)),f12(f12(a15,x3261),x3263))) % 0.38/0.61 [327]~P26(f12(f12(a16,x3271),x3273))+P26(f12(f12(a16,f12(f12(a19,x3271),x3272)),f12(f12(a19,x3273),x3272))) % 0.38/0.61 [334]~P26(f12(f12(f30(a16,a45),x3341),x3343))+P26(f12(f12(f30(a16,a45),f12(f12(a15,x3341),x3342)),f12(f12(a15,x3343),x3342))) % 0.38/0.61 [335]~P26(f12(f12(f30(a16,a45),x3352),x3353))+P26(f12(f12(f30(a16,a45),f12(f12(a15,x3351),x3352)),f12(f12(a15,x3351),x3353))) % 0.38/0.61 [336]~P26(f12(f12(f30(a16,a45),x3361),x3363))+P26(f12(f12(f30(a16,a45),f12(f12(a19,x3361),x3362)),f12(f12(a19,x3363),x3362))) % 0.38/0.61 [377]~P1(x3771)+E(f12(f12(f11(x3771),x3772),f24(f11(x3771),x3773,f5(x3771),x3771,x3771)),f20(f11(x3771),x3772,x3773,x3771,x3771)) % 0.38/0.61 [378]~P1(x3781)+E(f12(f12(f11(x3781),x3782),f20(f11(x3781),f5(x3781),x3783,x3781,x3781)),f20(f11(x3781),x3782,x3783,x3781,x3781)) % 0.38/0.61 [390]P26(f12(f12(a16,f20(a15,x3901,x3902,a45,a45)),f20(a15,x3901,x3903,a45,a45)))+~P26(f12(f12(f21(a16,a45),x3902),x3903)) % 0.38/0.61 [391]P26(f12(f12(f30(a16,a45),f20(a15,x3911,x3912,a45,a45)),f20(a15,x3913,x3912,a45,a45)))+~P26(f12(f12(f30(a16,a45),x3911),x3913)) % 0.38/0.61 [273]~P5(x2731,x2733,a2)+E(f12(f12(f12(a18,f14(x2731)),x2732),x2733),f14(x2731)) % 0.38/0.61 [315]~P26(f12(a4,x3151))+P26(f12(a4,f12(f12(f12(a18,x3151),f14(x3152)),x3153))) % 0.38/0.61 [392]P26(f12(f12(f21(a16,a45),x3921),f23(x3922,x3921,x3923)))+~P26(f12(f12(a16,f20(a15,f14(x3922),x3921,a45,a45)),x3923)) % 0.38/0.61 [397]E(f20(a15,f14(x3971),f23(x3971,x3972,x3973),a45,a45),x3973)+~P26(f12(f12(a16,f20(a15,f14(x3971),x3972,a45,a45)),x3973)) % 0.38/0.61 [366]~P7(x3661,x3664)+E(f24(x3661,x3662,x3663,x3664,x3664),f20(x3661,x3663,x3662,x3664,x3664)) % 0.38/0.61 [239]~P7(x2391,x2394)+E(f12(f12(x2391,x2392),x2393),f12(f12(x2391,x2393),x2392)) % 0.38/0.61 [246]E(x2461,x2462)+~E(f12(f12(a15,x2463),x2461),f12(f12(a15,x2464),x2462)) % 0.38/0.61 [247]E(x2471,x2472)+~E(f12(f12(a35,x2473),x2471),f12(f12(a35,x2474),x2472)) % 0.38/0.61 [248]E(x2481,x2482)+~E(f12(f12(a15,x2481),x2483),f12(f12(a15,x2482),x2484)) % 0.38/0.61 [249]E(x2491,x2492)+~E(f12(f12(a35,x2491),x2493),f12(f12(a35,x2492),x2494)) % 0.38/0.61 [381]E(x3811,x3812)+~E(f20(a15,f14(x3813),x3811,a45,a45),f20(a15,f14(x3814),x3812,a45,a45)) % 0.38/0.61 [382]E(x3821,x3822)+~E(f20(a15,f17(x3823),x3821,a45,a45),f20(a15,f17(x3824),x3822,a45,a45)) % 0.38/0.61 [383]E(x3831,x3832)+~E(f20(a15,f14(x3831),x3833,a45,a45),f20(a15,f14(x3832),x3834,a45,a45)) % 0.38/0.61 [384]E(x3841,x3842)+~E(f20(a15,f17(x3841),x3843,a45,a45),f20(a15,f17(x3842),x3844,a45,a45)) % 0.38/0.61 [286]~P26(f12(f12(x2861,x2863),x2864))+P26(f12(f12(f30(x2861,x2862),x2863),x2864)) % 0.38/0.61 [394]P6(x3941,x3942,f37(x3943,x3941,x3944,x3942))+~P26(f12(f12(f12(a33,x3941),f20(a15,x3944,x3942,a45,a45)),x3943)) % 0.38/0.61 [395]P6(x3951,x3952,f38(x3953,x3951,x3954,x3952))+~P26(f12(f12(f12(a33,x3951),f20(a15,x3954,x3952,a45,a45)),x3953)) % 0.38/0.61 [399]~P26(f12(f12(f12(a33,x3991),f20(a15,x3992,x3994,a45,a45)),x3993))+P26(f12(f12(f12(a33,x3991),x3992),f24(a35,f37(x3993,x3991,x3992,x3994),x3993,a46,a46))) % 0.38/0.61 [400]~P26(f12(f12(f12(a33,x4001),f20(a15,x4002,x4004,a45,a45)),x4003))+P26(f12(f12(f12(a33,x4001),x4002),f24(a35,f38(x4003,x4001,x4002,x4004),x4003,a46,a46))) % 0.38/0.61 [287]~P19(x2871)+E(f12(f12(f11(x2871),x2872),f12(f12(f11(x2871),x2873),x2874)),f12(f12(f11(x2871),x2873),f12(f12(f11(x2871),x2872),x2874))) % 0.38/0.61 [288]~P10(x2881)+E(f12(f12(f11(x2881),x2882),f12(f12(f11(x2881),x2883),x2884)),f12(f12(f11(x2881),x2883),f12(f12(f11(x2881),x2882),x2884))) % 0.38/0.61 [289]~P9(x2891)+E(f12(f12(f11(x2891),x2892),f12(f12(f11(x2891),x2893),x2894)),f12(f12(f11(x2891),x2893),f12(f12(f11(x2891),x2892),x2894))) % 0.38/0.61 [343]~P26(f12(f12(a16,x3431),x3434))+P26(f12(f12(a16,f12(f12(f12(a18,x3431),x3432),x3433)),f12(f12(f12(a18,x3434),x3432),x3433))) % 0.38/0.61 [347]~P26(f12(f12(a16,x3472),x3474))+P26(f12(f12(f30(a16,a45),f12(f12(f12(a18,x3471),x3472),x3473)),f12(f12(f12(a18,x3471),x3474),x3473))) % 0.38/0.61 [349]~P26(f12(f12(f30(x3491,x3492),x3494),x3493))+P26(f12(f12(f30(f31(x3491,x3492,x3492),x3492),x3493),x3494)) % 0.38/0.61 [351]~P26(f12(f12(f30(a16,a45),x3511),x3514))+P26(f12(f12(f30(a16,a45),f12(f12(f12(a18,x3511),x3512),x3513)),f12(f12(f12(a18,x3514),x3512),x3513))) % 0.38/0.61 [352]~P26(f12(f12(f30(a16,a45),x3522),x3524))+P26(f12(f12(f30(a16,a45),f12(f12(f12(a18,x3521),x3522),x3523)),f12(f12(f12(a18,x3521),x3524),x3523))) % 0.38/0.61 [355]P26(f12(f12(f30(x3551,x3552),x3553),x3554))+~P26(f12(f12(f30(f31(x3551,x3552,x3552),x3552),x3554),x3553)) % 0.38/0.61 [356]P26(f12(f12(f12(a33,x3561),x3562),f36(x3563,x3561,x3564,x3562)))+~P26(f12(f12(f12(a33,x3561),f12(f12(a15,x3564),x3562)),x3563)) % 0.38/0.61 [380]~P18(x3801)+E(f20(f11(x3801),f12(f12(f11(x3801),x3802),x3803),x3804,x3801,x3801),f12(f12(f11(x3801),x3802),f20(f11(x3801),x3803,x3804,x3801,x3801))) % 0.38/0.61 [387]~P26(f12(f12(f12(a33,x3871),f12(f12(a15,x3872),x3874)),x3873))+P26(f12(f12(f12(a33,x3871),x3872),f12(f12(a35,f36(x3873,x3871,x3872,x3874)),x3873))) % 0.38/0.61 [396]P6(x3961,x3962,f39(x3963,x3961,x3964,x3962))+~P26(f12(f12(f12(a33,x3961),f20(a15,f14(x3964),x3962,a45,a45)),x3963)) % 0.38/0.61 [401]P26(f12(f12(f12(a33,x4011),f14(x4012)),f24(a35,f39(x4013,x4011,x4012,x4014),x4013,a46,a46)))+~P26(f12(f12(f12(a33,x4011),f20(a15,f14(x4012),x4014,a45,a45)),x4013)) % 0.38/0.61 [310]~P2(x3101)+E(f12(f12(f11(x3101),f12(f12(f11(x3101),x3102),x3103)),x3104),f12(f12(f11(x3101),x3102),f12(f12(f11(x3101),x3103),x3104))) % 0.38/0.61 [311]~P19(x3111)+E(f12(f12(f11(x3111),f12(f12(f11(x3111),x3112),x3113)),x3114),f12(f12(f11(x3111),x3112),f12(f12(f11(x3111),x3113),x3114))) % 0.38/0.61 [312]~P10(x3121)+E(f12(f12(f11(x3121),f12(f12(f11(x3121),x3122),x3123)),x3124),f12(f12(f11(x3121),x3122),f12(f12(f11(x3121),x3123),x3124))) % 0.38/0.61 [321]~P19(x3211)+E(f12(f12(f11(x3211),f12(f12(f11(x3211),x3212),x3213)),x3214),f12(f12(f11(x3211),f12(f12(f11(x3211),x3212),x3214)),x3213)) % 0.38/0.61 [370]P26(f12(f12(f12(a33,x3701),f17(x3702)),f12(f12(a35,x3703),x3704)))+~P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),x3701),f5(a2)),x3703)),x3702),x3704)) % 0.38/0.61 [260]E(x2601,x2602)+~E(f25(x2603,x2601,x2604),f25(x2605,x2602,x2604)) % 0.38/0.61 [261]E(x2611,x2612)+~E(f25(x2611,x2613,x2614),f25(x2612,x2615,x2614)) % 0.38/0.61 [340]~P26(f12(f12(x3401,x3403),x3405))+P26(f12(f12(f21(x3401,x3402),f25(x3403,x3404,x3402)),f25(x3405,x3404,x3402))) % 0.38/0.61 [282]~P7(x2821,x2825)+E(f12(f12(x2821,x2822),f12(f12(x2821,x2823),x2824)),f12(f12(x2821,x2823),f12(f12(x2821,x2822),x2824))) % 0.38/0.61 [329]~P26(f12(f12(x3291,x3295),x3294))+P26(f12(f12(f31(x3291,x3292,x3293),x3294),x3295)) % 0.38/0.61 [338]P26(f12(f12(x3381,x3382),x3383))+~P26(f12(f12(f31(x3381,x3384,x3385),x3383),x3382)) % 0.38/0.61 [342]P26(f12(f12(f21(x3421,x3422),f25(x3423,x3424,x3422)),f25(x3423,x3425,x3422)))+~P26(f12(f12(f21(x3421,x3422),x3424),x3425)) % 0.38/0.61 [294]~P7(x2941,x2945)+E(f12(f12(x2941,f12(f12(x2941,x2942),x2943)),x2944),f12(f12(x2941,x2942),f12(f12(x2941,x2943),x2944))) % 0.38/0.61 [331]~P19(x3311)+E(f12(f12(f11(x3311),f12(f12(f11(x3311),x3312),x3313)),f12(f12(f11(x3311),x3314),x3315)),f12(f12(f11(x3311),f12(f12(f11(x3311),x3312),x3314)),f12(f12(f11(x3311),x3313),x3315))) % 0.38/0.61 [364]~P26(f12(f12(f12(a33,x3641),x3644),x3645))+P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),x3641),x3642),x3643)),f12(f12(a19,x3644),x3642)),x3645)) % 0.38/0.61 [298]~P5(x2985,x2983,a2)+E(f12(f12(f12(f12(f34(x2981),x2982),x2983),x2984),x2985),f12(x2982,x2985)) % 0.38/0.61 [242]E(x2421,x2422)+P5(x2422,x2421,a2)+P5(x2421,x2422,a2) % 0.38/0.61 [270]~P14(x2701)+P5(f5(x2701),f29(x2702,x2701),x2701)+~P5(f5(a2),x2702,a2) % 0.38/0.61 [274]~P14(x2742)+~P5(f5(x2742),f29(x2741,x2742),x2742)+P5(f5(a2),x2741,a2) % 0.38/0.61 [231]~P23(x2311)+~P8(x2311)+E(f12(f12(f11(x2311),x2312),f5(x2311)),x2312) % 0.38/0.61 [238]~P13(x2382)+E(x2381,f5(x2382))+~E(f12(f12(f11(x2382),x2381),x2381),f5(x2382)) % 0.38/0.61 [283]~P13(x2831)+~P5(f5(x2831),x2832,x2831)+P5(f5(x2831),f12(f12(f11(x2831),x2832),x2832),x2831) % 0.38/0.61 [284]~P24(x2841)+~P5(x2842,f5(x2841),x2841)+P5(f12(f12(f11(x2841),x2842),x2842),f5(x2841),x2841) % 0.38/0.61 [285]~P13(x2851)+~P5(x2852,f5(x2851),x2851)+P5(f12(f12(f11(x2851),x2852),x2852),f5(x2851),x2851) % 0.38/0.61 [290]~P24(x2902)+P5(x2901,f5(x2902),x2902)+~P5(f12(f12(f11(x2902),x2901),x2901),f5(x2902),x2902) % 0.38/0.61 [291]~P13(x2912)+P5(x2911,f5(x2912),x2912)+~P5(f12(f12(f11(x2912),x2911),x2911),f5(x2912),x2912) % 0.38/0.61 [292]~P13(x2921)+P5(f5(x2921),x2922,x2921)+~P5(f5(x2921),f12(f12(f11(x2921),x2922),x2922),x2921) % 0.38/0.61 [265]~P5(x2653,x2652,x2651)+~P20(x2651)+~P5(x2652,x2653,x2651) % 0.38/0.61 [267]~P5(x2673,x2672,x2671)+~P22(x2671)+~P5(x2672,x2673,x2671) % 0.38/0.61 [268]~P5(x2683,x2682,x2681)+~P21(x2681)+~P5(x2682,x2683,x2681) % 0.38/0.61 [222]~P3(x2223)+E(x2221,x2222)+~E(f29(x2221,x2223),f29(x2222,x2223)) % 0.38/0.61 [272]~P14(x2722)+~P5(x2721,x2723,a2)+P5(f29(x2721,x2722),f29(x2723,x2722),x2722) % 0.38/0.61 [277]~P14(x2773)+~P5(f29(x2771,x2773),f29(x2772,x2773),x2773)+P5(x2771,x2772,a2) % 0.38/0.61 [258]E(x2581,x2582)+P5(x2582,x2581,a2)+E(f12(f12(f12(a18,f14(x2581)),x2583),x2582),f14(x2581)) % 0.38/0.61 [388]~P26(f12(a4,x3882))+~P26(f12(a4,f20(a15,f12(f12(f12(a18,x3881),x3882),f5(a2)),x3883,a45,a45)))+P26(f12(a4,f20(a15,f12(f12(a15,f17(x3881)),x3882),x3883,a45,a45))) % 0.38/0.61 [393]~P26(f12(f42(f31(a16,a45,a45),a45),x3932))+~P26(f12(f42(f31(a16,a45,a45),a45),f20(a15,f12(f12(f12(a18,x3931),x3932),f5(a2)),x3933,a45,a45)))+P26(f12(f42(f31(a16,a45,a45),a45),f20(a15,f12(f12(a15,f17(x3931)),x3932),x3933,a45,a45))) % 0.38/0.61 [297]~P26(f12(f42(x2971,x2972),x2974))+P26(f12(f42(x2971,x2972),x2973))+~P26(f12(f12(x2971,x2973),x2974)) % 0.38/0.61 [374]E(x3741,f13(a45))+E(f20(a15,x3742,f22(x3743,x3744,x3742,x3741),a45,a45),x3743)+~E(f12(f12(a15,x3743),x3744),f20(a15,x3742,x3741,a45,a45)) % 0.38/0.61 [262]~P11(x2623)+E(x2621,x2622)+~E(f12(f12(f11(x2623),x2624),x2621),f12(f12(f11(x2623),x2624),x2622)) % 0.38/0.61 [263]~P12(x2633)+E(x2631,x2632)+~E(f12(f12(f11(x2633),x2634),x2631),f12(f12(f11(x2633),x2634),x2632)) % 0.38/0.61 [264]~P12(x2643)+E(x2641,x2642)+~E(f12(f12(f11(x2643),x2641),x2644),f12(f12(f11(x2643),x2642),x2644)) % 0.38/0.61 [300]~P16(x3001)+~P5(x3002,x3004,x3001)+P5(f12(f12(f11(x3001),x3002),x3003),f12(f12(f11(x3001),x3004),x3003),x3001) % 0.38/0.61 [301]~P17(x3011)+~P5(x3012,x3014,x3011)+P5(f12(f12(f11(x3011),x3012),x3013),f12(f12(f11(x3011),x3014),x3013),x3011) % 0.38/0.61 [302]~P16(x3021)+~P5(x3023,x3024,x3021)+P5(f12(f12(f11(x3021),x3022),x3023),f12(f12(f11(x3021),x3022),x3024),x3021) % 0.38/0.61 [303]~P17(x3031)+~P5(x3033,x3034,x3031)+P5(f12(f12(f11(x3031),x3032),x3033),f12(f12(f11(x3031),x3032),x3034),x3031) % 0.38/0.61 [316]~P16(x3163)+P5(x3161,x3162,x3163)+~P5(f12(f12(f11(x3163),x3164),x3161),f12(f12(f11(x3163),x3164),x3162),x3163) % 0.38/0.61 [317]~P16(x3173)+P5(x3171,x3172,x3173)+~P5(f12(f12(f11(x3173),x3171),x3174),f12(f12(f11(x3173),x3172),x3174),x3173) % 0.38/0.61 [319]P26(f12(f42(x3191,x3192),x3193))+~P26(f12(f42(x3191,x3192),x3194))+~P26(f12(f12(f30(x3191,x3192),x3193),x3194)) % 0.38/0.61 [322]~P26(f12(f12(a16,x3224),x3222))+~P26(f12(f12(f12(a33,x3221),x3224),x3223))+P26(f12(f12(f12(a33,x3221),x3222),x3223)) % 0.38/0.61 [330]~P26(f12(f12(f30(a16,a45),x3304),x3302))+~P26(f12(f12(f12(a33,x3301),x3304),x3303))+P26(f12(f12(f12(a33,x3301),x3302),x3303)) % 0.38/0.61 [339]~P26(f12(f42(x3391,x3392),x3393))+P26(f12(f42(f21(x3391,x3392),f44(x3392)),f25(x3393,x3394,x3392)))+~P26(f12(f42(f21(x3391,x3392),f44(x3392)),x3394)) % 0.38/0.61 [341]~P26(f12(f12(f30(a16,a45),x3411),x3413))+~P26(f12(f12(f30(a16,a45),x3412),x3414))+P26(f12(f12(f30(a16,a45),f12(f12(a15,x3411),x3412)),f12(f12(a15,x3413),x3414))) % 0.38/0.61 [323]~P26(f12(f12(x3231,x3235),x3234))+~P26(f12(f12(f30(x3231,x3232),x3233),x3235))+P26(f12(f12(f30(x3231,x3232),x3233),x3234)) % 0.38/0.61 [324]~P26(f12(f12(x3241,x3243),x3245))+~P26(f12(f12(f30(x3241,x3242),x3245),x3244))+P26(f12(f12(f30(x3241,x3242),x3243),x3244)) % 0.38/0.61 [333]~P26(f12(f12(f30(x3331,x3332),x3333),x3335))+P26(f12(f12(f30(x3331,x3332),x3333),x3334))+~P26(f12(f12(f30(x3331,x3332),x3335),x3334)) % 0.38/0.61 [398]~P6(x3981,x3983,x3985)+~P26(f12(f12(f12(a33,x3981),x3982),f24(a35,x3985,x3984,a46,a46)))+P26(f12(f12(f12(a33,x3981),f20(a15,x3982,x3983,a45,a45)),x3984)) % 0.38/0.61 [306]~P9(x3061)+E(f12(f12(f11(x3061),x3062),x3063),x3064)+~E(f12(f12(f11(x3061),x3062),f12(f12(f11(x3061),x3065),x3063)),f12(f12(f11(x3061),x3065),x3064)) % 0.38/0.61 [344]~P26(f12(f12(f12(a33,x3441),x3443),x3445))+~P26(f12(f12(f12(a33,x3441),x3442),f12(f12(a35,x3445),x3444)))+P26(f12(f12(f12(a33,x3441),f12(f12(a15,x3442),x3443)),x3444)) % 0.38/0.61 [402]E(x4021,x4022)+~P26(f12(f12(f12(a33,x4023),f20(a15,f14(x4024),x4025,a45,a45)),x4021))+~P26(f12(f12(f12(a33,x4023),f20(a15,f14(x4024),x4025,a45,a45)),x4022)) % 0.38/0.61 [348]E(x3481,x3482)+E(x3483,x3484)+~P26(f12(f12(f21(x3485,x3486),f25(x3484,x3482,x3486)),f25(x3483,x3481,x3486))) % 0.38/0.61 [350]E(x3501,x3502)+~P26(f12(f12(f21(x3503,x3504),f25(x3502,x3505,x3504)),f25(x3501,x3506,x3504)))+P26(f12(f12(x3503,x3502),x3501)) % 0.38/0.61 [353]E(x3531,x3532)+~P26(f12(f12(f21(x3533,x3534),f25(x3535,x3531,x3534)),f25(x3536,x3532,x3534)))+P26(f12(f12(f21(x3533,x3534),x3531),x3532)) % 0.38/0.61 [354]~P26(f12(f12(f21(x3541,x3544),f25(x3542,x3545,x3544)),f25(x3543,x3546,x3544)))+P26(f12(f12(x3541,x3542),x3543))+P26(f12(f12(f21(x3541,x3544),x3545),x3546)) % 0.38/0.61 [385]~P26(f12(f12(f12(a33,x3851),x3853),x3856))+P26(f12(f12(f12(a33,x3851),f12(f12(f12(a18,x3852),x3853),x3854)),x3855))+~P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),x3851),x3854),x3856)),x3852),x3855)) % 0.38/0.61 [250]P5(x2501,x2502,x2503)+~P24(x2503)+E(x2501,x2502)+P5(x2502,x2501,x2503) % 0.38/0.61 [254]P5(x2541,x2542,x2543)+~P21(x2543)+E(x2541,x2542)+P5(x2542,x2541,x2543) % 0.38/0.61 [240]~P23(x2402)+~P8(x2402)+E(x2401,f5(x2402))+~E(f12(f12(f11(x2402),x2403),x2401),x2403) % 0.38/0.61 [304]~P15(x3041)+~P5(f5(x3041),x3043,x3041)+~P5(f5(x3041),x3042,x3041)+P5(f5(x3041),f12(f12(f11(x3041),x3042),x3043),x3041) % 0.38/0.61 [305]~P15(x3051)+~P5(x3053,f5(x3051),x3051)+~P5(x3052,f5(x3051),x3051)+P5(f12(f12(f11(x3051),x3052),x3053),f5(x3051),x3051) % 0.38/0.61 [279]~P20(x2793)+~P5(x2791,x2794,x2793)+P5(x2791,x2792,x2793)+~P5(x2794,x2792,x2793) % 0.38/0.61 [280]~P22(x2803)+~P5(x2801,x2804,x2803)+P5(x2801,x2802,x2803)+~P5(x2804,x2802,x2803) % 0.38/0.61 [269]~P23(x2693)+~P8(x2693)+E(x2691,x2692)+~E(f12(f12(f11(x2693),x2694),x2691),f12(f12(f11(x2693),x2694),x2692)) % 0.38/0.61 [299]~P14(x2992)+~P5(x2991,x2994,x2992)+~P5(f5(x2992),x2993,x2992)+P5(x2991,f12(f12(f11(x2992),x2993),x2994),x2992) % 0.38/0.61 [373]~P26(f12(a4,x3731))+~P26(f12(f12(f12(a33,x3733),x3731),a49))+P26(f12(a4,f12(f12(f12(a18,a57),x3731),x3732)))+~P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),x3733),x3732),a49)),a57),x3734)) % 0.38/0.61 [313]~P17(x3131)+~P5(x3133,x3135,x3131)+~P5(x3132,x3134,x3131)+P5(f12(f12(f11(x3131),x3132),x3133),f12(f12(f11(x3131),x3134),x3135),x3131) % 0.38/0.61 [403]~P6(x4031,x4035,x4036)+P6(x4031,x4032,f40(x4033,x4034,x4031,x4032))+~P26(f12(f12(f12(a33,x4031),f20(a15,f14(x4037),x4035,a45,a45)),x4034))+~P26(f12(f12(f12(a33,x4031),f20(a15,f20(a15,f14(x4037),x4035,a45,a45),x4032,a45,a45)),x4033)) % 0.38/0.61 [404]~P6(x4043,x4045,x4046)+E(f24(a35,f40(x4041,x4042,x4043,x4044),x4041,a46,a46),x4042)+~P26(f12(f12(f12(a33,x4043),f20(a15,f14(x4047),x4045,a45,a45)),x4042))+~P26(f12(f12(f12(a33,x4043),f20(a15,f20(a15,f14(x4047),x4045,a45,a45),x4044,a45,a45)),x4041)) % 0.38/0.61 [375]~P26(f12(a4,x3752))+~P26(f12(a4,x3751))+~E(f12(f12(a35,x3754),x3755),a49)+~P26(f12(f12(f12(a33,x3756),x3752),x3755))+P26(f12(a4,f12(f12(f12(a18,x3751),x3752),x3753)))+~P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),x3756),x3753),x3755)),x3751),x3757)) % 0.38/0.61 [376]~P26(f12(a4,x3762))+~P26(f12(a4,x3761))+~E(f12(f12(a35,x3764),x3765),a49)+~P26(f12(f12(f12(a33,x3766),x3762),x3764))+P26(f12(a4,f12(f12(f12(a18,x3761),x3762),x3763)))+~P26(f12(f12(f12(a33,f12(f12(f12(f34(a46),x3766),x3763),x3764)),x3761),x3767)) % 0.38/0.61 %EqnAxiom % 0.38/0.61 [1]E(x11,x11) % 0.38/0.61 [2]E(x22,x21)+~E(x21,x22) % 0.38/0.61 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.38/0.61 [4]~E(x41,x42)+E(f12(x41,x43),f12(x42,x43)) % 0.38/0.61 [5]~E(x51,x52)+E(f12(x53,x51),f12(x53,x52)) % 0.38/0.61 [6]~E(x61,x62)+E(f20(x61,x63,x64,x65,x66),f20(x62,x63,x64,x65,x66)) % 0.38/0.61 [7]~E(x71,x72)+E(f20(x73,x71,x74,x75,x76),f20(x73,x72,x74,x75,x76)) % 0.38/0.61 [8]~E(x81,x82)+E(f20(x83,x84,x81,x85,x86),f20(x83,x84,x82,x85,x86)) % 0.38/0.61 [9]~E(x91,x92)+E(f20(x93,x94,x95,x91,x96),f20(x93,x94,x95,x92,x96)) % 0.38/0.61 [10]~E(x101,x102)+E(f20(x103,x104,x105,x106,x101),f20(x103,x104,x105,x106,x102)) % 0.38/0.61 [11]~E(x111,x112)+E(f13(x111),f13(x112)) % 0.38/0.61 [12]~E(x121,x122)+E(f44(x121),f44(x122)) % 0.38/0.61 [13]~E(x131,x132)+E(f26(x131,x133),f26(x132,x133)) % 0.38/0.61 [14]~E(x141,x142)+E(f26(x143,x141),f26(x143,x142)) % 0.38/0.61 [15]~E(x151,x152)+E(f5(x151),f5(x152)) % 0.38/0.61 [16]~E(x161,x162)+E(f14(x161),f14(x162)) % 0.38/0.61 [17]~E(x171,x172)+E(f11(x171),f11(x172)) % 0.38/0.61 [18]~E(x181,x182)+E(f30(x181,x183),f30(x182,x183)) % 0.38/0.61 [19]~E(x191,x192)+E(f30(x193,x191),f30(x193,x192)) % 0.38/0.61 [20]~E(x201,x202)+E(f24(x201,x203,x204,x205,x206),f24(x202,x203,x204,x205,x206)) % 0.38/0.61 [21]~E(x211,x212)+E(f24(x213,x211,x214,x215,x216),f24(x213,x212,x214,x215,x216)) % 0.38/0.61 [22]~E(x221,x222)+E(f24(x223,x224,x221,x225,x226),f24(x223,x224,x222,x225,x226)) % 0.38/0.61 [23]~E(x231,x232)+E(f24(x233,x234,x235,x231,x236),f24(x233,x234,x235,x232,x236)) % 0.38/0.61 [24]~E(x241,x242)+E(f24(x243,x244,x245,x246,x241),f24(x243,x244,x245,x246,x242)) % 0.38/0.61 [25]~E(x251,x252)+E(f7(x251,x253,x254),f7(x252,x253,x254)) % 0.38/0.61 [26]~E(x261,x262)+E(f7(x263,x261,x264),f7(x263,x262,x264)) % 0.38/0.61 [27]~E(x271,x272)+E(f7(x273,x274,x271),f7(x273,x274,x272)) % 0.38/0.61 [28]~E(x281,x282)+E(f17(x281),f17(x282)) % 0.38/0.61 [29]~E(x291,x292)+E(f32(x291),f32(x292)) % 0.38/0.61 [30]~E(x301,x302)+E(f31(x301,x303,x304),f31(x302,x303,x304)) % 0.38/0.61 [31]~E(x311,x312)+E(f31(x313,x311,x314),f31(x313,x312,x314)) % 0.38/0.61 [32]~E(x321,x322)+E(f31(x323,x324,x321),f31(x323,x324,x322)) % 0.38/0.61 [33]~E(x331,x332)+E(f47(x331,x333),f47(x332,x333)) % 0.38/0.61 [34]~E(x341,x342)+E(f47(x343,x341),f47(x343,x342)) % 0.38/0.61 [35]~E(x351,x352)+E(f36(x351,x353,x354,x355),f36(x352,x353,x354,x355)) % 0.38/0.61 [36]~E(x361,x362)+E(f36(x363,x361,x364,x365),f36(x363,x362,x364,x365)) % 0.38/0.61 [37]~E(x371,x372)+E(f36(x373,x374,x371,x375),f36(x373,x374,x372,x375)) % 0.38/0.61 [38]~E(x381,x382)+E(f36(x383,x384,x385,x381),f36(x383,x384,x385,x382)) % 0.38/0.61 [39]~E(x391,x392)+E(f6(x391,x393,x394),f6(x392,x393,x394)) % 0.38/0.61 [40]~E(x401,x402)+E(f6(x403,x401,x404),f6(x403,x402,x404)) % 0.38/0.61 [41]~E(x411,x412)+E(f6(x413,x414,x411),f6(x413,x414,x412)) % 0.38/0.61 [42]~E(x421,x422)+E(f25(x421,x423,x424),f25(x422,x423,x424)) % 0.38/0.61 [43]~E(x431,x432)+E(f25(x433,x431,x434),f25(x433,x432,x434)) % 0.38/0.61 [44]~E(x441,x442)+E(f25(x443,x444,x441),f25(x443,x444,x442)) % 0.38/0.61 [45]~E(x451,x452)+E(f28(x451,x453),f28(x452,x453)) % 0.38/0.61 [46]~E(x461,x462)+E(f28(x463,x461),f28(x463,x462)) % 0.38/0.61 [47]~E(x471,x472)+E(f21(x471,x473),f21(x472,x473)) % 0.38/0.61 [48]~E(x481,x482)+E(f21(x483,x481),f21(x483,x482)) % 0.38/0.61 [49]~E(x491,x492)+E(f42(x491,x493),f42(x492,x493)) % 0.38/0.61 [50]~E(x501,x502)+E(f42(x503,x501),f42(x503,x502)) % 0.38/0.61 [51]~E(x511,x512)+E(f40(x511,x513,x514,x515),f40(x512,x513,x514,x515)) % 0.38/0.61 [52]~E(x521,x522)+E(f40(x523,x521,x524,x525),f40(x523,x522,x524,x525)) % 0.38/0.61 [53]~E(x531,x532)+E(f40(x533,x534,x531,x535),f40(x533,x534,x532,x535)) % 0.38/0.61 [54]~E(x541,x542)+E(f40(x543,x544,x545,x541),f40(x543,x544,x545,x542)) % 0.38/0.61 [55]~E(x551,x552)+E(f9(x551,x553,x554),f9(x552,x553,x554)) % 0.38/0.61 [56]~E(x561,x562)+E(f9(x563,x561,x564),f9(x563,x562,x564)) % 0.38/0.61 [57]~E(x571,x572)+E(f9(x573,x574,x571),f9(x573,x574,x572)) % 0.38/0.61 [58]~E(x581,x582)+E(f34(x581),f34(x582)) % 0.38/0.61 [59]~E(x591,x592)+E(f29(x591,x593),f29(x592,x593)) % 0.38/0.61 [60]~E(x601,x602)+E(f29(x603,x601),f29(x603,x602)) % 0.38/0.61 [61]~E(x611,x612)+E(f8(x611),f8(x612)) % 0.38/0.61 [62]~E(x621,x622)+E(f64(x621,x623,x624,x625),f64(x622,x623,x624,x625)) % 0.38/0.61 [63]~E(x631,x632)+E(f64(x633,x631,x634,x635),f64(x633,x632,x634,x635)) % 0.38/0.61 [64]~E(x641,x642)+E(f64(x643,x644,x641,x645),f64(x643,x644,x642,x645)) % 0.38/0.61 [65]~E(x651,x652)+E(f64(x653,x654,x655,x651),f64(x653,x654,x655,x652)) % 0.38/0.61 [66]~E(x661,x662)+E(f27(x661,x663,x664,x665),f27(x662,x663,x664,x665)) % 0.38/0.61 [67]~E(x671,x672)+E(f27(x673,x671,x674,x675),f27(x673,x672,x674,x675)) % 0.38/0.61 [68]~E(x681,x682)+E(f27(x683,x684,x681,x685),f27(x683,x684,x682,x685)) % 0.38/0.61 [69]~E(x691,x692)+E(f27(x693,x694,x695,x691),f27(x693,x694,x695,x692)) % 0.38/0.61 [70]~E(x701,x702)+E(f22(x701,x703,x704,x705),f22(x702,x703,x704,x705)) % 0.38/0.61 [71]~E(x711,x712)+E(f22(x713,x711,x714,x715),f22(x713,x712,x714,x715)) % 0.38/0.61 [72]~E(x721,x722)+E(f22(x723,x724,x721,x725),f22(x723,x724,x722,x725)) % 0.38/0.61 [73]~E(x731,x732)+E(f22(x733,x734,x735,x731),f22(x733,x734,x735,x732)) % 0.38/0.61 [74]~E(x741,x742)+E(f23(x741,x743,x744),f23(x742,x743,x744)) % 0.38/0.61 [75]~E(x751,x752)+E(f23(x753,x751,x754),f23(x753,x752,x754)) % 0.38/0.61 [76]~E(x761,x762)+E(f23(x763,x764,x761),f23(x763,x764,x762)) % 0.38/0.61 [77]~E(x771,x772)+E(f39(x771,x773,x774,x775),f39(x772,x773,x774,x775)) % 0.38/0.61 [78]~E(x781,x782)+E(f39(x783,x781,x784,x785),f39(x783,x782,x784,x785)) % 0.38/0.61 [79]~E(x791,x792)+E(f39(x793,x794,x791,x795),f39(x793,x794,x792,x795)) % 0.38/0.61 [80]~E(x801,x802)+E(f39(x803,x804,x805,x801),f39(x803,x804,x805,x802)) % 0.38/0.61 [81]~E(x811,x812)+E(f38(x811,x813,x814,x815),f38(x812,x813,x814,x815)) % 0.38/0.61 [82]~E(x821,x822)+E(f38(x823,x821,x824,x825),f38(x823,x822,x824,x825)) % 0.38/0.61 [83]~E(x831,x832)+E(f38(x833,x834,x831,x835),f38(x833,x834,x832,x835)) % 0.38/0.61 [84]~E(x841,x842)+E(f38(x843,x844,x845,x841),f38(x843,x844,x845,x842)) % 0.38/0.61 [85]~E(x851,x852)+E(f10(x851),f10(x852)) % 0.38/0.61 [86]~E(x861,x862)+E(f62(x861,x863,x864,x865),f62(x862,x863,x864,x865)) % 0.38/0.61 [87]~E(x871,x872)+E(f62(x873,x871,x874,x875),f62(x873,x872,x874,x875)) % 0.38/0.61 [88]~E(x881,x882)+E(f62(x883,x884,x881,x885),f62(x883,x884,x882,x885)) % 0.38/0.61 [89]~E(x891,x892)+E(f62(x893,x894,x895,x891),f62(x893,x894,x895,x892)) % 0.38/0.61 [90]~E(x901,x902)+E(f37(x901,x903,x904,x905),f37(x902,x903,x904,x905)) % 0.38/0.61 [91]~E(x911,x912)+E(f37(x913,x911,x914,x915),f37(x913,x912,x914,x915)) % 0.38/0.61 [92]~E(x921,x922)+E(f37(x923,x924,x921,x925),f37(x923,x924,x922,x925)) % 0.38/0.61 [93]~E(x931,x932)+E(f37(x933,x934,x935,x931),f37(x933,x934,x935,x932)) % 0.38/0.61 [94]~E(x941,x942)+E(f63(x941,x943,x944,x945),f63(x942,x943,x944,x945)) % 0.38/0.61 [95]~E(x951,x952)+E(f63(x953,x951,x954,x955),f63(x953,x952,x954,x955)) % 0.38/0.61 [96]~E(x961,x962)+E(f63(x963,x964,x961,x965),f63(x963,x964,x962,x965)) % 0.38/0.61 [97]~E(x971,x972)+E(f63(x973,x974,x975,x971),f63(x973,x974,x975,x972)) % 0.38/0.61 [98]~P1(x981)+P1(x982)+~E(x981,x982) % 0.38/0.61 [99]~P2(x991)+P2(x992)+~E(x991,x992) % 0.38/0.61 [100]~P14(x1001)+P14(x1002)+~E(x1001,x1002) % 0.38/0.61 [101]~P25(x1011)+P25(x1012)+~E(x1011,x1012) % 0.38/0.61 [102]~P15(x1021)+P15(x1022)+~E(x1021,x1022) % 0.38/0.61 [103]~P16(x1031)+P16(x1032)+~E(x1031,x1032) % 0.38/0.61 [104]~P17(x1041)+P17(x1042)+~E(x1041,x1042) % 0.38/0.61 [105]~P3(x1051)+P3(x1052)+~E(x1051,x1052) % 0.38/0.61 [106]~P18(x1061)+P18(x1062)+~E(x1061,x1062) % 0.38/0.61 [107]~P19(x1071)+P19(x1072)+~E(x1071,x1072) % 0.38/0.61 [108]~P10(x1081)+P10(x1082)+~E(x1081,x1082) % 0.38/0.61 [109]~P11(x1091)+P11(x1092)+~E(x1091,x1092) % 0.38/0.61 [110]~P12(x1101)+P12(x1102)+~E(x1101,x1102) % 0.38/0.61 [111]~P20(x1111)+P20(x1112)+~E(x1111,x1112) % 0.38/0.61 [112]~P26(x1121)+P26(x1122)+~E(x1121,x1122) % 0.38/0.61 [113]~P22(x1131)+P22(x1132)+~E(x1131,x1132) % 0.38/0.61 [114]P7(x1142,x1143)+~E(x1141,x1142)+~P7(x1141,x1143) % 0.38/0.61 [115]P7(x1153,x1152)+~E(x1151,x1152)+~P7(x1153,x1151) % 0.38/0.61 [116]~P21(x1161)+P21(x1162)+~E(x1161,x1162) % 0.38/0.61 [117]~P27(x1171)+P27(x1172)+~E(x1171,x1172) % 0.38/0.61 [118]P5(x1182,x1183,x1184)+~E(x1181,x1182)+~P5(x1181,x1183,x1184) % 0.38/0.61 [119]P5(x1193,x1192,x1194)+~E(x1191,x1192)+~P5(x1193,x1191,x1194) % 0.38/0.61 [120]P5(x1203,x1204,x1202)+~E(x1201,x1202)+~P5(x1203,x1204,x1201) % 0.38/0.61 [121]P6(x1212,x1213,x1214)+~E(x1211,x1212)+~P6(x1211,x1213,x1214) % 0.38/0.61 [122]P6(x1223,x1222,x1224)+~E(x1221,x1222)+~P6(x1223,x1221,x1224) % 0.38/0.61 [123]P6(x1233,x1234,x1232)+~E(x1231,x1232)+~P6(x1233,x1234,x1231) % 0.38/0.61 [124]P4(x1242,x1243,x1244)+~E(x1241,x1242)+~P4(x1241,x1243,x1244) % 0.38/0.61 [125]P4(x1253,x1252,x1254)+~E(x1251,x1252)+~P4(x1253,x1251,x1254) % 0.38/0.61 [126]P4(x1263,x1264,x1262)+~E(x1261,x1262)+~P4(x1263,x1264,x1261) % 0.38/0.61 [127]~P9(x1271)+P9(x1272)+~E(x1271,x1272) % 0.38/0.61 [128]~P13(x1281)+P13(x1282)+~E(x1281,x1282) % 0.38/0.61 [129]~P24(x1291)+P24(x1292)+~E(x1291,x1292) % 0.38/0.61 [130]~P8(x1301)+P8(x1302)+~E(x1301,x1302) % 0.38/0.61 [131]~P23(x1311)+P23(x1312)+~E(x1311,x1312) % 0.38/0.61 % 0.38/0.61 %------------------------------------------- % 0.38/0.61 cnf(424,plain, % 0.38/0.61 ($false), % 0.38/0.61 inference(scs_inference,[],[192,183,369]), % 0.38/0.61 ['proof']). % 0.38/0.61 % SZS output end Proof % 0.38/0.61 % Total time :0.028995s %------------------------------------------------------------------------------