TIMEOUT

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

The following DP Processors were used

Problem 1 remains open; application of the following processors failed [DependencyGraph (2305ms), SubtermCriterion (1ms), DependencyGraph (2305ms), PolynomialLinearRange4iUR (9391ms), DependencyGraph (2185ms), PolynomialLinearRange8NegiUR (timeout), DependencyGraph (2182ms), ReductionPairSAT (timeout)].

The following open problems remain:

Open Dependency Pair Problem 1

Dependency Pairs

app^#(app(*, x), app(app(+, y), z))	→	app^#(+, app(app(*, x), y))		app^#(app(map, f), app(app(cons, x), xs))	→	app^#(app(cons, app(f, x)), app(app(map, f), xs))
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(f, x)		app^#(app(*, app(app(+, y), z)), x)	→	app^#(+, app(app(*, x), y))
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(, x), y)), z)	→	app^#(*, x)		app^#(app(*, app(app(+, y), z)), x)	→	app^#(app(+, app(app(, x), y)), app(app(, x), z))
app^#(app(*, x), app(app(+, y), z))	→	app^#(app(+, app(app(, x), y)), app(app(, x), z))		app^#(app(app(app(filter2, true), f), x), xs)	→	app^#(filter, f)
app^#(app(app(app(filter2, true), f), x), xs)	→	app^#(app(filter, f), xs)		app^#(app(*, app(app(+, y), z)), x)	→	app^#(app(*, x), y)
app^#(app(filter, f), app(app(cons, x), xs))	→	app^#(app(app(app(filter2, app(f, x)), f), x), xs)		app^#(app(*, x), app(app(+, y), z))	→	app^#(*, x)
app^#(app(*, app(app(+, y), z)), x)	→	app^#(app(*, x), z)		app^#(app(+, app(app(+, x), y)), z)	→	app^#(app(+, x), app(app(+, y), z))
app^#(app(filter, f), app(app(cons, x), xs))	→	app^#(filter2, app(f, x))		app^#(app(map, f), app(app(cons, x), xs))	→	app^#(map, f)
app^#(app(app(app(filter2, false), f), x), xs)	→	app^#(filter, f)		app^#(app(, app(app(, x), y)), z)	→	app^#(app(*, y), z)
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(app(map, f), xs)		app^#(app(*, app(app(+, y), z)), x)	→	app^#(*, x)
app^#(app(, app(app(, x), y)), z)	→	app^#(app(, x), app(app(, y), z))		app^#(app(filter, f), app(app(cons, x), xs))	→	app^#(app(app(filter2, app(f, x)), f), x)
app^#(app(+, app(app(+, x), y)), z)	→	app^#(+, x)		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(*, x), app(app(+, y), z))	→	app^#(app(*, x), z)
app^#(app(, app(app(, x), y)), z)	→	app^#(*, y)		app^#(app(+, app(app(+, x), y)), z)	→	app^#(app(+, y), z)
app^#(app(app(app(filter2, false), f), x), xs)	→	app^#(app(filter, f), xs)		app^#(app(*, x), app(app(+, y), z))	→	app^#(app(*, x), y)
app^#(app(map, f), app(app(cons, x), xs))	→	app^#(cons, app(f, x))		app^#(app(+, app(app(+, x), y)), z)	→	app^#(+, y)

Rewrite Rules

app(app(*, x), app(app(+, y), z))	→	app(app(+, app(app(, x), y)), app(app(, x), z))		app(app(*, app(app(+, y), z)), x)	→	app(app(+, app(app(, x), y)), app(app(, x), z))
app(app(, app(app(, x), y)), z)	→	app(app(, x), app(app(, y), z))		app(app(+, app(app(+, x), y)), z)	→	app(app(+, x), app(app(+, y), z))
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, map, *, false, true, +, filter2, filter, cons, nil