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