MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(1,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A = 1] (1,1) 1. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= A] (1,1) 2. f2(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,1,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= 2] (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f20(A,B,1 + B,S,T,1,G,H,I,J,K,L,M,N,O,P,Q,R) [A >= B] (?,1) 4. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f20(A,B,C,S,T,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 5. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,E,1 + F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f45(A,B,C,D,E,1 + F,S,T,U,J,K,L,M,N,O,P,Q,R) [B >= F] (?,1) 7. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1 + F,G,H,I,J,-1 + K,S,T,U,V,K,Q,R) [J >= F] (?,1) 8. f60(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f13(A,1 + B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + J] (?,1) 9. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f60(A,B,C,D,E,1,G,H,I,S,B,L,M,N,O,P,T,U) [F >= 1 + B] (?,1) 10. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,A,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && A = C] (?,1) 11. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f45(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [A >= 1 + C && F >= 1 + B] (?,1) 12. f31(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f45(A,B,C,D,E,1,S,T,U,J,K,L,M,N,O,P,Q,R) [C >= 1 + A && F >= 1 + B] (?,1) 13. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,E,1,G,H,I,J,K,L,M,N,O,P,Q,R) [E >= 1 && F >= 1 + B] (?,1) 15. f20(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f31(A,B,C,D,0,1,G,H,I,J,K,L,M,N,O,P,Q,R) [F >= 1 + B && E = 0] (?,1) 16. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) -> f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R) [B >= 1 + A] (?,1) Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: ArgumentFilter [3,6,7,8,10,11,12,13,14,15,16,17] + Details: We remove following argument positions: [3,6,7,8,10,11,12,13,14,15,16,17]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f2(A,B,C,E,F,J) -> f1(1,B,C,E,F,J) [A = 1] (1,1) 1. f2(A,B,C,E,F,J) -> f13(A,1,C,E,F,J) [0 >= A] (1,1) 2. f2(A,B,C,E,F,J) -> f13(A,1,C,E,F,J) [A >= 2] (1,1) 3. f13(A,B,C,E,F,J) -> f20(A,B,1 + B,T,1,J) [A >= B] (?,1) 4. f20(A,B,C,E,F,J) -> f20(A,B,C,T,1 + F,J) [B >= F] (?,1) 5. f31(A,B,C,E,F,J) -> f31(A,B,C,E,1 + F,J) [B >= F] (?,1) 6. f45(A,B,C,E,F,J) -> f45(A,B,C,E,1 + F,J) [B >= F] (?,1) 7. f60(A,B,C,E,F,J) -> f60(A,B,C,E,1 + F,J) [J >= F] (?,1) 8. f60(A,B,C,E,F,J) -> f13(A,1 + B,C,E,F,J) [F >= 1 + J] (?,1) 9. f45(A,B,C,E,F,J) -> f60(A,B,C,E,1,S) [F >= 1 + B] (?,1) 10. f31(A,B,C,E,F,J) -> f1(A,B,A,E,F,J) [F >= 1 + B && A = C] (?,1) 11. f31(A,B,C,E,F,J) -> f45(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] (?,1) 12. f31(A,B,C,E,F,J) -> f45(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] (?,1) 13. f20(A,B,C,E,F,J) -> f31(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f20(A,B,C,E,F,J) -> f31(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] (?,1) 15. f20(A,B,C,E,F,J) -> f31(A,B,C,0,1,J) [F >= 1 + B && E = 0] (?,1) 16. f13(A,B,C,E,F,J) -> f1(A,B,C,E,F,J) [B >= 1 + A] (?,1) Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Flow Graph: [0->{},1->{3,16},2->{3,16},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16} ,9->{7,8},10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,3),(2,16)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f2(A,B,C,E,F,J) -> f1(1,B,C,E,F,J) [A = 1] (1,1) 1. f2(A,B,C,E,F,J) -> f13(A,1,C,E,F,J) [0 >= A] (1,1) 2. f2(A,B,C,E,F,J) -> f13(A,1,C,E,F,J) [A >= 2] (1,1) 3. f13(A,B,C,E,F,J) -> f20(A,B,1 + B,T,1,J) [A >= B] (?,1) 4. f20(A,B,C,E,F,J) -> f20(A,B,C,T,1 + F,J) [B >= F] (?,1) 5. f31(A,B,C,E,F,J) -> f31(A,B,C,E,1 + F,J) [B >= F] (?,1) 6. f45(A,B,C,E,F,J) -> f45(A,B,C,E,1 + F,J) [B >= F] (?,1) 7. f60(A,B,C,E,F,J) -> f60(A,B,C,E,1 + F,J) [J >= F] (?,1) 8. f60(A,B,C,E,F,J) -> f13(A,1 + B,C,E,F,J) [F >= 1 + J] (?,1) 9. f45(A,B,C,E,F,J) -> f60(A,B,C,E,1,S) [F >= 1 + B] (?,1) 10. f31(A,B,C,E,F,J) -> f1(A,B,A,E,F,J) [F >= 1 + B && A = C] (?,1) 11. f31(A,B,C,E,F,J) -> f45(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] (?,1) 12. f31(A,B,C,E,F,J) -> f45(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] (?,1) 13. f20(A,B,C,E,F,J) -> f31(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] (?,1) 14. f20(A,B,C,E,F,J) -> f31(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] (?,1) 15. f20(A,B,C,E,F,J) -> f31(A,B,C,0,1,J) [F >= 1 + B && E = 0] (?,1) 16. f13(A,B,C,E,F,J) -> f1(A,B,C,E,F,J) [B >= 1 + A] (?,1) Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Flow Graph: [0->{},1->{16},2->{3},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16},9->{7,8} ,10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: FromIts + Details: () * Step 4: Unfold MAYBE + Considered Problem: Rules: f2(A,B,C,E,F,J) -> f1(1,B,C,E,F,J) [A = 1] f2(A,B,C,E,F,J) -> f13(A,1,C,E,F,J) [0 >= A] f2(A,B,C,E,F,J) -> f13(A,1,C,E,F,J) [A >= 2] f13(A,B,C,E,F,J) -> f20(A,B,1 + B,T,1,J) [A >= B] f20(A,B,C,E,F,J) -> f20(A,B,C,T,1 + F,J) [B >= F] f31(A,B,C,E,F,J) -> f31(A,B,C,E,1 + F,J) [B >= F] f45(A,B,C,E,F,J) -> f45(A,B,C,E,1 + F,J) [B >= F] f60(A,B,C,E,F,J) -> f60(A,B,C,E,1 + F,J) [J >= F] f60(A,B,C,E,F,J) -> f13(A,1 + B,C,E,F,J) [F >= 1 + J] f45(A,B,C,E,F,J) -> f60(A,B,C,E,1,S) [F >= 1 + B] f31(A,B,C,E,F,J) -> f1(A,B,A,E,F,J) [F >= 1 + B && A = C] f31(A,B,C,E,F,J) -> f45(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31(A,B,C,E,F,J) -> f45(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f20(A,B,C,E,F,J) -> f31(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20(A,B,C,E,F,J) -> f31(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20(A,B,C,E,F,J) -> f31(A,B,C,0,1,J) [F >= 1 + B && E = 0] f13(A,B,C,E,F,J) -> f1(A,B,C,E,F,J) [B >= 1 + A] Signature: {(f1,18);(f13,18);(f2,18);(f20,18);(f31,18);(f45,18);(f60,18)} Rule Graph: [0->{},1->{16},2->{3},3->{4,13,14,15},4->{4,13,14,15},5->{5,10,11,12},6->{6,9},7->{7,8},8->{3,16},9->{7,8} ,10->{},11->{6,9},12->{6,9},13->{5,10,11,12},14->{5,10,11,12},15->{5,10,11,12},16->{}] + Applied Processor: Unfold + Details: () * Step 5: AddSinks MAYBE + Considered Problem: Rules: f2.0(A,B,C,E,F,J) -> f1.17(1,B,C,E,F,J) [A = 1] f2.1(A,B,C,E,F,J) -> f13.16(A,1,C,E,F,J) [0 >= A] f2.2(A,B,C,E,F,J) -> f13.3(A,1,C,E,F,J) [A >= 2] f13.3(A,B,C,E,F,J) -> f20.4(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.13(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.14(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.15(A,B,1 + B,T,1,J) [A >= B] f20.4(A,B,C,E,F,J) -> f20.4(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.13(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.14(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.15(A,B,C,T,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.5(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.10(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.11(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.12(A,B,C,E,1 + F,J) [B >= F] f45.6(A,B,C,E,F,J) -> f45.6(A,B,C,E,1 + F,J) [B >= F] f45.6(A,B,C,E,F,J) -> f45.9(A,B,C,E,1 + F,J) [B >= F] f60.7(A,B,C,E,F,J) -> f60.7(A,B,C,E,1 + F,J) [J >= F] f60.7(A,B,C,E,F,J) -> f60.8(A,B,C,E,1 + F,J) [J >= F] f60.8(A,B,C,E,F,J) -> f13.3(A,1 + B,C,E,F,J) [F >= 1 + J] f60.8(A,B,C,E,F,J) -> f13.16(A,1 + B,C,E,F,J) [F >= 1 + J] f45.9(A,B,C,E,F,J) -> f60.7(A,B,C,E,1,S) [F >= 1 + B] f45.9(A,B,C,E,F,J) -> f60.8(A,B,C,E,1,S) [F >= 1 + B] f31.10(A,B,C,E,F,J) -> f1.17(A,B,A,E,F,J) [F >= 1 + B && A = C] f31.11(A,B,C,E,F,J) -> f45.6(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31.11(A,B,C,E,F,J) -> f45.9(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31.12(A,B,C,E,F,J) -> f45.6(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f31.12(A,B,C,E,F,J) -> f45.9(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.5(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.10(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.11(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.12(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.5(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.10(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.11(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.12(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.15(A,B,C,E,F,J) -> f31.5(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.10(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.11(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.12(A,B,C,0,1,J) [F >= 1 + B && E = 0] f13.16(A,B,C,E,F,J) -> f1.17(A,B,C,E,F,J) [B >= 1 + A] Signature: {(f1.17,6) ;(f13.16,6) ;(f13.3,6) ;(f2.0,6) ;(f2.1,6) ;(f2.2,6) ;(f20.13,6) ;(f20.14,6) ;(f20.15,6) ;(f20.4,6) ;(f31.10,6) ;(f31.11,6) ;(f31.12,6) ;(f31.5,6) ;(f45.6,6) ;(f45.9,6) ;(f60.7,6) ;(f60.8,6)} Rule Graph: [0->{},1->{40},2->{3,4,5,6},3->{7,8,9,10},4->{28,29,30,31},5->{32,33,34,35},6->{36,37,38,39},7->{7,8,9,10} ,8->{28,29,30,31},9->{32,33,34,35},10->{36,37,38,39},11->{11,12,13,14},12->{23},13->{24,25},14->{26,27} ,15->{15,16},16->{21,22},17->{17,18},18->{19,20},19->{3,4,5,6},20->{40},21->{17,18},22->{19,20},23->{} ,24->{15,16},25->{21,22},26->{15,16},27->{21,22},28->{11,12,13,14},29->{23},30->{24,25},31->{26,27},32->{11 ,12,13,14},33->{23},34->{24,25},35->{26,27},36->{11,12,13,14},37->{23},38->{24,25},39->{26,27},40->{}] + Applied Processor: AddSinks + Details: () * Step 6: Decompose MAYBE + Considered Problem: Rules: f2.0(A,B,C,E,F,J) -> f1.17(1,B,C,E,F,J) [A = 1] f2.1(A,B,C,E,F,J) -> f13.16(A,1,C,E,F,J) [0 >= A] f2.2(A,B,C,E,F,J) -> f13.3(A,1,C,E,F,J) [A >= 2] f13.3(A,B,C,E,F,J) -> f20.4(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.13(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.14(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.15(A,B,1 + B,T,1,J) [A >= B] f20.4(A,B,C,E,F,J) -> f20.4(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.13(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.14(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.15(A,B,C,T,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.5(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.10(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.11(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.12(A,B,C,E,1 + F,J) [B >= F] f45.6(A,B,C,E,F,J) -> f45.6(A,B,C,E,1 + F,J) [B >= F] f45.6(A,B,C,E,F,J) -> f45.9(A,B,C,E,1 + F,J) [B >= F] f60.7(A,B,C,E,F,J) -> f60.7(A,B,C,E,1 + F,J) [J >= F] f60.7(A,B,C,E,F,J) -> f60.8(A,B,C,E,1 + F,J) [J >= F] f60.8(A,B,C,E,F,J) -> f13.3(A,1 + B,C,E,F,J) [F >= 1 + J] f60.8(A,B,C,E,F,J) -> f13.16(A,1 + B,C,E,F,J) [F >= 1 + J] f45.9(A,B,C,E,F,J) -> f60.7(A,B,C,E,1,S) [F >= 1 + B] f45.9(A,B,C,E,F,J) -> f60.8(A,B,C,E,1,S) [F >= 1 + B] f31.10(A,B,C,E,F,J) -> f1.17(A,B,A,E,F,J) [F >= 1 + B && A = C] f31.11(A,B,C,E,F,J) -> f45.6(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31.11(A,B,C,E,F,J) -> f45.9(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31.12(A,B,C,E,F,J) -> f45.6(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f31.12(A,B,C,E,F,J) -> f45.9(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.5(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.10(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.11(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.12(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.5(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.10(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.11(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.12(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.15(A,B,C,E,F,J) -> f31.5(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.10(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.11(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.12(A,B,C,0,1,J) [F >= 1 + B && E = 0] f13.16(A,B,C,E,F,J) -> f1.17(A,B,C,E,F,J) [B >= 1 + A] f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True Signature: {(exitus616,6) ;(f1.17,6) ;(f13.16,6) ;(f13.3,6) ;(f2.0,6) ;(f2.1,6) ;(f2.2,6) ;(f20.13,6) ;(f20.14,6) ;(f20.15,6) ;(f20.4,6) ;(f31.10,6) ;(f31.11,6) ;(f31.12,6) ;(f31.5,6) ;(f45.6,6) ;(f45.9,6) ;(f60.7,6) ;(f60.8,6)} Rule Graph: [0->{47},1->{40},2->{3,4,5,6},3->{7,8,9,10},4->{28,29,30,31},5->{32,33,34,35},6->{36,37,38,39},7->{7,8,9 ,10},8->{28,29,30,31},9->{32,33,34,35},10->{36,37,38,39},11->{11,12,13,14},12->{23},13->{24,25},14->{26,27} ,15->{15,16},16->{21,22},17->{17,18},18->{19,20},19->{3,4,5,6},20->{40},21->{17,18},22->{19,20},23->{41,42 ,44,45},24->{15,16},25->{21,22},26->{15,16},27->{21,22},28->{11,12,13,14},29->{23},30->{24,25},31->{26,27} ,32->{11,12,13,14},33->{23},34->{24,25},35->{26,27},36->{11,12,13,14},37->{23},38->{24,25},39->{26,27} ,40->{43,46}] + 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,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47] | `- p:[3,19,18,17,21,16,15,24,13,11,28,4,8,7,32,5,9,36,6,10,30,34,38,26,14,31,35,39,25,27,22] c: [3,4,5,6,18,19,22] | +- p:[7] c: [7] | +- p:[11] c: [11] | +- p:[15] c: [15] | `- p:[17] c: [17] * Step 7: AbstractSize MAYBE + Considered Problem: (Rules: f2.0(A,B,C,E,F,J) -> f1.17(1,B,C,E,F,J) [A = 1] f2.1(A,B,C,E,F,J) -> f13.16(A,1,C,E,F,J) [0 >= A] f2.2(A,B,C,E,F,J) -> f13.3(A,1,C,E,F,J) [A >= 2] f13.3(A,B,C,E,F,J) -> f20.4(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.13(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.14(A,B,1 + B,T,1,J) [A >= B] f13.3(A,B,C,E,F,J) -> f20.15(A,B,1 + B,T,1,J) [A >= B] f20.4(A,B,C,E,F,J) -> f20.4(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.13(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.14(A,B,C,T,1 + F,J) [B >= F] f20.4(A,B,C,E,F,J) -> f20.15(A,B,C,T,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.5(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.10(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.11(A,B,C,E,1 + F,J) [B >= F] f31.5(A,B,C,E,F,J) -> f31.12(A,B,C,E,1 + F,J) [B >= F] f45.6(A,B,C,E,F,J) -> f45.6(A,B,C,E,1 + F,J) [B >= F] f45.6(A,B,C,E,F,J) -> f45.9(A,B,C,E,1 + F,J) [B >= F] f60.7(A,B,C,E,F,J) -> f60.7(A,B,C,E,1 + F,J) [J >= F] f60.7(A,B,C,E,F,J) -> f60.8(A,B,C,E,1 + F,J) [J >= F] f60.8(A,B,C,E,F,J) -> f13.3(A,1 + B,C,E,F,J) [F >= 1 + J] f60.8(A,B,C,E,F,J) -> f13.16(A,1 + B,C,E,F,J) [F >= 1 + J] f45.9(A,B,C,E,F,J) -> f60.7(A,B,C,E,1,S) [F >= 1 + B] f45.9(A,B,C,E,F,J) -> f60.8(A,B,C,E,1,S) [F >= 1 + B] f31.10(A,B,C,E,F,J) -> f1.17(A,B,A,E,F,J) [F >= 1 + B && A = C] f31.11(A,B,C,E,F,J) -> f45.6(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31.11(A,B,C,E,F,J) -> f45.9(A,B,C,E,1,J) [A >= 1 + C && F >= 1 + B] f31.12(A,B,C,E,F,J) -> f45.6(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f31.12(A,B,C,E,F,J) -> f45.9(A,B,C,E,1,J) [C >= 1 + A && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.5(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.10(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.11(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.13(A,B,C,E,F,J) -> f31.12(A,B,C,E,1,J) [0 >= 1 + E && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.5(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.10(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.11(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.14(A,B,C,E,F,J) -> f31.12(A,B,C,E,1,J) [E >= 1 && F >= 1 + B] f20.15(A,B,C,E,F,J) -> f31.5(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.10(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.11(A,B,C,0,1,J) [F >= 1 + B && E = 0] f20.15(A,B,C,E,F,J) -> f31.12(A,B,C,0,1,J) [F >= 1 + B && E = 0] f13.16(A,B,C,E,F,J) -> f1.17(A,B,C,E,F,J) [B >= 1 + A] f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True f1.17(A,B,C,E,F,J) -> exitus616(A,B,C,E,F,J) True Signature: {(exitus616,6) ;(f1.17,6) ;(f13.16,6) ;(f13.3,6) ;(f2.0,6) ;(f2.1,6) ;(f2.2,6) ;(f20.13,6) ;(f20.14,6) ;(f20.15,6) ;(f20.4,6) ;(f31.10,6) ;(f31.11,6) ;(f31.12,6) ;(f31.5,6) ;(f45.6,6) ;(f45.9,6) ;(f60.7,6) ;(f60.8,6)} Rule Graph: [0->{47},1->{40},2->{3,4,5,6},3->{7,8,9,10},4->{28,29,30,31},5->{32,33,34,35},6->{36,37,38,39},7->{7,8,9 ,10},8->{28,29,30,31},9->{32,33,34,35},10->{36,37,38,39},11->{11,12,13,14},12->{23},13->{24,25},14->{26,27} ,15->{15,16},16->{21,22},17->{17,18},18->{19,20},19->{3,4,5,6},20->{40},21->{17,18},22->{19,20},23->{41,42 ,44,45},24->{15,16},25->{21,22},26->{15,16},27->{21,22},28->{11,12,13,14},29->{23},30->{24,25},31->{26,27} ,32->{11,12,13,14},33->{23},34->{24,25},35->{26,27},36->{11,12,13,14},37->{23},38->{24,25},39->{26,27} ,40->{43,46}] ,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,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44,45,46,47] | `- p:[3,19,18,17,21,16,15,24,13,11,28,4,8,7,32,5,9,36,6,10,30,34,38,26,14,31,35,39,25,27,22] c: [3,4,5,6,18,19,22] | +- p:[7] c: [7] | +- p:[11] c: [11] | +- p:[15] c: [15] | `- p:[17] c: [17]) + Applied Processor: AbstractSize Minimize + Details: () * Step 8: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,C,E,F,J,0.0,0.0.0,0.0.1,0.0.2,0.0.3] f2.0 ~> f1.17 [A <= K, B <= B, C <= C, E <= E, F <= F, J <= J] f2.1 ~> f13.16 [A <= A, B <= K, C <= C, E <= E, F <= F, J <= J] f2.2 ~> f13.3 [A <= A, B <= K, C <= C, E <= E, F <= F, J <= J] f13.3 ~> f20.4 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f13.3 ~> f20.13 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f13.3 ~> f20.14 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f13.3 ~> f20.15 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f20.4 ~> f20.4 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.4 ~> f20.13 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.4 ~> f20.14 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.4 ~> f20.15 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f31.5 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f31.5 ~> f31.10 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f31.5 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f31.5 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f45.6 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f45.6 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f60.7 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f60.7 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f60.8 ~> f13.3 [A <= A, B <= K + B, C <= C, E <= E, F <= F, J <= J] f60.8 ~> f13.16 [A <= A, B <= K + B, C <= C, E <= E, F <= F, J <= J] f45.9 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown] f45.9 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown] f31.10 ~> f1.17 [A <= A, B <= B, C <= A, E <= E, F <= F, J <= J] f31.11 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f31.11 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f31.12 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f31.12 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.13 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.13 ~> f31.10 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.13 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.13 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.14 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.14 ~> f31.10 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.14 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.14 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.15 ~> f31.5 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f20.15 ~> f31.10 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f20.15 ~> f31.11 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f20.15 ~> f31.12 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f13.16 ~> f1.17 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] f1.17 ~> exitus616 [A <= A, B <= B, C <= C, E <= E, F <= F, J <= J] + Loop: [0.0 <= K + A + B] f13.3 ~> f20.4 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f60.8 ~> f13.3 [A <= A, B <= K + B, C <= C, E <= E, F <= F, J <= J] f60.7 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f60.7 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f45.9 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown] f45.6 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f45.6 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f31.11 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f31.5 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f31.5 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f20.13 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f13.3 ~> f20.13 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f20.4 ~> f20.13 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.4 ~> f20.4 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.14 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f13.3 ~> f20.14 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f20.4 ~> f20.14 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.15 ~> f31.5 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f13.3 ~> f20.15 [A <= A, B <= B, C <= K + B, E <= unknown, F <= K, J <= J] f20.4 ~> f20.15 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] f20.13 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.14 ~> f31.11 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.15 ~> f31.11 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f31.12 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f31.5 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] f20.13 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.14 ~> f31.12 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f20.15 ~> f31.12 [A <= A, B <= B, C <= C, E <= 0*K, F <= K, J <= J] f31.11 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f31.12 ~> f45.9 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= J] f45.9 ~> f60.8 [A <= A, B <= B, C <= C, E <= E, F <= K, J <= unknown] + Loop: [0.0.0 <= B + F] f20.4 ~> f20.4 [A <= A, B <= B, C <= C, E <= unknown, F <= K + F, J <= J] + Loop: [0.0.1 <= B + F] f31.5 ~> f31.5 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] + Loop: [0.0.2 <= B + F] f45.6 ~> f45.6 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] + Loop: [0.0.3 <= F + J] f60.7 ~> f60.7 [A <= A, B <= B, C <= C, E <= E, F <= K + F, J <= J] + Applied Processor: AbstractFlow + Details: () * Step 9: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,C,E,F,J,0.0,0.0.0,0.0.1,0.0.2,0.0.3] f2.0 ~> f1.17 [K ~=> A] f2.1 ~> f13.16 [K ~=> B] f2.2 ~> f13.3 [K ~=> B] f13.3 ~> f20.4 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f13.3 ~> f20.13 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f13.3 ~> f20.14 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f13.3 ~> f20.15 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f20.4 ~> f20.4 [huge ~=> E,F ~+> F,K ~+> F] f20.4 ~> f20.13 [huge ~=> E,F ~+> F,K ~+> F] f20.4 ~> f20.14 [huge ~=> E,F ~+> F,K ~+> F] f20.4 ~> f20.15 [huge ~=> E,F ~+> F,K ~+> F] f31.5 ~> f31.5 [F ~+> F,K ~+> F] f31.5 ~> f31.10 [F ~+> F,K ~+> F] f31.5 ~> f31.11 [F ~+> F,K ~+> F] f31.5 ~> f31.12 [F ~+> F,K ~+> F] f45.6 ~> f45.6 [F ~+> F,K ~+> F] f45.6 ~> f45.9 [F ~+> F,K ~+> F] f60.7 ~> f60.7 [F ~+> F,K ~+> F] f60.7 ~> f60.8 [F ~+> F,K ~+> F] f60.8 ~> f13.3 [B ~+> B,K ~+> B] f60.8 ~> f13.16 [B ~+> B,K ~+> B] f45.9 ~> f60.7 [K ~=> F,huge ~=> J] f45.9 ~> f60.8 [K ~=> F,huge ~=> J] f31.10 ~> f1.17 [A ~=> C] f31.11 ~> f45.6 [K ~=> F] f31.11 ~> f45.9 [K ~=> F] f31.12 ~> f45.6 [K ~=> F] f31.12 ~> f45.9 [K ~=> F] f20.13 ~> f31.5 [K ~=> F] f20.13 ~> f31.10 [K ~=> F] f20.13 ~> f31.11 [K ~=> F] f20.13 ~> f31.12 [K ~=> F] f20.14 ~> f31.5 [K ~=> F] f20.14 ~> f31.10 [K ~=> F] f20.14 ~> f31.11 [K ~=> F] f20.14 ~> f31.12 [K ~=> F] f20.15 ~> f31.5 [K ~=> E,K ~=> F] f20.15 ~> f31.10 [K ~=> E,K ~=> F] f20.15 ~> f31.11 [K ~=> E,K ~=> F] f20.15 ~> f31.12 [K ~=> E,K ~=> F] f13.16 ~> f1.17 [] f1.17 ~> exitus616 [] f1.17 ~> exitus616 [] f1.17 ~> exitus616 [] f1.17 ~> exitus616 [] f1.17 ~> exitus616 [] f1.17 ~> exitus616 [] f1.17 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~+> 0.0] f13.3 ~> f20.4 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f60.8 ~> f13.3 [B ~+> B,K ~+> B] f60.7 ~> f60.8 [F ~+> F,K ~+> F] f60.7 ~> f60.7 [F ~+> F,K ~+> F] f45.9 ~> f60.7 [K ~=> F,huge ~=> J] f45.6 ~> f45.9 [F ~+> F,K ~+> F] f45.6 ~> f45.6 [F ~+> F,K ~+> F] f31.11 ~> f45.6 [K ~=> F] f31.5 ~> f31.11 [F ~+> F,K ~+> F] f31.5 ~> f31.5 [F ~+> F,K ~+> F] f20.13 ~> f31.5 [K ~=> F] f13.3 ~> f20.13 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f20.4 ~> f20.13 [huge ~=> E,F ~+> F,K ~+> F] f20.4 ~> f20.4 [huge ~=> E,F ~+> F,K ~+> F] f20.14 ~> f31.5 [K ~=> F] f13.3 ~> f20.14 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f20.4 ~> f20.14 [huge ~=> E,F ~+> F,K ~+> F] f20.15 ~> f31.5 [K ~=> E,K ~=> F] f13.3 ~> f20.15 [K ~=> F,huge ~=> E,B ~+> C,K ~+> C] f20.4 ~> f20.15 [huge ~=> E,F ~+> F,K ~+> F] f20.13 ~> f31.11 [K ~=> F] f20.14 ~> f31.11 [K ~=> F] f20.15 ~> f31.11 [K ~=> E,K ~=> F] f31.12 ~> f45.6 [K ~=> F] f31.5 ~> f31.12 [F ~+> F,K ~+> F] f20.13 ~> f31.12 [K ~=> F] f20.14 ~> f31.12 [K ~=> F] f20.15 ~> f31.12 [K ~=> E,K ~=> F] f31.11 ~> f45.9 [K ~=> F] f31.12 ~> f45.9 [K ~=> F] f45.9 ~> f60.8 [K ~=> F,huge ~=> J] + Loop: [B ~+> 0.0.0,F ~+> 0.0.0] f20.4 ~> f20.4 [huge ~=> E,F ~+> F,K ~+> F] + Loop: [B ~+> 0.0.1,F ~+> 0.0.1] f31.5 ~> f31.5 [F ~+> F,K ~+> F] + Loop: [B ~+> 0.0.2,F ~+> 0.0.2] f45.6 ~> f45.6 [F ~+> F,K ~+> F] + Loop: [F ~+> 0.0.3,J ~+> 0.0.3] f60.7 ~> f60.7 [F ~+> F,K ~+> F] + Applied Processor: Lare + Details: Unknown bound. MAYBE