KILLED
proof of /export/starexec/sandbox2/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:

   COND1(true, z0, z1, z2) -> c(COND2(gr(z1, z2), z0, z1, z2), GR(z1, z2))
   COND2(true, z0, z1, z2) -> c1(COND2(gr(z1, z2), p(z0), p(z1), z2), GR(z1, z2))
   COND2(true, z0, z1, z2) -> c2(COND2(gr(z1, z2), p(z0), p(z1), z2), P(z0))
   COND2(true, z0, z1, z2) -> c3(COND2(gr(z1, z2), p(z0), p(z1), z2), P(z1))
   COND2(false, z0, z1, z2) -> c4(COND1(and(eq(z0, z1), gr(z0, z2)), z0, z1, z2), AND(eq(z0, z1), gr(z0, z2)), EQ(z0, z1))
   COND2(false, z0, z1, z2) -> c5(COND1(and(eq(z0, z1), gr(z0, z2)), z0, z1, z2), AND(eq(z0, z1), gr(z0, z2)), GR(z0, z2))
   GR(0, z0) -> c6
   GR(s(z0), 0) -> c7
   GR(s(z0), s(z1)) -> c8(GR(z0, z1))
   P(0) -> c9
   P(s(z0)) -> c10
   EQ(0, 0) -> c11
   EQ(s(z0), 0) -> c12
   EQ(0, s(z0)) -> c13
   EQ(s(z0), s(z1)) -> c14(EQ(z0, z1))
   AND(true, true) -> c15
   AND(false, z0) -> c16
   AND(z0, false) -> c17

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

   cond1(true, z0, z1, z2) -> cond2(gr(z1, z2), z0, z1, z2)
   cond2(true, z0, z1, z2) -> cond2(gr(z1, z2), p(z0), p(z1), z2)
   cond2(false, z0, z1, z2) -> cond1(and(eq(z0, z1), gr(z0, z2)), z0, z1, z2)
   gr(0, z0) -> false
   gr(s(z0), 0) -> true
   gr(s(z0), s(z1)) -> gr(z0, z1)
   p(0) -> 0
   p(s(z0)) -> z0
   eq(0, 0) -> true
   eq(s(z0), 0) -> false
   eq(0, s(z0)) -> false
   eq(s(z0), s(z1)) -> eq(z0, z1)
   and(true, true) -> true
   and(false, z0) -> false
   and(z0, false) -> false

Rewrite Strategy: INNERMOST