Cut unsatisfiable transition [t₈∈g₇: lbl52→1:stop; t₁₈∈g₁₇: lbl72→1:lbl72]
Found invariant X₅ ≤ X₀ ∧ X₃ ≤ X₅ ∧ X₀ ≤ X₅ ∧ X₃ ≤ 0 ∧ X₃ ≤ X₀ for location stop
Found invariant X₅ ≤ X₁ ∧ X₅ ≤ X₀ ∧ 1 ≤ X₅ ∧ 1 ≤ X₃+X₅ ∧ 1+X₃ ≤ X₅ ∧ 2 ≤ X₁+X₅ ∧ X₁ ≤ X₅ ∧ 2 ≤ X₀+X₅ ∧ X₀ ≤ X₅ ∧ 1+X₃ ≤ X₁ ∧ 1+X₃ ≤ X₀ ∧ 0 ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 1 ≤ X₀+X₃ ∧ X₁ ≤ X₀ ∧ 1 ≤ X₁ ∧ 2 ≤ X₀+X₁ ∧ X₀ ≤ X₁ ∧ 1 ≤ X₀ for location lbl72
Found invariant X₅ ≤ X₀ ∧ 1 ≤ X₅ ∧ 2 ≤ X₃+X₅ ∧ X₃ ≤ X₅ ∧ 1 ≤ X₁+X₅ ∧ 2 ≤ X₀+X₅ ∧ X₀ ≤ X₅ ∧ X₃ ≤ X₀ ∧ 1 ≤ X₃ ∧ 1 ≤ X₁+X₃ ∧ 2 ≤ X₀+X₃ ∧ 0 ≤ X₁ ∧ 1 ≤ X₀+X₁ ∧ 1 ≤ X₀ for location lbl52
Found invariant X₅ ≤ X₀ ∧ X₀ ≤ X₅ ∧ X₄ ≤ X₃ ∧ X₃ ≤ X₄ ∧ X₂ ≤ X₁ ∧ X₁ ≤ X₂ for location start
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: inf {Infinity}
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₁₉: inf {Infinity}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: inf {Infinity}
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₁₉: inf {Infinity}
(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}
new bound:
2⋅X₀ {O(n)}
MPRF:
• lbl52: [X₃]
• lbl72: [X₃]
new bound:
2⋅X₀+1 {O(n)}
MPRF:
• lbl52: [X₃-1]
• lbl72: [X₃]
Overall timebound:inf {Infinity}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: inf {Infinity}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
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₁₉: inf {Infinity}
(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₉,lbl52), X₀: 2⋅X₀ {O(n)}
(g₉,lbl52), X₁: 4⋅X₀+X₂ {O(n)}
(g₉,lbl52), X₂: 2⋅X₂ {O(n)}
(g₉,lbl52), X₃: 2⋅X₀ {O(n)}
(g₉,lbl52), X₄: 2⋅X₄ {O(n)}
(g₉,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₀: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₁: 3⋅X₀ {O(n)}
(g₁₁,lbl72), X₂: 2⋅X₂ {O(n)}
(g₁₁,lbl72), X₃: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₄: 2⋅X₄ {O(n)}
(g₁₁,lbl72), X₅: 2⋅X₀ {O(n)}
(g₁₃,stop), X₀: 3⋅X₀ {O(n)}
(g₁₃,stop), X₁: 4⋅X₀ {O(n)}
(g₁₃,stop), X₂: 3⋅X₂ {O(n)}
(g₁₃,stop), X₃: 0 {O(1)}
(g₁₃,stop), X₄: 3⋅X₄ {O(n)}
(g₁₃,stop), X₅: 3⋅X₀ {O(n)}
(g₁₅,lbl52), X₀: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₁: 4⋅X₀ {O(n)}
(g₁₅,lbl52), X₂: 2⋅X₂ {O(n)}
(g₁₅,lbl52), X₃: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₄: 2⋅X₄ {O(n)}
(g₁₅,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}
new bound:
24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
PLRF:
• lbl52: 2⋅X₁+2⋅X₅
• lbl72: 2⋅X₀
Overall timebound:24⋅X₀⋅X₀+18⋅X₀+2⋅X₂+6 {O(n^2)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: 24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
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₁₉: inf {Infinity}
(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₉,lbl52), X₀: 2⋅X₀ {O(n)}
(g₉,lbl52), X₁: 4⋅X₀+X₂ {O(n)}
(g₉,lbl52), X₂: 2⋅X₂ {O(n)}
(g₉,lbl52), X₃: 2⋅X₀ {O(n)}
(g₉,lbl52), X₄: 2⋅X₄ {O(n)}
(g₉,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₀: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₁: 3⋅X₀ {O(n)}
(g₁₁,lbl72), X₂: 2⋅X₂ {O(n)}
(g₁₁,lbl72), X₃: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₄: 2⋅X₄ {O(n)}
(g₁₁,lbl72), X₅: 2⋅X₀ {O(n)}
(g₁₃,stop), X₀: 3⋅X₀ {O(n)}
(g₁₃,stop), X₁: 4⋅X₀ {O(n)}
(g₁₃,stop), X₂: 3⋅X₂ {O(n)}
(g₁₃,stop), X₃: 0 {O(1)}
(g₁₃,stop), X₄: 3⋅X₄ {O(n)}
(g₁₃,stop), X₅: 3⋅X₀ {O(n)}
(g₁₅,lbl52), X₀: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₁: 4⋅X₀ {O(n)}
(g₁₅,lbl52), X₂: 2⋅X₂ {O(n)}
(g₁₅,lbl52), X₃: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₄: 2⋅X₄ {O(n)}
(g₁₅,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}
Overall timebound:24⋅X₀⋅X₀+18⋅X₀+2⋅X₂+6 {O(n^2)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: 24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
g₁₉: 1 {O(1)}
Overall costbound: 24⋅X₀⋅X₀+18⋅X₀+2⋅X₂+6 {O(n^2)}
g₁: 1 {O(1)}
g₃: 1 {O(1)}
g₅: 1 {O(1)}
g₉: 24⋅X₀⋅X₀+14⋅X₀+2⋅X₂ {O(n^2)}
g₁₁: 2⋅X₀ {O(n)}
g₁₃: 1 {O(1)}
g₁₅: 2⋅X₀+1 {O(n)}
g₁₉: 1 {O(1)}
(g₁,stop), X₀: X₀ {O(n)}
(g₁,stop), X₁: X₂ {O(n)}
(g₁,stop), X₂: X₂ {O(n)}
(g₁,stop), X₃: X₀ {O(n)}
(g₁,stop), X₄: X₄ {O(n)}
(g₁,stop), X₅: X₀ {O(n)}
(g₃,lbl52), X₀: X₀ {O(n)}
(g₃,lbl52), X₁: X₂ {O(n)}
(g₃,lbl52), X₂: X₂ {O(n)}
(g₃,lbl52), X₃: X₀ {O(n)}
(g₃,lbl52), X₄: X₄ {O(n)}
(g₃,lbl52), X₅: X₀ {O(n)}
(g₅,lbl72), X₀: X₀ {O(n)}
(g₅,lbl72), X₁: X₀ {O(n)}
(g₅,lbl72), X₂: X₂ {O(n)}
(g₅,lbl72), X₃: X₀ {O(n)}
(g₅,lbl72), X₄: X₄ {O(n)}
(g₅,lbl72), X₅: X₀ {O(n)}
(g₉,lbl52), X₀: 2⋅X₀ {O(n)}
(g₉,lbl52), X₁: 4⋅X₀+X₂ {O(n)}
(g₉,lbl52), X₂: 2⋅X₂ {O(n)}
(g₉,lbl52), X₃: 2⋅X₀ {O(n)}
(g₉,lbl52), X₄: 2⋅X₄ {O(n)}
(g₉,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₀: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₁: 3⋅X₀ {O(n)}
(g₁₁,lbl72), X₂: 2⋅X₂ {O(n)}
(g₁₁,lbl72), X₃: 2⋅X₀ {O(n)}
(g₁₁,lbl72), X₄: 2⋅X₄ {O(n)}
(g₁₁,lbl72), X₅: 2⋅X₀ {O(n)}
(g₁₃,stop), X₀: 3⋅X₀ {O(n)}
(g₁₃,stop), X₁: 4⋅X₀ {O(n)}
(g₁₃,stop), X₂: 3⋅X₂ {O(n)}
(g₁₃,stop), X₃: 0 {O(1)}
(g₁₃,stop), X₄: 3⋅X₄ {O(n)}
(g₁₃,stop), X₅: 3⋅X₀ {O(n)}
(g₁₅,lbl52), X₀: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₁: 4⋅X₀ {O(n)}
(g₁₅,lbl52), X₂: 2⋅X₂ {O(n)}
(g₁₅,lbl52), X₃: 2⋅X₀ {O(n)}
(g₁₅,lbl52), X₄: 2⋅X₄ {O(n)}
(g₁₅,lbl52), X₅: 2⋅X₀ {O(n)}
(g₁₉,start), X₀: X₀ {O(n)}
(g₁₉,start), X₁: X₂ {O(n)}
(g₁₉,start), X₂: X₂ {O(n)}
(g₁₉,start), X₃: X₄ {O(n)}
(g₁₉,start), X₄: X₄ {O(n)}
(g₁₉,start), X₅: X₀ {O(n)}