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