%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : ANA023-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n013.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 : 600s % DateTime : Thu Jul 14 19:15:39 EDT 2022 % Result : Unsatisfiable 12.10s 11.98s % Output : Proof 12.10s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : ANA023-10 : TPTP v8.1.0. Released v7.5.0. % 0.11/0.13 % Command : moca.sh %s % 0.12/0.34 % Computer : n013.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 : 600 % 0.12/0.34 % DateTime : Fri Jul 8 05:32:44 EDT 2022 % 0.12/0.34 % CPUTime : % 12.10/11.98 % SZS status Unsatisfiable % 12.10/11.98 % SZS output start Proof % 12.10/11.98 The input problem is unsatisfiable because % 12.10/11.98 % 12.10/11.98 [1] the following set of Horn clauses is unsatisfiable: % 12.10/11.98 % 12.10/11.98 ifeq2(A, A, B, C) = B % 12.10/11.98 ifeq(A, A, B, C) = B % 12.10/11.98 ifeq2(class_OrderedGroup_Ocomm__monoid__add(T_a), true, c_plus(c_0, V_y, T_a), V_y) = V_y % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a), true, ifeq(c_lessequals(V_a, c_minus(V_c, V_b, T_a), T_a), true, c_lessequals(c_plus(V_a, V_b, T_a), V_c, T_a), true), true) = true % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a), true, ifeq(c_lessequals(c_plus(V_a, V_b, T_a), V_c, T_a), true, c_lessequals(V_a, c_minus(V_c, V_b, T_a), T_a), true), true) = true % 12.10/11.98 ifeq(class_Orderings_Oorder(T_a), true, ifeq(c_lessequals(V_x, V_y, T_a), true, ifeq(c_lessequals(V_y, V_z, T_a), true, c_lessequals(V_x, V_z, T_a), true), true), true) = true % 12.10/11.98 c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) = true % 12.10/11.98 c_lessequals(v_k(v_x), v_f(v_x), t_b) = true % 12.10/11.98 c_lessequals(c_0, c_minus(v_f(v_x), v_g(v_x), t_b), t_b) = true ==> \bottom % 12.10/11.98 ifeq(class_Orderings_Olinorder(T), true, class_Orderings_Oorder(T), true) = true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_OrderedGroup_Ocomm__monoid__add(T), true) = true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_Orderings_Olinorder(T), true) = true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_OrderedGroup_Opordered__ab__group__add(T), true) = true % 12.10/11.98 class_Ring__and__Field_Oordered__idom(t_b) = true % 12.10/11.98 % 12.10/11.98 This holds because % 12.10/11.98 % 12.10/11.98 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 12.10/11.98 % 12.10/11.98 E: % 12.10/11.98 c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) = true % 12.10/11.98 c_lessequals(v_k(v_x), v_f(v_x), t_b) = true % 12.10/11.98 class_Ring__and__Field_Oordered__idom(t_b) = true % 12.10/11.98 f1(c_lessequals(c_0, c_minus(v_f(v_x), v_g(v_x), t_b), t_b)) = true__ % 12.10/11.98 f1(true) = false__ % 12.10/11.98 ifeq(A, A, B, C) = B % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a), true, ifeq(c_lessequals(V_a, c_minus(V_c, V_b, T_a), T_a), true, c_lessequals(c_plus(V_a, V_b, T_a), V_c, T_a), true), true) = true % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a), true, ifeq(c_lessequals(c_plus(V_a, V_b, T_a), V_c, T_a), true, c_lessequals(V_a, c_minus(V_c, V_b, T_a), T_a), true), true) = true % 12.10/11.98 ifeq(class_Orderings_Olinorder(T), true, class_Orderings_Oorder(T), true) = true % 12.10/11.98 ifeq(class_Orderings_Oorder(T_a), true, ifeq(c_lessequals(V_x, V_y, T_a), true, ifeq(c_lessequals(V_y, V_z, T_a), true, c_lessequals(V_x, V_z, T_a), true), true), true) = true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_OrderedGroup_Ocomm__monoid__add(T), true) = true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_OrderedGroup_Opordered__ab__group__add(T), true) = true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_Orderings_Olinorder(T), true) = true % 12.10/11.98 ifeq2(A, A, B, C) = B % 12.10/11.98 ifeq2(class_OrderedGroup_Ocomm__monoid__add(T_a), true, c_plus(c_0, V_y, T_a), V_y) = V_y % 12.10/11.98 G: % 12.10/11.98 true__ = false__ % 12.10/11.98 % 12.10/11.98 This holds because % 12.10/11.98 % 12.10/11.98 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 12.10/11.98 % 12.10/11.98 % 12.10/11.98 c_lessequals(c_0, c_minus(c_minus(v_k(v_x), v_g(v_x), t_b), c_0, t_b), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(c_0, c_minus(v_f(v_x), v_g(v_x), t_b), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(c_0, c_minus(v_f(v_x), v_k(v_x), t_b), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(c_plus(c_0, v_g(v_x), t_b), v_k(v_x), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(v_g(v_x), v_f(v_x), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(v_g(v_x), v_k(v_x), t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 c_lessequals(v_k(v_x), v_f(v_x), t_b) -> true % 12.10/11.98 c_plus(c_0, Y1, t_b) -> Y1 % 12.10/11.98 class_OrderedGroup_Opordered__ab__group__add(t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 class_Orderings_Olinorder(t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 class_Orderings_Oorder(t_b) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 class_Ring__and__Field_Oordered__idom(t_b) -> true % 12.10/11.98 f1(c_lessequals(c_0, c_minus(v_f(v_x), v_g(v_x), t_b), t_b)) -> true__ % 12.10/11.98 f1(c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b)) -> false__ % 12.10/11.98 f1(class_OrderedGroup_Ocomm__monoid__add(t_b)) -> false__ % 12.10/11.98 f1(true) -> false__ % 12.10/11.98 ifeq(A, A, B, C) -> B % 12.10/11.98 ifeq(c_lessequals(Y0, v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y0, v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(Y1, Y2, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(c_0, c_minus(Y2, Y1, t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(Y1, Y2, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y2, Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(Y1, c_0, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, c_minus(v_k(v_x), v_g(v_x), t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(Y1, c_minus(Y2, Y3, t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(c_plus(Y1, Y3, t_b), Y2, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(Y1, v_g(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(Y1, v_g(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_0, c_0, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_0, c_minus(Y1, Y2, t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y2, Y1, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_0, c_minus(c_minus(v_f(v_x), v_k(v_x), t_b), c_0, t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_0, c_minus(c_minus(v_k(v_x), v_g(v_x), t_b), c_0, t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_0, c_minus(v_f(v_x), v_g(v_x), t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_0, c_minus(v_f(v_x), v_k(v_x), t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_minus(v_k(v_x), v_g(v_x), t_b), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(c_0, Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_minus(v_k(v_x), v_g(v_x), t_b), c_minus(v_k(v_x), v_g(v_x), t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_plus(Y1, Y2, t_b), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, c_minus(Y3, Y2, t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(c_plus(c_0, v_g(v_x), t_b), v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_f(v_x), Y0, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(v_k(v_x), Y0, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_f(v_x), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(v_g(v_x), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_f(v_x), v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_g(v_x), Y2, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y2, v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_g(v_x), v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_k(v_x), Y0, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y0, v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_k(v_x), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(v_g(v_x), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(c_lessequals(v_k(v_x), v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a), true, ifeq(c_lessequals(V_a, c_minus(V_c, V_b, T_a), T_a), true, c_lessequals(c_plus(V_a, V_b, T_a), V_c, T_a), true), true) -> true % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(T_a), true, ifeq(c_lessequals(c_plus(V_a, V_b, T_a), V_c, T_a), true, c_lessequals(V_a, c_minus(V_c, V_b, T_a), T_a), true), true) -> true % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y1, c_minus(Y2, Y3, Y0), Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(c_plus(Y1, Y3, Y0), Y2, Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_OrderedGroup_Opordered__ab__group__add(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(c_plus(Y1, Y2, Y0), Y3, Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, c_minus(Y3, Y2, Y0), Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Orderings_Olinorder(T), true, class_Orderings_Oorder(T), true) -> true % 12.10/11.98 ifeq(class_Orderings_Olinorder(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b), class_Orderings_Oorder(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b)) -> c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) % 12.10/11.98 ifeq(class_Orderings_Olinorder(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), class_Orderings_Oorder(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Orderings_Oorder(T_a), true, ifeq(c_lessequals(V_x, V_y, T_a), true, ifeq(c_lessequals(V_y, V_z, T_a), true, c_lessequals(V_x, V_z, T_a), true), true), true) -> true % 12.10/11.98 ifeq(class_Orderings_Oorder(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y1, Y2, Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y2, Y3, Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, Y3, Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Orderings_Oorder(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y1, v_k(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(Y1, v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Orderings_Oorder(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(v_f(v_x), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), c_lessequals(v_k(v_x), Y3, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Orderings_Oorder(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(v_f(v_x), v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Orderings_Oorder(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(v_k(v_x), Y2, t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), ifeq(c_lessequals(Y2, v_f(v_x), t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_OrderedGroup_Ocomm__monoid__add(T), true) -> true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_OrderedGroup_Opordered__ab__group__add(T), true) -> true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(T), true, class_Orderings_Olinorder(T), true) -> true % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b), class_OrderedGroup_Ocomm__monoid__add(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b)) -> c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b), class_OrderedGroup_Opordered__ab__group__add(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b)) -> c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b), class_Orderings_Olinorder(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b)) -> c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Ocomm__monoid__add(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), class_OrderedGroup_Opordered__ab__group__add(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq(class_Ring__and__Field_Oordered__idom(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), class_Orderings_Olinorder(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b)) -> class_OrderedGroup_Ocomm__monoid__add(t_b) % 12.10/11.98 ifeq2(A, A, B, C) -> B % 12.10/11.98 ifeq2(class_OrderedGroup_Ocomm__monoid__add(T_a), true, c_plus(c_0, V_y, T_a), V_y) -> V_y % 12.10/11.98 ifeq2(class_OrderedGroup_Ocomm__monoid__add(Y0), c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b), c_plus(c_0, Y1, Y0), Y1) -> Y1 % 12.10/11.98 ifeq2(class_OrderedGroup_Ocomm__monoid__add(Y0), class_OrderedGroup_Ocomm__monoid__add(t_b), c_plus(c_0, Y1, Y0), Y1) -> Y1 % 12.10/11.98 true -> c_lessequals(c_0, c_minus(v_k(v_x), v_g(v_x), t_b), t_b) % 12.10/11.98 true__ -> false__ % 12.10/11.98 with the LPO induced by % 12.10/11.98 class_Orderings_Olinorder > class_Ring__and__Field_Oordered__idom > v_f > true > c_0 > f1 > t_b > v_g > v_x > v_k > class_Orderings_Oorder > c_minus > c_lessequals > class_OrderedGroup_Opordered__ab__group__add > c_plus > class_OrderedGroup_Ocomm__monoid__add > ifeq > ifeq2 > true__ > false__ % 12.10/11.98 % 12.10/11.98 % SZS output end Proof % 12.10/11.98 %------------------------------------------------------------------------------