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) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [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) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [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) -> f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [1 >= C] (?,1) 3. f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) True (?,1) 4. f54(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f57(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) 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) -> f52(A,B,C,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [D >= 1] (?,1) 6. f45(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f52(A,B,C,D,0,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [0 >= D] (?,1) 7. f37(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f45(A,B,2,D,1 + E,F,H,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) [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) -> f45(A,B,C,D,E,F,G,V,W,X,Y,E,V,V,O,P,Q,R,S,T,U) [V >= 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) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && Z >= 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) -> f37(A,B,Z,D,E,F,G,V,W,X,Y,E,V,V,V,Q,0,Z,Z,0,U) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U) -> f13(1 + A,B,1,D,E,F,G,V,W,X,Y,E,V,V,V,Q,Q,1,1,0,U) [0 >= V && 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) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [0 >= W] (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) -> f13(A,B,C,W,E,0,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,0) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} 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] + Details: We remove following argument positions: [4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20]. * Step 2: UnreachableRules MAYBE + Considered Problem: Rules: 0. f13(A,B,C,D) -> f45(A,B,C,D) [A >= B] (?,1) 1. f37(A,B,C,D) -> f45(A,B,C,D) [C >= 3] (?,1) 2. f37(A,B,C,D) -> f45(A,B,C,D) [1 >= C] (?,1) 3. f52(A,B,C,D) -> f52(A,B,C,D) True (?,1) 4. f54(A,B,C,D) -> f57(A,B,C,D) True (?,1) 5. f45(A,B,C,D) -> f52(A,B,C,D) [D >= 1] (?,1) 6. f45(A,B,C,D) -> f52(A,B,C,D) [0 >= D] (?,1) 7. f37(A,B,C,D) -> f45(A,B,2,D) [C = 2] (?,1) 8. f13(A,B,C,D) -> f45(A,B,C,D) [V >= 1 && B >= 1 + A] (?,1) 9. f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] (?,1) 10. f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D) -> f13(1 + A,B,1,D) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D) -> f13(A,B,C,W) [0 >= W] (1,1) 13. f0(A,B,C,D) -> f13(A,B,C,W) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} 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) -> f45(A,B,C,D) [A >= B] (?,1) 1. f37(A,B,C,D) -> f45(A,B,C,D) [C >= 3] (?,1) 2. f37(A,B,C,D) -> f45(A,B,C,D) [1 >= C] (?,1) 3. f52(A,B,C,D) -> f52(A,B,C,D) True (?,1) 5. f45(A,B,C,D) -> f52(A,B,C,D) [D >= 1] (?,1) 6. f45(A,B,C,D) -> f52(A,B,C,D) [0 >= D] (?,1) 7. f37(A,B,C,D) -> f45(A,B,2,D) [C = 2] (?,1) 8. f13(A,B,C,D) -> f45(A,B,C,D) [V >= 1 && B >= 1 + A] (?,1) 9. f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] (?,1) 10. f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D) -> f13(1 + A,B,1,D) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D) -> f13(A,B,C,W) [0 >= W] (1,1) 13. f0(A,B,C,D) -> f13(A,B,C,W) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} 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) -> f45(A,B,C,D) [A >= B] (?,1) 1. f37(A,B,C,D) -> f45(A,B,C,D) [C >= 3] (?,1) 2. f37(A,B,C,D) -> f45(A,B,C,D) [1 >= C] (?,1) 3. f52(A,B,C,D) -> f52(A,B,C,D) True (?,1) 5. f45(A,B,C,D) -> f52(A,B,C,D) [D >= 1] (?,1) 6. f45(A,B,C,D) -> f52(A,B,C,D) [0 >= D] (?,1) 7. f37(A,B,C,D) -> f45(A,B,2,D) [C = 2] (?,1) 8. f13(A,B,C,D) -> f45(A,B,C,D) [V >= 1 && B >= 1 + A] (?,1) 9. f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] (?,1) 10. f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && 0 >= Z] (?,1) 11. f13(A,B,C,D) -> f13(1 + A,B,1,D) [0 >= V && B >= 1 + A] (?,1) 12. f0(A,B,C,D) -> f13(A,B,C,W) [0 >= W] (1,1) 13. f0(A,B,C,D) -> f13(A,B,C,W) [W >= 1] (1,1) Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} 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) -> f45(A,B,C,D) [A >= B] f37(A,B,C,D) -> f45(A,B,C,D) [C >= 3] f37(A,B,C,D) -> f45(A,B,C,D) [1 >= C] f52(A,B,C,D) -> f52(A,B,C,D) True f45(A,B,C,D) -> f52(A,B,C,D) [D >= 1] f45(A,B,C,D) -> f52(A,B,C,D) [0 >= D] f37(A,B,C,D) -> f45(A,B,2,D) [C = 2] f13(A,B,C,D) -> f45(A,B,C,D) [V >= 1 && B >= 1 + A] f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] f13(A,B,C,D) -> f37(A,B,Z,D) [B >= 1 + A && 0 >= V && 0 >= Z] f13(A,B,C,D) -> f13(1 + A,B,1,D) [0 >= V && B >= 1 + A] f0(A,B,C,D) -> f13(A,B,C,W) [0 >= W] f0(A,B,C,D) -> f13(A,B,C,W) [W >= 1] Signature: {(f0,21);(f13,21);(f37,21);(f45,21);(f52,21);(f54,21);(f57,21)} 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) -> f45.5(A,B,C,D) [A >= B] f13.0(A,B,C,D) -> f45.6(A,B,C,D) [A >= B] f37.1(A,B,C,D) -> f45.5(A,B,C,D) [C >= 3] f37.1(A,B,C,D) -> f45.6(A,B,C,D) [C >= 3] f37.2(A,B,C,D) -> f45.5(A,B,C,D) [1 >= C] f37.2(A,B,C,D) -> f45.6(A,B,C,D) [1 >= C] f52.3(A,B,C,D) -> f52.3(A,B,C,D) True f45.5(A,B,C,D) -> f52.3(A,B,C,D) [D >= 1] f45.6(A,B,C,D) -> f52.3(A,B,C,D) [0 >= D] f37.7(A,B,C,D) -> f45.5(A,B,2,D) [C = 2] f37.7(A,B,C,D) -> f45.6(A,B,2,D) [C = 2] f13.8(A,B,C,D) -> f45.5(A,B,C,D) [V >= 1 && B >= 1 + A] f13.8(A,B,C,D) -> f45.6(A,B,C,D) [V >= 1 && B >= 1 + A] f13.9(A,B,C,D) -> f37.1(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] f13.9(A,B,C,D) -> f37.7(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] f13.10(A,B,C,D) -> f37.2(A,B,Z,D) [B >= 1 + A && 0 >= V && 0 >= Z] f13.11(A,B,C,D) -> f13.0(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.8(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.9(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.10(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.11(1 + A,B,1,D) [0 >= V && B >= 1 + A] f0.12(A,B,C,D) -> f13.0(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.8(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.9(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.10(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.11(A,B,C,W) [0 >= W] f0.13(A,B,C,D) -> f13.0(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.8(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.9(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.10(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.11(A,B,C,W) [W >= 1] Signature: {(f0.12,4) ;(f0.13,4) ;(f13.0,4) ;(f13.10,4) ;(f13.11,4) ;(f13.8,4) ;(f13.9,4) ;(f37.1,4) ;(f37.2,4) ;(f37.7,4) ;(f45.5,4) ;(f45.6,4) ;(f52.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) -> f45.5(A,B,C,D) [A >= B] f13.0(A,B,C,D) -> f45.6(A,B,C,D) [A >= B] f37.1(A,B,C,D) -> f45.5(A,B,C,D) [C >= 3] f37.1(A,B,C,D) -> f45.6(A,B,C,D) [C >= 3] f37.2(A,B,C,D) -> f45.5(A,B,C,D) [1 >= C] f37.2(A,B,C,D) -> f45.6(A,B,C,D) [1 >= C] f52.3(A,B,C,D) -> f52.3(A,B,C,D) True f45.5(A,B,C,D) -> f52.3(A,B,C,D) [D >= 1] f45.6(A,B,C,D) -> f52.3(A,B,C,D) [0 >= D] f37.7(A,B,C,D) -> f45.5(A,B,2,D) [C = 2] f37.7(A,B,C,D) -> f45.6(A,B,2,D) [C = 2] f13.8(A,B,C,D) -> f45.5(A,B,C,D) [V >= 1 && B >= 1 + A] f13.8(A,B,C,D) -> f45.6(A,B,C,D) [V >= 1 && B >= 1 + A] f13.9(A,B,C,D) -> f37.1(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] f13.9(A,B,C,D) -> f37.7(A,B,Z,D) [B >= 1 + A && 0 >= V && Z >= 2] f13.10(A,B,C,D) -> f37.2(A,B,Z,D) [B >= 1 + A && 0 >= V && 0 >= Z] f13.11(A,B,C,D) -> f13.0(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.8(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.9(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.10(1 + A,B,1,D) [0 >= V && B >= 1 + A] f13.11(A,B,C,D) -> f13.11(1 + A,B,1,D) [0 >= V && B >= 1 + A] f0.12(A,B,C,D) -> f13.0(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.8(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.9(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.10(A,B,C,W) [0 >= W] f0.12(A,B,C,D) -> f13.11(A,B,C,W) [0 >= W] f0.13(A,B,C,D) -> f13.0(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.8(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.9(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.10(A,B,C,W) [W >= 1] f0.13(A,B,C,D) -> f13.11(A,B,C,W) [W >= 1] f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.3(A,B,C,D) -> exitus616(A,B,C,D) True f52.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) ;(f37.1,4) ;(f37.2,4) ;(f37.7,4) ;(f45.5,4) ;(f45.6,4) ;(f52.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