YES * Step 1: UnsatPaths YES + Considered Problem: Rules: 0. f3(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,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 1. f3(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,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 2. 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [-2 + B >= 0 (?,1) && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] 3. 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [-2 + B >= 0 (?,1) && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] 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,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 6. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 7. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 8. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 9. 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,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && G1 >= 2 && T >= 0 && M = J] Signature: {(f1,32);(f10,32);(f3,32);(f4,32)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8,9},3->{5,6,7,8,9},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9} ,8->{5,6,7,8,9},9->{}] + Applied Processor: UnsatPaths + Details: We remove following edges from the transition graph: [(2,9),(3,9)] * Step 2: FromIts YES + Considered Problem: Rules: 0. f3(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,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1,F1) [J1 >= 2] (1,1) 1. f3(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,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] (1,1) 2. 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [-2 + B >= 0 (?,1) && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] 3. 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I,S1) [-2 + B >= 0 (?,1) && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] 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,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && A >= 1 + B && B >= 0] (?,1) 5. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 6. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 7. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 8. 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 9. 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,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1) [E1 + -1*I >= 0 (?,1) && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && G1 >= 2 && T >= 0 && M = J] Signature: {(f1,32);(f10,32);(f3,32);(f4,32)} Flow Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] + Applied Processor: FromIts + Details: () * Step 3: Decompose YES + Considered Problem: Rules: f3(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,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J ,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1 ,F1) [J1 >= 2] f3(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,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1 ,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1 ,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C ,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I ,S1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C ,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I ,S1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] 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,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J ,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && A >= 1 + B && B >= 0] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L ,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && G1 >= 2 && T >= 0 && M = J] Signature: {(f1,32);(f10,32);(f3,32);(f4,32)} Rule Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] + Applied Processor: Decompose NoGreedy + Details: We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [8] | `- p:[5,6,7] c: [7] | `- p:[5,6] c: [6] | `- p:[5] c: [5] * Step 4: CloseWith YES + Considered Problem: (Rules: f3(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,C1,D1,E1,F1) -> f1(J1,2,K1,L1,K1,F,G,H,I,J ,K,G1,M,G1,J1,P,Q,R,S,T,U,V,W,H1,I1,G1,A1,K1,M1,D1,E1 ,F1) [J1 >= 2] f3(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,C1,D1,E1,F1) -> f4(J1,M1,L1,T1,S1,F,G,H,I,W1 ,K,X,V1,X,I1,X,U1,X1,Q1,T,U,V,W,G1,H1,K1,N1,R1,C1,D1,E1 ,F1) [0 >= O1 && 0 >= I1 && 0 >= P1] 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C ,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I ,S1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && N >= 1 + C && K1 >= 0 && G1 >= 2] 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,C1,D1,E1,F1) -> f10(H1,K1,J1,R1,Q1,F,G,H,I,C ,T,N,N,N,G1,C,C,C,M1,T,U,V,W,X,Y,I1,L1,N1,C1,1 + T,I ,S1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && B >= A && B >= 0 && T1 >= G1 && U1 >= 2 && K1 >= U1 && C >= 1 + N && K1 >= 0 && G1 >= 2] 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,C1,D1,E1,F1) -> f1(A,1 + B,D,G1,D,H1,B,I,I,J ,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [-2 + B >= 0 && -4 + B + O >= 0 && -2 + O >= 0 && A >= 1 + B && B >= 0] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J >= 1 + J1 && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && J1 >= 1 + H1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f10(A,B,C,D,E,F,G,H,I,J,K,M ,M,M,G1,H1,H1,J,S,-1 + T,I1,I,-1 + T,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && J1 >= 1 + J && T >= 0 && H1 >= 1 + J1 && G1 >= 2] 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,B1,C1,D1,E1,F1) -> f4(A,B,C,D,E,F,G,H,I,K1,K,L ,J1,N,G1,P,I1,L1,H1,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1 ,F1) [E1 + -1*I >= 0 && -1*E1 + I >= 0 && 1 + -1*D1 + K >= 0 && -1 + D1 + -1*T >= 0 && -1 + D1 + -1*K >= 0 && K + -1*T >= 0 && -2 + B >= 0 && -4 + B + O >= 0 && J + -1*R >= 0 && -1*J + R >= 0 && -2 + O >= 0 && M + -1*N >= 0 && L + -1*N >= 0 && -1*M + N >= 0 && -1*L + N >= 0 && L + -1*M >= 0 && -1*L + M >= 0 && G1 >= 2 && T >= 0 && M = J] Signature: {(f1,32);(f10,32);(f3,32);(f4,32)} Rule Graph: [0->{2,3,4},1->{},2->{5,6,7,8},3->{5,6,7,8},4->{2,3,4},5->{5,6,7,8,9},6->{5,6,7,8,9},7->{5,6,7,8,9},8->{5 ,6,7,8,9},9->{}] ,We construct a looptree: P: [0,1,2,3,4,5,6,7,8,9] | +- p:[4] c: [4] | `- p:[5,6,7,8] c: [8] | `- p:[5,6,7] c: [7] | `- p:[5,6] c: [6] | `- p:[5] c: [5]) + Applied Processor: CloseWith True + Details: () YES