MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) [A >= B] (?,1) 1. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,1 + B,D,D,F,F,A,B,I,J,K,L) True (1,1) 2. f4(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 3. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(1 + A,B,D,D,F,F,A,B,I,J,K,L) True (1,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,A,M,N,O,P) [A = B] (?,1) 5. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(O,P,D,M,F,N,A,B,M,N,O,P) True (1,1) 6. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,M,N,M,N,K,L) True (1,1) 7. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(F,D,D,D,F,F,A,B,I,J,K,L) True (1,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [B >= 1 + A] (?,1) 9. f3(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,D,D,F,F,A,B,I,J,K,L) [A >= 1 + B] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f8(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 11. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f4(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) 12. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f3(A,B,C,D,E,F,G,H,I,J,K,L) True (1,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{4,8,9},1->{4,8,9},2->{4,8,9},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{0,2},9->{0,2},10->{} ,11->{0,2},12->{4,8,9}] + Applied Processor: ArgumentFilter [2,3,4,5,6,7,8,9,10,11] + Details: We remove following argument positions: [2,3,4,5,6,7,8,9,10,11]. * Step 2: UnsatPaths MAYBE + Considered Problem: Rules: 0. f4(A,B) -> f3(A,1 + B) [A >= B] (?,1) 1. f0(A,B) -> f3(A,1 + B) True (1,1) 2. f4(A,B) -> f3(1 + A,B) [B >= 1 + A] (?,1) 3. f0(A,B) -> f3(1 + A,B) True (1,1) 4. f3(A,B) -> f8(O,P) [A = B] (?,1) 5. f0(A,B) -> f8(O,P) True (1,1) 6. f0(A,B) -> f3(F,D) True (1,1) 7. f0(A,B) -> f3(F,D) True (1,1) 8. f3(A,B) -> f4(A,B) [B >= 1 + A] (?,1) 9. f3(A,B) -> f4(A,B) [A >= 1 + B] (?,1) 10. f0(A,B) -> f8(A,B) True (1,1) 11. f0(A,B) -> f4(A,B) True (1,1) 12. f0(A,B) -> f3(A,B) True (1,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{4,8,9},1->{4,8,9},2->{4,8,9},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{0,2},9->{0,2},10->{} ,11->{0,2},12->{4,8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(8,0),(9,2)] * Step 3: FromIts MAYBE + Considered Problem: Rules: 0. f4(A,B) -> f3(A,1 + B) [A >= B] (?,1) 1. f0(A,B) -> f3(A,1 + B) True (1,1) 2. f4(A,B) -> f3(1 + A,B) [B >= 1 + A] (?,1) 3. f0(A,B) -> f3(1 + A,B) True (1,1) 4. f3(A,B) -> f8(O,P) [A = B] (?,1) 5. f0(A,B) -> f8(O,P) True (1,1) 6. f0(A,B) -> f3(F,D) True (1,1) 7. f0(A,B) -> f3(F,D) True (1,1) 8. f3(A,B) -> f4(A,B) [B >= 1 + A] (?,1) 9. f3(A,B) -> f4(A,B) [A >= 1 + B] (?,1) 10. f0(A,B) -> f8(A,B) True (1,1) 11. f0(A,B) -> f4(A,B) True (1,1) 12. f0(A,B) -> f3(A,B) True (1,1) Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Flow Graph: [0->{4,8,9},1->{4,8,9},2->{4,8},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{2},9->{0},10->{},11->{0 ,2},12->{4,8,9}] + Applied Processor: FromIts + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f4(A,B) -> f3(A,1 + B) [A >= B] f0(A,B) -> f3(A,1 + B) True f4(A,B) -> f3(1 + A,B) [B >= 1 + A] f0(A,B) -> f3(1 + A,B) True f3(A,B) -> f8(O,P) [A = B] f0(A,B) -> f8(O,P) True f0(A,B) -> f3(F,D) True f0(A,B) -> f3(F,D) True f3(A,B) -> f4(A,B) [B >= 1 + A] f3(A,B) -> f4(A,B) [A >= 1 + B] f0(A,B) -> f8(A,B) True f0(A,B) -> f4(A,B) True f0(A,B) -> f3(A,B) True Signature: {(f0,12);(f3,12);(f4,12);(f8,12)} Rule Graph: [0->{4,8,9},1->{4,8,9},2->{4,8},3->{4,8,9},4->{},5->{},6->{4,8,9},7->{4,8,9},8->{2},9->{0},10->{},11->{0 ,2},12->{4,8,9}] + Applied Processor: AddSinks + Details: () * Step 5: Decompose MAYBE + Considered Problem: Rules: f4(A,B) -> f3(A,1 + B) [A >= B] f0(A,B) -> f3(A,1 + B) True f4(A,B) -> f3(1 + A,B) [B >= 1 + A] f0(A,B) -> f3(1 + A,B) True f3(A,B) -> f8(O,P) [A = B] f0(A,B) -> f8(O,P) True f0(A,B) -> f3(F,D) True f0(A,B) -> f3(F,D) True f3(A,B) -> f4(A,B) [B >= 1 + A] f3(A,B) -> f4(A,B) [A >= 1 + B] f0(A,B) -> f8(A,B) True f0(A,B) -> f4(A,B) True f0(A,B) -> f3(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True Signature: {(exitus616,2);(f0,12);(f3,12);(f4,12);(f8,12)} Rule Graph: [0->{4,8,9},1->{4,8,9},2->{4,8},3->{4,8,9},4->{13,14,16,17,19,20},5->{18},6->{4,8,9},7->{4,8,9},8->{2} ,9->{0},10->{15},11->{0,2},12->{4,8,9}] + 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] | +- p:[0,9] c: [0,9] | `- p:[8,2] c: [2,8] * Step 6: AbstractSize MAYBE + Considered Problem: (Rules: f4(A,B) -> f3(A,1 + B) [A >= B] f0(A,B) -> f3(A,1 + B) True f4(A,B) -> f3(1 + A,B) [B >= 1 + A] f0(A,B) -> f3(1 + A,B) True f3(A,B) -> f8(O,P) [A = B] f0(A,B) -> f8(O,P) True f0(A,B) -> f3(F,D) True f0(A,B) -> f3(F,D) True f3(A,B) -> f4(A,B) [B >= 1 + A] f3(A,B) -> f4(A,B) [A >= 1 + B] f0(A,B) -> f8(A,B) True f0(A,B) -> f4(A,B) True f0(A,B) -> f3(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True f8(A,B) -> exitus616(A,B) True Signature: {(exitus616,2);(f0,12);(f3,12);(f4,12);(f8,12)} Rule Graph: [0->{4,8,9},1->{4,8,9},2->{4,8},3->{4,8,9},4->{13,14,16,17,19,20},5->{18},6->{4,8,9},7->{4,8,9},8->{2} ,9->{0},10->{15},11->{0,2},12->{4,8,9}] ,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] | +- p:[0,9] c: [0,9] | `- p:[8,2] c: [2,8]) + Applied Processor: AbstractSize Minimize + Details: () * Step 7: AbstractFlow MAYBE + Considered Problem: Program: Domain: [A,B,0.0,0.1] f4 ~> f3 [A <= A, B <= K + B] f0 ~> f3 [A <= A, B <= K + B] f4 ~> f3 [A <= A + B, B <= B] f0 ~> f3 [A <= K + A, B <= B] f3 ~> f8 [A <= unknown, B <= unknown] f0 ~> f8 [A <= unknown, B <= unknown] f0 ~> f3 [A <= unknown, B <= unknown] f0 ~> f3 [A <= unknown, B <= unknown] f3 ~> f4 [A <= A, B <= B] f3 ~> f4 [A <= A, B <= B] f0 ~> f8 [A <= A, B <= B] f0 ~> f4 [A <= A, B <= B] f0 ~> f3 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] f8 ~> exitus616 [A <= A, B <= B] + Loop: [0.0 <= 2*K + A + B] f4 ~> f3 [A <= A, B <= K + B] f3 ~> f4 [A <= A, B <= B] + Loop: [0.1 <= 2*K + A + B] f3 ~> f4 [A <= A, B <= B] f4 ~> f3 [A <= A + B, B <= B] + Applied Processor: AbstractFlow + Details: () * Step 8: Failure MAYBE + Considered Problem: Program: Domain: [tick,huge,K,A,B,0.0,0.1] f4 ~> f3 [B ~+> B,K ~+> B] f0 ~> f3 [B ~+> B,K ~+> B] f4 ~> f3 [A ~+> A,B ~+> A] f0 ~> f3 [A ~+> A,K ~+> A] f3 ~> f8 [huge ~=> A,huge ~=> B] f0 ~> f8 [huge ~=> A,huge ~=> B] f0 ~> f3 [huge ~=> A,huge ~=> B] f0 ~> f3 [huge ~=> A,huge ~=> B] f3 ~> f4 [] f3 ~> f4 [] f0 ~> f8 [] f0 ~> f4 [] f0 ~> f3 [] f8 ~> exitus616 [] f8 ~> exitus616 [] f8 ~> exitus616 [] f8 ~> exitus616 [] f8 ~> exitus616 [] f8 ~> exitus616 [] f8 ~> exitus616 [] f8 ~> exitus616 [] + Loop: [A ~+> 0.0,B ~+> 0.0,K ~*> 0.0] f4 ~> f3 [B ~+> B,K ~+> B] f3 ~> f4 [] + Loop: [A ~+> 0.1,B ~+> 0.1,K ~*> 0.1] f3 ~> f4 [] f4 ~> f3 [A ~+> A,B ~+> A] + Applied Processor: Lare + Details: Unknown bound. MAYBE