YES * Step 1: FromIts YES + Considered Problem: Rules: 0. start(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) -> f2(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) True (1,1) 1. f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1) [B >= 1 + A] (?,1) 2. f2(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) -> f2(A,1 + B,B1*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) [A >= B] (?,1) 3. f10(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) -> 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) [1 + -1*D >= 0 && -1 + D >= 0 && -1 + -1*A + B >= 0 && 0 >= B] (?,1) Signature: {(f1,27);(f10,27);(f2,27);(start,27)} Flow Graph: [0->{1,2},1->{3},2->{1,2},3->{}] + Applied Processor: FromIts + Details: () * Step 2: Decompose YES + Considered Problem: Rules: start(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) -> f2(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) True f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f2(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) -> f2(A,1 + B,B1*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) [A >= B] f10(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) -> 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) [1 + -1*D >= 0 && -1 + D >= 0 && -1 + -1*A + B >= 0 && 0 >= B] Signature: {(f1,27);(f10,27);(f2,27);(start,27)} Rule Graph: [0->{1,2},1->{3},2->{1,2},3->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3] | `- p:[2] c: [2] * Step 3: CloseWith YES + Considered Problem: (Rules: start(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) -> f2(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) True f2(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) -> f10(A,B,C,1,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S ,T,U,V,W,X,Y,Z ,A1) [B >= 1 + A] f2(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) -> f2(A,1 + B,B1*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) [A >= B] f10(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) -> 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) [1 + -1*D >= 0 && -1 + D >= 0 && -1 + -1*A + B >= 0 && 0 >= B] Signature: {(f1,27);(f10,27);(f2,27);(start,27)} Rule Graph: [0->{1,2},1->{3},2->{1,2},3->{}] ,We construct a looptree: P: [0,1,2,3] | `- p:[2] c: [2]) + Applied Processor: CloseWith True + Details: () YES