Cut unsatisfiable transition [t₁₉∈g₁₈: j→1:g]
Found invariant X₃ ≤ 0 ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ X₀+X₃ ∧ X₁ ≤ X₀ ∧ 0 ≤ X₀ for location termination
Found invariant X₃ ≤ 0 ∧ X₃ ≤ X₁ ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 0 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₀ for location h
Found invariant 1+X₂ ≤ 0 ∧ 1+X₂ ≤ X₁ ∧ 1+X₂ ≤ X₀ ∧ 0 ≤ X₁ ∧ 0 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₀ for location j
Found invariant X₃ ≤ 0 ∧ X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 0 ≤ X₀+X₃ ∧ 0 ≤ X₀ for location g
Found invariant 0 ≤ X₃ ∧ 0 ≤ 2+X₂+X₃ ∧ X₂ ≤ 3+X₃ ∧ 0 ≤ X₁+X₃ ∧ 0 ≤ X₀+X₃ ∧ X₂ ≤ 3 ∧ X₂ ≤ 3+X₁ ∧ X₂ ≤ 3+X₀ ∧ 0 ≤ 2+X₂ ∧ 0 ≤ 2+X₁+X₂ ∧ 0 ≤ 2+X₀+X₂ ∧ 0 ≤ X₁ ∧ 0 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 0 ≤ X₀ for location i
Cut unsatisfiable transition [t₂₃∈g₂₂: termination→1:termination]
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 1 {O(1)}
g₅: 1 {O(1)}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₂₀: inf {Infinity}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 1 {O(1)}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₂₀: inf {Infinity}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: 2⋅X₀ {O(n)}
(g₂,h), X₁: 2⋅X₁+1 {O(n)}
(g₂,h), X₂: 2⋅X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: inf {Infinity}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₂₀: inf {Infinity}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: 12⋅X₀ {O(n)}
(g₅,i), X₁: 12⋅X₁+6 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}
new bound:
6 {O(1)}
MPRF:
• i: [X₂]
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₂₀: inf {Infinity}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: 6⋅X₀ {O(n)}
(g₁₂,i), X₁: 6⋅X₁+3 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 12⋅X₀ {O(n)}
(g₁₄,j), X₁: 12⋅X₁+6 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₂₀: inf {Infinity}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: X₀ {O(n)}
(g₁₂,i), X₁: X₁+1 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 7⋅X₀ {O(n)}
(g₁₄,j), X₁: 7⋅X₁+4 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₁₆,j), X₀: 12⋅X₀ {O(n)}
(g₁₆,j), X₁: 12⋅X₁+6 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: inf {Infinity}
g₀: inf {Infinity}
g₂: inf {Infinity}
g₅: inf {Infinity}
g₁₂: inf {Infinity}
g₁₄: inf {Infinity}
g₁₆: inf {Infinity}
g₂₀: inf {Infinity}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: X₀ {O(n)}
(g₁₂,i), X₁: X₁+1 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 7⋅X₀ {O(n)}
(g₁₄,j), X₁: 7⋅X₁+4 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₁₆,j), X₀: 7⋅X₀ {O(n)}
(g₁₆,j), X₁: 7⋅X₁+4 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}
Overall timebound:inf {Infinity}
g₀: 1 {O(1)}
g₂: 2 {O(1)}
g₅: 6 {O(1)}
g₁₂: 6 {O(1)}
g₁₄: 1 {O(1)}
g₁₆: inf {Infinity}
g₂₀: 1 {O(1)}
Overall costbound: 0 {O(1)}
g₀: 0 {O(1)}
g₂: 0 {O(1)}
g₅: 0 {O(1)}
g₁₂: 0 {O(1)}
g₁₄: 0 {O(1)}
g₁₆: 0 {O(1)}
g₂₀: 0 {O(1)}
(g₀,g), X₀: X₀ {O(n)}
(g₀,g), X₁: X₁ {O(n)}
(g₀,g), X₂: X₂ {O(n)}
(g₀,g), X₃: 0 {O(1)}
(g₂,h), X₀: X₀ {O(n)}
(g₂,h), X₁: X₁+1 {O(n)}
(g₂,h), X₂: X₂ {O(n)}
(g₂,h), X₃: 0 {O(1)}
(g₅,i), X₀: X₀ {O(n)}
(g₅,i), X₁: X₁+1 {O(n)}
(g₅,i), X₂: 9 {O(1)}
(g₅,i), X₃: 0 {O(1)}
(g₁₂,i), X₀: X₀ {O(n)}
(g₁₂,i), X₁: X₁+1 {O(n)}
(g₁₂,i), X₂: 2 {O(1)}
(g₁₂,i), X₃: 84⋅X₁+42 {O(n)}
(g₁₄,j), X₀: 7⋅X₀ {O(n)}
(g₁₄,j), X₁: 7⋅X₁+4 {O(n)}
(g₁₄,j), X₂: 3 {O(1)}
(g₁₄,j), X₃: 84⋅X₁+42 {O(n)}
(g₁₆,j), X₀: 7⋅X₀ {O(n)}
(g₁₆,j), X₁: 7⋅X₁+4 {O(n)}
(g₂₀,termination), X₀: X₀ {O(n)}
(g₂₀,termination), X₁: X₁ {O(n)}
(g₂₀,termination), X₂: X₂ {O(n)}
(g₂₀,termination), X₃: 0 {O(1)}