%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL839-1 : TPTP v9.3.1. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n017.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:19:58 AM UTC 2026 % Result : Unsatisfiable 0.48s 0.67s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL839-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.08/0.35 % Computer : n017.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 : Fri Sep 4 20:44:51 UTC 2026 % 0.08/0.35 % CPUTime : % 0.23/0.52 start to proof:theBenchmark % 0.40/0.62 %------------------------------------------- % 0.40/0.62 % File :CSE---1.7 % 0.40/0.62 % Problem :theBenchmark % 0.40/0.62 % Transform :cnf % 0.40/0.62 % Format :tptp:raw % 0.40/0.62 % Command :java -jar mcs_scs.jar %d %s % 0.40/0.62 % 0.40/0.62 % Result :Theorem 0.035942s % 0.40/0.62 % Output :CNFRefutation 0.035942s % 0.40/0.62 %------------------------------------------- % 0.40/0.62 %------------------------------------------------------------------------------ % 0.40/0.62 % File : LCL839-1 : TPTP v9.3.1. Released v4.1.0. % 0.40/0.62 % Domain : Logic Calculi % 0.40/0.62 % Problem : Strong normalization of typed lambda calculus 237_50 % 0.40/0.62 % Version : Especial. % 0.40/0.62 % English : % 0.40/0.62 % 0.40/0.62 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.40/0.62 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.40/0.62 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.40/0.62 % Source : [Nip10] % 0.40/0.62 % Names : StrongNorm-237_50 [Nip10] % 0.40/0.62 % 0.40/0.62 % Status : Unsatisfiable % 0.40/0.62 % Rating : 0.25 v9.3.0, 0.05 v9.1.0, 0.10 v9.0.0, 0.05 v8.2.0, 0.10 v8.1.0, 0.11 v7.4.0, 0.12 v7.3.0, 0.00 v7.0.0, 0.20 v6.3.0, 0.09 v6.2.0, 0.20 v6.1.0, 0.14 v6.0.0, 0.20 v5.5.0, 0.40 v5.3.0, 0.39 v5.2.0, 0.31 v5.1.0, 0.41 v5.0.0, 0.29 v4.1.0 % 0.40/0.63 % Syntax : Number of clauses : 389 ( 125 unt; 29 nHn; 226 RR) % 0.40/0.63 % Number of literals : 776 ( 262 equ; 385 neg) % 0.40/0.63 % Maximal clause size : 6 ( 1 avg) % 0.40/0.63 % Maximal term depth : 6 ( 2 avg) % 0.40/0.63 % Number of predicates : 33 ( 32 usr; 1 prp; 0-4 aty) % 0.40/0.63 % Number of functors : 53 ( 53 usr; 21 con; 0-5 aty) % 0.40/0.63 % Number of variables : 973 ( 141 sgn) % 0.40/0.63 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.40/0.63 % 0.40/0.63 % Comments : % 0.40/0.63 %------------------------------------------------------------------------------ % 0.40/0.63 cnf(cls_dB_Osize_I4_J_0,axiom, % 0.40/0.63 c_Nat_Osize__class_Osize(c_Lambda_OdB_OVar(V_nat),tc_Lambda_OdB) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_dB_Osize_I1_J_0,axiom, % 0.40/0.63 c_Lambda_OdB_OdB__size(c_Lambda_OdB_OVar(V_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_diff__less_0,axiom, % 0.40/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_m,tc_nat) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_zero__less__diff_1,axiom, % 0.40/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat),tc_nat) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_zero__less__diff_0,axiom, % 0.40/0.63 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat),tc_nat) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_nat__diff__split_0,axiom, % 0.40/0.63 ( hBOOL(hAPP(V_P,c_HOL_Ozero__class_Ozero(tc_nat))) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,tc_nat) % 0.40/0.63 | ~ hBOOL(hAPP(V_P,c_HOL_Ominus__class_Ominus(V_a,V_b,tc_nat))) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_less__iff__diff__less__0_0,axiom, % 0.40/0.63 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.40/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_less__iff__diff__less__0_1,axiom, % 0.40/0.63 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.40/0.63 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.40/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_add__diff__inverse_0,axiom, % 0.40/0.63 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat)) = V_m % 0.40/0.63 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.40/0.63 % 0.40/0.63 cnf(cls_less__eqI_1,axiom, % 0.40/0.63 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.40/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a) % 0.40/0.63 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_less__eqI_0,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a) % 0.48/0.63 | c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_less__diff__conv_1,axiom, % 0.48/0.63 ( c_HOL_Oord__class_Oless(V_i,c_HOL_Ominus__class_Ominus(V_j,V_k,tc_nat),tc_nat) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),V_j,tc_nat) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_less__diff__conv_0,axiom, % 0.48/0.63 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),V_j,tc_nat) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(V_i,c_HOL_Ominus__class_Ominus(V_j,V_k,tc_nat),tc_nat) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diffs0__imp__equal_0,axiom, % 0.48/0.63 ( c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.63 | V_m = V_n ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_less__imp__diff__less_0,axiom, % 0.48/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_j,V_n,tc_nat),V_k,tc_nat) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__Suc__Suc_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(c_Suc(V_m),c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_minus__nat_Odiff__0_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__self__eq__0_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(V_m,V_m,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_class__ringb_Osubr0__iff_1,axiom, % 0.48/0.63 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.48/0.63 | ~ class_Int_Onumber__ring(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__self_0,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_a,V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__0__right_0,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_right__minus__eq_1,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_eq__iff__diff__eq__0_0,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__less__mono2_0,axiom, % 0.48/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_l,V_n,tc_nat),c_HOL_Ominus__class_Ominus(V_l,V_m,tc_nat),tc_nat) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_l,tc_nat) % 0.48/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__Suc__1_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(c_Suc(V_n),c_HOL_Oone__class_Oone(tc_nat),tc_nat) = V_n ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__add__cancel_0,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.48/0.63 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ominus__class_Ominus(V_a,V_b,T_a)),V_b) = V_a ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_nat__diff__split__asm_1,axiom, % 0.48/0.63 ( ~ hBOOL(hAPP(V_P,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_b),V_x),V_b,tc_nat))) % 0.48/0.63 | hBOOL(hAPP(V_P,V_x)) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_nat__diff__split_1,axiom, % 0.48/0.63 ( ~ hBOOL(hAPP(V_P,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_b),V_d),V_b,tc_nat))) % 0.48/0.63 | hBOOL(hAPP(V_P,V_d)) ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__less__Suc_0,axiom, % 0.48/0.63 c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),c_Suc(V_m),tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__add__0_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(V_n,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__diff__left_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_i,V_j,tc_nat),V_k,tc_nat) = c_HOL_Ominus__class_Ominus(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_k),tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_eq__eqI_1,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) % 0.48/0.63 | V_xa = V_y ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_eq__eqI_0,axiom, % 0.48/0.63 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.48/0.63 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) != c_HOL_Ominus__class_Ominus(V_x_H,V_y_H,T_a) % 0.48/0.63 | V_x_H = V_y_H ) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__0__eq__0_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__cancel2_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_k),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_k),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_diff__cancel_0,axiom, % 0.48/0.63 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.48/0.63 % 0.48/0.63 cnf(cls_class__ringb_Osubr0__iff_0,axiom, % 0.48/0.63 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.48/0.63 | ~ class_Int_Onumber__ring(T_a) % 0.48/0.64 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.48/0.64 | V_x = V_y ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_right__minus__eq_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.48/0.64 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.48/0.64 | V_a = V_b ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_eq__iff__diff__eq__0_1,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.48/0.64 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.48/0.64 | V_a = V_b ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_diff__commute_0,axiom, % 0.48/0.64 c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_i,V_j,tc_nat),V_k,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_i,V_k,tc_nat),V_j,tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_Suc__diff__diff_0,axiom, % 0.48/0.64 c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(c_Suc(V_m),V_n,tc_nat),c_Suc(V_k),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_k,tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_diff__Suc__eq__diff__pred_0,axiom, % 0.48/0.64 c_HOL_Ominus__class_Ominus(V_m,c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(V_m,c_HOL_Oone__class_Oone(tc_nat),tc_nat),V_n,tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_diff__add__inverse2_0,axiom, % 0.48/0.64 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),V_n,tc_nat) = V_m ). % 0.48/0.64 % 0.48/0.64 cnf(cls_diff__add__inverse_0,axiom, % 0.48/0.64 c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m),V_n,tc_nat) = V_m ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__diff__cancel_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.48/0.64 | c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b),V_b,T_a) = V_a ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_diff__Suc__less_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_n,c_Suc(V_i),tc_nat),V_n,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_Suc__pred_0,axiom, % 0.48/0.64 ( c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = V_n % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_shift__lt_0,axiom, % 0.48/0.64 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,c_HOL_Ominus__class_Ominus(V_j,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_One__nat__def_0,axiom, % 0.48/0.64 c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_r__into__rtranclp_0,axiom, % 0.48/0.64 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(V_r,V_x),V_y)) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_not__Nil__step1_0,axiom, % 0.48/0.64 ~ c_ListOrder_Ostep1(V_r,c_List_Olist_ONil(T_a),V_xs,T_a) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_not__step1__Nil_0,axiom, % 0.48/0.64 ~ c_ListOrder_Ostep1(V_r,V_xs,c_List_Olist_ONil(T_a),T_a) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_one__is__add_1,axiom, % 0.48/0.64 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.48/0.64 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.64 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_one__is__add_2,axiom, % 0.48/0.64 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.48/0.64 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_foldl__Nil_0,axiom, % 0.48/0.64 c_List_Ofoldl(V_f,V_a,c_List_Olist_ONil(T_b),T_a,T_b) = V_a ). % 0.48/0.64 % 0.48/0.64 cnf(cls_one__neq__zero_0,axiom, % 0.48/0.64 ( ~ class_Ring__and__Field_Ozero__neq__one(T_a) % 0.48/0.64 | c_HOL_Oone__class_Oone(T_a) != c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_conversep__eq_0,axiom, % 0.48/0.64 c_Predicate_Oconversep(c_fequal(T_a),T_a,T_a) = c_fequal(T_a) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_less__SucE_0,axiom, % 0.48/0.64 ( V_m = V_n % 0.48/0.64 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_less__antisym_0,axiom, % 0.48/0.64 ( V_m = V_n % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.48/0.64 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_not__less__less__Suc__eq_0,axiom, % 0.48/0.64 ( V_n = V_m % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.48/0.64 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_one__is__add_4,axiom, % 0.48/0.64 c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__strict__mono_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_d),T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__less__mono_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_l),tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_nat_Osimps_I3_J_0,axiom, % 0.48/0.64 c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_Suc__neq__Zero_0,axiom, % 0.48/0.64 c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_lessI_0,axiom, % 0.48/0.64 c_HOL_Oord__class_Oless(V_n,c_Suc(V_n),tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_less__Suc__eq_2,axiom, % 0.48/0.64 c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_less__trans__Suc_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(c_Suc(V_i),V_k,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_foldl__foldr1_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.48/0.64 | 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.48/0.64 % 0.48/0.64 cnf(cls_less__add__one_0,axiom, % 0.48/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(V_a,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Oone__class_Oone(T_a)),T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_conversep__conversep_0,axiom, % 0.48/0.64 c_Predicate_Oconversep(c_Predicate_Oconversep(V_r,T_a,T_b),T_b,T_a) = V_r ). % 0.48/0.64 % 0.48/0.64 cnf(cls_not__add__less1_0,axiom, % 0.48/0.64 ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_i,tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_not__add__less2_0,axiom, % 0.48/0.64 ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_i),V_i,tc_nat) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_Suc__n__not__n_0,axiom, % 0.48/0.64 c_Suc(V_n) != V_n ). % 0.48/0.64 % 0.48/0.64 cnf(cls_n__not__Suc__n_0,axiom, % 0.48/0.64 V_n != c_Suc(V_n) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__strict__right__mono_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c),T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__less__cancel__right_1,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c),T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__less__cancel__right_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_c),T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__strict__left__mono_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_b),T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__less__cancel__left_1,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_b),T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__less__cancel__left_0,axiom, % 0.48/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.48/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_c),V_b),T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__less__mono1_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_k),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_k),tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_nat__add__left__cancel__less_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n),tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_nat__add__left__cancel__less_1,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n),tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__is__1_5,axiom, % 0.48/0.64 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_Suc__lessD_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_less__SucI_0,axiom, % 0.48/0.64 ( c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_of__nat__add_0,axiom, % 0.48/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.48/0.64 | c_Nat_Osemiring__1__class_Oof__nat(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a)) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__is__1_1,axiom, % 0.48/0.64 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.64 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.64 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_add__is__1_2,axiom, % 0.48/0.64 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.64 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_lift_Osimps_I3_J_0,axiom, % 0.48/0.64 c_Lambda_Olift(c_Lambda_OdB_OAbs(V_s),V_k) = c_Lambda_OdB_OAbs(c_Lambda_Olift(V_s,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_converse__rtranclp__into__rtranclp_0,axiom, % 0.48/0.64 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_c)) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_rtranclp_Ortrancl__into__rtrancl_0,axiom, % 0.48/0.64 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_c)) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_c)) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_b)) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_accp_Ocases_0,axiom, % 0.48/0.64 ( c_Wellfounded_Oaccp(V_r,V_y,T_a) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(V_r,V_y),V_a)) % 0.48/0.64 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_accp__downward_0,axiom, % 0.48/0.64 ( c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.48/0.64 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) % 0.48/0.64 | ~ c_Wellfounded_Oaccp(V_r,V_b,T_a) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_list__app__typeE_1,axiom, % 0.48/0.64 ( 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.48/0.64 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_list__app__typeD_1,axiom, % 0.48/0.64 ( 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.48/0.64 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_lift__subst_0,axiom, % 0.48/0.64 ( c_Lambda_Olift(c_Lambda_Osubst(V_t,V_s,V_j),V_i) = c_Lambda_Osubst(c_Lambda_Olift(V_t,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat))),c_Lambda_Olift(V_s,V_i),V_j) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_j,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_lift__subst__lt_0,axiom, % 0.48/0.64 ( c_Lambda_Olift(c_Lambda_Osubst(V_t,V_s,V_j),V_i) = c_Lambda_Osubst(c_Lambda_Olift(V_t,V_i),c_Lambda_Olift(V_s,V_i),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),c_HOL_Oone__class_Oone(tc_nat))) % 0.48/0.64 | ~ c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_lift_Osimps_I1_J_1,axiom, % 0.48/0.64 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),c_HOL_Oone__class_Oone(tc_nat))) % 0.48/0.64 | c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_typing__elims_I3_J_0,axiom, % 0.48/0.64 ( V_T = hAPP(hAPP(c_Type_Otype_OFun,c_Type_Osko__Type__Xtyping__elims__3__1(V_T,V_e,V_t)),c_Type_Osko__Type__Xtyping__elims__3__2(V_T,V_e,V_t)) % 0.48/0.64 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.48/0.64 % 0.48/0.64 cnf(cls_var__app__types_0,axiom, % 0.48/0.65 ( V_U = c_List_Ofoldr(c_Type_Otype_OFun,c_Type_Osko__Type__Xvar__app__types__1__1(V_T,V_U,V_e,V_us),V_T,tc_Type_Otype,tc_Type_Otype) % 0.48/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_U) % 0.48/0.65 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.48/0.65 | ~ c_Type_Otyping(V_e,c_List_Ofoldl(c_Lambda_OdB_OApp,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_i),V_ts,tc_Lambda_OdB,tc_Lambda_OdB),V_us,tc_Lambda_OdB,tc_Lambda_OdB),V_T) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__neg__neg_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.48/0.65 | 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.48/0.65 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.48/0.65 | 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.48/0.65 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.48/0.65 | ~ 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.48/0.65 % 0.48/0.65 cnf(cls_even__less__0__iff_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.48/0.65 | ~ 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.48/0.65 % 0.48/0.65 cnf(cls_even__less__0__iff_1,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.48/0.65 | 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.48/0.65 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_not__one__less__zero_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Oone__class_Oone(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__pos__pos_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b),T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_zero__less__one_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oone__class_Oone(T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_pos__add__strict_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(V_b,hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_c),T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_of__nat__0_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.48/0.65 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_of__nat__less__iff_1,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_of__nat__less__iff_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a),T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__gr__0_1,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__gr__0_2,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_gr0__conv__Suc_1,axiom, % 0.48/0.65 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_x),tc_nat) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_zero__less__Suc_0,axiom, % 0.48/0.65 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_n),tc_nat) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__gr__0_0,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.48/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n),tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_less__Suc0_0,axiom, % 0.48/0.65 ( V_n = c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_less__Suc0_1,axiom, % 0.48/0.65 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_foldl__absorb0_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.48/0.65 | 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.48/0.65 % 0.48/0.65 cnf(cls_rtrancl__beta__App_0,axiom, % 0.48/0.65 ( 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.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) % 0.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_rtrancl__beta__AppL_0,axiom, % 0.48/0.65 ( 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.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_rtrancl__beta__AppR_0,axiom, % 0.48/0.65 ( 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.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_rtrancl__beta__Abs_0,axiom, % 0.48/0.65 ( 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.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_s),V_s_H)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_App__eq__foldl__conv_0,axiom, % 0.48/0.65 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_t,c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) % 0.48/0.65 | hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = V_t ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_App__eq__foldl__conv_4,axiom, % 0.48/0.65 hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s) = c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,V_r),V_s),c_List_Olist_ONil(tc_Lambda_OdB),tc_Lambda_OdB,tc_Lambda_OdB) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_subst__preserves__beta2_0,axiom, % 0.48/0.65 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_t,V_r,V_i)),c_Lambda_Osubst(V_t,V_s,V_i))) % 0.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_subst__preserves__beta_H_0,axiom, % 0.48/0.65 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_r,V_t,V_i)),c_Lambda_Osubst(V_s,V_t,V_i))) % 0.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_subst__preserves__beta2_H_0,axiom, % 0.48/0.65 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Osubst(V_t,V_r,V_i)),c_Lambda_Osubst(V_t,V_s,V_i))) % 0.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_head__Var__reduction_0,axiom, % 0.48/0.65 ( c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,c_ListBeta_Osko__ListBeta__Xhead__Var__reduction__1__1(V_n,V_rs,V_v),tc_Lambda_OdB) % 0.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_OdB_OVar(V_n),V_rs,tc_Lambda_OdB,tc_Lambda_OdB)),V_v)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_typing__elims_I2_J_1,axiom, % 0.48/0.65 ( c_Type_Otyping(V_e,V_u,c_Type_Osko__Type__Xtyping__elims__2__1(V_T,V_e,V_t,V_u)) % 0.48/0.65 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_subst__gt_0,axiom, % 0.48/0.65 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_j,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_subst__Var_0,axiom, % 0.48/0.65 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(c_HOL_Ominus__class_Ominus(V_i,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_type_Osize_I2_J_0,axiom, % 0.48/0.65 c_Type_Otype_Otype__size(hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Type_Otype_Otype__size(V_type1)),c_Type_Otype_Otype__size(V_type2))),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_type_Osize_I4_J_0,axiom, % 0.48/0.65 c_Nat_Osize__class_Osize(hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2),tc_Type_Otype) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osize__class_Osize(V_type1,tc_Type_Otype)),c_Nat_Osize__class_Osize(V_type2,tc_Type_Otype))),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__eq__if_1,axiom, % 0.48/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ominus__class_Ominus(V_m,c_HOL_Oone__class_Oone(tc_nat),tc_nat)),V_n)) % 0.48/0.65 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_Suc__diff__1_0,axiom, % 0.48/0.65 ( c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) = V_n % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_Suc__pred_H_0,axiom, % 0.48/0.65 ( V_n = c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_HOL_Oone__class_Oone(tc_nat),tc_nat)) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_dB_Osize_I6_J_0,axiom, % 0.48/0.65 c_Nat_Osize__class_Osize(c_Lambda_OdB_OAbs(V_dB),tc_Lambda_OdB) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osize__class_Osize(V_dB,tc_Lambda_OdB)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_dB_Osize_I3_J_0,axiom, % 0.48/0.65 c_Lambda_OdB_OdB__size(c_Lambda_OdB_OAbs(V_dB)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(V_dB)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_dB_Osize_I5_J_0,axiom, % 0.48/0.65 c_Nat_Osize__class_Osize(hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2),tc_Lambda_OdB) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Nat_Osize__class_Osize(V_dB1,tc_Lambda_OdB)),c_Nat_Osize__class_Osize(V_dB2,tc_Lambda_OdB))),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_dB_Osize_I2_J_0,axiom, % 0.48/0.65 c_Lambda_OdB_OdB__size(hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Lambda_OdB_OdB__size(V_dB1)),c_Lambda_OdB_OdB__size(V_dB2))),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_foldr__conv__foldl_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.48/0.65 | 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.48/0.65 % 0.48/0.65 cnf(cls_nat_Oinject_0,axiom, % 0.48/0.65 ( c_Suc(V_nat) != c_Suc(V_nat_H) % 0.48/0.65 | V_nat = V_nat_H ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_Suc__inject_0,axiom, % 0.48/0.65 ( c_Suc(V_x) != c_Suc(V_y) % 0.48/0.65 | V_x = V_y ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_double__eq__0__iff_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.48/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.48/0.65 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__is__0_1,axiom, % 0.48/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.65 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__is__0_0,axiom, % 0.48/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.65 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_natgb_Oadd__r0__iff_0,axiom, % 0.48/0.65 ( V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_a) % 0.48/0.65 | V_a = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__eq__self__zero_0,axiom, % 0.48/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != V_m % 0.48/0.65 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.48/0.65 | ~ class_Int_Onumber__ring(T_a) % 0.48/0.65 | V_x != hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_a) % 0.48/0.65 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_of__nat__eq__iff_0,axiom, % 0.48/0.65 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.48/0.65 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.48/0.65 | V_m = V_n ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_foldl__assoc_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Osemigroup__add(T_a) % 0.48/0.65 | 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.48/0.65 % 0.48/0.65 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_y) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_y),V_x) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_less__add__eq__less_0,axiom, % 0.48/0.65 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_l) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.48/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_nat__add__commute_0,axiom, % 0.48/0.65 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_m) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.48/0.65 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.48/0.65 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),V_b) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_b),V_a) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.48/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.65 | 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.48/0.65 % 0.48/0.65 cnf(cls_trans__less__add2_0,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_j),tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_trans__less__add1_0,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),V_m),tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__lessD1_0,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_j),V_k,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_termination__basic__simps_I2_J_0,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(V_x,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z),tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_z,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_termination__basic__simps_I1_J_0,axiom, % 0.48/0.65 ( c_HOL_Oord__class_Oless(V_x,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z),tc_nat) % 0.48/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_less__iff__Suc__add_1,axiom, % 0.48/0.65 c_HOL_Oord__class_Oless(V_m,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_x)),tc_nat) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_less__add__Suc2_0,axiom, % 0.48/0.65 c_HOL_Oord__class_Oless(V_i,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_i)),tc_nat) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_less__add__Suc1_0,axiom, % 0.48/0.65 c_HOL_Oord__class_Oless(V_i,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_i),V_m)),tc_nat) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_Zero__neq__Suc_0,axiom, % 0.48/0.65 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_nat_Osimps_I2_J_0,axiom, % 0.48/0.65 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__Suc_0,axiom, % 0.48/0.65 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(V_m)),V_n) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_add__Suc__right_0,axiom, % 0.48/0.65 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_Suc(V_n)) = c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_termi__implies__IT_0,axiom, % 0.48/0.65 ( hBOOL(hAPP(c_InductTermi_OIT,V_r)) % 0.48/0.65 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_r,tc_Lambda_OdB) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_IT__implies__termi_0,axiom, % 0.48/0.65 ( c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_t,tc_Lambda_OdB) % 0.48/0.65 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.48/0.65 % 0.48/0.65 cnf(cls_rtranclp__trans_0,axiom, % 0.48/0.65 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_z)) % 0.48/0.65 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_z)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_y)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_accp__downwards__aux_0,axiom, % 0.48/0.66 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.48/0.66 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_accp__downwards_0,axiom, % 0.48/0.66 ( c_Wellfounded_Oaccp(V_r,V_b,T_a) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_b),V_a)) % 0.48/0.66 | ~ c_Wellfounded_Oaccp(V_r,V_a,T_a) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Nitpick_Ortranclp__def_1,axiom, % 0.48/0.66 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_x),V_x)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_rtranclp_Ortrancl__refl_0,axiom, % 0.48/0.66 hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_a),V_a)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_listsp_ONil_0,axiom, % 0.48/0.66 c_List_Olistsp(V_A,c_List_Olist_ONil(T_a),T_a) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__is__1_4,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Suc__eq__plus1__left_0,axiom, % 0.48/0.66 c_Suc(V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),V_n) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Suc__eq__plus1_0,axiom, % 0.48/0.66 c_Suc(V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),c_HOL_Oone__class_Oone(tc_nat)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_double__eq__0__iff_1,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_add__is__0_2,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_add__cancel__21_1,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_nat__add__left__commute_0,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),V_z)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_y),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_z)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_nat__add__assoc_0,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n)),V_k) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_k)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_conversep_Ointros_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_b),V_a)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(V_r,V_a),V_b)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_conversep_Ocases_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(V_r,V_a2),V_a1)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a1),V_a2)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_conversep__iff_1,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(V_r,V_b),V_a)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_conversepD_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(V_r,V_b),V_a)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Predicate_Oconversep(V_r,T_a,T_b),V_a),V_b)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__cancel__21_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.48/0.66 | 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.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),V_z) = V_u ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_foldr_Osimps_I1_J_0,axiom, % 0.48/0.66 c_List_Ofoldr(V_f,c_List_Olist_ONil(T_b),V_a,T_b,T_a) = V_a ). % 0.48/0.66 % 0.48/0.66 cnf(cls_one__is__add_5,axiom, % 0.48/0.66 c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_of__nat__1_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.48/0.66 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oone__class_Oone(tc_nat),T_a) = c_HOL_Oone__class_Oone(T_a) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_zero__neq__one_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ozero__neq__one(T_a) % 0.48/0.66 | c_HOL_Ozero__class_Ozero(T_a) != c_HOL_Oone__class_Oone(T_a) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_one__is__add_3,axiom, % 0.48/0.66 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.48/0.66 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.66 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_one__is__add_0,axiom, % 0.48/0.66 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) % 0.48/0.66 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.66 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_of__nat__Suc_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.48/0.66 | c_Nat_Osemiring__1__class_Oof__nat(c_Suc(V_m),T_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Oone__class_Oone(T_a)),c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__Suc__shift_0,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Suc(V_m)),V_n) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_Suc(V_n)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_rtranclp__converseD_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_rtranclp__converseI_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Predicate_Oconversep(V_r,T_a,T_a),T_a),V_x),V_y)) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(V_r,T_a),V_y),V_x)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_foldl__foldr1__lemma_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_Suc__lessI_0,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) % 0.48/0.66 | c_Suc(V_m) = V_n % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_natgb_Oadd__cancel_0,axiom, % 0.48/0.66 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_y) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),V_z) % 0.48/0.66 | V_y = V_z ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_nat__add__right__cancel_0,axiom, % 0.48/0.66 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_k) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_n),V_k) % 0.48/0.66 | V_m = V_n ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_nat__add__left__cancel_0,axiom, % 0.48/0.66 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_m) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),V_n) % 0.48/0.66 | V_m = V_n ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.48/0.66 | ~ class_Int_Onumber__ring(T_a) % 0.48/0.66 | 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.48/0.66 | V_y = V_z ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__imp__eq_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.48/0.66 | 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.48/0.66 | V_b = V_c ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__left__cancel_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.48/0.66 | 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.48/0.66 | V_b = V_c ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__right__cancel_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.48/0.66 | 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.48/0.66 | V_b = V_c ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_subst__subst_0,axiom, % 0.48/0.66 ( c_Lambda_Osubst(c_Lambda_Osubst(V_t,c_Lambda_Olift(V_v,V_i),c_Suc(V_j)),c_Lambda_Osubst(V_u,V_v,V_j),V_i) = c_Lambda_Osubst(c_Lambda_Osubst(V_t,V_u,V_i),V_v,V_j) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_j),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__is__1_3,axiom, % 0.48/0.66 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.66 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.66 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__is__1_0,axiom, % 0.48/0.66 ( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),V_n) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.48/0.66 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.48/0.66 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | 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.48/0.66 % 0.48/0.66 cnf(cls_not__less__less__Suc__eq_1,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.48/0.66 | c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_not__less__eq_1,axiom, % 0.48/0.66 ( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_not__less__eq_0,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.48/0.66 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_lift__lift_0,axiom, % 0.48/0.66 ( c_Lambda_Olift(c_Lambda_Olift(V_t,V_i),c_Suc(V_k)) = c_Lambda_Olift(c_Lambda_Olift(V_t,V_k),V_i) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_i,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)),tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_zero__less__two_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.66 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Oone__class_Oone(T_a)),c_HOL_Oone__class_Oone(T_a)),T_a) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_rtranclp__idemp_0,axiom, % 0.48/0.66 c_Transitive__Closure_Ortranclp(c_Transitive__Closure_Ortranclp(V_r,T_a),T_a) = c_Transitive__Closure_Ortranclp(V_r,T_a) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_x) = V_x ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_natgb_Oadd__r0__iff_1,axiom, % 0.48/0.66 V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_x),c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_plus__nat_Oadd__0_0,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),V_n) = V_n ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Nat_Oadd__0__right_0,axiom, % 0.48/0.66 hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_m),c_HOL_Ozero__class_Ozero(tc_nat)) = V_m ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.48/0.66 | ~ class_Int_Onumber__ring(T_a) % 0.48/0.66 | V_x = hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_x),c_HOL_Ozero__class_Ozero(T_a)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_add__0__left_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.48/0.66 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),V_a),c_HOL_Ozero__class_Ozero(T_a)) = V_a ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.48/0.66 | hAPP(hAPP(c_HOL_Oplus__class_Oplus(T_a),c_HOL_Ozero__class_Ozero(T_a)),V_a) = V_a ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_less__Suc__eq__0__disj_3,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(c_Suc(V_x),c_Suc(V_n),tc_nat) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_x,V_n,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Suc__less__eq_0,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Suc__mono_0,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_subst__Abs_0,axiom, % 0.48/0.66 c_Lambda_Osubst(c_Lambda_OdB_OAbs(V_t),V_s,V_k) = c_Lambda_OdB_OAbs(c_Lambda_Osubst(V_t,c_Lambda_Olift(V_s,c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),V_k),c_HOL_Oone__class_Oone(tc_nat)))) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_var__app__types_1,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ 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.48/0.66 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_var__app__typesE_1,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_subject__reduction_H_0,axiom, % 0.48/0.66 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.48/0.66 | ~ c_Type_Otyping(V_e,V_t,V_T) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_t),V_t_H)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_list__app__typeD_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_list__app__typeI_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ c_Type_Otypings(V_e,V_ts,V_Ts) % 0.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_list__app__typeE_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_lift__preserves__beta_H_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_shift__commute_0,axiom, % 0.48/0.66 c_Type_Oshift(c_Type_Oshift(V_e,V_i,V_U,T_a),c_HOL_Ozero__class_Ozero(tc_nat),V_T,T_a) = c_Type_Oshift(c_Type_Oshift(V_e,c_HOL_Ozero__class_Ozero(tc_nat),V_T,T_a),c_Suc(V_i),V_U,T_a) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_typing__elims_I3_J_1,axiom, % 0.48/0.66 ( c_Type_Otyping(c_Type_Oshift(V_e,c_HOL_Ozero__class_Ozero(tc_nat),c_Type_Osko__Type__Xtyping__elims__3__1(V_T,V_e,V_t),tc_Type_Otype),V_t,c_Type_Osko__Type__Xtyping__elims__3__2(V_T,V_e,V_t)) % 0.48/0.66 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_abs__typeE_0,axiom, % 0.48/0.66 ( c_Type_Otyping(c_Type_Oshift(V_e,c_HOL_Ozero__class_Ozero(tc_nat),c_Type_Osko__Type__Xabs__typeE__1__1(V_e,V_t),tc_Type_Otype),V_t,c_Type_Osko__Type__Xabs__typeE__1__2(V_e,V_t)) % 0.48/0.66 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OAbs(V_t),V_T) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_var__app__typesE_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_double__induction__lemma_0,axiom, % 0.48/0.66 ( ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) % 0.48/0.66 | ~ c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),V_s,tc_Lambda_OdB) % 0.48/0.66 | c_Wellfounded_Oaccp(c_Predicate_Oconversep(c_Lambda_Obeta,tc_Lambda_OdB,tc_Lambda_OdB),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_r)),V_s),V_ss,tc_Lambda_OdB,tc_Lambda_OdB),tc_Lambda_OdB) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_apps__preserves__betas_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ c_ListOrder_Ostep1(c_Lambda_Obeta,V_rs,V_ss,tc_Lambda_OdB) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_apps__preserves__beta2_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Transitive__Closure_Ortranclp(c_Lambda_Obeta,tc_Lambda_OdB),V_r),V_s)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_apps__eq__Abs__conv_2,axiom, % 0.48/0.66 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.48/0.66 % 0.48/0.66 cnf(cls_apps__eq__Abs__conv_1,axiom, % 0.48/0.66 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.48/0.66 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Abs__eq__apps__conv_2,axiom, % 0.48/0.66 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.48/0.66 % 0.48/0.66 cnf(cls_Abs__eq__apps__conv_1,axiom, % 0.48/0.66 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.48/0.66 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Var__eq__apps__conv_1,axiom, % 0.48/0.66 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.48/0.66 | V_ss = c_List_Olist_ONil(tc_Lambda_OdB) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Var__eq__apps__conv_2,axiom, % 0.48/0.66 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.48/0.66 % 0.48/0.66 cnf(cls_typing__elims_I2_J_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ c_Type_Otyping(V_e,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_T) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.66 | 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.48/0.66 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.48/0.66 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.48/0.66 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_head__Var__reduction_1,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ 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.48/0.66 % 0.48/0.66 cnf(cls_IT_OVar_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ c_List_Olistsp(c_InductTermi_OIT,V_rs,tc_Lambda_OdB) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Beta_I5_J_0,axiom, % 0.48/0.66 c_Type_Otyping(c_Type_Oshift(v_ea______,v_ia______,v_T____,tc_Type_Otype),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r____)),v_a____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_T_Ha______) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.48/0.66 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_abs_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OAbs(V_s)),c_Lambda_OdB_OAbs(V_t))) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Abs__App__neq__Var__apps_0,axiom, % 0.48/0.66 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.48/0.66 % 0.48/0.66 cnf(cls_app__Var__IT_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(c_InductTermi_OIT,hAPP(hAPP(c_Lambda_OdB_OApp,V_t),c_Lambda_OdB_OVar(V_i)))) % 0.48/0.66 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_lift__preserves__beta_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Olift(V_r,V_i)),c_Lambda_Olift(V_s,V_i))) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.48/0.66 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_subst__lift_0,axiom, % 0.48/0.66 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.48/0.66 % 0.48/0.66 cnf(cls_uIT_0,axiom, % 0.48/0.66 hBOOL(hAPP(c_InductTermi_OIT,v_u____)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_appL_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_appR_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_s),V_t)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Lambda_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OAbs(V_r))) % 0.48/0.66 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_apps__eq__tail__conv_0,axiom, % 0.48/0.66 ( 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.48/0.66 | V_r = V_s ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Abs__eq__apps__conv_0,axiom, % 0.48/0.66 ( c_Lambda_OdB_OAbs(V_r) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.48/0.66 | c_Lambda_OdB_OAbs(V_r) = V_s ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_subst__Var_1,axiom, % 0.48/0.66 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.48/0.66 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_not__less0_0,axiom, % 0.48/0.66 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_gr__implies__not0_0,axiom, % 0.48/0.66 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_xt1_I10_J_0,axiom, % 0.48/0.66 ( ~ class_Orderings_Oorder(T_a) % 0.48/0.66 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_order__less__trans_0,axiom, % 0.48/0.66 ( ~ class_Orderings_Opreorder(T_a) % 0.48/0.66 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.48/0.66 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Beta_I6_J_0,axiom, % 0.48/0.66 hBOOL(hAPP(c_InductTermi_OIT,v_ua______)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_subst__Var_2,axiom, % 0.48/0.66 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.48/0.66 | V_i = V_k % 0.48/0.66 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_subst__preserves__beta_0,axiom, % 0.48/0.66 ( hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_Osubst(V_r,V_t,V_i)),c_Lambda_Osubst(V_s,V_t,V_i))) % 0.48/0.66 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.48/0.66 c_Lambda_Olift(hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Olift(V_s,V_k)),c_Lambda_Olift(V_t,V_k)) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_Var__IT_0,axiom, % 0.48/0.66 hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_OdB_OVar(V_n))) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.48/0.66 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.48/0.66 % 0.48/0.66 cnf(cls_IT_OBeta_0,axiom, % 0.48/0.66 ( 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.48/0.66 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_s)) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_r,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_ss,tc_Lambda_OdB,tc_Lambda_OdB))) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_lift__IT_0,axiom, % 0.48/0.67 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Olift(V_t,V_i))) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Var__apps__neq__Abs__apps_0,axiom, % 0.48/0.67 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.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.48/0.67 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.48/0.67 | V_dB = V_dB_H ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.48/0.67 c_Lambda_OdB_OVar(V_nat) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Var__eq__apps__conv_0,axiom, % 0.48/0.67 ( c_Lambda_OdB_OVar(V_m) != c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) % 0.48/0.67 | c_Lambda_OdB_OVar(V_m) = V_s ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_apps__preserves__beta_0,axiom, % 0.48/0.67 ( 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.48/0.67 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_r),V_s)) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_nat__less__le_1,axiom, % 0.48/0.67 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_less__not__refl_0,axiom, % 0.48/0.67 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_order__less__le_1,axiom, % 0.48/0.67 ( ~ class_Orderings_Oorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_linorder__neq__iff_1,axiom, % 0.48/0.67 ( ~ class_Orderings_Olinorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_order__less__irrefl_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Opreorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_beta_0,axiom, % 0.48/0.67 hBOOL(hAPP(hAPP(c_Lambda_Obeta,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(V_s)),V_t)),c_Lambda_Osubst(V_s,V_t,c_HOL_Ozero__class_Ozero(tc_nat)))) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.48/0.67 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.48/0.67 | V_x = V_y ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Olinorder(T_a) % 0.48/0.67 | V_x = V_y % 0.48/0.67 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_nat__neq__iff_0,axiom, % 0.48/0.67 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.48/0.67 | V_m = V_n ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_nat__less__cases_0,axiom, % 0.48/0.67 ( hBOOL(hAPP(hAPP(V_P,V_n),V_m)) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.48/0.67 | V_m = V_n % 0.48/0.67 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_var__app__type__eq_0,axiom, % 0.48/0.67 ( V_T = V_U % 0.48/0.67 | ~ 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.48/0.67 | ~ 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.48/0.67 % 0.48/0.67 cnf(cls_linorder__neqE__nat_0,axiom, % 0.48/0.67 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.48/0.67 | V_x = V_y ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_linorder__neqE_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Olinorder(T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.48/0.67 | V_x = V_y ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_linorder__less__linear_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Olinorder(T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.48/0.67 | V_x = V_y % 0.48/0.67 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Olinorder(T_a) % 0.48/0.67 | V_x = V_y % 0.48/0.67 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.48/0.67 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.48/0.67 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.48/0.67 | V_dB2 = V_dB2_H ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.48/0.67 ( hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1_H),V_dB2_H) % 0.48/0.67 | V_dB1 = V_dB1_H ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Abs__apps__eq__Abs__apps__conv_1,axiom, % 0.48/0.67 ( 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.48/0.67 | V_rs = V_ss ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Abs__apps__eq__Abs__apps__conv_0,axiom, % 0.48/0.67 ( 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.48/0.67 | V_r = V_s ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_apps__eq__Abs__conv_0,axiom, % 0.48/0.67 ( c_List_Ofoldl(c_Lambda_OdB_OApp,V_s,V_ss,tc_Lambda_OdB,tc_Lambda_OdB) != c_Lambda_OdB_OAbs(V_r) % 0.48/0.67 | V_s = c_Lambda_OdB_OAbs(V_r) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_App_0,axiom, % 0.48/0.67 ( c_Type_Otyping(V_env,hAPP(hAPP(c_Lambda_OdB_OApp,V_s),V_t),V_U) % 0.48/0.67 | ~ c_Type_Otyping(V_env,V_t,V_T) % 0.48/0.67 | ~ c_Type_Otyping(V_env,V_s,hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_beta__cases_I1_J_0,axiom, % 0.48/0.67 ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,c_Lambda_OdB_OVar(V_i)),V_t)) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_SI1_0,axiom, % 0.48/0.67 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r____,v_a____,c_HOL_Ozero__class_Ozero(tc_nat)),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),V_u,V_i))) % 0.48/0.67 | ~ c_Type_Otyping(V_e,V_u,v_T____) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,v_T____,tc_Type_Otype),c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r____,v_a____,c_HOL_Ozero__class_Ozero(tc_nat)),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),V_T_H) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_gr0I_0,axiom, % 0.48/0.67 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.48/0.67 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_neq0__conv_1,axiom, % 0.48/0.67 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_subst__lt_0,axiom, % 0.48/0.67 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_subst__Var__IT_0,axiom, % 0.48/0.67 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j))) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_r)) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_type_Osimps_I2_J_1,axiom, % 0.48/0.67 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.48/0.67 | V_type2 = V_type2_H ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_type_Osimps_I2_J_0,axiom, % 0.48/0.67 ( hAPP(hAPP(c_Type_Otype_OFun,V_type1),V_type2) != hAPP(hAPP(c_Type_Otype_OFun,V_type1_H),V_type2_H) % 0.48/0.67 | V_type1 = V_type1_H ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_subst__eq_0,axiom, % 0.48/0.67 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Var__apps__eq__Var__apps__conv_1,axiom, % 0.48/0.67 ( 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.48/0.67 | V_rs = V_ss ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Var__apps__eq__Var__apps__conv_0,axiom, % 0.48/0.67 ( 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.48/0.67 | V_m = V_n ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.48/0.67 c_Lambda_OdB_OAbs(V_dB_H) != hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Beta_I1_J_0,axiom, % 0.48/0.67 hBOOL(hAPP(c_InductTermi_OIT,c_List_Ofoldl(c_Lambda_OdB_OApp,c_Lambda_Osubst(v_r____,v_a____,c_HOL_Ozero__class_Ozero(tc_nat)),v_as____,tc_Lambda_OdB,tc_Lambda_OdB))) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.48/0.67 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.48/0.67 | V_nat = V_nat_H ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.48/0.67 hAPP(hAPP(c_Lambda_OdB_OApp,V_dB1),V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.48/0.67 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_subst__App_0,axiom, % 0.48/0.67 c_Lambda_Osubst(hAPP(hAPP(c_Lambda_OdB_OApp,V_t),V_u),V_s,V_k) = hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_Osubst(V_t,V_s,V_k)),c_Lambda_Osubst(V_u,V_s,V_k)) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_xt1_I9_J_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Oorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.48/0.67 ( ~ class_Orderings_Olinorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_order__less__asym_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Opreorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_order__less__asym_H_0,axiom, % 0.48/0.67 ( ~ class_Orderings_Opreorder(T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_lift__type_0,axiom, % 0.48/0.67 ( c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_U,tc_Type_Otype),c_Lambda_Olift(V_t,V_i),V_T) % 0.48/0.67 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_SI2_0,axiom, % 0.48/0.67 ( hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(v_a____,V_u,V_i))) % 0.48/0.67 | ~ c_Type_Otyping(V_e,V_u,v_T____) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,v_T____,tc_Type_Otype),v_a____,V_T_H) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_uT_0,axiom, % 0.48/0.67 c_Type_Otyping(v_e____,v_u____,v_T____) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Beta_I3_J_0,axiom, % 0.48/0.67 hBOOL(hAPP(c_InductTermi_OIT,v_a____)) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_subject__reduction_0,axiom, % 0.48/0.67 ( c_Type_Otyping(V_e,V_t_H,V_T) % 0.48/0.67 | ~ hBOOL(hAPP(hAPP(c_Lambda_Obeta,V_t),V_t_H)) % 0.48/0.67 | ~ c_Type_Otyping(V_e,V_t,V_T) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_shift__gt_0,axiom, % 0.48/0.67 ( hAPP(c_Type_Oshift(V_e,V_i,V_T,T_a),V_j) = hAPP(V_e,V_j) % 0.48/0.67 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_MI2_0,axiom, % 0.48/0.67 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.48/0.67 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.48/0.67 | ~ c_Type_Otyping(V_e,V_u,V_T2) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T2,tc_Type_Otype),V_t,V_Ta) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_MI1_0,axiom, % 0.48/0.67 ( v_T____ != hAPP(hAPP(c_Type_Otype_OFun,V_T1),V_T2) % 0.48/0.67 | hBOOL(hAPP(c_InductTermi_OIT,c_Lambda_Osubst(V_t,V_u,V_i))) % 0.48/0.67 | ~ c_Type_Otyping(V_e,V_u,V_T1) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_u)) % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(V_e,V_i,V_T1,tc_Type_Otype),V_t,V_Ta) % 0.48/0.67 | ~ hBOOL(hAPP(c_InductTermi_OIT,V_t)) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_shift__eq_0,axiom, % 0.48/0.67 hAPP(c_Type_Oshift(V_e,V_x,V_T,T_a),V_x) = V_T ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Abs_0,axiom, % 0.48/0.67 ( c_Type_Otyping(V_env,c_Lambda_OdB_OAbs(V_t),hAPP(hAPP(c_Type_Otype_OFun,V_T),V_U)) % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(V_env,c_HOL_Ozero__class_Ozero(tc_nat),V_T,tc_Type_Otype),V_t,V_U) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_typing__elims_I1_J_0,axiom, % 0.48/0.67 ( hAPP(V_e,V_i) = V_T % 0.48/0.67 | ~ c_Type_Otyping(V_e,c_Lambda_OdB_OVar(V_i),V_T) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_Beta_I7_J_0,axiom, % 0.48/0.67 c_Type_Otyping(v_ea______,v_ua______,v_T____) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_T_0,axiom, % 0.48/0.67 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),c_List_Ofoldl(c_Lambda_OdB_OApp,hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r____)),v_a____),v_as____,tc_Lambda_OdB,tc_Lambda_OdB),v_T_H____) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_that_0,axiom, % 0.48/0.67 ( v_thesis____ % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,V_T_H_H) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_typing_OVar_0,axiom, % 0.48/0.67 c_Type_Otyping(V_env,c_Lambda_OdB_OVar(V_x),hAPP(V_env,V_x)) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_subst__lemma_0,axiom, % 0.48/0.67 ( ~ c_Type_Otyping(V_e_H,V_u,V_U) % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(V_e_H,V_i,V_U,tc_Type_Otype),V_t,V_T) % 0.48/0.67 | c_Type_Otyping(V_e_H,c_Lambda_Osubst(V_t,V_u,V_i),V_T) ) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_CHAINED_0,axiom, % 0.48/0.67 c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),hAPP(hAPP(c_Lambda_OdB_OApp,c_Lambda_OdB_OAbs(v_r____)),v_a____),v_Ua____) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_conjecture_0,negated_conjecture, % 0.48/0.67 ~ v_thesis____ ). % 0.48/0.67 % 0.48/0.67 cnf(cls_conjecture_1,negated_conjecture, % 0.48/0.67 ( v_thesis____ % 0.48/0.67 | ~ c_Type_Otyping(c_Type_Oshift(v_e____,v_i____,v_T____,tc_Type_Otype),v_a____,V_x) ) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_fun__Orderings_Opreorder,axiom, % 0.48/0.67 ( class_Orderings_Opreorder(tc_fun(T_2,T_1)) % 0.48/0.67 | ~ class_Orderings_Opreorder(T_1) ) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_fun__Orderings_Oorder,axiom, % 0.48/0.67 ( class_Orderings_Oorder(tc_fun(T_2,T_1)) % 0.48/0.67 | ~ class_Orderings_Oorder(T_1) ) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.48/0.67 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.48/0.67 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.48/0.67 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.48/0.67 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.48/0.67 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.48/0.67 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.48/0.67 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.48/0.67 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.48/0.67 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Ring__and__Field_Ozero__neq__one,axiom, % 0.48/0.67 class_Ring__and__Field_Ozero__neq__one(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Osemigroup__add,axiom, % 0.48/0.67 class_OrderedGroup_Osemigroup__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.48/0.67 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.48/0.67 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.48/0.67 class_Nat_Osemiring__char__0(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.48/0.67 class_Orderings_Opreorder(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.48/0.67 class_Orderings_Olinorder(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.48/0.67 class_Orderings_Oorder(tc_nat) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_bool__Orderings_Opreorder,axiom, % 0.48/0.67 class_Orderings_Opreorder(tc_bool) ). % 0.48/0.67 % 0.48/0.67 cnf(clsarity_bool__Orderings_Oorder,axiom, % 0.48/0.67 class_Orderings_Oorder(tc_bool) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_ATP__Linkup_Oequal__imp__fequal_0,axiom, % 0.48/0.67 hBOOL(hAPP(hAPP(c_fequal(T_a),V_x),V_x)) ). % 0.48/0.67 % 0.48/0.67 cnf(cls_ATP__Linkup_Ofequal__imp__equal_0,axiom, % 0.48/0.67 ( V_X = V_Y % 0.48/0.67 | ~ hBOOL(hAPP(hAPP(c_fequal(T_a),V_X),V_Y)) ) ). % 0.48/0.67 % 0.48/0.67 %------------------------------------------------------------------------------ % 0.48/0.67 %------------------------------------------- % 0.48/0.67 % Proof found % 0.48/0.67 % SZS status Theorem for theBenchmark % 0.48/0.67 % SZS output start Proof % 0.48/0.67 %ClaNum:513(EqnAxiom:125) % 0.48/0.67 %VarNum:1932(SingletonVarNum:854) % 0.48/0.67 %MaxLitNum:6 % 0.48/0.67 %MaxfuncDepth:5 % 0.48/0.67 %SharedTerms:83 % 0.48/0.67 %goalClause: 225 456 % 0.48/0.67 %singleGoalClaCount:1 % 0.48/0.67 [126]P1(a1) % 0.48/0.67 [127]P2(a1) % 0.48/0.67 [128]P3(a1) % 0.48/0.67 [129]P21(a1) % 0.48/0.67 [130]P19(a1) % 0.48/0.67 [131]P30(a1) % 0.48/0.67 [132]P22(a1) % 0.48/0.67 [133]P4(a1) % 0.48/0.67 [134]P5(a1) % 0.48/0.67 [135]P23(a1) % 0.48/0.67 [136]P24(a1) % 0.48/0.67 [137]P14(a1) % 0.48/0.67 [138]P15(a1) % 0.48/0.67 [139]P16(a1) % 0.48/0.67 [140]P25(a1) % 0.48/0.67 [141]P25(a2) % 0.48/0.67 [142]P27(a1) % 0.48/0.67 [143]P27(a2) % 0.48/0.67 [144]P26(a1) % 0.48/0.67 [151]P6(a46,a52,a41) % 0.48/0.67 [152]P6(a47,a45,a41) % 0.48/0.67 [225]~P32(a5000) % 0.48/0.67 [147]P31(f22(a8,a40)) % 0.48/0.67 [148]P31(f22(a8,a45)) % 0.48/0.67 [149]P31(f22(a8,a52)) % 0.48/0.67 [211]P6(f28(a47,a49,a41,a38),f22(f22(a11,f9(a50)),a40),a44) % 0.48/0.67 [222]P6(f28(a46,a51,a41,a38),f18(a11,f22(f22(a11,f9(a50)),a40),a48,a13,a13),a42) % 0.48/0.67 [223]P6(f28(a47,a49,a41,a38),f18(a11,f22(f22(a11,f9(a50)),a40),a48,a13,a13),a43) % 0.48/0.67 [224]P31(f22(a8,f18(a11,f16(a50,a40,f4(a1)),a48,a13,a13))) % 0.48/0.67 [239]~P8(x2391,x2391,a1) % 0.48/0.67 [157]E(f6(x1571,x1571,a1),f4(a1)) % 0.48/0.67 [241]~P8(x2411,f4(a1),a1) % 0.48/0.67 [145]E(f12(f3(x1451)),f4(a1)) % 0.48/0.67 [146]E(f14(f3(x1461),a13),f4(a1)) % 0.48/0.67 [150]P31(f22(a8,f3(x1501))) % 0.48/0.67 [154]E(f22(f22(f5(a1),x1541),f4(a1)),x1541) % 0.48/0.67 [158]E(f6(x1581,f4(a1),a1),x1581) % 0.48/0.67 [161]E(f6(f4(a1),x1611,a1),f4(a1)) % 0.48/0.67 [164]E(f24(f25(x1641),x1641,x1641),f25(x1641)) % 0.48/0.67 [174]P8(x1741,f22(f22(f5(a1),x1741),f7(a1)),a1) % 0.48/0.67 [176]P8(f4(a1),f22(f22(f5(a1),x1761),f7(a1)),a1) % 0.48/0.67 [233]~E(f22(f22(f5(a1),x2331),f7(a1)),x2331) % 0.48/0.67 [237]~E(f22(f22(f5(a1),x2371),f7(a1)),f4(a1)) % 0.48/0.67 [155]E(f22(f22(f5(a1),f4(a1)),x1551),x1551) % 0.48/0.67 [180]E(f22(f22(f5(a1),f12(x1801)),f22(f22(f5(a1),f4(a1)),f7(a1))),f12(f9(x1801))) % 0.48/0.67 [186]E(f22(f22(f5(a1),f14(x1861,a13)),f22(f22(f5(a1),f4(a1)),f7(a1))),f14(f9(x1861),a13)) % 0.48/0.67 [162]P7(x1621,f15(x1622),x1622) % 0.48/0.67 [166]P6(x1661,f3(x1662),f22(x1661,x1662)) % 0.48/0.67 [227]~E(f9(x2271),f3(x2272)) % 0.48/0.67 [156]E(f23(f23(x1561,x1562),x1562),f23(x1561,x1562)) % 0.48/0.67 [163]E(f16(f3(x1631),x1632,x1631),x1632) % 0.48/0.67 [188]P8(f6(x1881,x1882,a1),f22(f22(f5(a1),x1881),f7(a1)),a1) % 0.48/0.67 [207]P8(x2071,f22(f22(f5(a1),f22(f22(f5(a1),x2072),x2071)),f7(a1)),a1) % 0.48/0.67 [209]P8(x2091,f22(f22(f5(a1),f22(f22(f5(a1),x2091),x2092)),f7(a1)),a1) % 0.48/0.67 [167]E(f22(f22(f5(a1),x1671),x1672),f22(f22(f5(a1),x1672),x1671)) % 0.48/0.67 [169]P31(f22(f22(f25(x1691),x1692),x1692)) % 0.48/0.67 [194]E(f6(x1941,f22(f22(f5(a1),x1942),f7(a1)),a1),f6(f6(x1941,f7(a1),a1),x1942,a1)) % 0.48/0.67 [204]E(f22(f22(f5(a1),f22(f22(f5(a1),f12(x2041)),f12(x2042))),f22(f22(f5(a1),f4(a1)),f7(a1))),f12(f22(f22(a11,x2041),x2042))) % 0.48/0.67 [205]E(f22(f22(f5(a1),f22(f22(f5(a1),f26(x2051)),f26(x2052))),f22(f22(f5(a1),f4(a1)),f7(a1))),f26(f22(f22(a27,x2051),x2052))) % 0.48/0.67 [212]P31(f22(f22(a10,f22(f22(a11,f9(x2121)),x2122)),f16(x2121,x2122,f4(a1)))) % 0.48/0.67 [213]E(f22(f22(f5(a1),f22(f22(f5(a1),f14(x2131,a13)),f14(x2132,a13))),f22(f22(f5(a1),f4(a1)),f7(a1))),f14(f22(f22(a11,x2131),x2132),a13)) % 0.48/0.67 [214]E(f22(f22(f5(a1),f22(f22(f5(a1),f14(x2141,a38)),f14(x2142,a38))),f22(f22(f5(a1),f4(a1)),f7(a1))),f14(f22(f22(a27,x2141),x2142),a38)) % 0.48/0.67 [243]~P31(f22(f22(a10,f3(x2431)),x2432)) % 0.48/0.67 [244]~P8(f22(f22(f5(a1),x2441),x2442),x2442,a1) % 0.48/0.67 [245]~P8(f22(f22(f5(a1),x2451),x2452),x2451,a1) % 0.48/0.67 [170]E(f6(f22(f22(f5(a1),x1701),x1702),x1702,a1),x1701) % 0.48/0.67 [171]E(f6(f22(f22(f5(a1),x1711),x1712),x1711,a1),x1712) % 0.48/0.67 [172]E(f6(x1721,f22(f22(f5(a1),x1721),x1722),a1),f4(a1)) % 0.48/0.67 [187]E(f9(f17(x1871,f22(f22(f5(a1),x1872),f7(a1)))),f17(f9(x1871),x1872)) % 0.48/0.67 [200]E(f22(f22(f5(a1),f22(f22(f5(a1),x2001),f7(a1))),x2002),f22(f22(f5(a1),x2001),f22(f22(f5(a1),x2002),f7(a1)))) % 0.48/0.67 [202]E(f22(f22(f5(a1),f22(f22(f5(a1),x2021),f7(a1))),x2022),f22(f22(f5(a1),f22(f22(f5(a1),x2021),x2022)),f7(a1))) % 0.48/0.67 [246]~P9(x2461,x2462,f15(x2463),x2463) % 0.48/0.67 [247]~P9(x2471,f15(x2472),x2473,x2472) % 0.48/0.67 [165]E(f16(f17(x1651,x1652),x1653,x1652),x1651) % 0.48/0.67 [178]E(f24(f24(x1781,x1782,x1783),x1783,x1782),x1781) % 0.48/0.67 [195]E(f6(f6(x1951,x1952,a1),x1953,a1),f6(f6(x1951,x1953,a1),x1952,a1)) % 0.48/0.67 [228]~E(f3(x2281),f22(f22(a11,x2282),x2283)) % 0.48/0.67 [229]~E(f9(x2291),f22(f22(a11,x2292),x2293)) % 0.48/0.67 [230]~E(f22(f22(a11,x2301),x2302),f3(x2303)) % 0.48/0.67 [231]~E(f22(f22(a11,x2311),x2312),f9(x2313)) % 0.48/0.67 [182]P31(f22(f22(f23(x1821,x1822),x1823),x1823)) % 0.48/0.67 [183]E(f22(f22(a11,f17(x1831,x1832)),f17(x1833,x1832)),f17(f22(f22(a11,x1831),x1833),x1832)) % 0.48/0.67 [210]E(f6(f6(f22(f22(f5(a1),x2101),f7(a1)),x2102,a1),f22(f22(f5(a1),x2103),f7(a1)),a1),f6(f6(x2101,x2102,a1),x2103,a1)) % 0.48/0.67 [189]E(f22(f22(f5(a1),x1891),f22(f22(f5(a1),x1892),x1893)),f22(f22(f5(a1),x1892),f22(f22(f5(a1),x1891),x1893))) % 0.48/0.67 [190]E(f6(f22(f22(f5(a1),x1901),x1902),f22(f22(f5(a1),x1903),x1902),a1),f6(x1901,x1903,a1)) % 0.48/0.67 [191]E(f6(f22(f22(f5(a1),x1911),x1912),f22(f22(f5(a1),x1911),x1913),a1),f6(x1912,x1913,a1)) % 0.48/0.67 [193]E(f6(x1931,f22(f22(f5(a1),x1932),x1933),a1),f6(f6(x1931,x1932,a1),x1933,a1)) % 0.48/0.67 [201]E(f9(f16(x2011,f17(x2012,f4(a1)),f22(f22(f5(a1),x2013),f7(a1)))),f16(f9(x2011),x2012,x2013)) % 0.48/0.67 [198]E(f22(f22(f5(a1),f22(f22(f5(a1),x1981),x1982)),x1983),f22(f22(f5(a1),x1981),f22(f22(f5(a1),x1982),x1983))) % 0.48/0.67 [206]E(f22(f28(x2061,x2062,x2063,x2064),x2062),x2063) % 0.48/0.67 [215]E(f18(x2151,x2152,f15(x2153),x2154,x2153),x2152) % 0.48/0.67 [216]E(f20(x2161,f15(x2162),x2163,x2162,x2164),x2163) % 0.48/0.67 [249]~E(f18(a11,f9(x2491),x2492,a13,a13),f18(a11,f3(x2493),x2494,a13,a13)) % 0.48/0.67 [203]E(f22(f22(a11,f16(x2031,x2032,x2033)),f16(x2034,x2032,x2033)),f16(f22(f22(a11,x2031),x2034),x2032,x2033)) % 0.48/0.67 [248]~E(f22(f22(a11,f9(x2481)),x2482),f18(a11,f3(x2483),x2484,a13,a13)) % 0.48/0.67 [221]E(f28(f28(x2211,f4(a1),x2212,x2213),f22(f22(f5(a1),x2214),f7(a1)),x2215,x2213),f28(f28(x2211,x2214,x2215,x2213),f4(a1),x2212,x2213)) % 0.48/0.67 [253]~P1(x2531)+~E(f7(x2531),f4(x2531)) % 0.48/0.67 [259]E(x2591,f4(a1))+P8(f4(a1),x2591,a1) % 0.48/0.67 [273]~P21(x2731)+P8(f4(x2731),f7(x2731),x2731) % 0.48/0.67 [295]~P21(x2951)+~P8(f7(x2951),f4(x2951),x2951) % 0.48/0.67 [334]P11(f24(a10,a13,a13),x3341,a13)+~P31(f22(a8,x3341)) % 0.48/0.67 [366]~P11(f24(a10,a13,a13),x3661,a13)+P31(f22(a8,x3661)) % 0.48/0.67 [456]~P6(f28(a47,a49,a41,a38),a40,x4561)+P32(a5000) % 0.48/0.67 [254]~P30(x2541)+E(f21(f4(a1),x2541),f4(x2541)) % 0.48/0.67 [255]~P30(x2551)+E(f21(f7(a1),x2551),f7(x2551)) % 0.48/0.67 [278]~P18(x2781)+E(f22(f22(f5(x2781),f4(x2781)),f4(x2781)),f4(x2781)) % 0.48/0.67 [279]~P31(f22(a8,x2791))+P31(f22(a8,f9(x2791))) % 0.48/0.67 [340]~P21(x3401)+P8(f4(x3401),f22(f22(f5(x3401),f7(x3401)),f7(x3401)),x3401) % 0.48/0.67 [361]E(x3611,f4(a1))+~P8(x3611,f22(f22(f5(a1),f4(a1)),f7(a1)),a1) % 0.48/0.67 [409]~P8(f4(a1),x4091,a1)+E(f22(f22(f5(a1),f6(x4091,f7(a1),a1)),f7(a1)),x4091) % 0.48/0.67 [453]~P8(f4(a1),x4531,a1)+E(f22(f22(f5(a1),f6(x4531,f22(f22(f5(a1),f4(a1)),f7(a1)),a1)),f7(a1)),x4531) % 0.48/0.67 [280]~P8(x2802,x2802,x2801)+~P25(x2801) % 0.48/0.67 [281]~P8(x2812,x2812,x2811)+~P27(x2811) % 0.48/0.67 [282]~P8(x2822,x2822,x2821)+~P26(x2821) % 0.48/0.67 [250]E(x2501,x2502)+~E(f3(x2501),f3(x2502)) % 0.48/0.67 [251]E(x2511,x2512)+~E(f9(x2511),f9(x2512)) % 0.48/0.67 [256]~P25(x2562)+P25(f39(x2561,x2562)) % 0.48/0.67 [257]~P27(x2572)+P27(f39(x2571,x2572)) % 0.48/0.67 [261]~P17(x2612)+E(f6(x2611,x2611,x2612),f4(x2612)) % 0.48/0.67 [262]~P13(x2622)+E(f6(x2621,x2621,x2622),f4(x2622)) % 0.48/0.67 [308]~P21(x3081)+~P8(f21(x3082,x3081),f4(x3081),x3081) % 0.48/0.67 [360]~P8(x3602,x3601,a1)+P8(f4(a1),f6(x3601,x3602,a1),a1) % 0.48/0.67 [382]P8(x3821,x3822,a1)+~P8(f4(a1),f6(x3822,x3821,a1),a1) % 0.48/0.67 [263]~P3(x2631)+E(f22(f22(f5(x2631),x2632),f4(x2631)),x2632) % 0.48/0.67 [264]~P24(x2641)+E(f22(f22(f5(x2641),x2642),f4(x2641)),x2642) % 0.48/0.67 [265]~P14(x2651)+E(f22(f22(f5(x2651),x2652),f4(x2651)),x2652) % 0.48/0.67 [266]~P17(x2662)+E(f6(x2661,f4(x2662),x2662),x2661) % 0.48/0.67 [287]~P8(x2871,x2872,a1)+E(f17(f3(x2871),x2872),f3(x2871)) % 0.48/0.67 [307]~P31(f22(a8,x3071))+P31(f22(a8,f17(x3071,x3072))) % 0.48/0.67 [323]~P21(x3232)+P8(x3231,f22(f22(f5(x3232),x3231),f7(x3232)),x3232) % 0.48/0.67 [337]P8(x3371,x3372,a1)+P8(x3372,f22(f22(f5(a1),x3371),f7(a1)),a1) % 0.48/0.67 [339]P8(x3392,x3391,a1)+E(f22(f22(f5(a1),x3391),f6(x3392,x3391,a1)),x3392) % 0.48/0.67 [351]~P31(f22(f22(a10,x3511),x3512))+P31(f22(f22(a10,f9(x3511)),f9(x3512))) % 0.48/0.67 [391]~P8(x3911,x3912,a1)+~P8(x3912,f22(f22(f5(a1),x3911),f7(a1)),a1) % 0.48/0.67 [430]P8(x4301,x4302,a1)+~P8(f22(f22(f5(a1),x4301),f7(a1)),f22(f22(f5(a1),x4302),f7(a1)),a1) % 0.48/0.67 [486]~P3(x4861)+E(f20(f5(x4861),x4862,f4(x4861),x4861,x4861),f18(f5(x4861),f4(x4861),x4862,x4861,x4861)) % 0.48/0.67 [267]~P3(x2671)+E(f22(f22(f5(x2671),f4(x2671)),x2672),x2672) % 0.48/0.67 [269]~P24(x2691)+E(f22(f22(f5(x2691),f4(x2691)),x2692),x2692) % 0.48/0.67 [270]~P14(x2701)+E(f22(f22(f5(x2701),f4(x2701)),x2702),x2702) % 0.48/0.67 [275]E(x2751,f4(a1))+~E(f22(f22(f5(a1),x2752),x2751),x2752) % 0.48/0.67 [276]E(x2761,f4(a1))+~E(f22(f22(f5(a1),x2762),x2761),f4(a1)) % 0.48/0.67 [277]E(x2771,f4(a1))+~E(f22(f22(f5(a1),x2771),x2772),f4(a1)) % 0.48/0.67 [322]P8(x3221,x3222,a1)+E(f17(f3(x3221),x3222),f3(f22(f22(f5(a1),x3221),f7(a1)))) % 0.48/0.67 [341]~P30(x3412)+E(f21(f22(f22(f5(a1),x3411),f7(a1)),x3412),f22(f22(f5(x3412),f7(x3412)),f21(x3411,x3412))) % 0.48/0.67 [357]~P31(f22(a8,x3571))+P31(f22(a8,f22(f22(a11,x3571),f3(x3572)))) % 0.48/0.67 [428]~P8(f4(a1),x4281,a1)+P8(f6(x4281,f22(f22(f5(a1),x4282),f7(a1)),a1),x4281,a1) % 0.48/0.67 [431]P31(f22(f22(f23(a10,a13),f9(x4311)),f9(x4312)))+~P31(f22(f22(f23(a10,a13),x4311),x4312)) % 0.48/0.67 [471]E(x4711,f4(a1))+E(f22(f22(f5(a1),f22(f22(f5(a1),f6(x4711,f7(a1),a1)),x4712)),f7(a1)),f22(f22(f5(a1),x4711),x4712)) % 0.48/0.67 [498]~P7(a8,x4982,a13)+P31(f22(a8,f18(a11,f3(x4981),x4982,a13,a13))) % 0.48/0.67 [291]~P6(x2911,f3(x2912),x2913)+E(f22(x2911,x2912),x2913) % 0.48/0.67 [358]~P8(x3581,x3583,a1)+P8(f6(x3581,x3582,a1),x3583,a1) % 0.48/0.67 [477]~E(f3(x4772),f18(a11,x4773,x4771,a13,a13))+E(x4771,f15(a13)) % 0.48/0.67 [478]~E(f9(x4782),f18(a11,x4783,x4781,a13,a13))+E(x4781,f15(a13)) % 0.48/0.67 [479]~E(f18(a11,x4792,x4791,a13,a13),f9(x4793))+E(x4791,f15(a13)) % 0.48/0.67 [480]E(x4801,f9(x4802))+~E(f18(a11,x4801,x4803,a13,a13),f9(x4802)) % 0.48/0.67 [481]E(f3(x4811),x4812)+~E(f3(x4811),f18(a11,x4812,x4813,a13,a13)) % 0.48/0.67 [482]E(f9(x4821),x4822)+~E(f9(x4821),f18(a11,x4822,x4823,a13,a13)) % 0.48/0.67 [489]E(x4891,x4892)+~E(f18(a11,x4891,x4893,a13,a13),f18(a11,x4892,x4893,a13,a13)) % 0.48/0.67 [312]~P8(x3121,x3123,a1)+E(f16(f3(x3121),x3122,x3123),f3(x3121)) % 0.48/0.67 [403]~P31(f22(f22(a10,x4031),x4033))+P31(f22(f22(a10,f17(x4031,x4032)),f17(x4033,x4032))) % 0.48/0.67 [432]~P6(x4322,f9(x4323),x4321)+E(f22(f22(a27,f29(x4321,x4322,x4323)),f35(x4321,x4322,x4323)),x4321) % 0.48/0.67 [449]~P6(x4491,f9(x4492),x4493)+P6(f28(x4491,f4(a1),f30(x4491,x4492),a38),x4492,f31(x4491,x4492)) % 0.48/0.67 [463]~P6(x4631,f9(x4633),x4632)+P6(f28(x4631,f4(a1),f29(x4632,x4631,x4633),a38),x4633,f35(x4632,x4631,x4633)) % 0.48/0.67 [483]E(f22(f22(a11,x4831),x4832),x4833)+~E(f22(f22(a11,x4831),x4832),f18(a11,x4833,f15(a13),a13,a13)) % 0.48/0.67 [485]~P4(x4851)+E(f20(f5(x4851),x4852,x4853,x4851,x4851),f18(f5(x4851),x4853,x4852,x4851,x4851)) % 0.48/0.67 [506]~P31(f22(f22(a10,x5061),x5063))+P31(f22(f22(a10,f18(a11,x5061,x5062,a13,a13)),f18(a11,x5063,x5062,a13,a13))) % 0.48/0.67 [508]~P9(a10,x5082,x5083,a13)+P31(f22(f22(a10,f18(a11,x5081,x5082,a13,a13)),f18(a11,x5081,x5083,a13,a13))) % 0.48/0.67 [293]~P24(x2931)+E(f22(f22(f5(x2931),x2932),x2933),f22(f22(f5(x2931),x2933),x2932)) % 0.48/0.67 [294]~P14(x2941)+E(f22(f22(f5(x2941),x2942),x2943),f22(f22(f5(x2941),x2943),x2942)) % 0.48/0.67 [310]E(x3101,x3102)+~E(f22(f22(f5(a1),x3103),x3101),f22(f22(f5(a1),x3103),x3102)) % 0.48/0.67 [311]E(x3111,x3112)+~E(f22(f22(f5(a1),x3111),x3113),f22(f22(f5(a1),x3112),x3113)) % 0.48/0.67 [318]E(x3181,x3182)+~P31(f22(f22(f25(x3183),x3181),x3182)) % 0.48/0.67 [347]~P8(x3471,x3473,a1)+P8(x3471,f22(f22(f5(a1),x3472),x3473),a1) % 0.48/0.67 [349]~P8(x3491,x3492,a1)+P8(x3491,f22(f22(f5(a1),x3492),x3493),a1) % 0.48/0.67 [363]~P8(x3633,x3631,a1)+E(f16(f3(x3631),x3632,x3633),f3(f6(x3631,f7(a1),a1))) % 0.48/0.67 [374]~P17(x3741)+E(f22(f22(f5(x3741),f6(x3742,x3743,x3741)),x3743),x3742) % 0.48/0.67 [375]P8(x3751,x3752,a1)+~P8(f22(f22(f5(a1),x3751),x3753),x3752,a1) % 0.48/0.67 [383]~P31(f22(a8,x3831))+P31(f22(a8,f16(x3831,f3(x3832),x3833))) % 0.48/0.67 [388]~P8(x3881,x3883,a1)+P8(f22(f22(f5(a1),x3881),x3882),f22(f22(f5(a1),x3883),x3882),a1) % 0.48/0.67 [389]~P8(x3892,x3893,a1)+P8(f22(f22(f5(a1),x3891),x3892),f22(f22(f5(a1),x3891),x3893),a1) % 0.48/0.67 [412]P8(x4121,f6(x4122,x4123,a1),a1)+~P8(f22(f22(f5(a1),x4121),x4123),x4122,a1) % 0.48/0.67 [414]~P8(x4141,f6(x4143,x4142,a1),a1)+P8(f22(f22(f5(a1),x4141),x4142),x4143,a1) % 0.48/0.67 [417]~P8(x4172,f22(f22(f5(a1),x4173),f7(a1)),a1)+E(f17(f17(x4171,x4172),f22(f22(f5(a1),x4173),f7(a1))),f17(f17(x4171,x4173),x4172)) % 0.48/0.67 [424]P8(x4241,x4242,a1)+~P8(f22(f22(f5(a1),x4243),x4241),f22(f22(f5(a1),x4243),x4242),a1) % 0.48/0.67 [438]P31(f22(f22(f23(a10,a13),f17(x4381,x4382)),f17(x4383,x4382)))+~P31(f22(f22(f23(a10,a13),x4381),x4383)) % 0.48/0.67 [442]~P31(f22(f22(a10,x4421),x4423))+P31(f22(f22(a10,f22(f22(a11,x4421),x4422)),f22(f22(a11,x4423),x4422))) % 0.48/0.67 [443]~P31(f22(f22(a10,x4432),x4433))+P31(f22(f22(a10,f22(f22(a11,x4431),x4432)),f22(f22(a11,x4431),x4433))) % 0.48/0.67 [457]~P31(f22(f22(f23(a10,a13),x4571),x4573))+P31(f22(f22(f23(a10,a13),f22(f22(a11,x4571),x4572)),f22(f22(a11,x4573),x4572))) % 0.48/0.67 [458]~P31(f22(f22(f23(a10,a13),x4582),x4583))+P31(f22(f22(f23(a10,a13),f22(f22(a11,x4581),x4582)),f22(f22(a11,x4581),x4583))) % 0.48/0.67 [487]~P3(x4871)+E(f22(f22(f5(x4871),x4872),f20(f5(x4871),x4873,f4(x4871),x4871,x4871)),f18(f5(x4871),x4872,x4873,x4871,x4871)) % 0.48/0.67 [488]~P3(x4881)+E(f22(f22(f5(x4881),x4882),f18(f5(x4881),f4(x4881),x4883,x4881,x4881)),f18(f5(x4881),x4882,x4883,x4881,x4881)) % 0.48/0.67 [507]P31(f22(f22(f23(a10,a13),f18(a11,x5071,x5072,a13,a13)),f18(a11,x5073,x5072,a13,a13)))+~P31(f22(f22(f23(a10,a13),x5071),x5073)) % 0.48/0.67 [315]~P17(x3151)+E(f6(f22(f22(f5(x3151),x3152),x3153),x3153,x3151),x3152) % 0.48/0.67 [359]~P30(x3591)+E(f22(f22(f5(x3591),f21(x3592,x3591)),f21(x3593,x3591)),f21(f22(f22(f5(a1),x3592),x3593),x3591)) % 0.48/0.67 [509]P9(a10,x5091,f19(x5092,x5091,x5093),a13)+~P31(f22(f22(a10,f18(a11,f3(x5092),x5091,a13,a13)),x5093)) % 0.48/0.67 [512]E(f18(a11,f3(x5121),f19(x5121,x5122,x5123),a13,a13),x5123)+~P31(f22(f22(a10,f18(a11,f3(x5121),x5122,a13,a13)),x5123)) % 0.48/0.67 [465]P31(f22(x4651,x4652))+~P31(f22(x4651,f6(f22(f22(f5(a1),x4653),x4652),x4653,a1))) % 0.48/0.67 [495]P12(x4951,x4952,f33(x4953,x4951,x4954,x4952))+~P6(x4951,f18(a11,x4954,x4952,a13,a13),x4953) % 0.48/0.67 [496]P12(x4961,x4962,f34(x4963,x4961,x4964,x4962))+~P6(x4961,f18(a11,x4964,x4962,a13,a13),x4963) % 0.48/0.67 [297]E(x2971,x2972)+~E(f22(f22(a11,x2973),x2971),f22(f22(a11,x2974),x2972)) % 0.48/0.67 [298]E(x2981,x2982)+~E(f22(f22(a27,x2983),x2981),f22(f22(a27,x2984),x2982)) % 0.48/0.67 [299]E(x2991,x2992)+~E(f22(f22(a11,x2991),x2993),f22(f22(a11,x2992),x2994)) % 0.48/0.67 [300]E(x3001,x3002)+~E(f22(f22(a27,x3001),x3003),f22(f22(a27,x3002),x3004)) % 0.48/0.67 [446]E(f16(f17(x4461,f22(f22(f5(a1),x4462),f7(a1))),f17(x4463,x4462),x4464),f17(f16(x4461,x4463,x4464),x4462))+~P8(x4464,f22(f22(f5(a1),x4462),f7(a1)),a1) % 0.48/0.67 [451]P6(x4511,x4512,f32(x4513,x4511,x4514,x4512))+~P6(x4511,f22(f22(a11,x4514),x4512),x4513) % 0.48/0.67 [454]~P31(f22(f22(a10,x4541),x4544))+P31(f22(f22(a10,f16(x4541,x4542,x4543)),f16(x4544,x4542,x4543))) % 0.48/0.67 [462]P31(f22(f22(f23(a10,a13),f16(x4621,x4622,x4623)),f16(x4621,x4624,x4623)))+~P31(f22(f22(a10,x4622),x4624)) % 0.48/0.67 [466]P6(x4661,f9(x4662),f22(f22(a27,x4663),x4664))+~P6(f28(x4661,f4(a1),x4663,a38),x4662,x4664) % 0.48/0.67 [491]E(x4911,x4912)+~E(f18(a11,f3(x4913),x4911,a13,a13),f18(a11,f3(x4914),x4912,a13,a13)) % 0.48/0.67 [492]E(x4921,x4922)+~E(f18(a11,f9(x4923),x4921,a13,a13),f18(a11,f9(x4924),x4922,a13,a13)) % 0.48/0.67 [493]E(x4931,x4932)+~E(f18(a11,f3(x4931),x4933,a13,a13),f18(a11,f3(x4932),x4934,a13,a13)) % 0.48/0.67 [494]E(x4941,x4942)+~E(f18(a11,f9(x4941),x4943,a13,a13),f18(a11,f9(x4942),x4944,a13,a13)) % 0.48/0.67 [497]P12(x4971,x4972,f36(x4973,x4971,x4974,x4972))+~P6(x4971,f18(a11,f3(x4974),x4972,a13,a13),x4973) % 0.48/0.67 [500]~P6(x5001,f18(a11,x5002,x5004,a13,a13),x5003)+P6(x5001,x5002,f20(a27,f33(x5003,x5001,x5002,x5004),x5003,a38,a38)) % 0.48/0.67 [501]~P6(x5011,f18(a11,x5012,x5014,a13,a13),x5013)+P6(x5011,x5012,f20(a27,f34(x5013,x5011,x5012,x5014),x5013,a38,a38)) % 0.48/0.67 [502]~P6(x5021,f18(a11,f3(x5022),x5024,a13,a13),x5023)+P6(x5021,f3(x5022),f20(a27,f36(x5023,x5021,x5022,x5024),x5023,a38,a38)) % 0.48/0.67 [384]~P31(f22(f22(x3841,x3843),x3844))+P31(f22(f22(f23(x3841,x3842),x3843),x3844)) % 0.48/0.67 [437]~P8(x4372,f22(f22(f5(a1),x4374),f7(a1)),a1)+E(f16(f17(x4371,x4372),f17(x4373,x4372),f22(f22(f5(a1),x4374),f7(a1))),f17(f16(x4371,x4373,x4374),x4372)) % 0.48/0.67 [467]P31(f22(f22(f23(a10,a13),f16(x4671,x4672,x4673)),f16(x4674,x4672,x4673)))+~P31(f22(f22(f23(a10,a13),x4671),x4674)) % 0.48/0.67 [468]P31(f22(f22(f23(a10,a13),f16(x4681,x4682,x4683)),f16(x4681,x4684,x4683)))+~P31(f22(f22(f23(a10,a13),x4682),x4684)) % 0.48/0.67 [484]~P6(x4841,f22(f22(a11,x4842),x4844),x4843)+P6(x4841,x4842,f22(f22(a27,f32(x4843,x4841,x4842,x4844)),x4843)) % 0.48/0.67 [385]~P13(x3851)+E(f22(f22(f5(x3851),x3852),f22(f22(f5(x3851),x3853),x3854)),f22(f22(f5(x3851),x3853),f22(f22(f5(x3851),x3852),x3854))) % 0.48/0.67 [386]~P24(x3861)+E(f22(f22(f5(x3861),x3862),f22(f22(f5(x3861),x3863),x3864)),f22(f22(f5(x3861),x3863),f22(f22(f5(x3861),x3862),x3864))) % 0.48/0.67 [387]~P14(x3871)+E(f22(f22(f5(x3871),x3872),f22(f22(f5(x3871),x3873),x3874)),f22(f22(f5(x3871),x3873),f22(f22(f5(x3871),x3872),x3874))) % 0.48/0.67 [475]~P31(f22(f22(f23(x4751,x4752),x4754),x4753))+P31(f22(f22(f23(f24(x4751,x4752,x4752),x4752),x4753),x4754)) % 0.48/0.67 [476]P31(f22(f22(f23(x4761,x4762),x4763),x4764))+~P31(f22(f22(f23(f24(x4761,x4762,x4762),x4762),x4764),x4763)) % 0.48/0.67 [490]~P23(x4901)+E(f18(f5(x4901),f22(f22(f5(x4901),x4902),x4903),x4904,x4901,x4901),f22(f22(f5(x4901),x4902),f18(f5(x4901),x4903,x4904,x4901,x4901))) % 0.48/0.67 [421]~P4(x4211)+E(f22(f22(f5(x4211),f22(f22(f5(x4211),x4212),x4213)),x4214),f22(f22(f5(x4211),x4212),f22(f22(f5(x4211),x4213),x4214))) % 0.48/0.67 [422]~P24(x4221)+E(f22(f22(f5(x4221),f22(f22(f5(x4221),x4222),x4223)),x4224),f22(f22(f5(x4221),x4222),f22(f22(f5(x4221),x4223),x4224))) % 0.48/0.67 [423]~P14(x4231)+E(f22(f22(f5(x4231),f22(f22(f5(x4231),x4232),x4233)),x4234),f22(f22(f5(x4231),x4232),f22(f22(f5(x4231),x4233),x4234))) % 0.48/0.67 [436]~P24(x4361)+E(f22(f22(f5(x4361),f22(f22(f5(x4361),x4362),x4363)),x4364),f22(f22(f5(x4361),f22(f22(f5(x4361),x4362),x4364)),x4363)) % 0.48/0.67 [447]~P6(x4471,x4474,x4475)+P6(f28(x4471,x4472,x4473,a38),f17(x4474,x4472),x4475) % 0.48/0.67 [439]~P8(x4395,x4392,a1)+E(f22(f28(x4391,x4392,x4393,x4394),x4395),f22(x4391,x4395)) % 0.48/0.67 [461]E(f16(f16(x4611,f17(x4612,x4613),f22(f22(f5(a1),x4614),f7(a1))),f16(x4615,x4612,x4614),x4613),f16(f16(x4611,x4615,x4613),x4612,x4614))+~P8(x4613,f22(f22(f5(a1),x4614),f7(a1)),a1) % 0.48/0.67 [445]~P31(f22(f22(x4451,x4455),x4454))+P31(f22(f22(f24(x4451,x4452,x4453),x4454),x4455)) % 0.48/0.67 [448]~P8(x4482,x4485,a1)+E(f22(f28(x4481,x4482,x4483,x4484),x4485),f22(x4481,f6(x4485,f7(a1),a1))) % 0.48/0.67 [460]P31(f22(f22(x4601,x4602),x4603))+~P31(f22(f22(f24(x4601,x4604,x4605),x4603),x4602)) % 0.48/0.67 [450]~P24(x4501)+E(f22(f22(f5(x4501),f22(f22(f5(x4501),x4502),x4503)),f22(f22(f5(x4501),x4504),x4505)),f22(f22(f5(x4501),f22(f22(f5(x4501),x4502),x4504)),f22(f22(f5(x4501),x4503),x4505))) % 0.48/0.67 [290]E(x2901,x2902)+P8(x2902,x2901,a1)+P8(x2901,x2902,a1) % 0.48/0.67 [271]~P28(x2712)+~P10(x2712)+E(f6(x2711,x2711,x2712),f4(x2712)) % 0.48/0.67 [324]E(x3241,x3242)+~E(f6(x3242,x3241,a1),f4(a1))+~E(f6(x3241,x3242,a1),f4(a1)) % 0.48/0.67 [332]~P21(x3321)+P8(f4(x3321),f21(x3322,x3321),x3321)+~P8(f4(a1),x3322,a1) % 0.48/0.67 [336]~P21(x3362)+~P8(f4(x3362),f21(x3361,x3362),x3362)+P8(f4(a1),x3361,a1) % 0.48/0.67 [400]P8(f6(x4001,x4002,a1),x4001,a1)+~P8(f4(a1),x4002,a1)+~P8(f4(a1),x4001,a1) % 0.48/0.67 [272]~P28(x2721)+~P10(x2721)+E(f22(f22(f5(x2721),x2722),f4(x2721)),x2722) % 0.48/0.67 [377]~P8(x3771,x3772,a1)+P8(f22(f22(f5(a1),x3771),f7(a1)),x3772,a1)+E(f22(f22(f5(a1),x3771),f7(a1)),x3772) % 0.48/0.67 [379]E(x3791,x3792)+P8(x3792,x3791,a1)+~P8(x3792,f22(f22(f5(a1),x3791),f7(a1)),a1) % 0.48/0.67 [381]E(x3811,x3812)+P8(x3811,x3812,a1)+~P8(x3811,f22(f22(f5(a1),x3812),f7(a1)),a1) % 0.48/0.67 [283]~P18(x2832)+E(x2831,f4(x2832))+~E(f22(f22(f5(x2832),x2831),x2831),f4(x2832)) % 0.48/0.67 [316]E(x3161,f4(a1))+E(x3162,f4(a1))+~E(f22(f22(f5(a1),x3162),x3161),f22(f22(f5(a1),f4(a1)),f7(a1))) % 0.48/0.67 [317]E(x3171,f4(a1))+E(x3172,f4(a1))+~E(f22(f22(f5(a1),f4(a1)),f7(a1)),f22(f22(f5(a1),x3172),x3171)) % 0.48/0.67 [342]E(x3421,f4(a1))+E(x3421,f22(f22(f5(a1),f4(a1)),f7(a1)))+~E(f22(f22(f5(a1),x3422),x3421),f22(f22(f5(a1),f4(a1)),f7(a1))) % 0.48/0.67 [343]E(x3431,f4(a1))+E(x3431,f22(f22(f5(a1),f4(a1)),f7(a1)))+~E(f22(f22(f5(a1),x3431),x3432),f22(f22(f5(a1),f4(a1)),f7(a1))) % 0.48/0.67 [344]E(x3441,f4(a1))+E(x3441,f22(f22(f5(a1),f4(a1)),f7(a1)))+~E(f22(f22(f5(a1),f4(a1)),f7(a1)),f22(f22(f5(a1),x3442),x3441)) % 0.48/0.67 [345]E(x3451,f4(a1))+E(x3451,f22(f22(f5(a1),f4(a1)),f7(a1)))+~E(f22(f22(f5(a1),f4(a1)),f7(a1)),f22(f22(f5(a1),x3451),x3452)) % 0.48/0.67 [367]~P18(x3671)+~P8(f4(x3671),x3672,x3671)+P8(f4(x3671),f22(f22(f5(x3671),x3672),x3672),x3671) % 0.48/0.67 [368]~P18(x3681)+~P8(x3682,f4(x3681),x3681)+P8(f22(f22(f5(x3681),x3682),x3682),f4(x3681),x3681) % 0.48/0.67 [369]~P29(x3691)+~P8(x3692,f4(x3691),x3691)+P8(f22(f22(f5(x3691),x3692),x3692),f4(x3691),x3691) % 0.48/0.67 [372]E(x3721,f22(f22(f5(a1),f4(a1)),f7(a1)))+E(x3722,f22(f22(f5(a1),f4(a1)),f7(a1)))+~E(f22(f22(f5(a1),x3722),x3721),f22(f22(f5(a1),f4(a1)),f7(a1))) % 0.48/0.67 [373]E(x3731,f22(f22(f5(a1),f4(a1)),f7(a1)))+E(x3732,f22(f22(f5(a1),f4(a1)),f7(a1)))+~E(f22(f22(f5(a1),f4(a1)),f7(a1)),f22(f22(f5(a1),x3732),x3731)) % 0.48/0.67 [394]~P18(x3942)+P8(x3941,f4(x3942),x3942)+~P8(f22(f22(f5(x3942),x3941),x3941),f4(x3942),x3942) % 0.48/0.67 [395]~P29(x3952)+P8(x3951,f4(x3952),x3952)+~P8(f22(f22(f5(x3952),x3951),x3951),f4(x3952),x3952) % 0.48/0.67 [396]~P18(x3961)+P8(f4(x3961),x3962,x3961)+~P8(f4(x3961),f22(f22(f5(x3961),x3962),x3962),x3961) % 0.48/0.67 [401]P8(f4(a1),x4011,a1)+P8(f4(a1),x4012,a1)+~P8(f4(a1),f22(f22(f5(a1),x4011),x4012),a1) % 0.48/0.67 [325]~P8(x3253,x3252,x3251)+~P25(x3251)+~P8(x3252,x3253,x3251) % 0.48/0.67 [327]~P8(x3273,x3272,x3271)+~P27(x3271)+~P8(x3272,x3273,x3271) % 0.48/0.67 [328]~P8(x3283,x3282,x3281)+~P26(x3281)+~P8(x3282,x3283,x3281) % 0.48/0.67 [258]~P5(x2583)+E(x2581,x2582)+~E(f21(x2581,x2583),f21(x2582,x2583)) % 0.48/0.68 [284]~P17(x2843)+E(x2841,x2842)+~E(f6(x2841,x2842,x2843),f4(x2843)) % 0.48/0.68 [285]~P13(x2853)+E(x2851,x2852)+~E(f6(x2851,x2852,x2853),f4(x2853)) % 0.48/0.68 [335]~P21(x3352)+~P8(x3351,x3353,a1)+P8(f21(x3351,x3352),f21(x3353,x3352),x3352) % 0.48/0.68 [350]~P21(x3503)+~P8(f21(x3501,x3503),f21(x3502,x3503),x3503)+P8(x3501,x3502,a1) % 0.48/0.68 [365]~P20(x3653)+~P8(x3651,x3652,x3653)+P8(f6(x3651,x3652,x3653),f4(x3653),x3653) % 0.48/0.68 [397]~P20(x3973)+P8(x3971,x3972,x3973)+~P8(f6(x3971,x3972,x3973),f4(x3973),x3973) % 0.48/0.68 [425]~P8(x4253,x4252,a1)+~P8(x4253,x4251,a1)+P8(f6(x4251,x4252,a1),f6(x4251,x4253,a1),a1) % 0.48/0.68 [306]E(x3061,x3062)+P8(x3062,x3061,a1)+E(f16(f3(x3061),x3063,x3062),f3(x3061)) % 0.48/0.68 [390]~P8(x3901,x3903,a1)+~P8(x3903,x3902,a1)+P8(f22(f22(f5(a1),x3901),f7(a1)),x3902,a1) % 0.48/0.68 [435]~P8(x4352,x4353,a1)+~P31(f22(x4351,f6(x4352,x4353,a1)))+P31(f22(x4351,f4(a1))) % 0.48/0.68 [503]~P11(f24(a10,a13,a13),x5032,a13)+~P11(f24(a10,a13,a13),f18(a11,f16(x5031,x5032,f4(a1)),x5033,a13,a13),a13)+P11(f24(a10,a13,a13),f18(a11,f22(f22(a11,f9(x5031)),x5032),x5033,a13,a13),a13) % 0.48/0.68 [505]~P31(f22(a8,x5052))+~P31(f22(a8,f18(a11,f16(x5051,x5052,f4(a1)),x5053,a13,a13)))+P31(f22(a8,f18(a11,f22(f22(a11,f9(x5051)),x5052),x5053,a13,a13))) % 0.48/0.68 [329]~P13(x3294)+E(x3291,x3292)+~E(f6(x3293,x3293,x3294),f6(x3291,x3292,x3294)) % 0.48/0.68 [330]~P13(x3303)+E(x3301,x3302)+~E(f6(x3301,x3302,x3303),f6(x3304,x3304,x3303)) % 0.48/0.68 [364]P6(x3641,x3642,x3643)+~P6(x3641,x3644,x3643)+~P31(f22(f22(a10,x3644),x3642)) % 0.48/0.68 [371]P11(x3711,x3712,x3713)+~P11(x3711,x3714,x3713)+~P31(f22(f22(x3711,x3712),x3714)) % 0.48/0.68 [319]~P15(x3193)+E(x3191,x3192)+~E(f22(f22(f5(x3193),x3194),x3191),f22(f22(f5(x3193),x3194),x3192)) % 0.48/0.68 [320]~P16(x3203)+E(x3201,x3202)+~E(f22(f22(f5(x3203),x3204),x3201),f22(f22(f5(x3203),x3204),x3202)) % 0.48/0.68 [321]~P16(x3213)+E(x3211,x3212)+~E(f22(f22(f5(x3213),x3211),x3214),f22(f22(f5(x3213),x3212),x3214)) % 0.48/0.68 [376]~P8(x3764,x3763,a1)+P8(x3761,x3762,a1)+~E(f22(f22(f5(a1),x3761),x3763),f22(f22(f5(a1),x3764),x3762)) % 0.48/0.68 [404]~P2(x4041)+~P8(x4042,x4044,x4041)+P8(f22(f22(f5(x4041),x4042),x4043),f22(f22(f5(x4041),x4044),x4043),x4041) % 0.48/0.68 [405]~P19(x4051)+~P8(x4052,x4054,x4051)+P8(f22(f22(f5(x4051),x4052),x4053),f22(f22(f5(x4051),x4054),x4053),x4051) % 0.48/0.68 [406]~P2(x4061)+~P8(x4063,x4064,x4061)+P8(f22(f22(f5(x4061),x4062),x4063),f22(f22(f5(x4061),x4062),x4064),x4061) % 0.48/0.68 [407]~P19(x4071)+~P8(x4073,x4074,x4071)+P8(f22(f22(f5(x4071),x4072),x4073),f22(f22(f5(x4071),x4072),x4074),x4071) % 0.48/0.68 [415]P6(x4151,x4152,x4153)+~P6(x4151,x4154,x4153)+~P31(f22(f22(f23(a10,a13),x4154),x4152)) % 0.48/0.68 [416]~P8(x4162,x4164,a1)+~P8(x4161,x4163,a1)+P8(f22(f22(f5(a1),x4161),x4162),f22(f22(f5(a1),x4163),x4164),a1) % 0.48/0.68 [427]P11(x4271,x4272,x4273)+~P11(x4271,x4274,x4273)+~P31(f22(f22(f23(x4271,x4273),x4272),x4274)) % 0.48/0.68 [433]~P19(x4333)+P8(x4331,x4332,x4333)+~P8(f22(f22(f5(x4333),x4334),x4331),f22(f22(f5(x4333),x4334),x4332),x4333) % 0.48/0.68 [434]~P19(x4343)+P8(x4341,x4342,x4343)+~P8(f22(f22(f5(x4343),x4341),x4344),f22(f22(f5(x4343),x4342),x4344),x4343) % 0.48/0.68 [469]~P31(f22(f22(f23(a10,a13),x4691),x4693))+~P31(f22(f22(f23(a10,a13),x4692),x4694))+P31(f22(f22(f23(a10,a13),f22(f22(a11,x4691),x4692)),f22(f22(a11,x4693),x4694))) % 0.48/0.68 [499]~P12(x4991,x4993,x4995)+~P6(x4991,x4992,f20(a27,x4995,x4994,a38,a38))+P6(x4991,f18(a11,x4992,x4993,a13,a13),x4994) % 0.48/0.68 [418]~P6(x4181,x4183,x4185)+~P6(x4181,x4182,f22(f22(a27,x4185),x4184))+P6(x4181,f22(f22(a11,x4182),x4183),x4184) % 0.48/0.68 [504]E(x5041,x5042)+~P6(x5043,f18(a11,f3(x5044),x5045,a13,a13),x5041)+~P6(x5043,f18(a11,f3(x5044),x5045,a13,a13),x5042) % 0.48/0.68 [440]~P31(f22(f22(x4401,x4405),x4404))+~P31(f22(f22(f23(x4401,x4402),x4403),x4405))+P31(f22(f22(f23(x4401,x4402),x4403),x4404)) % 0.48/0.68 [441]~P31(f22(f22(x4411,x4413),x4415))+~P31(f22(f22(f23(x4411,x4412),x4415),x4414))+P31(f22(f22(f23(x4411,x4412),x4413),x4414)) % 0.48/0.68 [452]~P31(f22(f22(f23(x4521,x4522),x4523),x4525))+P31(f22(f22(f23(x4521,x4522),x4523),x4524))+~P31(f22(f22(f23(x4521,x4522),x4525),x4524)) % 0.48/0.68 [413]~P13(x4131)+E(f22(f22(f5(x4131),x4132),x4133),x4134)+~E(f22(f22(f5(x4131),x4132),f22(f22(f5(x4131),x4135),x4133)),f22(f22(f5(x4131),x4135),x4134)) % 0.48/0.68 [470]~P6(x4701,x4703,x4706)+P6(x4701,f16(x4702,x4703,x4704),x4705)+~P6(f28(x4701,x4704,x4706,a38),x4702,x4705) % 0.48/0.68 [301]P8(x3011,x3012,x3013)+~P29(x3013)+E(x3011,x3012)+P8(x3012,x3011,x3013) % 0.48/0.68 [305]P8(x3051,x3052,x3053)+~P26(x3053)+E(x3051,x3052)+P8(x3052,x3051,x3053) % 0.48/0.68 [288]~P28(x2883)+~P10(x2883)+E(x2881,x2882)+~E(f6(x2881,x2882,x2883),f4(x2883)) % 0.48/0.68 [286]~P28(x2862)+~P10(x2862)+E(x2861,f4(x2862))+~E(f22(f22(f5(x2862),x2863),x2861),x2863) % 0.48/0.68 [410]~P22(x4101)+~P8(f4(x4101),x4103,x4101)+~P8(f4(x4101),x4102,x4101)+P8(f4(x4101),f22(f22(f5(x4101),x4102),x4103),x4101) % 0.48/0.68 [411]~P22(x4111)+~P8(x4113,f4(x4111),x4111)+~P8(x4112,f4(x4111),x4111)+P8(f22(f22(f5(x4111),x4112),x4113),f4(x4111),x4111) % 0.48/0.68 [353]~P25(x3533)+~P8(x3531,x3534,x3533)+P8(x3531,x3532,x3533)+~P8(x3534,x3532,x3533) % 0.48/0.68 [354]~P27(x3543)+~P8(x3541,x3544,x3543)+P8(x3541,x3542,x3543)+~P8(x3544,x3542,x3543) % 0.48/0.68 [472]~P6(x4723,x4721,a41)+~P6(f28(x4723,x4722,a41,a38),a40,x4724)+~P31(f22(a8,x4721))+P31(f22(a8,f16(a40,x4721,x4722))) % 0.48/0.68 [331]~P28(x3313)+~P10(x3313)+E(x3311,x3312)+~E(f22(f22(f5(x3313),x3314),x3311),f22(f22(f5(x3313),x3314),x3312)) % 0.48/0.68 [402]~P21(x4022)+~P8(x4021,x4024,x4022)+~P8(f4(x4022),x4023,x4022)+P8(x4021,f22(f22(f5(x4022),x4023),x4024),x4022) % 0.48/0.68 [510]~P6(x5103,x5101,a41)+~P6(f28(x5103,x5102,a41,a38),f18(a11,f16(a50,a40,f4(a1)),a48,a13,a13),x5104)+~P31(f22(a8,x5101))+P31(f22(a8,f16(f18(a11,f16(a50,a40,f4(a1)),a48,a13,a13),x5101,x5102))) % 0.48/0.68 [392]~P20(x3923)+~P8(x3924,x3925,x3923)+P8(x3921,x3922,x3923)+~E(f6(x3924,x3925,x3923),f6(x3921,x3922,x3923)) % 0.48/0.68 [393]~P20(x3933)+~P8(x3934,x3935,x3933)+P8(x3931,x3932,x3933)+~E(f6(x3931,x3932,x3933),f6(x3934,x3935,x3933)) % 0.48/0.68 [429]~P2(x4291)+~P8(x4293,x4295,x4291)+~P8(x4292,x4294,x4291)+P8(f22(f22(f5(x4291),x4292),x4293),f22(f22(f5(x4291),x4294),x4295),x4291) % 0.48/0.68 [511]~P12(x5111,x5115,x5116)+P12(x5111,x5112,f37(x5113,x5114,x5111,x5112))+~P6(x5111,f18(a11,f3(x5117),x5115,a13,a13),x5114)+~P6(x5111,f18(a11,f18(a11,f3(x5117),x5115,a13,a13),x5112,a13,a13),x5113) % 0.48/0.68 [513]~P12(x5133,x5135,x5136)+~P6(x5133,f18(a11,f3(x5137),x5135,a13,a13),x5132)+~P6(x5133,f18(a11,f18(a11,f3(x5137),x5135,a13,a13),x5134,a13,a13),x5131)+E(f20(a27,f37(x5131,x5132,x5133,x5134),x5131,a38,a38),x5132) % 0.48/0.68 [473]~P6(x4736,x4732,x4735)+~P6(f28(x4736,x4733,x4735,a38),x4731,x4737)+~P31(f22(a8,x4732))+~P31(f22(a8,x4731))+~E(f22(f22(a27,x4734),x4735),a41)+P31(f22(a8,f16(x4731,x4732,x4733))) % 0.48/0.68 [474]~P6(x4746,x4742,x4744)+~P6(f28(x4746,x4743,x4744,a38),x4741,x4747)+~P31(f22(a8,x4742))+~P31(f22(a8,x4741))+~E(f22(f22(a27,x4744),x4745),a41)+P31(f22(a8,f16(x4741,x4742,x4743))) % 0.48/0.68 %EqnAxiom % 0.48/0.68 [1]E(x11,x11) % 0.48/0.68 [2]E(x22,x21)+~E(x21,x22) % 0.48/0.68 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.48/0.68 [4]~E(x41,x42)+E(f3(x41),f3(x42)) % 0.48/0.68 [5]~E(x51,x52)+E(f12(x51),f12(x52)) % 0.48/0.68 [6]~E(x61,x62)+E(f4(x61),f4(x62)) % 0.48/0.68 [7]~E(x71,x72)+E(f18(x71,x73,x74,x75,x76),f18(x72,x73,x74,x75,x76)) % 0.48/0.68 [8]~E(x81,x82)+E(f18(x83,x81,x84,x85,x86),f18(x83,x82,x84,x85,x86)) % 0.48/0.68 [9]~E(x91,x92)+E(f18(x93,x94,x91,x95,x96),f18(x93,x94,x92,x95,x96)) % 0.48/0.68 [10]~E(x101,x102)+E(f18(x103,x104,x105,x101,x106),f18(x103,x104,x105,x102,x106)) % 0.48/0.68 [11]~E(x111,x112)+E(f18(x113,x114,x115,x116,x111),f18(x113,x114,x115,x116,x112)) % 0.48/0.68 [12]~E(x121,x122)+E(f14(x121,x123),f14(x122,x123)) % 0.48/0.68 [13]~E(x131,x132)+E(f14(x133,x131),f14(x133,x132)) % 0.48/0.68 [14]~E(x141,x142)+E(f22(x141,x143),f22(x142,x143)) % 0.48/0.68 [15]~E(x151,x152)+E(f22(x153,x151),f22(x153,x152)) % 0.48/0.68 [16]~E(x161,x162)+E(f7(x161),f7(x162)) % 0.48/0.68 [17]~E(x171,x172)+E(f5(x171),f5(x172)) % 0.48/0.68 [18]~E(x181,x182)+E(f17(x181,x183),f17(x182,x183)) % 0.48/0.68 [19]~E(x191,x192)+E(f17(x193,x191),f17(x193,x192)) % 0.48/0.68 [20]~E(x201,x202)+E(f16(x201,x203,x204),f16(x202,x203,x204)) % 0.48/0.68 [21]~E(x211,x212)+E(f16(x213,x211,x214),f16(x213,x212,x214)) % 0.48/0.68 [22]~E(x221,x222)+E(f16(x223,x224,x221),f16(x223,x224,x222)) % 0.48/0.68 [23]~E(x231,x232)+E(f24(x231,x233,x234),f24(x232,x233,x234)) % 0.48/0.68 [24]~E(x241,x242)+E(f24(x243,x241,x244),f24(x243,x242,x244)) % 0.48/0.68 [25]~E(x251,x252)+E(f24(x253,x254,x251),f24(x253,x254,x252)) % 0.48/0.68 [26]~E(x261,x262)+E(f6(x261,x263,x264),f6(x262,x263,x264)) % 0.48/0.68 [27]~E(x271,x272)+E(f6(x273,x271,x274),f6(x273,x272,x274)) % 0.48/0.68 [28]~E(x281,x282)+E(f6(x283,x284,x281),f6(x283,x284,x282)) % 0.48/0.68 [29]~E(x291,x292)+E(f9(x291),f9(x292)) % 0.48/0.68 [30]~E(x301,x302)+E(f23(x301,x303),f23(x302,x303)) % 0.48/0.68 [31]~E(x311,x312)+E(f23(x313,x311),f23(x313,x312)) % 0.48/0.68 [32]~E(x321,x322)+E(f20(x321,x323,x324,x325,x326),f20(x322,x323,x324,x325,x326)) % 0.48/0.68 [33]~E(x331,x332)+E(f20(x333,x331,x334,x335,x336),f20(x333,x332,x334,x335,x336)) % 0.48/0.68 [34]~E(x341,x342)+E(f20(x343,x344,x341,x345,x346),f20(x343,x344,x342,x345,x346)) % 0.48/0.68 [35]~E(x351,x352)+E(f20(x353,x354,x355,x351,x356),f20(x353,x354,x355,x352,x356)) % 0.48/0.68 [36]~E(x361,x362)+E(f20(x363,x364,x365,x366,x361),f20(x363,x364,x365,x366,x362)) % 0.48/0.68 [37]~E(x371,x372)+E(f28(x371,x373,x374,x375),f28(x372,x373,x374,x375)) % 0.48/0.68 [38]~E(x381,x382)+E(f28(x383,x381,x384,x385),f28(x383,x382,x384,x385)) % 0.48/0.68 [39]~E(x391,x392)+E(f28(x393,x394,x391,x395),f28(x393,x394,x392,x395)) % 0.48/0.68 [40]~E(x401,x402)+E(f28(x403,x404,x405,x401),f28(x403,x404,x405,x402)) % 0.48/0.68 [41]~E(x411,x412)+E(f21(x411,x413),f21(x412,x413)) % 0.48/0.68 [42]~E(x421,x422)+E(f21(x423,x421),f21(x423,x422)) % 0.48/0.68 [43]~E(x431,x432)+E(f15(x431),f15(x432)) % 0.48/0.68 [44]~E(x441,x442)+E(f36(x441,x443,x444,x445),f36(x442,x443,x444,x445)) % 0.48/0.68 [45]~E(x451,x452)+E(f36(x453,x451,x454,x455),f36(x453,x452,x454,x455)) % 0.48/0.68 [46]~E(x461,x462)+E(f36(x463,x464,x461,x465),f36(x463,x464,x462,x465)) % 0.48/0.68 [47]~E(x471,x472)+E(f36(x473,x474,x475,x471),f36(x473,x474,x475,x472)) % 0.48/0.68 [48]~E(x481,x482)+E(f32(x481,x483,x484,x485),f32(x482,x483,x484,x485)) % 0.48/0.68 [49]~E(x491,x492)+E(f32(x493,x491,x494,x495),f32(x493,x492,x494,x495)) % 0.48/0.68 [50]~E(x501,x502)+E(f32(x503,x504,x501,x505),f32(x503,x504,x502,x505)) % 0.48/0.68 [51]~E(x511,x512)+E(f32(x513,x514,x515,x511),f32(x513,x514,x515,x512)) % 0.48/0.68 [52]~E(x521,x522)+E(f33(x521,x523,x524,x525),f33(x522,x523,x524,x525)) % 0.48/0.68 [53]~E(x531,x532)+E(f33(x533,x531,x534,x535),f33(x533,x532,x534,x535)) % 0.48/0.68 [54]~E(x541,x542)+E(f33(x543,x544,x541,x545),f33(x543,x544,x542,x545)) % 0.48/0.68 [55]~E(x551,x552)+E(f33(x553,x554,x555,x551),f33(x553,x554,x555,x552)) % 0.48/0.68 [56]~E(x561,x562)+E(f25(x561),f25(x562)) % 0.48/0.68 [57]~E(x571,x572)+E(f26(x571),f26(x572)) % 0.48/0.68 [58]~E(x581,x582)+E(f34(x581,x583,x584,x585),f34(x582,x583,x584,x585)) % 0.48/0.68 [59]~E(x591,x592)+E(f34(x593,x591,x594,x595),f34(x593,x592,x594,x595)) % 0.48/0.68 [60]~E(x601,x602)+E(f34(x603,x604,x601,x605),f34(x603,x604,x602,x605)) % 0.48/0.68 [61]~E(x611,x612)+E(f34(x613,x614,x615,x611),f34(x613,x614,x615,x612)) % 0.48/0.68 [62]~E(x621,x622)+E(f19(x621,x623,x624),f19(x622,x623,x624)) % 0.48/0.68 [63]~E(x631,x632)+E(f19(x633,x631,x634),f19(x633,x632,x634)) % 0.48/0.68 [64]~E(x641,x642)+E(f19(x643,x644,x641),f19(x643,x644,x642)) % 0.48/0.68 [65]~E(x651,x652)+E(f29(x651,x653,x654),f29(x652,x653,x654)) % 0.48/0.68 [66]~E(x661,x662)+E(f29(x663,x661,x664),f29(x663,x662,x664)) % 0.48/0.68 [67]~E(x671,x672)+E(f29(x673,x674,x671),f29(x673,x674,x672)) % 0.48/0.68 [68]~E(x681,x682)+E(f31(x681,x683),f31(x682,x683)) % 0.48/0.68 [69]~E(x691,x692)+E(f31(x693,x691),f31(x693,x692)) % 0.48/0.68 [70]~E(x701,x702)+E(f39(x701,x703),f39(x702,x703)) % 0.48/0.68 [71]~E(x711,x712)+E(f39(x713,x711),f39(x713,x712)) % 0.48/0.68 [72]~E(x721,x722)+E(f35(x721,x723,x724),f35(x722,x723,x724)) % 0.48/0.68 [73]~E(x731,x732)+E(f35(x733,x731,x734),f35(x733,x732,x734)) % 0.48/0.68 [74]~E(x741,x742)+E(f35(x743,x744,x741),f35(x743,x744,x742)) % 0.48/0.68 [75]~E(x751,x752)+E(f37(x751,x753,x754,x755),f37(x752,x753,x754,x755)) % 0.48/0.68 [76]~E(x761,x762)+E(f37(x763,x761,x764,x765),f37(x763,x762,x764,x765)) % 0.48/0.68 [77]~E(x771,x772)+E(f37(x773,x774,x771,x775),f37(x773,x774,x772,x775)) % 0.48/0.68 [78]~E(x781,x782)+E(f37(x783,x784,x785,x781),f37(x783,x784,x785,x782)) % 0.48/0.68 [79]~E(x791,x792)+E(f30(x791,x793),f30(x792,x793)) % 0.48/0.68 [80]~E(x801,x802)+E(f30(x803,x801),f30(x803,x802)) % 0.48/0.68 [81]~P1(x811)+P1(x812)+~E(x811,x812) % 0.48/0.68 [82]~P2(x821)+P2(x822)+~E(x821,x822) % 0.48/0.68 [83]~P3(x831)+P3(x832)+~E(x831,x832) % 0.48/0.68 [84]~P21(x841)+P21(x842)+~E(x841,x842) % 0.48/0.68 [85]~P19(x851)+P19(x852)+~E(x851,x852) % 0.48/0.68 [86]~P30(x861)+P30(x862)+~E(x861,x862) % 0.48/0.68 [87]~P22(x871)+P22(x872)+~E(x871,x872) % 0.48/0.68 [88]~P4(x881)+P4(x882)+~E(x881,x882) % 0.48/0.68 [89]~P5(x891)+P5(x892)+~E(x891,x892) % 0.48/0.68 [90]~P23(x901)+P23(x902)+~E(x901,x902) % 0.48/0.68 [91]~P24(x911)+P24(x912)+~E(x911,x912) % 0.48/0.68 [92]~P14(x921)+P14(x922)+~E(x921,x922) % 0.48/0.68 [93]~P15(x931)+P15(x932)+~E(x931,x932) % 0.48/0.68 [94]~P16(x941)+P16(x942)+~E(x941,x942) % 0.48/0.68 [95]~P25(x951)+P25(x952)+~E(x951,x952) % 0.48/0.68 [96]~P31(x961)+P31(x962)+~E(x961,x962) % 0.48/0.68 [97]~P27(x971)+P27(x972)+~E(x971,x972) % 0.48/0.68 [98]P8(x982,x983,x984)+~E(x981,x982)+~P8(x981,x983,x984) % 0.48/0.68 [99]P8(x993,x992,x994)+~E(x991,x992)+~P8(x993,x991,x994) % 0.48/0.68 [100]P8(x1003,x1004,x1002)+~E(x1001,x1002)+~P8(x1003,x1004,x1001) % 0.48/0.68 [101]~P26(x1011)+P26(x1012)+~E(x1011,x1012) % 0.48/0.68 [102]P6(x1022,x1023,x1024)+~E(x1021,x1022)+~P6(x1021,x1023,x1024) % 0.48/0.68 [103]P6(x1033,x1032,x1034)+~E(x1031,x1032)+~P6(x1033,x1031,x1034) % 0.48/0.68 [104]P6(x1043,x1044,x1042)+~E(x1041,x1042)+~P6(x1043,x1044,x1041) % 0.48/0.68 [105]P9(x1052,x1053,x1054,x1055)+~E(x1051,x1052)+~P9(x1051,x1053,x1054,x1055) % 0.48/0.68 [106]P9(x1063,x1062,x1064,x1065)+~E(x1061,x1062)+~P9(x1063,x1061,x1064,x1065) % 0.48/0.68 [107]P9(x1073,x1074,x1072,x1075)+~E(x1071,x1072)+~P9(x1073,x1074,x1071,x1075) % 0.48/0.68 [108]P9(x1083,x1084,x1085,x1082)+~E(x1081,x1082)+~P9(x1083,x1084,x1085,x1081) % 0.48/0.68 [109]~P32(x1091)+P32(x1092)+~E(x1091,x1092) % 0.48/0.68 [110]P11(x1102,x1103,x1104)+~E(x1101,x1102)+~P11(x1101,x1103,x1104) % 0.48/0.68 [111]P11(x1113,x1112,x1114)+~E(x1111,x1112)+~P11(x1113,x1111,x1114) % 0.48/0.68 [112]P11(x1123,x1124,x1122)+~E(x1121,x1122)+~P11(x1123,x1124,x1121) % 0.48/0.68 [113]P12(x1132,x1133,x1134)+~E(x1131,x1132)+~P12(x1131,x1133,x1134) % 0.48/0.68 [114]P12(x1143,x1142,x1144)+~E(x1141,x1142)+~P12(x1143,x1141,x1144) % 0.48/0.68 [115]P12(x1153,x1154,x1152)+~E(x1151,x1152)+~P12(x1153,x1154,x1151) % 0.48/0.68 [116]~P17(x1161)+P17(x1162)+~E(x1161,x1162) % 0.48/0.68 [117]P7(x1172,x1173,x1174)+~E(x1171,x1172)+~P7(x1171,x1173,x1174) % 0.48/0.68 [118]P7(x1183,x1182,x1184)+~E(x1181,x1182)+~P7(x1183,x1181,x1184) % 0.48/0.68 [119]P7(x1193,x1194,x1192)+~E(x1191,x1192)+~P7(x1193,x1194,x1191) % 0.48/0.68 [120]~P28(x1201)+P28(x1202)+~E(x1201,x1202) % 0.48/0.68 [121]~P10(x1211)+P10(x1212)+~E(x1211,x1212) % 0.48/0.68 [122]~P20(x1221)+P20(x1222)+~E(x1221,x1222) % 0.48/0.68 [123]~P18(x1231)+P18(x1232)+~E(x1231,x1232) % 0.48/0.68 [124]~P13(x1241)+P13(x1242)+~E(x1241,x1242) % 0.48/0.68 [125]~P29(x1251)+P29(x1252)+~E(x1251,x1252) % 0.48/0.68 % 0.48/0.68 %------------------------------------------- % 0.48/0.68 cnf(546,plain, % 0.48/0.68 ($false), % 0.48/0.68 inference(scs_inference,[],[225,211,456,451]), % 0.48/0.68 ['proof']). % 0.48/0.68 % SZS output end Proof % 0.48/0.68 % Total time :0.035942s %------------------------------------------------------------------------------