%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL774-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 : n020.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:48 AM UTC 2026 % Result : Unsatisfiable 0.51s 0.65s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL774-1 : TPTP v9.3.1. Released v4.1.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.35 % Computer : n020.cluster.edu % 0.07/0.35 % Model : x86_64 x86_64 % 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.35 % Memory : 8046.5625MB % 0.07/0.35 % OS : Linux 6.8.0-71-generic % 0.07/0.35 % CPULimit : 300 % 0.07/0.35 % WCLimit : 300 % 0.07/0.35 % DateTime : Sat Sep 5 17:28:42 UTC 2026 % 0.07/0.35 % CPUTime : % 0.25/0.52 start to proof:theBenchmark % 0.43/0.60 %------------------------------------------- % 0.43/0.60 % File :CSE---1.7 % 0.43/0.60 % Problem :theBenchmark % 0.43/0.60 % Transform :cnf % 0.43/0.60 % Format :tptp:raw % 0.43/0.60 % Command :java -jar mcs_scs.jar %d %s % 0.43/0.60 % 0.43/0.60 % Result :Theorem 0.024953s % 0.43/0.60 % Output :CNFRefutation 0.024953s % 0.43/0.60 %------------------------------------------- % 0.43/0.60 %------------------------------------------------------------------------------ % 0.43/0.60 % File : LCL774-1 : TPTP v9.3.1. Released v4.1.0. % 0.43/0.60 % Domain : Logic Calculi % 0.43/0.60 % Problem : Strong normalization of typed lambda calculus 081_4 % 0.43/0.60 % Version : Especial. % 0.43/0.60 % English : % 0.43/0.61 % 0.43/0.61 % Refs : [vON99] von Oheimb & Nipkow (1999), Machine-Checking the Java % 0.43/0.61 % : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.43/0.61 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.43/0.61 % Source : [Nip10] % 0.43/0.61 % Names : StrongNorm-081_4 [Nip10] % 0.43/0.61 % 0.43/0.61 % Status : Unsatisfiable % 0.43/0.61 % Rating : 0.17 v9.3.0, 0.05 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v5.5.0, 0.05 v5.4.0, 0.10 v5.3.0, 0.06 v5.2.0, 0.00 v5.1.0, 0.06 v5.0.0, 0.07 v4.1.0 % 0.43/0.61 % Syntax : Number of clauses : 382 ( 108 unt; 54 nHn; 226 RR) % 0.43/0.61 % Number of literals : 848 ( 296 equ; 436 neg) % 0.43/0.61 % Maximal clause size : 5 ( 2 avg) % 0.43/0.61 % Maximal term depth : 5 ( 1 avg) % 0.43/0.61 % Number of predicates : 38 ( 37 usr; 0 prp; 1-3 aty) % 0.43/0.61 % Number of functors : 20 ( 20 usr; 3 con; 0-3 aty) % 0.43/0.61 % Number of variables : 977 ( 89 sgn) % 0.43/0.61 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.43/0.61 % 0.43/0.61 % Comments : % 0.43/0.61 %------------------------------------------------------------------------------ % 0.43/0.61 cnf(cls_class__semiring_Osemiring__rules_I7_J_0,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.61 | c_HOL_Otimes__class_Otimes(V_a,V_b,T_a) = c_HOL_Otimes__class_Otimes(V_b,V_a,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_add__is__0_2,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_double__eq__0__iff_1,axiom, % 0.43/0.61 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_nat__mult__commute_0,axiom, % 0.43/0.61 c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) = c_HOL_Otimes__class_Otimes(V_n,V_m,tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_class__semiring_Omul__c_0,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.61 | c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) = c_HOL_Otimes__class_Otimes(V_y,V_x,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_diff__add__cancel_0,axiom, % 0.43/0.61 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_class__ringb_Oadd__mul__solve_1,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.61 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_y,T_a),c_HOL_Otimes__class_Otimes(V_x,V_z,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_z,T_a),c_HOL_Otimes__class_Otimes(V_x,V_y,T_a),T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_class__ringb_Onoteq__reduce_1,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.61 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_c,T_a),c_HOL_Otimes__class_Otimes(V_x,V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_d,T_a),c_HOL_Otimes__class_Otimes(V_x,V_c,T_a),T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_natgb_Onoteq__reduce_1,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_c,tc_nat),c_HOL_Otimes__class_Otimes(V_x,V_d,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_d,tc_nat),c_HOL_Otimes__class_Otimes(V_x,V_c,tc_nat),tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_natgb_Oadd__mul__solve_1,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_y,tc_nat),c_HOL_Otimes__class_Otimes(V_x,V_z,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_z,tc_nat),c_HOL_Otimes__class_Otimes(V_x,V_y,tc_nat),tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_add__is__1_4,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_eq__add__iff1_1,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Oring(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_e,T_a),V_c,T_a),T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_add__Suc__right_0,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat)) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_add__Suc_0,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(c_Suc(V_m),V_n,tc_nat) = c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat)) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_eq__add__iff2_1,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Oring(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),V_e,T_a),V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_eq__add__iff2_0,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Oring(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a) != c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a) % 0.43/0.61 | V_c = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),V_e,T_a),V_d,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_eq__add__iff1_0,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Oring(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a) != c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_e,T_a),V_c,T_a) = V_d ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_less__add__Suc1_0,axiom, % 0.43/0.61 c_HOL_Oord__class_Oless(V_i,c_Suc(c_HOL_Oplus__class_Oplus(V_i,V_m,tc_nat)),tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_less__add__Suc2_0,axiom, % 0.43/0.61 c_HOL_Oord__class_Oless(V_i,c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_i,tc_nat)),tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_less__iff__Suc__add_1,axiom, % 0.43/0.61 c_HOL_Oord__class_Oless(V_m,c_Suc(c_HOL_Oplus__class_Oplus(V_m,V_x,tc_nat)),tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_termination__basic__simps_I1_J_0,axiom, % 0.43/0.61 ( c_HOL_Oord__class_Oless(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,tc_nat),tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_termination__basic__simps_I2_J_0,axiom, % 0.43/0.61 ( c_HOL_Oord__class_Oless(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,tc_nat),tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(V_x,V_z,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_add__lessD1_0,axiom, % 0.43/0.61 ( c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_k,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_trans__less__add1_0,axiom, % 0.43/0.61 ( c_HOL_Oord__class_Oless(V_i,c_HOL_Oplus__class_Oplus(V_j,V_m,tc_nat),tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_trans__less__add2_0,axiom, % 0.43/0.61 ( c_HOL_Oord__class_Oless(V_i,c_HOL_Oplus__class_Oplus(V_m,V_j,tc_nat),tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(V_a,V_c,T_a) = c_HOL_Oplus__class_Oplus(V_c,V_a,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.43/0.61 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_nat__add__commute_0,axiom, % 0.43/0.61 c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) = c_HOL_Oplus__class_Oplus(V_n,V_m,tc_nat) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_less__add__eq__less_0,axiom, % 0.43/0.61 ( c_HOL_Oplus__class_Oplus(V_m,V_l,tc_nat) != c_HOL_Oplus__class_Oplus(V_k,V_n,tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.43/0.61 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.43/0.61 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.61 | c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_y,V_x,T_a) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_mult__eq__1__iff_0,axiom, % 0.43/0.61 ( c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.43/0.61 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_mult__eq__1__iff_1,axiom, % 0.43/0.61 ( c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.43/0.61 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_diff__less__mono2_0,axiom, % 0.43/0.61 ( 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.43/0.61 | ~ c_HOL_Oord__class_Oless(V_m,V_l,tc_nat) % 0.43/0.61 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.43/0.61 % 0.43/0.61 cnf(cls_of__nat__eq__iff_0,axiom, % 0.43/0.61 ( ~ class_Nat_Osemiring__char__0(T_a) % 0.43/0.62 | c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a) != c_Nat_Osemiring__1__class_Oof__nat(V_n,T_a) % 0.43/0.62 | V_m = V_n ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__ringb_Oadd__r0__iff_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.62 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.62 | V_x != c_HOL_Oplus__class_Oplus(V_x,V_a,T_a) % 0.43/0.62 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__eq__self__zero_0,axiom, % 0.43/0.62 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != V_m % 0.43/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_natgb_Oadd__r0__iff_0,axiom, % 0.43/0.62 ( V_x != c_HOL_Oplus__class_Oplus(V_x,V_a,tc_nat) % 0.43/0.62 | V_a = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_eq__iff__diff__eq__0_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_right__minus__eq_1,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__0__right_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__self_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_a,V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__ringb_Osubr0__iff_1,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.62 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__self__eq__0_0,axiom, % 0.43/0.62 c_HOL_Ominus__class_Ominus(V_m,V_m,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_minus__nat_Odiff__0_0,axiom, % 0.43/0.62 c_HOL_Ominus__class_Ominus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m ). % 0.43/0.62 % 0.43/0.62 cnf(cls_nat__mult__eq__cancel__disj_0,axiom, % 0.43/0.62 ( c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat) != c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat) % 0.43/0.62 | V_m = V_n % 0.43/0.62 | V_k = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_mult__cancel1_0,axiom, % 0.43/0.62 ( c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat) != c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat) % 0.43/0.62 | V_k = c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.62 | V_m = V_n ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_mult__cancel2_0,axiom, % 0.43/0.62 ( c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat) != c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat) % 0.43/0.62 | V_k = c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.62 | V_m = V_n ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__is__0_0,axiom, % 0.43/0.62 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.62 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__is__0_1,axiom, % 0.43/0.62 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_double__eq__0__iff_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_a,V_a,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_less__add__iff2_1,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Opordered__ring(T_a) % 0.43/0.62 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a),T_a) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),V_e,T_a),V_d,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_less__add__iff2_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Opordered__ring(T_a) % 0.43/0.62 | c_HOL_Oord__class_Oless(V_c,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),V_e,T_a),V_d,T_a),T_a) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_less__add__iff1_1,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Opordered__ring(T_a) % 0.43/0.62 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a),T_a) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_e,T_a),V_c,T_a),V_d,T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_less__add__iff1_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Opordered__ring(T_a) % 0.43/0.62 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_e,T_a),V_c,T_a),V_d,T_a) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),V_c,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_d,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_mult__eq__0__iff_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a) % 0.43/0.62 | c_HOL_Otimes__class_Otimes(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_b = c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_no__zero__divisors_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Ono__zero__divisors(T_a) % 0.43/0.62 | c_HOL_Otimes__class_Otimes(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_b = c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_a = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__less__Suc_0,axiom, % 0.43/0.62 c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),c_Suc(V_m),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_x,V_y,T_a),V_z,T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__cancel__21_1,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) = c_HOL_Oplus__class_Oplus(V_y,c_HOL_Oplus__class_Oplus(V_x,V_z,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_nat__add__left__commute_0,axiom, % 0.43/0.62 c_HOL_Oplus__class_Oplus(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(V_y,c_HOL_Oplus__class_Oplus(V_x,V_z,tc_nat),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_nat__add__assoc_0,axiom, % 0.43/0.62 c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_k,tc_nat) = c_HOL_Oplus__class_Oplus(V_m,c_HOL_Oplus__class_Oplus(V_n,V_k,tc_nat),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) = c_HOL_Oplus__class_Oplus(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(V_c,V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),V_d,T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),V_b,T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(V_c,V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(V_c,c_HOL_Oplus__class_Oplus(V_a,V_d,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__gr__0_0,axiom, % 0.43/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.43/0.62 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__cancel__21_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) != c_HOL_Oplus__class_Oplus(V_y,V_u,T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(V_x,V_z,T_a) = V_u ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_one__is__add_5,axiom, % 0.43/0.62 c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__add__0_0,axiom, % 0.43/0.62 c_HOL_Ominus__class_Ominus(V_n,c_HOL_Oplus__class_Oplus(V_n,V_m,tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__diff__left_0,axiom, % 0.43/0.62 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,c_HOL_Oplus__class_Oplus(V_j,V_k,tc_nat),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_eq__eqI_1,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) % 0.43/0.62 | V_xa = V_y ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_eq__eqI_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.62 | 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.43/0.62 | V_x_H = V_y_H ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_nat__mult__eq__cancel1_0,axiom, % 0.43/0.62 ( c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat) != c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) % 0.43/0.62 | V_m = V_n ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_one__is__add_3,axiom, % 0.43/0.62 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) % 0.43/0.62 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.43/0.62 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_one__is__add_0,axiom, % 0.43/0.62 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) % 0.43/0.62 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.62 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_mult__less__cancel2_0,axiom, % 0.43/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat),c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat),tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_mult__less__cancel1_0,axiom, % 0.43/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__Suc__shift_0,axiom, % 0.43/0.62 c_HOL_Oplus__class_Oplus(c_Suc(V_m),V_n,tc_nat) = c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__0__eq__0_0,axiom, % 0.43/0.62 c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__cancel2_0,axiom, % 0.43/0.62 c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_k,tc_nat),c_HOL_Oplus__class_Oplus(V_n,V_k,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__cancel_0,axiom, % 0.43/0.62 c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_k,V_m,tc_nat),c_HOL_Oplus__class_Oplus(V_k,V_n,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_left__add__mult__distrib_0,axiom, % 0.43/0.62 c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_i,V_u,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_j,V_u,tc_nat),V_k,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_u,tc_nat),V_k,tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_combine__common__factor_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Osemiring(T_a) % 0.43/0.62 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_e,T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_b,V_e,T_a),V_c,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_e,T_a),V_c,T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_of__nat__0_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.43/0.62 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Ozero__class_Ozero(tc_nat),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_nat__0__less__mult__iff_1,axiom, % 0.43/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_nat__0__less__mult__iff_0,axiom, % 0.43/0.62 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_add__neg__neg_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.43/0.62 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.62 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_class__ringb_Osubr0__iff_0,axiom, % 0.43/0.62 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.62 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_x = V_y ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_right__minus__eq_0,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_a = V_b ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_eq__iff__diff__eq__0_1,axiom, % 0.43/0.62 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.43/0.62 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.43/0.62 | V_a = V_b ) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__mult__distrib2_0,axiom, % 0.43/0.62 c_HOL_Otimes__class_Otimes(V_k,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) ). % 0.43/0.62 % 0.43/0.62 cnf(cls_diff__mult__distrib_0,axiom, % 0.43/0.63 c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_k,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat),c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat),tc_nat) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_diff__commute_0,axiom, % 0.43/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(c_HOL_Ominus__class_Ominus(V_i,V_k,tc_nat),V_j,tc_nat) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_not__square__less__zero_0,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_Suc__mult__less__cancel1_1,axiom, % 0.43/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(V_k),V_m,tc_nat),c_HOL_Otimes__class_Otimes(c_Suc(V_k),V_n,tc_nat),tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_Suc__mult__less__cancel1_0,axiom, % 0.43/0.63 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(V_k),V_m,tc_nat),c_HOL_Otimes__class_Otimes(c_Suc(V_k),V_n,tc_nat),tc_nat) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_natgb_Oadd__cancel_0,axiom, % 0.43/0.63 ( c_HOL_Oplus__class_Oplus(V_x,V_y,tc_nat) != c_HOL_Oplus__class_Oplus(V_x,V_z,tc_nat) % 0.43/0.63 | V_y = V_z ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_nat__add__right__cancel_0,axiom, % 0.43/0.63 ( c_HOL_Oplus__class_Oplus(V_m,V_k,tc_nat) != c_HOL_Oplus__class_Oplus(V_n,V_k,tc_nat) % 0.43/0.63 | V_m = V_n ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_nat__add__left__cancel_0,axiom, % 0.43/0.63 ( c_HOL_Oplus__class_Oplus(V_k,V_m,tc_nat) != c_HOL_Oplus__class_Oplus(V_k,V_n,tc_nat) % 0.43/0.63 | V_m = V_n ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.43/0.63 | ~ class_Int_Onumber__ring(T_a) % 0.43/0.63 | c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) != c_HOL_Oplus__class_Oplus(V_x,V_z,T_a) % 0.43/0.63 | V_y = V_z ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_add__imp__eq_0,axiom, % 0.43/0.63 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.43/0.63 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Oplus__class_Oplus(V_a,V_c,T_a) % 0.43/0.63 | V_b = V_c ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_add__left__cancel_0,axiom, % 0.43/0.63 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.43/0.63 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Oplus__class_Oplus(V_a,V_c,T_a) % 0.43/0.63 | V_b = V_c ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_add__right__cancel_0,axiom, % 0.43/0.63 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.43/0.63 | c_HOL_Oplus__class_Oplus(V_b,V_a,T_a) != c_HOL_Oplus__class_Oplus(V_c,V_a,T_a) % 0.43/0.63 | V_b = V_c ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_add__is__1_3,axiom, % 0.43/0.63 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.43/0.63 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.43/0.63 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_add__is__1_0,axiom, % 0.43/0.63 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.43/0.63 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.43/0.63 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_Suc__diff__diff_0,axiom, % 0.43/0.63 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.43/0.63 % 0.43/0.63 cnf(cls_sum__squares__gt__zero__iff_1,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),T_a) % 0.43/0.63 | V_x = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_sum__squares__gt__zero__iff_2,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),T_a) % 0.43/0.63 | V_y = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.43/0.63 | c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_c,V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_d,T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_of__nat__less__0__iff_0,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_Nat_Osemiring__1__class_Oof__nat(V_m,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__cancel__left__disj_0,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__cancel__left__disj_3,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__cancel__right__disj_0,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__cancel__right__disj_3,axiom, % 0.43/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.43/0.63 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__cancel2_2,axiom, % 0.43/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat),c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat),tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__cancel1_2,axiom, % 0.43/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) ) ). % 0.43/0.63 % 0.43/0.63 cnf(cls_mult__less__mono2_0,axiom, % 0.43/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_i,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_j,tc_nat),tc_nat) % 0.43/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__mono1_0,axiom, % 0.51/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_i,V_k,tc_nat),c_HOL_Otimes__class_Otimes(V_j,V_k,tc_nat),tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_nat__mult__less__cancel1_0,axiom, % 0.51/0.63 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_nat__mult__less__cancel1_1,axiom, % 0.51/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__left__neg_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__left__neg_1,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__left__pos_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__left__pos_1,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__strict__left__mono__neg_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__strict__left__mono_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__left__disj_4,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__left__disj_5,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__strict__right__mono__neg_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__strict__right__mono_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__right__disj_4,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__less__cancel__right__disj_5,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_mult__strict__left__mono__comm_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__comm__semiring__strict(T_a) % 0.51/0.63 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_class__semiring_Osemiring__rules_I1_J_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_m,T_a),c_HOL_Otimes__class_Otimes(V_b,V_m,T_a),T_a) = c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_m,T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_class__semiring_Oadd__0_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a) = V_x ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_comm__monoid__add_Omult__1_0,axiom, % 0.51/0.63 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_natgb_Oadd__r0__iff_1,axiom, % 0.51/0.63 V_x = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_plus__nat_Oadd__0_0,axiom, % 0.51/0.63 c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = V_n ). % 0.51/0.63 % 0.51/0.63 cnf(cls_Nat_Oadd__0__right_0,axiom, % 0.51/0.63 c_HOL_Oplus__class_Oplus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m ). % 0.51/0.63 % 0.51/0.63 cnf(cls_class__ringb_Oadd__r0__iff_1,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.51/0.63 | ~ class_Int_Onumber__ring(T_a) % 0.51/0.63 | V_x = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_comm__monoid__add_Omult__1__right_0,axiom, % 0.51/0.63 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_add__0__left_0,axiom, % 0.51/0.63 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_monoid__add__class_Oadd__0__right_0,axiom, % 0.51/0.63 ( ~ class_OrderedGroup_Omonoid__add(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_class__semiring_Osemiring__rules_I6_J_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_class__semiring_Osemiring__rules_I5_J_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.63 | c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_sum__squares__gt__zero__iff_0,axiom, % 0.51/0.63 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a),T_a) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_diff__add__inverse2_0,axiom, % 0.51/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_n,tc_nat) = V_m ). % 0.51/0.63 % 0.51/0.63 cnf(cls_diff__add__inverse_0,axiom, % 0.51/0.63 c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_n,V_m,tc_nat),V_n,tc_nat) = V_m ). % 0.51/0.63 % 0.51/0.63 cnf(cls_add__diff__cancel_0,axiom, % 0.51/0.63 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.51/0.63 | c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_b,T_a) = V_a ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_add__gr__0_2,axiom, % 0.51/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.63 % 0.51/0.63 cnf(cls_add__gr__0_1,axiom, % 0.51/0.63 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat) % 0.51/0.63 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) ) ). % 0.51/0.63 % 0.51/0.64 cnf(cls_zero__less__double__add__iff__zero__less__single__add_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_zero__less__double__add__iff__zero__less__single__add_1,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_no__zero__divirors__neq0_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ono__zero__divisors(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_a,V_b,T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.51/0.64 | V_a = c_HOL_Ozero__class_Ozero(T_a) % 0.51/0.64 | V_b = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__is__0_0,axiom, % 0.51/0.64 ( c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.64 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_double__add__less__zero__iff__single__less__zero_1,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_double__add__less__zero__iff__single__less__zero_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_even__less__0__iff_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_even__less__0__iff_1,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_one__is__add_1,axiom, % 0.51/0.64 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) % 0.51/0.64 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.51/0.64 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_one__is__add_2,axiom, % 0.51/0.64 ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) % 0.51/0.64 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_zero__less__mult__pos2_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Otimes__class_Otimes(V_b,V_a,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_zero__less__mult__pos_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__pos__pos_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__neg__neg_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_nat__0__less__mult__iff_2,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__Suc__right_0,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(V_m,c_Suc(V_n),tc_nat) = c_HOL_Oplus__class_Oplus(V_m,c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__Suc_0,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(c_Suc(V_m),V_n,tc_nat) = c_HOL_Oplus__class_Oplus(V_n,c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_not__sum__squares__lt__zero_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_of__nat__mult_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.51/0.64 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),T_a) = c_HOL_Otimes__class_Otimes(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.51/0.64 % 0.51/0.64 cnf(cls_class__ringb_Oadd__mul__solve_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.51/0.64 | ~ class_Int_Onumber__ring(T_a) % 0.51/0.64 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_w,V_y,T_a),c_HOL_Otimes__class_Otimes(V_x,V_z,T_a),T_a) != c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_w,V_z,T_a),c_HOL_Otimes__class_Otimes(V_x,V_y,T_a),T_a) % 0.51/0.64 | V_y = V_z % 0.51/0.64 | V_w = V_x ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__ringb_Onoteq__reduce_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.51/0.64 | ~ class_Int_Onumber__ring(T_a) % 0.51/0.64 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_d,T_a),T_a) != c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_d,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) % 0.51/0.64 | V_c = V_d % 0.51/0.64 | V_a = V_b ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_natgb_Onoteq__reduce_0,axiom, % 0.51/0.64 ( c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_c,tc_nat),c_HOL_Otimes__class_Otimes(V_b,V_d,tc_nat),tc_nat) != c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_d,tc_nat),c_HOL_Otimes__class_Otimes(V_b,V_c,tc_nat),tc_nat) % 0.51/0.64 | V_c = V_d % 0.51/0.64 | V_a = V_b ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_natgb_Oadd__mul__solve_0,axiom, % 0.51/0.64 ( c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_w,V_y,tc_nat),c_HOL_Otimes__class_Otimes(V_x,V_z,tc_nat),tc_nat) != c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_w,V_z,tc_nat),c_HOL_Otimes__class_Otimes(V_x,V_y,tc_nat),tc_nat) % 0.51/0.64 | V_y = V_z % 0.51/0.64 | V_w = V_x ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_diff__Suc__Suc_0,axiom, % 0.51/0.64 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.51/0.64 % 0.51/0.64 cnf(cls_mult__eq__1__iff_2,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I13_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_rx,T_a),c_HOL_Otimes__class_Otimes(V_ly,V_ry,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I14_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a) = c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_ly,c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I15_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a) = c_HOL_Otimes__class_Otimes(V_rx,c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_ry,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I9_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I10_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__eq__0__iff_2,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__eq__0__iff_1,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oring__no__zero__divisors(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__zero__right_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Omult__zero(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__zero__left_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Omult__zero(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__is__0_1,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__is__0_2,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Omul__0_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),V_x,T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_less__imp__diff__less_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_j,V_n,tc_nat),V_k,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_one__is__add_4,axiom, % 0.51/0.64 c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__pos__pos_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__comm__monoid__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_diffs0__imp__equal_0,axiom, % 0.51/0.64 ( c_HOL_Ominus__class_Ominus(V_n,V_m,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.64 | c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.64 | V_m = V_n ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__strict__mono_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_d,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__less__mono_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_k,tc_nat),c_HOL_Oplus__class_Oplus(V_j,V_l,tc_nat),tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_k,V_l,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_less__iff__diff__less__0_1,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.64 | ~ 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.51/0.64 % 0.51/0.64 cnf(cls_less__iff__diff__less__0_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.51/0.64 | 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.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_of__nat__less__iff_1,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.51/0.64 | 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.51/0.64 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_of__nat__less__iff_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.64 | ~ 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.51/0.64 % 0.51/0.64 cnf(cls_mult__less__cancel1_1,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__less__cancel2_1,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat),c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat),tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__left__idem_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Oab__semigroup__idem__mult(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_x,c_HOL_Otimes__class_Otimes(V_x,V_y,T_a),T_a) = c_HOL_Otimes__class_Otimes(V_x,V_y,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__pos__neg2_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_b,V_a,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__pos__neg_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__neg__pos_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semiring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ozero__class_Ozero(T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_pos__add__strict_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_b,V_c,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__cancel1_1,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) = c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__cancel2_1,axiom, % 0.51/0.64 c_HOL_Otimes__class_Otimes(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Otimes__class_Otimes(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_not__add__less1_0,axiom, % 0.51/0.64 ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_j,tc_nat),V_i,tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_not__add__less2_0,axiom, % 0.51/0.64 ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_j,V_i,tc_nat),V_i,tc_nat) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__ringb_Oadd__scale__eq__noteq_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.51/0.64 | ~ class_Int_Onumber__ring(T_a) % 0.51/0.64 | c_HOL_Oplus__class_Oplus(V_x,c_HOL_Otimes__class_Otimes(V_r,V_c,T_a),T_a) != c_HOL_Oplus__class_Oplus(V_x,c_HOL_Otimes__class_Otimes(V_r,V_d,T_a),T_a) % 0.51/0.64 | V_c = V_d % 0.51/0.64 | V_r = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_natgb_Oadd__scale__eq__noteq_0,axiom, % 0.51/0.64 ( c_HOL_Oplus__class_Oplus(V_x,c_HOL_Otimes__class_Otimes(V_r,V_c,tc_nat),tc_nat) != c_HOL_Oplus__class_Oplus(V_x,c_HOL_Otimes__class_Otimes(V_r,V_d,tc_nat),tc_nat) % 0.51/0.64 | V_c = V_d % 0.51/0.64 | V_r = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_sum__squares__eq__zero__iff_1,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.51/0.64 | V_y = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_sum__squares__eq__zero__iff_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_x,T_a),c_HOL_Otimes__class_Otimes(V_y,V_y,T_a),T_a) != c_HOL_Ozero__class_Ozero(T_a) % 0.51/0.64 | V_x = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_less__diff__conv_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_k,tc_nat),V_j,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_i,c_HOL_Ominus__class_Ominus(V_j,V_k,tc_nat),tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_less__diff__conv_1,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(V_i,c_HOL_Ominus__class_Ominus(V_j,V_k,tc_nat),tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_k,tc_nat),V_j,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__strict__right__mono_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__less__cancel__right_1,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__less__cancel__right_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__strict__left__mono_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_c,V_a,T_a),c_HOL_Oplus__class_Oplus(V_c,V_b,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__less__cancel__left_1,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_c,V_a,T_a),c_HOL_Oplus__class_Oplus(V_c,V_b,T_a),T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__less__cancel__left_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_c,V_a,T_a),c_HOL_Oplus__class_Oplus(V_c,V_b,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__less__mono1_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_i,V_k,tc_nat),c_HOL_Oplus__class_Oplus(V_j,V_k,tc_nat),tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_nat__add__left__cancel__less_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_k,V_m,tc_nat),c_HOL_Oplus__class_Oplus(V_k,V_n,tc_nat),tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_nat__add__left__cancel__less_1,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Oplus__class_Oplus(V_k,V_m,tc_nat),c_HOL_Oplus__class_Oplus(V_k,V_n,tc_nat),tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__is__1_5,axiom, % 0.51/0.64 c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__idem_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Oab__semigroup__idem__mult(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_x,V_x,T_a) = V_x ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_zero__less__diff_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.64 | ~ 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.51/0.64 % 0.51/0.64 cnf(cls_zero__less__diff_1,axiom, % 0.51/0.64 ( 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.51/0.64 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_sum__squares__eq__zero__iff_2,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(T_a),c_HOL_Ozero__class_Ozero(T_a),T_a),T_a) = c_HOL_Ozero__class_Ozero(T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__less__cancel__right__disj_2,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__less__cancel__right__disj_1,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__less__cancel__left__disj_2,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_c,c_HOL_Ozero__class_Ozero(T_a),T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_mult__less__cancel__left__disj_1,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Oordered__ring__strict(T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.64 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_c,V_a,T_a),c_HOL_Otimes__class_Otimes(V_c,V_b,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_Suc__mult__cancel1_0,axiom, % 0.51/0.64 ( c_HOL_Otimes__class_Otimes(c_Suc(V_k),V_m,tc_nat) != c_HOL_Otimes__class_Otimes(c_Suc(V_k),V_n,tc_nat) % 0.51/0.64 | V_m = V_n ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_of__nat__add_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Osemiring__1(T_a) % 0.51/0.64 | c_Nat_Osemiring__1__class_Oof__nat(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),T_a) = c_HOL_Oplus__class_Oplus(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.51/0.64 % 0.51/0.64 cnf(cls_diff__less_0,axiom, % 0.51/0.64 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_m,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_less__eqI_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.51/0.64 | 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.51/0.64 | c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_less__eqI_1,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.51/0.64 | 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.51/0.64 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.51/0.64 | ~ c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__diff__inverse_0,axiom, % 0.51/0.64 ( c_HOL_Oplus__class_Oplus(V_n,c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),tc_nat) = V_m % 0.51/0.64 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__is__1_1,axiom, % 0.51/0.64 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.51/0.64 | V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.51/0.64 | V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_add__is__1_2,axiom, % 0.51/0.64 ( c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) % 0.51/0.64 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.64 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_ab__semigroup__mult__class_Omult__ac_I1_J_0,axiom, % 0.51/0.64 ( ~ class_OrderedGroup_Oab__semigroup__mult(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_a,V_b,T_a),V_c,T_a) = c_HOL_Otimes__class_Otimes(V_a,c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I16_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_rx,T_a),V_ly,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I17_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_ly,T_a),V_rx,T_a) = c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_ly,V_rx,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I18_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_lx,V_rx,T_a),V_ry,T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_class__semiring_Osemiring__rules_I19_J_0,axiom, % 0.51/0.64 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.64 | c_HOL_Otimes__class_Otimes(V_lx,c_HOL_Otimes__class_Otimes(V_rx,V_ry,T_a),T_a) = c_HOL_Otimes__class_Otimes(V_rx,c_HOL_Otimes__class_Otimes(V_lx,V_ry,T_a),T_a) ) ). % 0.51/0.64 % 0.51/0.64 cnf(cls_nat__mult__assoc_0,axiom, % 0.51/0.65 c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),V_k,tc_nat) = c_HOL_Otimes__class_Otimes(V_m,c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_class__semiring_Omul__a_0,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.65 | c_HOL_Otimes__class_Otimes(V_x,c_HOL_Otimes__class_Otimes(V_y,V_z,T_a),T_a) = c_HOL_Otimes__class_Otimes(c_HOL_Otimes__class_Otimes(V_x,V_y,T_a),V_z,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_class__semiring_Osemiring__rules_I8_J_0,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.65 | c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_comm__semiring__class_Odistrib_0,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring(T_a) % 0.51/0.65 | c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_a,V_c,T_a),c_HOL_Otimes__class_Otimes(V_b,V_c,T_a),T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_add__mult__distrib_0,axiom, % 0.51/0.65 c_HOL_Otimes__class_Otimes(c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),V_k,tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat),c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_add__mult__distrib2_0,axiom, % 0.51/0.65 c_HOL_Otimes__class_Otimes(V_k,c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat),tc_nat) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_class__semiring_Omul__d_0,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.51/0.65 | c_HOL_Otimes__class_Otimes(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_x,V_y,T_a),c_HOL_Otimes__class_Otimes(V_x,V_z,T_a),T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_order__less__asym_H_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_order__less__asym_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.51/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_xt1_I9_J_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Oorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_diff__Suc__less_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_n,c_Suc(V_i),tc_nat),V_n,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__pred_0,axiom, % 0.51/0.65 ( c_Suc(c_HOL_Ominus__class_Ominus(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = V_n % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__SucI_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__lessD_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_n__not__Suc__n_0,axiom, % 0.51/0.65 V_n != c_Suc(V_n) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__n__not__n_0,axiom, % 0.51/0.65 c_Suc(V_n) != V_n ). % 0.51/0.65 % 0.51/0.65 cnf(cls_n__less__n__mult__m_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_n,c_HOL_Otimes__class_Otimes(V_n,V_m,tc_nat),tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_m,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_n__less__m__mult__n_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_n,c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_m,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_neq0__conv_1,axiom, % 0.51/0.65 ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_liftn__0_0,axiom, % 0.51/0.65 c_Lambda_Oliftn(c_HOL_Ozero__class_Ozero(tc_nat),V_t,V_k) = V_t ). % 0.51/0.65 % 0.51/0.65 cnf(cls_gr0I_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.51/0.65 | V_n = c_HOL_Ozero__class_Ozero(tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_of__nat__0__less__iff_0,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) % 0.51/0.65 | ~ 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.51/0.65 % 0.51/0.65 cnf(cls_of__nat__0__less__iff_1,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Oordered__semidom(T_a) % 0.51/0.65 | 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.51/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__trans__Suc_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_Suc(V_i),V_k,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__Suc__eq_2,axiom, % 0.51/0.65 c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_lessI_0,axiom, % 0.51/0.65 c_HOL_Oord__class_Oless(V_n,c_Suc(V_n),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__neq__Zero_0,axiom, % 0.51/0.65 c_Suc(V_m) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_nat_Osimps_I3_J_0,axiom, % 0.51/0.65 c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.51/0.65 | V_x = V_y % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_linorder__less__linear_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.51/0.65 | V_x = V_y % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_linorder__neqE_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.51/0.65 | V_x = V_y ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_linorder__neqE__nat_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_y,V_x,tc_nat) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,tc_nat) % 0.51/0.65 | V_x = V_y ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_nat__neq__iff_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.65 | V_m = V_n ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.51/0.65 | V_x = V_y % 0.51/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.51/0.65 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.51/0.65 | V_x = V_y ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_liftn_Osimps_I1_J_1,axiom, % 0.51/0.65 ( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(c_HOL_Oplus__class_Oplus(V_i,V_n,tc_nat)) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_order__less__irrefl_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_linorder__neq__iff_1,axiom, % 0.51/0.65 ( ~ class_Orderings_Olinorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_order__less__le_1,axiom, % 0.51/0.65 ( ~ class_Orderings_Oorder(T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__not__refl_0,axiom, % 0.51/0.65 ~ c_HOL_Oord__class_Oless(V_n,V_n,tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_nat__less__le_1,axiom, % 0.51/0.65 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__Suc__eq__0__disj_0,axiom, % 0.51/0.65 ( V_m = c_Suc(c_ATP__Linkup_Osko__Nat__Xless__Suc__eq__0__disj__1__1(V_m,V_n)) % 0.51/0.65 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less__less__Suc__eq_0,axiom, % 0.51/0.65 ( V_n = V_m % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__antisym_0,axiom, % 0.51/0.65 ( V_m = V_n % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_n,V_m,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__SucE_0,axiom, % 0.51/0.65 ( V_m = V_n % 0.51/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__Suc0_1,axiom, % 0.51/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.51/0.65 % 0.51/0.65 cnf(cls_nat_Oinject_0,axiom, % 0.51/0.65 ( c_Suc(V_nat) != c_Suc(V_nat_H) % 0.51/0.65 | V_nat = V_nat_H ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__inject_0,axiom, % 0.51/0.65 ( c_Suc(V_x) != c_Suc(V_y) % 0.51/0.65 | V_x = V_y ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Zero__neq__Suc_0,axiom, % 0.51/0.65 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_m) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_nat_Osimps_I2_J_0,axiom, % 0.51/0.65 c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(V_nat_H) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_gr0__implies__Suc_0,axiom, % 0.51/0.65 ( V_n = c_Suc(c_ATP__Linkup_Osko__Nat__Xgr0__implies__Suc__1__1(V_n)) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__Suc0_0,axiom, % 0.51/0.65 ( V_n = c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_gr0__conv__Suc_0,axiom, % 0.51/0.65 ( V_n = c_Suc(c_ATP__Linkup_Osko__Nat__Xgr0__conv__Suc__1__1(V_n)) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__Suc__eq__0__disj_1,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_ATP__Linkup_Osko__Nat__Xless__Suc__eq__0__disj__1__1(V_m,V_n),V_n,tc_nat) % 0.51/0.65 | V_m = c_HOL_Ozero__class_Ozero(tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_order__less__trans_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Opreorder(T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_xt1_I10_J_0,axiom, % 0.51/0.65 ( ~ class_Orderings_Oorder(T_a) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_gr__implies__not0_0,axiom, % 0.51/0.65 ~ c_HOL_Oord__class_Oless(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less0_0,axiom, % 0.51/0.65 ~ c_HOL_Oord__class_Oless(V_n,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_one__less__mult_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Otimes__class_Otimes(V_m,V_n,tc_nat),tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_m,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_zero__less__Suc_0,axiom, % 0.51/0.65 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_n),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_gr0__conv__Suc_1,axiom, % 0.51/0.65 c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_x),tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__lessI_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) % 0.51/0.65 | c_Suc(V_m) = V_n % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less__less__Suc__eq_1,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_x,c_Suc(V_x),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less__eq_1,axiom, % 0.51/0.65 ( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_not__less__eq_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat) % 0.51/0.65 | c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_less__Suc__eq__0__disj_3,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_Suc(V_x),c_Suc(V_n),tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_x,V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__less__eq_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Suc__mono_0,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(c_Suc(V_m),c_Suc(V_n),tc_nat) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_abs_0,axiom, % 0.51/0.65 ( c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_s),c_Lambda_OdB_OAbs(V_t)) % 0.51/0.65 | ~ c_Lambda_Obeta(V_s,V_t) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_beta__cases_I2_J_0,axiom, % 0.51/0.65 ( V_s = c_Lambda_OdB_OAbs(c_Lambda_Osko__Lambda__Xbeta__cases__2__1(V_r,V_s)) % 0.51/0.65 | ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_r),V_s) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_substn_Osimps_I1_J_1,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.51/0.65 | c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_x),V_s,V_x) = c_Lambda_Oliftn(V_x,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_lift__preserves__beta_0,axiom, % 0.51/0.65 ( c_Lambda_Obeta(c_Lambda_Olift(V_r,V_i),c_Lambda_Olift(V_s,V_i)) % 0.51/0.65 | ~ c_Lambda_Obeta(V_r,V_s) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_lift_Osimps_I1_J_0,axiom, % 0.51/0.65 ( c_Lambda_Olift(c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__lift_0,axiom, % 0.51/0.65 c_Lambda_Osubst(c_Lambda_Olift(V_t,V_k),V_s,V_k) = V_t ). % 0.51/0.65 % 0.51/0.65 cnf(cls_liftn_Osimps_I1_J_0,axiom, % 0.51/0.65 ( c_Lambda_Oliftn(V_n,c_Lambda_OdB_OVar(V_i),V_k) = c_Lambda_OdB_OVar(V_i) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_i,V_k,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__Var_1,axiom, % 0.51/0.65 ( c_HOL_Oord__class_Oless(V_x,V_x,tc_nat) % 0.51/0.65 | c_Lambda_Osubst(c_Lambda_OdB_OVar(V_x),V_s,V_x) = V_s ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_substn__subst__n_0,axiom, % 0.51/0.65 c_Lambda_Osubstn(V_t,V_s,V_n) = c_Lambda_Osubst(V_t,c_Lambda_Oliftn(V_n,V_s,c_HOL_Ozero__class_Ozero(tc_nat)),V_n) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__Var_2,axiom, % 0.51/0.65 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.51/0.65 | V_i = V_k % 0.51/0.65 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__preserves__beta_0,axiom, % 0.51/0.65 ( c_Lambda_Obeta(c_Lambda_Osubst(V_r,V_t,V_i),c_Lambda_Osubst(V_s,V_t,V_i)) % 0.51/0.65 | ~ c_Lambda_Obeta(V_r,V_s) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_liftn__lift_0,axiom, % 0.51/0.65 c_Lambda_Oliftn(c_Suc(V_n),V_t,V_k) = c_Lambda_Olift(c_Lambda_Oliftn(V_n,V_t,V_k),V_k) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_substn_Osimps_I1_J_2,axiom, % 0.51/0.65 ( c_Lambda_Osubstn(c_Lambda_OdB_OVar(V_i),V_s,V_k) = c_Lambda_OdB_OVar(V_i) % 0.51/0.65 | V_i = V_k % 0.51/0.65 | c_HOL_Oord__class_Oless(V_k,V_i,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I3_J_0,axiom, % 0.51/0.65 ( c_Lambda_OdB_OAbs(V_dB) != c_Lambda_OdB_OAbs(V_dB_H) % 0.51/0.65 | V_dB = V_dB_H ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_beta_0,axiom, % 0.51/0.65 c_Lambda_Obeta(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.51/0.65 % 0.51/0.65 cnf(cls_beta__cases_I2_J_1,axiom, % 0.51/0.65 ( c_Lambda_Obeta(V_r,c_Lambda_Osko__Lambda__Xbeta__cases__2__1(V_r,V_s)) % 0.51/0.65 | ~ c_Lambda_Obeta(c_Lambda_OdB_OAbs(V_r),V_s) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_substn__subst__0_0,axiom, % 0.51/0.65 c_Lambda_Osubstn(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) = c_Lambda_Osubst(V_t,V_s,c_HOL_Ozero__class_Ozero(tc_nat)) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__lt_0,axiom, % 0.51/0.65 ( c_Lambda_Osubst(c_Lambda_OdB_OVar(V_j),V_u,V_i) = c_Lambda_OdB_OVar(V_j) % 0.51/0.65 | ~ c_HOL_Oord__class_Oless(V_j,V_i,tc_nat) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__App_0,axiom, % 0.51/0.65 c_Lambda_Osubst(c_Lambda_OdB_OApp(V_t,V_u),V_s,V_k) = c_Lambda_OdB_OApp(c_Lambda_Osubst(V_t,V_s,V_k),c_Lambda_Osubst(V_u,V_s,V_k)) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I7_J_0,axiom, % 0.51/0.65 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I8_J_0,axiom, % 0.51/0.65 c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I1_J_0,axiom, % 0.51/0.65 ( c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OVar(V_nat_H) % 0.51/0.65 | V_nat = V_nat_H ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I9_J_0,axiom, % 0.51/0.65 c_Lambda_OdB_OAbs(V_dB_H) != c_Lambda_OdB_OApp(V_dB1,V_dB2) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__eq_0,axiom, % 0.51/0.65 c_Lambda_Osubst(c_Lambda_OdB_OVar(V_k),V_u,V_k) = V_u ). % 0.51/0.65 % 0.51/0.65 cnf(cls_subst__Var__IT_0,axiom, % 0.51/0.65 ( c_InductTermi_OIT(c_Lambda_Osubst(V_r,c_Lambda_OdB_OVar(V_i),V_j)) % 0.51/0.65 | ~ c_InductTermi_OIT(V_r) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_beta__cases_I1_J_0,axiom, % 0.51/0.65 ~ c_Lambda_Obeta(c_Lambda_OdB_OVar(V_i),V_t) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I2_J_0,axiom, % 0.51/0.65 ( c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) % 0.51/0.65 | V_dB1 = V_dB1_H ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I2_J_1,axiom, % 0.51/0.65 ( c_Lambda_OdB_OApp(V_dB1,V_dB2) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) % 0.51/0.65 | V_dB2 = V_dB2_H ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I4_J_0,axiom, % 0.51/0.65 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_lift__IT_0,axiom, % 0.51/0.65 ( c_InductTermi_OIT(c_Lambda_Olift(V_t,V_i)) % 0.51/0.65 | ~ c_InductTermi_OIT(V_t) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I6_J_0,axiom, % 0.51/0.65 c_Lambda_OdB_OVar(V_nat) != c_Lambda_OdB_OAbs(V_dB_H) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Var__IT_0,axiom, % 0.51/0.65 c_InductTermi_OIT(c_Lambda_OdB_OVar(V_n)) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_lift_Osimps_I2_J_0,axiom, % 0.51/0.65 c_Lambda_Olift(c_Lambda_OdB_OApp(V_s,V_t),V_k) = c_Lambda_OdB_OApp(c_Lambda_Olift(V_s,V_k),c_Lambda_Olift(V_t,V_k)) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_Lambda_0,axiom, % 0.51/0.65 ( c_InductTermi_OIT(c_Lambda_OdB_OAbs(V_r)) % 0.51/0.65 | ~ c_InductTermi_OIT(V_r) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_appR_0,axiom, % 0.51/0.65 ( c_Lambda_Obeta(c_Lambda_OdB_OApp(V_u,V_s),c_Lambda_OdB_OApp(V_u,V_t)) % 0.51/0.65 | ~ c_Lambda_Obeta(V_s,V_t) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_appL_0,axiom, % 0.51/0.65 ( c_Lambda_Obeta(c_Lambda_OdB_OApp(V_s,V_u),c_Lambda_OdB_OApp(V_t,V_u)) % 0.51/0.65 | ~ c_Lambda_Obeta(V_s,V_t) ) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_liftn_Osimps_I2_J_0,axiom, % 0.51/0.65 c_Lambda_Oliftn(V_n,c_Lambda_OdB_OApp(V_s,V_t),V_k) = c_Lambda_OdB_OApp(c_Lambda_Oliftn(V_n,V_s,V_k),c_Lambda_Oliftn(V_n,V_t,V_k)) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_substn_Osimps_I2_J_0,axiom, % 0.51/0.65 c_Lambda_Osubstn(c_Lambda_OdB_OApp(V_t,V_u),V_s,V_k) = c_Lambda_OdB_OApp(c_Lambda_Osubstn(V_t,V_s,V_k),c_Lambda_Osubstn(V_u,V_s,V_k)) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_dB_Osimps_I5_J_0,axiom, % 0.51/0.65 c_Lambda_OdB_OApp(V_dB1_H,V_dB2_H) != c_Lambda_OdB_OVar(V_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_conjecture_0,negated_conjecture, % 0.51/0.65 c_InductTermi_OIT(v_r) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_conjecture_1,negated_conjecture, % 0.51/0.65 c_InductTermi_OIT(c_Lambda_OdB_OApp(v_r,c_Lambda_OdB_OVar(v_i))) ). % 0.51/0.65 % 0.51/0.65 cnf(cls_conjecture_2,negated_conjecture, % 0.51/0.65 ~ c_InductTermi_OIT(c_Lambda_OdB_OVar(v_i)) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.51/0.65 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.51/0.65 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Oordered__comm__semiring__strict,axiom, % 0.51/0.65 class_Ring__and__Field_Oordered__comm__semiring__strict(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Oordered__semiring__strict,axiom, % 0.51/0.65 class_Ring__and__Field_Oordered__semiring__strict(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Opordered__comm__monoid__add,axiom, % 0.51/0.65 class_OrderedGroup_Opordered__comm__monoid__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.51/0.65 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.51/0.65 class_OrderedGroup_Ocancel__semigroup__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Ono__zero__divisors,axiom, % 0.51/0.65 class_Ring__and__Field_Ono__zero__divisors(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Oordered__semidom,axiom, % 0.51/0.65 class_Ring__and__Field_Oordered__semidom(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.51/0.65 class_Ring__and__Field_Ocomm__semiring__1(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__mult,axiom, % 0.51/0.65 class_OrderedGroup_Oab__semigroup__mult(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Oab__semigroup__add,axiom, % 0.51/0.65 class_OrderedGroup_Oab__semigroup__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Ocomm__semiring,axiom, % 0.51/0.65 class_Ring__and__Field_Ocomm__semiring(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Ocomm__monoid__add,axiom, % 0.51/0.65 class_OrderedGroup_Ocomm__monoid__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Osemiring__1,axiom, % 0.51/0.65 class_Ring__and__Field_Osemiring__1(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Omult__zero,axiom, % 0.51/0.65 class_Ring__and__Field_Omult__zero(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Ring__and__Field_Osemiring,axiom, % 0.51/0.65 class_Ring__and__Field_Osemiring(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__OrderedGroup_Omonoid__add,axiom, % 0.51/0.65 class_OrderedGroup_Omonoid__add(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Nat_Osemiring__char__0,axiom, % 0.51/0.65 class_Nat_Osemiring__char__0(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Orderings_Opreorder,axiom, % 0.51/0.65 class_Orderings_Opreorder(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Orderings_Olinorder,axiom, % 0.51/0.65 class_Orderings_Olinorder(tc_nat) ). % 0.51/0.65 % 0.51/0.65 cnf(clsarity_nat__Orderings_Oorder,axiom, % 0.51/0.65 class_Orderings_Oorder(tc_nat) ). % 0.51/0.65 % 0.51/0.65 %------------------------------------------------------------------------------ % 0.51/0.65 %------------------------------------------- % 0.51/0.65 % Proof found % 0.51/0.65 % SZS status Theorem for theBenchmark % 0.51/0.65 % SZS output start Proof % 0.51/0.65 %ClaNum:455(EqnAxiom:74) % 0.51/0.65 %VarNum:2092(SingletonVarNum:800) % 0.51/0.65 %MaxLitNum:5 % 0.51/0.65 %MaxfuncDepth:4 % 0.51/0.65 %SharedTerms:42 % 0.51/0.65 %goalClause: 97 99 167 % 0.51/0.65 %singleGoalClaCount:3 % 0.51/0.65 [75]P1(a1) % 0.51/0.65 [76]P2(a1) % 0.51/0.65 [77]P3(a1) % 0.51/0.65 [78]P25(a1) % 0.51/0.65 [79]P8(a1) % 0.51/0.65 [80]P28(a1) % 0.51/0.65 [81]P37(a1) % 0.51/0.65 [82]P14(a1) % 0.51/0.65 [83]P10(a1) % 0.51/0.65 [84]P13(a1) % 0.51/0.65 [85]P29(a1) % 0.51/0.65 [86]P33(a1) % 0.51/0.65 [87]P30(a1) % 0.51/0.65 [88]P15(a1) % 0.51/0.65 [89]P26(a1) % 0.51/0.65 [90]P18(a1) % 0.51/0.65 [91]P19(a1) % 0.51/0.65 [92]P11(a1) % 0.51/0.65 [93]P21(a1) % 0.51/0.65 [94]P22(a1) % 0.51/0.65 [95]P23(a1) % 0.51/0.65 [96]P24(a1) % 0.51/0.65 [97]P4(a18) % 0.51/0.65 [167]~P4(f2(a19)) % 0.51/0.65 [99]P4(f3(a18,f2(a19))) % 0.51/0.65 [121]E(f10(f14(f8(a1)),f14(f8(a1)),a1),f14(f8(a1))) % 0.51/0.65 [176]~P5(x1761,x1761,a1) % 0.51/0.65 [98]P4(f2(x981)) % 0.51/0.65 [100]E(f4(x1001,x1001,a1),f8(a1)) % 0.51/0.65 [110]P5(x1101,f14(x1101),a1) % 0.51/0.65 [114]P5(f8(a1),f14(x1141),a1) % 0.51/0.65 [162]~E(f14(x1621),x1621) % 0.51/0.65 [166]~E(f14(x1661),f8(a1)) % 0.51/0.65 [178]~P5(x1781,f8(a1),a1) % 0.51/0.65 [102]E(f9(x1021,f8(a1),a1),x1021) % 0.51/0.65 [103]E(f4(x1031,f8(a1),a1),x1031) % 0.51/0.65 [104]E(f9(f8(a1),x1041,a1),x1041) % 0.51/0.65 [106]E(f10(x1061,f8(a1),a1),f8(a1)) % 0.51/0.65 [107]E(f10(f8(a1),x1071,a1),f8(a1)) % 0.51/0.65 [108]E(f4(f8(a1),x1081,a1),f8(a1)) % 0.51/0.65 [122]E(f10(x1221,x1222,a1),f10(x1222,x1221,a1)) % 0.51/0.65 [123]E(f9(x1231,x1232,a1),f9(x1232,x1231,a1)) % 0.51/0.65 [132]P5(f4(x1321,x1322,a1),f14(x1321),a1) % 0.51/0.65 [169]~E(f11(x1691),f2(x1692)) % 0.51/0.65 [174]~P6(f2(x1741),x1742) % 0.51/0.65 [180]~P5(f9(x1801,x1802,a1),x1802,a1) % 0.51/0.65 [181]~P5(f9(x1811,x1812,a1),x1811,a1) % 0.51/0.65 [105]E(f12(f8(a1),x1051,x1052),x1051) % 0.51/0.65 [111]E(f15(f2(x1111),x1112,x1111),x1112) % 0.51/0.65 [125]E(f10(x1251,f8(a1),a1),f10(x1252,f8(a1),a1)) % 0.51/0.65 [126]E(f10(f8(a1),x1261,a1),f10(f8(a1),x1262,a1)) % 0.51/0.65 [127]E(f9(f14(x1271),x1272,a1),f9(x1271,f14(x1272),a1)) % 0.51/0.65 [128]E(f4(f14(x1281),f14(x1282),a1),f4(x1281,x1282,a1)) % 0.51/0.65 [129]E(f4(f9(x1291,x1292,a1),x1292,a1),x1291) % 0.51/0.65 [130]E(f4(f9(x1301,x1302,a1),x1301,a1),x1302) % 0.51/0.65 [131]E(f4(x1311,f9(x1311,x1312,a1),a1),f8(a1)) % 0.51/0.65 [133]P6(f3(f11(x1331),x1332),f15(x1331,x1332,f8(a1))) % 0.51/0.65 [134]E(f14(f9(x1341,x1342,a1)),f9(x1341,f14(x1342),a1)) % 0.51/0.65 [135]E(f14(f9(x1351,x1352,a1)),f9(f14(x1351),x1352,a1)) % 0.51/0.65 [137]E(f9(x1371,f10(x1371,x1372,a1),a1),f10(x1371,f14(x1372),a1)) % 0.51/0.65 [138]E(f9(x1381,f10(x1382,x1381,a1),a1),f10(f14(x1382),x1381,a1)) % 0.51/0.65 [139]E(f15(x1391,f12(f8(a1),x1392,f8(a1)),f8(a1)),f15(x1391,x1392,f8(a1))) % 0.51/0.65 [140]P5(x1401,f14(f9(x1402,x1401,a1)),a1) % 0.51/0.65 [142]P5(x1421,f14(f9(x1421,x1422,a1)),a1) % 0.51/0.65 [170]~E(f2(x1701),f3(x1702,x1703)) % 0.51/0.65 [171]~E(f11(x1711),f3(x1712,x1713)) % 0.51/0.65 [172]~E(f3(x1721,x1722),f2(x1723)) % 0.51/0.65 [173]~E(f3(x1731,x1732),f11(x1733)) % 0.51/0.65 [120]E(f15(f13(x1201,x1202),x1203,x1202),x1201) % 0.51/0.65 [124]E(f3(f13(x1241,x1242),f13(x1243,x1242)),f13(f3(x1241,x1243),x1242)) % 0.51/0.65 [136]E(f13(f12(x1361,x1362,x1363),x1363),f12(f14(x1361),x1362,x1363)) % 0.51/0.65 [145]E(f9(x1451,f9(x1452,x1453,a1),a1),f9(x1452,f9(x1451,x1453,a1),a1)) % 0.51/0.65 [146]E(f10(f10(x1461,x1462,a1),x1463,a1),f10(x1461,f10(x1462,x1463,a1),a1)) % 0.51/0.65 [147]E(f9(f9(x1471,x1472,a1),x1473,a1),f9(x1471,f9(x1472,x1473,a1),a1)) % 0.51/0.65 [148]E(f4(f4(x1481,x1482,a1),x1483,a1),f4(x1481,f9(x1482,x1483,a1),a1)) % 0.51/0.65 [149]E(f4(f4(x1491,x1492,a1),x1493,a1),f4(f4(x1491,x1493,a1),x1492,a1)) % 0.51/0.65 [150]E(f4(f9(x1501,x1502,a1),f9(x1503,x1502,a1),a1),f4(x1501,x1503,a1)) % 0.51/0.65 [151]E(f4(f9(x1511,x1512,a1),f9(x1511,x1513,a1),a1),f4(x1512,x1513,a1)) % 0.51/0.65 [152]E(f4(f4(f14(x1521),x1522,a1),f14(x1523),a1),f4(f4(x1521,x1522,a1),x1523,a1)) % 0.51/0.65 [153]E(f9(f10(x1531,x1532,a1),f10(x1531,x1533,a1),a1),f10(x1531,f9(x1532,x1533,a1),a1)) % 0.51/0.65 [154]E(f4(f10(x1541,x1542,a1),f10(x1541,x1543,a1),a1),f10(x1541,f4(x1542,x1543,a1),a1)) % 0.51/0.65 [155]E(f9(f10(x1551,x1552,a1),f10(x1553,x1552,a1),a1),f10(f9(x1551,x1553,a1),x1552,a1)) % 0.51/0.65 [156]E(f4(f10(x1561,x1562,a1),f10(x1563,x1562,a1),a1),f10(f4(x1561,x1563,a1),x1562,a1)) % 0.51/0.65 [143]E(f3(f12(x1431,x1432,x1433),f12(x1431,x1434,x1433)),f12(x1431,f3(x1432,x1434),x1433)) % 0.51/0.65 [144]E(f3(f15(x1441,x1442,x1443),f15(x1444,x1442,x1443)),f15(f3(x1441,x1444),x1442,x1443)) % 0.51/0.65 [159]E(f9(f10(x1591,x1592,a1),f9(f10(x1593,x1592,a1),x1594,a1),a1),f9(f10(f9(x1591,x1593,a1),x1592,a1),x1594,a1)) % 0.51/0.65 [186]~P4(x1861)+P4(f11(x1861)) % 0.51/0.65 [193]E(x1931,f8(a1))+P5(f8(a1),x1931,a1) % 0.51/0.65 [187]~P37(x1871)+E(f17(f8(a1),x1871),f8(x1871)) % 0.51/0.65 [217]~P17(x2171)+E(f9(f8(x2171),f8(x2171),x2171),f8(x2171)) % 0.51/0.65 [229]~P5(f8(a1),x2291,a1)+E(f14(f5(x2291)),x2291) % 0.51/0.65 [230]~P5(f8(a1),x2301,a1)+E(f14(f6(x2301)),x2301) % 0.51/0.65 [238]E(x2381,f8(a1))+~P5(x2381,f14(f8(a1)),a1) % 0.51/0.65 [342]~P32(x3421)+E(f9(f10(f8(x3421),f8(x3421),x3421),f10(f8(x3421),f8(x3421),x3421),x3421),f8(x3421)) % 0.51/0.65 [451]~P32(x4511)+~P5(f8(x4511),f9(f10(f8(x4511),f8(x4511),x4511),f10(f8(x4511),f8(x4511),x4511),x4511),x4511) % 0.51/0.65 [308]~P5(f8(a1),x3081,a1)+E(f14(f4(x3081,f14(f8(a1)),a1)),x3081) % 0.51/0.65 [225]~P5(x2252,x2252,x2251)+~P22(x2251) % 0.51/0.65 [226]~P5(x2262,x2262,x2261)+~P23(x2261) % 0.51/0.65 [227]~P5(x2272,x2272,x2271)+~P24(x2271) % 0.51/0.65 [183]E(x1831,x1832)+~E(f14(x1831),f14(x1832)) % 0.51/0.65 [184]E(x1841,x1842)+~E(f2(x1841),f2(x1842)) % 0.51/0.65 [185]E(x1851,x1852)+~E(f11(x1851),f11(x1852)) % 0.51/0.65 [188]~P4(x1881)+P4(f13(x1881,x1882)) % 0.51/0.65 [191]~P6(x1911,x1912)+P6(f11(x1911),f11(x1912)) % 0.51/0.65 [194]~P12(x1942)+E(f10(x1941,x1941,x1942),x1941) % 0.51/0.65 [197]~P16(x1972)+E(f4(x1971,x1971,x1972),f8(x1972)) % 0.51/0.65 [198]~P9(x1982)+E(f4(x1981,x1981,x1982),f8(x1982)) % 0.51/0.65 [214]~P6(f11(x2141),x2142)+P6(x2141,f16(x2141,x2142)) % 0.51/0.65 [219]~E(f9(x2192,x2191,a1),x2192)+E(x2191,f8(a1)) % 0.51/0.65 [223]E(x2231,f8(a1))+~E(f9(x2232,x2231,a1),f8(a1)) % 0.51/0.65 [224]E(x2241,f8(a1))+~E(f9(x2241,x2242,a1),f8(a1)) % 0.51/0.65 [253]P5(x2531,x2532,a1)+P5(x2532,f14(x2531),a1) % 0.51/0.65 [269]~P5(x2691,x2692,a1)+P5(x2691,f14(x2692),a1) % 0.51/0.65 [270]~P29(x2701)+~P5(f17(x2702,x2701),f8(x2701),x2701) % 0.51/0.65 [271]P5(x2711,x2712,a1)+~P5(f14(x2711),x2712,a1) % 0.51/0.65 [279]~P5(x2791,x2792,a1)+P5(f14(x2791),f14(x2792),a1) % 0.51/0.65 [280]P5(x2801,x2802,a1)+~P5(f14(x2801),f14(x2802),a1) % 0.51/0.65 [291]~P5(x2911,x2912,a1)+~P5(x2912,f14(x2911),a1) % 0.51/0.65 [322]~P5(x3222,x3221,a1)+P5(f8(a1),f4(x3221,x3222,a1),a1) % 0.51/0.65 [332]~P32(x3321)+~P5(f10(x3322,x3322,x3321),f8(x3321),x3321) % 0.51/0.65 [336]P5(x3361,x3362,a1)+~P5(f8(a1),f4(x3362,x3361,a1),a1) % 0.51/0.65 [337]P5(f8(a1),x3371,a1)+~P5(f8(a1),f10(x3372,x3371,a1),a1) % 0.51/0.65 [338]P5(f8(a1),x3381,a1)+~P5(f8(a1),f10(x3381,x3382,a1),a1) % 0.51/0.65 [195]~P6(f11(x1951),x1952)+E(f11(f16(x1951,x1952)),x1952) % 0.51/0.65 [199]~P1(x1992)+E(f9(x1991,f8(x1992),x1992),x1991) % 0.51/0.65 [200]~P2(x2002)+E(f9(x2001,f8(x2002),x2002),x2001) % 0.51/0.65 [201]~P15(x2012)+E(f9(x2011,f8(x2012),x2012),x2011) % 0.51/0.65 [202]~P16(x2022)+E(f4(x2021,f8(x2022),x2022),x2021) % 0.51/0.65 [204]~P1(x2041)+E(f9(f8(x2041),x2042,x2041),x2042) % 0.51/0.65 [205]~P2(x2051)+E(f9(f8(x2051),x2052,x2051),x2052) % 0.51/0.65 [206]~P15(x2061)+E(f9(f8(x2061),x2062,x2061),x2062) % 0.51/0.65 [207]~P1(x2072)+E(f10(x2071,f8(x2072),x2072),f8(x2072)) % 0.51/0.65 [208]~P34(x2082)+E(f10(x2081,f8(x2082),x2082),f8(x2082)) % 0.51/0.65 [209]~P26(x2092)+E(f10(x2091,f8(x2092),x2092),f8(x2092)) % 0.51/0.65 [211]~P1(x2111)+E(f10(f8(x2111),x2112,x2111),f8(x2111)) % 0.51/0.65 [212]~P34(x2121)+E(f10(f8(x2121),x2122,x2121),f8(x2121)) % 0.51/0.65 [213]~P26(x2131)+E(f10(f8(x2131),x2132,x2131),f8(x2131)) % 0.51/0.65 [235]E(x2351,f14(f8(a1)))+~E(f10(x2352,x2351,a1),f14(f8(a1))) % 0.51/0.65 [236]E(x2361,f14(f8(a1)))+~E(f10(x2361,x2362,a1),f14(f8(a1))) % 0.51/0.65 [244]~P5(x2441,x2442,a1)+E(f13(f2(x2441),x2442),f2(x2441)) % 0.51/0.65 [306]P5(x3062,x3061,a1)+E(f9(x3061,f4(x3062,x3061,a1),a1),x3062) % 0.51/0.65 [327]~P5(f8(a1),x3271,a1)+P5(f4(x3271,f14(x3272),a1),x3271,a1) % 0.51/0.65 [220]~P6(x2201,x2203)+P6(f13(x2201,x2202),f13(x2203,x2202)) % 0.51/0.65 [221]~P6(x2211,x2213)+P6(f3(x2211,x2212),f3(x2213,x2212)) % 0.51/0.65 [222]~P6(x2222,x2223)+P6(f3(x2221,x2222),f3(x2221,x2223)) % 0.51/0.65 [257]~P1(x2573)+E(f10(x2571,x2572,x2573),f10(x2572,x2571,x2573)) % 0.51/0.65 [259]~P1(x2593)+E(f9(x2591,x2592,x2593),f9(x2592,x2591,x2593)) % 0.51/0.65 [260]~P2(x2603)+E(f9(x2601,x2602,x2603),f9(x2602,x2601,x2603)) % 0.51/0.65 [282]E(x2821,x2822)+~E(f9(x2823,x2821,a1),f9(x2823,x2822,a1)) % 0.51/0.65 [283]E(x2831,x2832)+~E(f9(x2831,x2833,a1),f9(x2832,x2833,a1)) % 0.51/0.65 [318]~P5(x3181,x3183,a1)+P5(x3181,f9(x3182,x3183,a1),a1) % 0.51/0.65 [320]~P5(x3201,x3202,a1)+P5(x3201,f9(x3202,x3203,a1),a1) % 0.51/0.65 [321]~P5(x3211,x3213,a1)+P5(f4(x3211,x3212,a1),x3213,a1) % 0.51/0.65 [334]P5(x3341,x3342,a1)+~P5(f9(x3341,x3343,a1),x3342,a1) % 0.51/0.65 [363]~P5(x3631,x3633,a1)+P5(f9(x3631,x3632,a1),f9(x3633,x3632,a1),a1) % 0.51/0.65 [364]~P5(x3642,x3643,a1)+P5(f9(x3641,x3642,a1),f9(x3641,x3643,a1),a1) % 0.51/0.65 [383]~P5(f9(x3831,x3833,a1),x3832,a1)+P5(x3831,f4(x3832,x3833,a1),a1) % 0.51/0.65 [384]~P5(x3841,f4(x3843,x3842,a1),a1)+P5(f9(x3841,x3842,a1),x3843,a1) % 0.51/0.65 [412]P5(x4121,x4122,a1)+~P5(f10(x4123,x4121,a1),f10(x4123,x4122,a1),a1) % 0.51/0.65 [413]P5(x4131,x4132,a1)+~P5(f10(x4131,x4133,a1),f10(x4132,x4133,a1),a1) % 0.51/0.66 [414]P5(x4141,x4142,a1)+~P5(f9(x4143,x4141,a1),f9(x4143,x4142,a1),a1) % 0.51/0.66 [415]~P5(f10(x4152,x4151,a1),f10(x4153,x4151,a1),a1)+P5(f8(a1),x4151,a1) % 0.51/0.66 [416]~P5(f10(x4161,x4162,a1),f10(x4161,x4163,a1),a1)+P5(f8(a1),x4161,a1) % 0.51/0.66 [268]~P4(x2681)+P4(f15(x2681,f2(x2682),x2683)) % 0.51/0.66 [272]~P5(x2722,x2723,a1)+E(f12(x2721,f2(x2722),x2723),f2(x2722)) % 0.51/0.66 [273]~P5(x2731,x2733,a1)+E(f15(f2(x2731),x2732,x2733),f2(x2731)) % 0.51/0.66 [284]~P16(x2843)+E(f9(f4(x2841,x2842,x2843),x2842,x2843),x2841) % 0.51/0.66 [285]~P16(x2853)+E(f4(f9(x2851,x2852,x2853),x2852,x2853),x2851) % 0.51/0.66 [302]E(x3021,x3022)+~E(f10(f14(x3023),x3021,a1),f10(f14(x3023),x3022,a1)) % 0.51/0.66 [307]P5(x3072,x3073,a1)+E(f12(x3071,f2(x3072),x3073),f2(f9(x3072,x3071,a1))) % 0.51/0.66 [309]~P12(x3093)+E(f10(x3091,f10(x3091,x3092,x3093),x3093),f10(x3091,x3092,x3093)) % 0.51/0.66 [312]~P37(x3122)+E(f10(f17(x3121,x3122),f17(x3123,x3122),x3122),f17(f10(x3121,x3123,a1),x3122)) % 0.51/0.66 [313]~P37(x3132)+E(f9(f17(x3131,x3132),f17(x3133,x3132),x3132),f17(f9(x3131,x3133,a1),x3132)) % 0.51/0.66 [380]~P5(x3802,x3803,a1)+P5(f10(f14(x3801),x3802,a1),f10(f14(x3801),x3803,a1),a1) % 0.51/0.66 [448]~P32(x4481)+~P5(f9(f10(x4482,x4482,x4481),f10(x4483,x4483,x4481),x4481),f8(x4481),x4481) % 0.51/0.66 [189]E(x1891,x1892)+~E(f3(x1893,x1891),f3(x1894,x1892)) % 0.51/0.66 [190]E(x1901,x1902)+~E(f3(x1901,x1903),f3(x1902,x1904)) % 0.51/0.66 [325]~P6(x3251,x3254)+P6(f15(x3251,x3252,x3253),f15(x3254,x3252,x3253)) % 0.51/0.66 [343]~P1(x3434)+E(f10(x3431,f10(x3432,x3433,x3434),x3434),f10(x3432,f10(x3431,x3433,x3434),x3434)) % 0.51/0.66 [344]~P1(x3444)+E(f9(x3441,f9(x3442,x3443,x3444),x3444),f9(x3442,f9(x3441,x3443,x3444),x3444)) % 0.51/0.66 [345]~P2(x3454)+E(f9(x3451,f9(x3452,x3453,x3454),x3454),f9(x3452,f9(x3451,x3453,x3454),x3454)) % 0.51/0.66 [346]~P9(x3464)+E(f9(x3461,f9(x3462,x3463,x3464),x3464),f9(x3462,f9(x3461,x3463,x3464),x3464)) % 0.51/0.66 [351]~P1(x3513)+E(f10(f10(x3511,x3512,x3513),x3514,x3513),f10(x3511,f10(x3512,x3514,x3513),x3513)) % 0.51/0.66 [352]~P11(x3523)+E(f10(f10(x3521,x3522,x3523),x3524,x3523),f10(x3521,f10(x3522,x3524,x3523),x3523)) % 0.51/0.66 [353]~P1(x3533)+E(f9(f9(x3531,x3532,x3533),x3534,x3533),f9(x3531,f9(x3532,x3534,x3533),x3533)) % 0.51/0.66 [354]~P2(x3543)+E(f9(f9(x3541,x3542,x3543),x3544,x3543),f9(x3541,f9(x3542,x3544,x3543),x3543)) % 0.51/0.66 [355]~P8(x3553)+E(f9(f9(x3551,x3552,x3553),x3554,x3553),f9(x3551,f9(x3552,x3554,x3553),x3553)) % 0.51/0.66 [356]~P1(x3563)+E(f10(f10(x3561,x3562,x3563),x3564,x3563),f10(f10(x3561,x3564,x3563),x3562,x3563)) % 0.51/0.66 [357]~P1(x3573)+E(f9(f9(x3571,x3572,x3573),x3574,x3573),f9(f9(x3571,x3574,x3573),x3572,x3573)) % 0.51/0.66 [394]~P1(x3943)+E(f9(f10(x3941,x3942,x3943),f10(x3941,x3944,x3943),x3943),f10(x3941,f9(x3942,x3944,x3943),x3943)) % 0.51/0.66 [396]~P21(x3963)+E(f9(f10(x3961,x3962,x3963),f10(x3964,x3962,x3963),x3963),f10(f9(x3961,x3964,x3963),x3962,x3963)) % 0.51/0.66 [397]~P1(x3973)+E(f9(f10(x3971,x3972,x3973),f10(x3974,x3972,x3973),x3973),f10(f9(x3971,x3974,x3973),x3972,x3973)) % 0.51/0.66 [424]~P1(x4243)+E(f10(f10(x4241,x4242,x4243),f10(x4244,x4245,x4243),x4243),f10(f10(x4241,x4244,x4243),f10(x4242,x4245,x4243),x4243)) % 0.51/0.66 [425]~P1(x4253)+E(f9(f9(x4251,x4252,x4253),f9(x4254,x4255,x4253),x4253),f9(f9(x4251,x4254,x4253),f9(x4252,x4255,x4253),x4253)) % 0.51/0.66 [445]~P28(x4453)+E(f9(f10(x4451,x4452,x4453),f9(f10(x4454,x4452,x4453),x4455,x4453),x4453),f9(f10(f9(x4451,x4454,x4453),x4452,x4453),x4455,x4453)) % 0.51/0.66 [450]~P35(x4503)+E(f9(f10(x4501,x4502,x4503),f9(f10(f4(x4504,x4501,x4503),x4502,x4503),x4505,x4503),x4503),f9(f10(x4504,x4502,x4503),x4505,x4503)) % 0.51/0.66 [247]E(x2471,x2472)+P5(x2472,x2471,a1)+P5(x2471,x2472,a1) % 0.51/0.66 [215]~P27(x2152)+~P7(x2152)+E(f4(x2151,x2151,x2152),f8(x2152)) % 0.51/0.66 [228]E(x2281,f8(a1))+E(x2282,f8(a1))+~E(f10(x2282,x2281,a1),f8(a1)) % 0.51/0.66 [237]~P17(x2372)+~E(f9(x2371,x2371,x2372),f8(x2372))+E(x2371,f8(x2372)) % 0.51/0.66 [274]~P5(x2741,x2742,a1)+E(f14(x2741),x2742)+P5(f14(x2741),x2742,a1) % 0.51/0.66 [275]E(x2751,x2752)+P5(x2752,x2751,a1)+~P5(x2752,f14(x2751),a1) % 0.51/0.66 [277]E(x2771,x2772)+P5(x2771,x2772,a1)+~P5(x2771,f14(x2772),a1) % 0.51/0.66 [289]~P5(x2891,f14(x2892),a1)+P5(f7(x2891,x2892),x2892,a1)+E(x2891,f8(a1)) % 0.51/0.66 [290]E(x2901,x2902)+~E(f4(x2902,x2901,a1),f8(a1))+~E(f4(x2901,x2902,a1),f8(a1)) % 0.51/0.66 [301]~P29(x3011)+P5(f8(x3011),f17(x3012,x3011),x3011)+~P5(f8(a1),x3012,a1) % 0.51/0.66 [305]~P29(x3052)+~P5(f8(x3052),f17(x3051,x3052),x3052)+P5(f8(a1),x3051,a1) % 0.51/0.66 [329]~P17(x3291)+~P5(f8(x3291),x3292,x3291)+P5(f8(x3291),f9(x3292,x3292,x3291),x3291) % 0.51/0.66 [330]~P17(x3302)+~P5(x3301,f8(x3302),x3302)+P5(f9(x3301,x3301,x3302),f8(x3302),x3302) % 0.51/0.66 [331]~P31(x3312)+~P5(x3311,f8(x3312),x3312)+P5(f9(x3311,x3311,x3312),f8(x3312),x3312) % 0.51/0.66 [358]~P17(x3582)+~P5(f9(x3581,x3581,x3582),f8(x3582),x3582)+P5(x3581,f8(x3582),x3582) % 0.51/0.66 [359]~P31(x3592)+~P5(f9(x3591,x3591,x3592),f8(x3592),x3592)+P5(x3591,f8(x3592),x3592) % 0.51/0.66 [360]~P17(x3601)+~P5(f8(x3601),f9(x3602,x3602,x3601),x3601)+P5(f8(x3601),x3602,x3601) % 0.51/0.66 [361]P5(f4(x3611,x3612,a1),x3611,a1)+~P5(f8(a1),x3612,a1)+~P5(f8(a1),x3611,a1) % 0.51/0.66 [362]~P5(f8(a1),x3622,a1)+~P5(f8(a1),x3621,a1)+P5(f8(a1),f10(x3621,x3622,a1),a1) % 0.51/0.66 [372]P5(f8(a1),x3721,a1)+P5(f8(a1),x3722,a1)+~P5(f8(a1),f9(x3721,x3722,a1),a1) % 0.51/0.66 [216]~P27(x2162)+~P7(x2162)+E(f9(x2161,f8(x2162),x2162),x2161) % 0.51/0.66 [234]E(x2341,f8(a1))+E(x2342,f8(a1))+~E(f9(x2342,x2341,a1),f14(f8(a1))) % 0.51/0.66 [241]E(x2411,f8(a1))+E(x2411,f14(f8(a1)))+~E(f9(x2412,x2411,a1),f14(f8(a1))) % 0.51/0.66 [242]E(x2421,f8(a1))+E(x2421,f14(f8(a1)))+~E(f9(x2421,x2422,a1),f14(f8(a1))) % 0.51/0.66 [252]E(x2521,f14(f8(a1)))+E(x2522,f14(f8(a1)))+~E(f9(x2522,x2521,a1),f14(f8(a1))) % 0.51/0.66 [267]~P5(x2671,f14(x2672),a1)+E(x2671,f8(a1))+E(f14(f7(x2671,x2672)),x2671) % 0.51/0.66 [370]P5(x3701,f10(x3702,x3701,a1),a1)+~P5(f14(f8(a1)),x3702,a1)+~P5(f14(f8(a1)),x3701,a1) % 0.51/0.66 [371]P5(x3711,f10(x3711,x3712,a1),a1)+~P5(f14(f8(a1)),x3712,a1)+~P5(f14(f8(a1)),x3711,a1) % 0.51/0.66 [381]~P5(f14(f8(a1)),x3812,a1)+~P5(f14(f8(a1)),x3811,a1)+P5(f14(f8(a1)),f10(x3811,x3812,a1),a1) % 0.51/0.66 [293]~P5(x2933,x2932,x2931)+~P22(x2931)+~P5(x2932,x2933,x2931) % 0.51/0.66 [294]~P5(x2943,x2942,x2941)+~P23(x2941)+~P5(x2942,x2943,x2941) % 0.51/0.66 [295]~P5(x2953,x2952,x2951)+~P24(x2951)+~P5(x2952,x2953,x2951) % 0.51/0.66 [192]~P3(x1923)+E(x1921,x1922)+~E(f17(x1921,x1923),f17(x1922,x1923)) % 0.51/0.66 [231]~P16(x2313)+E(x2311,x2312)+~E(f4(x2311,x2312,x2313),f8(x2313)) % 0.51/0.66 [232]~P9(x2323)+E(x2321,x2322)+~E(f4(x2321,x2322,x2323),f8(x2323)) % 0.51/0.66 [287]E(x2871,x2872)+~E(f10(x2873,x2871,a1),f10(x2873,x2872,a1))+E(x2873,f8(a1)) % 0.51/0.66 [288]E(x2881,x2882)+~E(f10(x2881,x2883,a1),f10(x2882,x2883,a1))+E(x2883,f8(a1)) % 0.51/0.66 [304]~P29(x3042)+~P5(x3041,x3043,a1)+P5(f17(x3041,x3042),f17(x3043,x3042),x3042) % 0.51/0.66 [310]~P5(x3101,x3103,a1)+~P5(x3103,x3102,a1)+P5(f14(x3101),x3102,a1) % 0.51/0.66 [311]~P29(x3113)+~P5(f17(x3111,x3113),f17(x3112,x3113),x3113)+P5(x3111,x3112,a1) % 0.51/0.66 [326]E(x3261,x3262)+~E(f10(x3263,x3261,a1),f10(x3263,x3262,a1))+~P5(f8(a1),x3263,a1) % 0.51/0.66 [328]~P20(x3283)+~P5(x3281,x3282,x3283)+P5(f4(x3281,x3282,x3283),f8(x3283),x3283) % 0.51/0.66 [341]~P20(x3413)+P5(x3411,x3412,x3413)+~P5(f4(x3411,x3412,x3413),f8(x3413),x3413) % 0.51/0.66 [388]~P5(x3883,x3882,a1)+~P5(x3883,x3881,a1)+P5(f4(x3881,x3882,a1),f4(x3881,x3883,a1),a1) % 0.51/0.66 [390]~P5(x3901,x3903,a1)+P5(f10(x3901,x3902,a1),f10(x3903,x3902,a1),a1)+~P5(f8(a1),x3902,a1) % 0.51/0.66 [393]~P5(x3932,x3933,a1)+P5(f10(x3931,x3932,a1),f10(x3931,x3933,a1),a1)+~P5(f8(a1),x3931,a1) % 0.51/0.66 [266]E(x2661,x2662)+P5(x2662,x2661,a1)+E(f15(f2(x2661),x2663,x2662),f2(x2661)) % 0.51/0.66 [398]~P32(x3982)+E(x3981,f8(x3982))+~E(f9(f10(x3983,x3983,x3982),f10(x3981,x3981,x3982),x3982),f8(x3982)) % 0.51/0.66 [399]~P32(x3992)+E(x3991,f8(x3992))+~E(f9(f10(x3991,x3991,x3992),f10(x3993,x3993,x3992),x3992),f8(x3992)) % 0.51/0.66 [437]~P32(x4372)+E(x4371,f8(x4372))+P5(f8(x4372),f9(f10(x4373,x4373,x4372),f10(x4371,x4371,x4372),x4372),x4372) % 0.51/0.66 [438]~P32(x4382)+E(x4381,f8(x4382))+P5(f8(x4382),f9(f10(x4381,x4381,x4382),f10(x4383,x4383,x4382),x4382),x4382) % 0.51/0.66 [296]~P10(x2964)+E(x2961,x2962)+~E(f9(x2963,x2961,x2964),f9(x2963,x2962,x2964)) % 0.51/0.66 [297]~P13(x2974)+E(x2971,x2972)+~E(f9(x2973,x2971,x2974),f9(x2973,x2972,x2974)) % 0.51/0.66 [298]~P9(x2984)+E(x2981,x2982)+~E(f4(x2983,x2983,x2984),f4(x2981,x2982,x2984)) % 0.51/0.66 [299]~P13(x2994)+E(x2991,x2992)+~E(f9(x2991,x2993,x2994),f9(x2992,x2993,x2994)) % 0.51/0.66 [300]~P9(x3003)+E(x3001,x3002)+~E(f4(x3001,x3002,x3003),f4(x3004,x3004,x3003)) % 0.51/0.66 [335]~P5(x3354,x3353,a1)+P5(x3351,x3352,a1)+~E(f9(x3351,x3353,a1),f9(x3354,x3352,a1)) % 0.51/0.66 [366]~P18(x3663)+~P5(x3661,x3664,x3663)+P5(f9(x3661,x3662,x3663),f9(x3664,x3662,x3663),x3663) % 0.51/0.66 [367]~P19(x3673)+~P5(x3671,x3674,x3673)+P5(f9(x3671,x3672,x3673),f9(x3674,x3672,x3673),x3673) % 0.51/0.66 [368]~P18(x3683)+~P5(x3682,x3684,x3683)+P5(f9(x3681,x3682,x3683),f9(x3681,x3684,x3683),x3683) % 0.51/0.66 [369]~P19(x3693)+~P5(x3692,x3694,x3693)+P5(f9(x3691,x3692,x3693),f9(x3691,x3694,x3693),x3693) % 0.51/0.66 [387]~P5(x3872,x3874,a1)+~P5(x3871,x3873,a1)+P5(f9(x3871,x3872,a1),f9(x3873,x3874,a1),a1) % 0.51/0.66 [417]~P19(x4173)+P5(x4171,x4172,x4173)+~P5(f9(x4174,x4171,x4173),f9(x4174,x4172,x4173),x4173) % 0.51/0.66 [418]~P19(x4183)+P5(x4181,x4182,x4183)+~P5(f9(x4181,x4184,x4183),f9(x4182,x4184,x4183),x4183) % 0.51/0.66 [419]E(x4191,x4192)+E(x4193,f8(a1))+~E(f9(x4194,f10(x4193,x4191,a1),a1),f9(x4194,f10(x4193,x4192,a1),a1)) % 0.51/0.66 [431]~P27(x4313)+~P7(x4313)+E(f9(f10(x4311,x4312,x4313),f10(x4311,x4314,x4313),x4313),f9(f10(x4311,x4314,x4313),f10(x4311,x4312,x4313),x4313)) % 0.51/0.66 [442]E(x4421,x4422)+E(x4423,x4424)+~E(f9(f10(x4423,x4421,a1),f10(x4424,x4422,a1),a1),f9(f10(x4423,x4422,a1),f10(x4424,x4421,a1),a1)) % 0.51/0.66 [382]~P9(x3823)+E(f9(x3821,x3822,x3823),x3824)+~E(f9(x3821,f9(x3825,x3822,x3823),x3823),f9(x3825,x3824,x3823)) % 0.51/0.66 [446]~P35(x4464)+~E(f9(f10(x4463,x4465,x4464),x4461,x4464),f9(f10(x4462,x4465,x4464),x4466,x4464))+E(x4461,f9(f10(f4(x4462,x4463,x4464),x4465,x4464),x4466,x4464)) % 0.51/0.66 [447]~P35(x4473)+~E(f9(f10(x4471,x4474,x4473),x4475,x4473),f9(f10(x4472,x4474,x4473),x4476,x4473))+E(f9(f10(f4(x4471,x4472,x4473),x4474,x4473),x4475,x4473),x4476) % 0.51/0.66 [452]~P36(x4524)+~P5(f9(f10(x4523,x4525,x4524),x4521,x4524),f9(f10(x4522,x4525,x4524),x4526,x4524),x4524)+P5(x4521,f9(f10(f4(x4522,x4523,x4524),x4525,x4524),x4526,x4524),x4524) % 0.51/0.66 [453]~P36(x4533)+~P5(f9(f10(x4531,x4534,x4533),x4535,x4533),f9(f10(x4532,x4534,x4533),x4536,x4533),x4533)+P5(f9(f10(f4(x4531,x4532,x4533),x4534,x4533),x4535,x4533),x4536,x4533) % 0.51/0.66 [454]~P36(x4543)+P5(f9(f10(x4541,x4542,x4543),x4544,x4543),f9(f10(x4545,x4542,x4543),x4546,x4543),x4543)+~P5(x4544,f9(f10(f4(x4545,x4541,x4543),x4542,x4543),x4546,x4543),x4543) % 0.51/0.66 [455]~P36(x4553)+P5(f9(f10(x4551,x4552,x4553),x4554,x4553),f9(f10(x4555,x4552,x4553),x4556,x4553),x4553)+~P5(f9(f10(f4(x4551,x4555,x4553),x4552,x4553),x4554,x4553),x4556,x4553) % 0.51/0.66 [261]P5(x2611,x2612,x2613)+~P31(x2613)+E(x2611,x2612)+P5(x2612,x2611,x2613) % 0.51/0.66 [265]P5(x2651,x2652,x2653)+~P23(x2653)+E(x2651,x2652)+P5(x2652,x2651,x2653) % 0.51/0.66 [243]~P27(x2432)+~P7(x2432)+~E(f9(x2433,x2431,x2432),x2433)+E(x2431,f8(x2432)) % 0.51/0.66 [245]~P27(x2453)+~P7(x2453)+E(x2451,x2452)+~E(f4(x2451,x2452,x2453),f8(x2453)) % 0.51/0.66 [248]~P34(x2482)+~E(f10(x2483,x2481,x2482),f8(x2482))+E(x2481,f8(x2482))+E(x2483,f8(x2482)) % 0.51/0.66 [250]~P25(x2502)+~E(f10(x2503,x2501,x2502),f8(x2502))+E(x2501,f8(x2502))+E(x2503,f8(x2502)) % 0.51/0.66 [373]~P32(x3731)+~P5(x3733,f8(x3731),x3731)+~P5(x3732,f8(x3731),x3731)+P5(f8(x3731),f10(x3732,x3733,x3731),x3731) % 0.51/0.66 [374]~P33(x3741)+~P5(f8(x3741),x3743,x3741)+~P5(f8(x3741),x3742,x3741)+P5(f8(x3741),f10(x3742,x3743,x3741),x3741) % 0.51/0.66 [375]~P14(x3751)+~P5(f8(x3751),x3753,x3751)+~P5(f8(x3751),x3752,x3751)+P5(f8(x3751),f9(x3752,x3753,x3751),x3751) % 0.51/0.66 [376]~P14(x3763)+~P5(x3762,f8(x3763),x3763)+~P5(x3761,f8(x3763),x3763)+P5(f9(x3761,x3762,x3763),f8(x3763),x3763) % 0.51/0.66 [377]~P33(x3773)+~P5(x3772,f8(x3773),x3773)+~P5(f8(x3773),x3771,x3773)+P5(f10(x3771,x3772,x3773),f8(x3773),x3773) % 0.51/0.66 [379]~P33(x3793)+~P5(x3791,f8(x3793),x3793)+~P5(f8(x3793),x3792,x3793)+P5(f10(x3791,x3792,x3793),f8(x3793),x3793) % 0.51/0.66 [385]~P33(x3851)+~P5(f8(x3851),f10(x3853,x3852,x3851),x3851)+P5(f8(x3851),x3852,x3851)+~P5(f8(x3851),x3853,x3851) % 0.51/0.66 [386]~P33(x3861)+~P5(f8(x3861),f10(x3862,x3863,x3861),x3861)+P5(f8(x3861),x3862,x3861)+~P5(f8(x3861),x3863,x3861) % 0.51/0.66 [315]~P22(x3153)+~P5(x3151,x3154,x3153)+P5(x3151,x3152,x3153)+~P5(x3154,x3152,x3153) % 0.51/0.66 [316]~P24(x3163)+~P5(x3161,x3164,x3163)+P5(x3161,x3162,x3163)+~P5(x3164,x3162,x3163) % 0.51/0.66 [303]~P27(x3034)+~P7(x3034)+E(x3031,x3032)+~E(f9(x3033,x3031,x3034),f9(x3033,x3032,x3034)) % 0.51/0.66 [365]~P29(x3654)+~P5(x3651,x3653,x3654)+~P5(f8(x3654),x3652,x3654)+P5(x3651,f9(x3652,x3653,x3654),x3654) % 0.51/0.66 [402]~P32(x4023)+~P5(x4024,x4021,x4023)+~P5(x4022,f8(x4023),x4023)+P5(f10(x4021,x4022,x4023),f10(x4024,x4022,x4023),x4023) % 0.51/0.66 [405]~P32(x4053)+~P5(x4054,x4052,x4053)+~P5(x4051,f8(x4053),x4053)+P5(f10(x4051,x4052,x4053),f10(x4051,x4054,x4053),x4053) % 0.51/0.66 [406]~P32(x4063)+~P5(x4061,x4064,x4063)+~P5(f8(x4063),x4062,x4063)+P5(f10(x4061,x4062,x4063),f10(x4064,x4062,x4063),x4063) % 0.51/0.66 [407]~P33(x4073)+~P5(x4071,x4074,x4073)+~P5(f8(x4073),x4072,x4073)+P5(f10(x4071,x4072,x4073),f10(x4074,x4072,x4073),x4073) % 0.51/0.66 [409]~P32(x4093)+~P5(x4092,x4094,x4093)+~P5(f8(x4093),x4091,x4093)+P5(f10(x4091,x4092,x4093),f10(x4091,x4094,x4093),x4093) % 0.51/0.66 [410]~P33(x4103)+~P5(x4102,x4104,x4103)+~P5(f8(x4103),x4101,x4103)+P5(f10(x4101,x4102,x4103),f10(x4101,x4104,x4103),x4103) % 0.51/0.66 [411]~P30(x4113)+~P5(x4112,x4114,x4113)+~P5(f8(x4113),x4111,x4113)+P5(f10(x4111,x4112,x4113),f10(x4111,x4114,x4113),x4113) % 0.51/0.66 [422]P5(x4222,x4221,x4223)+~P32(x4223)+P5(x4221,x4222,x4223)+~P5(f10(x4224,x4221,x4223),f10(x4224,x4222,x4223),x4223) % 0.51/0.66 [423]P5(x4232,x4231,x4233)+~P32(x4233)+P5(x4231,x4232,x4233)+~P5(f10(x4231,x4234,x4233),f10(x4232,x4234,x4233),x4233) % 0.51/0.66 [426]~P32(x4263)+P5(x4261,x4262,x4263)+~P5(f10(x4261,x4264,x4263),f10(x4262,x4264,x4263),x4263)+P5(x4264,f8(x4263),x4263) % 0.51/0.66 [427]~P32(x4273)+P5(x4271,x4272,x4273)+~P5(f10(x4274,x4271,x4273),f10(x4274,x4272,x4273),x4273)+P5(x4274,f8(x4273),x4273) % 0.51/0.66 [428]~P32(x4283)+P5(x4281,x4282,x4283)+~P5(f10(x4284,x4282,x4283),f10(x4284,x4281,x4283),x4283)+P5(f8(x4283),x4284,x4283) % 0.51/0.66 [429]~P32(x4293)+P5(x4291,x4292,x4293)+~P5(f10(x4292,x4294,x4293),f10(x4291,x4294,x4293),x4293)+P5(f8(x4293),x4294,x4293) % 0.51/0.66 [432]~P32(x4322)+~P5(f10(x4323,x4321,x4322),f10(x4324,x4321,x4322),x4322)+P5(x4321,f8(x4322),x4322)+P5(f8(x4322),x4321,x4322) % 0.51/0.66 [433]~P32(x4332)+~P5(f10(x4331,x4333,x4332),f10(x4331,x4334,x4332),x4332)+P5(x4331,f8(x4332),x4332)+P5(f8(x4332),x4331,x4332) % 0.51/0.66 [435]~P32(x4353)+P5(x4351,x4352,x4353)+~P5(f10(x4354,x4352,x4353),f10(x4354,x4351,x4353),x4353)+~P5(x4354,f8(x4353),x4353) % 0.51/0.66 [436]~P32(x4363)+P5(x4361,x4362,x4363)+~P5(f10(x4364,x4361,x4363),f10(x4364,x4362,x4363),x4363)+~P5(f8(x4363),x4364,x4363) % 0.51/0.66 [339]~P20(x3393)+~P5(x3394,x3395,x3393)+P5(x3391,x3392,x3393)+~E(f4(x3394,x3395,x3393),f4(x3391,x3392,x3393)) % 0.51/0.66 [340]~P20(x3403)+~P5(x3404,x3405,x3403)+P5(x3401,x3402,x3403)+~E(f4(x3401,x3402,x3403),f4(x3404,x3405,x3403)) % 0.51/0.66 [400]~P18(x4003)+~P5(x4002,x4005,x4003)+~P5(x4001,x4004,x4003)+P5(f9(x4001,x4002,x4003),f9(x4004,x4005,x4003),x4003) % 0.51/0.66 [421]~P27(x4214)+~P7(x4214)+E(x4211,x4212)+E(x4213,f8(x4214))+~E(f9(x4215,f10(x4213,x4211,x4214),x4214),f9(x4215,f10(x4213,x4212,x4214),x4214)) % 0.51/0.66 [444]~P27(x4445)+~P7(x4445)+E(x4441,x4442)+E(x4443,x4444)+~E(f9(f10(x4443,x4441,x4445),f10(x4444,x4442,x4445),x4445),f9(f10(x4443,x4442,x4445),f10(x4444,x4441,x4445),x4445)) % 0.51/0.66 %EqnAxiom % 0.51/0.66 [1]E(x11,x11) % 0.51/0.66 [2]E(x22,x21)+~E(x21,x22) % 0.51/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.51/0.66 [4]~E(x41,x42)+E(f2(x41),f2(x42)) % 0.51/0.66 [5]~E(x51,x52)+E(f9(x51,x53,x54),f9(x52,x53,x54)) % 0.51/0.66 [6]~E(x61,x62)+E(f9(x63,x61,x64),f9(x63,x62,x64)) % 0.51/0.66 [7]~E(x71,x72)+E(f9(x73,x74,x71),f9(x73,x74,x72)) % 0.51/0.66 [8]~E(x81,x82)+E(f3(x81,x83),f3(x82,x83)) % 0.51/0.66 [9]~E(x91,x92)+E(f3(x93,x91),f3(x93,x92)) % 0.51/0.66 [10]~E(x101,x102)+E(f4(x101,x103,x104),f4(x102,x103,x104)) % 0.51/0.66 [11]~E(x111,x112)+E(f4(x113,x111,x114),f4(x113,x112,x114)) % 0.51/0.66 [12]~E(x121,x122)+E(f4(x123,x124,x121),f4(x123,x124,x122)) % 0.51/0.66 [13]~E(x131,x132)+E(f8(x131),f8(x132)) % 0.51/0.66 [14]~E(x141,x142)+E(f10(x141,x143,x144),f10(x142,x143,x144)) % 0.51/0.66 [15]~E(x151,x152)+E(f10(x153,x151,x154),f10(x153,x152,x154)) % 0.51/0.66 [16]~E(x161,x162)+E(f10(x163,x164,x161),f10(x163,x164,x162)) % 0.51/0.66 [17]~E(x171,x172)+E(f14(x171),f14(x172)) % 0.51/0.66 [18]~E(x181,x182)+E(f12(x181,x183,x184),f12(x182,x183,x184)) % 0.51/0.66 [19]~E(x191,x192)+E(f12(x193,x191,x194),f12(x193,x192,x194)) % 0.51/0.66 [20]~E(x201,x202)+E(f12(x203,x204,x201),f12(x203,x204,x202)) % 0.51/0.66 [21]~E(x211,x212)+E(f15(x211,x213,x214),f15(x212,x213,x214)) % 0.51/0.66 [22]~E(x221,x222)+E(f15(x223,x221,x224),f15(x223,x222,x224)) % 0.51/0.66 [23]~E(x231,x232)+E(f15(x233,x234,x231),f15(x233,x234,x232)) % 0.51/0.66 [24]~E(x241,x242)+E(f13(x241,x243),f13(x242,x243)) % 0.51/0.66 [25]~E(x251,x252)+E(f13(x253,x251),f13(x253,x252)) % 0.51/0.66 [26]~E(x261,x262)+E(f16(x261,x263),f16(x262,x263)) % 0.51/0.66 [27]~E(x271,x272)+E(f16(x273,x271),f16(x273,x272)) % 0.51/0.66 [28]~E(x281,x282)+E(f17(x281,x283),f17(x282,x283)) % 0.51/0.66 [29]~E(x291,x292)+E(f17(x293,x291),f17(x293,x292)) % 0.51/0.66 [30]~E(x301,x302)+E(f6(x301),f6(x302)) % 0.51/0.66 [31]~E(x311,x312)+E(f11(x311),f11(x312)) % 0.51/0.66 [32]~E(x321,x322)+E(f7(x321,x323),f7(x322,x323)) % 0.51/0.66 [33]~E(x331,x332)+E(f7(x333,x331),f7(x333,x332)) % 0.51/0.66 [34]~E(x341,x342)+E(f5(x341),f5(x342)) % 0.51/0.66 [35]~P1(x351)+P1(x352)+~E(x351,x352) % 0.51/0.66 [36]~P2(x361)+P2(x362)+~E(x361,x362) % 0.51/0.66 [37]~P3(x371)+P3(x372)+~E(x371,x372) % 0.51/0.66 [38]~P25(x381)+P25(x382)+~E(x381,x382) % 0.51/0.66 [39]~P8(x391)+P8(x392)+~E(x391,x392) % 0.51/0.66 [40]~P28(x401)+P28(x402)+~E(x401,x402) % 0.51/0.66 [41]~P37(x411)+P37(x412)+~E(x411,x412) % 0.51/0.66 [42]~P14(x421)+P14(x422)+~E(x421,x422) % 0.51/0.66 [43]~P10(x431)+P10(x432)+~E(x431,x432) % 0.51/0.66 [44]~P13(x441)+P13(x442)+~E(x441,x442) % 0.51/0.66 [45]~P29(x451)+P29(x452)+~E(x451,x452) % 0.51/0.66 [46]~P33(x461)+P33(x462)+~E(x461,x462) % 0.51/0.66 [47]~P30(x471)+P30(x472)+~E(x471,x472) % 0.51/0.66 [48]~P15(x481)+P15(x482)+~E(x481,x482) % 0.51/0.66 [49]~P26(x491)+P26(x492)+~E(x491,x492) % 0.51/0.66 [50]~P18(x501)+P18(x502)+~E(x501,x502) % 0.51/0.66 [51]~P19(x511)+P19(x512)+~E(x511,x512) % 0.51/0.66 [52]~P11(x521)+P11(x522)+~E(x521,x522) % 0.51/0.66 [53]~P21(x531)+P21(x532)+~E(x531,x532) % 0.51/0.66 [54]~P22(x541)+P22(x542)+~E(x541,x542) % 0.51/0.66 [55]~P23(x551)+P23(x552)+~E(x551,x552) % 0.51/0.66 [56]~P24(x561)+P24(x562)+~E(x561,x562) % 0.51/0.66 [57]~P4(x571)+P4(x572)+~E(x571,x572) % 0.51/0.66 [58]P5(x582,x583,x584)+~E(x581,x582)+~P5(x581,x583,x584) % 0.51/0.66 [59]P5(x593,x592,x594)+~E(x591,x592)+~P5(x593,x591,x594) % 0.51/0.66 [60]P5(x603,x604,x602)+~E(x601,x602)+~P5(x603,x604,x601) % 0.51/0.66 [61]~P32(x611)+P32(x612)+~E(x611,x612) % 0.51/0.66 [62]~P7(x621)+P7(x622)+~E(x621,x622) % 0.51/0.66 [63]~P31(x631)+P31(x632)+~E(x631,x632) % 0.51/0.66 [64]~P27(x641)+P27(x642)+~E(x641,x642) % 0.51/0.66 [65]~P16(x651)+P16(x652)+~E(x651,x652) % 0.51/0.66 [66]~P20(x661)+P20(x662)+~E(x661,x662) % 0.51/0.66 [67]~P36(x671)+P36(x672)+~E(x671,x672) % 0.51/0.66 [68]P6(x682,x683)+~E(x681,x682)+~P6(x681,x683) % 0.51/0.66 [69]P6(x693,x692)+~E(x691,x692)+~P6(x693,x691) % 0.51/0.66 [70]~P9(x701)+P9(x702)+~E(x701,x702) % 0.51/0.66 [71]~P17(x711)+P17(x712)+~E(x711,x712) % 0.51/0.66 [72]~P35(x721)+P35(x722)+~E(x721,x722) % 0.51/0.66 [73]~P34(x731)+P34(x732)+~E(x731,x732) % 0.51/0.66 [74]~P12(x741)+P12(x742)+~E(x741,x742) % 0.51/0.66 % 0.51/0.66 %------------------------------------------- % 0.51/0.66 cnf(483,plain, % 0.51/0.66 ($false), % 0.51/0.66 inference(scs_inference,[],[167,98]), % 0.51/0.66 ['proof']). % 0.51/0.66 % SZS output end Proof % 0.51/0.66 % Total time :0.024953s %------------------------------------------------------------------------------