(GOAL COMPLEXITY) (STARTTERM (FUNCTIONSYMBOLS f2)) (VAR 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 G1 H1 I1 J1 K1 L1 M1 N1 O1 P1 Q1 R1 S1 T1 U1 V1 W1 X1 Y1 Z1 A2 B2 C2 D2 E2 F2 G2 H2 I2 J2 K2 L2 M2 N2 O2 P2 Q2 R2 S2 T2 U2 V2 W2 X2 Y2 Z2 A3) (RULES f44(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f73(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= 2 + B f44(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f73(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B >= A f73(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f75(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 29 >= C f73(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f75(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C >= 31 f75(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f77(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 9 >= C f75(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f77(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C >= 11 f144(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f148(A,B,C,0,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: D = 0 f152(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 0 >= E + 1 f152(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: E >= 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,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f4(A,B,C,D,E,0,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) f4(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: G >= H f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f7(A,B,C,D,E,F + B2,G,H,I + 1,B2,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: G >= I f18(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f23(A,B,0,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= 1 f23(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f34(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 1 >= B f23(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f31(A,B,C,D,B2 + C2,F,G,H,I,J,B2,C2,D2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 0 >= 1 + B2 + C2 && B >= 2 f23(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f31(A,B,C,D,B2 + C2,F,G,H,I,J,B2,C2,D2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B2 + C2 >= 1 && B >= 2 f23(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f31(A,B,C,D,F,F,G,H,I,J,-B2,B2,C2,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B >= 2 f31(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f34(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) f31(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f23(A,B - 1,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 0 >= M + 1 f31(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f23(A,B - 1,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: M >= 1 f34(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f41(A - 1,A,C,B2,E,F,G,H,I,J,K,L,M,A,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A = B f34(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f44(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,D2*E2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= B + 1 f34(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f44(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,D2*E2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B >= 1 + A f44(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f61(A,A - 1,C,D + Q,E,F,G,H,I,2*O - 2*D,K,L,M,N,O,P,Q,2*O - 2*D,4*O*O - 8*D*O + 4*D*D + P,B2,C2,2*O - 2*D + D2,D2,D2,-D + Q + 2*O + D2,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 4*O*O + 4*D*D + P >= 8*D*O && 2*O >= 2*D && B + 1 = A f44(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f61(A,A - 1,C,D + Q,E,F,G,H,I,2*O - 2*D,K,L,M,N,O,P,Q,2*O - 2*D,4*O*O - 8*D*O + 4*D*D + P,B2,C2,2*O - 2*D - D2,W,-D2,-D + Q + 2*O - D2,D2,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 4*O*O + 4*D*D + P >= 8*D*O && 2*D >= 2*O + 1 && B + 1 = A f61(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f41(A - 2,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,R,S,T,U,0,W,X,Y,Z,0,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: V = 0 f61(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f41(A - 2,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,0,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 0 >= V + 1 f61(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f41(A - 2,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,0,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: V >= 1 f44(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f41(A - 2,A - 1,C,D + Q,E,F,G,H,I,B2,K,L,M,N,O,P,Q,2*O - 2*D,4*O*O - 8*D*O + 4*D*D + P,C2,B2,B2,W,X,Y,Z,A1,-D + Q + 2*O,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 8*D*O >= 1 + 4*O*O + 4*D*D + P && B + 1 = A f73(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f75(A,B,30,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C = 30 f77(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f80(A,B,20,D,E,F,G,H,I,J,K,L,M,N,O,P,Q + D,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C = 20 f75(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f80(A,B,10,D,E,F,G,H,I,J,K,L,M,N,O,P,Q + D,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C = 10 f80(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f80(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= H f77(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f93(A,B,C + 1,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 19 >= C f77(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f93(A,B,C + 1,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C >= 21 f93(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f119(A,B,C,D,B2 + C2 + D2,F,G,H,I,J,K,L,M,N,O,P,Q,E2,S2,T,U,J2,W,X,Y,Z,A1,B1,C1,H2,B2,C2,D2,U2,V2,W2,U2*V2 + U2*W2,X2,Y2,Z2,A3,X2*Y2 + X2*Z2 + X2*A3,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B >= C1 + 1 && C1 >= B && F2 >= B2*G2 + C2*G2 + D2*G2 && B2*G2 + C2*G2 + D2*G2 + G2 >= F2 + 1 && G2 >= H2 && F2 >= B2*I2 + C2*I2 + D2*I2 && B2*I2 + C2*I2 + D2*I2 + I2 >= F2 + 1 && H2 >= I2 && D*O + J2*J2 >= D*J2 + O*J2 + P + K2*L2 && K2*L2 + L2 + D*J2 + O*J2 + P >= D*O + J2*J2 + 1 && L2 + M2 >= B2*N2 + C2*N2 + D2*N2 && B2*N2 + C2*N2 + D2*N2 + N2 >= L2 + M2 + 1 && N2 >= E2 && D*O + J2*J2 >= D*J2 + O*J2 + P + K2*O2 && K2*O2 + O2 + D*J2 + O*J2 + P >= D*O + J2*J2 + 1 && O2 + M2 >= B2*P2 + C2*P2 + D2*P2 && B2*P2 + C2*P2 + D2*P2 + P2 >= O2 + M2 + 1 && E2 >= P2 && Q2 + J2 >= D + O + B2*R2 + C2*R2 + D2*R2 && B2*R2 + C2*R2 + D2*R2 + R2 + D + O >= Q2 + J2 + 1 && R2 >= S2 && Q2 + J2 >= D + O + B2*T2 + C2*T2 + D2*T2 && B2*T2 + C2*T2 + D2*T2 + T2 + D + O >= Q2 + J2 + 1 && S2 >= T2 f93(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f119(A,B,C,D,B2 + C2 + D2,F,G,H,I,J,K,L,M,N,O,P,Q,E2,S2,T,U,J2,W,X,Y,Z,A1,B1,C1,H2,B2,C2,D2,U2,V2,W2,U2*V2 + U2*W2,X2,Y2,Z2,A3,X2*Y2 + X2*Z2 + X2*A3,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: F2 >= B2*G2 + C2*G2 + D2*G2 && B2*G2 + C2*G2 + D2*G2 + G2 >= F2 + 1 && G2 >= H2 && F2 >= B2*I2 + C2*I2 + D2*I2 && B2*I2 + C2*I2 + D2*I2 + I2 >= F2 + 1 && H2 >= I2 && K2 + J2 >= D + O + B2*L2 + C2*L2 + D2*L2 && B2*L2 + C2*L2 + D2*L2 + L2 + D + O >= K2 + J2 + 1 && L2 >= S2 && K2 + J2 >= D + O + B2*N2 + C2*N2 + D2*N2 && B2*N2 + C2*N2 + D2*N2 + N2 + D + O >= K2 + J2 + 1 && S2 >= N2 && D*O + J2*J2 >= D*J2 + O*J2 + P + M2*O2 && M2*O2 + M2 + D*J2 + O*J2 + P >= D*O + J2*J2 + 1 && M2 + R2 >= B2*P2 + C2*P2 + D2*P2 && B2*P2 + C2*P2 + D2*P2 + P2 >= M2 + R2 + 1 && P2 >= E2 && D*O + J2*J2 >= D*J2 + O*J2 + P + O2*Q2 && O2*Q2 + Q2 + D*J2 + O*J2 + P >= D*O + J2*J2 + 1 && Q2 + R2 >= B2*T2 + C2*T2 + D2*T2 && B2*T2 + C2*T2 + D2*T2 + T2 >= Q2 + R2 + 1 && E2 >= T2 && C1 >= 1 + B f119(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f93(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 - 1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 0 >= K1 + 1 f119(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f93(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 - 1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: K1 >= 1 f124(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f124(A,B,C,D,E,F,G,C1 + 3,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= C1 + 2 && H = C1 + 2 f124(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f124(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C1 + 1 >= H && A >= H f124(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f124(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: H >= 3 + C1 && A >= H f132(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f148(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,C1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= 1 + Q1 && C1 = Q1 f132(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,B2,C2,T,U,V,W,X,Y,Z,A1,B1,C1,0,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C1 >= Q1 + 1 && A >= 1 + Q1 f132(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f138(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,B2,C2,T,U,V,W,X,Y,Z,A1,B1,C1,0,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= 1 + C1 && A >= 1 + Q1 f138(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f144(A,B,C,B2 + C2 + D2,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,A - 1,B2,C2,D2,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 + 1 = A f138(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f144(A,B,C,B2 + C2 + D2,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,E2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,B2,C2,D2,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= 2 + Q1 f138(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f144(A,B,C,B2 + C2 + D2,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,E2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,B2,C2,D2,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= A f144(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f148(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,B2,C2,T,U,V,W,X,Y,Z,A1,B1,C1,D2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: D1 >= D*E2 && D*E2 + E2 >= D1 + 1 && E2 >= D2 && D1 >= D*S2 && D*S2 + S2 >= D1 + 1 && D2 >= S2 && S >= D*J2 && D*J2 + J2 >= S + 1 && J2 >= C2 && S >= D*H2 && D*H2 + H2 >= S + 1 && C2 >= H2 && 0 >= D + 1 && R >= D*U2 && D*U2 + U2 >= R + 1 && U2 >= B2 && R >= D*V2 && D*V2 + V2 >= R + 1 && B2 >= V2 f144(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f148(A,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,Q,B2,C2,T,U,V,W,X,Y,Z,A1,B1,C1,D2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: D1 >= D*E2 && D*E2 + E2 >= D1 + 1 && E2 >= D2 && D1 >= D*S2 && D*S2 + S2 >= D1 + 1 && D2 >= S2 && S >= D*J2 && D*J2 + J2 >= S + 1 && J2 >= C2 && S >= D*H2 && D*H2 + H2 >= S + 1 && C2 >= H2 && D >= 1 && R >= D*U2 && D*U2 + U2 >= R + 1 && U2 >= B2 && R >= D*V2 && D*V2 + V2 >= R + 1 && B2 >= V2 f148(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f152(A,B,C,D,B2,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,C2,B2,W1,X1,Y1,Z1,A2)) :|: R >= 0 f148(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f152(A,B,C,D,-B2,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,C2,B2,Y1,Z1,A2)) :|: 0 >= R + 1 f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,P,Q,R + E,D2,T,U,E2,W,X,Y,Z,A1,B1,B,S2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,B,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: D1 >= R*J2 + E*J2 && R*J2 + E*J2 + J2 >= D1 + 1 && J2 >= S2 && D1 >= R*H2 + E*H2 && R*H2 + E*H2 + H2 >= D1 + 1 && S2 >= H2 && D1 >= E*U2 && E*U2 + U2 >= D1 + 1 && U2 >= E2 && D1 >= E*V2 && E*V2 + V2 >= D1 + 1 && E2 >= V2 && S >= R*W2 + E*W2 && R*W2 + E*W2 + W2 >= S + 1 && W2 >= D2 && S >= R*X2 + E*X2 && R*X2 + E*X2 + X2 >= S + 1 && D2 >= X2 && R + E >= E*Y2 && E*Y2 + Y2 >= R + E + 1 && Y2 >= B2 && R + E >= E*Z2 && E*Z2 + Z2 >= R + E + 1 && B2 >= Z2 && S >= E*A3 && E*A3 + A3 >= S + 1 && A3 >= C2 && S >= E*G2 && E*G2 + G2 >= S + 1 && C2 >= G2 && B = Q1 && C1 = Q1 f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,P,Q,R + E,D2,T,U,E2,W,X,Y,Z,A1,B1,C1,S2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,C1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= B + 1 && D1 >= R*J2 + E*J2 && R*J2 + E*J2 + J2 >= D1 + 1 && J2 >= S2 && D1 >= R*H2 + E*H2 && R*H2 + E*H2 + H2 >= D1 + 1 && S2 >= H2 && D1 >= E*U2 && E*U2 + U2 >= D1 + 1 && U2 >= E2 && D1 >= E*V2 && E*V2 + V2 >= D1 + 1 && E2 >= V2 && S >= R*W2 + E*W2 && R*W2 + E*W2 + W2 >= S + 1 && W2 >= D2 && S >= R*X2 + E*X2 && R*X2 + E*X2 + X2 >= S + 1 && D2 >= X2 && R + E >= E*Y2 && E*Y2 + Y2 >= R + E + 1 && Y2 >= B2 && R + E >= E*Z2 && E*Z2 + Z2 >= R + E + 1 && B2 >= Z2 && S >= E*A3 && E*A3 + A3 >= S + 1 && A3 >= C2 && S >= E*G2 && E*G2 + G2 >= S + 1 && C2 >= G2 && C1 = Q1 f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,P,Q,R + E,D2,T,U,E2,W,X,Y,Z,A1,B1,C1,S2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,C1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B >= 1 + Q1 && D1 >= R*J2 + E*J2 && R*J2 + E*J2 + J2 >= D1 + 1 && J2 >= S2 && D1 >= R*H2 + E*H2 && R*H2 + E*H2 + H2 >= D1 + 1 && S2 >= H2 && D1 >= E*U2 && E*U2 + U2 >= D1 + 1 && U2 >= E2 && D1 >= E*V2 && E*V2 + V2 >= D1 + 1 && E2 >= V2 && S >= R*W2 + E*W2 && R*W2 + E*W2 + W2 >= S + 1 && W2 >= D2 && S >= R*X2 + E*X2 && R*X2 + E*X2 + X2 >= S + 1 && D2 >= X2 && R + E >= E*Y2 && E*Y2 + Y2 >= R + E + 1 && Y2 >= B2 && R + E >= E*Z2 && E*Z2 + Z2 >= R + E + 1 && B2 >= Z2 && S >= E*A3 && E*A3 + A3 >= S + 1 && A3 >= C2 && S >= E*G2 && E*G2 + G2 >= S + 1 && C2 >= G2 && C1 = Q1 f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,P,Q,R + E,D2,T,U,E2,W,X,Y,Z,A1,B1,C1,S2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C1 >= Q1 + 1 && D1 >= R*J2 + E*J2 && R*J2 + E*J2 + J2 >= D1 + 1 && J2 >= S2 && D1 >= R*H2 + E*H2 && R*H2 + E*H2 + H2 >= D1 + 1 && S2 >= H2 && D1 >= E*U2 && E*U2 + U2 >= D1 + 1 && U2 >= E2 && D1 >= E*V2 && E*V2 + V2 >= D1 + 1 && E2 >= V2 && S >= R*W2 + E*W2 && R*W2 + E*W2 + W2 >= S + 1 && W2 >= D2 && S >= R*X2 + E*X2 && R*X2 + E*X2 + X2 >= S + 1 && D2 >= X2 && R + E >= E*Y2 && E*Y2 + Y2 >= R + E + 1 && Y2 >= B2 && R + E >= E*Z2 && E*Z2 + Z2 >= R + E + 1 && B2 >= Z2 && S >= E*A3 && E*A3 + A3 >= S + 1 && A3 >= C2 && S >= E*G2 && E*G2 + G2 >= S + 1 && C2 >= G2 f156(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,B2,E,F,G,H,I,J,K,L,M,N,C2,P,Q,R + E,D2,T,U,E2,W,X,Y,Z,A1,B1,C1,S2,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= 1 + C1 && D1 >= R*J2 + E*J2 && R*J2 + E*J2 + J2 >= D1 + 1 && J2 >= S2 && D1 >= R*H2 + E*H2 && R*H2 + E*H2 + H2 >= D1 + 1 && S2 >= H2 && D1 >= E*U2 && E*U2 + U2 >= D1 + 1 && U2 >= E2 && D1 >= E*V2 && E*V2 + V2 >= D1 + 1 && E2 >= V2 && S >= R*W2 + E*W2 && R*W2 + E*W2 + W2 >= S + 1 && W2 >= D2 && S >= R*X2 + E*X2 && R*X2 + E*X2 + X2 >= S + 1 && D2 >= X2 && R + E >= E*Y2 && E*Y2 + Y2 >= R + E + 1 && Y2 >= B2 && R + E >= E*Z2 && E*Z2 + Z2 >= R + E + 1 && B2 >= Z2 && S >= E*A3 && E*A3 + A3 >= S + 1 && A3 >= C2 && S >= E*G2 && E*G2 + G2 >= S + 1 && C2 >= G2 f167(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,D,E,F,G,H,I + 1,J,K,L,M,N,O,P,Q,B2 + S*C2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,A - 1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= I && Q1 + 1 = A f167(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,D,E,F,G,H,I + 1,J,K,L,M,N,O,P,Q,B2 + S*C2 + D1*D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= 2 + Q1 && A >= I f167(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f167(A,B,C,D,E,F,G,H,I + 1,J,K,L,M,N,O,P,Q,B2 + S*C2 + D1*D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= A && A >= I f181(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f181(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,D*B2 + O*C2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,A - 1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Y1 >= H && Q1 + 1 = A f181(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f181(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,D*B2 + O*C2 + V*D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: A >= 2 + Q1 && Y1 >= H f181(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f181(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,D*B2 + O*C2 + V*D2,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= A && Y1 >= H f152(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f132(A,B,C,D,0,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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 + 1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: E = 0 f41(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f23(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 30 >= C && A >= 2 + B f41(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f18(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: C >= 31 && A >= 2 + B f41(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f18(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B + 1 >= A f181(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f132(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1 + 1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: H >= 1 + Y1 f167(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f181(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,A,Z1,A2)) :|: I >= 1 + A && Q1 + 2 >= A f167(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f181(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Q1 + 3,Z1,A2)) :|: I >= 1 + A && A >= Q1 + 3 f132(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f41(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: Q1 >= A f124(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f132(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: H >= 1 + A f93(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f124(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: B >= C1 + 1 f93(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f124(A,B,C,D,B2 + C2 + D2,F,G,H,I,J,K,L,M,N,O,P,Q,E2,S2,T,U,J2,W,X,Y,Z,A1,B1,B,H2,B2,C2,D2,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: V2 >= B2*U2 + C2*U2 + D2*U2 && B2*U2 + C2*U2 + D2*U2 + U2 >= V2 + 1 && U2 >= H2 && V2 >= B2*W2 + C2*W2 + D2*W2 && B2*W2 + C2*W2 + D2*W2 + W2 >= V2 + 1 && H2 >= W2 && D*O + J2*J2 >= D*J2 + O*J2 + P + X2*Y2 && X2*Y2 + X2 + D*J2 + O*J2 + P >= D*O + J2*J2 + 1 && X2 + A3 >= B2*Z2 + C2*Z2 + D2*Z2 && B2*Z2 + C2*Z2 + D2*Z2 + Z2 >= X2 + A3 + 1 && Z2 >= E2 && D*O + J2*J2 >= D*J2 + O*J2 + P + G2*Y2 && G2*Y2 + G2 + D*J2 + O*J2 + P >= D*O + J2*J2 + 1 && G2 + A3 >= B2*F2 + C2*F2 + D2*F2 && B2*F2 + C2*F2 + D2*F2 + F2 >= G2 + A3 + 1 && E2 >= F2 && L2 + J2 >= D + O + B2*I2 + C2*I2 + D2*I2 && B2*I2 + C2*I2 + D2*I2 + I2 + D + O >= L2 + J2 + 1 && I2 >= S2 && L2 + J2 >= D + O + B2*K2 + C2*K2 + D2*K2 && B2*K2 + C2*K2 + D2*K2 + K2 + D + O >= L2 + J2 + 1 && S2 >= K2 && B = C1 f119(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f124(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) f80(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f93(A,B,C + 1,3*B2,4*B2,F,G,H,I,B2,K,L,M,N,3*B2,D2,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,-C2 + 4*B2,C2)) :|: H >= 1 + A f18(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_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,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: 0 >= A f7(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f4(A,B,C,D,E,F,G,H + 1,I,J,K,L,M,N,O,P,Q,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: I >= 1 + G f4(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,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2) -> Com_1(f18(G,B,C,D,E,F,G,H,I,J,K,L,M,N,O,P,0,R,S,T,U,V,W,X,Y,Z,A1,B1,C1,D1,E1,F1,G1,H1,I1,J1,K1,L1,M1,N1,O1,P1,Q1,R1,S1,T1,U1,V1,W1,X1,Y1,Z1,A2)) :|: H >= 1 + G )