YES

Succeeded in reading "/export/starexec/sandbox2/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x x\'\' x\' y y\'\' y\' x3 x2 x1)
    (RULES
      f(x\',x\'\') -> g(x) | x\' == x, x\'\' == x
      f(y\',h(y\'\')) -> g(y) | y\' == y, y\'\' == y
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x x\'\' x\' y y\'\' y\' x3 x2 x1)
    (RULES
      f(x\',x\'\') -> g(x) | x\' == x, x\'\' == x
      f(y\',h(y\'\')) -> g(y) | y\' == y, y\'\' == y
    )

(VAR x3 x2 x x1)
(CONDITION 
x1 == x, h(x2) == x, x1 == x3, x2 == x3
)

Optimized the infeasibility problem if possible.

(VAR x3 x2 x x1)
(CONDITION 
x1 == x, h(x2) == x, x1 == x3, x2 == x3
)

This is ultra-RL and deterministic.

This is not operationally terminating and confluent.

This is a constructor-based system.

(RTG_of_NARROWINGTREE
(START
  Gamma[x1 == x : { e } & h(x2) == x : { e, 1 } & x1 == x3 : { e } & x2 == x3 : { e }]
)
(NONTERMINALS
  Gamma[x1 == x : { e } & h(x2) == x : { e, 1 } & x1 == x3 : { e } & x2 == x3 : { e }]
)
(RULES
  Gamma[x1 == x : { e } & h(x2) == x : { e, 1 } & x1 == x3 : { e } & x2 == x3 : { e }] -> EmptySet
)
)

YES