TIMEOUT

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

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (934ms), SubtermCriterion (1ms), DependencyGraph (888ms), PolynomialLinearRange4iUR (7344ms), DependencyGraph (784ms), PolynomialLinearRange8NegiUR (22637ms), DependencyGraph (835ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app^#(app(app(app(filter2, true), fun), x), xs)	→	app^#(cons, x)		app^#(app(app(copy, app(s, x)), y), z)	→	app^#(app(copy, x), y)
app^#(app(filter, fun), app(app(cons, x), xs))	→	app^#(app(app(app(filter2, app(fun, x)), fun), x), xs)		app^#(app(app(copy, app(s, x)), y), z)	→	app^#(app(cons, app(f, y)), z)
app^#(app(app(copy, app(s, x)), y), z)	→	app^#(app(app(copy, x), y), app(app(cons, app(f, y)), z))		app^#(app(filter, fun), app(app(cons, x), xs))	→	app^#(app(app(filter2, app(fun, x)), fun), x)
app^#(app(app(copy, app(s, x)), y), z)	→	app^#(cons, app(f, y))		app^#(app(app(copy, 0), y), z)	→	app^#(f, z)
app^#(app(filter, fun), app(app(cons, x), xs))	→	app^#(fun, x)		app^#(app(map, fun), app(app(cons, x), xs))	→	app^#(fun, x)
app^#(app(app(app(filter2, false), fun), x), xs)	→	app^#(filter, fun)		app^#(app(map, fun), app(app(cons, x), xs))	→	app^#(app(cons, app(fun, x)), app(app(map, fun), xs))
app^#(f, app(app(cons, app(f, app(app(cons, nil), y))), z))	→	app^#(app(copy, n), y)		app^#(app(app(copy, app(s, x)), y), z)	→	app^#(copy, x)
app^#(app(app(app(filter2, true), fun), x), xs)	→	app^#(app(cons, x), app(app(filter, fun), xs))		app^#(app(app(app(filter2, true), fun), x), xs)	→	app^#(app(filter, fun), xs)
app^#(f, app(app(cons, app(f, app(app(cons, nil), y))), z))	→	app^#(copy, n)		app^#(app(app(app(filter2, false), fun), x), xs)	→	app^#(app(filter, fun), xs)
app^#(app(app(copy, app(s, x)), y), z)	→	app^#(f, y)		app^#(f, app(app(cons, app(f, app(app(cons, nil), y))), z))	→	app^#(app(app(copy, n), y), z)
app^#(app(map, fun), app(app(cons, x), xs))	→	app^#(map, fun)		app^#(app(filter, fun), app(app(cons, x), xs))	→	app^#(app(filter2, app(fun, x)), fun)
app^#(app(app(app(filter2, true), fun), x), xs)	→	app^#(filter, fun)		app^#(app(map, fun), app(app(cons, x), xs))	→	app^#(cons, app(fun, x))
app^#(app(map, fun), app(app(cons, x), xs))	→	app^#(app(map, fun), xs)		app^#(app(filter, fun), app(app(cons, x), xs))	→	app^#(filter2, app(fun, x))

Rewrite Rules

app(f, app(app(cons, nil), y))	→	y		app(f, app(app(cons, app(f, app(app(cons, nil), y))), z))	→	app(app(app(copy, n), y), z)
app(app(app(copy, 0), y), z)	→	app(f, z)		app(app(app(copy, app(s, x)), y), z)	→	app(app(app(copy, x), y), app(app(cons, app(f, y)), z))
app(app(map, fun), nil)	→	nil		app(app(map, fun), app(app(cons, x), xs))	→	app(app(cons, app(fun, x)), app(app(map, fun), xs))
app(app(filter, fun), nil)	→	nil		app(app(filter, fun), app(app(cons, x), xs))	→	app(app(app(app(filter2, app(fun, x)), fun), x), xs)
app(app(app(app(filter2, true), fun), x), xs)	→	app(app(cons, x), app(app(filter, fun), xs))		app(app(app(app(filter2, false), fun), x), xs)	→	app(app(filter, fun), xs)

Original Signature

Termination of terms over the following signature is verified: f, app, n, true, 0, s, map, false, filter2, filter, cons, nil, copy