TIMEOUT

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

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (428ms), SubtermCriterion (2ms), DependencyGraph (381ms), PolynomialLinearRange4iUR (5691ms), DependencyGraph (358ms), PolynomialLinearRange8NegiUR (28556ms), DependencyGraph (351ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(app(map_3, f), g)		app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(app(cons, app(app(f, h), c)), app(app(app(map_2, f), c), t))
app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(app(app(app(map_3, f), g), c), t)		app^#(app(map_1, f), app(app(cons, h), t))	→	app^#(map_1, f)
app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(app(cons, app(app(app(f, g), h), c)), app(app(app(app(map_3, f), g), c), t))		app^#(app(map_1, f), app(app(cons, h), t))	→	app^#(app(map_1, f), t)
app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(app(map_2, f), c)		app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(f, h)
app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(app(f, h), c)		app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(app(app(map_3, f), g), c)
app^#(app(map_1, f), app(app(cons, h), t))	→	app^#(app(cons, app(f, h)), app(app(map_1, f), t))		app^#(app(map_1, f), app(app(cons, h), t))	→	app^#(cons, app(f, h))
app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(map_3, f)		app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(f, g)
app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(cons, app(app(app(f, g), h), c))		app^#(app(map_1, f), app(app(cons, h), t))	→	app^#(f, h)
app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(cons, app(app(f, h), c))		app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(app(f, g), h)
app^#(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app^#(app(app(f, g), h), c)		app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(app(app(map_2, f), c), t)
app^#(app(app(map_2, f), c), app(app(cons, h), t))	→	app^#(map_2, f)

Rewrite Rules

app(app(map_1, f), app(app(cons, h), t))	→	app(app(cons, app(f, h)), app(app(map_1, f), t))		app(app(app(map_2, f), c), app(app(cons, h), t))	→	app(app(cons, app(app(f, h), c)), app(app(app(map_2, f), c), t))
app(app(app(app(map_3, f), g), c), app(app(cons, h), t))	→	app(app(cons, app(app(app(f, g), h), c)), app(app(app(app(map_3, f), g), c), t))

Original Signature

Termination of terms over the following signature is verified: g, app, map_3, map_1, map_2, cons