The TRS could not be proven terminating. The proof attempt took 60096 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (95ms), SubtermCriterion (1ms), DependencyGraph (62ms), PolynomialLinearRange4iUR (2506ms), DependencyGraph (57ms), PolynomialLinearRange8NegiUR (15987ms), DependencyGraph (44ms), ReductionPairSAT (timeout)].
| app#(app(forall, p), app(app(cons, x), xs)) | → | app#(app(and, app(p, x)), app(app(forall, p), xs)) | app#(app(forsome, p), app(app(cons, x), xs)) | → | app#(forsome, p) | |
| app#(app(forsome, p), app(app(cons, x), xs)) | → | app#(app(or, app(p, x)), app(app(forsome, p), xs)) | app#(app(forsome, p), app(app(cons, x), xs)) | → | app#(app(forsome, p), xs) | |
| app#(app(forall, p), app(app(cons, x), xs)) | → | app#(forall, p) | app#(app(forall, p), app(app(cons, x), xs)) | → | app#(and, app(p, x)) | |
| app#(app(forall, p), app(app(cons, x), xs)) | → | app#(p, x) | app#(app(forall, p), app(app(cons, x), xs)) | → | app#(app(forall, p), xs) | |
| app#(app(forsome, p), app(app(cons, x), xs)) | → | app#(p, x) | app#(app(forsome, p), app(app(cons, x), xs)) | → | app#(or, app(p, x)) |
| app(app(and, true), true) | → | true | app(app(and, true), false) | → | false | |
| app(app(and, false), true) | → | false | app(app(and, false), false) | → | false | |
| app(app(or, true), true) | → | true | app(app(or, true), false) | → | true | |
| app(app(or, false), true) | → | true | app(app(or, false), false) | → | false | |
| app(app(forall, p), nil) | → | true | app(app(forall, p), app(app(cons, x), xs)) | → | app(app(and, app(p, x)), app(app(forall, p), xs)) | |
| app(app(forsome, p), nil) | → | false | app(app(forsome, p), app(app(cons, x), xs)) | → | app(app(or, app(p, x)), app(app(forsome, p), xs)) |
Termination of terms over the following signature is verified: app, or, forsome, false, true, forall, cons, nil, and