%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : MSC014-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n001.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 : Tue Jul 15 07:20:30 AM UTC 2025 % Result : Satisfiable 1.03s 1.20s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : MSC014-10 : TPTP v9.0.0. Released v7.5.0. % 0.07/0.13 % Command : run_Leo-III %s %d THM % 0.13/0.35 % Computer : n001.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Jul 14 14:05:04 EDT 2025 % 0.13/0.35 % CPUTime : % 1.03/1.20 % SZS status Satisfiable % 1.03/1.20 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 1.03/1.20 1: equalish(n0, n0) -> true % 1.03/1.20 2: equalish(n1, n1) -> true % 1.03/1.20 3: ifeq2(X, X, Y, Z) -> Y % 1.03/1.20 4: ifeq(X, X, Y, Z) -> Y % 1.03/1.20 5: ifeq(equalish(n0, n1), true, a, b) -> b % 1.03/1.20 6: ifeq(equalish(n1, n0), true, a, b) -> b % 1.03/1.20 7: ifeq2(f(X, Y, Z, W, V), true, ifeq2(f(U, U2, U3, U4, V), true, equalish(U2, Y), true), true) -> true % 1.03/1.20 8: ifeq2(f(X, n0, Y, Z, W), true, ifeq2(f(V, n0, U, U2, W), true, true, true), true) -> true % 1.03/1.20 9: ifeq2(f(X, n1, Y, Z, W), true, ifeq2(f(V, n1, U, U2, W), true, true, true), true) -> true % 1.03/1.20 10: ifeq2(f(X, Y, Z, W, V), true, ifeq2(f(U, U2, U3, U4, V), true, equalish(U, X), true), true) -> true % 1.03/1.20 11: ifeq2(f(n0, X, Y, Z, W), true, ifeq2(f(n0, V, U, U2, W), true, true, true), true) -> true % 1.03/1.20 12: ifeq2(f(n1, X, Y, Z, W), true, ifeq2(f(n1, V, U, U2, W), true, true, true), true) -> true % 1.03/1.20 13: ifeq2(f(X, Y, Z, W, V), true, ifeq2(f(U, U2, U3, U4, V), true, equalish(U4, W), true), true) -> true % 1.03/1.20 14: ifeq2(f(X, Y, Z, n0, W), true, ifeq2(f(V, U, U2, n0, W), true, true, true), true) -> true % 1.03/1.20 15: ifeq2(f(X, Y, Z, n1, W), true, ifeq2(f(V, U, U2, n1, W), true, true, true), true) -> true % 1.03/1.20 16: ifeq2(f(X, Y, Z, W, V), true, ifeq2(f(U, U2, U3, U4, V), true, equalish(U3, Z), true), true) -> true % 1.03/1.20 17: ifeq2(f(X, Y, n0, Z, W), true, ifeq2(f(V, U, n0, U2, W), true, true, true), true) -> true % 1.03/1.20 18: ifeq2(f(X, Y, n1, Z, W), true, ifeq2(f(V, U, n1, U2, W), true, true, true), true) -> true % 1.03/1.20 19: ifeq2(equalish(X, X), true, ifeq2(equalish(Y, Y), true, ifeq2(equalish(Z, Z), true, ifeq2(equalish(W, W), true, f(W, Z, Y, X, sK1_exists_f_Z(W, Z, Y, X)), true), true), true), true) -> true % 1.03/1.20 20: ifeq2(equalish(X, X), true, ifeq2(equalish(Y, Y), true, ifeq2(equalish(Z, Z), true, f(Z, Y, X, n0, sK1_exists_f_Z(Z, Y, X, n0)), true), true), true) -> true % 1.03/1.20 21: ifeq2(equalish(X, X), true, ifeq2(equalish(Y, Y), true, f(Y, X, n0, n0, sK1_exists_f_Z(Y, X, n0, n0)), true), true) -> true % 1.03/1.20 22: ifeq2(equalish(X, X), true, f(X, n0, n0, n0, sK1_exists_f_Z(X, n0, n0, n0)), true) -> true % 1.03/1.20 23: true -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 24: f(n1, n0, n0, n0, sK1_exists_f_Z(n1, n0, n0, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 25: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n1, n0, n0, sK1_exists_f_Z(X, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 26: f(n0, n1, n0, n0, sK1_exists_f_Z(n0, n1, n0, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 27: f(n1, n1, n0, n0, sK1_exists_f_Z(n1, n1, n0, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 28: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, X, n0, n0, sK1_exists_f_Z(n0, X, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 29: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, X, n0, n0, sK1_exists_f_Z(n1, X, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 30: ifeq(equalish(n1, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), a, b) -> b % 1.03/1.20 31: ifeq(equalish(n0, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), a, b) -> b % 1.03/1.20 32: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, X, n1, n0, sK1_exists_f_Z(Y, X, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 33: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n0, X, n0, sK1_exists_f_Z(Y, n0, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 34: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n1, X, n0, sK1_exists_f_Z(Y, n1, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 35: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, Y, X, n0, sK1_exists_f_Z(n0, Y, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 36: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, Y, X, n0, sK1_exists_f_Z(n1, Y, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 37: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Z, Y, X, n1, sK1_exists_f_Z(Z, Y, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 38: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Z, Y, n0, X, sK1_exists_f_Z(Z, Y, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 39: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Z, Y, n1, X, sK1_exists_f_Z(Z, Y, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 40: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Z, n0, Y, X, sK1_exists_f_Z(Z, n0, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 41: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Z, n1, Y, X, sK1_exists_f_Z(Z, n1, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 42: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, Z, Y, X, sK1_exists_f_Z(n0, Z, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 43: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, Z, Y, X, sK1_exists_f_Z(n1, Z, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 44: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n1, X, n0, sK1_exists_f_Z(n0, n1, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 45: f(n0, n1, n1, n0, sK1_exists_f_Z(n0, n1, n1, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 46: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n0, X, n0, sK1_exists_f_Z(n1, n0, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 47: f(n1, n0, n1, n0, sK1_exists_f_Z(n1, n0, n1, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 48: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, X, n0, sK1_exists_f_Z(n0, n0, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 49: f(n0, n0, n1, n0, sK1_exists_f_Z(n0, n0, n1, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 50: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, X, n1, n0, sK1_exists_f_Z(n1, X, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 51: f(n1, n1, n1, n0, sK1_exists_f_Z(n1, n1, n1, n0)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 52: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n0, n1, n0, sK1_exists_f_Z(X, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 53: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n1, X, n0, sK1_exists_f_Z(n1, n1, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 54: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n1, n1, n0, sK1_exists_f_Z(X, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 55: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, X, n1, n0, sK1_exists_f_Z(n0, X, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 56: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n0, n0, n0, sK1_exists_f_Z(X, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 57: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 58: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 59: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 60: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 61: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 62: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 63: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 64: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 65: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 66: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 67: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 68: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 69: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 70: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 71: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 72: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 73: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 74: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 75: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 76: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 77: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 78: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 79: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 80: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 81: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 82: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 83: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 84: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 85: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 86: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 87: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 88: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 89: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 90: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 91: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 92: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 93: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 94: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 95: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 96: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 97: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 98: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 99: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 100: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 101: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 102: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 103: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 104: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 105: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 106: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 107: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 108: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 109: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 110: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 111: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 112: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 113: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 114: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 115: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 116: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 117: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 118: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 119: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 120: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 121: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 122: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 123: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 124: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 125: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 126: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 127: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 128: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 129: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 130: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 131: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 132: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 133: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 134: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 135: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 136: ifeq2(f(X, Y, Z, n0, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 137: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 138: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 139: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 140: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 141: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, Y, n1, X, sK1_exists_f_Z(n0, Y, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 142: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, X, n1, n1, sK1_exists_f_Z(n0, X, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 143: f(n0, n0, n1, n1, sK1_exists_f_Z(n0, n0, n1, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 144: f(n0, n1, n1, n1, sK1_exists_f_Z(n0, n1, n1, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 145: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n1, X, sK1_exists_f_Z(n0, n0, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 146: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n1, n1, X, sK1_exists_f_Z(n0, n1, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 147: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 148: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 149: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 150: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 151: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 152: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 153: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 154: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 155: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 156: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 157: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 158: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 159: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 160: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 161: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 162: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 163: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 164: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 165: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 166: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 167: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 168: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 169: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 170: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 171: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n1, Y, X, sK1_exists_f_Z(n0, n1, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 172: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n1, X, n1, sK1_exists_f_Z(n0, n1, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 173: f(n0, n1, n0, n1, sK1_exists_f_Z(n0, n1, n0, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 174: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n1, n0, X, sK1_exists_f_Z(n0, n1, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 175: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 176: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 177: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 178: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 179: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 180: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 181: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 182: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 183: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 184: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 185: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 186: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 187: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, X, n1, n1, sK1_exists_f_Z(Y, X, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 188: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n0, n1, n1, sK1_exists_f_Z(X, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 189: f(n1, n0, n1, n1, sK1_exists_f_Z(n1, n0, n1, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 190: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n1, n1, n1, sK1_exists_f_Z(X, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 191: f(n1, n1, n1, n1, sK1_exists_f_Z(n1, n1, n1, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 192: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, X, n1, n1, sK1_exists_f_Z(n1, X, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 193: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 194: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 195: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 196: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 197: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 198: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 199: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 200: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 201: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 202: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 203: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 204: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 205: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 206: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 207: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 208: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 209: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 210: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 211: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 212: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 213: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 214: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 215: ifeq2(f(X, Y, n1, Z, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 216: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 217: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, Y, X, sK1_exists_f_Z(n0, n0, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 218: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, X, n1, sK1_exists_f_Z(n0, n0, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 219: f(n0, n0, n0, n1, sK1_exists_f_Z(n0, n0, n0, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 220: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, X, sK1_exists_f_Z(n0, n0, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 221: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 222: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 223: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 224: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 225: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 226: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 227: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 228: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 229: ifeq2(f(n0, X, Y, Z, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 230: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 231: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 232: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 233: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n0, Y, X, sK1_exists_f_Z(n1, n0, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 234: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n0, X, n1, sK1_exists_f_Z(n1, n0, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 235: f(n1, n0, n0, n1, sK1_exists_f_Z(n1, n0, n0, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 236: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n0, n0, X, sK1_exists_f_Z(n1, n0, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 237: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n0, n1, X, sK1_exists_f_Z(n1, n0, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 238: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 239: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 240: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 241: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 242: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 243: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 244: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 245: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 246: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 247: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 248: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 249: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 250: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n0, X, n1, sK1_exists_f_Z(Y, n0, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 251: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n0, n0, n1, sK1_exists_f_Z(X, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 252: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n1, n1, X, sK1_exists_f_Z(Y, n1, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 253: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n1, n1, X, sK1_exists_f_Z(n1, n1, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 254: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n1, n0, X, sK1_exists_f_Z(Y, n1, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 255: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(X, n1, n0, n1, sK1_exists_f_Z(X, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 256: f(n1, n1, n0, n1, sK1_exists_f_Z(n1, n1, n0, n1)) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 257: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n1, n0, X, sK1_exists_f_Z(n1, n1, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 258: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 259: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 260: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 261: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 262: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 263: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 264: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n1, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 265: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n1), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 266: ifeq2(f(n1, X, Y, Z, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 267: ifeq2(f(X, n1, Y, Z, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 268: ifeq2(f(X, Y, n0, Z, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 269: ifeq2(f(X, Y, Z, n1, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 270: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n1, X, n1, sK1_exists_f_Z(Y, n1, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 271: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n1, X, n1, sK1_exists_f_Z(n1, n1, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 272: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n0, n1, X, sK1_exists_f_Z(Y, n0, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 273: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, n1, Y, X, sK1_exists_f_Z(n1, n1, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 274: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, X, n0, n1, sK1_exists_f_Z(Y, X, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 275: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, X, n0, n1, sK1_exists_f_Z(n0, X, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 276: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, X, n0, n1, sK1_exists_f_Z(n1, X, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 277: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, X, n0, n0, sK1_exists_f_Z(Y, X, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 278: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Y, n0, n0, X, sK1_exists_f_Z(Y, n0, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 279: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, Y, n0, X, sK1_exists_f_Z(n0, Y, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 280: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, Y, X, n1, sK1_exists_f_Z(n0, Y, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 281: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, Y, n1, X, sK1_exists_f_Z(n1, Y, n1, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 282: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, Y, n0, X, sK1_exists_f_Z(n1, Y, n0, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 283: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n1, Y, X, n1, sK1_exists_f_Z(n1, Y, X, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 284: ifeq2(f(X, Y, Z, W, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(U, U2, U3, U4, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(U2, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 285: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Y, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 286: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 287: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 288: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 289: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 290: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 291: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 292: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 293: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 294: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n1)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 295: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 296: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 297: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 298: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 299: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 300: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 301: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n1, n1, n1, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 302: ifeq2(f(X, n0, Y, Z, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 303: ifeq2(f(X, Y, Z, W, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(U, U2, U3, U4, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(U, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 304: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(X, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 305: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 306: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 307: ifeq2(f(X, Y, Z, W, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(U, U2, U3, U4, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(U3, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 308: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(Z, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 309: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 310: ifeq2(f(X, Y, Z, W, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(U, U2, U3, U4, V), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(U4, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 311: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(W, n0), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 312: ifeq2(f(X, Y, Z, W, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), equalish(n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 313: ifeq2(f(X, Y, Z, n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(V, U, U2, n0, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 314: ifeq2(f(X, n1, Y, Z, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(V, n1, U, U2, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 315: ifeq2(f(X, n0, Y, Z, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(V, n0, U, U2, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 316: ifeq2(f(X, Y, Z, n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(V, U, U2, n1, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 317: ifeq2(f(X, Y, n0, Z, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(V, U, n0, U2, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 318: ifeq2(f(n0, X, Y, Z, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(n0, V, U, U2, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 319: ifeq2(f(n1, X, Y, Z, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(n1, V, U, U2, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 320: ifeq2(f(X, Y, n1, Z, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(f(V, U, n1, U2, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 321: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(Z, Y, X, n0, sK1_exists_f_Z(Z, Y, X, n0)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 322: ifeq2(equalish(X, X), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Y, Y), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(Z, Z), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), ifeq2(equalish(W, W), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)), f(W, Z, Y, X, sK1_exists_f_Z(W, Z, Y, X)), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))), f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0))) -> f(n0, n0, n0, n0, sK1_exists_f_Z(n0, n0, n0, n0)) % 1.03/1.20 %------------------------------------------------------------------------------