MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 1. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f56(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) True (?,1) 2. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [A >= B] (?,1) 3. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E >= 3] (?,1) 4. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [1 >= E] (?,1) 5. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,2,G,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) [E = 2] (?,1) 6. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f51(A,B,0,0,E,F,W,X,Y,Z,D,W,W,W,O,P,Q,R,S,T,U,V) [W >= 1 && B >= 1 + A] (?,1) 7. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1) 8. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f37(A,B,C,D,A1,F,W,X,Y,Z,D,W,W,W,W,Q,0,A1,A1,A1,0,V) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1) 9. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(1 + A,B,C,D,1,F,W,X,Y,Z,D,W,W,W,W,Q,Q,1,1,1,0,V) [0 >= W && B >= 1 + A] (?,1) 10. f0(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V) -> f11(A,B,0,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0) True (1,1) Signature: {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)} Flow Graph: [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: ArgumentFilter [2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21] + Details: We remove following argument positions: [2,3,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21]. * Step 2: UnreachableRules MAYBE + Considered Problem: Rules: 0. f51(A,B,E) -> f51(A,B,E) True (?,1) 1. f53(A,B,E) -> f56(A,B,E) True (?,1) 2. f11(A,B,E) -> f51(A,B,E) [A >= B] (?,1) 3. f37(A,B,E) -> f51(A,B,E) [E >= 3] (?,1) 4. f37(A,B,E) -> f51(A,B,E) [1 >= E] (?,1) 5. f37(A,B,E) -> f51(A,B,2) [E = 2] (?,1) 6. f11(A,B,E) -> f51(A,B,E) [W >= 1 && B >= 1 + A] (?,1) 7. f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1) 8. f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1) 9. f11(A,B,E) -> f11(1 + A,B,1) [0 >= W && B >= 1 + A] (?,1) 10. f0(A,B,E) -> f11(A,B,E) True (1,1) Signature: {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)} Flow Graph: [0->{0},1->{},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: UnreachableRules + Details: Following transitions are not reachable from the starting states and are revomed: [1] * Step 3: UnsatPaths MAYBE + Considered Problem: Rules: 0. f51(A,B,E) -> f51(A,B,E) True (?,1) 2. f11(A,B,E) -> f51(A,B,E) [A >= B] (?,1) 3. f37(A,B,E) -> f51(A,B,E) [E >= 3] (?,1) 4. f37(A,B,E) -> f51(A,B,E) [1 >= E] (?,1) 5. f37(A,B,E) -> f51(A,B,2) [E = 2] (?,1) 6. f11(A,B,E) -> f51(A,B,E) [W >= 1 && B >= 1 + A] (?,1) 7. f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1) 8. f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1) 9. f11(A,B,E) -> f11(1 + A,B,1) [0 >= W && B >= 1 + A] (?,1) 10. f0(A,B,E) -> f11(A,B,E) True (1,1) Signature: {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)} Flow Graph: [0->{0},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,4,5},8->{3,4,5},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(7,4),(8,3),(8,5)] * Step 4: FromIts MAYBE + Considered Problem: Rules: 0. f51(A,B,E) -> f51(A,B,E) True (?,1) 2. f11(A,B,E) -> f51(A,B,E) [A >= B] (?,1) 3. f37(A,B,E) -> f51(A,B,E) [E >= 3] (?,1) 4. f37(A,B,E) -> f51(A,B,E) [1 >= E] (?,1) 5. f37(A,B,E) -> f51(A,B,2) [E = 2] (?,1) 6. f11(A,B,E) -> f51(A,B,E) [W >= 1 && B >= 1 + A] (?,1) 7. f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] (?,1) 8. f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && 0 >= A1] (?,1) 9. f11(A,B,E) -> f11(1 + A,B,1) [0 >= W && B >= 1 + A] (?,1) 10. f0(A,B,E) -> f11(A,B,E) True (1,1) Signature: {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)} Flow Graph: [0->{0},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: FromIts + Details: () * Step 5: Unfold MAYBE + Considered Problem: Rules: f51(A,B,E) -> f51(A,B,E) True f11(A,B,E) -> f51(A,B,E) [A >= B] f37(A,B,E) -> f51(A,B,E) [E >= 3] f37(A,B,E) -> f51(A,B,E) [1 >= E] f37(A,B,E) -> f51(A,B,2) [E = 2] f11(A,B,E) -> f51(A,B,E) [W >= 1 && B >= 1 + A] f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] f11(A,B,E) -> f37(A,B,A1) [B >= 1 + A && 0 >= W && 0 >= A1] f11(A,B,E) -> f11(1 + A,B,1) [0 >= W && B >= 1 + A] f0(A,B,E) -> f11(A,B,E) True Signature: {(f0,22);(f11,22);(f37,22);(f51,22);(f53,22);(f56,22)} Rule Graph: [0->{0},2->{0},3->{0},4->{0},5->{0},6->{0},7->{3,5},8->{4},9->{2,6,7,8,9},10->{2,6,7,8,9}] + Applied Processor: Unfold + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f51.0(A,B,E) -> f51.0(A,B,E) True f11.2(A,B,E) -> f51.0(A,B,E) [A >= B] f37.3(A,B,E) -> f51.0(A,B,E) [E >= 3] f37.4(A,B,E) -> f51.0(A,B,E) [1 >= E] f37.5(A,B,E) -> f51.0(A,B,2) [E = 2] f11.6(A,B,E) -> f51.0(A,B,E) [W >= 1 && B >= 1 + A] f11.7(A,B,E) -> f37.3(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] f11.7(A,B,E) -> f37.5(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] f11.8(A,B,E) -> f37.4(A,B,A1) [B >= 1 + A && 0 >= W && 0 >= A1] f11.9(A,B,E) -> f11.2(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.6(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.7(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.8(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.9(1 + A,B,1) [0 >= W && B >= 1 + A] f0.10(A,B,E) -> f11.2(A,B,E) True f0.10(A,B,E) -> f11.6(A,B,E) True f0.10(A,B,E) -> f11.7(A,B,E) True f0.10(A,B,E) -> f11.8(A,B,E) True f0.10(A,B,E) -> f11.9(A,B,E) True Signature: {(f0.10,3);(f11.2,3);(f11.6,3);(f11.7,3);(f11.8,3);(f11.9,3);(f37.3,3);(f37.4,3);(f37.5,3);(f51.0,3)} Rule Graph: [0->{0},1->{0},2->{0},3->{0},4->{0},5->{0},6->{2},7->{4},8->{3},9->{1},10->{5},11->{6,7},12->{8},13->{9,10 ,11,12,13},14->{1},15->{5},16->{6,7},17->{8},18->{9,10,11,12,13}] + Applied Processor: AddSinks + Details: () * Step 7: Failure MAYBE + Considered Problem: Rules: f51.0(A,B,E) -> f51.0(A,B,E) True f11.2(A,B,E) -> f51.0(A,B,E) [A >= B] f37.3(A,B,E) -> f51.0(A,B,E) [E >= 3] f37.4(A,B,E) -> f51.0(A,B,E) [1 >= E] f37.5(A,B,E) -> f51.0(A,B,2) [E = 2] f11.6(A,B,E) -> f51.0(A,B,E) [W >= 1 && B >= 1 + A] f11.7(A,B,E) -> f37.3(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] f11.7(A,B,E) -> f37.5(A,B,A1) [B >= 1 + A && 0 >= W && A1 >= 2] f11.8(A,B,E) -> f37.4(A,B,A1) [B >= 1 + A && 0 >= W && 0 >= A1] f11.9(A,B,E) -> f11.2(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.6(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.7(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.8(1 + A,B,1) [0 >= W && B >= 1 + A] f11.9(A,B,E) -> f11.9(1 + A,B,1) [0 >= W && B >= 1 + A] f0.10(A,B,E) -> f11.2(A,B,E) True f0.10(A,B,E) -> f11.6(A,B,E) True f0.10(A,B,E) -> f11.7(A,B,E) True f0.10(A,B,E) -> f11.8(A,B,E) True f0.10(A,B,E) -> f11.9(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True f51.0(A,B,E) -> exitus616(A,B,E) True Signature: {(exitus616,3) ;(f0.10,3) ;(f11.2,3) ;(f11.6,3) ;(f11.7,3) ;(f11.8,3) ;(f11.9,3) ;(f37.3,3) ;(f37.4,3) ;(f37.5,3) ;(f51.0,3)} Rule Graph: [0->{0,19,20,21,22,23,24,25,26,27,28},1->{0},2->{0},3->{0},4->{0},5->{0},6->{2},7->{4},8->{3},9->{1} ,10->{5},11->{6,7},12->{8},13->{9,10,11,12,13},14->{1},15->{5},16->{6,7},17->{8},18->{9,10,11,12,13}] + 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] | +- p:[13] c: [13] | `- p:[0] c: [] MAYBE