%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : ALG030-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n026.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 17:40:27 EDT 2022 % Result : Unsatisfiable 14.49s 14.23s % Output : Proof 14.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : ALG030-10 : TPTP v8.1.0. Released v7.3.0. % 0.07/0.13 % Command : moca.sh %s % 0.12/0.34 % Computer : n026.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 : Wed Jun 8 23:05:47 EDT 2022 % 0.12/0.34 % CPUTime : % 14.49/14.23 % SZS status Unsatisfiable % 14.49/14.23 % SZS output start Proof % 14.49/14.23 The input problem is unsatisfiable because % 14.49/14.23 % 14.49/14.23 [1] the following set of Horn clauses is unsatisfiable: % 14.49/14.23 % 14.49/14.23 ifeq2(A, A, B, C) = B % 14.49/14.23 ifeq(A, A, B, C) = B % 14.49/14.23 ifeq(sorti1(V), true, ifeq(sorti1(U), true, sorti1(op1(U, V)), true), true) = true % 14.49/14.23 ifeq(sorti2(V), true, ifeq(sorti2(U), true, sorti2(op2(U, V)), true), true) = true % 14.49/14.23 op1(sK2_ax3_U, sK1_ax3_V) = op1(sK1_ax3_V, sK2_ax3_U) ==> \bottom % 14.49/14.23 sorti1(sK1_ax3_V) = true % 14.49/14.23 sorti1(sK2_ax3_U) = true % 14.49/14.23 ifeq2(sorti2(V), true, ifeq2(sorti2(U), true, op2(U, V), op2(V, U)), op2(V, U)) = op2(V, U) % 14.49/14.23 ifeq(sorti1(U), true, sorti2(h(U)), true) = true % 14.49/14.23 ifeq2(sorti1(X), true, ifeq2(sorti1(W), true, op2(h(W), h(X)), h(op1(W, X))), h(op1(W, X))) = h(op1(W, X)) % 14.49/14.23 ifeq2(sorti1(X2), true, j(h(X2)), X2) = X2 % 14.49/14.23 ifeq(sorti2(V), true, sorti1(j(V)), true) = true % 14.49/14.23 ifeq2(sorti2(Z), true, ifeq2(sorti2(Y), true, op1(j(Y), j(Z)), j(op2(Y, Z))), j(op2(Y, Z))) = j(op2(Y, Z)) % 14.49/14.23 ifeq2(sorti2(X1), true, h(j(X1)), X1) = X1 % 14.49/14.23 % 14.49/14.23 This holds because % 14.49/14.23 % 14.49/14.23 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 14.49/14.23 % 14.49/14.23 E: % 14.49/14.23 f1(op1(sK1_ax3_V, sK2_ax3_U)) = false__ % 14.49/14.23 f1(op1(sK2_ax3_U, sK1_ax3_V)) = true__ % 14.49/14.23 ifeq(A, A, B, C) = B % 14.49/14.23 ifeq(sorti1(U), true, sorti2(h(U)), true) = true % 14.49/14.23 ifeq(sorti1(V), true, ifeq(sorti1(U), true, sorti1(op1(U, V)), true), true) = true % 14.49/14.23 ifeq(sorti2(V), true, ifeq(sorti2(U), true, sorti2(op2(U, V)), true), true) = true % 14.49/14.23 ifeq(sorti2(V), true, sorti1(j(V)), true) = true % 14.49/14.23 ifeq2(A, A, B, C) = B % 14.49/14.23 ifeq2(sorti1(X), true, ifeq2(sorti1(W), true, op2(h(W), h(X)), h(op1(W, X))), h(op1(W, X))) = h(op1(W, X)) % 14.49/14.23 ifeq2(sorti1(X2), true, j(h(X2)), X2) = X2 % 14.49/14.23 ifeq2(sorti2(V), true, ifeq2(sorti2(U), true, op2(U, V), op2(V, U)), op2(V, U)) = op2(V, U) % 14.49/14.23 ifeq2(sorti2(X1), true, h(j(X1)), X1) = X1 % 14.49/14.23 ifeq2(sorti2(Z), true, ifeq2(sorti2(Y), true, op1(j(Y), j(Z)), j(op2(Y, Z))), j(op2(Y, Z))) = j(op2(Y, Z)) % 14.49/14.23 sorti1(sK1_ax3_V) = true % 14.49/14.23 sorti1(sK2_ax3_U) = true % 14.49/14.23 G: % 14.49/14.23 true__ = false__ % 14.49/14.23 % 14.49/14.23 This holds because % 14.49/14.23 % 14.49/14.23 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 14.49/14.23 % 14.49/14.23 % 14.49/14.23 f1(op1(sK1_ax3_V, sK2_ax3_U)) -> false__ % 14.49/14.23 f1(op1(sK2_ax3_U, sK1_ax3_V)) -> true__ % 14.49/14.23 h(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)) -> op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK1_ax3_V)) % 14.49/14.23 h(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)) -> op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK2_ax3_U)) % 14.49/14.23 h(op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V)) -> op2(op2(h(sK2_ax3_U), h(sK1_ax3_V)), h(sK1_ax3_V)) % 14.49/14.23 h(op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U)) -> op2(op2(h(sK2_ax3_U), h(sK1_ax3_V)), h(sK2_ax3_U)) % 14.49/14.23 h(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)) -> op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(sK1_ax3_V)) % 14.49/14.23 h(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)) -> op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(sK2_ax3_U)) % 14.49/14.23 h(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))) -> op2(h(sK1_ax3_V), op2(h(sK1_ax3_V), h(sK2_ax3_U))) % 14.49/14.23 h(op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V))) -> op2(h(sK1_ax3_V), op2(h(sK2_ax3_U), h(sK1_ax3_V))) % 14.49/14.23 h(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))) -> op2(h(sK1_ax3_V), op2(h(sK2_ax3_U), h(sK2_ax3_U))) % 14.49/14.23 h(op1(sK1_ax3_V, sK1_ax3_V)) -> op2(h(sK1_ax3_V), h(sK1_ax3_V)) % 14.49/14.24 h(op1(sK1_ax3_V, sK2_ax3_U)) -> op2(h(sK1_ax3_V), h(sK2_ax3_U)) % 14.49/14.24 h(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))) -> op2(h(sK2_ax3_U), op2(h(sK1_ax3_V), h(sK2_ax3_U))) % 14.49/14.24 h(op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V))) -> op2(h(sK2_ax3_U), op2(h(sK2_ax3_U), h(sK1_ax3_V))) % 14.49/14.24 h(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))) -> op2(h(sK2_ax3_U), op2(h(sK2_ax3_U), h(sK2_ax3_U))) % 14.49/14.24 h(op1(sK2_ax3_U, sK1_ax3_V)) -> op2(h(sK2_ax3_U), h(sK1_ax3_V)) % 14.49/14.24 h(op1(sK2_ax3_U, sK2_ax3_U)) -> op2(h(sK2_ax3_U), h(sK2_ax3_U)) % 14.49/14.24 ifeq(A, A, B, C) -> B % 14.49/14.24 ifeq(sorti1(U), true, sorti2(h(U)), true) -> true % 14.49/14.24 ifeq(sorti1(V), true, ifeq(sorti1(U), true, sorti1(op1(U, V)), true), true) -> true % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, Y0)), sorti1(sK1_ax3_V)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(op1(sK1_ax3_V, sK1_ax3_V), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(op1(sK2_ax3_U, sK1_ax3_V), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(sK1_ax3_V, Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti1(op1(sK2_ax3_U, Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y0), sorti1(sK1_ax3_V), sorti2(h(Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, op1(sK1_ax3_V, sK1_ax3_V))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, op1(sK1_ax3_V, sK2_ax3_U))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, op1(sK2_ax3_U, sK1_ax3_V))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, op1(sK2_ax3_U, sK2_ax3_U))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, sK1_ax3_V)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti1(Y1), sorti1(sK1_ax3_V), sorti1(op1(Y1, sK2_ax3_U)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(V), true, ifeq(sorti2(U), true, sorti2(op2(U, V)), true), true) -> true % 14.49/14.24 ifeq(sorti2(V), true, sorti1(j(V)), true) -> true % 14.49/14.24 ifeq(sorti2(Y0), sorti1(sK1_ax3_V), ifeq(sorti2(Y1), sorti1(sK1_ax3_V), sorti2(op2(Y1, Y0)), sorti1(sK1_ax3_V)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y0), sorti1(sK1_ax3_V), sorti1(j(Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y0), sorti1(sK1_ax3_V), sorti2(op2(h(sK1_ax3_V), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y0), sorti1(sK1_ax3_V), sorti2(op2(h(sK2_ax3_U), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y0), sorti1(sK1_ax3_V), sorti2(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y0), sorti1(sK1_ax3_V), sorti2(op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), Y0)), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y1), sorti1(sK1_ax3_V), sorti2(op2(Y1, h(sK1_ax3_V))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y1), sorti1(sK1_ax3_V), sorti2(op2(Y1, h(sK2_ax3_U))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y1), sorti1(sK1_ax3_V), sorti2(op2(Y1, op2(h(sK1_ax3_V), h(sK2_ax3_U)))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq(sorti2(Y1), sorti1(sK1_ax3_V), sorti2(op2(Y1, op2(h(sK2_ax3_U), h(sK2_ax3_U)))), sorti1(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 ifeq2(A, A, B, C) -> B % 14.49/14.24 ifeq2(sorti1(X), true, ifeq2(sorti1(W), true, op2(h(W), h(X)), h(op1(W, X))), h(op1(W, X))) -> h(op1(W, X)) % 14.49/14.24 ifeq2(sorti1(X2), true, j(h(X2)), X2) -> X2 % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), ifeq2(sorti1(Y1), sorti1(sK1_ax3_V), op2(h(Y1), h(Y0)), h(op1(Y1, Y0))), h(op1(Y1, Y0))) -> h(op1(Y1, Y0)) % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), j(h(Y0)), Y0) -> Y0 % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), op2(h(sK1_ax3_V), h(Y0)), h(op1(sK1_ax3_V, Y0))) -> h(op1(sK1_ax3_V, Y0)) % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), op2(h(sK2_ax3_U), h(Y0)), h(op1(sK2_ax3_U, Y0))) -> h(op1(sK2_ax3_U, Y0)) % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(Y0)), h(op1(op1(sK1_ax3_V, sK2_ax3_U), Y0))) -> h(op1(op1(sK1_ax3_V, sK2_ax3_U), Y0)) % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), op2(op2(h(sK2_ax3_U), h(sK1_ax3_V)), h(Y0)), h(op1(op1(sK2_ax3_U, sK1_ax3_V), Y0))) -> h(op1(op1(sK2_ax3_U, sK1_ax3_V), Y0)) % 14.49/14.24 ifeq2(sorti1(Y0), sorti1(sK1_ax3_V), op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(Y0)), h(op1(op1(sK2_ax3_U, sK2_ax3_U), Y0))) -> h(op1(op1(sK2_ax3_U, sK2_ax3_U), Y0)) % 14.49/14.24 ifeq2(sorti1(Y1), sorti1(sK1_ax3_V), op2(h(Y1), h(sK1_ax3_V)), h(op1(Y1, sK1_ax3_V))) -> h(op1(Y1, sK1_ax3_V)) % 14.49/14.24 ifeq2(sorti1(Y1), sorti1(sK1_ax3_V), op2(h(Y1), h(sK2_ax3_U)), h(op1(Y1, sK2_ax3_U))) -> h(op1(Y1, sK2_ax3_U)) % 14.49/14.24 ifeq2(sorti1(Y1), sorti1(sK1_ax3_V), op2(h(Y1), op2(h(sK1_ax3_V), h(sK2_ax3_U))), h(op1(Y1, op1(sK1_ax3_V, sK2_ax3_U)))) -> h(op1(Y1, op1(sK1_ax3_V, sK2_ax3_U))) % 14.49/14.24 ifeq2(sorti1(Y1), sorti1(sK1_ax3_V), op2(h(Y1), op2(h(sK2_ax3_U), h(sK1_ax3_V))), h(op1(Y1, op1(sK2_ax3_U, sK1_ax3_V)))) -> h(op1(Y1, op1(sK2_ax3_U, sK1_ax3_V))) % 14.49/14.24 ifeq2(sorti1(Y1), sorti1(sK1_ax3_V), op2(h(Y1), op2(h(sK2_ax3_U), h(sK2_ax3_U))), h(op1(Y1, op1(sK2_ax3_U, sK2_ax3_U)))) -> h(op1(Y1, op1(sK2_ax3_U, sK2_ax3_U))) % 14.49/14.24 ifeq2(sorti2(V), true, ifeq2(sorti2(U), true, op2(U, V), op2(V, U)), op2(V, U)) -> op2(V, U) % 14.49/14.24 ifeq2(sorti2(X1), true, h(j(X1)), X1) -> X1 % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), h(j(Y0)), Y0) -> Y0 % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), ifeq2(sorti2(Y1), sorti1(sK1_ax3_V), op1(j(Y1), j(Y0)), j(op2(Y1, Y0))), j(op2(Y1, Y0))) -> j(op2(Y1, Y0)) % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), ifeq2(sorti2(Y1), sorti1(sK1_ax3_V), op2(Y1, Y0), op2(Y0, Y1)), op2(Y0, Y1)) -> op2(Y0, Y1) % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), op1(sK1_ax3_V, j(Y0)), j(op2(h(sK1_ax3_V), Y0))) -> j(op2(h(sK1_ax3_V), Y0)) % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), op1(sK2_ax3_U, j(Y0)), j(op2(h(sK2_ax3_U), Y0))) -> j(op2(h(sK2_ax3_U), Y0)) % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), op2(h(sK1_ax3_V), Y0), op2(Y0, h(sK1_ax3_V))) -> op2(Y0, h(sK1_ax3_V)) % 14.49/14.24 ifeq2(sorti2(Y0), sorti1(sK1_ax3_V), op2(h(sK2_ax3_U), Y0), op2(Y0, h(sK2_ax3_U))) -> op2(Y0, h(sK2_ax3_U)) % 14.49/14.24 ifeq2(sorti2(Y1), sorti1(sK1_ax3_V), op1(j(Y1), sK1_ax3_V), j(op2(Y1, h(sK1_ax3_V)))) -> j(op2(Y1, h(sK1_ax3_V))) % 14.49/14.24 ifeq2(sorti2(Y1), sorti1(sK1_ax3_V), op1(j(Y1), sK2_ax3_U), j(op2(Y1, h(sK2_ax3_U)))) -> j(op2(Y1, h(sK2_ax3_U))) % 14.49/14.24 ifeq2(sorti2(Y1), sorti1(sK1_ax3_V), op2(Y1, h(sK1_ax3_V)), op2(h(sK1_ax3_V), Y1)) -> op2(h(sK1_ax3_V), Y1) % 14.49/14.24 ifeq2(sorti2(Y1), sorti1(sK1_ax3_V), op2(Y1, h(sK2_ax3_U)), op2(h(sK2_ax3_U), Y1)) -> op2(h(sK2_ax3_U), Y1) % 14.49/14.24 ifeq2(sorti2(Z), true, ifeq2(sorti2(Y), true, op1(j(Y), j(Z)), j(op2(Y, Z))), j(op2(Y, Z))) -> j(op2(Y, Z)) % 14.49/14.24 j(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V))) -> op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U))) -> op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V))) -> op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U))) -> op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V))) -> op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U))) -> op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V))) -> op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U))) -> op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V))) -> op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U))) -> op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V))) -> op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U))) -> op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK1_ax3_V, sK2_ax3_U)))) -> op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK1_ax3_V, sK2_ax3_U)) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK2_ax3_U, sK2_ax3_U)))) -> op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK2_ax3_U, sK2_ax3_U)) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK1_ax3_V), sK1_ax3_V))) -> op1(op1(sK1_ax3_V, sK1_ax3_V), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U))) -> op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V)))) -> op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V)) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U)))) -> op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U)) % 14.49/14.24 j(h(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U)))) -> op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U)) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V))) -> op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U))) -> op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V))) -> op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U))) -> op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V)))) -> op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V)) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U)))) -> op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U)) % 14.49/14.24 j(h(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U)))) -> op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U)) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)))) -> op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)))) -> op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)))) -> op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)))) -> op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))))) -> op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))))) -> op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(sK1_ax3_V, sK1_ax3_V)))) -> op1(sK1_ax3_V, op1(sK1_ax3_V, sK1_ax3_V)) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))))) -> op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))))) -> op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)))) -> op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)))) -> op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)))) -> op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)))) -> op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))))) -> op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))))) -> op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V)))) -> op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V)) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))))) -> op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))) % 14.49/14.24 j(h(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))))) -> op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))) % 14.49/14.24 j(h(sK1_ax3_V)) -> sK1_ax3_V % 14.49/14.24 j(h(sK2_ax3_U)) -> sK2_ax3_U % 14.49/14.24 j(op2(h(sK1_ax3_V), h(sK1_ax3_V))) -> op1(sK1_ax3_V, sK1_ax3_V) % 14.49/14.24 j(op2(h(sK1_ax3_V), h(sK2_ax3_U))) -> op1(sK1_ax3_V, sK2_ax3_U) % 14.49/14.24 j(op2(h(sK1_ax3_V), op2(h(sK1_ax3_V), h(sK2_ax3_U)))) -> op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)) % 14.49/14.24 j(op2(h(sK1_ax3_V), op2(h(sK1_ax3_V), h(sK2_ax3_U)))) -> op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V)) % 14.49/14.24 j(op2(h(sK1_ax3_V), op2(h(sK2_ax3_U), h(sK2_ax3_U)))) -> op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)) % 14.49/14.24 j(op2(h(sK2_ax3_U), h(sK1_ax3_V))) -> op1(sK2_ax3_U, sK1_ax3_V) % 14.49/14.24 j(op2(h(sK2_ax3_U), h(sK2_ax3_U))) -> op1(sK2_ax3_U, sK2_ax3_U) % 14.49/14.24 j(op2(h(sK2_ax3_U), op2(h(sK1_ax3_V), h(sK2_ax3_U)))) -> op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)) % 14.49/14.24 j(op2(h(sK2_ax3_U), op2(h(sK1_ax3_V), h(sK2_ax3_U)))) -> op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V)) % 14.49/14.24 j(op2(h(sK2_ax3_U), op2(h(sK2_ax3_U), h(sK2_ax3_U)))) -> op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)) % 14.49/14.24 j(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK1_ax3_V))) -> op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V) % 14.49/14.24 j(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK1_ax3_V))) -> op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V) % 14.49/14.24 j(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK2_ax3_U))) -> op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U) % 14.49/14.24 j(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK2_ax3_U))) -> op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U) % 14.49/14.24 j(op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(sK1_ax3_V))) -> op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V) % 14.49/14.24 j(op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(sK2_ax3_U))) -> op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U) % 14.49/14.24 op1(sK2_ax3_U, sK1_ax3_V) -> op1(sK1_ax3_V, sK2_ax3_U) % 14.49/14.24 op2(h(sK2_ax3_U), h(sK1_ax3_V)) -> op2(h(sK1_ax3_V), h(sK2_ax3_U)) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK1_ax3_V), sK1_ax3_V), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK1_ax3_V)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK1_ax3_V, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK2_ax3_U, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK1_ax3_V), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK2_ax3_U, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK1_ax3_V), op1(sK1_ax3_V, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK1_ax3_V), op1(sK2_ax3_U, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK1_ax3_V), op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK2_ax3_U, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK1_ax3_V, sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK1_ax3_V), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK1_ax3_V), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK2_ax3_U, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(op1(sK2_ax3_U, sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti1(sK2_ax3_U) -> true % 14.49/14.24 sorti2(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK1_ax3_V), op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK1_ax3_V), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK1_ax3_V), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK1_ax3_V, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U)), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U)), sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK1_ax3_V, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(op1(sK2_ax3_U, sK2_ax3_U), op1(sK2_ax3_U, sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(sK1_ax3_V, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK1_ax3_V, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(op1(sK1_ax3_V, sK2_ax3_U), sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(op1(sK2_ax3_U, sK2_ax3_U), sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK1_ax3_V, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(sK1_ax3_V, op1(sK2_ax3_U, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(sK1_ax3_V, sK1_ax3_V)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK1_ax3_V, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(op1(sK2_ax3_U, op1(sK2_ax3_U, op1(sK2_ax3_U, sK2_ax3_U))))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(sK1_ax3_V)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(h(sK2_ax3_U)) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK1_ax3_V), h(sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK1_ax3_V), h(sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK1_ax3_V), op2(h(sK1_ax3_V), h(sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK1_ax3_V), op2(h(sK2_ax3_U), h(sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK2_ax3_U), h(sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK2_ax3_U), h(sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK2_ax3_U), op2(h(sK1_ax3_V), h(sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(h(sK2_ax3_U), op2(h(sK2_ax3_U), h(sK2_ax3_U)))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(op2(h(sK1_ax3_V), h(sK1_ax3_V)), h(sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(op2(h(sK1_ax3_V), h(sK2_ax3_U)), h(sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(sK1_ax3_V))) -> sorti1(sK1_ax3_V) % 14.49/14.24 sorti2(op2(op2(h(sK2_ax3_U), h(sK2_ax3_U)), h(sK2_ax3_U))) -> sorti1(sK1_ax3_V) % 14.49/14.24 true -> sorti1(sK1_ax3_V) % 14.49/14.24 true__ -> false__ % 14.49/14.24 with the LPO induced by % 14.49/14.24 j > h > sK2_ax3_U > true > sK1_ax3_V > sorti1 > f1 > op2 > sorti2 > op1 > ifeq > ifeq2 > true__ > false__ % 14.49/14.24 % 14.49/14.24 % SZS output end Proof % 14.49/14.24 %------------------------------------------------------------------------------