MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(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. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(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. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(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. f53(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(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. f55(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f58(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. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [0 >= X] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f53(A,B,C,0,X,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [X >= 1] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f45(A,B,2,1 + D,E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) [C = 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,W) -> f45(A,B,C,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,P,Q,R,S,T,U,V,W) [Y >= 1 && B >= 1 + A] (?,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,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f37(A,B,B1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,0,B1,B1,B1,0,W) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W) -> f11(1 + A,B,1,D,E,F,G,Y,X,Z,A1,D,Y,Y,Y,Y,R,R,1,1,1,0,W) [0 >= Y && 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) -> f11(A,B,C,D,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,0) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,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}] + Applied Processor: ArgumentFilter [3,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: [3,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. f11(A,B,C) -> f45(A,B,C) [A >= B] (?,1) 1. f37(A,B,C) -> f45(A,B,C) [C >= 3] (?,1) 2. f37(A,B,C) -> f45(A,B,C) [1 >= C] (?,1) 3. f53(A,B,C) -> f53(A,B,C) True (?,1) 4. f55(A,B,C) -> f58(A,B,C) True (?,1) 5. f45(A,B,C) -> f53(A,B,C) [0 >= X] (?,1) 6. f45(A,B,C) -> f53(A,B,C) [X >= 1] (?,1) 7. f37(A,B,C) -> f45(A,B,2) [C = 2] (?,1) 8. f11(A,B,C) -> f45(A,B,C) [Y >= 1 && B >= 1 + A] (?,1) 9. f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C) -> f11(1 + A,B,1) [0 >= Y && B >= 1 + A] (?,1) 12. f0(A,B,C) -> f11(A,B,C) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,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}] + 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. f11(A,B,C) -> f45(A,B,C) [A >= B] (?,1) 1. f37(A,B,C) -> f45(A,B,C) [C >= 3] (?,1) 2. f37(A,B,C) -> f45(A,B,C) [1 >= C] (?,1) 3. f53(A,B,C) -> f53(A,B,C) True (?,1) 5. f45(A,B,C) -> f53(A,B,C) [0 >= X] (?,1) 6. f45(A,B,C) -> f53(A,B,C) [X >= 1] (?,1) 7. f37(A,B,C) -> f45(A,B,2) [C = 2] (?,1) 8. f11(A,B,C) -> f45(A,B,C) [Y >= 1 && B >= 1 + A] (?,1) 9. f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C) -> f11(1 + A,B,1) [0 >= Y && B >= 1 + A] (?,1) 12. f0(A,B,C) -> f11(A,B,C) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,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}] + 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. f11(A,B,C) -> f45(A,B,C) [A >= B] (?,1) 1. f37(A,B,C) -> f45(A,B,C) [C >= 3] (?,1) 2. f37(A,B,C) -> f45(A,B,C) [1 >= C] (?,1) 3. f53(A,B,C) -> f53(A,B,C) True (?,1) 5. f45(A,B,C) -> f53(A,B,C) [0 >= X] (?,1) 6. f45(A,B,C) -> f53(A,B,C) [X >= 1] (?,1) 7. f37(A,B,C) -> f45(A,B,2) [C = 2] (?,1) 8. f11(A,B,C) -> f45(A,B,C) [Y >= 1 && B >= 1 + A] (?,1) 9. f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] (?,1) 10. f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && 0 >= B1] (?,1) 11. f11(A,B,C) -> f11(1 + A,B,1) [0 >= Y && B >= 1 + A] (?,1) 12. f0(A,B,C) -> f11(A,B,C) True (1,1) Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,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}] + Applied Processor: FromIts + Details: () * Step 5: Unfold MAYBE + Considered Problem: Rules: f11(A,B,C) -> f45(A,B,C) [A >= B] f37(A,B,C) -> f45(A,B,C) [C >= 3] f37(A,B,C) -> f45(A,B,C) [1 >= C] f53(A,B,C) -> f53(A,B,C) True f45(A,B,C) -> f53(A,B,C) [0 >= X] f45(A,B,C) -> f53(A,B,C) [X >= 1] f37(A,B,C) -> f45(A,B,2) [C = 2] f11(A,B,C) -> f45(A,B,C) [Y >= 1 && B >= 1 + A] f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] f11(A,B,C) -> f37(A,B,B1) [B >= 1 + A && 0 >= Y && 0 >= B1] f11(A,B,C) -> f11(1 + A,B,1) [0 >= Y && B >= 1 + A] f0(A,B,C) -> f11(A,B,C) True Signature: {(f0,23);(f11,23);(f37,23);(f45,23);(f53,23);(f55,23);(f58,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}] + Applied Processor: Unfold + Details: () * Step 6: AddSinks MAYBE + Considered Problem: Rules: f11.0(A,B,C) -> f45.5(A,B,C) [A >= B] f11.0(A,B,C) -> f45.6(A,B,C) [A >= B] f37.1(A,B,C) -> f45.5(A,B,C) [C >= 3] f37.1(A,B,C) -> f45.6(A,B,C) [C >= 3] f37.2(A,B,C) -> f45.5(A,B,C) [1 >= C] f37.2(A,B,C) -> f45.6(A,B,C) [1 >= C] f53.3(A,B,C) -> f53.3(A,B,C) True f45.5(A,B,C) -> f53.3(A,B,C) [0 >= X] f45.6(A,B,C) -> f53.3(A,B,C) [X >= 1] f37.7(A,B,C) -> f45.5(A,B,2) [C = 2] f37.7(A,B,C) -> f45.6(A,B,2) [C = 2] f11.8(A,B,C) -> f45.5(A,B,C) [Y >= 1 && B >= 1 + A] f11.8(A,B,C) -> f45.6(A,B,C) [Y >= 1 && B >= 1 + A] f11.9(A,B,C) -> f37.1(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] f11.9(A,B,C) -> f37.7(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] f11.10(A,B,C) -> f37.2(A,B,B1) [B >= 1 + A && 0 >= Y && 0 >= B1] f11.11(A,B,C) -> f11.0(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.8(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.9(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.10(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.11(1 + A,B,1) [0 >= Y && B >= 1 + A] f0.12(A,B,C) -> f11.0(A,B,C) True f0.12(A,B,C) -> f11.8(A,B,C) True f0.12(A,B,C) -> f11.9(A,B,C) True f0.12(A,B,C) -> f11.10(A,B,C) True f0.12(A,B,C) -> f11.11(A,B,C) True Signature: {(f0.12,3) ;(f11.0,3) ;(f11.10,3) ;(f11.11,3) ;(f11.8,3) ;(f11.9,3) ;(f37.1,3) ;(f37.2,3) ;(f37.7,3) ;(f45.5,3) ;(f45.6,3) ;(f53.3,3)} 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}] + Applied Processor: AddSinks + Details: () * Step 7: Failure MAYBE + Considered Problem: Rules: f11.0(A,B,C) -> f45.5(A,B,C) [A >= B] f11.0(A,B,C) -> f45.6(A,B,C) [A >= B] f37.1(A,B,C) -> f45.5(A,B,C) [C >= 3] f37.1(A,B,C) -> f45.6(A,B,C) [C >= 3] f37.2(A,B,C) -> f45.5(A,B,C) [1 >= C] f37.2(A,B,C) -> f45.6(A,B,C) [1 >= C] f53.3(A,B,C) -> f53.3(A,B,C) True f45.5(A,B,C) -> f53.3(A,B,C) [0 >= X] f45.6(A,B,C) -> f53.3(A,B,C) [X >= 1] f37.7(A,B,C) -> f45.5(A,B,2) [C = 2] f37.7(A,B,C) -> f45.6(A,B,2) [C = 2] f11.8(A,B,C) -> f45.5(A,B,C) [Y >= 1 && B >= 1 + A] f11.8(A,B,C) -> f45.6(A,B,C) [Y >= 1 && B >= 1 + A] f11.9(A,B,C) -> f37.1(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] f11.9(A,B,C) -> f37.7(A,B,B1) [B >= 1 + A && 0 >= Y && B1 >= 2] f11.10(A,B,C) -> f37.2(A,B,B1) [B >= 1 + A && 0 >= Y && 0 >= B1] f11.11(A,B,C) -> f11.0(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.8(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.9(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.10(1 + A,B,1) [0 >= Y && B >= 1 + A] f11.11(A,B,C) -> f11.11(1 + A,B,1) [0 >= Y && B >= 1 + A] f0.12(A,B,C) -> f11.0(A,B,C) True f0.12(A,B,C) -> f11.8(A,B,C) True f0.12(A,B,C) -> f11.9(A,B,C) True f0.12(A,B,C) -> f11.10(A,B,C) True f0.12(A,B,C) -> f11.11(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True f53.3(A,B,C) -> exitus616(A,B,C) True Signature: {(exitus616,3) ;(f0.12,3) ;(f11.0,3) ;(f11.10,3) ;(f11.11,3) ;(f11.8,3) ;(f11.9,3) ;(f37.1,3) ;(f37.2,3) ;(f37.7,3) ;(f45.5,3) ;(f45.6,3) ;(f53.3,3)} Rule Graph: [0->{7},1->{8},2->{7},3->{8},4->{7},5->{8},6->{6,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40,41,42,43,44 ,45},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}] + 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] | +- p:[20] c: [20] | `- p:[6] c: [] MAYBE