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

0 CpxTRS
0.00/0.58 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
0.00/0.58 
↳2 CdtProblem
0.00/0.58 
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
0.00/0.58 
↳4 CdtProblem
0.00/0.58 
↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
0.00/0.58 
↳6 CdtProblem
0.00/0.58 
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))
0.00/0.58 
↳8 CdtProblem
0.00/0.58 
↳9 CdtKnowledgeProof (⇔)
0.00/0.58 
↳10 BOUNDS(O(1), O(1))
0.00/0.58
0.00/0.58 0.00/0.58
0.00/0.58
0.00/0.58

(0) Obligation:

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

f(x, y, z) → g(<=(x, y), x, y, z) 0.00/0.58
g(true, x, y, z) → z 0.00/0.58
g(false, x, y, z) → f(f(p(x), y, z), f(p(y), z, x), f(p(z), x, y)) 0.00/0.58
p(0) → 0 0.00/0.58
p(s(x)) → x

Rewrite Strategy: INNERMOST
0.00/0.58
0.00/0.58

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

Converted CpxTRS to CDT
0.00/0.58
0.00/0.58

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1, z2) → g(<=(z0, z1), z0, z1, z2) 0.00/0.58
g(true, z0, z1, z2) → z2 0.00/0.58
g(false, z0, z1, z2) → f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)) 0.00/0.58
p(0) → 0 0.00/0.58
p(s(z0)) → z0
Tuples:

F(z0, z1, z2) → c(G(<=(z0, z1), z0, z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), P(z0), F(p(z1), z2, z0), P(z1), F(p(z2), z0, z1), P(z2))
S tuples:

F(z0, z1, z2) → c(G(<=(z0, z1), z0, z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), P(z0), F(p(z1), z2, z0), P(z1), F(p(z2), z0, z1), P(z2))
K tuples:none
Defined Rule Symbols:

f, g, p

Defined Pair Symbols:

F, G

Compound Symbols:

c, c2

0.00/0.58
0.00/0.58

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

Removed 4 trailing tuple parts
0.00/0.58
0.00/0.58

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1, z2) → g(<=(z0, z1), z0, z1, z2) 0.00/0.58
g(true, z0, z1, z2) → z2 0.00/0.58
g(false, z0, z1, z2) → f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)) 0.00/0.58
p(0) → 0 0.00/0.58
p(s(z0)) → z0
Tuples:

F(z0, z1, z2) → c 0.00/0.58
G(false, z0, z1, z2) → c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), F(p(z1), z2, z0), F(p(z2), z0, z1))
S tuples:

F(z0, z1, z2) → c 0.00/0.58
G(false, z0, z1, z2) → c2(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)), F(p(z0), z1, z2), F(p(z1), z2, z0), F(p(z2), z0, z1))
K tuples:none
Defined Rule Symbols:

f, g, p

Defined Pair Symbols:

F, G

Compound Symbols:

c, c2

0.00/0.58
0.00/0.58

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

Split RHS of tuples not part of any SCC
0.00/0.58
0.00/0.58

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1, z2) → g(<=(z0, z1), z0, z1, z2) 0.00/0.58
g(true, z0, z1, z2) → z2 0.00/0.58
g(false, z0, z1, z2) → f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)) 0.00/0.58
p(0) → 0 0.00/0.58
p(s(z0)) → z0
Tuples:

F(z0, z1, z2) → c 0.00/0.58
G(false, z0, z1, z2) → c1(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z0), z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z1), z2, z0)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z2), z0, z1))
S tuples:

F(z0, z1, z2) → c 0.00/0.58
G(false, z0, z1, z2) → c1(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z0), z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z1), z2, z0)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z2), z0, z1))
K tuples:none
Defined Rule Symbols:

f, g, p

Defined Pair Symbols:

F, G

Compound Symbols:

c, c1

0.00/0.58
0.00/0.58

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

Removed 5 trailing nodes:

G(false, z0, z1, z2) → c1(F(p(z0), z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z1), z2, z0)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z2), z0, z1)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))) 0.00/0.58
F(z0, z1, z2) → c
0.00/0.58
0.00/0.58

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1, z2) → g(<=(z0, z1), z0, z1, z2) 0.00/0.58
g(true, z0, z1, z2) → z2 0.00/0.58
g(false, z0, z1, z2) → f(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1)) 0.00/0.58
p(0) → 0 0.00/0.58
p(s(z0)) → z0
Tuples:

F(z0, z1, z2) → c 0.00/0.58
G(false, z0, z1, z2) → c1(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z0), z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z1), z2, z0)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z2), z0, z1))
S tuples:

F(z0, z1, z2) → c 0.00/0.58
G(false, z0, z1, z2) → c1(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z0), z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z1), z2, z0)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z2), z0, z1))
K tuples:none
Defined Rule Symbols:

f, g, p

Defined Pair Symbols:

F, G

Compound Symbols:

c, c1

0.00/0.58
0.00/0.58

(9) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

G(false, z0, z1, z2) → c1(F(f(p(z0), z1, z2), f(p(z1), z2, z0), f(p(z2), z0, z1))) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z0), z1, z2)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z1), z2, z0)) 0.00/0.58
G(false, z0, z1, z2) → c1(F(p(z2), z0, z1)) 0.00/0.58
F(z0, z1, z2) → c 0.00/0.58
F(z0, z1, z2) → c 0.00/0.58
F(z0, z1, z2) → c 0.00/0.58
F(z0, z1, z2) → c
Now S is empty
0.00/0.58
0.00/0.58

(10) BOUNDS(O(1), O(1))

0.00/0.58
0.00/0.58
0.00/0.63 EOF