MAYBE

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

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x)
    (RULES
      c -> k(f(a))
      c -> k(g(b))
      h(x) -> k(x)
      h(f(a)) -> c
      a -> b
      f(x) -> g(x) | h(f(x)) == k(g(b))
    )

(CONDITION 
h(f(a)) == k(g(b))
)

Optimized the infeasibility problem if possible.

(CONDITION 
h(f(a)) == k(g(b))
)

This is not ultra-RL and deterministic.

The inverted system is ultra-RL and deterministic.

(RTG_of_NARROWINGTREE
(START
  Gamma[k(g(b)) == h(f(a)) : { e, 1, 1.1, 1.1.1 }]
)
(NONTERMINALS
  Gamma[k(g(b)) == h(f(a)) : { e, 1, 1.1, 1.1.1 }]
  Gamma[b == b2 : { e, 1 }]
  Gamma[g(b3) == g2 : { e, 1 }]
  Gamma[k(g3) == h(f(a)) : { e, 1 }]
  Gamma[k(g5) == h2 : { e, 1 }]
  Gamma[c == h(f(a)) : { e, 1 }]
  Gamma[c == h3 : { e, 1 }]
)
(RULES
  Gamma[k(g(b)) == h(f(a)) : { e, 1, 1.1, 1.1.1 }] -> (Rec(Gamma[b == b2 : { e, 1 }], { b1 -> b2 }) & (Rec(Gamma[g(b3) == g2 : { e, 1 }], { g1 -> g2, b1 -> b3 }) & Rec(Gamma[k(g3) == h(f(a)) : { e, 1 }], { g1 -> g3 })))
  Gamma[b == b2 : { e, 1 }] -> { b2 -> b }
  Gamma[b == b2 : { e, 1 }] -> { b2 -> a }
  Gamma[g(b3) == g2 : { e, 1 }] -> { g2 -> g(b3) }
  Gamma[g(b3) == g2 : { e, 1 }] -> (((Rec(Gamma[b == b2 : { e, 1 }], { b4 -> b2 }) & (Rec(Gamma[g(b3) == g2 : { e, 1 }], { g4 -> g2, b4 -> b3 }) & (Rec(Gamma[k(g5) == h2 : { e, 1 }], { h1 -> h2, g4 -> g5 }) & { h1 -> h(f(x18)) }))) & { g2 -> f(x18) }) . { b3 -> x18 })
  Gamma[k(g3) == h(f(a)) : { e, 1 }] -> (Rec(Gamma[c == h(f(a)) : { e, 1 }], {  }) . { g3 -> f(a) })
  Gamma[k(g3) == h(f(a)) : { e, 1 }] -> (Rec(Gamma[c == h(f(a)) : { e, 1 }], {  }) . { g3 -> g(b) })
  Gamma[k(g3) == h(f(a)) : { e, 1 }] -> { x30 -> f(a), g3 -> f(a) }
  Gamma[k(g5) == h2 : { e, 1 }] -> { h2 -> k(g5) }
  Gamma[k(g5) == h2 : { e, 1 }] -> (Rec(Gamma[c == h3 : { e, 1 }], { h2 -> h3 }) . { g5 -> f(a) })
  Gamma[k(g5) == h2 : { e, 1 }] -> (Rec(Gamma[c == h3 : { e, 1 }], { h2 -> h3 }) . { g5 -> g(b) })
  Gamma[k(g5) == h2 : { e, 1 }] -> { h2 -> h(x38), g5 -> x38 }
  Gamma[c == h(f(a)) : { e, 1 }] -> {  }
  Gamma[c == h3 : { e, 1 }] -> { h3 -> c }
  Gamma[c == h3 : { e, 1 }] -> { h3 -> h(f(a)) }
)
)


MAYBE