%------------------------------------------------------------------------------ % File : Moca---0.1 % Problem : SWX200-1 : TPTP v9.3.0. Released v9.3.0. % Transfm : none % Format : tptp:raw % Command : moca.sh %s % Computer : n015.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 11.24s 11.22s % Output : Proof 11.24s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWX200-1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % Command : moca.sh %s % 0.16/0.33 % Computer : n015.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.33 % CPULimit : 300 % 0.16/0.33 % WCLimit : 300 % 0.16/0.33 % DateTime : Tue May 5 11:16:16 EDT 2026 % 0.16/0.33 % CPUTime : % 11.24/11.22 % SZS status Unsatisfiable % 11.24/11.22 % SZS output start Proof % 11.24/11.22 The input problem is unsatisfiable because % 11.24/11.22 % 11.24/11.22 [1] the following set of Horn clauses is unsatisfiable: % 11.24/11.22 % 11.24/11.22 aux(Z, Xs, Y2, Ys, btrue) = cons(Z, merge(Xs, cons(Y2, Ys))) % 11.24/11.22 aux(Z, Xs, Y2, Ys, bfalse) = cons(Y2, merge(cons(Z, Xs), Ys)) % 11.24/11.22 aux2(Y, Y2, Xs, btrue) = ord(cons(Y2, Xs)) % 11.24/11.22 aux2(Y, Y2, Xs, bfalse) = bfalse % 11.24/11.22 leqNat(z, Y) = btrue % 11.24/11.22 leqNat(s(Z), z) = bfalse % 11.24/11.22 leqNat(s(Z), s(M)) = leqNat(Z, M) % 11.24/11.22 merge(nil, Y) = Y % 11.24/11.22 merge(cons(Z, Xs), nil) = cons(Z, Xs) % 11.24/11.22 merge(cons(Z, Xs), cons(Y2, Ys)) = aux(Z, Xs, Y2, Ys, leqNat(Z, Y2)) % 11.24/11.22 ord(nil) = btrue % 11.24/11.22 ord(cons(Y, nil)) = btrue % 11.24/11.22 ord(cons(Y, cons(Y2, Xs))) = aux2(Y, Y2, Xs, leqNat(Y, Y2)) % 11.24/11.22 impl(btrue, Q) = Q % 11.24/11.22 impl(bfalse, Q) = btrue % 11.24/11.22 prop_merge_ord_not3(X, Y) = impl(eq2(ord(X), btrue), impl(eq2(ord(Y), bfalse), eq2(ord(merge(X, Y)), btrue))) % 11.24/11.22 eq2(bfalse, btrue) = bfalse % 11.24/11.22 eq2(btrue, bfalse) = bfalse % 11.24/11.22 eq(s(X), s(Y)) = eq(X, Y) % 11.24/11.22 eq(z, s(X)) = bfalse % 11.24/11.22 eq(s(X), z) = bfalse % 11.24/11.22 eq(X, X) = btrue % 11.24/11.22 eq2(X, X) = btrue % 11.24/11.22 eq2(prop_merge_ord_not3(X, Y), bfalse) = btrue ==> \bottom % 11.24/11.22 % 11.24/11.22 This holds because % 11.24/11.22 % 11.24/11.22 [2] the following E entails the following G (Claessen-Smallbone's transformation (2018)): % 11.24/11.22 % 11.24/11.22 E: % 11.24/11.22 aux(Z, Xs, Y2, Ys, bfalse) = cons(Y2, merge(cons(Z, Xs), Ys)) % 11.24/11.22 aux(Z, Xs, Y2, Ys, btrue) = cons(Z, merge(Xs, cons(Y2, Ys))) % 11.24/11.22 aux2(Y, Y2, Xs, bfalse) = bfalse % 11.24/11.22 aux2(Y, Y2, Xs, btrue) = ord(cons(Y2, Xs)) % 11.24/11.22 eq(X, X) = btrue % 11.24/11.22 eq(s(X), s(Y)) = eq(X, Y) % 11.24/11.22 eq(s(X), z) = bfalse % 11.24/11.22 eq(z, s(X)) = bfalse % 11.24/11.22 eq2(X, X) = btrue % 11.24/11.22 eq2(bfalse, btrue) = bfalse % 11.24/11.22 eq2(btrue, bfalse) = bfalse % 11.24/11.22 f1(btrue) = false__ % 11.24/11.22 f1(eq2(prop_merge_ord_not3(X, Y), bfalse)) = true__ % 11.24/11.22 impl(bfalse, Q) = btrue % 11.24/11.22 impl(btrue, Q) = Q % 11.24/11.22 leqNat(s(Z), s(M)) = leqNat(Z, M) % 11.24/11.22 leqNat(s(Z), z) = bfalse % 11.24/11.22 leqNat(z, Y) = btrue % 11.24/11.22 merge(cons(Z, Xs), cons(Y2, Ys)) = aux(Z, Xs, Y2, Ys, leqNat(Z, Y2)) % 11.24/11.22 merge(cons(Z, Xs), nil) = cons(Z, Xs) % 11.24/11.22 merge(nil, Y) = Y % 11.24/11.22 ord(cons(Y, cons(Y2, Xs))) = aux2(Y, Y2, Xs, leqNat(Y, Y2)) % 11.24/11.22 ord(cons(Y, nil)) = btrue % 11.24/11.22 ord(nil) = btrue % 11.24/11.22 prop_merge_ord_not3(X, Y) = impl(eq2(ord(X), btrue), impl(eq2(ord(Y), bfalse), eq2(ord(merge(X, Y)), btrue))) % 11.24/11.22 G: % 11.24/11.22 true__ = false__ % 11.24/11.22 % 11.24/11.22 This holds because % 11.24/11.22 % 11.24/11.22 [3] E entails the following ordered TRS and the lhs and rhs of G join by the TRS: % 11.24/11.22 % 11.24/11.22 aux(Y0, nil, Y1, Y2, ord(nil)) = aux(Y1, Y2, Y0, nil, bfalse) % 11.24/11.22 cons(Y0, aux(X1, X2, Y1, X3, bfalse)) = aux(Y0, nil, Y1, merge(cons(X1, X2), X3), ord(nil)) % 11.24/11.22 cons(Y0, aux(Y1, X1, X2, X3, ord(nil))) = aux(Y0, nil, Y1, merge(X1, cons(X2, X3)), ord(nil)) % 11.24/11.22 cons(Y0, aux(Y1, nil, X1, X2, ord(nil))) = aux(Y0, nil, Y1, cons(X1, X2), ord(nil)) % 11.24/11.22 cons(Y0, merge(Y1, aux(Y2, X1, X2, X3, ord(nil)))) = aux(Y0, Y1, Y2, merge(X1, cons(X2, X3)), ord(nil)) % 11.24/11.22 cons(Y0, merge(Y1, aux(Y2, nil, X1, X2, ord(nil)))) = aux(Y0, Y1, Y2, cons(X1, X2), ord(nil)) % 11.24/11.22 cons(Y0, merge(aux(Y1, nil, X1, X2, ord(nil)), Y3)) = aux(Y1, cons(X1, X2), Y0, Y3, bfalse) % 11.24/11.22 merge(aux(Y0, nil, X1, X2, ord(nil)), cons(Y2, Y3)) = aux(Y0, cons(X1, X2), Y2, Y3, leqNat(Y0, Y2)) % 11.24/11.22 ord(aux(X1, X2, Y0, X3, bfalse)) = ord(aux(Y0, merge(cons(X1, X2), X3), z, nil, bfalse)) % 11.24/11.22 ord(aux(X1, X2, Y0, X3, bfalse)) = ord(aux(z, nil, Y0, merge(cons(X1, X2), X3), ord(nil))) % 11.24/11.22 ord(aux(Y0, X1, X2, X3, ord(nil))) = ord(aux(z, nil, Y0, merge(X1, cons(X2, X3)), ord(nil))) % 11.24/11.22 ord(aux(Y0, Y1, z, nil, bfalse)) = ord(cons(Y0, Y1)) % 11.24/11.22 ord(aux(Y0, nil, X1, X2, ord(nil))) = ord(aux(z, nil, Y0, cons(X1, X2), ord(nil))) % 11.24/11.22 ord(aux(s(X0), nil, s(X1), Y2, ord(nil))) = ord(aux(z, nil, s(X0), cons(s(X1), Y2), ord(nil))) % 11.24/11.22 ord(aux(z, nil, Y0, cons(Y1, Y2), ord(nil))) = ord(aux(Y1, Y2, Y0, nil, bfalse)) % 11.24/11.22 ord(cons(Y1, Y2)) = ord(aux(z, nil, Y1, Y2, ord(nil))) % 11.24/11.22 aux2(Y, Y2, Xs, bfalse) -> bfalse % 11.24/11.22 aux2(Y, Y2, Xs, btrue) -> ord(cons(Y2, Xs)) % 11.24/11.22 aux2(Y, Y2, Xs, leqNat(Y, Y2)) -> ord(cons(Y, cons(Y2, Xs))) % 11.24/11.22 aux2(Y0, Y1, Y2, ord(nil)) -> ord(cons(Y1, Y2)) % 11.24/11.22 aux2(s(X0), s(X1), Y2, leqNat(X0, X1)) -> ord(aux(s(X0), nil, s(X1), Y2, ord(nil))) % 11.24/11.22 aux2(z, Y1, Y2, ord(nil)) -> ord(cons(z, cons(Y1, Y2))) % 11.24/11.22 btrue -> ord(nil) % 11.24/11.22 cons(Y0, cons(Y2, Y3)) -> aux(Y0, nil, Y2, Y3, ord(nil)) % 11.24/11.22 cons(Y2, merge(cons(Z, Xs), Ys)) -> aux(Z, Xs, Y2, Ys, bfalse) % 11.24/11.22 cons(Z, merge(Xs, cons(Y2, Ys))) -> aux(Z, Xs, Y2, Ys, btrue) % 11.24/11.22 eq(X, X) -> btrue % 11.24/11.22 eq(s(X), s(Y)) -> eq(X, Y) % 11.24/11.22 eq(s(X), z) -> bfalse % 11.24/11.22 eq(z, s(X)) -> bfalse % 11.24/11.22 eq2(X, X) -> btrue % 11.24/11.22 eq2(bfalse, btrue) -> bfalse % 11.24/11.22 eq2(bfalse, ord(nil)) -> bfalse % 11.24/11.22 eq2(btrue, bfalse) -> bfalse % 11.24/11.22 eq2(ord(nil), bfalse) -> bfalse % 11.24/11.22 f1(bfalse) -> true__ % 11.24/11.22 f1(btrue) -> false__ % 11.24/11.22 f1(eq2(impl(eq2(ord(Y0), ord(nil)), impl(eq2(ord(Y1), bfalse), eq2(ord(merge(Y0, Y1)), ord(nil)))), bfalse)) -> true__ % 11.24/11.22 f1(eq2(impl(eq2(ord(Y1), bfalse), eq2(ord(Y1), ord(nil))), bfalse)) -> true__ % 11.24/11.22 f1(eq2(impl(eq2(ord(aux(X0, X1, z, nil, bfalse)), bfalse), eq2(ord(cons(X0, X1)), ord(nil))), bfalse)) -> true__ % 11.24/11.22 f1(eq2(impl(eq2(ord(aux(z, nil, X0, X1, ord(nil))), bfalse), eq2(ord(cons(X0, X1)), ord(nil))), bfalse)) -> true__ % 11.24/11.22 f1(eq2(impl(eq2(ord(cons(X0, X1)), bfalse), eq2(ord(aux(X0, X1, z, nil, bfalse)), ord(nil))), bfalse)) -> true__ % 11.24/11.22 f1(eq2(impl(eq2(ord(cons(X0, X1)), bfalse), eq2(ord(aux(z, nil, X0, X1, ord(nil))), ord(nil))), bfalse)) -> true__ % 11.24/11.22 f1(eq2(prop_merge_ord_not3(X, Y), bfalse)) -> true__ % 11.24/11.22 f1(ord(nil)) -> false__ % 11.24/11.22 impl(bfalse, Q) -> btrue % 11.24/11.22 impl(btrue, Q) -> Q % 11.24/11.22 impl(ord(nil), Y0) -> Y0 % 11.24/11.22 leqNat(s(Z), s(M)) -> leqNat(Z, M) % 11.24/11.22 leqNat(s(Z), z) -> bfalse % 11.24/11.22 leqNat(z, Y) -> btrue % 11.24/11.22 merge(aux(X1, X2, Y0, X3, bfalse), nil) -> aux(X1, X2, Y0, X3, bfalse) % 11.24/11.22 merge(aux(Y0, X1, X2, X3, ord(nil)), nil) -> aux(Y0, X1, X2, X3, ord(nil)) % 11.24/11.22 merge(aux(Y0, nil, X1, X2, ord(nil)), nil) -> aux(Y0, nil, X1, X2, ord(nil)) % 11.24/11.22 merge(cons(Z, Xs), cons(Y2, Ys)) -> aux(Z, Xs, Y2, Ys, leqNat(Z, Y2)) % 11.24/11.22 merge(cons(Z, Xs), nil) -> cons(Z, Xs) % 11.24/11.22 merge(nil, Y) -> Y % 11.24/11.22 ord(aux(Y0, cons(X1, X2), z, nil, bfalse)) -> ord(aux(Y0, nil, X1, X2, ord(nil))) % 11.24/11.22 ord(aux(Y0, merge(X1, cons(X2, X3)), z, nil, bfalse)) -> ord(aux(Y0, X1, X2, X3, ord(nil))) % 11.24/11.22 ord(aux(Y0, nil, z, nil, bfalse)) -> ord(nil) % 11.24/11.22 ord(aux(s(X0), nil, z, Y2, ord(nil))) -> bfalse % 11.24/11.22 ord(aux(s(z), Y2, s(s(X0)), nil, bfalse)) -> bfalse % 11.24/11.22 ord(aux(s(z), nil, s(Y1), Y2, ord(nil))) -> ord(aux(z, nil, s(Y1), Y2, ord(nil))) % 11.24/11.22 ord(aux(z, Y1, s(Y0), nil, bfalse)) -> bfalse % 11.24/11.22 ord(aux(z, nil, Y0, nil, ord(nil))) -> ord(nil) % 11.24/11.22 ord(aux(z, nil, s(X0), cons(z, Y2), ord(nil))) -> bfalse % 11.24/11.22 ord(aux(z, nil, s(Y0), aux(X1, X2, z, X3, bfalse), ord(nil))) -> bfalse % 11.24/11.22 ord(aux(z, nil, s(Y0), aux(z, X1, X2, X3, ord(nil)), ord(nil))) -> bfalse % 11.24/11.22 ord(aux(z, nil, s(Y0), aux(z, nil, X1, X2, ord(nil)), ord(nil))) -> bfalse % 11.24/11.22 ord(aux(z, nil, z, aux(Y0, nil, X1, X2, ord(nil)), ord(nil))) -> ord(aux(Y0, nil, X1, X2, ord(nil))) % 11.24/11.22 ord(aux(z, nil, z, cons(Y1, Y2), ord(nil))) -> ord(cons(Y1, Y2)) % 11.24/11.22 ord(cons(Y, nil)) -> btrue % 11.24/11.22 prop_merge_ord_not3(X, Y) -> impl(eq2(ord(X), btrue), impl(eq2(ord(Y), bfalse), eq2(ord(merge(X, Y)), btrue))) % 11.24/11.22 true__ -> false__ % 11.24/11.22 with the LPO induced by % 11.24/11.22 f1 > aux2 > eq > prop_merge_ord_not3 > eq2 > impl > s > z > cons > btrue > ord > nil > bfalse > merge > leqNat > aux > true__ > false__ % 11.24/11.22 % 11.24/11.22 % SZS output end Proof % 11.24/11.22 %------------------------------------------------------------------------------