TIMEOUT

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

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (674ms), SubtermCriterion (1ms), DependencyGraph (632ms), PolynomialLinearRange4iUR (7647ms), DependencyGraph (561ms), PolynomialLinearRange8NegiUR (timeout), PolynomialLinearRange8NegiUR (-2ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app^#(app(d, app(s, x)), app(s, y))	→	app^#(app(d, app(s, x)), app(app(sub, y), x))		app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(cons, x)
app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(filter, p)		app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(app(cons, x), app(app(filter, p), xs))
app^#(app(d, app(s, x)), app(s, y))	→	app^#(app(gtr, x), y)		app^#(app(sub, app(s, x)), app(s, y))	→	app^#(app(sub, x), y)
app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(app(app(if, app(p, x)), app(app(cons, x), app(app(filter, p), xs))), app(app(filter, p), xs))		app^#(app(gtr, app(s, x)), app(s, y))	→	app^#(gtr, x)
app^#(app(sub, app(s, x)), app(s, y))	→	app^#(sub, x)		app^#(app(d, app(s, x)), app(s, y))	→	app^#(gtr, x)
app^#(app(gtr, app(s, x)), app(s, y))	→	app^#(app(gtr, x), y)		app^#(app(d, app(s, x)), app(s, y))	→	app^#(app(if, app(app(gtr, x), y)), false)
app^#(app(d, app(s, x)), app(s, y))	→	app^#(app(sub, y), x)		app^#(len, app(app(cons, x), xs))	→	app^#(len, xs)
app^#(len, app(app(cons, x), xs))	→	app^#(s, app(len, xs))		app^#(app(d, app(s, x)), app(s, y))	→	app^#(d, app(s, x))
app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(app(filter, p), xs)		app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(app(if, app(p, x)), app(app(cons, x), app(app(filter, p), xs)))
app^#(app(d, app(s, x)), app(s, y))	→	app^#(if, app(app(gtr, x), y))		app^#(app(d, app(s, x)), app(s, y))	→	app^#(s, x)
app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(if, app(p, x))		app^#(app(d, app(s, x)), app(s, y))	→	app^#(sub, y)
app^#(app(filter, p), app(app(cons, x), xs))	→	app^#(p, x)		app^#(app(d, app(s, x)), app(s, y))	→	app^#(app(app(if, app(app(gtr, x), y)), false), app(app(d, app(s, x)), app(app(sub, y), x)))

Rewrite Rules

app(app(app(if, true), xs), ys)	→	xs		app(app(app(if, false), xs), ys)	→	ys
app(app(sub, x), 0)	→	x		app(app(sub, app(s, x)), app(s, y))	→	app(app(sub, x), y)
app(app(gtr, 0), y)	→	false		app(app(gtr, app(s, x)), 0)	→	true
app(app(gtr, app(s, x)), app(s, y))	→	app(app(gtr, x), y)		app(app(d, x), 0)	→	true
app(app(d, app(s, x)), app(s, y))	→	app(app(app(if, app(app(gtr, x), y)), false), app(app(d, app(s, x)), app(app(sub, y), x)))		app(len, nil)	→	0
app(len, app(app(cons, x), xs))	→	app(s, app(len, xs))		app(app(filter, p), nil)	→	nil
app(app(filter, p), app(app(cons, x), xs))	→	app(app(app(if, app(p, x)), app(app(cons, x), app(app(filter, p), xs))), app(app(filter, p), xs))

Original Signature

Termination of terms over the following signature is verified: app, sub, d, true, len, gtr, 0, s, if, false, filter, nil, cons