YES(?,PRIMREC) * Step 1: TrivialSCCs MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (?,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 12. evalfbb3in(A,B,C,D,E,F) -> evalfbb4in(A,B,C,D,E,F) [0 >= 3] (?,1) 13. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 14. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [G >= 1] (?,1) 15. evalfbb4in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 16. evalfbb2in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,1 + E,-2 + F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (?,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11,12},11->{17} ,12->{13,14,15},13->{16},14->{16},15->{17},16->{11,12},17->{5,6},18->{2,3},19->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 2: UnsatRules MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (1,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (1,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 12. evalfbb3in(A,B,C,D,E,F) -> evalfbb4in(A,B,C,D,E,F) [0 >= 3] (?,1) 13. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 14. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [G >= 1] (?,1) 15. evalfbb4in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 16. evalfbb2in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,1 + E,-2 + F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (1,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11,12},11->{17} ,12->{13,14,15},13->{16},14->{16},15->{17},16->{11,12},17->{5,6},18->{2,3},19->{}] + Applied Processor: UnsatRules + Details: Following transitions have unsatisfiable constraints and are removed: [12] * Step 3: UnreachableRules MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (1,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (1,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 13. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 14. evalfbb4in(A,B,C,D,E,F) -> evalfbb2in(A,B,C,D,E,F) [G >= 1] (?,1) 15. evalfbb4in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 16. evalfbb2in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,1 + E,-2 + F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (1,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,13->{16},14->{16},15->{17},16->{11},17->{5,6},18->{2,3},19->{}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [13,14,15,16] * Step 4: AddSinks MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (1,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (1,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (1,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,17->{5,6},18->{2,3},19->{}] + Applied Processor: AddSinks + Details: () * Step 5: LooptreeTransformer MAYBE + Considered Problem: Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (?,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (?,1) 20. evalfreturnin(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6) ;(exitus616,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19,20},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,17->{5,6},18->{2,3},19->{},20->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,17,18,19,20] | `- p:[2,18,5,4,17,11,10,7,6,8,9] c: [2] | `- p:[6,17,11,10,7,8] c: [6] * Step 6: SizeAbstraction MAYBE + Considered Problem: (Rules: 0. evalfstart(A,B,C,D,E,F) -> evalfentryin(A,B,C,D,E,F) True (1,1) 1. evalfentryin(A,B,C,D,E,F) -> evalfbb9in(B,B,C,D,E,F) True (?,1) 2. evalfbb9in(A,B,C,D,E,F) -> evalfbbin(A,B,C,D,E,F) [B >= 2] (?,1) 3. evalfbb9in(A,B,C,D,E,F) -> evalfreturnin(A,B,C,D,E,F) [1 >= B] (?,1) 4. evalfbbin(A,B,C,D,E,F) -> evalfbb6in(A,B,-1 + B,-1 + A + B,E,F) True (?,1) 5. evalfbb6in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) [C >= D] (?,1) 6. evalfbb6in(A,B,C,D,E,F) -> evalfbb7in(A,B,C,D,E,F) [D >= 1 + C] (?,1) 7. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [0 >= 1 + G] (?,1) 8. evalfbb7in(A,B,C,D,E,F) -> evalfbb1in(A,B,C,D,E,F) [G >= 1] (?,1) 9. evalfbb7in(A,B,C,D,E,F) -> evalfbb8in(A,B,C,D,E,F) True (?,1) 10. evalfbb1in(A,B,C,D,E,F) -> evalfbb3in(A,B,C,D,C,-1 + D) True (?,1) 11. evalfbb3in(A,B,C,D,E,F) -> evalfbb5in(A,B,C,D,E,F) True (?,1) 17. evalfbb5in(A,B,C,D,E,F) -> evalfbb6in(A,B,E,-1 + F,E,F) True (?,1) 18. evalfbb8in(A,B,C,D,E,F) -> evalfbb9in(1 + -1*C + D,-1 + C,C,D,E,F) True (?,1) 19. evalfreturnin(A,B,C,D,E,F) -> evalfstop(A,B,C,D,E,F) True (?,1) 20. evalfreturnin(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True (?,1) Signature: {(evalfbb1in,6) ;(evalfbb2in,6) ;(evalfbb3in,6) ;(evalfbb4in,6) ;(evalfbb5in,6) ;(evalfbb6in,6) ;(evalfbb7in,6) ;(evalfbb8in,6) ;(evalfbb9in,6) ;(evalfbbin,6) ;(evalfentryin,6) ;(evalfreturnin,6) ;(evalfstart,6) ;(evalfstop,6) ;(exitus616,6)} Flow Graph: [0->{1},1->{2,3},2->{4},3->{19,20},4->{5,6},5->{18},6->{7,8,9},7->{10},8->{10},9->{18},10->{11},11->{17} ,17->{5,6},18->{2,3},19->{},20->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,17,18,19,20] | `- p:[2,18,5,4,17,11,10,7,6,8,9] c: [2] | `- p:[6,17,11,10,7,8] c: [6]) + Applied Processor: SizeAbstraction UseCFG Minimize + Details: () * Step 7: FlowAbstraction MAYBE + Considered Problem: Program: Domain: [A,B,C,D,E,F,0.0,0.0.0] evalfstart ~> evalfentryin [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfentryin ~> evalfbb9in [A <= B, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb9in ~> evalfbbin [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb9in ~> evalfreturnin [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbbin ~> evalfbb6in [A <= A, B <= B, C <= K + B, D <= K + A + B, E <= E, F <= F] evalfbb6in ~> evalfbb8in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb6in ~> evalfbb7in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb7in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb7in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb7in ~> evalfbb8in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb1in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D, E <= C, F <= K + D] evalfbb3in ~> evalfbb5in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb5in ~> evalfbb6in [A <= A, B <= B, C <= E, D <= K + F, E <= E, F <= F] evalfbb8in ~> evalfbb9in [A <= K + C + D, B <= K + C, C <= C, D <= D, E <= E, F <= F] evalfreturnin ~> evalfstop [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfreturnin ~> exitus616 [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] + Loop: [0.0 <= 2*K + B + C + E] evalfbb9in ~> evalfbbin [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb8in ~> evalfbb9in [A <= K + C + D, B <= K + C, C <= C, D <= D, E <= E, F <= F] evalfbb6in ~> evalfbb8in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbbin ~> evalfbb6in [A <= A, B <= B, C <= K + B, D <= K + A + B, E <= E, F <= F] evalfbb5in ~> evalfbb6in [A <= A, B <= B, C <= E, D <= K + F, E <= E, F <= F] evalfbb3in ~> evalfbb5in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb1in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D, E <= C, F <= K + D] evalfbb7in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb6in ~> evalfbb7in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb7in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb7in ~> evalfbb8in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] + Loop: [0.0.0 <= 2*K + C + D + E + F] evalfbb6in ~> evalfbb7in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb5in ~> evalfbb6in [A <= A, B <= B, C <= E, D <= K + F, E <= E, F <= F] evalfbb3in ~> evalfbb5in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb1in ~> evalfbb3in [A <= A, B <= B, C <= C, D <= D, E <= C, F <= K + D] evalfbb7in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] evalfbb7in ~> evalfbb1in [A <= A, B <= B, C <= C, D <= D, E <= E, F <= F] + Applied Processor: FlowAbstraction + Details: () * Step 8: LareProcessor MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,D,E,F,0.0,0.0.0] evalfstart ~> evalfentryin [] evalfentryin ~> evalfbb9in [B ~=> A] evalfbb9in ~> evalfbbin [] evalfbb9in ~> evalfreturnin [] evalfbbin ~> evalfbb6in [A ~+> D,B ~+> C,B ~+> D,K ~+> C,K ~+> D] evalfbb6in ~> evalfbb8in [] evalfbb6in ~> evalfbb7in [] evalfbb7in ~> evalfbb1in [] evalfbb7in ~> evalfbb1in [] evalfbb7in ~> evalfbb8in [] evalfbb1in ~> evalfbb3in [C ~=> E,D ~+> F,K ~+> F] evalfbb3in ~> evalfbb5in [] evalfbb5in ~> evalfbb6in [E ~=> C,F ~+> D,K ~+> D] evalfbb8in ~> evalfbb9in [C ~+> A,C ~+> B,D ~+> A,K ~+> A,K ~+> B] evalfreturnin ~> evalfstop [] evalfreturnin ~> exitus616 [] + Loop: [B ~+> 0.0,C ~+> 0.0,E ~+> 0.0,K ~*> 0.0] evalfbb9in ~> evalfbbin [] evalfbb8in ~> evalfbb9in [C ~+> A,C ~+> B,D ~+> A,K ~+> A,K ~+> B] evalfbb6in ~> evalfbb8in [] evalfbbin ~> evalfbb6in [A ~+> D,B ~+> C,B ~+> D,K ~+> C,K ~+> D] evalfbb5in ~> evalfbb6in [E ~=> C,F ~+> D,K ~+> D] evalfbb3in ~> evalfbb5in [] evalfbb1in ~> evalfbb3in [C ~=> E,D ~+> F,K ~+> F] evalfbb7in ~> evalfbb1in [] evalfbb6in ~> evalfbb7in [] evalfbb7in ~> evalfbb1in [] evalfbb7in ~> evalfbb8in [] + Loop: [C ~+> 0.0.0,D ~+> 0.0.0,E ~+> 0.0.0,F ~+> 0.0.0,K ~*> 0.0.0] evalfbb6in ~> evalfbb7in [] evalfbb5in ~> evalfbb6in [E ~=> C,F ~+> D,K ~+> D] evalfbb3in ~> evalfbb5in [] evalfbb1in ~> evalfbb3in [C ~=> E,D ~+> F,K ~+> F] evalfbb7in ~> evalfbb1in [] evalfbb7in ~> evalfbb1in [] + Applied Processor: LareProcessor + Details: evalfstart ~> exitus616 [B ~=> A ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> E ,B ~+> F ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,F ~+> 0.0.0 ,F ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> E ,K ~+> F ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> F ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> D ,C ~*> F ,C ~*> 0.0.0 ,C ~*> tick ,E ~*> A ,E ~*> B ,E ~*> D ,E ~*> F ,E ~*> 0.0.0 ,E ~*> tick ,F ~*> A ,F ~*> D ,F ~*> F ,F ~*> 0.0.0 ,F ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> E ,K ~*> F ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> F ,B ~^> 0.0.0 ,B ~^> tick ,C ~^> A ,C ~^> D ,C ~^> F ,C ~^> 0.0.0 ,C ~^> tick ,E ~^> A ,E ~^> D ,E ~^> F ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> A ,K ~^> D ,K ~^> F ,K ~^> 0.0.0 ,K ~^> tick] evalfstart ~> evalfstop [B ~=> A ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> E ,B ~+> F ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,F ~+> 0.0.0 ,F ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> E ,K ~+> F ,K ~+> 0.0.0 ,K ~+> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> F ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> D ,C ~*> F ,C ~*> 0.0.0 ,C ~*> tick ,E ~*> A ,E ~*> B ,E ~*> D ,E ~*> F ,E ~*> 0.0.0 ,E ~*> tick ,F ~*> A ,F ~*> D ,F ~*> F ,F ~*> 0.0.0 ,F ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> E ,K ~*> F ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> F ,B ~^> 0.0.0 ,B ~^> tick ,C ~^> A ,C ~^> D ,C ~^> F ,C ~^> 0.0.0 ,C ~^> tick ,E ~^> A ,E ~^> D ,E ~^> F ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> A ,K ~^> D ,K ~^> F ,K ~^> 0.0.0 ,K ~^> tick] + evalfbb9in> [A ~+> A ,A ~+> D ,A ~+> F ,A ~+> 0.0.0 ,A ~+> tick ,B ~+> A ,B ~+> B ,B ~+> C ,B ~+> D ,B ~+> E ,B ~+> F ,B ~+> 0.0 ,B ~+> 0.0.0 ,B ~+> tick ,C ~+> 0.0 ,C ~+> tick ,E ~+> 0.0 ,E ~+> 0.0.0 ,E ~+> tick ,F ~+> 0.0.0 ,F ~+> tick ,tick ~+> tick ,K ~+> A ,K ~+> B ,K ~+> C ,K ~+> D ,K ~+> E ,K ~+> F ,K ~+> 0.0.0 ,K ~+> tick ,A ~*> A ,A ~*> D ,A ~*> F ,A ~*> 0.0.0 ,A ~*> tick ,B ~*> A ,B ~*> B ,B ~*> D ,B ~*> F ,B ~*> 0.0.0 ,B ~*> tick ,C ~*> A ,C ~*> B ,C ~*> D ,C ~*> F ,C ~*> 0.0.0 ,C ~*> tick ,E ~*> A ,E ~*> B ,E ~*> D ,E ~*> F ,E ~*> 0.0.0 ,E ~*> tick ,F ~*> A ,F ~*> D ,F ~*> F ,F ~*> 0.0.0 ,F ~*> tick ,K ~*> A ,K ~*> B ,K ~*> C ,K ~*> D ,K ~*> E ,K ~*> F ,K ~*> 0.0 ,K ~*> 0.0.0 ,K ~*> tick ,B ~^> A ,B ~^> D ,B ~^> F ,B ~^> 0.0.0 ,B ~^> tick ,C ~^> A ,C ~^> D ,C ~^> F ,C ~^> 0.0.0 ,C ~^> tick ,E ~^> A ,E ~^> D ,E ~^> F ,E ~^> 0.0.0 ,E ~^> tick ,K ~^> A ,K ~^> D ,K ~^> F ,K ~^> 0.0.0 ,K ~^> tick] + evalfbb7in> [C ~=> E ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> F ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> 0.0.0 ,E ~+> tick ,F ~+> 0.0.0 ,F ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> F ,C ~*> D ,D ~*> D ,E ~*> D ,F ~*> D ,K ~*> D ,K ~*> F ,K ~*> 0.0.0 ,K ~*> tick] evalfbb6in> [C ~=> E ,C ~+> 0.0.0 ,C ~+> tick ,D ~+> D ,D ~+> F ,D ~+> 0.0.0 ,D ~+> tick ,E ~+> 0.0.0 ,E ~+> tick ,F ~+> 0.0.0 ,F ~+> tick ,tick ~+> tick ,K ~+> D ,K ~+> F ,C ~*> D ,C ~*> F ,D ~*> D ,D ~*> F ,E ~*> D ,E ~*> F ,F ~*> D ,F ~*> F ,K ~*> D ,K ~*> F ,K ~*> 0.0.0 ,K ~*> tick] YES(?,PRIMREC)