TIMEOUT

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

The following DP Processors were used


Problem 1 remains open; application of the following processors failed [DependencyGraph (3797ms), SubtermCriterion (1ms), DependencyGraph (3592ms), DependencyGraph (3512ms), PolynomialLinearRange8NegiUR (30001ms), DependencyGraph (timeout), ReductionPairSAT (8425ms)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app#(app(map, f), app(app(cons, x), xs)) → app#(f, x)app#(app(map, f), app(app(cons, x), xs)) → app#(app(cons, app(f, x)), app(app(map, f), xs))
app#(app(app(app(filter2, true), f), x), xs) → app#(app(cons, x), app(app(filter, f), xs))app#(app(filter, f), app(app(cons, x), xs)) → app#(f, x)
app#(app(app(app(filter2, true), f), x), xs) → app#(filter, f)app#(app(d, z), app(app(g, x), y)) → app#(e, x)
app#(app(app(app(filter2, true), f), x), xs) → app#(app(filter, f), xs)app#(app(filter, f), app(app(cons, x), xs)) → app#(app(app(app(filter2, app(f, x)), f), x), xs)
app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(d, app(c, z))app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(d, z)
app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))app#(app(h, z), app(e, x)) → app#(h, app(c, z))
app#(app(filter, f), app(app(cons, x), xs)) → app#(filter2, app(f, x))app#(app(g, app(e, x)), app(e, y)) → app#(e, app(app(g, x), y))
app#(app(g, app(e, x)), app(e, y)) → app#(g, x)app#(app(h, z), app(e, x)) → app#(d, z)
app#(app(map, f), app(app(cons, x), xs)) → app#(map, f)app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(c, z)
app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(g, app(app(d, app(c, z)), app(app(g, x), y)))app#(app(h, z), app(e, x)) → app#(app(h, app(c, z)), app(app(d, z), x))
app#(app(app(app(filter2, false), f), x), xs) → app#(filter, f)app#(app(d, z), app(app(g, x), y)) → app#(d, z)
app#(app(d, z), app(app(g, x), y)) → app#(g, app(e, x))app#(app(map, f), app(app(cons, x), xs)) → app#(app(map, f), xs)
app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(app(d, app(c, z)), app(app(g, x), y))app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(app(g, x), y)
app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(app(d, z), app(app(g, x), y))app#(app(filter, f), app(app(cons, x), xs)) → app#(app(app(filter2, app(f, x)), f), x)
app#(app(h, z), app(e, x)) → app#(app(d, z), x)app#(app(h, z), app(e, x)) → app#(c, z)
app#(app(g, app(e, x)), app(e, y)) → app#(app(g, x), y)app#(app(app(app(filter2, true), f), x), xs) → app#(cons, x)
app#(app(filter, f), app(app(cons, x), xs)) → app#(app(filter2, app(f, x)), f)app#(app(app(app(filter2, false), f), x), xs) → app#(app(filter, f), xs)
app#(app(d, z), app(app(g, x), y)) → app#(app(g, app(e, x)), app(app(d, z), y))app#(app(d, z), app(app(g, 0), 0)) → app#(e, 0)
app#(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app#(g, x)app#(app(map, f), app(app(cons, x), xs)) → app#(cons, app(f, x))
app#(app(d, z), app(app(g, x), y)) → app#(app(d, z), y)

Rewrite Rules

app(app(h, z), app(e, x)) → app(app(h, app(c, z)), app(app(d, z), x))app(app(d, z), app(app(g, 0), 0)) → app(e, 0)
app(app(d, z), app(app(g, x), y)) → app(app(g, app(e, x)), app(app(d, z), y))app(app(d, app(c, z)), app(app(g, app(app(g, x), y)), 0)) → app(app(g, app(app(d, app(c, z)), app(app(g, x), y))), app(app(d, z), app(app(g, x), y)))
app(app(g, app(e, x)), app(e, y)) → app(e, app(app(g, x), y))app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))app(app(filter, f), nil) → nil
app(app(filter, f), app(app(cons, x), xs)) → app(app(app(app(filter2, app(f, x)), f), x), xs)app(app(app(app(filter2, true), f), x), xs) → app(app(cons, x), app(app(filter, f), xs))
app(app(app(app(filter2, false), f), x), xs) → app(app(filter, f), xs)

Original Signature

Termination of terms over the following signature is verified: app, g, d, e, c, true, h, 0, map, false, filter2, filter, nil, cons