%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : ALG350-1 : TPTP v8.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n009.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 03:41:25 EDT 2024 % Result : Unsatisfiable 0.55s 0.72s % Output : CNFRefutation 0.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ALG350-1 : TPTP v8.2.0. Released v4.1.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n009.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Jun 19 17:03:08 EDT 2024 % 0.12/0.34 % CPUTime : % 0.21/0.58 start to proof:theBenchmark % 0.55/0.68 %------------------------------------------- % 0.55/0.68 % File :CSE---1.7 % 0.55/0.68 % Problem :theBenchmark % 0.55/0.68 % Transform :cnf % 0.55/0.68 % Format :tptp:raw % 0.55/0.68 % Command :java -jar mcs_scs.jar %d %s % 0.55/0.68 % 0.55/0.68 % Result :Theorem 0.010000s % 0.55/0.68 % Output :CNFRefutation 0.010000s % 0.55/0.68 %------------------------------------------- % 0.55/0.69 %------------------------------------------------------------------------------ % 0.55/0.69 % File : ALG350-1 : TPTP v8.2.0. Released v4.1.0. % 0.55/0.69 % Domain : General Algebra % 0.55/0.69 % Problem : Fundamental theorem of algebra 0166_5 % 0.55/0.69 % Version : Especial. % 0.55/0.69 % English : % 0.55/0.69 % 0.55/0.69 % Refs : [Nip10] Nipkow (2010), Email to Geoff Sutcliffe % 0.55/0.69 % : [BN10] Boehme & Nipkow (2010), Sledgehammer: Judgement Day % 0.55/0.69 % Source : [Nip10] % 0.55/0.69 % Names : Fundamental_Theorem_Algebra-0166_5 [Nip10] % 0.55/0.69 % 0.55/0.69 % Status : Unsatisfiable % 0.55/0.69 % Rating : 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.0.0, 0.10 v5.5.0, 0.15 v5.4.0, 0.20 v5.3.0, 0.17 v5.2.0, 0.06 v5.1.0, 0.18 v5.0.0, 0.14 v4.1.0 % 0.55/0.69 % Syntax : Number of clauses : 380 ( 36 unt; 25 nHn; 190 RR) % 0.55/0.69 % Number of literals : 960 ( 187 equ; 563 neg) % 0.55/0.69 % Maximal clause size : 4 ( 2 avg) % 0.55/0.69 % Maximal term depth : 4 ( 1 avg) % 0.55/0.69 % Number of predicates : 35 ( 34 usr; 0 prp; 1-3 aty) % 0.55/0.69 % Number of functors : 23 ( 23 usr; 7 con; 0-3 aty) % 0.55/0.69 % Number of variables : 1141 ( 71 sgn) % 0.55/0.69 % SPC : CNF_UNS_RFO_SEQ_NHN % 0.55/0.69 % 0.55/0.69 % Comments : % 0.55/0.69 %------------------------------------------------------------------------------ % 0.55/0.69 cnf(cls_norm__minus__cancel_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_RealVector_Onorm__class_Onorm(c_HOL_Ouminus__class_Ouminus(V_x,T_a),T_a) = c_RealVector_Onorm__class_Onorm(V_x,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_abs__norm__cancel_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_HOL_Oabs__class_Oabs(c_RealVector_Onorm__class_Onorm(V_a,T_a),tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(V_a,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_norm__minus__commute_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a) = c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_norm__triangle__ineq_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(V_x,V_y,T_a),T_a),c_HOL_Oplus__class_Oplus(c_RealVector_Onorm__class_Onorm(V_x,T_a),c_RealVector_Onorm__class_Onorm(V_y,T_a),tc_RealDef_Oreal),tc_RealDef_Oreal) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_norm__add__less_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(c_HOL_Oplus__class_Oplus(V_x,V_y,T_a),T_a),c_HOL_Oplus__class_Oplus(V_r,V_s,tc_RealDef_Oreal),tc_RealDef_Oreal) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_y,T_a),V_s,tc_RealDef_Oreal) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(c_RealVector_Onorm__class_Onorm(V_x,T_a),V_r,tc_RealDef_Oreal) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_norm__triangle__ineq4_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a),c_HOL_Oplus__class_Oplus(c_RealVector_Onorm__class_Onorm(V_a,T_a),c_RealVector_Onorm__class_Onorm(V_b,T_a),tc_RealDef_Oreal),tc_RealDef_Oreal) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_order__less__trans_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_xt1_I10_J_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_sup__idem_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.69 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_x,T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_lordered__ab__group__add__class_Oadd__sup__inf__distribs_I3_J_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.69 | c_HOL_Oplus__class_Oplus(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_c,T_a) = c_Lattices_Oupper__semilattice__class_Osup(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.55/0.69 % 0.55/0.69 cnf(cls_lordered__ab__group__add__class_Oadd__sup__inf__distribs_I4_J_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.69 | c_HOL_Oplus__class_Oplus(V_a,c_Lattices_Oupper__semilattice__class_Osup(V_b,V_c,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_add__sup__distrib__left_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add__join(T_a) % 0.55/0.69 | c_HOL_Oplus__class_Oplus(V_a,c_Lattices_Oupper__semilattice__class_Osup(V_b,V_c,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_add__sup__distrib__right_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add__join(T_a) % 0.55/0.69 | c_HOL_Oplus__class_Oplus(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_c,T_a) = c_Lattices_Oupper__semilattice__class_Osup(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.55/0.69 % 0.55/0.69 cnf(cls_inf__sup__distrib1_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Odistrib__lattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__sup__distrib2_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Odistrib__lattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),V_x,T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a),c_Lattices_Olower__semilattice__class_Oinf(V_z,V_x,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_diff__add__cancel_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.69 | c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),V_b,T_a) = V_a ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_min__max_Oinf__left__idem_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) = c_Orderings_Oord__class_Omin(V_x,V_y,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_abs__triangle__ineq3_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.69 | c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Oabs__class_Oabs(V_b,T_a),T_a),T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_min__less__iff__conj_2,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_z,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_z,V_x,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_max__less__iff__conj_2,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_x,V_z,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_min__max_Oinf__sup__distrib1_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omax(V_y,V_z,T_a),T_a) = c_Orderings_Oord__class_Omax(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),c_Orderings_Oord__class_Omin(V_x,V_z,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_min__max_Oinf__sup__distrib2_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_Orderings_Oord__class_Omin(c_Orderings_Oord__class_Omax(V_y,V_z,T_a),V_x,T_a) = c_Orderings_Oord__class_Omax(c_Orderings_Oord__class_Omin(V_y,V_x,T_a),c_Orderings_Oord__class_Omin(V_z,V_x,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_add__eq__inf__sup_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.69 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__bot__left_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Obot__class_Obot(T_a),V_x,T_a) = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__bot__right_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Orderings_Obot__class_Obot(T_a),T_a) = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_abs__less__iff_1,axiom, % 0.55/0.69 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__sup__aci_I2_J_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__sup__aci_I3_J_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__assoc_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__left__commute_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_sup__bot__left_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.69 | c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Obot__class_Obot(T_a),V_x,T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_sup__bot__right_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.69 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Orderings_Obot__class_Obot(T_a),T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_neg__less__iff__less_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_b,T_a),c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_neg__less__iff__less_1,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_b,T_a),c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) % 0.55/0.69 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_abs__lattice_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add__abs(T_a) % 0.55/0.69 | c_HOL_Oabs__class_Oabs(V_a,T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_a,c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__top__left_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(c_Orderings_Otop__class_Otop(T_a),V_x,T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__top__right_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Orderings_Otop__class_Otop(T_a),T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_distrib__sup__le_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.69 | c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a),c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),c_Lattices_Oupper__semilattice__class_Osup(V_x,V_z,T_a),T_a),T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_min__max_Oinf__idem_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_Orderings_Oord__class_Omin(V_x,V_x,T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_estimate__by__abs_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Olordered__ab__group__add__abs(T_a) % 0.55/0.69 | c_lessequals(V_a,c_HOL_Oplus__class_Oplus(V_c,c_HOL_Oabs__class_Oabs(V_b,T_a),T_a),T_a) % 0.55/0.69 | ~ c_lessequals(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_c,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_neg__equal__iff__equal_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.69 | c_HOL_Ouminus__class_Ouminus(V_a,T_a) != c_HOL_Ouminus__class_Ouminus(V_b,T_a) % 0.55/0.69 | V_a = V_b ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_compl__eq__compl__iff_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.69 | c_HOL_Ouminus__class_Ouminus(V_x,T_a) != c_HOL_Ouminus__class_Ouminus(V_y,T_a) % 0.55/0.69 | V_x = V_y ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_linorder__neqE_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.69 | V_x = V_y ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_linorder__less__linear_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.69 | V_x = V_y % 0.55/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_linorder__antisym__conv3_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | V_x = V_y % 0.55/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_not__less__iff__gr__or__eq_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | V_x = V_y % 0.55/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_linorder__neqE__ordered__idom_0,axiom, % 0.55/0.69 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.69 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.69 | V_x = V_y ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_min__max_Osup__idem_0,axiom, % 0.55/0.69 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.69 | c_Orderings_Oord__class_Omax(V_x,V_x,T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_inf__sup__absorb_0,axiom, % 0.55/0.69 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.69 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) = V_x ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_norm__diff__triangle__ineq_0,axiom, % 0.55/0.69 ( ~ class_RealVector_Oreal__normed__vector(T_a) % 0.55/0.69 | c_lessequals(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_c,V_d,T_a),T_a),T_a),c_HOL_Oplus__class_Oplus(c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_a,V_c,T_a),T_a),c_RealVector_Onorm__class_Onorm(c_HOL_Ominus__class_Ominus(V_b,V_d,T_a),T_a),tc_RealDef_Oreal),tc_RealDef_Oreal) ) ). % 0.55/0.69 % 0.55/0.69 cnf(cls_comm__monoid__add_Omult__left__commute_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.69 | 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.55/0.69 % 0.55/0.69 cnf(cls_comm__monoid__add_Omult__assoc_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.69 | 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.55/0.69 % 0.55/0.69 cnf(cls_class__semiring_Oadd__a_0,axiom, % 0.55/0.69 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.69 | 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.55/0.69 % 0.55/0.69 cnf(cls_add__cancel__21_1,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.69 | 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.55/0.69 % 0.55/0.69 cnf(cls_ab__semigroup__add__class_Oadd__ac_I1_J_0,axiom, % 0.55/0.69 ( ~ class_OrderedGroup_Oab__semigroup__add(T_a) % 0.55/0.69 | 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.55/0.69 % 0.55/0.69 cnf(cls_class__semiring_Osemiring__rules_I25_J_0,axiom, % 0.55/0.69 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.69 | 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.55/0.70 % 0.55/0.70 cnf(cls_class__semiring_Osemiring__rules_I23_J_0,axiom, % 0.55/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.70 | 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.55/0.70 % 0.55/0.70 cnf(cls_class__semiring_Osemiring__rules_I22_J_0,axiom, % 0.55/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.70 | 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.55/0.70 % 0.55/0.70 cnf(cls_class__semiring_Osemiring__rules_I21_J_0,axiom, % 0.55/0.70 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.70 | 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.55/0.70 % 0.55/0.70 cnf(cls_abs__triangle__ineq_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.70 | c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a),c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Oabs__class_Oabs(V_b,T_a),T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_COMBI__def_0,axiom, % 0.55/0.70 c_COMBI(V_P,T_a) = V_P ). % 0.55/0.70 % 0.55/0.70 cnf(cls_eq__eqI_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.70 | 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.55/0.70 | V_x_H = V_y_H ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_eq__eqI_1,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.70 | c_HOL_Ominus__class_Ominus(V_xa,V_y,T_a) != c_HOL_Ominus__class_Ominus(V_x,V_x,T_a) % 0.55/0.70 | V_xa = V_y ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oinf__sup__absorb_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) = V_x ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_diff__eq_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.70 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__left__commute_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__assoc_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__sup__aci_I7_J_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__sup__aci_I6_J_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_max__less__iff__conj_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_max__less__iff__conj_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__max__iff__disj_2,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_z,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__max__iff__disj_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_z,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_z,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oless__supI2_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,c_Orderings_Oord__class_Omax(V_a,V_b,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oless__supI1_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,c_Orderings_Oord__class_Omax(V_a,V_b,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_a,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__commute_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.70 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__sup__aci_I1_J_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.70 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oinf__commute_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omin(V_x,V_y,T_a) = c_Orderings_Oord__class_Omin(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_Deriv_Oadd__diff__add_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.70 | c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),c_HOL_Oplus__class_Oplus(V_b,V_d,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),c_HOL_Ominus__class_Ominus(V_c,V_d,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__less__iff__disj_2,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__less__iff__disj_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__less__iff__conj_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_z,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__less__iff__conj_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_z,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oless__infI2_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omin(V_a,V_b,T_a),V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_b,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oless__infI1_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omin(V_a,V_b,T_a),V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_a,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__diff__less__iff_0,axiom, % 0.55/0.70 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_a,V_r,T_a),V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_x,V_a,T_a),T_a),V_r,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__eq__bot__eq2_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,T_a) != c_Orderings_Obot__class_Obot(T_a) % 0.55/0.70 | V_B = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__eq__bot__eq1_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_A,V_B,T_a) != c_Orderings_Obot__class_Obot(T_a) % 0.55/0.70 | V_A = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__eq__neg__sup_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.70 | c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a) = c_HOL_Ouminus__class_Ouminus(c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__commute_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__sup__aci_I5_J_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_neg__inf__eq__sup_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_compl__inf_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ouminus__class_Ouminus(V_x,T_a),c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_add__cancel__end_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.70 | c_HOL_Oplus__class_Oplus(V_x,c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) != V_y % 0.55/0.70 | V_x = c_HOL_Ouminus__class_Ouminus(V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__left__idem_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_inf__sup__aci_I8_J_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) = c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_real__sqrt__less__iff_0,axiom, % 0.55/0.70 ( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_real__sqrt__less__iff_1,axiom, % 0.55/0.70 ( c_HOL_Oord__class_Oless(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__left__commute_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,c_Orderings_Oord__class_Omax(V_y,V_z,T_a),T_a) = c_Orderings_Oord__class_Omax(V_y,c_Orderings_Oord__class_Omax(V_x,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__assoc_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) = c_Orderings_Oord__class_Omax(V_x,c_Orderings_Oord__class_Omax(V_y,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_diff__minus__eq__add_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | c_HOL_Ominus__class_Ominus(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) = c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_add__diff__cancel_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),V_b,T_a) = V_a ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__diff__less__iff_2,axiom, % 0.55/0.70 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_x,V_a,T_a),T_a),V_r,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,c_HOL_Oplus__class_Oplus(V_a,V_r,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_a,V_r,T_a),V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_minus__equation__iff_1,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) = V_b ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_equation__minus__iff_1,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | V_a = c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_equation__minus__iff_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | V_b = c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_double__compl_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_x,T_a),T_a) = V_x ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_minus__minus_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) = V_a ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_minus__diff__eq_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a) = c_HOL_Ominus__class_Ominus(V_b,V_a,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_add__less__le__mono_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.70 | 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.55/0.70 | ~ c_lessequals(V_c,V_d,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_add__le__less__mono_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.70 | 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.55/0.70 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.55/0.70 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_minus__less__iff_1,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_b,T_a),V_a,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_minus__less__iff_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_b,T_a),V_a,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__minus__iff_1,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_b,c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__minus__iff_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_b,c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_xt1_I7_J_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.55/0.70 | ~ c_lessequals(V_z,V_y,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_xt1_I8_J_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.55/0.70 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_le__add__right__mono_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | c_lessequals(V_a,c_HOL_Oplus__class_Oplus(V_b,V_d,T_a),T_a) % 0.55/0.70 | ~ c_lessequals(V_c,V_d,T_a) % 0.55/0.70 | ~ c_lessequals(V_a,c_HOL_Oplus__class_Oplus(V_b,V_c,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_order__less__le__trans_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.55/0.70 | ~ c_lessequals(V_y,V_z,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_order__le__less__trans_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__absorb1_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) = V_x % 0.55/0.70 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_le__iff__sup_1,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) != V_y % 0.55/0.70 | c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_le__iff__sup_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) = V_y % 0.55/0.70 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_order__less__imp__le_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_y,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_order__le__less_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_y,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__le__not__le_2,axiom, % 0.55/0.70 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.70 | c_lessequals(V_y,V_x,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__sup__iff_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_y,V_z,T_a) % 0.55/0.70 | ~ c_lessequals(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__sup__iff_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_z,T_a) % 0.55/0.70 | ~ c_lessequals(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_le__max__iff__disj_2,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_z,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) % 0.55/0.70 | ~ c_lessequals(V_z,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_le__max__iff__disj_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_z,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) % 0.55/0.70 | ~ c_lessequals(V_z,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__supI2_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,c_Orderings_Oord__class_Omax(V_a,V_b,T_a),T_a) % 0.55/0.70 | ~ c_lessequals(V_x,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__supI1_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,c_Orderings_Oord__class_Omax(V_a,V_b,T_a),T_a) % 0.55/0.70 | ~ c_lessequals(V_x,V_a,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__supE_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_b,V_x,T_a) % 0.55/0.70 | ~ c_lessequals(c_Orderings_Oord__class_Omax(V_a,V_b,T_a),V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__supE_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_a,V_x,T_a) % 0.55/0.70 | ~ c_lessequals(c_Orderings_Oord__class_Omax(V_a,V_b,T_a),V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__le__iff__disj_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_y,V_z,T_a) % 0.55/0.70 | c_lessequals(V_x,V_z,T_a) % 0.55/0.70 | ~ c_lessequals(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__ge__self_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.70 | c_lessequals(V_a,c_HOL_Oabs__class_Oabs(V_a,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__inf__iff_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_z,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__inf__iff_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_y,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__le__iff__disj_2,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) % 0.55/0.70 | ~ c_lessequals(V_y,V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__le__iff__disj_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,V_z,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__infI2_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(c_Orderings_Oord__class_Omin(V_a,V_b,T_a),V_x,T_a) % 0.55/0.70 | ~ c_lessequals(V_b,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__infI1_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(c_Orderings_Oord__class_Omin(V_a,V_b,T_a),V_x,T_a) % 0.55/0.70 | ~ c_lessequals(V_a,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__infE_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_b,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_a,V_b,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__infE_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_x,V_a,T_a) % 0.55/0.70 | ~ c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_a,V_b,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_le__max__iff__disj_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_lessequals(V_z,V_y,T_a) % 0.55/0.70 | c_lessequals(V_z,V_x,T_a) % 0.55/0.70 | ~ c_lessequals(V_z,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_add__mono_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add(T_a) % 0.55/0.70 | c_lessequals(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.55/0.70 | ~ c_lessequals(V_c,V_d,T_a) % 0.55/0.70 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__absorb1_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,V_y,T_a) = V_x % 0.55/0.70 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__iff__sup_1,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,V_y,T_a) != V_y % 0.55/0.70 | c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Ole__iff__sup_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,V_y,T_a) = V_y % 0.55/0.70 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Oinf__absorb2_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omin(V_x,V_y,T_a) = V_y % 0.55/0.70 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__infI1_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_a,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__infI2_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_b,V_x,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__less__iff_2,axiom, % 0.55/0.70 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__le__D2_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.70 | c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.70 | ~ c_lessequals(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_add__minus__cancel_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.70 | c_HOL_Oplus__class_Oplus(V_a,c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a),T_a) = V_b ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__inf__distrib1_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Odistrib__lattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),c_Lattices_Oupper__semilattice__class_Osup(V_x,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_sup__inf__distrib2_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Odistrib__lattice(T_a) % 0.55/0.70 | c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),V_x,T_a) = c_Lattices_Olower__semilattice__class_Oinf(c_Lattices_Oupper__semilattice__class_Osup(V_y,V_x,T_a),c_Lattices_Oupper__semilattice__class_Osup(V_z,V_x,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_compl__bot__eq_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.70 | c_HOL_Ouminus__class_Ouminus(c_Orderings_Obot__class_Obot(T_a),T_a) = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_real__sqrt__eq__iff_0,axiom, % 0.55/0.70 ( c_NthRoot_Osqrt(V_x) != c_NthRoot_Osqrt(V_y) % 0.55/0.70 | V_x = V_y ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_exp__inj__iff_0,axiom, % 0.55/0.70 ( c_Transcendental_Oexp(V_x,tc_RealDef_Oreal) != c_Transcendental_Oexp(V_y,tc_RealDef_Oreal) % 0.55/0.70 | V_x = V_y ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__eqI_1,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | 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.55/0.70 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__eqI_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.70 | 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.55/0.70 | c_HOL_Oord__class_Oless(V_x_H,V_y_H,T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__inf__distrib1_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) = c_Orderings_Oord__class_Omin(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),c_Orderings_Oord__class_Omax(V_x,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__inf__distrib2_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(c_Orderings_Oord__class_Omin(V_y,V_z,T_a),V_x,T_a) = c_Orderings_Oord__class_Omin(c_Orderings_Oord__class_Omax(V_y,V_x,T_a),c_Orderings_Oord__class_Omax(V_z,V_x,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__triangle__ineq2_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.70 | c_lessequals(c_HOL_Ominus__class_Ominus(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Oabs__class_Oabs(V_b,T_a),T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__supI1_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_a,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_less__supI2_0,axiom, % 0.55/0.70 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.70 | c_HOL_Oord__class_Oless(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a) % 0.55/0.70 | ~ c_HOL_Oord__class_Oless(V_x,V_b,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_abs__minus__commute_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.70 | c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a) = c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_b,V_a,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__left__idem_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) = c_Orderings_Oord__class_Omax(V_x,V_y,T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_max__add__distrib__left_0,axiom, % 0.55/0.70 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.70 | c_HOL_Oplus__class_Oplus(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) = c_Orderings_Oord__class_Omax(c_HOL_Oplus__class_Oplus(V_x,V_z,T_a),c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_min__max_Osup__inf__absorb_0,axiom, % 0.55/0.70 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.70 | c_Orderings_Oord__class_Omax(V_x,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) = V_x ) ). % 0.55/0.70 % 0.55/0.70 cnf(cls_compl__sup_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_HOL_Ouminus__class_Ouminus(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(V_x,T_a),c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_neg__sup__eq__inf_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.71 | c_HOL_Ouminus__class_Ouminus(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Odistrib__inf__le_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omax(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),c_Orderings_Oord__class_Omin(V_x,V_z,T_a),T_a),c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omax(V_y,V_z,T_a),T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Osup__commute_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_Orderings_Oord__class_Omax(V_x,V_y,T_a) = c_Orderings_Oord__class_Omax(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_class__semiring_Osemiring__rules_I20_J_0,axiom, % 0.55/0.71 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.71 | 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.55/0.71 % 0.55/0.71 cnf(cls_diff__def_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_class__ring_Osub__add_0,axiom, % 0.55/0.71 ( ~ class_Int_Onumber__ring(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_x,c_HOL_Ouminus__class_Ouminus(V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_diff__minus_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_ab__diff__minus_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__add__distrib__left_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) = c_Orderings_Oord__class_Omin(c_HOL_Oplus__class_Oplus(V_x,V_z,T_a),c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__leI_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) % 0.55/0.71 | ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__le__iff_2,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) % 0.55/0.71 | ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__minus__cancel_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_HOL_Oabs__class_Oabs(c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) = c_HOL_Oabs__class_Oabs(V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_class__ringb_Oadd__cancel_0,axiom, % 0.55/0.71 ( ~ class_Ring__and__Field_Oidom(T_a) % 0.55/0.71 | ~ class_Int_Onumber__ring(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) != c_HOL_Oplus__class_Oplus(V_x,V_z,T_a) % 0.55/0.71 | V_y = V_z ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__imp__eq_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ocancel__ab__semigroup__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Oplus__class_Oplus(V_a,V_c,T_a) % 0.55/0.71 | V_b = V_c ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__left__cancel_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) != c_HOL_Oplus__class_Oplus(V_a,V_c,T_a) % 0.55/0.71 | V_b = V_c ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__right__cancel_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ocancel__semigroup__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_b,V_a,T_a) != c_HOL_Oplus__class_Oplus(V_c,V_a,T_a) % 0.55/0.71 | V_b = V_c ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_exp__less__mono_0,axiom, % 0.55/0.71 ( c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_Transcendental_Oexp(V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_exp__less__cancel_0,axiom, % 0.55/0.71 ( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_Transcendental_Oexp(V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_compl__sup__top_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(c_HOL_Ouminus__class_Ouminus(V_x,T_a),V_x,T_a) = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__compl__top_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_HOL_Ouminus__class_Ouminus(V_x,T_a),T_a) = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_compl__unique_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a) != c_Orderings_Otop__class_Otop(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) != c_Orderings_Obot__class_Obot(T_a) % 0.55/0.71 | c_HOL_Ouminus__class_Ouminus(V_x,T_a) = V_y ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_distrib__inf__le_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),c_Lattices_Olower__semilattice__class_Oinf(V_x,V_z,T_a),T_a),c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Oinf__assoc_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_Orderings_Oord__class_Omin(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) = c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Oinf__left__commute_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) = c_Orderings_Oord__class_Omin(V_y,c_Orderings_Oord__class_Omin(V_x,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_lordered__ab__group__add__class_Oadd__sup__inf__distribs_I1_J_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_c,T_a) = c_Lattices_Olower__semilattice__class_Oinf(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.55/0.71 % 0.55/0.71 cnf(cls_lordered__ab__group__add__class_Oadd__sup__inf__distribs_I2_J_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_a,c_Lattices_Olower__semilattice__class_Oinf(V_b,V_c,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__inf__distrib__left_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Olordered__ab__group__add__meet(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_a,c_Lattices_Olower__semilattice__class_Oinf(V_b,V_c,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__inf__distrib__right_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Olordered__ab__group__add__meet(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_c,T_a) = c_Lattices_Olower__semilattice__class_Oinf(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.55/0.71 % 0.55/0.71 cnf(cls_max__diff__distrib__left_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) = c_Orderings_Oord__class_Omax(c_HOL_Ominus__class_Ominus(V_x,V_z,T_a),c_HOL_Ominus__class_Ominus(V_y,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__cancel__21_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.71 | 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.55/0.71 | c_HOL_Oplus__class_Oplus(V_x,V_z,T_a) = V_u ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__diff__triangle__ineq_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),c_HOL_Oplus__class_Oplus(V_c,V_d,T_a),T_a),T_a),c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_a,V_c,T_a),T_a),c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_b,V_d,T_a),T_a),T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_arctan__monotone_0,axiom, % 0.55/0.71 ( c_HOL_Oord__class_Oless(c_Transcendental_Oarctan(V_x),c_Transcendental_Oarctan(V_y),tc_RealDef_Oreal) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__diff__distrib__left_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) = c_Orderings_Oord__class_Omin(c_HOL_Ominus__class_Ominus(V_x,V_z,T_a),c_HOL_Ominus__class_Ominus(V_y,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_compl__inf__bot_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(V_x,T_a),V_x,T_a) = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__compl__bot_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_HOL_Ouminus__class_Ouminus(V_x,T_a),T_a) = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__idempotent_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_HOL_Oabs__class_Oabs(c_HOL_Oabs__class_Oabs(V_a,T_a),T_a) = c_HOL_Oabs__class_Oabs(V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__top__left_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(c_Orderings_Otop__class_Otop(T_a),V_x,T_a) = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__top__right_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Orderings_Otop__class_Otop(T_a),T_a) = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_class__semiring_Osemiring__rules_I24_J_0,axiom, % 0.55/0.71 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_a,V_c,T_a) = c_HOL_Oplus__class_Oplus(V_c,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_class__semiring_Oadd__c_0,axiom, % 0.55/0.71 ( ~ class_Ring__and__Field_Ocomm__semiring__1(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_x,V_y,T_a) = c_HOL_Oplus__class_Oplus(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_comm__monoid__add_Omult__commute_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ocomm__monoid__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(V_a,V_b,T_a) = c_HOL_Oplus__class_Oplus(V_b,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__ge__minus__self_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Oabs__class_Oabs(V_a,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_less__max__iff__disj_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_z,V_y,T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_z,V_x,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_z,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__less__iff_0,axiom, % 0.55/0.71 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__less__iff__disj_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_y,V_z,T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_z,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__exp__cancel_0,axiom, % 0.55/0.71 c_HOL_Oabs__class_Oabs(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),tc_RealDef_Oreal) = c_Transcendental_Oexp(V_x,tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__eq__top__eq1_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,T_a) != c_Orderings_Otop__class_Otop(T_a) % 0.55/0.71 | V_A = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__eq__top__eq2_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Obounded__lattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_A,V_B,T_a) != c_Orderings_Otop__class_Otop(T_a) % 0.55/0.71 | V_B = c_Orderings_Otop__class_Otop(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_compl__top__eq_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oboolean__algebra(T_a) % 0.55/0.71 | c_HOL_Ouminus__class_Ouminus(c_Orderings_Otop__class_Otop(T_a),T_a) = c_Orderings_Obot__class_Obot(T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__neq__iff_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__less__le_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__less__def_1,axiom, % 0.55/0.71 ~ c_HOL_Oord__class_Oless(V_x,V_x,tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__less__irrefl_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__inf__absorb_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = V_x ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__strict__mono_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.71 | 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.55/0.71 | ~ c_HOL_Oord__class_Oless(V_c,V_d,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__cancel__end_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_z,T_a),c_HOL_Oplus__class_Oplus(V_y,V_z,T_a),T_a) = V_y ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_minus__add__cancel_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.71 | c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a) = V_b ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__triangle__ineq4_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a),c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Oabs__class_Oabs(V_b,T_a),T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__sup__aci_I4_J_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__left__idem_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),T_a) = c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_Lim_Ominus__diff__minus_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.71 | c_HOL_Ominus__class_Ominus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) = c_HOL_Ouminus__class_Ouminus(c_HOL_Ominus__class_Ominus(V_a,V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__add__abs_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_HOL_Oabs__class_Oabs(c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Oabs__class_Oabs(V_b,T_a),T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Oabs__class_Oabs(V_a,T_a),c_HOL_Oabs__class_Oabs(V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__idem_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_x,T_a) = V_x ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__less__cancel__left_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.71 | ~ 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.55/0.71 % 0.55/0.71 cnf(cls_add__less__cancel__left_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | 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.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__strict__left__mono_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.71 | 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.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__less__cancel__right_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.71 | ~ 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.55/0.71 % 0.55/0.71 cnf(cls_add__less__cancel__right_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | 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.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__strict__right__mono_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__cancel__ab__semigroup__add(T_a) % 0.55/0.71 | 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.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__diff__less__iff_1,axiom, % 0.55/0.71 ( ~ class_Ring__and__Field_Oordered__idom(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,c_HOL_Oplus__class_Oplus(V_a,V_r,T_a),T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(c_HOL_Oabs__class_Oabs(c_HOL_Ominus__class_Ominus(V_x,V_a,T_a),T_a),V_r,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Odistrib__sup__le_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omax(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a),c_Orderings_Oord__class_Omin(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),c_Orderings_Oord__class_Omax(V_x,V_z,T_a),T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__eq__neg__inf_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Olordered__ab__group__add(T_a) % 0.55/0.71 | c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a) = c_HOL_Ouminus__class_Ouminus(c_Lattices_Olower__semilattice__class_Oinf(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_minus__add_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Ogroup__add(T_a) % 0.55/0.71 | c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_b,T_a),c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_minus__add__distrib_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Oab__group__add(T_a) % 0.55/0.71 | c_HOL_Ouminus__class_Ouminus(c_HOL_Oplus__class_Oplus(V_a,V_b,T_a),T_a) = c_HOL_Oplus__class_Oplus(c_HOL_Ouminus__class_Ouminus(V_a,T_a),c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__less__asym_H_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__less__asym_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_not__less__iff__gr__or__eq_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_xt1_I9_J_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_b,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Ole__iff__inf_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_Orderings_Oord__class_Omin(V_x,V_y,T_a) != V_x % 0.55/0.71 | c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Ole__iff__inf_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_Orderings_Oord__class_Omin(V_x,V_y,T_a) = V_x % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__sup__iff_2,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_z,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__least_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_y,V_z,T_a),V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_z,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__ge2_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_sup__ge1_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__supI_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_b,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__sup__ord_I4_J_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_lessequals(V_y,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__sup__ord_I3_J_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__inf__iff_1,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__inf__iff_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,V_y,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__infI2_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_b,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__infI1_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__infE_1,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__infE_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,V_a,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_xt1_I11_J_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.55/0.71 | V_a = V_b % 0.55/0.71 | ~ c_lessequals(V_b,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_xt1_I12_J_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_b,V_a,T_a) % 0.55/0.71 | ~ c_lessequals(V_b,V_a,T_a) % 0.55/0.71 | V_a = V_b ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__antisym__conv2_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__antisym__conv1_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__neq__le__trans_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) % 0.55/0.71 | V_a = V_b ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__le__neq__trans_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_a,V_b,T_a) % 0.55/0.71 | V_a = V_b % 0.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__le__less_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__less__le_2,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__eqI_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | 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.55/0.71 | c_lessequals(V_y_H,V_x_H,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__eqI_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | 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.55/0.71 | c_lessequals(V_y,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_y_H,V_x_H,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__sup__iff_1,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_y,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__sup__iff_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_x,V_y,T_a),V_z,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__supI2_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__supI1_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__supE_1,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_b,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__supE_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Oupper__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_a,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(c_Lattices_Oupper__semilattice__class_Osup(V_a,V_b,T_a),V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_top__greatest_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Otop(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Orderings_Otop__class_Otop(T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__greatest_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__inf__iff_2,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_y,V_z,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__infI_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Lattices_Olower__semilattice__class_Oinf(V_a,V_b,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__le2_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__le1_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__sup__ord_I2_J_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__sup__ord_I1_J_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olattice(T_a) % 0.55/0.71 | c_lessequals(c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a),V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__le__cancel__right_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_lessequals(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.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__le__cancel__right_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_lessequals(V_a,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(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.55/0.71 % 0.55/0.71 cnf(cls_add__le__cancel__left_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_lessequals(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.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__le__cancel__left_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) % 0.55/0.71 | c_lessequals(V_a,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(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.55/0.71 % 0.55/0.71 cnf(cls_add__right__mono_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add(T_a) % 0.55/0.71 | c_lessequals(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.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_add__left__mono_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__semigroup__add(T_a) % 0.55/0.71 | c_lessequals(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.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_bot__least_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Obot(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Obot__class_Obot(T_a),V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Ole__sup__iff_2,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omax(V_x,V_y,T_a),V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_z,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Osup__least_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omax(V_y,V_z,T_a),V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_z,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Ole__supI_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omax(V_a,V_b,T_a),V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_b,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__maxI1_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__maxI2_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_y,c_Orderings_Oord__class_Omax(V_x,V_y,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_neg__le__iff__le_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_lessequals(V_a,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(V_b,T_a),c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__imp__neg__le_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Ouminus__class_Ouminus(V_b,T_a),c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_a,V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__le__D1_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add__abs(T_a) % 0.55/0.71 | c_lessequals(V_a,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(c_HOL_Oabs__class_Oabs(V_a,T_a),V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Oinf__greatest_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Ole__inf__iff_2,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_y,V_z,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Ole__infI_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_x,c_Orderings_Oord__class_Omin(V_a,V_b,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_b,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Oinf__le2_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_min__max_Oinf__le1_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(c_Orderings_Oord__class_Omin(V_x,V_y,T_a),V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_less__le__not__le_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_not__leE_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.71 | c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__antisym__conv2_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_x,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__antisym__conv1_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_x,T_a) % 0.55/0.71 | c_lessequals(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__not__less_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__not__less_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_y,V_x,T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__not__le_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_HOL_Oord__class_Oless(V_y,V_x,T_a) % 0.55/0.71 | c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__not__le_1,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_inf__absorb2_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = V_y % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__iff__inf_1,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) != V_x % 0.55/0.71 | c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__iff__inf_0,axiom, % 0.55/0.71 ( ~ class_Lattices_Olower__semilattice(T_a) % 0.55/0.71 | c_Lattices_Olower__semilattice__class_Oinf(V_x,V_y,T_a) = V_x % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_minus__le__iff_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) % 0.55/0.71 | ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(V_b,T_a),V_a,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_minus__le__iff_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_lessequals(c_HOL_Ouminus__class_Ouminus(V_b,T_a),V_a,T_a) % 0.55/0.71 | ~ c_lessequals(c_HOL_Ouminus__class_Ouminus(V_a,T_a),V_b,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__minus__iff_1,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_lessequals(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_b,c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_le__minus__iff_0,axiom, % 0.55/0.71 ( ~ class_OrderedGroup_Opordered__ab__group__add(T_a) % 0.55/0.71 | c_lessequals(V_b,c_HOL_Ouminus__class_Ouminus(V_a,T_a),T_a) % 0.55/0.71 | ~ c_lessequals(V_a,c_HOL_Ouminus__class_Ouminus(V_b,T_a),T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__less__def_0,axiom, % 0.55/0.71 ( c_lessequals(V_x,V_y,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__sqrt__le__iff_0,axiom, % 0.55/0.71 ( c_lessequals(V_x,V_y,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__sqrt__le__iff_1,axiom, % 0.55/0.71 ( c_lessequals(c_NthRoot_Osqrt(V_x),c_NthRoot_Osqrt(V_y),tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__less__def_2,axiom, % 0.55/0.71 ( c_HOL_Oord__class_Oless(V_x,V_y,tc_RealDef_Oreal) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__add__left__mono_0,axiom, % 0.55/0.71 ( c_lessequals(c_HOL_Oplus__class_Oplus(V_z,V_x,tc_RealDef_Oreal),c_HOL_Oplus__class_Oplus(V_z,V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_exp__le__cancel__iff_1,axiom, % 0.55/0.71 ( c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_Transcendental_Oexp(V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_exp__le__cancel__iff_0,axiom, % 0.55/0.71 ( c_lessequals(V_x,V_y,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(c_Transcendental_Oexp(V_x,tc_RealDef_Oreal),c_Transcendental_Oexp(V_y,tc_RealDef_Oreal),tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_arctan__monotone_H_0,axiom, % 0.55/0.71 ( c_lessequals(c_Transcendental_Oarctan(V_x),c_Transcendental_Oarctan(V_y),tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_abs__le__interval__iff_1,axiom, % 0.55/0.71 ( c_lessequals(V_x,V_r,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(c_HOL_Oabs__class_Oabs(V_x,tc_RealDef_Oreal),V_r,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_xY_0,axiom, % 0.55/0.71 c_HOL_Oord__class_Oless(v_x____,v_Y____,tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_x_0,axiom, % 0.55/0.71 hBOOL(hAPP(v_P,v_x____)) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_COMBI__def__raw_0,axiom, % 0.55/0.71 c_COMBI(v_P,t_a) = v_P ). % 0.55/0.71 % 0.55/0.71 cnf(cls_L_H_0,axiom, % 0.55/0.71 ( c_lessequals(V_x,v_L____,tc_RealDef_Oreal) % 0.55/0.71 | ~ hBOOL(hAPP(v_P,V_x)) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_Y_0,axiom, % 0.55/0.71 ( c_HOL_Oord__class_Oless(V_x,v_Y____,tc_RealDef_Oreal) % 0.55/0.71 | ~ hBOOL(hAPP(v_P,V_x)) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__le__linear_0,axiom, % 0.55/0.71 ( c_lessequals(V_w,V_z,tc_RealDef_Oreal) % 0.55/0.71 | c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_linorder__linear_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Olinorder(T_a) % 0.55/0.71 | c_lessequals(V_y,V_x,T_a) % 0.55/0.71 | c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_xt1_I6_J_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_lessequals(V_z,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_z,V_y,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__trans_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.71 | c_lessequals(V_x,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_z,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__le__refl_0,axiom, % 0.55/0.71 c_lessequals(V_w,V_w,tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__le__trans_0,axiom, % 0.55/0.71 ( c_lessequals(V_i,V_k,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_j,V_k,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_i,V_j,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__eq__iff_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | c_lessequals(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__eq__refl_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Opreorder(T_a) % 0.55/0.71 | c_lessequals(V_x,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__antisym__conv_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__eq__iff_2,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_order__antisym_0,axiom, % 0.55/0.71 ( ~ class_Orderings_Oorder(T_a) % 0.55/0.71 | V_x = V_y % 0.55/0.71 | ~ c_lessequals(V_y,V_x,T_a) % 0.55/0.71 | ~ c_lessequals(V_x,V_y,T_a) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_real__le__antisym_0,axiom, % 0.55/0.71 ( V_z = V_w % 0.55/0.71 | ~ c_lessequals(V_w,V_z,tc_RealDef_Oreal) % 0.55/0.71 | ~ c_lessequals(V_z,V_w,tc_RealDef_Oreal) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_CHAINED_0,axiom, % 0.55/0.71 ( c_HOL_Oord__class_Oless(V_x,v_Y____,tc_RealDef_Oreal) % 0.55/0.71 | ~ hBOOL(hAPP(v_P,V_x)) ) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_conjecture_0,negated_conjecture, % 0.55/0.71 hBOOL(hAPP(v_P,v_xa)) ). % 0.55/0.71 % 0.55/0.71 cnf(cls_conjecture_1,negated_conjecture, % 0.55/0.71 ~ c_lessequals(v_xa,v_Y____,tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(clsarity_RealDef__Oreal__OrderedGroup_Opordered__cancel__ab__semigroup__add,axiom, % 0.55/0.71 class_OrderedGroup_Opordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__semigroup__add__imp__le,axiom, % 0.55/0.71 class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add__meet,axiom, % 0.55/0.71 class_OrderedGroup_Olordered__ab__group__add__meet(tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add__join,axiom, % 0.55/0.71 class_OrderedGroup_Olordered__ab__group__add__join(tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__semigroup__add,axiom, % 0.55/0.71 class_OrderedGroup_Opordered__ab__semigroup__add(tc_RealDef_Oreal) ). % 0.55/0.71 % 0.55/0.71 cnf(clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add__abs,axiom, % 0.55/0.72 class_OrderedGroup_Opordered__ab__group__add__abs(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add__abs,axiom, % 0.55/0.72 class_OrderedGroup_Olordered__ab__group__add__abs(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Ocancel__ab__semigroup__add,axiom, % 0.55/0.72 class_OrderedGroup_Ocancel__ab__semigroup__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Opordered__ab__group__add,axiom, % 0.55/0.72 class_OrderedGroup_Opordered__ab__group__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Olordered__ab__group__add,axiom, % 0.55/0.72 class_OrderedGroup_Olordered__ab__group__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Ocancel__semigroup__add,axiom, % 0.55/0.72 class_OrderedGroup_Ocancel__semigroup__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Ring__and__Field_Ocomm__semiring__1,axiom, % 0.55/0.72 class_Ring__and__Field_Ocomm__semiring__1(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__RealVector_Oreal__normed__vector,axiom, % 0.55/0.72 class_RealVector_Oreal__normed__vector(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Oab__semigroup__add,axiom, % 0.55/0.72 class_OrderedGroup_Oab__semigroup__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Ocomm__monoid__add,axiom, % 0.55/0.72 class_OrderedGroup_Ocomm__monoid__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Ring__and__Field_Oordered__idom,axiom, % 0.55/0.72 class_Ring__and__Field_Oordered__idom(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Lattices_Oupper__semilattice,axiom, % 0.55/0.72 class_Lattices_Oupper__semilattice(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Lattices_Olower__semilattice,axiom, % 0.55/0.72 class_Lattices_Olower__semilattice(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Oab__group__add,axiom, % 0.55/0.72 class_OrderedGroup_Oab__group__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Lattices_Odistrib__lattice,axiom, % 0.55/0.72 class_Lattices_Odistrib__lattice(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__OrderedGroup_Ogroup__add,axiom, % 0.55/0.72 class_OrderedGroup_Ogroup__add(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Ring__and__Field_Oidom,axiom, % 0.55/0.72 class_Ring__and__Field_Oidom(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Orderings_Opreorder,axiom, % 0.55/0.72 class_Orderings_Opreorder(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Orderings_Olinorder,axiom, % 0.55/0.72 class_Orderings_Olinorder(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Lattices_Olattice,axiom, % 0.55/0.72 class_Lattices_Olattice(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Orderings_Oorder,axiom, % 0.55/0.72 class_Orderings_Oorder(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 cnf(clsarity_RealDef__Oreal__Int_Onumber__ring,axiom, % 0.55/0.72 class_Int_Onumber__ring(tc_RealDef_Oreal) ). % 0.55/0.72 % 0.55/0.72 %------------------------------------------------------------------------------ % 0.55/0.72 %------------------------------------------- % 0.55/0.72 % Proof found % 0.55/0.72 % SZS status Theorem for theBenchmark % 0.55/0.72 % SZS output start Proof % 0.55/0.72 %ClaNum:451(EqnAxiom:73) % 0.55/0.72 %VarNum:2594(SingletonVarNum:958) % 0.55/0.72 %MaxLitNum:4 % 0.55/0.72 %MaxfuncDepth:3 % 0.55/0.72 %SharedTerms:39 % 0.55/0.72 %goalClause: 102 106 % 0.55/0.72 %singleGoalClaCount:2 % 0.55/0.72 [74]P1(a1) % 0.55/0.72 [75]P2(a1) % 0.55/0.72 [76]P3(a1) % 0.55/0.72 [77]P4(a1) % 0.55/0.72 [78]P13(a1) % 0.55/0.72 [79]P20(a1) % 0.55/0.72 [80]P5(a1) % 0.55/0.72 [81]P14(a1) % 0.55/0.72 [82]P22(a1) % 0.55/0.72 [83]P23(a1) % 0.55/0.72 [84]P31(a1) % 0.55/0.72 [85]P11(a1) % 0.55/0.72 [86]P12(a1) % 0.55/0.72 [87]P24(a1) % 0.55/0.72 [88]P21(a1) % 0.55/0.72 [89]P15(a1) % 0.55/0.72 [90]P32(a1) % 0.55/0.72 [91]P16(a1) % 0.55/0.72 [92]P17(a1) % 0.55/0.72 [93]P26(a1) % 0.55/0.72 [94]P27(a1) % 0.55/0.72 [95]P28(a1) % 0.55/0.72 [96]P6(a1) % 0.55/0.72 [97]P33(a1) % 0.55/0.72 [98]P18(a1) % 0.55/0.72 [99]P19(a1) % 0.55/0.72 [100]P25(a1) % 0.55/0.72 [104]P7(a19,a20,a1) % 0.55/0.72 [106]~P8(a21,a20,a1) % 0.55/0.72 [101]P34(f2(a17,a19)) % 0.55/0.72 [102]P34(f2(a17,a21)) % 0.55/0.72 [105]P8(x1051,x1051,a1) % 0.55/0.72 [107]~P7(x1071,x1071,a1) % 0.55/0.72 [103]E(f4(f3(x1031,a1),a1),f3(x1031,a1)) % 0.55/0.72 [147]P8(x1471,a18,a1)+~P34(f2(a17,x1471)) % 0.55/0.72 [149]P7(x1491,a20,a1)+~P34(f2(a17,x1491)) % 0.55/0.72 [109]~P9(x1091)+E(f6(f11(x1091),x1091),f12(x1091)) % 0.55/0.72 [110]~P9(x1101)+E(f6(f12(x1101),x1101),f11(x1101)) % 0.55/0.72 [123]~P2(x1232)+P8(x1231,x1231,x1232) % 0.55/0.72 [124]~P3(x1242)+P8(x1241,x1241,x1242) % 0.55/0.72 [144]~P7(x1442,x1442,x1441)+~P2(x1441) % 0.55/0.72 [145]~P7(x1452,x1452,x1451)+~P3(x1451) % 0.55/0.72 [146]~P7(x1462,x1462,x1461)+~P22(x1461) % 0.55/0.72 [155]P8(x1552,x1551,a1)+P8(x1551,x1552,a1) % 0.55/0.72 [176]~P7(x1761,x1762,a1)+P8(x1761,x1762,a1) % 0.55/0.72 [108]E(x1081,x1082)+~E(f5(x1081),f5(x1082)) % 0.55/0.72 [111]E(x1111,x1112)+~E(f3(x1111,a1),f3(x1112,a1)) % 0.55/0.72 [125]~P4(x1252)+E(f9(x1251,x1251,x1252),x1251) % 0.55/0.72 [126]~P12(x1262)+E(f10(x1261,x1261,x1262),x1261) % 0.55/0.72 [127]~P22(x1272)+E(f13(x1271,x1271,x1272),x1271) % 0.55/0.72 [128]~P22(x1282)+E(f14(x1281,x1281,x1282),x1281) % 0.55/0.72 [129]~P30(x1292)+P8(x1291,f12(x1292),x1292) % 0.55/0.72 [130]~P29(x1301)+P8(f11(x1301),x1302,x1301) % 0.55/0.72 [139]~P23(x1392)+P8(x1391,f4(x1391,x1392),x1392) % 0.55/0.72 [156]~P23(x1562)+P8(f6(x1561,x1562),f4(x1561,x1562),x1562) % 0.55/0.72 [194]~P8(x1941,x1942,a1)+P8(f5(x1941),f5(x1942),a1) % 0.55/0.72 [195]~P8(x1951,x1952,a1)+P8(f16(x1951),f16(x1952),a1) % 0.55/0.72 [196]~P7(x1961,x1962,a1)+P7(f5(x1961),f5(x1962),a1) % 0.55/0.72 [197]~P7(x1971,x1972,a1)+P7(f16(x1971),f16(x1972),a1) % 0.55/0.72 [210]P8(x2101,x2102,a1)+~P8(f5(x2101),f5(x2102),a1) % 0.55/0.72 [211]P7(x2111,x2112,a1)+~P7(f5(x2111),f5(x2112),a1) % 0.55/0.72 [231]P8(x2311,x2312,a1)+~P8(f4(x2311,a1),x2312,a1) % 0.55/0.72 [249]~P8(x2491,x2492,a1)+P8(f3(x2491,a1),f3(x2492,a1),a1) % 0.55/0.72 [250]~P7(x2501,x2502,a1)+P7(f3(x2501,a1),f3(x2502,a1),a1) % 0.55/0.72 [260]P8(x2601,x2602,a1)+~P8(f3(x2601,a1),f3(x2602,a1),a1) % 0.55/0.72 [261]P7(x2611,x2612,a1)+~P7(f3(x2611,a1),f3(x2612,a1),a1) % 0.55/0.72 [115]~P14(x1152)+E(f6(f6(x1151,x1152),x1152),x1151) % 0.55/0.72 [116]~P9(x1162)+E(f6(f6(x1161,x1162),x1162),x1161) % 0.55/0.72 [119]~P1(x1192)+E(f4(f15(x1191,x1192),a1),f15(x1191,x1192)) % 0.55/0.72 [120]~P1(x1202)+E(f15(f6(x1201,x1202),x1202),f15(x1201,x1202)) % 0.55/0.72 [121]~P23(x1212)+E(f4(f6(x1211,x1212),x1212),f4(x1211,x1212)) % 0.55/0.72 [122]~P23(x1222)+E(f4(f4(x1221,x1222),x1222),f4(x1221,x1222)) % 0.55/0.72 [131]~P10(x1312)+E(f9(x1311,f11(x1312),x1312),x1311) % 0.55/0.72 [132]~P10(x1322)+E(f10(x1321,f12(x1322),x1322),x1321) % 0.55/0.72 [133]~P10(x1331)+E(f9(f11(x1331),x1332,x1331),x1332) % 0.55/0.72 [134]~P10(x1341)+E(f10(f12(x1341),x1342,x1341),x1342) % 0.55/0.72 [135]~P10(x1352)+E(f9(x1351,f12(x1352),x1352),f12(x1352)) % 0.55/0.72 [136]~P10(x1362)+E(f10(x1361,f11(x1362),x1362),f11(x1362)) % 0.55/0.72 [137]~P10(x1371)+E(f9(f12(x1371),x1372,x1371),f12(x1371)) % 0.55/0.72 [138]~P10(x1381)+E(f10(f11(x1381),x1382,x1381),f11(x1381)) % 0.55/0.72 [140]~P9(x1402)+E(f9(x1401,f6(x1401,x1402),x1402),f12(x1402)) % 0.55/0.72 [141]~P9(x1412)+E(f10(x1411,f6(x1411,x1412),x1412),f11(x1412)) % 0.55/0.72 [142]~P9(x1422)+E(f9(f6(x1421,x1422),x1421,x1422),f12(x1422)) % 0.55/0.72 [143]~P9(x1432)+E(f10(f6(x1431,x1432),x1431,x1432),f11(x1432)) % 0.55/0.72 [150]~P21(x1502)+E(f9(x1501,f6(x1501,x1502),x1502),f4(x1501,x1502)) % 0.55/0.72 [157]~P15(x1573)+E(f7(x1571,x1572,x1573),f7(x1572,x1571,x1573)) % 0.55/0.72 [159]~P32(x1593)+E(f7(x1591,x1592,x1593),f7(x1592,x1591,x1593)) % 0.55/0.72 [160]~P4(x1603)+E(f9(x1601,x1602,x1603),f9(x1602,x1601,x1603)) % 0.55/0.72 [161]~P11(x1613)+E(f9(x1611,x1612,x1613),f9(x1612,x1611,x1613)) % 0.55/0.72 [162]~P11(x1623)+E(f10(x1621,x1622,x1623),f10(x1622,x1621,x1623)) % 0.55/0.72 [163]~P12(x1633)+E(f10(x1631,x1632,x1633),f10(x1632,x1631,x1633)) % 0.55/0.72 [164]~P22(x1643)+E(f13(x1641,x1642,x1643),f13(x1642,x1641,x1643)) % 0.55/0.72 [165]~P22(x1653)+E(f14(x1651,x1652,x1653),f14(x1652,x1651,x1653)) % 0.55/0.72 [212]~P4(x2123)+P8(x2121,f9(x2122,x2121,x2123),x2123) % 0.55/0.72 [213]~P11(x2133)+P8(x2131,f9(x2132,x2131,x2133),x2133) % 0.55/0.72 [214]~P4(x2143)+P8(x2141,f9(x2141,x2142,x2143),x2143) % 0.55/0.72 [215]~P11(x2153)+P8(x2151,f9(x2151,x2152,x2153),x2153) % 0.55/0.72 [216]~P22(x2163)+P8(x2161,f14(x2162,x2161,x2163),x2163) % 0.55/0.72 [217]~P22(x2173)+P8(x2171,f14(x2171,x2172,x2173),x2173) % 0.55/0.72 [218]~P11(x2183)+P8(f10(x2181,x2182,x2183),x2182,x2183) % 0.55/0.72 [219]~P12(x2193)+P8(f10(x2191,x2192,x2193),x2192,x2193) % 0.55/0.72 [220]~P11(x2203)+P8(f10(x2201,x2202,x2203),x2201,x2203) % 0.55/0.72 [221]~P12(x2213)+P8(f10(x2211,x2212,x2213),x2211,x2213) % 0.55/0.72 [222]~P22(x2223)+P8(f13(x2221,x2222,x2223),x2222,x2223) % 0.55/0.72 [223]~P22(x2233)+P8(f13(x2231,x2232,x2233),x2231,x2233) % 0.55/0.72 [390]~P8(x3902,x3903,a1)+P8(f7(x3901,x3902,a1),f7(x3901,x3903,a1),a1) % 0.55/0.72 [178]~P14(x1783)+E(f7(x1781,f6(x1782,x1783),x1783),f8(x1781,x1782,x1783)) % 0.55/0.72 [180]~P16(x1803)+E(f7(x1801,f6(x1802,x1803),x1803),f8(x1801,x1802,x1803)) % 0.55/0.72 [181]~P6(x1813)+E(f7(x1811,f6(x1812,x1813),x1813),f8(x1811,x1812,x1813)) % 0.55/0.72 [182]~P9(x1823)+E(f10(x1821,f6(x1822,x1823),x1823),f8(x1821,x1822,x1823)) % 0.55/0.72 [183]~P14(x1833)+E(f8(x1831,f6(x1832,x1833),x1833),f7(x1831,x1832,x1833)) % 0.55/0.72 [224]~P11(x2243)+E(f9(x2241,f10(x2241,x2242,x2243),x2243),x2241) % 0.55/0.72 [225]~P11(x2253)+E(f10(x2251,f9(x2251,x2252,x2253),x2253),x2251) % 0.55/0.72 [226]~P22(x2263)+E(f13(x2261,f14(x2261,x2262,x2263),x2263),x2261) % 0.55/0.72 [227]~P22(x2273)+E(f14(x2271,f13(x2271,x2272,x2273),x2273),x2271) % 0.55/0.72 [228]~P14(x2283)+E(f8(f7(x2281,x2282,x2283),x2282,x2283),x2281) % 0.55/0.72 [229]~P14(x2293)+E(f7(f8(x2291,x2292,x2293),x2292,x2293),x2291) % 0.55/0.72 [248]~P16(x2483)+E(f6(f8(x2481,x2482,x2483),x2483),f8(x2482,x2481,x2483)) % 0.55/0.72 [254]~P16(x2542)+E(f7(f6(x2541,x2542),f7(x2543,x2541,x2542),x2542),x2543) % 0.55/0.72 [255]~P14(x2552)+E(f7(f6(x2551,x2552),f7(x2551,x2553,x2552),x2552),x2553) % 0.55/0.72 [274]~P4(x2743)+E(f9(x2741,f9(x2741,x2742,x2743),x2743),f9(x2741,x2742,x2743)) % 0.55/0.72 [275]~P11(x2753)+E(f9(x2751,f9(x2751,x2752,x2753),x2753),f9(x2751,x2752,x2753)) % 0.55/0.72 [276]~P11(x2763)+E(f10(x2761,f10(x2761,x2762,x2763),x2763),f10(x2761,x2762,x2763)) % 0.55/0.72 [277]~P12(x2773)+E(f10(x2771,f10(x2771,x2772,x2773),x2773),f10(x2771,x2772,x2773)) % 0.55/0.72 [278]~P22(x2783)+E(f13(x2781,f13(x2781,x2782,x2783),x2783),f13(x2781,x2782,x2783)) % 0.55/0.72 [279]~P22(x2793)+E(f14(x2791,f14(x2791,x2792,x2793),x2793),f14(x2791,x2792,x2793)) % 0.55/0.72 [282]~P14(x2822)+E(f7(f6(x2821,x2822),f6(x2823,x2822),x2822),f6(f7(x2823,x2821,x2822),x2822)) % 0.55/0.72 [283]~P16(x2832)+E(f7(f6(x2831,x2832),f6(x2833,x2832),x2832),f6(f7(x2831,x2833,x2832),x2832)) % 0.55/0.72 [284]~P13(x2842)+E(f10(f6(x2841,x2842),f6(x2843,x2842),x2842),f6(f9(x2841,x2843,x2842),x2842)) % 0.55/0.72 [285]~P9(x2852)+E(f10(f6(x2851,x2852),f6(x2853,x2852),x2852),f6(f9(x2851,x2853,x2852),x2852)) % 0.55/0.72 [286]~P13(x2862)+E(f9(f6(x2861,x2862),f6(x2863,x2862),x2862),f6(f10(x2861,x2863,x2862),x2862)) % 0.55/0.72 [287]~P9(x2872)+E(f9(f6(x2871,x2872),f6(x2873,x2872),x2872),f6(f10(x2871,x2873,x2872),x2872)) % 0.55/0.72 [288]~P16(x2882)+E(f8(f6(x2881,x2882),f6(x2883,x2882),x2882),f6(f8(x2881,x2883,x2882),x2882)) % 0.55/0.72 [297]~P1(x2973)+E(f15(f8(x2971,x2972,x2973),x2973),f15(f8(x2972,x2971,x2973),x2973)) % 0.55/0.72 [298]~P23(x2983)+E(f4(f8(x2981,x2982,x2983),x2983),f4(f8(x2982,x2981,x2983),x2983)) % 0.55/0.72 [353]~P13(x3533)+E(f7(f9(x3531,x3532,x3533),f10(x3531,x3532,x3533),x3533),f7(x3531,x3532,x3533)) % 0.55/0.72 [433]~P1(x4333)+P8(f15(f8(x4331,x4332,x4333),x4333),f7(f15(x4331,x4333),f15(x4332,x4333),a1),a1) % 0.55/0.72 [434]~P1(x4343)+P8(f15(f7(x4341,x4342,x4343),x4343),f7(f15(x4341,x4343),f15(x4342,x4343),a1),a1) % 0.55/0.72 [436]~P23(x4363)+P8(f4(f8(x4361,x4362,x4363),x4363),f7(f4(x4361,x4363),f4(x4362,x4363),x4363),x4363) % 0.55/0.72 [437]~P23(x4373)+P8(f4(f7(x4371,x4372,x4373),x4373),f7(f4(x4371,x4373),f4(x4372,x4373),x4373),x4373) % 0.55/0.72 [438]~P23(x4382)+P8(f8(f4(x4381,x4382),f4(x4383,x4382),x4382),f4(f8(x4381,x4383,x4382),x4382),x4382) % 0.55/0.72 [273]~P14(x2732)+E(f7(x2731,f7(f6(x2731,x2732),x2733,x2732),x2732),x2733) % 0.55/0.72 [324]~P13(x3242)+E(f6(f10(f6(x3241,x3242),f6(x3243,x3242),x3242),x3242),f9(x3241,x3243,x3242)) % 0.55/0.72 [325]~P13(x3252)+E(f6(f9(f6(x3251,x3252),f6(x3253,x3252),x3252),x3252),f10(x3251,x3253,x3252)) % 0.55/0.72 [375]~P23(x3752)+E(f4(f7(f4(x3751,x3752),f4(x3753,x3752),x3752),x3752),f7(f4(x3751,x3752),f4(x3753,x3752),x3752)) % 0.55/0.72 [444]~P23(x4442)+P8(f4(f8(f4(x4441,x4442),f4(x4443,x4442),x4442),x4442),f4(f8(x4441,x4443,x4442),x4442),x4442) % 0.55/0.72 [354]~P15(x3544)+E(f7(x3541,f7(x3542,x3543,x3544),x3544),f7(x3542,f7(x3541,x3543,x3544),x3544)) % 0.55/0.72 [355]~P32(x3554)+E(f7(x3551,f7(x3552,x3553,x3554),x3554),f7(x3552,f7(x3551,x3553,x3554),x3554)) % 0.55/0.72 [356]~P16(x3564)+E(f7(x3561,f7(x3562,x3563,x3564),x3564),f7(x3562,f7(x3561,x3563,x3564),x3564)) % 0.55/0.72 [357]~P4(x3574)+E(f9(x3571,f9(x3572,x3573,x3574),x3574),f9(x3572,f9(x3571,x3573,x3574),x3574)) % 0.55/0.72 [358]~P11(x3584)+E(f9(x3581,f9(x3582,x3583,x3584),x3584),f9(x3582,f9(x3581,x3583,x3584),x3584)) % 0.55/0.72 [359]~P11(x3594)+E(f10(x3591,f10(x3592,x3593,x3594),x3594),f10(x3592,f10(x3591,x3593,x3594),x3594)) % 0.55/0.72 [360]~P12(x3604)+E(f10(x3601,f10(x3602,x3603,x3604),x3604),f10(x3602,f10(x3601,x3603,x3604),x3604)) % 0.55/0.72 [361]~P22(x3614)+E(f13(x3611,f13(x3612,x3613,x3614),x3614),f13(x3612,f13(x3611,x3613,x3614),x3614)) % 0.55/0.72 [362]~P22(x3624)+E(f14(x3621,f14(x3622,x3623,x3624),x3624),f14(x3622,f14(x3621,x3623,x3624),x3624)) % 0.55/0.72 [365]~P15(x3653)+E(f7(f7(x3651,x3652,x3653),x3654,x3653),f7(x3651,f7(x3652,x3654,x3653),x3653)) % 0.55/0.72 [366]~P32(x3663)+E(f7(f7(x3661,x3662,x3663),x3664,x3663),f7(x3661,f7(x3662,x3664,x3663),x3663)) % 0.55/0.72 [367]~P17(x3673)+E(f7(f7(x3671,x3672,x3673),x3674,x3673),f7(x3671,f7(x3672,x3674,x3673),x3673)) % 0.55/0.72 [368]~P4(x3683)+E(f9(f9(x3681,x3682,x3683),x3684,x3683),f9(x3681,f9(x3682,x3684,x3683),x3683)) % 0.55/0.72 [369]~P11(x3693)+E(f9(f9(x3691,x3692,x3693),x3694,x3693),f9(x3691,f9(x3692,x3694,x3693),x3693)) % 0.55/0.72 [370]~P11(x3703)+E(f10(f10(x3701,x3702,x3703),x3704,x3703),f10(x3701,f10(x3702,x3704,x3703),x3703)) % 0.55/0.72 [371]~P12(x3713)+E(f10(f10(x3711,x3712,x3713),x3714,x3713),f10(x3711,f10(x3712,x3714,x3713),x3713)) % 0.55/0.72 [372]~P22(x3723)+E(f13(f13(x3721,x3722,x3723),x3724,x3723),f13(x3721,f13(x3722,x3724,x3723),x3723)) % 0.55/0.72 [373]~P22(x3733)+E(f14(f14(x3731,x3732,x3733),x3734,x3733),f14(x3731,f14(x3732,x3734,x3733),x3733)) % 0.55/0.72 [374]~P32(x3743)+E(f7(f7(x3741,x3742,x3743),x3744,x3743),f7(f7(x3741,x3744,x3743),x3742,x3743)) % 0.55/0.72 [404]~P13(x4043)+E(f9(f7(x4041,x4042,x4043),f7(x4041,x4044,x4043),x4043),f7(x4041,f9(x4042,x4044,x4043),x4043)) % 0.55/0.72 [405]~P20(x4053)+E(f9(f7(x4051,x4052,x4053),f7(x4051,x4054,x4053),x4053),f7(x4051,f9(x4052,x4054,x4053),x4053)) % 0.55/0.72 [406]~P13(x4063)+E(f10(f7(x4061,x4062,x4063),f7(x4061,x4064,x4063),x4063),f7(x4061,f10(x4062,x4064,x4063),x4063)) % 0.55/0.72 [407]~P25(x4073)+E(f10(f7(x4071,x4072,x4073),f7(x4071,x4074,x4073),x4073),f7(x4071,f10(x4072,x4074,x4073),x4073)) % 0.55/0.72 [408]~P5(x4083)+E(f10(f9(x4081,x4082,x4083),f9(x4081,x4084,x4083),x4083),f9(x4081,f10(x4082,x4084,x4083),x4083)) % 0.55/0.72 [409]~P5(x4093)+E(f9(f10(x4091,x4092,x4093),f10(x4091,x4094,x4093),x4093),f10(x4091,f9(x4092,x4094,x4093),x4093)) % 0.55/0.72 [410]~P22(x4103)+E(f14(f13(x4101,x4102,x4103),f13(x4101,x4104,x4103),x4103),f13(x4101,f14(x4102,x4104,x4103),x4103)) % 0.55/0.72 [411]~P22(x4113)+E(f13(f14(x4111,x4112,x4113),f14(x4111,x4114,x4113),x4113),f14(x4111,f13(x4112,x4114,x4113),x4113)) % 0.55/0.72 [412]~P24(x4123)+E(f13(f8(x4121,x4122,x4123),f8(x4124,x4122,x4123),x4123),f8(f13(x4121,x4124,x4123),x4122,x4123)) % 0.55/0.72 [413]~P24(x4133)+E(f14(f8(x4131,x4132,x4133),f8(x4134,x4132,x4133),x4133),f8(f14(x4131,x4134,x4133),x4132,x4133)) % 0.55/0.72 [414]~P13(x4143)+E(f9(f7(x4141,x4142,x4143),f7(x4144,x4142,x4143),x4143),f7(f9(x4141,x4144,x4143),x4142,x4143)) % 0.55/0.72 [415]~P20(x4153)+E(f9(f7(x4151,x4152,x4153),f7(x4154,x4152,x4153),x4153),f7(f9(x4151,x4154,x4153),x4152,x4153)) % 0.55/0.72 [416]~P13(x4163)+E(f10(f7(x4161,x4162,x4163),f7(x4164,x4162,x4163),x4163),f7(f10(x4161,x4164,x4163),x4162,x4163)) % 0.55/0.72 [417]~P25(x4173)+E(f10(f7(x4171,x4172,x4173),f7(x4174,x4172,x4173),x4173),f7(f10(x4171,x4174,x4173),x4172,x4173)) % 0.55/0.72 [418]~P28(x4183)+E(f13(f7(x4181,x4182,x4183),f7(x4184,x4182,x4183),x4183),f7(f13(x4181,x4184,x4183),x4182,x4183)) % 0.55/0.72 [419]~P28(x4193)+E(f14(f7(x4191,x4192,x4193),f7(x4194,x4192,x4193),x4193),f7(f14(x4191,x4194,x4193),x4192,x4193)) % 0.55/0.72 [420]~P5(x4203)+E(f10(f9(x4201,x4202,x4203),f9(x4204,x4202,x4203),x4203),f9(f10(x4201,x4204,x4203),x4202,x4203)) % 0.55/0.72 [421]~P5(x4213)+E(f9(f10(x4211,x4212,x4213),f10(x4214,x4212,x4213),x4213),f10(f9(x4211,x4214,x4213),x4212,x4213)) % 0.55/0.72 [422]~P22(x4223)+E(f14(f13(x4221,x4222,x4223),f13(x4224,x4222,x4223),x4223),f13(f14(x4221,x4224,x4223),x4222,x4223)) % 0.55/0.72 [423]~P22(x4233)+E(f13(f14(x4231,x4232,x4233),f14(x4234,x4232,x4233),x4233),f14(f13(x4231,x4234,x4233),x4232,x4233)) % 0.55/0.72 [446]~P11(x4464)+P8(f9(x4461,f10(x4462,x4463,x4464),x4464),f10(f9(x4461,x4462,x4464),f9(x4461,x4463,x4464),x4464),x4464) % 0.55/0.72 [447]~P22(x4474)+P8(f14(x4471,f13(x4472,x4473,x4474),x4474),f13(f14(x4471,x4472,x4474),f14(x4471,x4473,x4474),x4474),x4474) % 0.55/0.72 [448]~P11(x4483)+P8(f9(f10(x4481,x4482,x4483),f10(x4481,x4484,x4483),x4483),f10(x4481,f9(x4482,x4484,x4483),x4483),x4483) % 0.55/0.72 [449]~P22(x4493)+P8(f14(f13(x4491,x4492,x4493),f13(x4491,x4494,x4493),x4493),f13(x4491,f14(x4492,x4494,x4493),x4493),x4493) % 0.55/0.72 [439]~P16(x4393)+E(f8(f7(x4391,x4392,x4393),f7(x4394,x4395,x4393),x4393),f7(f8(x4391,x4394,x4393),f8(x4392,x4395,x4393),x4393)) % 0.55/0.72 [440]~P32(x4403)+E(f7(f7(x4401,x4402,x4403),f7(x4404,x4405,x4403),x4403),f7(f7(x4401,x4404,x4403),f7(x4402,x4405,x4403),x4403)) % 0.55/0.72 [450]~P1(x4503)+P8(f15(f8(f7(x4501,x4502,x4503),f7(x4504,x4505,x4503),x4503),x4503),f7(f15(f8(x4501,x4504,x4503),x4503),f15(f8(x4502,x4505,x4503),x4503),a1),a1) % 0.55/0.72 [451]~P23(x4513)+P8(f4(f8(f7(x4511,x4512,x4513),f7(x4514,x4515,x4513),x4513),x4513),f7(f4(f8(x4511,x4514,x4513),x4513),f4(f8(x4512,x4515,x4513),x4513),x4513),x4513) % 0.55/0.72 [177]E(x1771,x1772)+P7(x1771,x1772,a1)+~P8(x1771,x1772,a1) % 0.55/0.72 [230]E(x2301,x2302)+~P8(x2302,x2301,a1)+~P8(x2301,x2302,a1) % 0.55/0.72 [166]P8(x1662,x1661,x1663)+~P22(x1663)+P8(x1661,x1662,x1663) % 0.55/0.72 [169]P7(x1692,x1691,x1693)+~P22(x1693)+P8(x1691,x1692,x1693) % 0.55/0.72 [184]~P2(x1843)+~P7(x1841,x1842,x1843)+P8(x1841,x1842,x1843) % 0.55/0.72 [185]~P3(x1853)+~P7(x1851,x1852,x1853)+P8(x1851,x1852,x1853) % 0.55/0.72 [232]~P7(x2323,x2322,x2321)+~P2(x2321)+~P8(x2322,x2323,x2321) % 0.55/0.72 [234]~P7(x2343,x2342,x2341)+~P2(x2341)+~P7(x2342,x2343,x2341) % 0.55/0.72 [235]~P7(x2353,x2352,x2351)+~P3(x2351)+~P7(x2352,x2353,x2351) % 0.55/0.72 [237]~P7(x2373,x2372,x2371)+~P22(x2371)+~P8(x2372,x2373,x2371) % 0.55/0.72 [239]~P7(x2393,x2392,x2391)+~P22(x2391)+~P7(x2392,x2393,x2391) % 0.55/0.72 [272]~P8(x2721,x2723,a1)+P8(x2721,x2722,a1)+~P8(x2723,x2722,a1) % 0.55/0.72 [117]~P14(x1173)+E(x1171,x1172)+~E(f6(x1171,x1173),f6(x1172,x1173)) % 0.55/0.72 [118]~P9(x1183)+E(x1181,x1182)+~E(f6(x1181,x1183),f6(x1182,x1183)) % 0.55/0.72 [151]~P10(x1512)+~E(f9(x1513,x1511,x1512),f11(x1512))+E(x1511,f11(x1512)) % 0.55/0.72 [152]~P10(x1522)+~E(f10(x1523,x1521,x1522),f12(x1522))+E(x1521,f12(x1522)) % 0.55/0.72 [153]~P10(x1532)+~E(f9(x1531,x1533,x1532),f11(x1532))+E(x1531,f11(x1532)) % 0.55/0.72 [154]~P10(x1542)+~E(f10(x1541,x1543,x1542),f12(x1542))+E(x1541,f12(x1542)) % 0.55/0.72 [186]~P4(x1863)+~P8(x1861,x1862,x1863)+E(f9(x1861,x1862,x1863),x1862) % 0.55/0.72 [187]~P4(x1873)+~P8(x1872,x1871,x1873)+E(f9(x1871,x1872,x1873),x1871) % 0.55/0.72 [188]~P12(x1883)+~P8(x1882,x1881,x1883)+E(f10(x1881,x1882,x1883),x1882) % 0.55/0.72 [189]~P12(x1893)+~P8(x1891,x1892,x1893)+E(f10(x1891,x1892,x1893),x1891) % 0.55/0.72 [190]~P22(x1903)+~P8(x1902,x1901,x1903)+E(f13(x1901,x1902,x1903),x1902) % 0.55/0.72 [191]~P22(x1913)+~P8(x1911,x1912,x1913)+E(f13(x1911,x1912,x1913),x1911) % 0.55/0.72 [192]~P22(x1923)+~P8(x1921,x1922,x1923)+E(f14(x1921,x1922,x1923),x1922) % 0.55/0.72 [193]~P22(x1933)+~P8(x1932,x1931,x1933)+E(f14(x1931,x1932,x1933),x1931) % 0.55/0.72 [198]~P4(x1983)+P8(x1981,x1982,x1983)+~E(f9(x1981,x1982,x1983),x1982) % 0.55/0.72 [199]~P12(x1993)+P8(x1991,x1992,x1993)+~E(f10(x1991,x1992,x1993),x1991) % 0.55/0.72 [200]~P22(x2003)+P8(x2001,x2002,x2003)+~E(f13(x2001,x2002,x2003),x2001) % 0.55/0.72 [201]~P22(x2013)+P8(x2011,x2012,x2013)+~E(f14(x2011,x2012,x2013),x2012) % 0.55/0.72 [252]~P23(x2523)+P8(x2521,x2522,x2523)+~P8(f4(x2521,x2523),x2522,x2523) % 0.55/0.72 [253]~P31(x2533)+P7(x2531,x2532,x2533)+~P7(f4(x2531,x2533),x2532,x2533) % 0.55/0.72 [256]~P24(x2562)+~P8(x2563,x2561,x2562)+P8(f6(x2561,x2562),f6(x2563,x2562),x2562) % 0.55/0.72 [257]~P24(x2572)+~P7(x2573,x2571,x2572)+P7(f6(x2571,x2572),f6(x2573,x2572),x2572) % 0.55/0.72 [263]~P24(x2633)+~P8(x2632,f6(x2631,x2633),x2633)+P8(x2631,f6(x2632,x2633),x2633) % 0.55/0.72 [265]~P24(x2653)+~P7(x2652,f6(x2651,x2653),x2653)+P7(x2651,f6(x2652,x2653),x2653) % 0.55/0.72 [266]~P23(x2662)+~P8(f4(x2661,x2662),x2663,x2662)+P8(f6(x2661,x2662),x2663,x2662) % 0.55/0.72 [268]~P24(x2682)+~P8(f6(x2683,x2682),x2681,x2682)+P8(f6(x2681,x2682),x2683,x2682) % 0.55/0.72 [269]~P31(x2692)+~P7(f4(x2691,x2692),x2693,x2692)+P7(f6(x2691,x2692),x2693,x2692) % 0.55/0.72 [271]~P24(x2712)+~P7(f6(x2713,x2712),x2711,x2712)+P7(f6(x2711,x2712),x2713,x2712) % 0.55/0.72 [280]~P24(x2803)+P8(x2801,x2802,x2803)+~P8(f6(x2802,x2803),f6(x2801,x2803),x2803) % 0.55/0.72 [281]~P24(x2813)+P7(x2811,x2812,x2813)+~P7(f6(x2812,x2813),f6(x2811,x2813),x2813) % 0.55/0.72 [240]~P16(x2404)+E(x2401,x2402)+~E(f8(x2403,x2403,x2404),f8(x2401,x2402,x2404)) % 0.55/0.72 [241]~P18(x2414)+E(x2411,x2412)+~E(f7(x2413,x2411,x2414),f7(x2413,x2412,x2414)) % 0.55/0.72 [242]~P19(x2424)+E(x2421,x2422)+~E(f7(x2423,x2421,x2424),f7(x2423,x2422,x2424)) % 0.55/0.72 [243]~P19(x2434)+E(x2431,x2432)+~E(f7(x2431,x2433,x2434),f7(x2432,x2433,x2434)) % 0.55/0.72 [244]~P16(x2443)+E(x2441,x2442)+~E(f8(x2441,x2442,x2443),f8(x2444,x2444,x2443)) % 0.55/0.72 [299]~P4(x2994)+~P8(x2991,x2993,x2994)+P8(x2991,f9(x2992,x2993,x2994),x2994) % 0.55/0.72 [300]~P4(x3004)+~P8(x3001,x3002,x3004)+P8(x3001,f9(x3002,x3003,x3004),x3004) % 0.55/0.72 [302]~P22(x3024)+~P8(x3021,x3023,x3024)+P8(x3021,f14(x3022,x3023,x3024),x3024) % 0.55/0.72 [304]~P22(x3044)+~P8(x3041,x3042,x3044)+P8(x3041,f14(x3042,x3043,x3044),x3044) % 0.55/0.72 [305]~P4(x3054)+~P7(x3051,x3053,x3054)+P7(x3051,f9(x3052,x3053,x3054),x3054) % 0.55/0.72 [306]~P4(x3064)+~P7(x3061,x3062,x3064)+P7(x3061,f9(x3062,x3063,x3064),x3064) % 0.55/0.72 [308]~P22(x3084)+~P7(x3081,x3083,x3084)+P7(x3081,f14(x3082,x3083,x3084),x3084) % 0.55/0.72 [310]~P22(x3104)+~P7(x3101,x3102,x3104)+P7(x3101,f14(x3102,x3103,x3104),x3104) % 0.55/0.72 [311]~P12(x3113)+~P8(x3112,x3114,x3113)+P8(f10(x3111,x3112,x3113),x3114,x3113) % 0.55/0.72 [312]~P12(x3123)+~P8(x3121,x3124,x3123)+P8(f10(x3121,x3122,x3123),x3124,x3123) % 0.55/0.72 [314]~P22(x3143)+~P8(x3142,x3144,x3143)+P8(f13(x3141,x3142,x3143),x3144,x3143) % 0.55/0.72 [316]~P22(x3163)+~P8(x3161,x3164,x3163)+P8(f13(x3161,x3162,x3163),x3164,x3163) % 0.55/0.72 [317]~P12(x3173)+~P7(x3172,x3174,x3173)+P7(f10(x3171,x3172,x3173),x3174,x3173) % 0.55/0.72 [318]~P12(x3183)+~P7(x3181,x3184,x3183)+P7(f10(x3181,x3182,x3183),x3184,x3183) % 0.55/0.72 [320]~P22(x3203)+~P7(x3202,x3204,x3203)+P7(f13(x3201,x3202,x3203),x3204,x3203) % 0.55/0.72 [322]~P22(x3223)+~P7(x3221,x3224,x3223)+P7(f13(x3221,x3222,x3223),x3224,x3223) % 0.55/0.72 [330]~P22(x3303)+P8(x3301,x3302,x3303)+~P8(x3301,f13(x3304,x3302,x3303),x3303) % 0.55/0.72 [332]~P22(x3323)+P8(x3321,x3322,x3323)+~P8(x3321,f13(x3322,x3324,x3323),x3323) % 0.55/0.72 [334]~P12(x3343)+P8(x3341,x3342,x3343)+~P8(x3341,f10(x3344,x3342,x3343),x3343) % 0.55/0.72 [336]~P12(x3363)+P8(x3361,x3362,x3363)+~P8(x3361,f10(x3362,x3364,x3363),x3363) % 0.55/0.72 [337]~P22(x3373)+P7(x3371,x3372,x3373)+~P7(x3371,f13(x3374,x3372,x3373),x3373) % 0.55/0.72 [338]~P22(x3383)+P7(x3381,x3382,x3383)+~P7(x3381,f13(x3382,x3384,x3383),x3383) % 0.55/0.72 [340]~P4(x3403)+P8(x3401,x3402,x3403)+~P8(f9(x3404,x3401,x3403),x3402,x3403) % 0.55/0.72 [342]~P4(x3423)+P8(x3421,x3422,x3423)+~P8(f9(x3421,x3424,x3423),x3422,x3423) % 0.55/0.72 [344]~P22(x3443)+P8(x3441,x3442,x3443)+~P8(f14(x3444,x3441,x3443),x3442,x3443) % 0.55/0.72 [346]~P22(x3463)+P8(x3461,x3462,x3463)+~P8(f14(x3461,x3464,x3463),x3462,x3463) % 0.55/0.72 [347]~P22(x3473)+P7(x3471,x3472,x3473)+~P7(f14(x3474,x3471,x3473),x3472,x3473) % 0.55/0.72 [348]~P22(x3483)+P7(x3481,x3482,x3483)+~P7(f14(x3481,x3484,x3483),x3482,x3483) % 0.55/0.72 [391]~P27(x3913)+~P8(x3911,x3914,x3913)+P8(f7(x3911,x3912,x3913),f7(x3914,x3912,x3913),x3913) % 0.55/0.72 [392]~P28(x3923)+~P8(x3921,x3924,x3923)+P8(f7(x3921,x3922,x3923),f7(x3924,x3922,x3923),x3923) % 0.55/0.72 [393]~P27(x3933)+~P8(x3932,x3934,x3933)+P8(f7(x3931,x3932,x3933),f7(x3931,x3934,x3933),x3933) % 0.55/0.72 [394]~P28(x3943)+~P8(x3942,x3944,x3943)+P8(f7(x3941,x3942,x3943),f7(x3941,x3944,x3943),x3943) % 0.55/0.72 [395]~P26(x3953)+~P7(x3951,x3954,x3953)+P7(f7(x3951,x3952,x3953),f7(x3954,x3952,x3953),x3953) % 0.55/0.72 [396]~P28(x3963)+~P7(x3961,x3964,x3963)+P7(f7(x3961,x3962,x3963),f7(x3964,x3962,x3963),x3963) % 0.55/0.72 [397]~P26(x3973)+~P7(x3972,x3974,x3973)+P7(f7(x3971,x3972,x3973),f7(x3971,x3974,x3973),x3973) % 0.55/0.72 [398]~P28(x3983)+~P7(x3982,x3984,x3983)+P7(f7(x3981,x3982,x3983),f7(x3981,x3984,x3983),x3983) % 0.55/0.72 [429]~P28(x4293)+P8(x4291,x4292,x4293)+~P8(f7(x4294,x4291,x4293),f7(x4294,x4292,x4293),x4293) % 0.55/0.72 [430]~P28(x4303)+P8(x4301,x4302,x4303)+~P8(f7(x4301,x4304,x4303),f7(x4302,x4304,x4303),x4303) % 0.55/0.72 [431]~P28(x4313)+P7(x4311,x4312,x4313)+~P7(f7(x4314,x4311,x4313),f7(x4314,x4312,x4313),x4313) % 0.55/0.72 [432]~P28(x4323)+P7(x4321,x4322,x4323)+~P7(f7(x4321,x4324,x4323),f7(x4322,x4324,x4323),x4323) % 0.55/0.72 [323]~P16(x3233)+E(x3231,f6(x3232,x3233))+~E(f7(x3231,f7(x3234,x3232,x3233),x3233),x3234) % 0.55/0.72 [428]~P21(x4284)+~P8(f7(x4281,x4283,x4284),x4282,x4284)+P8(x4281,f7(x4282,f4(x4283,x4284),x4284),x4284) % 0.55/0.72 [441]~P31(x4414)+P7(x4411,f7(x4412,x4413,x4414),x4414)+~P7(f4(f8(x4411,x4412,x4414),x4414),x4413,x4414) % 0.55/0.72 [442]~P31(x4423)+P7(f8(x4421,x4422,x4423),x4424,x4423)+~P7(f4(f8(x4424,x4421,x4423),x4423),x4422,x4423) % 0.55/0.72 [403]~P16(x4033)+E(f7(x4031,x4032,x4033),x4034)+~E(f7(x4031,f7(x4035,x4032,x4033),x4033),f7(x4035,x4034,x4033)) % 0.55/0.72 [174]P7(x1741,x1742,x1743)+~P22(x1743)+E(x1741,x1742)+P7(x1742,x1741,x1743) % 0.55/0.72 [175]P7(x1751,x1752,x1753)+~P31(x1753)+E(x1751,x1752)+P7(x1752,x1751,x1753) % 0.55/0.72 [207]~P3(x2073)+~P8(x2071,x2072,x2073)+E(x2071,x2072)+P7(x2071,x2072,x2073) % 0.55/0.72 [209]~P22(x2093)+~P8(x2091,x2092,x2093)+E(x2091,x2092)+P7(x2091,x2092,x2093) % 0.55/0.72 [247]~P8(x2472,x2471,x2473)+~P8(x2471,x2472,x2473)+E(x2471,x2472)+~P3(x2473) % 0.55/0.72 [258]P7(x2582,x2581,x2583)+~P2(x2583)+~P8(x2582,x2581,x2583)+P8(x2581,x2582,x2583) % 0.55/0.72 [259]~P9(x2592)+~E(f9(x2591,x2593,x2592),f12(x2592))+~E(f10(x2591,x2593,x2592),f11(x2592))+E(f6(x2591,x2592),x2593) % 0.55/0.72 [327]~P23(x3272)+~P8(x3271,x3273,x3272)+~P8(f6(x3271,x3272),x3273,x3272)+P8(f4(x3271,x3272),x3273,x3272) % 0.55/0.72 [328]~P31(x3282)+~P7(x3281,x3283,x3282)+~P7(f6(x3281,x3282),x3283,x3282)+P7(f4(x3281,x3282),x3283,x3282) % 0.55/0.72 [289]~P2(x2893)+~P8(x2891,x2894,x2893)+P8(x2891,x2892,x2893)+~P8(x2894,x2892,x2893) % 0.55/0.72 [290]~P3(x2903)+~P8(x2901,x2904,x2903)+P8(x2901,x2902,x2903)+~P8(x2904,x2902,x2903) % 0.55/0.72 [291]~P2(x2913)+~P7(x2911,x2914,x2913)+P7(x2911,x2912,x2913)+~P8(x2914,x2912,x2913) % 0.55/0.72 [292]~P2(x2923)+~P7(x2924,x2922,x2923)+P7(x2921,x2922,x2923)+~P8(x2921,x2924,x2923) % 0.55/0.72 [293]~P2(x2933)+~P7(x2931,x2934,x2933)+P7(x2931,x2932,x2933)+~P7(x2934,x2932,x2933) % 0.55/0.72 [294]~P3(x2943)+~P7(x2941,x2944,x2943)+P7(x2941,x2942,x2943)+~P8(x2944,x2942,x2943) % 0.55/0.72 [295]~P3(x2953)+~P7(x2954,x2952,x2953)+P7(x2951,x2952,x2953)+~P8(x2951,x2954,x2953) % 0.55/0.72 [296]~P3(x2963)+~P7(x2961,x2964,x2963)+P7(x2961,x2962,x2963)+~P7(x2964,x2962,x2963) % 0.55/0.72 [251]~P6(x2514)+~P33(x2514)+E(x2511,x2512)+~E(f7(x2513,x2511,x2514),f7(x2513,x2512,x2514)) % 0.55/0.72 [378]~P12(x3784)+~P8(x3781,x3783,x3784)+~P8(x3781,x3782,x3784)+P8(x3781,f10(x3782,x3783,x3784),x3784) % 0.55/0.72 [381]~P22(x3814)+~P8(x3811,x3813,x3814)+~P8(x3811,x3812,x3814)+P8(x3811,f13(x3812,x3813,x3814),x3814) % 0.55/0.72 [382]~P22(x3824)+~P7(x3821,x3823,x3824)+~P7(x3821,x3822,x3824)+P7(x3821,f13(x3822,x3823,x3824),x3824) % 0.55/0.72 [385]~P4(x3853)+~P8(x3852,x3854,x3853)+~P8(x3851,x3854,x3853)+P8(f9(x3851,x3852,x3853),x3854,x3853) % 0.55/0.72 [388]~P22(x3883)+~P8(x3882,x3884,x3883)+~P8(x3881,x3884,x3883)+P8(f14(x3881,x3882,x3883),x3884,x3883) % 0.55/0.72 [389]~P22(x3893)+~P7(x3892,x3894,x3893)+~P7(x3891,x3894,x3893)+P7(f14(x3891,x3892,x3893),x3894,x3893) % 0.55/0.72 [399]~P22(x3993)+P8(x3991,x3992,x3993)+P8(x3991,x3994,x3993)+~P8(x3991,f14(x3992,x3994,x3993),x3993) % 0.55/0.72 [400]~P22(x4003)+P7(x4001,x4002,x4003)+P7(x4001,x4004,x4003)+~P7(x4001,f14(x4002,x4004,x4003),x4003) % 0.55/0.72 [401]~P22(x4013)+P8(x4011,x4012,x4013)+P8(x4014,x4012,x4013)+~P8(f13(x4011,x4014,x4013),x4012,x4013) % 0.55/0.72 [402]~P22(x4023)+P7(x4021,x4022,x4023)+P7(x4024,x4022,x4023)+~P7(f13(x4021,x4024,x4023),x4022,x4023) % 0.55/0.72 [445]~P31(x4453)+~P7(x4451,f7(x4452,x4454,x4453),x4453)+~P7(f8(x4452,x4454,x4453),x4451,x4453)+P7(f4(f8(x4451,x4452,x4453),x4453),x4454,x4453) % 0.55/0.72 [349]~P24(x3493)+~P8(x3495,x3494,x3493)+P8(x3491,x3492,x3493)+~E(f8(x3494,x3495,x3493),f8(x3492,x3491,x3493)) % 0.55/0.72 [350]~P24(x3503)+~P8(x3505,x3504,x3503)+P8(x3501,x3502,x3503)+~E(f8(x3502,x3501,x3503),f8(x3504,x3505,x3503)) % 0.55/0.72 [351]~P24(x3513)+~P7(x3514,x3515,x3513)+P7(x3511,x3512,x3513)+~E(f8(x3514,x3515,x3513),f8(x3511,x3512,x3513)) % 0.55/0.72 [352]~P24(x3523)+~P7(x3524,x3525,x3523)+P7(x3521,x3522,x3523)+~E(f8(x3521,x3522,x3523),f8(x3524,x3525,x3523)) % 0.55/0.72 [424]~P27(x4243)+~P8(x4242,x4245,x4243)+~P8(x4241,x4244,x4243)+P8(f7(x4241,x4242,x4243),f7(x4244,x4245,x4243),x4243) % 0.55/0.72 [425]~P26(x4253)+~P8(x4252,x4255,x4253)+~P7(x4251,x4254,x4253)+P7(f7(x4251,x4252,x4253),f7(x4254,x4255,x4253),x4253) % 0.55/0.72 [426]~P26(x4263)+~P8(x4261,x4264,x4263)+~P7(x4262,x4265,x4263)+P7(f7(x4261,x4262,x4263),f7(x4264,x4265,x4263),x4263) % 0.55/0.72 [427]~P26(x4273)+~P7(x4272,x4275,x4273)+~P7(x4271,x4274,x4273)+P7(f7(x4271,x4272,x4273),f7(x4274,x4275,x4273),x4273) % 0.55/0.72 [435]~P24(x4354)+~P8(x4355,x4353,x4354)+~P8(x4351,f7(x4352,x4355,x4354),x4354)+P8(x4351,f7(x4352,x4353,x4354),x4354) % 0.55/0.72 [443]~P1(x4433)+~P7(f15(x4432,x4433),x4435,a1)+~P7(f15(x4431,x4433),x4434,a1)+P7(f15(f7(x4431,x4432,x4433),x4433),f7(x4434,x4435,a1),a1) % 0.55/0.72 %EqnAxiom % 0.55/0.72 [1]E(x11,x11) % 0.55/0.72 [2]E(x22,x21)+~E(x21,x22) % 0.55/0.72 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.55/0.72 [4]~E(x41,x42)+E(f2(x41,x43),f2(x42,x43)) % 0.55/0.72 [5]~E(x51,x52)+E(f2(x53,x51),f2(x53,x52)) % 0.55/0.72 [6]~E(x61,x62)+E(f7(x61,x63,x64),f7(x62,x63,x64)) % 0.55/0.72 [7]~E(x71,x72)+E(f7(x73,x71,x74),f7(x73,x72,x74)) % 0.55/0.72 [8]~E(x81,x82)+E(f7(x83,x84,x81),f7(x83,x84,x82)) % 0.55/0.72 [9]~E(x91,x92)+E(f3(x91,x93),f3(x92,x93)) % 0.55/0.72 [10]~E(x101,x102)+E(f3(x103,x101),f3(x103,x102)) % 0.55/0.72 [11]~E(x111,x112)+E(f4(x111,x113),f4(x112,x113)) % 0.55/0.72 [12]~E(x121,x122)+E(f4(x123,x121),f4(x123,x122)) % 0.55/0.72 [13]~E(x131,x132)+E(f13(x131,x133,x134),f13(x132,x133,x134)) % 0.55/0.72 [14]~E(x141,x142)+E(f13(x143,x141,x144),f13(x143,x142,x144)) % 0.55/0.72 [15]~E(x151,x152)+E(f13(x153,x154,x151),f13(x153,x154,x152)) % 0.55/0.72 [16]~E(x161,x162)+E(f5(x161),f5(x162)) % 0.55/0.72 [17]~E(x171,x172)+E(f9(x171,x173,x174),f9(x172,x173,x174)) % 0.55/0.72 [18]~E(x181,x182)+E(f9(x183,x181,x184),f9(x183,x182,x184)) % 0.55/0.72 [19]~E(x191,x192)+E(f9(x193,x194,x191),f9(x193,x194,x192)) % 0.55/0.72 [20]~E(x201,x202)+E(f11(x201),f11(x202)) % 0.55/0.72 [21]~E(x211,x212)+E(f6(x211,x213),f6(x212,x213)) % 0.55/0.72 [22]~E(x221,x222)+E(f6(x223,x221),f6(x223,x222)) % 0.55/0.72 [23]~E(x231,x232)+E(f12(x231),f12(x232)) % 0.55/0.72 [24]~E(x241,x242)+E(f8(x241,x243,x244),f8(x242,x243,x244)) % 0.55/0.72 [25]~E(x251,x252)+E(f8(x253,x251,x254),f8(x253,x252,x254)) % 0.55/0.72 [26]~E(x261,x262)+E(f8(x263,x264,x261),f8(x263,x264,x262)) % 0.55/0.72 [27]~E(x271,x272)+E(f10(x271,x273,x274),f10(x272,x273,x274)) % 0.55/0.72 [28]~E(x281,x282)+E(f10(x283,x281,x284),f10(x283,x282,x284)) % 0.55/0.72 [29]~E(x291,x292)+E(f10(x293,x294,x291),f10(x293,x294,x292)) % 0.55/0.72 [30]~E(x301,x302)+E(f14(x301,x303,x304),f14(x302,x303,x304)) % 0.55/0.72 [31]~E(x311,x312)+E(f14(x313,x311,x314),f14(x313,x312,x314)) % 0.55/0.72 [32]~E(x321,x322)+E(f14(x323,x324,x321),f14(x323,x324,x322)) % 0.55/0.72 [33]~E(x331,x332)+E(f15(x331,x333),f15(x332,x333)) % 0.55/0.72 [34]~E(x341,x342)+E(f15(x343,x341),f15(x343,x342)) % 0.55/0.72 [35]~E(x351,x352)+E(f16(x351),f16(x352)) % 0.55/0.72 [36]~P1(x361)+P1(x362)+~E(x361,x362) % 0.55/0.72 [37]~P2(x371)+P2(x372)+~E(x371,x372) % 0.55/0.72 [38]~P3(x381)+P3(x382)+~E(x381,x382) % 0.55/0.72 [39]~P4(x391)+P4(x392)+~E(x391,x392) % 0.55/0.72 [40]~P13(x401)+P13(x402)+~E(x401,x402) % 0.55/0.72 [41]~P20(x411)+P20(x412)+~E(x411,x412) % 0.55/0.72 [42]~P5(x421)+P5(x422)+~E(x421,x422) % 0.55/0.72 [43]~P14(x431)+P14(x432)+~E(x431,x432) % 0.55/0.72 [44]~P22(x441)+P22(x442)+~E(x441,x442) % 0.55/0.72 [45]~P23(x451)+P23(x452)+~E(x451,x452) % 0.55/0.72 [46]~P31(x461)+P31(x462)+~E(x461,x462) % 0.55/0.72 [47]~P11(x471)+P11(x472)+~E(x471,x472) % 0.55/0.72 [48]~P12(x481)+P12(x482)+~E(x481,x482) % 0.55/0.72 [49]~P24(x491)+P24(x492)+~E(x491,x492) % 0.55/0.72 [50]~P21(x501)+P21(x502)+~E(x501,x502) % 0.55/0.72 [51]~P15(x511)+P15(x512)+~E(x511,x512) % 0.55/0.72 [52]~P32(x521)+P32(x522)+~E(x521,x522) % 0.55/0.72 [53]~P16(x531)+P16(x532)+~E(x531,x532) % 0.55/0.72 [54]~P17(x541)+P17(x542)+~E(x541,x542) % 0.55/0.72 [55]~P26(x551)+P26(x552)+~E(x551,x552) % 0.55/0.72 [56]~P27(x561)+P27(x562)+~E(x561,x562) % 0.55/0.72 [57]~P28(x571)+P28(x572)+~E(x571,x572) % 0.55/0.72 [58]~P6(x581)+P6(x582)+~E(x581,x582) % 0.55/0.72 [59]~P33(x591)+P33(x592)+~E(x591,x592) % 0.55/0.72 [60]~P18(x601)+P18(x602)+~E(x601,x602) % 0.55/0.72 [61]~P19(x611)+P19(x612)+~E(x611,x612) % 0.55/0.72 [62]~P25(x621)+P25(x622)+~E(x621,x622) % 0.55/0.72 [63]~P34(x631)+P34(x632)+~E(x631,x632) % 0.55/0.72 [64]P8(x642,x643,x644)+~E(x641,x642)+~P8(x641,x643,x644) % 0.55/0.72 [65]P8(x653,x652,x654)+~E(x651,x652)+~P8(x653,x651,x654) % 0.55/0.72 [66]P8(x663,x664,x662)+~E(x661,x662)+~P8(x663,x664,x661) % 0.55/0.72 [67]P7(x672,x673,x674)+~E(x671,x672)+~P7(x671,x673,x674) % 0.55/0.72 [68]P7(x683,x682,x684)+~E(x681,x682)+~P7(x683,x681,x684) % 0.55/0.72 [69]P7(x693,x694,x692)+~E(x691,x692)+~P7(x693,x694,x691) % 0.55/0.72 [70]~P9(x701)+P9(x702)+~E(x701,x702) % 0.55/0.72 [71]~P30(x711)+P30(x712)+~E(x711,x712) % 0.55/0.72 [72]~P29(x721)+P29(x722)+~E(x721,x722) % 0.55/0.72 [73]~P10(x731)+P10(x732)+~E(x731,x732) % 0.55/0.72 % 0.55/0.72 %------------------------------------------- % 0.55/0.72 cnf(473,plain, % 0.55/0.72 ($false), % 0.55/0.72 inference(scs_inference,[],[102,106,147,149,155,176]), % 0.55/0.72 ['proof']). % 0.55/0.72 % SZS output end Proof % 0.55/0.72 % Total time :0.010000s %------------------------------------------------------------------------------