YES(?,POLY) * Step 1: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) 1. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 2. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 3. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 4. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 5. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 7. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 8. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 9. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 10. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 11. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{0,1,2,3,4,5,6,7},1->{0,1,2,3,4,5,6,7},2->{0,1,2,3,4,5,6,7},3->{0,1,2,3,4,5,6,7},4->{0,1,2,3,4,5,6,7} ,5->{0,1,2,3,4,5,6,7},6->{0,1,2,3,4,5,6,7},7->{0,1,2,3,4,5,6,7},8->{0,1,2,3,4,5,6,7},9->{0,1,2,3,4,5,6,7} ,10->{0,1,2,3,4,5,6,7},11->{0,1,2,3,4,5,6,7}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(0,1) ,(0,2) ,(0,3) ,(0,4) ,(0,5) ,(0,6) ,(0,7) ,(1,0) ,(1,2) ,(1,3) ,(1,4) ,(1,5) ,(1,6) ,(2,0) ,(2,1) ,(2,3) ,(2,4) ,(2,5) ,(2,6) ,(2,7) ,(3,1) ,(3,2) ,(3,4) ,(3,5) ,(3,6) ,(3,7) ,(4,0) ,(4,1) ,(4,3) ,(4,5) ,(4,6) ,(4,7) ,(5,0) ,(5,1) ,(5,2) ,(5,3) ,(5,4) ,(5,6) ,(5,7) ,(6,0) ,(6,1) ,(6,2) ,(6,3) ,(6,4) ,(6,7) ,(7,0) ,(7,1) ,(7,2) ,(7,3) ,(7,4) ,(7,5) ,(7,6) ,(8,0) ,(8,1) ,(8,3) ,(8,5) ,(8,6) ,(8,7) ,(9,1) ,(9,2) ,(9,4) ,(9,5) ,(9,6) ,(9,7) ,(10,0) ,(10,1) ,(10,2) ,(10,3) ,(10,4) ,(10,7) ,(11,0) ,(11,2) ,(11,3) ,(11,4) ,(11,5) ,(11,6)] * Step 2: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] (?,1) 1. f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] (?,1) 2. f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 3. f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] (?,1) 4. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] (?,1) 5. f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] (?,1) 6. f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] (?,1) 7. f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] (?,1) 8. f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] (1,1) 9. f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] (1,1) 10. f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] (1,1) 11. f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] (1,1) Signature: {(f0,2);(f2,2)} Flow Graph: [0->{0},1->{1,7},2->{2},3->{0,3},4->{2,4},5->{5},6->{5,6},7->{7},8->{2,4},9->{0,3},10->{5,6},11->{1,7}] + Applied Processor: FromIts + Details: () * Step 3: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] f2(A,B) -> f2(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2(A,B) -> f2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2(A,B) -> f2(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2(A,B) -> f2(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2(A,B) -> f2(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f0(A,B) -> f2(A,B) [0 >= 1 + A && 0 >= 1 + B] f0(A,B) -> f2(A,B) [0 >= 1 + A && B >= 1] f0(A,B) -> f2(A,B) [A >= 1 && 0 >= 1 + B] f0(A,B) -> f2(A,B) [A >= 1 && B >= 1] Signature: {(f0,2);(f2,2)} Rule Graph: [0->{0},1->{1,7},2->{2},3->{0,3},4->{2,4},5->{5},6->{5,6},7->{7},8->{2,4},9->{0,3},10->{5,6},11->{1,7}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f2.0(A,B) -> f2.0(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] f2.1(A,B) -> f2.1(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.1(A,B) -> f2.7(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.2(A,B) -> f2.2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2.3(A,B) -> f2.0(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.3(A,B) -> f2.3(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.4(A,B) -> f2.2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.4(A,B) -> f2.4(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.5(A,B) -> f2.5(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2.6(A,B) -> f2.5(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.6(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.7(A,B) -> f2.7(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f0.8(A,B) -> f2.2(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.8(A,B) -> f2.4(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.9(A,B) -> f2.0(A,B) [0 >= 1 + A && B >= 1] f0.9(A,B) -> f2.3(A,B) [0 >= 1 + A && B >= 1] f0.10(A,B) -> f2.5(A,B) [A >= 1 && 0 >= 1 + B] f0.10(A,B) -> f2.6(A,B) [A >= 1 && 0 >= 1 + B] f0.11(A,B) -> f2.1(A,B) [A >= 1 && B >= 1] f0.11(A,B) -> f2.7(A,B) [A >= 1 && B >= 1] Signature: {(f0.10,2) ;(f0.11,2) ;(f0.8,2) ;(f0.9,2) ;(f2.0,2) ;(f2.1,2) ;(f2.2,2) ;(f2.3,2) ;(f2.4,2) ;(f2.5,2) ;(f2.6,2) ;(f2.7,2)} Rule Graph: [0->{0},1->{1,2},2->{11},3->{3},4->{0},5->{4,5},6->{3},7->{6,7},8->{8},9->{8},10->{9,10},11->{11},12->{3} ,13->{6,7},14->{0},15->{4,5},16->{8},17->{9,10},18->{1,2},19->{11}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f2.0(A,B) -> f2.0(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] f2.1(A,B) -> f2.1(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.1(A,B) -> f2.7(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.2(A,B) -> f2.2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2.3(A,B) -> f2.0(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.3(A,B) -> f2.3(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.4(A,B) -> f2.2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.4(A,B) -> f2.4(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.5(A,B) -> f2.5(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2.6(A,B) -> f2.5(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.6(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.7(A,B) -> f2.7(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f0.8(A,B) -> f2.2(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.8(A,B) -> f2.4(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.9(A,B) -> f2.0(A,B) [0 >= 1 + A && B >= 1] f0.9(A,B) -> f2.3(A,B) [0 >= 1 + A && B >= 1] f0.10(A,B) -> f2.5(A,B) [A >= 1 && 0 >= 1 + B] f0.10(A,B) -> f2.6(A,B) [A >= 1 && 0 >= 1 + B] f0.11(A,B) -> f2.1(A,B) [A >= 1 && B >= 1] f0.11(A,B) -> f2.7(A,B) [A >= 1 && B >= 1] f2.7(A,B) -> exitus616(A,B) True f2.7(A,B) -> exitus616(A,B) True f2.5(A,B) -> exitus616(A,B) True f2.5(A,B) -> exitus616(A,B) True f2.0(A,B) -> exitus616(A,B) True f2.0(A,B) -> exitus616(A,B) True f2.2(A,B) -> exitus616(A,B) True f2.2(A,B) -> exitus616(A,B) True Signature: {(exitus616,2) ;(f0.10,2) ;(f0.11,2) ;(f0.8,2) ;(f0.9,2) ;(f2.0,2) ;(f2.1,2) ;(f2.2,2) ;(f2.3,2) ;(f2.4,2) ;(f2.5,2) ;(f2.6,2) ;(f2.7,2)} Rule Graph: [0->{0,24,25},1->{1,2},2->{11},3->{3,26,27},4->{0},5->{4,5},6->{3},7->{6,7},8->{8,22,23},9->{8},10->{9,10} ,11->{11,20,21},12->{3},13->{6,7},14->{0},15->{4,5},16->{8},17->{9,10},18->{1,2},19->{11}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27] | +- p:[10] c: [10] | +- p:[8] c: [8] | +- p:[7] c: [7] | +- p:[5] c: [5] | +- p:[3] c: [3] | +- p:[1] c: [1] | +- p:[11] c: [11] | `- p:[0] c: [0] * Step 6: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f2.0(A,B) -> f2.0(1 + A,B) [A + B >= 0 && B >= 1 + A && 0 >= 2 + A && B >= 1] f2.1(A,B) -> f2.1(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.1(A,B) -> f2.7(1 + A,B) [A + B >= 0 && B >= 1 + A && A >= 0 && B >= 1] f2.2(A,B) -> f2.2(A,1 + B) [B >= A && 0 >= 2 + B && 0 >= 1 + A && 0 >= 1 + A + B] f2.3(A,B) -> f2.0(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.3(A,B) -> f2.3(A,1 + B) [B >= A && B >= 0 && 0 >= 1 + A && 0 >= 1 + A + B] f2.4(A,B) -> f2.2(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.4(A,B) -> f2.4(-1 + A,B) [1 >= A + B && A >= 1 + B && 0 >= A && 0 >= 1 + B] f2.5(A,B) -> f2.5(-1 + A,B) [1 >= A + B && A >= 1 + B && A >= 2 && 0 >= 1 + B] f2.6(A,B) -> f2.5(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.6(A,B) -> f2.6(A,-1 + B) [A >= B && 0 >= B && A >= 1 && A + B >= 2] f2.7(A,B) -> f2.7(A,-1 + B) [A >= B && B >= 2 && A >= 1 && A + B >= 2] f0.8(A,B) -> f2.2(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.8(A,B) -> f2.4(A,B) [0 >= 1 + A && 0 >= 1 + B] f0.9(A,B) -> f2.0(A,B) [0 >= 1 + A && B >= 1] f0.9(A,B) -> f2.3(A,B) [0 >= 1 + A && B >= 1] f0.10(A,B) -> f2.5(A,B) [A >= 1 && 0 >= 1 + B] f0.10(A,B) -> f2.6(A,B) [A >= 1 && 0 >= 1 + B] f0.11(A,B) -> f2.1(A,B) [A >= 1 && B >= 1] f0.11(A,B) -> f2.7(A,B) [A >= 1 && B >= 1] f2.7(A,B) -> exitus616(A,B) True f2.7(A,B) -> exitus616(A,B) True f2.5(A,B) -> exitus616(A,B) True f2.5(A,B) -> exitus616(A,B) True f2.0(A,B) -> exitus616(A,B) True f2.0(A,B) -> exitus616(A,B) True f2.2(A,B) -> exitus616(A,B) True f2.2(A,B) -> exitus616(A,B) True Signature: {(exitus616,2) ;(f0.10,2) ;(f0.11,2) ;(f0.8,2) ;(f0.9,2) ;(f2.0,2) ;(f2.1,2) ;(f2.2,2) ;(f2.3,2) ;(f2.4,2) ;(f2.5,2) ;(f2.6,2) ;(f2.7,2)} Rule Graph: [0->{0,24,25},1->{1,2},2->{11},3->{3,26,27},4->{0},5->{4,5},6->{3},7->{6,7},8->{8,22,23},9->{8},10->{9,10} ,11->{11,20,21},12->{3},13->{6,7},14->{0},15->{4,5},16->{8},17->{9,10},18->{1,2},19->{11}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27] | +- p:[10] c: [10] | +- p:[8] c: [8] | +- p:[7] c: [7] | +- p:[5] c: [5] | +- p:[3] c: [3] | +- p:[1] c: [1] | +- p:[11] c: [11] | `- p:[0] c: [0]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f2.0 ~> f2.0 [A <= B, B <= B] f2.1 ~> f2.1 [A <= B, B <= B] f2.1 ~> f2.7 [A <= B, B <= B] f2.2 ~> f2.2 [A <= A, B <= B] f2.3 ~> f2.0 [A <= A, B <= A] f2.3 ~> f2.3 [A <= A, B <= A] f2.4 ~> f2.2 [A <= B, B <= B] f2.4 ~> f2.4 [A <= B, B <= B] f2.5 ~> f2.5 [A <= B, B <= B] f2.6 ~> f2.5 [A <= A, B <= A] f2.6 ~> f2.6 [A <= A, B <= A] f2.7 ~> f2.7 [A <= A, B <= B] f0.8 ~> f2.2 [A <= A, B <= B] f0.8 ~> f2.4 [A <= A, B <= B] f0.9 ~> f2.0 [A <= A, B <= B] f0.9 ~> f2.3 [A <= A, B <= B] f0.10 ~> f2.5 [A <= A, B <= B] f0.10 ~> f2.6 [A <= A, B <= B] f0.11 ~> f2.1 [A <= A, B <= B] f0.11 ~> f2.7 [A <= A, B <= B] f2.7 ~> exitus616 [A <= A, B <= B] f2.7 ~> exitus616 [A <= A, B <= B] f2.5 ~> exitus616 [A <= A, B <= B] f2.5 ~> exitus616 [A <= A, B <= B] f2.0 ~> exitus616 [A <= A, B <= B] f2.0 ~> exitus616 [A <= A, B <= B] f2.2 ~> exitus616 [A <= A, B <= B] f2.2 ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= 2*K + A + B] f2.6 ~> f2.6 [A <= A, B <= A] + Loop: [0.1 <= 2*K + A] f2.5 ~> f2.5 [A <= B, B <= B] + Loop: [0.2 <= K + A + B] f2.4 ~> f2.4 [A <= B, B <= B] + Loop: [0.3 <= K + A + B] f2.3 ~> f2.3 [A <= A, B <= A] + Loop: [0.4 <= K + A + B] f2.2 ~> f2.2 [A <= A, B <= B] + Loop: [0.5 <= K + A + B] f2.1 ~> f2.1 [A <= B, B <= B] + Loop: [0.6 <= 2*K + A + B] f2.7 ~> f2.7 [A <= A, B <= B] + Loop: [0.7 <= 2*K + A] f2.0 ~> f2.0 [A <= B, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 8: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.1,0.2,0.3,0.4,0.5,0.6,0.7] f2.0 ~> f2.0 [B ~=> A] f2.1 ~> f2.1 [B ~=> A] f2.1 ~> f2.7 [B ~=> A] f2.2 ~> f2.2 [] f2.3 ~> f2.0 [A ~=> B] f2.3 ~> f2.3 [A ~=> B] f2.4 ~> f2.2 [B ~=> A] f2.4 ~> f2.4 [B ~=> A] f2.5 ~> f2.5 [B ~=> A] f2.6 ~> f2.5 [A ~=> B] f2.6 ~> f2.6 [A ~=> B] f2.7 ~> f2.7 [] f0.8 ~> f2.2 [] f0.8 ~> f2.4 [] f0.9 ~> f2.0 [] f0.9 ~> f2.3 [] f0.10 ~> f2.5 [] f0.10 ~> f2.6 [] f0.11 ~> f2.1 [] f0.11 ~> f2.7 [] f2.7 ~> exitus616 [] f2.7 ~> exitus616 [] f2.5 ~> exitus616 [] f2.5 ~> exitus616 [] f2.0 ~> exitus616 [] f2.0 ~> exitus616 [] f2.2 ~> exitus616 [] f2.2 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] f2.6 ~> f2.6 [A ~=> B] + Loop: [A ~+> 0.1,K ~*> 0.1] f2.5 ~> f2.5 [B ~=> A] + Loop: [A ~+> 0.2,B ~+> 0.2,K ~+> 0.2] f2.4 ~> f2.4 [B ~=> A] + Loop: [A ~+> 0.3,B ~+> 0.3,K ~+> 0.3] f2.3 ~> f2.3 [A ~=> B] + Loop: [A ~+> 0.4,B ~+> 0.4,K ~+> 0.4] f2.2 ~> f2.2 [] + Loop: [A ~+> 0.5,B ~+> 0.5,K ~+> 0.5] f2.1 ~> f2.1 [B ~=> A] + Loop: [A ~+> 0.6,B ~+> 0.6,K ~*> 0.6] f2.7 ~> f2.7 [] + Loop: [A ~+> 0.7,K ~*> 0.7] f2.0 ~> f2.0 [B ~=> A] + Applied Processor: Lare + Details: f0.10 ~> exitus616 [A ~=> B ,B ~=> A ,A ~+> 0.0 ,A ~+> 0.1 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,A ~*> tick ,K ~*> 0.0 ,K ~*> 0.1 ,K ~*> tick] f0.9 ~> exitus616 [A ~=> B ,B ~=> A ,A ~+> 0.3 ,A ~+> 0.7 ,A ~+> tick ,B ~+> 0.3 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.3 ,K ~+> tick ,A ~*> tick ,K ~*> 0.7 ,K ~*> tick] f0.11 ~> exitus616 [B ~=> A ,A ~+> 0.5 ,A ~+> 0.6 ,A ~+> tick ,B ~+> 0.5 ,B ~+> 0.6 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.5 ,K ~+> tick ,B ~*> 0.6 ,B ~*> tick ,K ~*> 0.6 ,K ~*> tick] f0.8 ~> exitus616 [B ~=> A ,A ~+> 0.2 ,A ~+> 0.4 ,A ~+> tick ,B ~+> 0.2 ,B ~+> 0.4 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.2 ,K ~+> 0.4 ,K ~+> tick ,B ~*> 0.4 ,B ~*> tick ,K ~*> tick] + f2.6> [A ~=> B,A ~+> 0.0,A ~+> tick,B ~+> 0.0,B ~+> tick,tick ~+> tick,K ~*> 0.0,K ~*> tick] + f2.5> [B ~=> A,A ~+> 0.1,A ~+> tick,tick ~+> tick,K ~*> 0.1,K ~*> tick] + f2.4> [B ~=> A,A ~+> 0.2,A ~+> tick,B ~+> 0.2,B ~+> tick,tick ~+> tick,K ~+> 0.2,K ~+> tick] + f2.3> [A ~=> B,A ~+> 0.3,A ~+> tick,B ~+> 0.3,B ~+> tick,tick ~+> tick,K ~+> 0.3,K ~+> tick] + f2.2> [A ~+> 0.4,A ~+> tick,B ~+> 0.4,B ~+> tick,tick ~+> tick,K ~+> 0.4,K ~+> tick] + f2.1> [B ~=> A,A ~+> 0.5,A ~+> tick,B ~+> 0.5,B ~+> tick,tick ~+> tick,K ~+> 0.5,K ~+> tick] + f2.7> [A ~+> 0.6,A ~+> tick,B ~+> 0.6,B ~+> tick,tick ~+> tick,K ~*> 0.6,K ~*> tick] + f2.0> [B ~=> A,A ~+> 0.7,A ~+> tick,tick ~+> tick,K ~*> 0.7,K ~*> tick] YES(?,POLY)