MAYBE * Step 1: ArgumentFilter MAYBE + Considered Problem: Rules: 0. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,C1,D1,E,E,G,G,A,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2] 1. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f1(A,B,C,D,E,F,G,H,I,1 + J,L,C1,L,D1,J,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 2. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f1(A,C1,C,D,E,F,G,H,C1,2,E1,F1,E1,N,O,D1,E1,G1,2,T,U,V,W,X,Y,Z,A1,B1) [C1 >= 2] (1,1) 3. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f9(A,C1,0,D,0,F,G,H,N1,L1,O1,R1,Q1,N,O,M1,P1,R,S,D1,E1,F1,G1,K1,S1,T1,U1,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 4. f1(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f12(A,C1,D1,D,K,F,G,H,G1,F1,K1,N1,M1,N,O,P,L1,R,S,T,U,V,W,X,O1,P1,A1,E1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && C1 >= 2 && E1 >= C1] 5. f12(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f9(A,C1,0,D,0,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,D1,E1,F1,G1,K1,Y,L1,M1,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && N1 >= 2 && O1 >= 2 && A >= 0 && C1 >= 2 && E = 0 && C = 0] 6. f8(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1) -> f9(A,1,K1,D,0,F,G,H,N1,L1,O1,R1,Q1,N,O,M1,P1,R,S,C1,D1,E1,F1,G1,S1,T1,U1,B1) [L = 0] (1,1) Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,5},1->{1,4},2->{1,4},3->{},4->{0,5},5->{},6->{}] + Applied Processor: ArgumentFilter [3,5,6,7,10,12,13,14,15,16,17,19,20,21,22,23,24,25,26] + Details: We remove following argument positions: [3,5,6,7,10,12,13,14,15,16,17,19,20,21,22,23,24,25,26]. * Step 2: TrivialSCCs MAYBE + Considered Problem: Rules: 0. f12(A,B,C,E,I,J,L,S,B1) -> f12(A,C1,D1,E,I,J,L,S,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2] 1. f1(A,B,C,E,I,J,L,S,B1) -> f1(A,B,C,E,I,1 + J,C1,S,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 2. f8(A,B,C,E,I,J,L,S,B1) -> f1(A,C1,C,E,C1,2,F1,2,B1) [C1 >= 2] (1,1) 3. f8(A,B,C,E,I,J,L,S,B1) -> f9(A,C1,0,0,N1,L1,R1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 4. f1(A,B,C,E,I,J,L,S,B1) -> f12(A,C1,D1,K,G1,F1,N1,S,E1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && C1 >= 2 && E1 >= C1] 5. f12(A,B,C,E,I,J,L,S,B1) -> f9(A,C1,0,0,I,J,L,S,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && N1 >= 2 && O1 >= 2 && A >= 0 && C1 >= 2 && E = 0 && C = 0] 6. f8(A,B,C,E,I,J,L,S,B1) -> f9(A,1,K1,0,N1,L1,R1,S,B1) [L = 0] (1,1) Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,5},1->{1,4},2->{1,4},3->{},4->{0,5},5->{},6->{}] + Applied Processor: TrivialSCCs + Details: All trivial SCCs of the transition graph admit timebound 1. * Step 3: AddSinks MAYBE + Considered Problem: Rules: 0. f12(A,B,C,E,I,J,L,S,B1) -> f12(A,C1,D1,E,I,J,L,S,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2] 1. f1(A,B,C,E,I,J,L,S,B1) -> f1(A,B,C,E,I,1 + J,C1,S,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 2. f8(A,B,C,E,I,J,L,S,B1) -> f1(A,C1,C,E,C1,2,F1,2,B1) [C1 >= 2] (1,1) 3. f8(A,B,C,E,I,J,L,S,B1) -> f9(A,C1,0,0,N1,L1,R1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 4. f1(A,B,C,E,I,J,L,S,B1) -> f12(A,C1,D1,K,G1,F1,N1,S,E1) [-2 + I >= 0 (1,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && C1 >= 2 && E1 >= C1] 5. f12(A,B,C,E,I,J,L,S,B1) -> f9(A,C1,0,0,I,J,L,S,B1) [-2 + B1 >= 0 (1,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && N1 >= 2 && O1 >= 2 && A >= 0 && C1 >= 2 && E = 0 && C = 0] 6. f8(A,B,C,E,I,J,L,S,B1) -> f9(A,1,K1,0,N1,L1,R1,S,B1) [L = 0] (1,1) Signature: {(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,5},1->{1,4},2->{1,4},3->{},4->{0,5},5->{},6->{}] + Applied Processor: AddSinks + Details: () * Step 4: Failure MAYBE + Considered Problem: Rules: 0. f12(A,B,C,E,I,J,L,S,B1) -> f12(A,C1,D1,E,I,J,L,S,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && A >= 0 && C1 >= 2] 1. f1(A,B,C,E,I,J,L,S,B1) -> f1(A,B,C,E,I,1 + J,C1,S,B1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && I >= 1 + J && J >= 0] 2. f8(A,B,C,E,I,J,L,S,B1) -> f1(A,C1,C,E,C1,2,F1,2,B1) [C1 >= 2] (1,1) 3. f8(A,B,C,E,I,J,L,S,B1) -> f9(A,C1,0,0,N1,L1,R1,S,B1) [0 >= H1 && 0 >= I1 && 0 >= C1 && 0 >= J1] (1,1) 4. f1(A,B,C,E,I,J,L,S,B1) -> f12(A,C1,D1,K,G1,F1,N1,S,E1) [-2 + I >= 0 (?,1) && -4 + I + S >= 0 && I + -1*S >= 0 && -4 + I + J >= 0 && I + -1*J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && J >= I && J >= 0 && Q1 >= 2 && F1 >= Q1 && F1 >= 0 && C1 >= 2 && E1 >= C1] 5. f12(A,B,C,E,I,J,L,S,B1) -> f9(A,C1,0,0,I,J,L,S,B1) [-2 + B1 >= 0 (?,1) && -4 + B + B1 >= 0 && -4 + B1 + S >= 0 && B1 + -1*S >= 0 && -4 + B1 + J >= 0 && -2 + B >= 0 && -4 + B + S >= 0 && B + -1*S >= 0 && -4 + B + J >= 0 && 2 + -1*S >= 0 && J + -1*S >= 0 && -2 + S >= 0 && -4 + J + S >= 0 && -2 + J >= 0 && N1 >= 2 && O1 >= 2 && A >= 0 && C1 >= 2 && E = 0 && C = 0] 6. f8(A,B,C,E,I,J,L,S,B1) -> f9(A,1,K1,0,N1,L1,R1,S,B1) [L = 0] (1,1) 7. f8(A,B,C,E,I,J,L,S,B1) -> exitus616(A,B,C,E,I,J,L,S,B1) True (1,1) 8. f12(A,B,C,E,I,J,L,S,B1) -> exitus616(A,B,C,E,I,J,L,S,B1) True (?,1) Signature: {(exitus616,9);(f1,28);(f12,28);(f8,28);(f9,28)} Flow Graph: [0->{0,5,8},1->{1,4},2->{1,4},3->{},4->{0,5,8},5->{},6->{},7->{},8->{}] + Applied Processor: LooptreeTransformer + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8] | +- p:[1] c: [1] | `- p:[0] c: [] MAYBE