TIMEOUT

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

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (841ms).
 | – Problem 2 remains open; application of the following processors failed [SubtermCriterion (1ms), DependencyGraph (350ms), PolynomialLinearRange4iUR (4451ms), DependencyGraph (333ms), PolynomialLinearRange8NegiUR (12817ms), DependencyGraph (296ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 2

Dependency Pairs

app#(sum, l) → app#(app(app(fold, add), id), 0)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(f_3, app(g_2, z)), app(app(app(app(fold, f_3), g_2), x), t))
app#(app(app(swap, f_2), y), x) → app#(app(f_2, x), y)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(fold, f_3), g_2)
app#(app(app(compose, g_1), f_1), x) → app#(f_1, x)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(fold, f_3)
app#(listify, x) → app#(app(cons, x), nil)app#(app(app(compose, g_1), f_1), x) → app#(g_1, app(f_1, x))
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(app(app(fold, f_3), g_2), x), t)app#(listify, x) → app#(cons, x)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(app(fold, f_3), g_2), x)app#(sum, l) → app#(fold, add)
app#(sum, l) → app#(app(fold, add), id)app#(app(app(uncurry, f_2), x), y) → app#(app(f_2, x), y)
app#(app(app(uncurry, f_2), x), y) → app#(f_2, x)app#(app(apply, f_1), x) → app#(f_1, x)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(f_3, app(g_2, z))app#(sum, l) → app#(app(app(app(fold, add), id), 0), l)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(g_2, z)app#(app(app(swap, f_2), y), x) → app#(f_2, x)

Rewrite Rules

app(app(apply, f_1), x) → app(f_1, x)app(id, x) → x
app(app(app(uncurry, f_2), x), y) → app(app(f_2, x), y)app(app(app(swap, f_2), y), x) → app(app(f_2, x), y)
app(app(app(compose, g_1), f_1), x) → app(g_1, app(f_1, x))app(app(const, x), y) → x
app(listify, x) → app(app(cons, x), nil)app(app(app(app(fold, f_3), g_2), x), nil) → x
app(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app(app(f_3, app(g_2, z)), app(app(app(app(fold, f_3), g_2), x), t))app(sum, l) → app(app(app(app(fold, add), id), 0), l)
app(app(uncurry, app(app(fold, cons), id)), nil) → idappend → app(app(compose, app(app(swap, fold), cons)), id)
reverse → app(app(uncurry, app(app(fold, app(swap, append)), listify)), nil)length → app(app(uncurry, app(app(fold, add), app(cons, 1))), 0)

Original Signature

Termination of terms over the following signature is verified: append, app, apply, reverse, const, sum, add, fold, id, 1, 0, uncurry, length, compose, listify, swap, cons, nil

Problem 1: DependencyGraph

Dependency Pair Problem

Dependency Pairs

append# → app#(swap, fold)app#(sum, l) → app#(app(app(fold, add), id), 0)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(f_3, app(g_2, z)), app(app(app(app(fold, f_3), g_2), x), t))app#(app(app(swap, f_2), y), x) → app#(app(f_2, x), y)
length# → app#(app(fold, add), app(cons, 1))app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(fold, f_3)
app#(listify, x) → app#(app(cons, x), nil)append# → app#(app(compose, app(app(swap, fold), cons)), id)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(app(app(fold, f_3), g_2), x), t)length# → app#(fold, add)
app#(listify, x) → app#(cons, x)app#(sum, l) → app#(fold, add)
app#(sum, l) → app#(app(fold, add), id)app#(app(app(uncurry, f_2), x), y) → app#(f_2, x)
app#(app(apply, f_1), x) → app#(f_1, x)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(f_3, app(g_2, z))
length# → app#(cons, 1)append# → app#(app(swap, fold), cons)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(fold, f_3), g_2)app#(app(app(compose, g_1), f_1), x) → app#(f_1, x)
reverse# → app#(app(fold, app(swap, append)), listify)app#(app(app(compose, g_1), f_1), x) → app#(g_1, app(f_1, x))
length# → app#(uncurry, app(app(fold, add), app(cons, 1)))append# → app#(compose, app(app(swap, fold), cons))
reverse# → app#(swap, append)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(app(fold, f_3), g_2), x)
reverse# → app#(fold, app(swap, append))app#(app(app(uncurry, f_2), x), y) → app#(app(f_2, x), y)
reverse# → app#(uncurry, app(app(fold, app(swap, append)), listify))reverse# → app#(app(uncurry, app(app(fold, app(swap, append)), listify)), nil)
reverse# → append#length# → app#(app(uncurry, app(app(fold, add), app(cons, 1))), 0)
app#(sum, l) → app#(app(app(app(fold, add), id), 0), l)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(g_2, z)
app#(app(app(swap, f_2), y), x) → app#(f_2, x)

Rewrite Rules

app(app(apply, f_1), x) → app(f_1, x)app(id, x) → x
app(app(app(uncurry, f_2), x), y) → app(app(f_2, x), y)app(app(app(swap, f_2), y), x) → app(app(f_2, x), y)
app(app(app(compose, g_1), f_1), x) → app(g_1, app(f_1, x))app(app(const, x), y) → x
app(listify, x) → app(app(cons, x), nil)app(app(app(app(fold, f_3), g_2), x), nil) → x
app(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app(app(f_3, app(g_2, z)), app(app(app(app(fold, f_3), g_2), x), t))app(sum, l) → app(app(app(app(fold, add), id), 0), l)
app(app(uncurry, app(app(fold, cons), id)), nil) → idappend → app(app(compose, app(app(swap, fold), cons)), id)
reverse → app(app(uncurry, app(app(fold, app(swap, append)), listify)), nil)length → app(app(uncurry, app(app(fold, add), app(cons, 1))), 0)

Original Signature

Termination of terms over the following signature is verified: append, app, apply, reverse, const, sum, add, fold, id, 1, 0, uncurry, length, compose, listify, swap, nil, cons

Strategy

The following SCCs where found

app#(sum, l) → app#(app(app(fold, add), id), 0)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(f_3, app(g_2, z)), app(app(app(app(fold, f_3), g_2), x), t))
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(fold, f_3), g_2)app#(app(app(swap, f_2), y), x) → app#(app(f_2, x), y)
app#(app(app(compose, g_1), f_1), x) → app#(f_1, x)app#(listify, x) → app#(app(cons, x), nil)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(fold, f_3)app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(app(app(fold, f_3), g_2), x), t)
app#(app(app(compose, g_1), f_1), x) → app#(g_1, app(f_1, x))app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(app(app(fold, f_3), g_2), x)
app#(listify, x) → app#(cons, x)app#(sum, l) → app#(app(fold, add), id)
app#(sum, l) → app#(fold, add)app#(app(app(uncurry, f_2), x), y) → app#(app(f_2, x), y)
app#(app(app(uncurry, f_2), x), y) → app#(f_2, x)app#(app(apply, f_1), x) → app#(f_1, x)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(f_3, app(g_2, z))app#(sum, l) → app#(app(app(app(fold, add), id), 0), l)
app#(app(app(app(fold, f_3), g_2), x), app(app(cons, z), t)) → app#(g_2, z)app#(app(app(swap, f_2), y), x) → app#(f_2, x)