MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x)
    (RULES
      a -> h(c)
      a -> h(f(c))
      h(x) -> h(h(x))
      f(x) -> f(g(x))
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (VAR x)
    (RULES
      a -> h(c)
      a -> h(f(c))
      h(x) -> h(h(x))
      f(x) -> f(g(x))
    )

(VAR x)
(CONDITION 
h(c) == x, h(f(c)) == x
)

Optimized the infeasibility problem if possible.

(VAR x)
(CONDITION 
h(c) == x, h(f(c)) == x
)

This is ultra-RL and deterministic.

This is not operationally terminating and confluent.

This is a constructor-based system.

(RTG_of_NARROWINGTREE
(START
  Gamma[h(c) == x : { e, 1, 1.1 } & h(f(c)) == x : { e, 1, 1.1, 1.1.1 }]
)
(NONTERMINALS
  Gamma[h(c) == x : { e, 1, 1.1 } & h(f(c)) == x : { e, 1, 1.1, 1.1.1 }]
  Gamma[h(c2) == x38 : { e, 1 }]
  Gamma[f(c4) == f2 : { e, 1 }]
)
(RULES
  Gamma[h(c) == x : { e, 1, 1.1 } & h(f(c)) == x : { e, 1, 1.1, 1.1.1 }] -> (({ c1 -> c } & Rec(Gamma[h(c2) == x38 : { e, 1 }], { x -> x38, c1 -> c2 })) & ({ c3 -> c } & (Rec(Gamma[f(c4) == f2 : { e, 1 }], { f1 -> f2, c3 -> c4 }) & Rec(Gamma[h(c2) == x38 : { e, 1 }], { x -> x38, f1 -> c2 }))))
  Gamma[h(c2) == x38 : { e, 1 }] -> { x38 -> h(c2) }
  Gamma[h(c2) == x38 : { e, 1 }] -> ((Rec(Gamma[h(c2) == x38 : { e, 1 }], { h1 -> x38, x46 -> c2 }) & Rec(Gamma[h(c2) == x38 : { e, 1 }], { x38 -> x38, h1 -> c2 })) . { c2 -> x46 })
  Gamma[f(c4) == f2 : { e, 1 }] -> { f2 -> f(c4) }
  Gamma[f(c4) == f2 : { e, 1 }] -> (({ g1 -> g(x56) } & Rec(Gamma[f(c4) == f2 : { e, 1 }], { f2 -> f2, g1 -> c4 })) . { c4 -> x56 })
)
)

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

This is not ultra-RL and deterministic.

The inverted system is ultra-RL and deterministic.


MAYBE