MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(1 + H1,B,C,D,E,G1,G1,G1,G1,1 + L1,G1,L,M,N,O,J1,K1,R,S,T,I1,N1,O1,P1,Q1,Z,A1,B1,C1,D1,E1,F1) [A >= 0 && M1 >= 0 && Q >= 1 + J && H1 >= 0] (?,1) 1. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f18(G1,B,C,D,E,F,G,H,I,K1,K,L,0,N,0,H1,J1,0,S,T,U,V,W,X,Y,L1,A1,B1,C1,D1,E1,F1) [A >= 0 && I1 >= 0 && J >= Q && G1 >= 0] (?,1) 2. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(G1,N1,C,D,E,F,G,H,I,I1,J1,Q1,0,N,H1,K1,L1,M1,S,T,U,V,W,X,Y,V1,O1,P1,T1,U1,E1,F1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && O1 >= 1] (?,1) 3. f16(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(G1,N1,C,D,E,F,G,H,I,I1,J1,Q1,0,N,H1,K1,L1,M1,S,T,U,V,W,X,Y,V1,O1,P1,T1,U1,E1,F1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && 0 >= 1 + O1] (?,1) 4. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f25(G1,B,B,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 && B >= 1 && G1 >= 1] (?,1) 5. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f25(G1,B,B,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [A >= 1 && 0 >= 1 + B && G1 >= 1] (?,1) 6. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(J,B,C,D,G1,H1,H1,H1,H1,1 + J,H1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (?,1) 7. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f16(1 + H1,B,C,D,E,G1,G1,G1,G1,1 + J,G1,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [H1 >= 0 && A >= 0] (?,1) 8. f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f22(G1,L,0,0,E,F,G,H,L,J,K,L,L,L,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [H1 >= 1 && A >= 1 && B = 0] (?,1) 9. f33(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) -> f3(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) True (1,1) Signature: {(f16,32);(f18,32);(f22,32);(f25,32);(f3,32);(f33,32)} Flow Graph: [0->{0,1,2,3},1->{},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{},5->{},6->{0,1,2,3},7->{0,1,2,3},8->{},9->{4,5,6,7 ,8}] + Applied Processor: ArgumentFilter [2,3,4,5,6,7,8,10,11,12,13,14,15,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31] + Details: We remove following argument positions: [2 ,3 ,4 ,5 ,6 ,7 ,8 ,10 ,11 ,12 ,13 ,14 ,15 ,17 ,18 ,19 ,20 ,21 ,22 ,23 ,24 ,25 ,26 ,27 ,28 ,29 ,30 ,31]. * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f16(A,B,J,Q) -> f16(1 + H1,B,1 + L1,K1) [A >= 0 && M1 >= 0 && Q >= 1 + J && H1 >= 0] (?,1) 1. f16(A,B,J,Q) -> f18(G1,B,K1,J1) [A >= 0 && I1 >= 0 && J >= Q && G1 >= 0] (?,1) 2. f16(A,B,J,Q) -> f3(G1,N1,I1,L1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && O1 >= 1] (?,1) 3. f16(A,B,J,Q) -> f3(G1,N1,I1,L1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && 0 >= 1 + O1] (?,1) 4. f3(A,B,J,Q) -> f25(G1,B,J,Q) [A >= 1 && B >= 1 && G1 >= 1] (?,1) 5. f3(A,B,J,Q) -> f25(G1,B,J,Q) [A >= 1 && 0 >= 1 + B && G1 >= 1] (?,1) 6. f3(A,B,J,Q) -> f16(J,B,1 + J,Q) True (?,1) 7. f3(A,B,J,Q) -> f16(1 + H1,B,1 + J,Q) [H1 >= 0 && A >= 0] (?,1) 8. f3(A,B,J,Q) -> f22(G1,L,J,Q) [H1 >= 1 && A >= 1 && B = 0] (?,1) 9. f33(A,B,J,Q) -> f3(A,B,J,Q) True (1,1) Signature: {(f16,32);(f18,32);(f22,32);(f25,32);(f3,32);(f33,32)} Flow Graph: [0->{0,1,2,3},1->{},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{},5->{},6->{0,1,2,3},7->{0,1,2,3},8->{},9->{4,5,6,7 ,8}] + Applied Processor: FromIts + Details: () * Step 3: AddSinks MAYBE + Considered Problem: Rules: f16(A,B,J,Q) -> f16(1 + H1,B,1 + L1,K1) [A >= 0 && M1 >= 0 && Q >= 1 + J && H1 >= 0] f16(A,B,J,Q) -> f18(G1,B,K1,J1) [A >= 0 && I1 >= 0 && J >= Q && G1 >= 0] f16(A,B,J,Q) -> f3(G1,N1,I1,L1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && O1 >= 1] f16(A,B,J,Q) -> f3(G1,N1,I1,L1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && 0 >= 1 + O1] f3(A,B,J,Q) -> f25(G1,B,J,Q) [A >= 1 && B >= 1 && G1 >= 1] f3(A,B,J,Q) -> f25(G1,B,J,Q) [A >= 1 && 0 >= 1 + B && G1 >= 1] f3(A,B,J,Q) -> f16(J,B,1 + J,Q) True f3(A,B,J,Q) -> f16(1 + H1,B,1 + J,Q) [H1 >= 0 && A >= 0] f3(A,B,J,Q) -> f22(G1,L,J,Q) [H1 >= 1 && A >= 1 && B = 0] f33(A,B,J,Q) -> f3(A,B,J,Q) True Signature: {(f16,32);(f18,32);(f22,32);(f25,32);(f3,32);(f33,32)} Rule Graph: [0->{0,1,2,3},1->{},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{},5->{},6->{0,1,2,3},7->{0,1,2,3},8->{},9->{4,5,6,7 ,8}] + Applied Processor: AddSinks + Details: () * Step 4: Failure MAYBE + Considered Problem: Rules: f16(A,B,J,Q) -> f16(1 + H1,B,1 + L1,K1) [A >= 0 && M1 >= 0 && Q >= 1 + J && H1 >= 0] f16(A,B,J,Q) -> f18(G1,B,K1,J1) [A >= 0 && I1 >= 0 && J >= Q && G1 >= 0] f16(A,B,J,Q) -> f3(G1,N1,I1,L1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && O1 >= 1] f16(A,B,J,Q) -> f3(G1,N1,I1,L1) [A >= 0 && R1 >= 0 && S1 >= 0 && J >= Q && 0 >= 1 + O1] f3(A,B,J,Q) -> f25(G1,B,J,Q) [A >= 1 && B >= 1 && G1 >= 1] f3(A,B,J,Q) -> f25(G1,B,J,Q) [A >= 1 && 0 >= 1 + B && G1 >= 1] f3(A,B,J,Q) -> f16(J,B,1 + J,Q) True f3(A,B,J,Q) -> f16(1 + H1,B,1 + J,Q) [H1 >= 0 && A >= 0] f3(A,B,J,Q) -> f22(G1,L,J,Q) [H1 >= 1 && A >= 1 && B = 0] f33(A,B,J,Q) -> f3(A,B,J,Q) True f22(A,B,J,Q) -> exitus616(A,B,J,Q) True f25(A,B,J,Q) -> exitus616(A,B,J,Q) True f25(A,B,J,Q) -> exitus616(A,B,J,Q) True f18(A,B,J,Q) -> exitus616(A,B,J,Q) True Signature: {(exitus616,4);(f16,32);(f18,32);(f22,32);(f25,32);(f3,32);(f33,32)} Rule Graph: [0->{0,1,2,3},1->{13},2->{4,5,6,7,8},3->{4,5,6,7,8},4->{12},5->{11},6->{0,1,2,3},7->{0,1,2,3},8->{10} ,9->{4,5,6,7,8}] + Applied Processor: Decompose Greedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9,10,11,12,13] | `- p:[0,6,2,7,3] c: [] MAYBE