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