The TRS could not be proven terminating. The proof attempt took 60001 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (64ms), SubtermCriterion (1ms), DependencyGraph (32ms), PolynomialLinearRange4iUR (1964ms), DependencyGraph (33ms), PolynomialLinearRange8NegiUR (10795ms), DependencyGraph (30ms), ReductionPairSAT (timeout)].
| app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(app(mapbt, f), r) | app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(mapbt, f) | |
| app#(app(mapbt, f), app(leaf, x)) | → | app#(f, x) | app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(app(branch, app(f, x)), app(app(mapbt, f), l)) | |
| app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(app(mapbt, f), l) | app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(f, x) | |
| app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r)) | app#(app(mapbt, f), app(leaf, x)) | → | app#(leaf, app(f, x)) | |
| app#(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app#(branch, app(f, x)) |
| app(app(mapbt, f), app(leaf, x)) | → | app(leaf, app(f, x)) | app(app(mapbt, f), app(app(app(branch, x), l), r)) | → | app(app(app(branch, app(f, x)), app(app(mapbt, f), l)), app(app(mapbt, f), r)) |
Termination of terms over the following signature is verified: mapbt, app, branch, leaf