MAYBE


Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR y x)
    (RULES
      f(x,y) -> g(x) | c(g(x)) == c(a)
      f(x,y) -> h(x) | c(h(x)) == c(a)
      g(s(x)) -> x
      h(s(x)) -> x
    )

No "->="-rules.

Decomposed conditions if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR y x)
    (RULES
      f(x,y) -> g(x) | g(x) == a
      f(x,y) -> h(x) | h(x) == a
      g(s(x)) -> x
      h(s(x)) -> x
    )

Removed infeasible rules as much as possible.
    (CONDITIONTYPE ORIENTED)
    (VAR y x)
    (RULES
      f(x,y) -> g(x) | g(x) == a
      f(x,y) -> h(x) | h(x) == a
      g(s(x)) -> x
      h(s(x)) -> x
    )

Try to disprove confluence of the following (C)TRS:
    (CONDITIONTYPE ORIENTED)
    (VAR y x)
    (RULES
      f(x,y) -> g(x) | g(x) == a
      f(x,y) -> h(x) | h(x) == a
      g(s(x)) -> x
      h(s(x)) -> x
    )

Failed either to apply SR and U for normal 1CTRSs to the above CTRS or to prove confluence of any converted TRSs.

Try to apply SR and U for 3DCTRSs to the above CTRS.

Succeeded in applying U for 3DCTRSs to the above CTRS.
U(R) =
    (VAR x2 x1)
    (RULES
      f(x1,x2) -> u1(g(x1),x1,x2)
      u1(a,x1,x2) -> g(x1)
      f(x1,x2) -> u2(h(x1),x1,x2)
      u2(a,x1,x2) -> h(x1)
      g(s(x1)) -> x1
      h(s(x1)) -> x1
    )

U for 3DCTRSs is sound for the above CTRS.

Failed to prove confluence of U(R).

Try to prove operational termination of R, i.e., termination of U(R).

Succeeded in proving operational termination of R.

Try to prove joinability of all (conditional) CPs.

Failed to prove joinability of conditional CPs (via narrowing trees).

MAYBE