MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y x2 x1)
    (RULES
      pin(x) -> pout(g(x))
      pin(x) -> pout(f(y)) | pin(x) == pout(g(y))
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y x2 x1)
    (RULES
      pin(x) -> pout(g(x))
      pin(x) -> pout(f(y)) | pin(x) == pout(g(y))
    )

(VAR x2 x1)
(CONDITION 
pin(x1) == pout(g(x2))
)

Optimized the infeasibility problem if possible.

(VAR x2 x1)
(CONDITION 
pin(x1) == pout(g(x2))
)

This is ultra-RL and deterministic.

This is not operationally terminating and confluent.

This is a constructor-based system.

(RTG_of_NARROWINGTREE
(START
  Gamma[pin(x1) == pout(g(x2)) : { e, 1 }]
)
(NONTERMINALS
  Gamma[pin(x1) == pout(g(x2)) : { e, 1 }]
  Gamma[pin(x17) == pout2 : { e, 1 }]
)
(RULES
  Gamma[pin(x1) == pout(g(x2)) : { e, 1 }] -> (Rec(Gamma[pin(x17) == pout2 : { e, 1 }], { pout1 -> pout2, x1 -> x17 }) & { pout1 -> pout(g(x2)) })
  Gamma[pin(x17) == pout2 : { e, 1 }] -> { pout2 -> pin(x17) }
  Gamma[pin(x17) == pout2 : { e, 1 }] -> { pout2 -> pout(g(x19)), x17 -> x19 }
  Gamma[pin(x17) == pout2 : { e, 1 }] -> (((Rec(Gamma[pin(x17) == pout2 : { e, 1 }], { pout3 -> pout2, x20 -> x17 }) & { pout3 -> pout(g(y3)) }) & { pout2 -> pout(f(y3)) }) . { x17 -> x20 })
)
)

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.

(RTG_of_NARROWINGTREE
(START
  Gamma[pout(g(x2)) == pin(x1) : { e, 1, 1.1 }]
)
(NONTERMINALS
  Gamma[pout(g(x2)) == pin(x1) : { e, 1, 1.1 }]
)
(RULES
  Gamma[pout(g(x2)) == pin(x1) : { e, 1, 1.1 }] -> { x1 -> x29 }
)
)


MAYBE