MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (?,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (?,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (?,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (?,1) Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,10,11,12,13,14,15,16,17,21},3->{0,1,18},4->{0,1,18},5->{0,1,18},6->{8,9,10 ,11,12,13,14,15,16,17,21},7->{8,9,10,11,12,13,14,15,16,17,21},8->{3,19},9->{3,19},10->{3,19},11->{3,19} ,12->{3,19},13->{4,20},14->{4,20},15->{4,20},16->{4,20},17->{4,20},18->{},19->{},20->{},21->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,10) ,(2,11) ,(2,15) ,(2,16) ,(5,0) ,(5,18) ,(6,11) ,(6,12) ,(6,16) ,(6,17) ,(7,10) ,(7,12) ,(7,15) ,(7,17)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] (?,1) 1. f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] (?,1) 2. f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] (?,1) 3. f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] (?,1) 4. f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] (?,1) 5. f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True (1,1) 6. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] (?,1) 7. f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] (?,1) 8. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] (?,1) 9. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] (?,1) 10. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] (?,1) 11. f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] (?,1) 12. f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] (?,1) 13. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] (?,1) 14. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] (?,1) 15. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] (?,1) 16. f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] (?,1) 17. f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] (?,1) 18. f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] (?,1) 19. f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] (?,1) 20. f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] (?,1) 21. f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] (?,1) Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Flow Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,12,13,14,17,21},3->{0,1,18},4->{0,1,18},5->{1},6->{8,9,10,13,14,15,21} ,7->{8,9,11,13,14,16,21},8->{3,19},9->{3,19},10->{3,19},11->{3,19},12->{3,19},13->{4,20},14->{4,20},15->{4 ,20},16->{4,20},17->{4,20},18->{},19->{},20->{},21->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [0 >= A] f5(A,B,C,D,E,F) -> f7(A,B,C,D,E,F) [A >= 2] f7(A,B,C,D,E,F) -> f9(A,0,C,D,E,F) [B = 0] f16(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [255 >= C] f25(A,B,C,D,E,F) -> f5(A,B,C,G,E,F) [C >= 0] f0(A,B,C,D,E,F) -> f5(4,0,C,G,0,F) True f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7(A,B,C,D,E,F) -> f9(-1 + A,B,C,D,E,F) [B >= 1] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] f9(A,B,C,D,E,F) -> f16(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] f9(A,B,C,D,E,F) -> f16(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] f9(A,B,C,D,E,F) -> f25(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] f9(A,B,C,D,E,F) -> f25(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] f5(A,B,C,D,E,F) -> f30(1,B,C,D,E,F) [A = 1] f16(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [C >= 256] f25(A,B,C,D,E,F) -> f30(A,B,C,D,E,F) [0 >= 1 + C] f9(A,B,C,D,E,F) -> f30(A,B,C,D,E,D) [D = F] Signature: {(f0,6);(f16,6);(f25,6);(f30,6);(f5,6);(f7,6);(f9,6)} Rule Graph: [0->{2,6,7},1->{2,6,7},2->{8,9,12,13,14,17,21},3->{0,1,18},4->{0,1,18},5->{1},6->{8,9,10,13,14,15,21} ,7->{8,9,11,13,14,16,21},8->{3,19},9->{3,19},10->{3,19},11->{3,19},12->{3,19},13->{4,20},14->{4,20},15->{4 ,20},16->{4,20},17->{4,20},18->{},19->{},20->{},21->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f5.0(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [0 >= A] f5.0(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [0 >= A] f5.0(A,B,C,D,E,F) -> f7.7(A,B,C,D,E,F) [0 >= A] f5.1(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [A >= 2] f5.1(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [A >= 2] f5.1(A,B,C,D,E,F) -> f7.7(A,B,C,D,E,F) [A >= 2] f7.2(A,B,C,D,E,F) -> f9.8(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.9(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.12(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.13(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.14(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.17(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.21(A,0,C,D,E,F) [B = 0] f16.3(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [255 >= C] f16.3(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [255 >= C] f16.3(A,B,C,D,E,F) -> f5.18(A,B,C,G,E,F) [255 >= C] f25.4(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [C >= 0] f25.4(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [C >= 0] f25.4(A,B,C,D,E,F) -> f5.18(A,B,C,G,E,F) [C >= 0] f0.5(A,B,C,D,E,F) -> f5.1(4,0,C,G,0,F) True f7.6(A,B,C,D,E,F) -> f9.8(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.9(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.10(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.13(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.14(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.15(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.21(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.7(A,B,C,D,E,F) -> f9.8(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.9(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.11(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.13(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.14(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.16(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.21(-1 + A,B,C,D,E,F) [B >= 1] f9.8(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] f9.8(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] f9.9(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] f9.9(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] f9.10(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] f9.10(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] f9.11(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] f9.11(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] f9.12(A,B,C,D,E,F) -> f16.3(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] f9.12(A,B,C,D,E,F) -> f16.19(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] f9.13(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] f9.13(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] f9.14(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] f9.14(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] f9.15(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] f9.15(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] f9.16(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] f9.16(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] f9.17(A,B,C,D,E,F) -> f25.4(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] f9.17(A,B,C,D,E,F) -> f25.20(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] f5.18(A,B,C,D,E,F) -> f30.22(1,B,C,D,E,F) [A = 1] f16.19(A,B,C,D,E,F) -> f30.22(A,B,C,D,E,F) [C >= 256] f25.20(A,B,C,D,E,F) -> f30.22(A,B,C,D,E,F) [0 >= 1 + C] f9.21(A,B,C,D,E,F) -> f30.22(A,B,C,D,E,D) [D = F] Signature: {(f0.5,6) ;(f16.19,6) ;(f16.3,6) ;(f25.20,6) ;(f25.4,6) ;(f30.22,6) ;(f5.0,6) ;(f5.1,6) ;(f5.18,6) ;(f7.2,6) ;(f7.6,6) ;(f7.7,6) ;(f9.10,6) ;(f9.11,6) ;(f9.12,6) ;(f9.13,6) ;(f9.14,6) ;(f9.15,6) ;(f9.16,6) ;(f9.17,6) ;(f9.21,6) ;(f9.8,6) ;(f9.9,6)} Rule Graph: [0->{6,7,8,9,10,11,12},1->{20,21,22,23,24,25,26},2->{27,28,29,30,31,32,33},3->{6,7,8,9,10,11,12},4->{20,21 ,22,23,24,25,26},5->{27,28,29,30,31,32,33},6->{34,35},7->{36,37},8->{42,43},9->{44,45},10->{46,47},11->{52 ,53},12->{57},13->{0,1,2},14->{3,4,5},15->{54},16->{0,1,2},17->{3,4,5},18->{54},19->{3,4,5},20->{34,35} ,21->{36,37},22->{38,39},23->{44,45},24->{46,47},25->{48,49},26->{57},27->{34,35},28->{36,37},29->{40,41} ,30->{44,45},31->{46,47},32->{50,51},33->{57},34->{13,14,15},35->{55},36->{13,14,15},37->{55},38->{13,14,15} ,39->{55},40->{13,14,15},41->{55},42->{13,14,15},43->{55},44->{16,17,18},45->{56},46->{16,17,18},47->{56} ,48->{16,17,18},49->{56},50->{16,17,18},51->{56},52->{16,17,18},53->{56},54->{},55->{},56->{},57->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f5.0(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [0 >= A] f5.0(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [0 >= A] f5.0(A,B,C,D,E,F) -> f7.7(A,B,C,D,E,F) [0 >= A] f5.1(A,B,C,D,E,F) -> f7.2(A,B,C,D,E,F) [A >= 2] f5.1(A,B,C,D,E,F) -> f7.6(A,B,C,D,E,F) [A >= 2] f5.1(A,B,C,D,E,F) -> f7.7(A,B,C,D,E,F) [A >= 2] f7.2(A,B,C,D,E,F) -> f9.8(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.9(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.12(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.13(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.14(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.17(A,0,C,D,E,F) [B = 0] f7.2(A,B,C,D,E,F) -> f9.21(A,0,C,D,E,F) [B = 0] f16.3(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [255 >= C] f16.3(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [255 >= C] f16.3(A,B,C,D,E,F) -> f5.18(A,B,C,G,E,F) [255 >= C] f25.4(A,B,C,D,E,F) -> f5.0(A,B,C,G,E,F) [C >= 0] f25.4(A,B,C,D,E,F) -> f5.1(A,B,C,G,E,F) [C >= 0] f25.4(A,B,C,D,E,F) -> f5.18(A,B,C,G,E,F) [C >= 0] f0.5(A,B,C,D,E,F) -> f5.1(4,0,C,G,0,F) True f7.6(A,B,C,D,E,F) -> f9.8(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.9(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.10(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.13(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.14(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.15(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.6(A,B,C,D,E,F) -> f9.21(-1 + A,B,C,D,E,F) [0 >= 1 + B] f7.7(A,B,C,D,E,F) -> f9.8(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.9(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.11(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.13(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.14(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.16(-1 + A,B,C,D,E,F) [B >= 1] f7.7(A,B,C,D,E,F) -> f9.21(-1 + A,B,C,D,E,F) [B >= 1] f9.8(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] f9.8(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [0 >= E && D >= 1 + F] f9.9(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] f9.9(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [E >= 2 && D >= 1 + F] f9.10(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] f9.10(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [0 >= 1 + B && D >= 1 + F && E = 1] f9.11(A,B,C,D,E,F) -> f16.3(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] f9.11(A,B,C,D,E,F) -> f16.19(A,B,A + C,D,2,F) [B >= 1 && D >= 1 + F && E = 1] f9.12(A,B,C,D,E,F) -> f16.3(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] f9.12(A,B,C,D,E,F) -> f16.19(-1 + A,1,-1 + A + C,D,2,F) [D >= 1 + F && B = 0 && E = 1] f9.13(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] f9.13(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [1 >= E && F >= 1 + D] f9.14(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] f9.14(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [E >= 3 && F >= 1 + D] f9.15(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] f9.15(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [0 >= 1 + B && F >= 1 + D && E = 2] f9.16(A,B,C,D,E,F) -> f25.4(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] f9.16(A,B,C,D,E,F) -> f25.20(A,B,-1*A + C,D,1,F) [B >= 1 && F >= 1 + D && E = 2] f9.17(A,B,C,D,E,F) -> f25.4(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] f9.17(A,B,C,D,E,F) -> f25.20(-1 + A,1,1 + -1*A + C,D,1,F) [F >= 1 + D && B = 0 && E = 2] f5.18(A,B,C,D,E,F) -> f30.22(1,B,C,D,E,F) [A = 1] f16.19(A,B,C,D,E,F) -> f30.22(A,B,C,D,E,F) [C >= 256] f25.20(A,B,C,D,E,F) -> f30.22(A,B,C,D,E,F) [0 >= 1 + C] f9.21(A,B,C,D,E,F) -> f30.22(A,B,C,D,E,D) [D = F] f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True f30.22(A,B,C,D,E,F) -> exitus616(A,B,C,D,E,F) True Signature: {(exitus616,6) ;(f0.5,6) ;(f16.19,6) ;(f16.3,6) ;(f25.20,6) ;(f25.4,6) ;(f30.22,6) ;(f5.0,6) ;(f5.1,6) ;(f5.18,6) ;(f7.2,6) ;(f7.6,6) ;(f7.7,6) ;(f9.10,6) ;(f9.11,6) ;(f9.12,6) ;(f9.13,6) ;(f9.14,6) ;(f9.15,6) ;(f9.16,6) ;(f9.17,6) ;(f9.21,6) ;(f9.8,6) ;(f9.9,6)} Rule Graph: [0->{6,7,8,9,10,11,12},1->{20,21,22,23,24,25,26},2->{27,28,29,30,31,32,33},3->{6,7,8,9,10,11,12},4->{20,21 ,22,23,24,25,26},5->{27,28,29,30,31,32,33},6->{34,35},7->{36,37},8->{42,43},9->{44,45},10->{46,47},11->{52 ,53},12->{57},13->{0,1,2},14->{3,4,5},15->{54},16->{0,1,2},17->{3,4,5},18->{54},19->{3,4,5},20->{34,35} ,21->{36,37},22->{38,39},23->{44,45},24->{46,47},25->{48,49},26->{57},27->{34,35},28->{36,37},29->{40,41} ,30->{44,45},31->{46,47},32->{50,51},33->{57},34->{13,14,15},35->{55},36->{13,14,15},37->{55},38->{13,14,15} ,39->{55},40->{13,14,15},41->{55},42->{13,14,15},43->{55},44->{16,17,18},45->{56},46->{16,17,18},47->{56} ,48->{16,17,18},49->{56},50->{16,17,18},51->{56},52->{16,17,18},53->{56},54->{64,70},55->{66,68,69,71,72} ,56->{59,61,63,65,67},57->{58,60,62}] + 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,48,49,50,51,52,53,54,55,56,57,58,59,60,61,62,63,64,65,66,67,68,69,70,71,72] | `- p:[0,13,34,6,3,14,36,7,21,1,16,44,9,23,4,17,46,10,24,31,2,5,48,25,50,32,52,11,30,28,38,22,40,29,42,8,20,27] c: [4,5,8,11,42,52] | `- p:[0,13,34,6,3,14,36,7,21,1,16,44,9,23,30,2,46,10,24,31,48,25,50,32,28,38,22,40,29,17,20,27] c: [] MAYBE