KILLED
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).

(0) CpxRelTRS


----------------------------------------

(0)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, INF).


The TRS R consists of the following rules:

   F(true, z0, z1, z2) -> c(F(and(gt(z0, z1), gt(z0, z2)), z0, s(z1), z2), AND(gt(z0, z1), gt(z0, z2)), GT(z0, z1))
   F(true, z0, z1, z2) -> c1(F(and(gt(z0, z1), gt(z0, z2)), z0, s(z1), z2), AND(gt(z0, z1), gt(z0, z2)), GT(z0, z2))
   F(true, z0, z1, z2) -> c2(F(and(gt(z0, z1), gt(z0, z2)), z0, z1, s(z2)), AND(gt(z0, z1), gt(z0, z2)), GT(z0, z1))
   F(true, z0, z1, z2) -> c3(F(and(gt(z0, z1), gt(z0, z2)), z0, z1, s(z2)), AND(gt(z0, z1), gt(z0, z2)), GT(z0, z2))
   GT(0, z0) -> c4
   GT(s(z0), 0) -> c5
   GT(s(z0), s(z1)) -> c6(GT(z0, z1))
   AND(z0, true) -> c7
   AND(z0, false) -> c8

The (relative) TRS S consists of the following rules:

   f(true, z0, z1, z2) -> f(and(gt(z0, z1), gt(z0, z2)), z0, s(z1), z2)
   f(true, z0, z1, z2) -> f(and(gt(z0, z1), gt(z0, z2)), z0, z1, s(z2))
   gt(0, z0) -> false
   gt(s(z0), 0) -> true
   gt(s(z0), s(z1)) -> gt(z0, z1)
   and(z0, true) -> z0
   and(z0, false) -> false

Rewrite Strategy: INNERMOST