The TRS could not be proven terminating. The proof attempt took 53865 ms.
Problem 1 remains open; application of the following processors failed [DependencyGraph (86ms), SubtermCriterion (1ms), DependencyGraph (55ms), PolynomialLinearRange4iUR (2335ms), DependencyGraph (53ms), PolynomialLinearRange8NegiUR (14822ms), DependencyGraph (42ms), ReductionPairSAT (36030ms), DependencyGraph (39ms), SizeChangePrinciple (43ms)].
| 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, x), false) | → | false | |
| app(app(and, false), y) | → | false | app(app(or, true), y) | → | true | |
| app(app(or, x), 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