MAYBE * Step 1: UnsatPaths MAYBE + Considered Problem: Rules: 0. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] (?,1) 1. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] (?,1) 2. f0(A,B,C,D) -> f4(A,B,C,1 + B) [B >= 0 && C >= B] (1,1) 3. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] (?,1) 4. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] (?,1) 5. f7(A,B,C,D) -> f4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] (?,1) 6. f7(A,B,C,D) -> f4(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] (?,1) 7. f6(A,B,C,D) -> f14(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] (?,1) 8. f4(A,B,C,D) -> f14(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] (?,1) Signature: {(f0,4);(f14,4);(f4,4);(f6,4);(f7,4)} Flow Graph: [0->{5,6},1->{5,6},2->{3,4,8},3->{0,1,7},4->{0,1,7},5->{3,4,8},6->{3,4,8},7->{},8->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,3),(2,8),(6,4)] * Step 2: FromIts MAYBE + Considered Problem: Rules: 0. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] (?,1) 1. f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] (?,1) 2. f0(A,B,C,D) -> f4(A,B,C,1 + B) [B >= 0 && C >= B] (1,1) 3. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] (?,1) 4. f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] (?,1) 5. f7(A,B,C,D) -> f4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] (?,1) 6. f7(A,B,C,D) -> f4(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] (?,1) 7. f6(A,B,C,D) -> f14(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] (?,1) 8. f4(A,B,C,D) -> f14(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] (?,1) Signature: {(f0,4);(f14,4);(f4,4);(f6,4);(f7,4)} Flow Graph: [0->{5,6},1->{5,6},2->{4},3->{0,1,7},4->{0,1,7},5->{3,4,8},6->{3,8},7->{},8->{}] + Applied Processor: FromIts + Details: () * Step 3: Unfold MAYBE + Considered Problem: Rules: f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] f6(A,B,C,D) -> f7(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] f0(A,B,C,D) -> f4(A,B,C,1 + B) [B >= 0 && C >= B] f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4(A,B,C,D) -> f6(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f7(A,B,C,D) -> f4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7(A,B,C,D) -> f4(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] f6(A,B,C,D) -> f14(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] f4(A,B,C,D) -> f14(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] Signature: {(f0,4);(f14,4);(f4,4);(f6,4);(f7,4)} Rule Graph: [0->{5,6},1->{5,6},2->{4},3->{0,1,7},4->{0,1,7},5->{3,4,8},6->{3,8},7->{},8->{}] + Applied Processor: Unfold + Details: () * Step 4: AddSinks MAYBE + Considered Problem: Rules: f6.0(A,B,C,D) -> f7.5(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] f6.0(A,B,C,D) -> f7.6(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] f6.1(A,B,C,D) -> f7.5(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] f6.1(A,B,C,D) -> f7.6(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] f0.2(A,B,C,D) -> f4.4(A,B,C,1 + B) [B >= 0 && C >= B] f4.3(A,B,C,D) -> f6.0(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4.3(A,B,C,D) -> f6.1(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4.3(A,B,C,D) -> f6.7(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4.4(A,B,C,D) -> f6.0(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f4.4(A,B,C,D) -> f6.1(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f4.4(A,B,C,D) -> f6.7(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f7.5(A,B,C,D) -> f4.3(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7.5(A,B,C,D) -> f4.4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7.5(A,B,C,D) -> f4.8(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7.6(A,B,C,D) -> f4.3(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] f7.6(A,B,C,D) -> f4.8(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] f6.7(A,B,C,D) -> f14.9(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] f4.8(A,B,C,D) -> f14.9(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] Signature: {(f0.2,4);(f14.9,4);(f4.3,4);(f4.4,4);(f4.8,4);(f6.0,4);(f6.1,4);(f6.7,4);(f7.5,4);(f7.6,4)} Rule Graph: [0->{11,12,13},1->{14,15},2->{11,12,13},3->{14,15},4->{8,9,10},5->{0,1},6->{2,3},7->{16},8->{0,1},9->{2,3} ,10->{16},11->{5,6,7},12->{8,9,10},13->{17},14->{5,6,7},15->{17},16->{},17->{}] + Applied Processor: AddSinks + Details: () * Step 5: Failure MAYBE + Considered Problem: Rules: f6.0(A,B,C,D) -> f7.5(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] f6.0(A,B,C,D) -> f7.6(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && 0 >= 1 + A] f6.1(A,B,C,D) -> f7.5(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] f6.1(A,B,C,D) -> f7.6(A,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A >= 1] f0.2(A,B,C,D) -> f4.4(A,B,C,1 + B) [B >= 0 && C >= B] f4.3(A,B,C,D) -> f6.0(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4.3(A,B,C,D) -> f6.1(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4.3(A,B,C,D) -> f6.7(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B >= 1 + D] f4.4(A,B,C,D) -> f6.0(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f4.4(A,B,C,D) -> f6.1(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f4.4(A,B,C,D) -> f6.7(E,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + B] f7.5(A,B,C,D) -> f4.3(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7.5(A,B,C,D) -> f4.4(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7.5(A,B,C,D) -> f4.8(A,B,C,1 + D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && C >= D] f7.6(A,B,C,D) -> f4.3(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] f7.6(A,B,C,D) -> f4.8(A,B,C,0) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && D >= 1 + C] f6.7(A,B,C,D) -> f14.9(0,B,C,D) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && A = 0] f4.8(A,B,C,D) -> f14.9(A,B,C,B) [1 + C + -1*D >= 0 && C >= 0 && B + C >= 0 && -1*B + C >= 0 && B >= 0 && B = D] f14.9(A,B,C,D) -> exitus616(A,B,C,D) True f14.9(A,B,C,D) -> exitus616(A,B,C,D) True f14.9(A,B,C,D) -> exitus616(A,B,C,D) True f14.9(A,B,C,D) -> exitus616(A,B,C,D) True Signature: {(exitus616,4);(f0.2,4);(f14.9,4);(f4.3,4);(f4.4,4);(f4.8,4);(f6.0,4);(f6.1,4);(f6.7,4);(f7.5,4);(f7.6,4)} Rule Graph: [0->{11,12,13},1->{14,15},2->{11,12,13},3->{14,15},4->{8,9,10},5->{0,1},6->{2,3},7->{16},8->{0,1},9->{2,3} ,10->{16},11->{5,6,7},12->{8,9,10},13->{17},14->{5,6,7},15->{17},16->{18,20},17->{19,21}] + 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] | `- p:[0,5,11,2,6,14,1,8,12,3,9] c: [] MAYBE