MAYBE

Succeeded in reading "/export/starexec/sandbox/benchmark/theBenchmark.ari".
    (CONDITIONTYPE ORIENTED)
    (VAR x y z x3 x1 x2)
    (RULES
      pin(a) -> pout(b)
      pin(b) -> pout(c)
      tc(x) -> x
      tc(x) -> y | pin(x) == pout(z), tc(z) == y
    )

No "->="-rules.

Decomposed conditions and removed infeasible rules if possible.
    (CONDITIONTYPE ORIENTED)
    (VAR x y z x3 x1 x2)
    (RULES
      pin(a) -> pout(b)
      pin(b) -> pout(c)
      tc(x) -> x
      tc(x) -> y | pin(x) == pout(z), tc(z) == y
    )

(VAR x3 x1 x2)
(CONDITION 
pin(x2) == pout(x1), tc(x1) == x3
)

Optimized the infeasibility problem if possible.

(VAR x3 x1 x2)
(CONDITION 
pin(x2) == pout(x1), tc(x1) == 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[pin(x2) == pout(x1) : { e, 1 } & tc(x1) == x3 : { e, 1 }]
)
(NONTERMINALS
  Gamma[pin(x2) == pout(x1) : { e, 1 } & tc(x1) == x3 : { e, 1 }]
  Gamma[pin(x52) == pout2 : { e, 1 }]
  Gamma[tc(x56) == x57 : { e, 1 }]
)
(RULES
  Gamma[pin(x2) == pout(x1) : { e, 1 } & tc(x1) == x3 : { e, 1 }] -> ((Rec(Gamma[pin(x52) == pout2 : { e, 1 }], { pout1 -> pout2, x2 -> x52 }) & { pout1 -> pout(x1) }) & Rec(Gamma[tc(x56) == x57 : { e, 1 }], { x3 -> x57, x1 -> x56 }))
  Gamma[pin(x52) == pout2 : { e, 1 }] -> { pout2 -> pin(x52) }
  Gamma[pin(x52) == pout2 : { e, 1 }] -> { pout2 -> pout(b), x52 -> a }
  Gamma[pin(x52) == pout2 : { e, 1 }] -> { pout2 -> pout(c), x52 -> b }
  Gamma[tc(x56) == x57 : { e, 1 }] -> { x57 -> tc(x56) }
  Gamma[tc(x56) == x57 : { e, 1 }] -> { x63 -> x65, x57 -> x65, x56 -> x65 }
  Gamma[tc(x56) == x57 : { e, 1 }] -> (((Rec(Gamma[pin(x52) == pout2 : { e, 1 }], { pout3 -> pout2, x64 -> x52 }) & { pout3 -> pout(z5) }) & (Rec(Gamma[tc(x56) == x57 : { e, 1 }], { y5 -> x57, z5 -> x56 }) & { x57 -> x73, y5 -> x73 })) . { x56 -> x64 })
)
)

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

This is not ultra-RL and deterministic.


MAYBE