MAYBE 182.93/123.89 MAYBE 183.04/123.92 183.04/123.92 183.04/123.92 183.04/123.92 183.04/123.92 183.04/123.92 Runtime Complexity (innermost) proof of /export/starexec/sandbox/benchmark/theBenchmark.xml.xml 183.04/123.92 183.04/123.92 183.04/123.92
183.04/123.92
183.04/123.92
183.04/123.92
The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), INFINITE).

0 CpxTRS
183.04/123.92 
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳2 CdtProblem
183.04/123.92 
↳3 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳4 CdtProblem
183.04/123.92 
↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳6 CdtProblem
183.04/123.92 
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳8 CdtProblem
183.04/123.92 
↳9 CdtRewritingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳10 CdtProblem
183.04/123.92 
↳11 CdtRewritingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳12 CdtProblem
183.04/123.92 
↳13 CdtRewritingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳14 CdtProblem
183.04/123.92 
↳15 CdtRewritingProof (BOTH BOUNDS(ID, ID))
183.04/123.92 
↳16 CdtProblem
183.04/123.92
183.04/123.92 183.04/123.92
183.04/123.92
183.04/123.92

(0) Obligation:

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

g(f(x, y)) → f(f(g(g(x)), g(g(y))), f(g(g(x)), g(g(y))))

Rewrite Strategy: INNERMOST
183.04/123.92
183.04/123.92

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

Converted CpxTRS to CDT
183.04/123.92
183.04/123.92

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(z0, z1)) → c(G(g(z0)), G(z0), G(g(z1)), G(z1), G(g(z0)), G(z0), G(g(z1)), G(z1))
S tuples:

G(f(z0, z1)) → c(G(g(z0)), G(z0), G(g(z1)), G(z1), G(g(z0)), G(z0), G(g(z1)), G(z1))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c

183.04/123.92
183.04/123.92

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

Use narrowing to replace G(f(z0, z1)) → c(G(g(z0)), G(z0), G(g(z1)), G(z1), G(g(z0)), G(z0), G(g(z1)), G(z1)) by

G(f(f(z0, z1), x1)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(x1)), G(x1), G(g(f(z0, z1))), G(f(z0, z1)), G(g(x1)), G(x1)) 183.04/123.92
G(f(x0, x1)) → c(G(g(x1)), G(x1), G(g(x1)), G(x1))
183.04/123.92
183.04/123.92

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(f(z0, z1), x1)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(x1)), G(x1), G(g(f(z0, z1))), G(f(z0, z1)), G(g(x1)), G(x1)) 183.04/123.92
G(f(x0, x1)) → c(G(g(x1)), G(x1), G(g(x1)), G(x1))
S tuples:

G(f(f(z0, z1), x1)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(x1)), G(x1), G(g(f(z0, z1))), G(f(z0, z1)), G(g(x1)), G(x1)) 183.04/123.92
G(f(x0, x1)) → c(G(g(x1)), G(x1), G(g(x1)), G(x1))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92

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

Use narrowing to replace G(f(f(z0, z1), x1)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(x1)), G(x1), G(g(f(z0, z1))), G(f(z0, z1)), G(g(x1)), G(x1)) by

G(f(f(x0, x1), f(z0, z1))) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(x0, x1))), G(f(x0, x1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1)))
183.04/123.92
183.04/123.92

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(x0, x1)) → c(G(g(x1)), G(x1), G(g(x1)), G(x1)) 183.04/123.92
G(f(f(x0, x1), f(z0, z1))) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(x0, x1))), G(f(x0, x1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1)))
S tuples:

G(f(x0, x1)) → c(G(g(x1)), G(x1), G(g(x1)), G(x1)) 183.04/123.92
G(f(f(x0, x1), f(z0, z1))) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(x0, x1))), G(f(x0, x1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1)))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92

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

Use narrowing to replace G(f(x0, x1)) → c(G(g(x1)), G(x1), G(g(x1)), G(x1)) by

G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1)))
183.04/123.92
183.04/123.92

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(f(x0, x1), f(z0, z1))) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(x0, x1))), G(f(x0, x1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1))) 183.04/123.92
G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1)))
S tuples:

G(f(f(x0, x1), f(z0, z1))) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(x0, x1))), G(f(x0, x1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1))) 183.04/123.92
G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1)))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92

(9) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace G(f(f(x0, x1), f(z0, z1))) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(x0, x1))), G(f(x0, x1)), G(g(f(z0, z1))), G(f(z0, z1))) by G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)))
183.04/123.92
183.04/123.92

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1))) 183.04/123.92
G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)))
S tuples:

G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1))) 183.04/123.92
G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92

(11) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace G(f(f(x0, x1), x2)) → c(G(f(f(g(g(x0)), g(g(x1))), f(g(g(x0)), g(g(x1))))), G(f(x0, x1)), G(g(f(x0, x1))), G(f(x0, x1))) by G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)))
183.04/123.92
183.04/123.92

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3))) 183.04/123.92
G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)))
S tuples:

G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1))) 183.04/123.92
G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3))) 183.04/123.92
G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92

(13) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace G(f(x0, f(z0, z1))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(g(f(z0, z1))), G(f(z0, z1))) by G(f(z0, f(z1, z2))) → c(G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)), G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)))
183.04/123.92
183.04/123.92

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3))) 183.04/123.92
G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1))) 183.04/123.92
G(f(z0, f(z1, z2))) → c(G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)), G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)))
S tuples:

G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3))) 183.04/123.92
G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1))) 183.04/123.92
G(f(z0, f(z1, z2))) → c(G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)), G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92

(15) CdtRewritingProof (BOTH BOUNDS(ID, ID) transformation)

Used rewriting to replace G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(g(f(z0, z1))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3))) by G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)))
183.04/123.92
183.04/123.92

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

g(f(z0, z1)) → f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))
Tuples:

G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1))) 183.04/123.92
G(f(z0, f(z1, z2))) → c(G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)), G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2))) 183.04/123.92
G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)))
S tuples:

G(f(f(z0, z1), z2)) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1))) 183.04/123.92
G(f(z0, f(z1, z2))) → c(G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2)), G(f(f(g(g(z1)), g(g(z2))), f(g(g(z1)), g(g(z2))))), G(f(z1, z2))) 183.04/123.92
G(f(f(z0, z1), f(z2, z3))) → c(G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)), G(f(f(g(g(z0)), g(g(z1))), f(g(g(z0)), g(g(z1))))), G(f(z0, z1)), G(f(f(g(g(z2)), g(g(z3))), f(g(g(z2)), g(g(z3))))), G(f(z2, z3)))
K tuples:none
Defined Rule Symbols:

g

Defined Pair Symbols:

G

Compound Symbols:

c, c

183.04/123.92
183.04/123.92
183.04/123.99 EOF