YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (?,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (?,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (?,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (?,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (?,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (?,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (?,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (?,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26},1->{24,25,26},2->{3,34},3->{3,34},4->{6,7,8},5->{6,7,8},6->{4,5,9,33},7->{4,5,9,33},8->{4,5 ,9,33},9->{4,5,9,33},10->{11,12,16,31},11->{13,14,15},12->{13,14,15},13->{11,12,16,31},14->{11,12,16,31} ,15->{11,12,16,31},16->{11,12,16,31},17->{19,20,21,22},18->{19,20,21,22},19->{17,18,23,28,29,30},20->{17,18 ,23,28,29,30},21->{17,18,23,28,29,30},22->{17,18,23,28,29,30},23->{17,18,23,28,29,30},24->{},25->{},26->{} ,27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30},33->{10,32},34->{4,5,9,33}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,34) ,(6,4) ,(6,9) ,(7,4) ,(7,5) ,(8,4) ,(8,5) ,(9,4) ,(9,5) ,(10,31) ,(13,11) ,(13,16) ,(14,11) ,(14,16) ,(15,11) ,(15,12) ,(16,11) ,(16,12) ,(19,17) ,(19,23) ,(20,17) ,(20,23) ,(21,17) ,(21,18) ,(22,17) ,(22,18) ,(23,17) ,(23,18)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] (?,1) 1. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] (?,1) 2. f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True (1,1) 3. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] (?,1) 4. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] (?,1) 5. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] (?,1) 6. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] (?,1) 7. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] (?,1) 8. f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] (?,1) 9. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] (?,1) 10. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] (?,1) 11. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] (?,1) 12. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] (?,1) 13. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] (?,1) 14. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True (?,1) 15. f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True (?,1) 16. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] (?,1) 17. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] (?,1) 18. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] (?,1) 19. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] (?,1) 20. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] (?,1) 21. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] (?,1) 22. f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True (?,1) 23. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] (?,1) 24. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] (?,1) 25. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] (?,1) 26. f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] (?,1) 27. f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] (?,1) 28. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] (?,1) 29. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] (?,1) 30. f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] (?,1) 31. f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] (?,1) 32. f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] (?,1) 33. f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) 34. f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] (?,1) Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Flow Graph: [0->{24,25,26},1->{24,25,26},2->{3},3->{3,34},4->{6,7,8},5->{6,7,8},6->{5,33},7->{9,33},8->{9,33},9->{9 ,33},10->{11,12,16},11->{13,14,15},12->{13,14,15},13->{12,31},14->{12,31},15->{16,31},16->{16,31},17->{19,20 ,21,22},18->{19,20,21,22},19->{18,28,29,30},20->{18,28,29,30},21->{23,28,29,30},22->{23,28,29,30},23->{23,28 ,29,30},24->{},25->{},26->{},27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30} ,33->{10,32},34->{4,5,9,33}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Rule Graph: [0->{24,25,26},1->{24,25,26},2->{3},3->{3,34},4->{6,7,8},5->{6,7,8},6->{5,33},7->{9,33},8->{9,33},9->{9 ,33},10->{11,12,16},11->{13,14,15},12->{13,14,15},13->{12,31},14->{12,31},15->{16,31},16->{16,31},17->{19,20 ,21,22},18->{19,20,21,22},19->{18,28,29,30},20->{18,28,29,30},21->{23,28,29,30},22->{23,28,29,30},23->{23,28 ,29,30},24->{},25->{},26->{},27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30} ,33->{10,32},34->{4,5,9,33}] + Applied Processor: Decompose NoGreedy + 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] | +- p:[3] c: [3] | +- p:[6,5] c: [5,6] | +- p:[9] c: [9] | +- p:[10,31,13,11,12,14,15,16] c: [10,11,31] | | | +- p:[12,13,14] c: [12,13,14] | | | `- p:[16] c: [16] | +- p:[19,18,20] c: [18,19,20] | `- p:[23] c: [23] * Step 4: CloseWith YES + Considered Problem: (Rules: f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f63(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1] f0(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(1,12,1,1,M,0,G,H,I,J,K,L) True f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f13(A,B,C,D,E,1 + F,G,H,I,J,K,L) [B >= 1 + F] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && B >= 1 + F] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f22(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && B >= 1 + F] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,1,D,E,1 + F,1,H,I,J,K,L) [M >= 0 && B >= 1 + N] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [M >= 0] f22(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [0 >= 1 + M] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,0,D,E,1 + F,0,H,I,J,K,L) [B >= 1 + F && C = 0] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(A,B,C,D,E,F,G,1 + F,I,J,K,L) [B >= 2 + F] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + A && B >= 1 + H] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f38(A,B,C,D,E,F,G,H,I,J,K,L) [A >= 1 && B >= 1 + H] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) [M >= 1 + N] f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(1,B,C,D,E,F,G,1 + H,1,J,K,L) True f38(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) True f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f35(0,B,C,D,E,F,G,1 + H,0,J,K,L) [B >= 1 + H && A = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [0 >= 1 + D && B >= 2 + F] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f52(A,B,C,D,E,F,G,H,I,M,K,L) [D >= 1 && B >= 2 + F] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [0 >= 1 + J] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,1,E,1 + F,G,H,I,J,1,L) [J >= 1] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,0,0,L) [J = 0] f52(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,J,0,L) True f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,0,E,1 + F,G,H,I,M,0,L) [B >= 2 + F && D = 0] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [0 >= 1 + D] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,D,E,F,G,H,I,J,K,0) [D >= 1] f63(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,C,0,E,F,G,H,I,J,K,1) [D = 0] f62(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(0,B,C,D,E,F,G,H,I,J,K,1) [A = 0] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [0 >= 1 + C && 1 + F >= B] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f62(A,B,C,D,E,F,G,H,I,J,K,L) [C >= 1 && 1 + F >= B] f48(A,B,C,D,E,F,G,H,I,J,K,L) -> f71(A,B,0,D,E,F,G,H,I,J,K,1) [1 + F >= B && C = 0] f35(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,1 + F,G,H,I,J,K,L) [H >= B] f32(A,B,C,D,E,F,G,H,I,J,K,L) -> f48(A,B,C,D,E,0,G,H,I,J,K,L) [1 + F >= B] f19(A,B,C,D,E,F,G,H,I,J,K,L) -> f32(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] f13(A,B,C,D,E,F,G,H,I,J,K,L) -> f19(A,B,C,D,E,0,G,H,I,J,K,L) [F >= B] Signature: {(f0,12) ;(f13,12) ;(f19,12) ;(f22,12) ;(f32,12) ;(f35,12) ;(f38,12) ;(f48,12) ;(f52,12) ;(f62,12) ;(f63,12) ;(f71,12)} Rule Graph: [0->{24,25,26},1->{24,25,26},2->{3},3->{3,34},4->{6,7,8},5->{6,7,8},6->{5,33},7->{9,33},8->{9,33},9->{9 ,33},10->{11,12,16},11->{13,14,15},12->{13,14,15},13->{12,31},14->{12,31},15->{16,31},16->{16,31},17->{19,20 ,21,22},18->{19,20,21,22},19->{18,28,29,30},20->{18,28,29,30},21->{23,28,29,30},22->{23,28,29,30},23->{23,28 ,29,30},24->{},25->{},26->{},27->{},28->{0,1,27},29->{0,1,27},30->{},31->{10,32},32->{17,18,23,28,29,30} ,33->{10,32},34->{4,5,9,33}] ,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] | +- p:[3] c: [3] | +- p:[6,5] c: [5,6] | +- p:[9] c: [9] | +- p:[10,31,13,11,12,14,15,16] c: [10,11,31] | | | +- p:[12,13,14] c: [12,13,14] | | | `- p:[16] c: [16] | +- p:[19,18,20] c: [18,19,20] | `- p:[23] c: [23]) + Applied Processor: CloseWith True + Details: () YES