MAYBE

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

No "->="-rules.

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

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

Optimized the infeasibility problem if possible.

(VAR x)
(CONDITION 
h(f(c,d),d) == x, f(c,d) == 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(f(c,d),d) == x : { e, 1, 1.1, 1.1.1, 1.1.2, 1.2 } & f(c,d) == x : { e, 1, 1.1, 1.2 }]
)
(NONTERMINALS
  Gamma[h(f(c,d),d) == x : { e, 1, 1.1, 1.1.1, 1.1.2, 1.2 } & f(c,d) == x : { e, 1, 1.1, 1.2 }]
  Gamma[c == c2 : { e, 1 }]
  Gamma[f(c3,d3) == f2 : { e, 1 }]
  Gamma[h(f3,d4) == x39 : { e, 1 }]
)
(RULES
  Gamma[h(f(c,d),d) == x : { e, 1, 1.1, 1.1.1, 1.1.2, 1.2 } & f(c,d) == x : { e, 1, 1.1, 1.2 }] -> ((Rec(Gamma[c == c2 : { e, 1 }], { c1 -> c2 }) & ({ d2 -> d } & (Rec(Gamma[f(c3,d3) == f2 : { e, 1 }], { f1 -> f2, d2 -> d3, c1 -> c3 }) & ({ d1 -> d } & Rec(Gamma[h(f3,d4) == x39 : { e, 1 }], { x -> x39, d1 -> d4, f1 -> f3 }))))) & (Rec(Gamma[c == c2 : { e, 1 }], { c4 -> c2 }) & ({ d5 -> d } & Rec(Gamma[f(c3,d3) == f2 : { e, 1 }], { x -> f2, d5 -> d3, c4 -> c3 }))))
  Gamma[c == c2 : { e, 1 }] -> { c2 -> c }
  Gamma[c == c2 : { e, 1 }] -> (Rec(Gamma[c == c2 : { e, 1 }], { c5 -> c2 }) & ({ d6 -> d } & Rec(Gamma[f(c3,d3) == f2 : { e, 1 }], { c2 -> f2, d6 -> d3, c5 -> c3 })))
  Gamma[c == c2 : { e, 1 }] -> (Rec(Gamma[c == c2 : { e, 1 }], { c6 -> c2 }) & ({ d7 -> d } & Rec(Gamma[h(f3,d4) == x39 : { e, 1 }], { c2 -> x39, d7 -> d4, c6 -> f3 })))
  Gamma[f(c3,d3) == f2 : { e, 1 }] -> { f2 -> f(c3,d3) }
  Gamma[f(c3,d3) == f2 : { e, 1 }] -> (({ g1 -> g(y29) } & Rec(Gamma[h(f3,d4) == x39 : { e, 1 }], { f2 -> x39, x64 -> d4, g1 -> f3 })) . { d3 -> y29, c3 -> x64 })
  Gamma[h(f3,d4) == x39 : { e, 1 }] -> { x39 -> h(f3,d4) }
  Gamma[h(f3,d4) == x39 : { e, 1 }] -> (({ g2 -> g(y36) } & Rec(Gamma[f(c3,d3) == f2 : { e, 1 }], { x39 -> f2, x73 -> d3, g2 -> c3 })) . { d4 -> y36, f3 -> x73 })
)
)

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