MAYBE

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

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (VAR y x)
    (RULES
      f(x,y) -> g(x)
      f(x,y) -> h(x)
      g(s(x)) -> x
      h(s(x)) -> x
      a -> d
      b -> d
      e -> e
    )

(CONDITION 
a == d, b == d
)

Optimized the infeasibility problem if possible.

(CONDITION 
a == d, b == d
)

This is ultra-RL and deterministic.

This is not operationally terminating and confluent.

This is a constructor-based system.

(RTG_of_NARROWINGTREE
(START
  Gamma[a == d : { e, 1 } & b == d : { e, 1 }]
)
(NONTERMINALS
  Gamma[a == d : { e, 1 } & b == d : { e, 1 }]
  Gamma[a == d : { e, 1 }]
  Gamma[b == d : { e, 1 }]
)
(RULES
  Gamma[a == d : { e, 1 } & b == d : { e, 1 }] -> {  }
  Gamma[a == d : { e, 1 }] -> {  }
  Gamma[b == d : { e, 1 }] -> {  }
)
)

Failed to prove infeasibility of the linearized conditions by means of narrowing trees.

This is not ultra-RL and deterministic.


MAYBE