TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (210ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (133ms), PolynomialLinearRange4iUR (3536ms), DependencyGraph (107ms), PolynomialLinearRange8NegiUR (19416ms), DependencyGraph (112ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(filter, f)app#(app(filter, f), app(app(cons, y), ys)) → app#(filtersub, app(f, y))
app#(app(filter, f), app(app(cons, y), ys)) → app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))app#(app(filter, f), app(app(cons, y), ys)) → app#(app(filtersub, app(f, y)), f)
app#(app(neq, app(s, x)), app(s, y)) → app#(app(neq, x), y)app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(app(filter, f), ys)
app#(app(filter, f), app(app(cons, y), ys)) → app#(f, y)app#(app(app(filtersub, false), f), app(app(cons, y), ys)) → app#(app(filter, f), ys)
app#(app(filter, f), app(app(cons, y), ys)) → app#(app(cons, y), ys)app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(app(cons, y), app(app(filter, f), ys))
app#(app(neq, app(s, x)), app(s, y)) → app#(neq, x)app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(cons, y)
app#(app(filter, f), app(app(cons, y), ys)) → app#(cons, y)app#(app(app(filtersub, false), f), app(app(cons, y), ys)) → app#(filter, f)

Rewrite Rules

app(app(neq, 0), 0) → falseapp(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → trueapp(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nilapp(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))

Original Signature

Termination of terms over the following signature is verified: app, 0, s, true, false, neq, nonzero, filtersub, filter, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

app#(app(filter, f), app(app(cons, y), ys)) → app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))app#(app(filter, f), app(app(cons, y), ys)) → app#(filtersub, app(f, y))
app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(filter, f)app#(app(neq, app(s, x)), app(s, y)) → app#(app(neq, x), y)
app#(app(filter, f), app(app(cons, y), ys)) → app#(app(filtersub, app(f, y)), f)nonzero# → app#(neq, 0)
app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(app(filter, f), ys)app#(app(filter, f), app(app(cons, y), ys)) → app#(f, y)
app#(app(app(filtersub, false), f), app(app(cons, y), ys)) → app#(app(filter, f), ys)nonzero# → app#(filter, app(neq, 0))
app#(app(neq, app(s, x)), app(s, y)) → app#(neq, x)app#(app(filter, f), app(app(cons, y), ys)) → app#(app(cons, y), ys)
app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(app(cons, y), app(app(filter, f), ys))app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(cons, y)
app#(app(filter, f), app(app(cons, y), ys)) → app#(cons, y)app#(app(app(filtersub, false), f), app(app(cons, y), ys)) → app#(filter, f)

Rewrite Rules

app(app(neq, 0), 0) → falseapp(app(neq, 0), app(s, y)) → true
app(app(neq, app(s, x)), 0) → trueapp(app(neq, app(s, x)), app(s, y)) → app(app(neq, x), y)
app(app(filter, f), nil) → nilapp(app(filter, f), app(app(cons, y), ys)) → app(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))
app(app(app(filtersub, true), f), app(app(cons, y), ys)) → app(app(cons, y), app(app(filter, f), ys))app(app(app(filtersub, false), f), app(app(cons, y), ys)) → app(app(filter, f), ys)
nonzero → app(filter, app(neq, 0))

Original Signature

Termination of terms over the following signature is verified: app, 0, s, false, true, neq, nonzero, filter, filtersub, nil, cons

Strategy

The following SCCs where found

app#(app(filter, f), app(app(cons, y), ys)) → app#(app(app(filtersub, app(f, y)), f), app(app(cons, y), ys))app#(app(filter, f), app(app(cons, y), ys)) → app#(filtersub, app(f, y))
app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(filter, f)app#(app(neq, app(s, x)), app(s, y)) → app#(app(neq, x), y)
app#(app(filter, f), app(app(cons, y), ys)) → app#(app(filtersub, app(f, y)), f)app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(app(filter, f), ys)
app#(app(filter, f), app(app(cons, y), ys)) → app#(f, y)app#(app(app(filtersub, false), f), app(app(cons, y), ys)) → app#(app(filter, f), ys)
app#(app(neq, app(s, x)), app(s, y)) → app#(neq, x)app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(app(cons, y), app(app(filter, f), ys))
app#(app(filter, f), app(app(cons, y), ys)) → app#(app(cons, y), ys)app#(app(app(filtersub, true), f), app(app(cons, y), ys)) → app#(cons, y)
app#(app(filter, f), app(app(cons, y), ys)) → app#(cons, y)app#(app(app(filtersub, false), f), app(app(cons, y), ys)) → app#(filter, f)