%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : SWX204-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n021.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 May 5 07:04:54 PM UTC 2026 % Result : Unsatisfiable 5.09s 5.04s % Output : Proof 5.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : SWX204-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : moca.sh %s % 0.17/0.33 % Computer : n021.cluster.edu % 0.17/0.33 % Model : x86_64 x86_64 % 0.17/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.17/0.33 % Memory : 8042.1875MB % 0.17/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.17/0.33 % CPULimit : 300 % 0.17/0.33 % WCLimit : 300 % 0.17/0.33 % DateTime : Tue May 5 11:30:40 EDT 2026 % 0.17/0.33 % CPUTime : % 5.09/5.04 % SZS status Unsatisfiable % 5.09/5.04 % SZS output start Proof % 5.09/5.04 The input problem is unsatisfiable because % 5.09/5.04 % 5.09/5.04 [1] the following set of Horn clauses is unsatisfiable: % 5.09/5.04 % 5.09/5.04 x2(z, Y) = Y % 5.09/5.04 x2(s(N), Y) = s(x2(N, Y)) % 5.09/5.04 x22(z, Y) = z % 5.09/5.04 x22(s(N), Y) = x2(Y, x22(N, Y)) % 5.09/5.04 mul_idem(X) = eq(x22(X, X), X) % 5.09/5.04 eq2(bfalse, btrue) = bfalse % 5.09/5.04 eq2(btrue, bfalse) = bfalse % 5.09/5.04 eq(s(X), s(Y)) = eq(X, Y) % 5.09/5.04 eq(z, s(X)) = bfalse % 5.09/5.04 eq(s(X), z) = bfalse % 5.09/5.04 eq(X, X) = btrue % 5.09/5.04 eq2(X, X) = btrue % 5.09/5.04 eq2(mul_idem(X), bfalse) = btrue ==> \bottom % 5.09/5.04 % 5.09/5.04 This holds because % 5.09/5.04 % 5.09/5.04 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 5.09/5.04 % 5.09/5.04 E: % 5.09/5.04 eq(X, X) = btrue % 5.09/5.04 eq(s(X), s(Y)) = eq(X, Y) % 5.09/5.04 eq(s(X), z) = bfalse % 5.09/5.04 eq(z, s(X)) = bfalse % 5.09/5.04 eq2(X, X) = btrue % 5.09/5.04 eq2(bfalse, btrue) = bfalse % 5.09/5.04 eq2(btrue, bfalse) = bfalse % 5.09/5.04 f1(btrue) = false__ % 5.09/5.04 f1(eq2(mul_idem(X), bfalse)) = true__ % 5.09/5.04 mul_idem(X) = eq(x22(X, X), X) % 5.09/5.04 x2(s(N), Y) = s(x2(N, Y)) % 5.09/5.04 x2(z, Y) = Y % 5.09/5.04 x22(s(N), Y) = x2(Y, x22(N, Y)) % 5.09/5.04 x22(z, Y) = z % 5.09/5.04 G: % 5.09/5.04 true__ = false__ % 5.09/5.04 % 5.09/5.04 This holds because % 5.09/5.04 % 5.09/5.04 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 5.09/5.04 % 5.09/5.04 eq(x2(Y0, x22(Y0, x2(s(z), Y0))), Y0) = mul_idem(s(Y0)) % 5.09/5.04 eq(x2(x2(X0, X1), x22(x2(X0, X1), x2(s(X0), X1))), x2(X0, X1)) = mul_idem(x2(s(z), x2(X0, X1))) % 5.09/5.04 s(Y1) = x2(s(z), Y1) % 5.09/5.04 x2(s(z), s(Y1)) = x2(x2(s(z), s(z)), Y1) % 5.09/5.04 x2(s(z), x2(Y0, Y1)) = x2(s(Y0), Y1) % 5.09/5.04 x2(x2(s(X0), X1), Y1) = x2(s(z), x2(x2(X0, X1), Y1)) % 5.09/5.04 x2(x2(x2(s(X0), X1), Y1), Y2) = x2(s(z), x2(x2(x2(X0, X1), Y1), Y2)) % 5.09/5.04 eq(X, X) -> btrue % 5.09/5.04 eq(s(X), s(Y)) -> eq(X, Y) % 5.09/5.04 eq(s(X), z) -> bfalse % 5.09/5.04 eq(s(Y0), x2(s(X0), X1)) -> eq(Y0, x2(X0, X1)) % 5.09/5.04 eq(s(Y0), x2(x2(s(X0), X1), Y2)) -> eq(Y0, x2(x2(X0, X1), Y2)) % 5.09/5.04 eq(x2(X0, x2(s(z), x2(s(X0), x22(X0, x2(s(z), s(X0)))))), X0) -> mul_idem(x2(s(z), s(X0))) % 5.09/5.04 eq(x2(X0, x2(s(z), x2(s(z), x2(X0, x22(X0, x2(s(z), x2(s(z), X0))))))), X0) -> mul_idem(x2(s(z), x2(s(z), X0))) % 5.09/5.04 eq(x2(X0, x22(X0, x2(s(z), X0))), X0) -> mul_idem(x2(s(z), X0)) % 5.09/5.04 eq(x2(Y0, x22(Y0, s(Y0))), Y0) -> mul_idem(s(Y0)) % 5.09/5.04 eq(x2(s(X0), X1), s(Y1)) -> eq(x2(X0, X1), Y1) % 5.09/5.04 eq(x2(s(X0), X1), z) -> bfalse % 5.09/5.04 eq(x2(s(X0), x22(X0, s(X0))), s(X0)) -> mul_idem(s(X0)) % 5.09/5.04 eq(x2(s(Y0), Y1), x2(s(X0), X1)) -> eq(x2(Y0, Y1), x2(X0, X1)) % 5.09/5.04 eq(x2(s(Y0), Y1), x2(s(z), Y2)) -> eq(x2(Y0, Y1), Y2) % 5.09/5.04 eq(x2(s(z), Y0), x2(s(Y1), Y2)) -> eq(Y0, x2(Y1, Y2)) % 5.09/5.04 eq(x2(s(z), Y0), x2(x2(s(Y1), Y2), Y3)) -> eq(Y0, x2(x2(Y1, Y2), Y3)) % 5.09/5.04 eq(x2(x2(s(X0), X1), Y1), s(Y2)) -> eq(x2(x2(X0, X1), Y1), Y2) % 5.09/5.04 eq(x2(x2(s(X0), X1), Y1), z) -> bfalse % 5.09/5.04 eq(x2(x2(s(X0), X1), x22(x2(X0, X1), x2(s(X0), X1))), x2(s(X0), X1)) -> mul_idem(x2(s(X0), X1)) % 5.09/5.04 eq(x2(x2(s(Y0), Y1), Y2), x2(s(z), Y3)) -> eq(x2(x2(Y0, Y1), Y2), Y3) % 5.09/5.04 eq(x2(x2(s(z), Y0), Y1), s(Y2)) -> eq(x2(Y0, Y1), Y2) % 5.09/5.04 eq(x2(x2(s(z), Y0), Y1), z) -> bfalse % 5.09/5.04 eq(x2(x2(x2(s(X0), X1), X2), x22(x2(x2(X0, X1), X2), x2(x2(s(X0), X1), X2))), x2(x2(s(X0), X1), X2)) -> mul_idem(x2(x2(s(X0), X1), X2)) % 5.09/5.04 eq(x2(x2(x2(s(X0), X1), Y1), Y2), s(Y3)) -> eq(x2(x2(x2(X0, X1), Y1), Y2), Y3) % 5.09/5.04 eq(x2(x2(x2(s(X0), X1), Y1), Y2), z) -> bfalse % 5.09/5.04 eq(x2(x2(x2(x2(s(X0), X1), Y1), Y2), Y3), z) -> bfalse % 5.09/5.04 eq(x2(x2(x2(x2(x2(s(X0), X1), Y1), Y2), Y3), Y4), z) -> bfalse % 5.09/5.04 eq(x2(x2(x2(x2(x2(x2(s(X0), X1), Y1), Y2), Y3), Y4), Y5), z) -> bfalse % 5.09/5.04 eq(x22(X, X), X) -> mul_idem(X) % 5.09/5.04 eq(z, s(X)) -> bfalse % 5.09/5.04 eq(z, x2(s(X0), X1)) -> bfalse % 5.09/5.04 eq(z, x2(x2(s(X0), X1), Y1)) -> bfalse % 5.09/5.04 eq(z, x2(x2(s(z), Y0), Y1)) -> bfalse % 5.09/5.04 eq(z, x2(x2(x2(s(X0), X1), Y1), Y2)) -> bfalse % 5.09/5.04 eq(z, x2(x2(x2(x2(s(X0), X1), Y1), Y2), Y3)) -> bfalse % 5.09/5.04 eq(z, x2(x2(x2(x2(x2(s(X0), X1), Y1), Y2), Y3), Y4)) -> bfalse % 5.09/5.04 eq(z, x2(x2(x2(x2(x2(x2(s(X0), X1), Y1), Y2), Y3), Y4), Y5)) -> bfalse % 5.09/5.04 eq2(X, X) -> btrue % 5.09/5.04 eq2(bfalse, btrue) -> bfalse % 5.09/5.04 eq2(btrue, bfalse) -> bfalse % 5.09/5.04 f1(bfalse) -> true__ % 5.09/5.04 f1(btrue) -> false__ % 5.09/5.04 f1(eq2(mul_idem(X), bfalse)) -> true__ % 5.09/5.04 mul_idem(s(z)) -> btrue % 5.09/5.04 mul_idem(x2(s(z), s(z))) -> bfalse % 5.09/5.04 mul_idem(z) -> btrue % 5.09/5.04 s(x2(N, Y)) -> x2(s(N), Y) % 5.09/5.04 true__ -> false__ % 5.09/5.04 x2(x2(s(z), Y0), Y1) -> x2(s(z), x2(Y0, Y1)) % 5.09/5.04 x2(x2(s(z), s(z)), Y0) -> x2(s(z), x2(s(z), Y0)) % 5.09/5.04 x2(z, Y) -> Y % 5.09/5.04 x22(s(N), Y) -> x2(Y, x22(N, Y)) % 5.09/5.04 x22(x2(s(X0), X1), Y1) -> x2(Y1, x22(x2(X0, X1), Y1)) % 5.09/5.04 x22(x2(s(z), Y0), Y1) -> x2(Y1, x22(Y0, Y1)) % 5.09/5.04 x22(x2(x2(s(X0), X1), Y1), Y2) -> x2(Y2, x22(x2(x2(X0, X1), Y1), Y2)) % 5.09/5.04 x22(z, Y) -> z % 5.09/5.04 with the LPO induced by % 5.09/5.04 f1 > s > bfalse > eq2 > eq > mul_idem > btrue > x22 > x2 > z > true__ > false__ % 5.09/5.04 % 5.09/5.04 % SZS output end Proof % 5.09/5.04 %------------------------------------------------------------------------------