YES(O(1), O(1)) 0.00/0.59 YES(O(1), O(1)) 0.00/0.63 0.00/0.63 0.00/0.63 0.00/0.63 0.00/0.63 0.00/0.63 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 0.00/0.63 0.00/0.63 0.00/0.63
0.00/0.63
0.00/0.63
0.00/0.63
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(1)).

0 CpxTRS
0.00/0.63 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
0.00/0.63 
↳2 CdtProblem
0.00/0.63 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
0.00/0.63 
↳4 CdtProblem
0.00/0.63 
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
0.00/0.63 
↳6 CdtProblem
0.00/0.63 
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))
0.00/0.63 
↳8 BOUNDS(O(1), O(1))
0.00/0.63
0.00/0.63 0.00/0.63
0.00/0.63
0.00/0.63

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f0(S(x''), S(x'), x3, S(x), y) → f1(x', S(x'), x, S(x), S(S(y))) 0.00/0.63
f4(S(x'), S(x'), x3, x4, S(x)) → f4[Ite][False][Ite][False][Ite](False, S(x'), S(x'), x3, x4, S(x)) 0.00/0.63
f4(S(x'), S(x), x3, x4, 0) → f4[Ite][False][Ite][False][Ite](True, S(x'), S(x), x3, x4, 0) 0.00/0.63
f4(S(x'), 0, x3, x4, S(x)) → f4[Ite][False][Ite][True][Ite](False, S(x'), 0, x3, x4, S(x)) 0.00/0.63
f4(S(x), 0, x3, x4, 0) → f4[Ite][False][Ite][True][Ite](True, S(x), 0, x3, x4, 0) 0.00/0.63
f2(x1, x2, S(x'), S(x'), S(x)) → f2[Ite][False][Ite][False][Ite](False, x1, x2, S(x'), S(x'), S(x)) 0.00/0.63
f2(x1, x2, S(x'), S(x), 0) → f2[Ite][False][Ite][False][Ite](True, x1, x2, S(x'), S(x), 0) 0.00/0.63
f2(x1, x2, S(x'), 0, S(x)) → f2[Ite][False][Ite][True][Ite](False, x1, x2, S(x'), 0, S(x)) 0.00/0.63
f2(x1, x2, S(x), 0, 0) → f2[Ite][False][Ite][True][Ite](True, x1, x2, S(x), 0, 0) 0.00/0.63
f0(S(x), x2, x3, 0, x5) → 0 0.00/0.63
f6(x1, x2, x3, x4, S(x)) → f0(x1, x2, x4, x3, x) 0.00/0.63
f5(x1, x2, x3, x4, S(x)) → f6(x2, x1, x3, x4, x) 0.00/0.63
f3(x1, x2, x3, x4, S(x)) → f4(x1, x2, x4, x3, x) 0.00/0.63
f1(x1, x2, x3, x4, S(x)) → f2(x2, x1, x3, x4, x) 0.00/0.63
f6(x1, x2, x3, x4, 0) → 0 0.00/0.63
f5(x1, x2, x3, x4, 0) → 0 0.00/0.63
f4(0, x2, x3, x4, x5) → 0 0.00/0.63
f3(x1, x2, x3, x4, 0) → 0 0.00/0.63
f2(x1, x2, 0, x4, x5) → 0 0.00/0.63
f1(x1, x2, x3, x4, 0) → 0 0.00/0.63
f0(0, x2, x3, x4, x5) → 0

Rewrite Strategy: INNERMOST
0.00/0.63
0.00/0.63

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT
0.00/0.63
0.00/0.63

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f0(S(z0), S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(S(z4))) 0.00/0.63
f0(S(z0), z1, z2, 0, z3) → 0 0.00/0.63
f0(0, z0, z1, z2, z3) → 0 0.00/0.63
f4(S(z0), S(z0), z1, z2, S(z3)) → f4[Ite][False][Ite][False][Ite](False, S(z0), S(z0), z1, z2, S(z3)) 0.00/0.63
f4(S(z0), S(z1), z2, z3, 0) → f4[Ite][False][Ite][False][Ite](True, S(z0), S(z1), z2, z3, 0) 0.00/0.63
f4(S(z0), 0, z1, z2, S(z3)) → f4[Ite][False][Ite][True][Ite](False, S(z0), 0, z1, z2, S(z3)) 0.00/0.63
f4(S(z0), 0, z1, z2, 0) → f4[Ite][False][Ite][True][Ite](True, S(z0), 0, z1, z2, 0) 0.00/0.63
f4(0, z0, z1, z2, z3) → 0 0.00/0.63
f2(z0, z1, S(z2), S(z2), S(z3)) → f2[Ite][False][Ite][False][Ite](False, z0, z1, S(z2), S(z2), S(z3)) 0.00/0.63
f2(z0, z1, S(z2), S(z3), 0) → f2[Ite][False][Ite][False][Ite](True, z0, z1, S(z2), S(z3), 0) 0.00/0.63
f2(z0, z1, S(z2), 0, S(z3)) → f2[Ite][False][Ite][True][Ite](False, z0, z1, S(z2), 0, S(z3)) 0.00/0.63
f2(z0, z1, S(z2), 0, 0) → f2[Ite][False][Ite][True][Ite](True, z0, z1, S(z2), 0, 0) 0.00/0.63
f2(z0, z1, 0, z2, z3) → 0 0.00/0.63
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4) 0.00/0.63
f6(z0, z1, z2, z3, 0) → 0 0.00/0.63
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4) 0.00/0.63
f5(z0, z1, z2, z3, 0) → 0 0.00/0.63
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4) 0.00/0.63
f3(z0, z1, z2, z3, 0) → 0 0.00/0.63
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4) 0.00/0.63
f1(z0, z1, z2, z3, 0) → 0
Tuples:

F0(S(z0), S(z1), z2, S(z3), z4) → c(F1(z1, S(z1), z3, S(z3), S(S(z4)))) 0.00/0.63
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4)) 0.00/0.63
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4)) 0.00/0.63
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4)) 0.00/0.63
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
S tuples:

F0(S(z0), S(z1), z2, S(z3), z4) → c(F1(z1, S(z1), z3, S(z3), S(S(z4)))) 0.00/0.63
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4)) 0.00/0.63
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4)) 0.00/0.63
F3(z0, z1, z2, z3, S(z4)) → c17(F4(z0, z1, z3, z2, z4)) 0.00/0.63
F1(z0, z1, z2, z3, S(z4)) → c19(F2(z1, z0, z2, z3, z4))
K tuples:none
Defined Rule Symbols:

f0, f4, f2, f6, f5, f3, f1

Defined Pair Symbols:

F0, F6, F5, F3, F1

Compound Symbols:

c, c13, c15, c17, c19

0.00/0.63
0.00/0.63

(3) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts
0.00/0.63
0.00/0.63

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f0(S(z0), S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(S(z4))) 0.00/0.63
f0(S(z0), z1, z2, 0, z3) → 0 0.00/0.63
f0(0, z0, z1, z2, z3) → 0 0.00/0.63
f4(S(z0), S(z0), z1, z2, S(z3)) → f4[Ite][False][Ite][False][Ite](False, S(z0), S(z0), z1, z2, S(z3)) 0.00/0.63
f4(S(z0), S(z1), z2, z3, 0) → f4[Ite][False][Ite][False][Ite](True, S(z0), S(z1), z2, z3, 0) 0.00/0.63
f4(S(z0), 0, z1, z2, S(z3)) → f4[Ite][False][Ite][True][Ite](False, S(z0), 0, z1, z2, S(z3)) 0.00/0.63
f4(S(z0), 0, z1, z2, 0) → f4[Ite][False][Ite][True][Ite](True, S(z0), 0, z1, z2, 0) 0.00/0.63
f4(0, z0, z1, z2, z3) → 0 0.00/0.63
f2(z0, z1, S(z2), S(z2), S(z3)) → f2[Ite][False][Ite][False][Ite](False, z0, z1, S(z2), S(z2), S(z3)) 0.00/0.63
f2(z0, z1, S(z2), S(z3), 0) → f2[Ite][False][Ite][False][Ite](True, z0, z1, S(z2), S(z3), 0) 0.00/0.63
f2(z0, z1, S(z2), 0, S(z3)) → f2[Ite][False][Ite][True][Ite](False, z0, z1, S(z2), 0, S(z3)) 0.00/0.63
f2(z0, z1, S(z2), 0, 0) → f2[Ite][False][Ite][True][Ite](True, z0, z1, S(z2), 0, 0) 0.00/0.63
f2(z0, z1, 0, z2, z3) → 0 0.00/0.63
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4) 0.00/0.63
f6(z0, z1, z2, z3, 0) → 0 0.00/0.63
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4) 0.00/0.63
f5(z0, z1, z2, z3, 0) → 0 0.00/0.63
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4) 0.00/0.63
f3(z0, z1, z2, z3, 0) → 0 0.00/0.63
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4) 0.00/0.63
f1(z0, z1, z2, z3, 0) → 0
Tuples:

F0(S(z0), S(z1), z2, S(z3), z4) → c(F1(z1, S(z1), z3, S(z3), S(S(z4)))) 0.00/0.63
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4)) 0.00/0.63
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4)) 0.00/0.63
F3(z0, z1, z2, z3, S(z4)) → c17 0.00/0.63
F1(z0, z1, z2, z3, S(z4)) → c19
S tuples:

F0(S(z0), S(z1), z2, S(z3), z4) → c(F1(z1, S(z1), z3, S(z3), S(S(z4)))) 0.00/0.63
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4)) 0.00/0.63
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4)) 0.00/0.63
F3(z0, z1, z2, z3, S(z4)) → c17 0.00/0.63
F1(z0, z1, z2, z3, S(z4)) → c19
K tuples:none
Defined Rule Symbols:

f0, f4, f2, f6, f5, f3, f1

Defined Pair Symbols:

F0, F6, F5, F3, F1

Compound Symbols:

c, c13, c15, c17, c19

0.00/0.63
0.00/0.63

(5) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 5 trailing nodes:

F1(z0, z1, z2, z3, S(z4)) → c19 0.00/0.63
F0(S(z0), S(z1), z2, S(z3), z4) → c(F1(z1, S(z1), z3, S(z3), S(S(z4)))) 0.00/0.63
F3(z0, z1, z2, z3, S(z4)) → c17 0.00/0.63
F5(z0, z1, z2, z3, S(z4)) → c15(F6(z1, z0, z2, z3, z4)) 0.00/0.63
F6(z0, z1, z2, z3, S(z4)) → c13(F0(z0, z1, z3, z2, z4))
0.00/0.63
0.00/0.63

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f0(S(z0), S(z1), z2, S(z3), z4) → f1(z1, S(z1), z3, S(z3), S(S(z4))) 0.00/0.63
f0(S(z0), z1, z2, 0, z3) → 0 0.00/0.63
f0(0, z0, z1, z2, z3) → 0 0.00/0.63
f4(S(z0), S(z0), z1, z2, S(z3)) → f4[Ite][False][Ite][False][Ite](False, S(z0), S(z0), z1, z2, S(z3)) 0.00/0.63
f4(S(z0), S(z1), z2, z3, 0) → f4[Ite][False][Ite][False][Ite](True, S(z0), S(z1), z2, z3, 0) 0.00/0.63
f4(S(z0), 0, z1, z2, S(z3)) → f4[Ite][False][Ite][True][Ite](False, S(z0), 0, z1, z2, S(z3)) 0.00/0.63
f4(S(z0), 0, z1, z2, 0) → f4[Ite][False][Ite][True][Ite](True, S(z0), 0, z1, z2, 0) 0.00/0.63
f4(0, z0, z1, z2, z3) → 0 0.00/0.63
f2(z0, z1, S(z2), S(z2), S(z3)) → f2[Ite][False][Ite][False][Ite](False, z0, z1, S(z2), S(z2), S(z3)) 0.00/0.63
f2(z0, z1, S(z2), S(z3), 0) → f2[Ite][False][Ite][False][Ite](True, z0, z1, S(z2), S(z3), 0) 0.00/0.63
f2(z0, z1, S(z2), 0, S(z3)) → f2[Ite][False][Ite][True][Ite](False, z0, z1, S(z2), 0, S(z3)) 0.00/0.63
f2(z0, z1, S(z2), 0, 0) → f2[Ite][False][Ite][True][Ite](True, z0, z1, S(z2), 0, 0) 0.00/0.63
f2(z0, z1, 0, z2, z3) → 0 0.00/0.63
f6(z0, z1, z2, z3, S(z4)) → f0(z0, z1, z3, z2, z4) 0.00/0.63
f6(z0, z1, z2, z3, 0) → 0 0.00/0.63
f5(z0, z1, z2, z3, S(z4)) → f6(z1, z0, z2, z3, z4) 0.00/0.63
f5(z0, z1, z2, z3, 0) → 0 0.00/0.63
f3(z0, z1, z2, z3, S(z4)) → f4(z0, z1, z3, z2, z4) 0.00/0.63
f3(z0, z1, z2, z3, 0) → 0 0.00/0.63
f1(z0, z1, z2, z3, S(z4)) → f2(z1, z0, z2, z3, z4) 0.00/0.63
f1(z0, z1, z2, z3, 0) → 0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f0, f4, f2, f6, f5, f3, f1

Defined Pair Symbols:none

Compound Symbols:none

0.00/0.63
0.00/0.63

(7) SIsEmptyProof (BOTH BOUNDS(ID, ID) transformation)

The set S is empty
0.00/0.63
0.00/0.63

(8) BOUNDS(O(1), O(1))

0.00/0.63
0.00/0.63
0.00/0.69 EOF