MAYBE

The TRS could not be proven terminating. The proof attempt took 2478 ms.

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (34ms), SubtermCriterion (1ms), DependencyGraph (7ms), PolynomialLinearRange4iUR (322ms), DependencyGraph (4ms), PolynomialLinearRange8NegiUR (740ms), DependencyGraph (5ms), ReductionPairSAT (1154ms), DependencyGraph (4ms), SizeChangePrinciple (9ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app#(app(app(comp, f), g), x) → app#(f, app(g, x))app#(twice, f) → app#(app(comp, f), f)
app#(app(app(comp, f), g), x) → app#(g, x)app#(twice, f) → app#(comp, f)

Rewrite Rules

app(app(app(comp, f), g), x) → app(f, app(g, x))app(twice, f) → app(app(comp, f), f)

Original Signature

Termination of terms over the following signature is verified: app, comp, twice