YES(?,POLY) * Step 1: UnsatRules WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f2(A,B,C,D) -> f300(A,B,C,D) True (1,1) 1. f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] (?,1) 2. f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] (?,1) 3. f300(A,B,C,D) -> f300(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] (?,1) 4. f300(A,B,C,D) -> f1(A,B,C,E) [A >= 1 && 0 >= A + B && B >= 1] (?,1) 5. f300(A,B,C,D) -> f1(A,B,C,E) [B >= 1 && 0 >= A] (?,1) 6. f300(A,B,C,D) -> f1(A,B,C,E) [0 >= B] (?,1) Signature: {(f1,4);(f2,4);(f300,4)} Flow Graph: [0->{1,2,3,4,5,6},1->{1,2,3,4,5,6},2->{1,2,3,4,5,6},3->{1,2,3,4,5,6},4->{},5->{},6->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [4] * Step 2: UnsatPaths WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f2(A,B,C,D) -> f300(A,B,C,D) True (1,1) 1. f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] (?,1) 2. f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] (?,1) 3. f300(A,B,C,D) -> f300(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] (?,1) 5. f300(A,B,C,D) -> f1(A,B,C,E) [B >= 1 && 0 >= A] (?,1) 6. f300(A,B,C,D) -> f1(A,B,C,E) [0 >= B] (?,1) Signature: {(f1,4);(f2,4);(f300,4)} Flow Graph: [0->{1,2,3,5,6},1->{1,2,3,5,6},2->{1,2,3,5,6},3->{1,2,3,5,6},5->{},6->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,5),(2,5),(3,5)] * Step 3: FromIts WORST_CASE(?,POLY) + Considered Problem: Rules: 0. f2(A,B,C,D) -> f300(A,B,C,D) True (1,1) 1. f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] (?,1) 2. f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] (?,1) 3. f300(A,B,C,D) -> f300(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] (?,1) 5. f300(A,B,C,D) -> f1(A,B,C,E) [B >= 1 && 0 >= A] (?,1) 6. f300(A,B,C,D) -> f1(A,B,C,E) [0 >= B] (?,1) Signature: {(f1,4);(f2,4);(f300,4)} Flow Graph: [0->{1,2,3,5,6},1->{1,2,3,6},2->{1,2,3,6},3->{1,2,3,6},5->{},6->{}] + Applied Processor: FromIts + Details: () * Step 4: Unfold WORST_CASE(?,POLY) + Considered Problem: Rules: f2(A,B,C,D) -> f300(A,B,C,D) True f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300(A,B,C,D) -> f300(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300(A,B,C,D) -> f300(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300(A,B,C,D) -> f1(A,B,C,E) [B >= 1 && 0 >= A] f300(A,B,C,D) -> f1(A,B,C,E) [0 >= B] Signature: {(f1,4);(f2,4);(f300,4)} Rule Graph: [0->{1,2,3,5,6},1->{1,2,3,6},2->{1,2,3,6},3->{1,2,3,6},5->{},6->{}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks WORST_CASE(?,POLY) + Considered Problem: Rules: f2.0(A,B,C,D) -> f300.1(A,B,C,D) True f2.0(A,B,C,D) -> f300.2(A,B,C,D) True f2.0(A,B,C,D) -> f300.3(A,B,C,D) True f2.0(A,B,C,D) -> f300.5(A,B,C,D) True f2.0(A,B,C,D) -> f300.6(A,B,C,D) True f300.1(A,B,C,D) -> f300.1(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.2(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.3(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.6(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.2(A,B,C,D) -> f300.1(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.2(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.3(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.6(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.3(A,B,C,D) -> f300.1(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.2(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.3(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.6(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.5(A,B,C,D) -> f1.7(A,B,C,E) [B >= 1 && 0 >= A] f300.6(A,B,C,D) -> f1.7(A,B,C,E) [0 >= B] Signature: {(f1.7,4);(f2.0,4);(f300.1,4);(f300.2,4);(f300.3,4);(f300.5,4);(f300.6,4)} Rule Graph: [0->{5,6,7,8},1->{9,10,11,12},2->{13,14,15,16},3->{17},4->{18},5->{5,6,7,8},6->{9,10,11,12},7->{13,14,15 ,16},8->{18},9->{5,6,7,8},10->{9,10,11,12},11->{13,14,15,16},12->{18},13->{5,6,7,8},14->{9,10,11,12},15->{13 ,14,15,16},16->{18},17->{},18->{}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose WORST_CASE(?,POLY) + Considered Problem: Rules: f2.0(A,B,C,D) -> f300.1(A,B,C,D) True f2.0(A,B,C,D) -> f300.2(A,B,C,D) True f2.0(A,B,C,D) -> f300.3(A,B,C,D) True f2.0(A,B,C,D) -> f300.5(A,B,C,D) True f2.0(A,B,C,D) -> f300.6(A,B,C,D) True f300.1(A,B,C,D) -> f300.1(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.2(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.3(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.6(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.2(A,B,C,D) -> f300.1(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.2(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.3(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.6(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.3(A,B,C,D) -> f300.1(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.2(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.3(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.6(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.5(A,B,C,D) -> f1.7(A,B,C,E) [B >= 1 && 0 >= A] f300.6(A,B,C,D) -> f1.7(A,B,C,E) [0 >= B] f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(exitus616,4);(f1.7,4);(f2.0,4);(f300.1,4);(f300.2,4);(f300.3,4);(f300.5,4);(f300.6,4)} Rule Graph: [0->{5,6,7,8},1->{9,10,11,12},2->{13,14,15,16},3->{17},4->{18},5->{5,6,7,8},6->{9,10,11,12},7->{13,14,15 ,16},8->{18},9->{5,6,7,8},10->{9,10,11,12},11->{13,14,15,16},12->{18},13->{5,6,7,8},14->{9,10,11,12},15->{13 ,14,15,16},16->{18},17->{20},18->{19,21,22,23,24,25,26,27,28,29}] + 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,28,29] | `- p:[5,9,6,13,7,11,10,14,15] c: [5,6,7,9,10,11,13,14,15] * Step 7: AbstractSize WORST_CASE(?,POLY) + Considered Problem: (Rules: f2.0(A,B,C,D) -> f300.1(A,B,C,D) True f2.0(A,B,C,D) -> f300.2(A,B,C,D) True f2.0(A,B,C,D) -> f300.3(A,B,C,D) True f2.0(A,B,C,D) -> f300.5(A,B,C,D) True f2.0(A,B,C,D) -> f300.6(A,B,C,D) True f300.1(A,B,C,D) -> f300.1(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.2(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.3(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.1(A,B,C,D) -> f300.6(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && E >= 1 && A + B >= 1] f300.2(A,B,C,D) -> f300.1(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.2(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.3(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.2(A,B,C,D) -> f300.6(-1 + B,-1 + B,E,D) [A >= 1 && B >= 1 && 0 >= 1 + E && A + B >= 1] f300.3(A,B,C,D) -> f300.1(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.2(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.3(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.3(A,B,C,D) -> f300.6(-1 + A,-2 + A,0,D) [A >= 1 && A + B >= 1 && B >= 1] f300.5(A,B,C,D) -> f1.7(A,B,C,E) [B >= 1 && 0 >= A] f300.6(A,B,C,D) -> f1.7(A,B,C,E) [0 >= B] f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True f1.7(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(exitus616,4);(f1.7,4);(f2.0,4);(f300.1,4);(f300.2,4);(f300.3,4);(f300.5,4);(f300.6,4)} Rule Graph: [0->{5,6,7,8},1->{9,10,11,12},2->{13,14,15,16},3->{17},4->{18},5->{5,6,7,8},6->{9,10,11,12},7->{13,14,15 ,16},8->{18},9->{5,6,7,8},10->{9,10,11,12},11->{13,14,15,16},12->{18},13->{5,6,7,8},14->{9,10,11,12},15->{13 ,14,15,16},16->{18},17->{20},18->{19,21,22,23,24,25,26,27,28,29}] ,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,28,29] | `- p:[5,9,6,13,7,11,10,14,15] c: [5,6,7,9,10,11,13,14,15]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [A,B,C,D,0.0] f2.0 ~> f300.1 [A <= A, B <= B, C <= C, D <= D] f2.0 ~> f300.2 [A <= A, B <= B, C <= C, D <= D] f2.0 ~> f300.3 [A <= A, B <= B, C <= C, D <= D] f2.0 ~> f300.5 [A <= A, B <= B, C <= C, D <= D] f2.0 ~> f300.6 [A <= A, B <= B, C <= C, D <= D] f300.1 ~> f300.1 [A <= B, B <= B, C <= unknown, D <= D] f300.1 ~> f300.2 [A <= B, B <= B, C <= unknown, D <= D] f300.1 ~> f300.3 [A <= B, B <= B, C <= unknown, D <= D] f300.1 ~> f300.6 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.1 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.2 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.3 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.6 [A <= B, B <= B, C <= unknown, D <= D] f300.3 ~> f300.1 [A <= A, B <= A, C <= 0*K, D <= D] f300.3 ~> f300.2 [A <= A, B <= A, C <= 0*K, D <= D] f300.3 ~> f300.3 [A <= A, B <= A, C <= 0*K, D <= D] f300.3 ~> f300.6 [A <= A, B <= A, C <= 0*K, D <= D] f300.5 ~> f1.7 [A <= A, B <= B, C <= C, D <= unknown] f300.6 ~> f1.7 [A <= A, B <= B, C <= C, D <= unknown] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] f1.7 ~> exitus616 [A <= A, B <= B, C <= C, D <= D] + Loop: [0.0 <= K + A + B] f300.1 ~> f300.1 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.1 [A <= B, B <= B, C <= unknown, D <= D] f300.1 ~> f300.2 [A <= B, B <= B, C <= unknown, D <= D] f300.3 ~> f300.1 [A <= A, B <= A, C <= 0*K, D <= D] f300.1 ~> f300.3 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.3 [A <= B, B <= B, C <= unknown, D <= D] f300.2 ~> f300.2 [A <= B, B <= B, C <= unknown, D <= D] f300.3 ~> f300.2 [A <= A, B <= A, C <= 0*K, D <= D] f300.3 ~> f300.3 [A <= A, B <= A, C <= 0*K, D <= D] + Applied Processor: AbstractFlow + Details: () * Step 9: Lare WORST_CASE(?,POLY) + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,0.0] f2.0 ~> f300.1 [] f2.0 ~> f300.2 [] f2.0 ~> f300.3 [] f2.0 ~> f300.5 [] f2.0 ~> f300.6 [] f300.1 ~> f300.1 [B ~=> A,huge ~=> C] f300.1 ~> f300.2 [B ~=> A,huge ~=> C] f300.1 ~> f300.3 [B ~=> A,huge ~=> C] f300.1 ~> f300.6 [B ~=> A,huge ~=> C] f300.2 ~> f300.1 [B ~=> A,huge ~=> C] f300.2 ~> f300.2 [B ~=> A,huge ~=> C] f300.2 ~> f300.3 [B ~=> A,huge ~=> C] f300.2 ~> f300.6 [B ~=> A,huge ~=> C] f300.3 ~> f300.1 [A ~=> B,K ~=> C] f300.3 ~> f300.2 [A ~=> B,K ~=> C] f300.3 ~> f300.3 [A ~=> B,K ~=> C] f300.3 ~> f300.6 [A ~=> B,K ~=> C] f300.5 ~> f1.7 [huge ~=> D] f300.6 ~> f1.7 [huge ~=> D] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] f1.7 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f300.1 ~> f300.1 [B ~=> A,huge ~=> C] f300.2 ~> f300.1 [B ~=> A,huge ~=> C] f300.1 ~> f300.2 [B ~=> A,huge ~=> C] f300.3 ~> f300.1 [A ~=> B,K ~=> C] f300.1 ~> f300.3 [B ~=> A,huge ~=> C] f300.2 ~> f300.3 [B ~=> A,huge ~=> C] f300.2 ~> f300.2 [B ~=> A,huge ~=> C] f300.3 ~> f300.2 [A ~=> B,K ~=> C] f300.3 ~> f300.3 [A ~=> B,K ~=> C] + Applied Processor: Lare + Details: f2.0 ~> exitus616 [A ~=> B ,B ~=> A ,K ~=> C ,huge ~=> C ,huge ~=> D ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick ,A ~*> 0.0 ,A ~*> tick ,B ~*> 0.0 ,B ~*> tick ,K ~*> tick] + f300.1> [B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.3> [B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.2> [B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.1> [A ~=> B ,B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.3> [A ~=> B ,B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.2> [A ~=> B ,B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.1> [B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.3> [B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] f300.2> [B ~=> A ,K ~=> C ,huge ~=> C ,A ~+> 0.0 ,A ~+> tick ,B ~+> 0.0 ,B ~+> tick ,tick ~+> tick ,K ~+> 0.0 ,K ~+> tick] YES(?,POLY)