%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : ALG069-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n023.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:41 EDT 2022 % Result : Unsatisfiable 8.60s 8.63s % Output : Proof 8.60s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ALG069-10 : TPTP v8.1.0. Released v7.3.0. % 0.03/0.13 % Command : moca.sh %s % 0.13/0.34 % Computer : n023.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Wed Jun 8 08:32:38 EDT 2022 % 0.13/0.34 % CPUTime : % 8.60/8.63 % SZS status Unsatisfiable % 8.60/8.63 % SZS output start Proof % 8.60/8.63 The input problem is unsatisfiable because % 8.60/8.63 % 8.60/8.63 [1] the following set of Horn clauses is unsatisfiable: % 8.60/8.63 % 8.60/8.63 ifeq2(A, A, B, C) = B % 8.60/8.63 ifeq(A, A, B, C) = B % 8.60/8.63 ifeq(sorti1(V), true, ifeq(sorti1(U), true, sorti1(op1(U, V)), true), true) = true % 8.60/8.63 ifeq(sorti2(V), true, ifeq(sorti2(U), true, sorti2(op2(U, V)), true), true) = true % 8.60/8.63 ifeq(sorti1(U), true, sorti1(sK2_ax3_V(U)), true) = true % 8.60/8.63 ifeq2(sorti1(U), true, op1(sK2_ax3_V(U), sK2_ax3_V(U)), U) = U % 8.60/8.63 tuple(op2(V, V), sorti2(V)) = tuple(sK1_ax4_U, true) ==> \bottom % 8.60/8.63 sorti2(sK1_ax4_U) = true % 8.60/8.63 ifeq(sorti1(U), true, sorti2(h(U)), true) = true % 8.60/8.63 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)) % 8.60/8.63 ifeq2(sorti1(X2), true, j(h(X2)), X2) = X2 % 8.60/8.63 ifeq(sorti2(V), true, sorti1(j(V)), true) = true % 8.60/8.63 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)) % 8.60/8.63 ifeq2(sorti2(X1), true, h(j(X1)), X1) = X1 % 8.60/8.63 % 8.60/8.63 This holds because % 8.60/8.63 % 8.60/8.63 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 8.60/8.63 % 8.60/8.63 E: % 8.60/8.63 f1(tuple(op2(V, V), sorti2(V))) = true__ % 8.60/8.63 f1(tuple(sK1_ax4_U, true)) = false__ % 8.60/8.63 ifeq(A, A, B, C) = B % 8.60/8.63 ifeq(sorti1(U), true, sorti1(sK2_ax3_V(U)), true) = true % 8.60/8.63 ifeq(sorti1(U), true, sorti2(h(U)), true) = true % 8.60/8.63 ifeq(sorti1(V), true, ifeq(sorti1(U), true, sorti1(op1(U, V)), true), true) = true % 8.60/8.63 ifeq(sorti2(V), true, ifeq(sorti2(U), true, sorti2(op2(U, V)), true), true) = true % 8.60/8.63 ifeq(sorti2(V), true, sorti1(j(V)), true) = true % 8.60/8.63 ifeq2(A, A, B, C) = B % 8.60/8.63 ifeq2(sorti1(U), true, op1(sK2_ax3_V(U), sK2_ax3_V(U)), U) = U % 8.60/8.63 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)) % 8.60/8.63 ifeq2(sorti1(X2), true, j(h(X2)), X2) = X2 % 8.60/8.63 ifeq2(sorti2(X1), true, h(j(X1)), X1) = X1 % 8.60/8.63 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)) % 8.60/8.63 sorti2(sK1_ax4_U) = true % 8.60/8.63 G: % 8.60/8.63 true__ = false__ % 8.60/8.63 % 8.60/8.63 This holds because % 8.60/8.63 % 8.60/8.63 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 8.60/8.63 % 8.60/8.63 % 8.60/8.63 f1(tuple(op2(V, V), sorti2(V))) -> true__ % 8.60/8.63 f1(tuple(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U)), sorti2(sK1_ax4_U))) -> true__ % 8.60/8.63 f1(tuple(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U))), sorti2(sK1_ax4_U))) -> true__ % 8.60/8.63 f1(tuple(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(sK1_ax4_U, sK1_ax4_U)), sorti2(sK1_ax4_U))) -> true__ % 8.60/8.63 f1(tuple(sK1_ax4_U, sorti2(sK1_ax4_U))) -> false__ % 8.60/8.63 f1(tuple(sK1_ax4_U, true)) -> false__ % 8.60/8.63 h(j(sK1_ax4_U)) -> sK1_ax4_U % 8.60/8.63 h(op1(j(sK1_ax4_U), j(sK1_ax4_U))) -> op2(sK1_ax4_U, sK1_ax4_U) % 8.60/8.63 h(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U)))) -> op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)) % 8.60/8.63 h(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) -> op2(sK1_ax4_U, op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 h(op1(j(sK1_ax4_U), op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) -> op2(sK1_ax4_U, op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U)) % 8.60/8.63 h(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U)))) -> op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U)))) % 8.60/8.63 h(op1(j(sK1_ax4_U), sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> op2(sK1_ax4_U, h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 h(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U))) -> op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U) % 8.60/8.63 h(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), sK2_ax3_V(j(sK1_ax4_U)))) -> op2(op2(sK1_ax4_U, sK1_ax4_U), h(sK2_ax3_V(j(sK1_ax4_U)))) % 8.60/8.63 h(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), j(sK1_ax4_U))) -> op2(op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U)))), sK1_ax4_U) % 8.60/8.63 h(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), sK2_ax3_V(j(sK1_ax4_U)))) -> op2(op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U)))), h(sK2_ax3_V(j(sK1_ax4_U)))) % 8.60/8.63 h(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), j(sK1_ax4_U))) -> op2(op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U), sK1_ax4_U) % 8.60/8.63 h(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), sK2_ax3_V(j(sK1_ax4_U)))) -> op2(op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U), h(sK2_ax3_V(j(sK1_ax4_U)))) % 8.60/8.63 h(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U))) -> op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U) % 8.60/8.63 h(op1(sK2_ax3_V(j(sK1_ax4_U)), op1(j(sK1_ax4_U), j(sK1_ax4_U)))) -> op2(h(sK2_ax3_V(j(sK1_ax4_U))), op2(sK1_ax4_U, sK1_ax4_U)) % 8.60/8.63 h(op1(sK2_ax3_V(j(sK1_ax4_U)), op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) -> op2(h(sK2_ax3_V(j(sK1_ax4_U))), op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 h(op1(sK2_ax3_V(j(sK1_ax4_U)), op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) -> op2(h(sK2_ax3_V(j(sK1_ax4_U))), op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U)) % 8.60/8.63 h(op1(sK2_ax3_V(j(sK1_ax4_U)), sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> op2(h(sK2_ax3_V(j(sK1_ax4_U))), h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 h(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), j(sK1_ax4_U))) -> op2(h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))), sK1_ax4_U) % 8.60/8.63 h(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), sK2_ax3_V(j(sK1_ax4_U)))) -> op2(h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))), h(sK2_ax3_V(j(sK1_ax4_U)))) % 8.60/8.63 ifeq(A, A, B, C) -> B % 8.60/8.63 ifeq(sorti1(U), true, sorti1(sK2_ax3_V(U)), true) -> true % 8.60/8.63 ifeq(sorti1(U), true, sorti2(h(U)), true) -> true % 8.60/8.63 ifeq(sorti1(V), true, ifeq(sorti1(U), true, sorti1(op1(U, V)), true), true) -> true % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, Y0)), sorti2(sK1_ax4_U)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(op1(j(sK1_ax4_U), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(op1(sK2_ax3_V(j(sK1_ax4_U)), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti1(sK2_ax3_V(Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y0), sorti2(sK1_ax4_U), sorti2(h(Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, j(sK1_ax4_U))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, op1(j(sK1_ax4_U), j(sK1_ax4_U)))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, sK2_ax3_V(j(sK1_ax4_U)))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti1(Y1), sorti2(sK1_ax4_U), sorti1(op1(Y1, sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(V), true, ifeq(sorti2(U), true, sorti2(op2(U, V)), true), true) -> true % 8.60/8.63 ifeq(sorti2(V), true, sorti1(j(V)), true) -> true % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), ifeq(sorti2(Y1), sorti2(sK1_ax4_U), sorti2(op2(Y1, Y0)), sorti2(sK1_ax4_U)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), sorti1(j(Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), sorti2(op2(h(sK2_ax3_V(j(sK1_ax4_U))), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), sorti2(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), sorti2(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), sorti2(op2(op2(sK1_ax4_U, sK1_ax4_U), Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y0), sorti2(sK1_ax4_U), sorti2(op2(sK1_ax4_U, Y0)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y1), sorti2(sK1_ax4_U), sorti2(op2(Y1, h(sK2_ax3_V(j(sK1_ax4_U))))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y1), sorti2(sK1_ax4_U), sorti2(op2(Y1, op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y1), sorti2(sK1_ax4_U), sorti2(op2(Y1, op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y1), sorti2(sK1_ax4_U), sorti2(op2(Y1, op2(sK1_ax4_U, sK1_ax4_U))), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq(sorti2(Y1), sorti2(sK1_ax4_U), sorti2(op2(Y1, sK1_ax4_U)), sorti2(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 ifeq2(A, A, B, C) -> B % 8.60/8.63 ifeq2(sorti1(U), true, op1(sK2_ax3_V(U), sK2_ax3_V(U)), U) -> U % 8.60/8.63 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)) % 8.60/8.63 ifeq2(sorti1(X2), true, j(h(X2)), X2) -> X2 % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), h(Y0)), h(op1(Y1, Y0))), h(op1(Y1, Y0))) -> h(op1(Y1, Y0)) % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), j(h(Y0)), Y0) -> Y0 % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op1(sK2_ax3_V(Y0), sK2_ax3_V(Y0)), Y0) -> Y0 % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op2(h(sK2_ax3_V(j(sK1_ax4_U))), h(Y0)), h(op1(sK2_ax3_V(j(sK1_ax4_U)), Y0))) -> h(op1(sK2_ax3_V(j(sK1_ax4_U)), Y0)) % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op2(h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))), h(Y0)), h(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), Y0))) -> h(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), Y0)) % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op2(op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U), h(Y0)), h(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), Y0))) -> h(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), Y0)) % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op2(op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U)))), h(Y0)), h(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), Y0))) -> h(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), Y0)) % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op2(op2(sK1_ax4_U, sK1_ax4_U), h(Y0)), h(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), Y0))) -> h(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), Y0)) % 8.60/8.63 ifeq2(sorti1(Y0), sorti2(sK1_ax4_U), op2(sK1_ax4_U, h(Y0)), h(op1(j(sK1_ax4_U), Y0))) -> h(op1(j(sK1_ax4_U), Y0)) % 8.60/8.63 ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), h(sK2_ax3_V(j(sK1_ax4_U)))), h(op1(Y1, sK2_ax3_V(j(sK1_ax4_U))))) -> h(op1(Y1, sK2_ax3_V(j(sK1_ax4_U)))) % 8.60/8.63 ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))), h(op1(Y1, sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))))) -> h(op1(Y1, sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U)), h(op1(Y1, op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U))))) -> h(op1(Y1, op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) % 8.60/8.63 ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U))))), h(op1(Y1, op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U)))))) -> h(op1(Y1, op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), op2(sK1_ax4_U, sK1_ax4_U)), h(op1(Y1, op1(j(sK1_ax4_U), j(sK1_ax4_U))))) -> h(op1(Y1, op1(j(sK1_ax4_U), j(sK1_ax4_U)))) % 8.60/8.63 ifeq2(sorti1(Y1), sorti2(sK1_ax4_U), op2(h(Y1), sK1_ax4_U), h(op1(Y1, j(sK1_ax4_U)))) -> h(op1(Y1, j(sK1_ax4_U))) % 8.60/8.63 ifeq2(sorti2(X1), true, h(j(X1)), X1) -> X1 % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), h(j(Y0)), Y0) -> Y0 % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), ifeq2(sorti2(Y1), sorti2(sK1_ax4_U), op1(j(Y1), j(Y0)), j(op2(Y1, Y0))), j(op2(Y1, Y0))) -> j(op2(Y1, Y0)) % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), op1(j(sK1_ax4_U), j(Y0)), j(op2(sK1_ax4_U, Y0))) -> j(op2(sK1_ax4_U, Y0)) % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(Y0)), j(op2(op2(sK1_ax4_U, sK1_ax4_U), Y0))) -> j(op2(op2(sK1_ax4_U, sK1_ax4_U), Y0)) % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), op1(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U))), j(Y0)), j(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), Y0))) -> j(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), Y0)) % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), op1(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U)), j(Y0)), j(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), Y0))) -> j(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), Y0)) % 8.60/8.63 ifeq2(sorti2(Y0), sorti2(sK1_ax4_U), op1(sK2_ax3_V(j(sK1_ax4_U)), j(Y0)), j(op2(h(sK2_ax3_V(j(sK1_ax4_U))), Y0))) -> j(op2(h(sK2_ax3_V(j(sK1_ax4_U))), Y0)) % 8.60/8.63 ifeq2(sorti2(Y1), sorti2(sK1_ax4_U), op1(j(Y1), j(sK1_ax4_U)), j(op2(Y1, sK1_ax4_U))) -> j(op2(Y1, sK1_ax4_U)) % 8.60/8.63 ifeq2(sorti2(Y1), sorti2(sK1_ax4_U), op1(j(Y1), op1(j(sK1_ax4_U), j(sK1_ax4_U))), j(op2(Y1, op2(sK1_ax4_U, sK1_ax4_U)))) -> j(op2(Y1, op2(sK1_ax4_U, sK1_ax4_U))) % 8.60/8.63 ifeq2(sorti2(Y1), sorti2(sK1_ax4_U), op1(j(Y1), op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U)))), j(op2(Y1, op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U))))) -> j(op2(Y1, op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)))) % 8.60/8.63 ifeq2(sorti2(Y1), sorti2(sK1_ax4_U), op1(j(Y1), op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U))), j(op2(Y1, op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U)))) -> j(op2(Y1, op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U))) % 8.60/8.63 ifeq2(sorti2(Y1), sorti2(sK1_ax4_U), op1(j(Y1), sK2_ax3_V(j(sK1_ax4_U))), j(op2(Y1, h(sK2_ax3_V(j(sK1_ax4_U)))))) -> j(op2(Y1, h(sK2_ax3_V(j(sK1_ax4_U))))) % 8.60/8.63 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)) % 8.60/8.63 j(h(sK2_ax3_V(j(sK1_ax4_U)))) -> sK2_ax3_V(j(sK1_ax4_U)) % 8.60/8.63 j(h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))) % 8.60/8.63 j(op2(h(sK2_ax3_V(j(sK1_ax4_U))), op2(sK1_ax4_U, sK1_ax4_U))) -> op1(sK2_ax3_V(j(sK1_ax4_U)), op1(j(sK1_ax4_U), j(sK1_ax4_U))) % 8.60/8.63 j(op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U)) -> op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)) % 8.60/8.63 j(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), op2(sK1_ax4_U, sK1_ax4_U))) -> op1(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U)), op1(j(sK1_ax4_U), j(sK1_ax4_U))) % 8.60/8.63 j(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), sK1_ax4_U)) -> op1(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U)), j(sK1_ax4_U)) % 8.60/8.63 j(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), op2(sK1_ax4_U, sK1_ax4_U))) -> op1(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U))), op1(j(sK1_ax4_U), j(sK1_ax4_U))) % 8.60/8.63 j(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), sK1_ax4_U)) -> op1(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U))), j(sK1_ax4_U)) % 8.60/8.63 j(op2(op2(sK1_ax4_U, sK1_ax4_U), h(sK2_ax3_V(j(sK1_ax4_U))))) -> op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), sK2_ax3_V(j(sK1_ax4_U))) % 8.60/8.63 j(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U))) -> op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U))) % 8.60/8.63 j(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)))) -> op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U)))) % 8.60/8.63 j(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(sK1_ax4_U, sK1_ax4_U))) -> op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), op1(j(sK1_ax4_U), j(sK1_ax4_U))) % 8.60/8.63 j(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U)) -> op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U)) % 8.60/8.63 j(op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U))))) -> op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))) % 8.60/8.63 j(op2(sK1_ax4_U, op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U))) -> op1(j(sK1_ax4_U), op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U))) % 8.60/8.63 j(op2(sK1_ax4_U, op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)))) -> op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U)))) % 8.60/8.63 j(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U))) -> op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U))) % 8.60/8.63 j(op2(sK1_ax4_U, sK1_ax4_U)) -> op1(j(sK1_ax4_U), j(sK1_ax4_U)) % 8.60/8.63 op1(sK2_ax3_V(j(sK1_ax4_U)), sK2_ax3_V(j(sK1_ax4_U))) -> j(sK1_ax4_U) % 8.60/8.63 op1(sK2_ax3_V(op1(j(sK1_ax4_U), j(sK1_ax4_U))), sK2_ax3_V(op1(j(sK1_ax4_U), j(sK1_ax4_U)))) -> op1(j(sK1_ax4_U), j(sK1_ax4_U)) % 8.60/8.63 op1(sK2_ax3_V(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U)))), sK2_ax3_V(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) -> op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))) % 8.60/8.63 op1(sK2_ax3_V(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U))), sK2_ax3_V(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) -> op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)) % 8.60/8.63 op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))) -> sK2_ax3_V(j(sK1_ax4_U)) % 8.60/8.63 op1(sK2_ax3_V(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))), sK2_ax3_V(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))) % 8.60/8.63 op2(h(sK2_ax3_V(j(sK1_ax4_U))), h(sK2_ax3_V(j(sK1_ax4_U)))) -> sK1_ax4_U % 8.60/8.63 op2(h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))), h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> h(sK2_ax3_V(j(sK1_ax4_U))) % 8.60/8.63 sorti1(j(sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(j(sK1_ax4_U), j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(j(sK1_ax4_U), op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(j(sK1_ax4_U), op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(j(sK1_ax4_U), sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(op1(j(sK1_ax4_U), j(sK1_ax4_U)), sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))), sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)), sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(j(sK1_ax4_U)), op1(j(sK1_ax4_U), j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(j(sK1_ax4_U)), op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(j(sK1_ax4_U)), op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(j(sK1_ax4_U)), sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(op1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))), sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(sK2_ax3_V(j(sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(sK2_ax3_V(op1(j(sK1_ax4_U), j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(sK2_ax3_V(op1(j(sK1_ax4_U), sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(sK2_ax3_V(op1(sK2_ax3_V(j(sK1_ax4_U)), j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti1(sK2_ax3_V(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(h(sK2_ax3_V(j(sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(h(sK2_ax3_V(sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(h(sK2_ax3_V(j(sK1_ax4_U))), op2(sK1_ax4_U, sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(h(sK2_ax3_V(j(sK1_ax4_U))), sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), op2(sK1_ax4_U, sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U), sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), op2(sK1_ax4_U, sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)), sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, sK1_ax4_U), h(sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, sK1_ax4_U), op2(sK1_ax4_U, sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(sK1_ax4_U, h(sK2_ax3_V(j(sK1_ax4_U))))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(sK1_ax4_U, op2(op2(sK1_ax4_U, sK1_ax4_U), sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(sK1_ax4_U, op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U)))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(sK1_ax4_U, op2(sK1_ax4_U, sK1_ax4_U))) -> sorti2(sK1_ax4_U) % 8.60/8.63 sorti2(op2(sK1_ax4_U, sK1_ax4_U)) -> sorti2(sK1_ax4_U) % 8.60/8.63 true -> sorti2(sK1_ax4_U) % 8.60/8.63 true__ -> false__ % 8.60/8.63 with the LPO induced by % 8.60/8.63 j > h > true > sK1_ax4_U > tuple > f1 > sK2_ax3_V > op2 > sorti2 > op1 > ifeq > sorti1 > ifeq2 > true__ > false__ % 8.60/8.63 % 8.60/8.63 % SZS output end Proof % 8.60/8.63 %------------------------------------------------------------------------------