MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E) -> f300(A,B,C,D,E) True (1,1) 1. f4(A,B,C,D,E) -> f300(A,B,1 + C,D,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && A >= B] (?,1) 2. f4(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] (?,1) 3. f4(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] (?,1) 4. f4(A,B,C,D,E) -> f2(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] (?,1) 5. f2(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-1*D >= 0 (?,1) && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] 6. f2(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-1*D >= 0 (?,1) && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] 7. f2(A,B,C,D,E) -> f2(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 8. f300(A,B,C,D,E) -> f1(A,B,C,D,F) [C >= A] (?,1) 9. f300(A,B,C,D,E) -> f300(A,B,1 + C,D,E) [A >= 1 + C && A >= B] (?,1) 10. f300(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] (?,1) 11. f300(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] (?,1) 12. f300(A,B,C,D,E) -> f2(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] (?,1) Signature: {(f1,5);(f2,5);(f300,5);(f4,5);(f5,5)} Flow Graph: [0->{8,9,10,11,12},1->{8,9,10,11,12},2->{1,2,3,4},3->{1,2,3,4},4->{5,6,7},5->{1,2,3,4},6->{1,2,3,4},7->{5 ,6,7},8->{},9->{8,9,10,11,12},10->{1,2,3,4},11->{1,2,3,4},12->{5,6,7}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(1,8),(1,10),(1,11),(1,12),(9,10),(9,11),(9,12)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f5(A,B,C,D,E) -> f300(A,B,C,D,E) True (1,1) 1. f4(A,B,C,D,E) -> f300(A,B,1 + C,D,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && A >= B] (?,1) 2. f4(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] (?,1) 3. f4(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] (?,1) 4. f4(A,B,C,D,E) -> f2(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] (?,1) 5. f2(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-1*D >= 0 (?,1) && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] 6. f2(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-1*D >= 0 (?,1) && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] 7. f2(A,B,C,D,E) -> f2(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] (?,1) 8. f300(A,B,C,D,E) -> f1(A,B,C,D,F) [C >= A] (?,1) 9. f300(A,B,C,D,E) -> f300(A,B,1 + C,D,E) [A >= 1 + C && A >= B] (?,1) 10. f300(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] (?,1) 11. f300(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] (?,1) 12. f300(A,B,C,D,E) -> f2(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] (?,1) Signature: {(f1,5);(f2,5);(f300,5);(f4,5);(f5,5)} Flow Graph: [0->{8,9,10,11,12},1->{9},2->{1,2,3,4},3->{1,2,3,4},4->{5,6,7},5->{1,2,3,4},6->{1,2,3,4},7->{5,6,7},8->{} ,9->{8,9},10->{1,2,3,4},11->{1,2,3,4},12->{5,6,7}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f5(A,B,C,D,E) -> f300(A,B,C,D,E) True f4(A,B,C,D,E) -> f300(A,B,1 + C,D,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && A >= B] f4(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4(A,B,C,D,E) -> f2(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f2(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2(A,B,C,D,E) -> f2(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f300(A,B,C,D,E) -> f1(A,B,C,D,F) [C >= A] f300(A,B,C,D,E) -> f300(A,B,1 + C,D,E) [A >= 1 + C && A >= B] f300(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300(A,B,C,D,E) -> f4(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300(A,B,C,D,E) -> f2(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] Signature: {(f1,5);(f2,5);(f300,5);(f4,5);(f5,5)} Rule Graph: [0->{8,9,10,11,12},1->{9},2->{1,2,3,4},3->{1,2,3,4},4->{5,6,7},5->{1,2,3,4},6->{1,2,3,4},7->{5,6,7},8->{} ,9->{8,9},10->{1,2,3,4},11->{1,2,3,4},12->{5,6,7}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f5.0(A,B,C,D,E) -> f300.8(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.9(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.10(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.11(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.12(A,B,C,D,E) True f4.1(A,B,C,D,E) -> f300.9(A,B,1 + C,D,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && A >= B] f4.2(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.2(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.2(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.2(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.4(A,B,C,D,E) -> f2.5(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f4.4(A,B,C,D,E) -> f2.6(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f4.4(A,B,C,D,E) -> f2.7(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.7(A,B,C,D,E) -> f2.5(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f2.7(A,B,C,D,E) -> f2.6(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f2.7(A,B,C,D,E) -> f2.7(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f300.8(A,B,C,D,E) -> f1.13(A,B,C,D,F) [C >= A] f300.9(A,B,C,D,E) -> f300.8(A,B,1 + C,D,E) [A >= 1 + C && A >= B] f300.9(A,B,C,D,E) -> f300.9(A,B,1 + C,D,E) [A >= 1 + C && A >= B] f300.10(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.10(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.10(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.10(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.12(A,B,C,D,E) -> f2.5(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] f300.12(A,B,C,D,E) -> f2.6(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] f300.12(A,B,C,D,E) -> f2.7(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] Signature: {(f1.13,5) ;(f2.5,5) ;(f2.6,5) ;(f2.7,5) ;(f300.10,5) ;(f300.11,5) ;(f300.12,5) ;(f300.8,5) ;(f300.9,5) ;(f4.1,5) ;(f4.2,5) ;(f4.3,5) ;(f4.4,5) ;(f5.0,5)} Rule Graph: [0->{28},1->{29,30},2->{31,32,33,34},3->{35,36,37,38},4->{39,40,41},5->{29,30},6->{5},7->{6,7,8,9},8->{10 ,11,12,13},9->{14,15,16},10->{5},11->{6,7,8,9},12->{10,11,12,13},13->{14,15,16},14->{17,18,19,20},15->{21,22 ,23,24},16->{25,26,27},17->{5},18->{6,7,8,9},19->{10,11,12,13},20->{14,15,16},21->{5},22->{6,7,8,9},23->{10 ,11,12,13},24->{14,15,16},25->{17,18,19,20},26->{21,22,23,24},27->{25,26,27},28->{},29->{28},30->{29,30} ,31->{5},32->{6,7,8,9},33->{10,11,12,13},34->{14,15,16},35->{5},36->{6,7,8,9},37->{10,11,12,13},38->{14,15 ,16},39->{17,18,19,20},40->{21,22,23,24},41->{25,26,27}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f5.0(A,B,C,D,E) -> f300.8(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.9(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.10(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.11(A,B,C,D,E) True f5.0(A,B,C,D,E) -> f300.12(A,B,C,D,E) True f4.1(A,B,C,D,E) -> f300.9(A,B,1 + C,D,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && A >= B] f4.2(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.2(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.2(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.2(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && F >= 1 && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.3(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f4.4(A,B,C,D,E) -> f2.5(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f4.4(A,B,C,D,E) -> f2.6(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f4.4(A,B,C,D,E) -> f2.7(A,B,C,0,E) [-2 + B + -1*C >= 0 && -2 + A + -1*C >= 0 && -1*A + B >= 0 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.5(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && F >= 1 && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.6(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && 0 >= 1 + F && B >= 1 + A] f2.7(A,B,C,D,E) -> f2.5(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f2.7(A,B,C,D,E) -> f2.6(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f2.7(A,B,C,D,E) -> f2.7(A,B,C,0,E) [-1*D >= 0 && D >= 0 && -2 + B + -1*C >= 0 && -1 + A + -1*C >= 0 && -1 + -1*A + B >= 0 && B >= 1 + A] f300.8(A,B,C,D,E) -> f1.13(A,B,C,D,F) [C >= A] f300.9(A,B,C,D,E) -> f300.8(A,B,1 + C,D,E) [A >= 1 + C && A >= B] f300.9(A,B,C,D,E) -> f300.9(A,B,1 + C,D,E) [A >= 1 + C && A >= B] f300.10(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.10(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.10(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.10(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [F >= 1 && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.1(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.2(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.3(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.11(A,B,C,D,E) -> f4.4(1 + A,B,C,F,E) [0 >= 1 + F && A >= 1 + C && B >= 1 + A] f300.12(A,B,C,D,E) -> f2.5(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] f300.12(A,B,C,D,E) -> f2.6(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] f300.12(A,B,C,D,E) -> f2.7(A,B,C,0,E) [A >= 1 + C && B >= 1 + A] f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True f1.13(A,B,C,D,E) -> exitus616(A,B,C,D,E) True Signature: {(exitus616,5) ;(f1.13,5) ;(f2.5,5) ;(f2.6,5) ;(f2.7,5) ;(f300.10,5) ;(f300.11,5) ;(f300.12,5) ;(f300.8,5) ;(f300.9,5) ;(f4.1,5) ;(f4.2,5) ;(f4.3,5) ;(f4.4,5) ;(f5.0,5)} Rule Graph: [0->{28},1->{29,30},2->{31,32,33,34},3->{35,36,37,38},4->{39,40,41},5->{29,30},6->{5},7->{6,7,8,9},8->{10 ,11,12,13},9->{14,15,16},10->{5},11->{6,7,8,9},12->{10,11,12,13},13->{14,15,16},14->{17,18,19,20},15->{21,22 ,23,24},16->{25,26,27},17->{5},18->{6,7,8,9},19->{10,11,12,13},20->{14,15,16},21->{5},22->{6,7,8,9},23->{10 ,11,12,13},24->{14,15,16},25->{17,18,19,20},26->{21,22,23,24},27->{25,26,27},28->{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,73,74,75,76,77,78,79,80,81},29->{28} ,30->{29,30},31->{5},32->{6,7,8,9},33->{10,11,12,13},34->{14,15,16},35->{5},36->{6,7,8,9},37->{10,11,12,13} ,38->{14,15,16},39->{17,18,19,20},40->{21,22,23,24},41->{25,26,27}] + 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,73,74,75,76,77,78,79,80,81] | +- p:[7,11,8,18,14,9,22,15,13,12,19,25,16,20,24,26,27,23] c: [7,8,9,11,12,13,14,15,16,18,19,20,22,23,24,25,26] | | | `- p:[27] c: [] | `- p:[30] c: [30] MAYBE