stateNumbers(200). initialConstraints( param(P1,P2,P3), [ -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000, 0*P1 + 0*P2 + 1*P3 < 5050000 ] ). trans( statevar(X1,X2,X3,X4), param(P1,P2,P3), [ ( X1= 1 /\ X2= 1 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 1, [( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 1, [( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 1, [( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 1, [( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 1, [( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 1, [( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 1, [( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 1, [( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 1, [( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 1 /\ X4= 1, [( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 1, [] ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 1, [( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 1, [( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 1, [( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, [( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, [( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 1, [( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, [( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 1, [( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 1, [( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 1, [( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 1, [( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 1, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 1, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, [( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 1, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 1, [( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 1, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 1, [( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, [( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, [( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 1, [( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 1, [] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 1, [( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 1, [( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 1, [( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 1, [( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 1, [( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 1, [] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 4 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 1, [( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 1, [( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 1, [( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 1, [( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 1, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, [( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, [( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 1, [( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 1, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 1, [( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 1 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, [( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 1, [( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 1, [( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 1, [( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 1, [] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 4 /\ X4= 1, [( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 1 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 1, [( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 1, [( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 1, [( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 1, [( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 1, [] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 4 /\ X4= 1, [( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 1, [( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 1, [( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 1, [( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 4 /\ X4= 1, [( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 1, [] ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 1, [] ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 1, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 2, [( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 2, [( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 2, [( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 2, [( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 2, [( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 2, [( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 2, [( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 1 /\ X4= 2, [( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 2, [] ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 2, [( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 2, [( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 2, [( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 2, [( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 2, [( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 2, [( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 2, [( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 2, [( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 3 /\ X4= 2, [( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 2, [( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 2, [( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 2, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 2, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 2, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 2, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 2, [( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 2, [0*P1 + 0*P2 + -1*P3 < -4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + 1*P3 < 5050000] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 2, [( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, [( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 2, [( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 2, [( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 2, [( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 2, [( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 2, [( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 2, [( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 2, [( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 1 /\ X3= 4 /\ X4= 2, [( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 2, [( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 2, [( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 2, [( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 2, [( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 2, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 2, [( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 2, [( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, [( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 2, [( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 2, [0*P1 + 0*P2 + 1*P3 < 4192265, -1*P1 + 0*P2 + 0*P3 < -840000, 1*P1 + 0*P2 + 0*P3 < 850000, 0*P1 + -1*P2 + 0*P3 < -365000, 0*P1 + 1*P2 + 0*P3 < 370000, 0*P1 + 0*P2 + -1*P3 < -4000000] ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 2, [( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ), ( X1= 1 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 2, [( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 2, [( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 2, [( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 2, [( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 4 /\ X3= 4 /\ X4= 2, [( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ), ( X1= 1 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 2, [( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 2, [( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 2, [( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 2, [( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 1 /\ X2= 5 /\ X3= 4 /\ X4= 2, [( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 2, [( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 2, [( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 2, [( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ), ( X1= 5 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ), ( X1= 5 /\ X2= 5 /\ X3= 4 /\ X4= 2, [( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 2, [] ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 2, [] ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 2, [] ) ] ) ] ). self_loop( statevar(X1,X2,X3,X4), param(P1,P2,P3), [ ( X1= 1 /\ X2= 1 /\ X3= 1 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 1 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 1 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 4 /\ X3= 1 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 5 /\ X3= 1 /\ X4= 1, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 5 /\ X3= 1 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 1 /\ X3= 2 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 1, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 1 /\ X3= 3 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ P3<4192265 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 1, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 1 /\ X2= 1 /\ X3= 4 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ P3>4192265 ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3>4192265 ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3>4192265 ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3>4192265 ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3>4192265 ), ( X1= 1 /\ X2= 4 /\ X3= 4 /\ X4= 1, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 1 /\ X2= 5 /\ X3= 4 /\ X4= 1, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 5 /\ X2= 5 /\ X3= 4 /\ X4= 1, 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 1 /\ X2= 1 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 3 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 3 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 3 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 3 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 4 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 4 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 4 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 4 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 4 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 5 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 5 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 5 /\ X3= 1 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 5 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 5 /\ X3= 1 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 1 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 3 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 3 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 3 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 3 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 4 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 4 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 4 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 4 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 4 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 5 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 5 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 5 /\ X3= 2 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 5 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 5 /\ X3= 2 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 1 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3<4192265 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ P3<4192265 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 3 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 3 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 3 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 3 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 4 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 4 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 4 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 4 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 4 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 5 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 2 /\ X2= 5 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 3 /\ X2= 5 /\ X3= 3 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 4 /\ X2= 5 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 5 /\ X2= 5 /\ X3= 3 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 1 /\ X2= 1 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 1 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 1 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 1 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 1 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 2 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 2 /\ X2= 2 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 3 /\ X2= 2 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 4 /\ X2= 2 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 ), ( X1= 5 /\ X2= 2 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 ), ( X1= 1 /\ X2= 3 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ P3>4192265 ), ( X1= 2 /\ X2= 3 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ P3>4192265 ), ( X1= 3 /\ X2= 3 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3>4192265 ), ( X1= 4 /\ X2= 3 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3>4192265 ), ( X1= 5 /\ X2= 3 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ P3>4192265 ), ( X1= 1 /\ X2= 4 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 2 /\ X2= 4 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 3 /\ X2= 4 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 4 /\ X2= 4 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 5 /\ X2= 4 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 1 /\ X2= 5 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 2 /\ X2= 5 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=1 /\ 1=0 ), ( X1= 3 /\ X2= 5 /\ X3= 4 /\ X4= 2, 1=0 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 4 /\ X2= 5 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ), ( X1= 5 /\ X2= 5 /\ X3= 4 /\ X4= 2, 1=1 /\ 1=1 /\ 1=1 /\ 1=0 /\ 1=1 /\ 1=0 ) ] ). state_formulas( param(X), [ ( 1, [ X=1 ] ), ( 2, [ X=2 ] ), ( 3, [ X=3 ] ), ( 4, [ X=4 ] ), ( 5, [ X=5 ] ), ( 6, [ X=6 ] ), ( 7, [ X=7 ] ), ( 8, [ X=8 ] ), ( 9, [ X=9 ] ), ( 10, [ X=10 ] ), ( 11, [ X=11 ] ), ( 12, [ X=12 ] ), ( 13, [ X=13 ] ), ( 14, [ X=14 ] ), ( 15, [ X=15 ] ), ( 16, [ X=16 ] ), ( 17, [ X=17 ] ), ( 18, [ X=18 ] ), ( 19, [ X=19 ] ), ( 20, [ X=20 ] ), ( 21, [ X=21 ] ), ( 22, [ X=22 ] ), ( 23, [ X=23 ] ), ( 24, [ X=24 ] ), ( 25, [ X=25 ] ), ( 26, [ X=26 ] ), ( 27, [ X=27 ] ), ( 28, [ X=28 ] ), ( 29, [ X=29 ] ), ( 30, [ X=30 ] ), ( 31, [ X=31 ] ), ( 32, [ X=32 ] ), ( 33, [ X=33 ] ), ( 34, [ X=34 ] ), ( 35, [ X=35 ] ), ( 36, [ X=36 ] ), ( 37, [ X=37 ] ), ( 38, [ X=38 ] ), ( 39, [ X=39 ] ), ( 40, [ X=40 ] ), ( 41, [ X=41 ] ), ( 42, [ X=42 ] ), ( 43, [ X=43 ] ), ( 44, [ X=44 ] ), ( 45, [ X=45 ] ), ( 46, [ X=46 ] ), ( 47, [ X=47 ] ), ( 48, [ X=48 ] ), ( 49, [ X=49 ] ), ( 50, [ X=50 ] ), ( 51, [ X=51 ] ), ( 52, [ X=52 ] ), ( 53, [ X=53 ] ), ( 54, [ X=54 ] ), ( 55, [ X=55 ] ), ( 56, [ X=56 ] ), ( 57, [ X=57 ] ), ( 58, [ X=58 ] ), ( 59, [ X=59 ] ), ( 60, [ X=60 ] ), ( 61, [ X=61 ] ), ( 62, [ X=62 ] ), ( 63, [ X=63 ] ), ( 64, [ X=64 ] ), ( 65, [ X=65 ] ), ( 66, [ X=66 ] ), ( 67, [ X=67 ] ), ( 68, [ X=68 ] ), ( 69, [ X=69 ] ), ( 70, [ X=70 ] ), ( 71, [ X=71 ] ), ( 72, [ X=72 ] ), ( 73, [ X=73 ] ), ( 74, [ X=74 ] ), ( 75, [ X=75 ] ), ( 76, [ X=76 ] ), ( 77, [ X=77 ] ), ( 78, [ X=78 ] ), ( 79, [ X=79 ] ), ( 80, [ X=80 ] ), ( 81, [ X=81 ] ), ( 82, [ X=82 ] ), ( 83, [ X=83 ] ), ( 84, [ X=84 ] ), ( 85, [ X=85 ] ), ( 86, [ X=86 ] ), ( 87, [ X=87 ] ), ( 88, [ X=88 ] ), ( 89, [ X=89 ] ), ( 90, [ X=90 ] ), ( 91, [ X=91 ] ), ( 92, [ X=92 ] ), ( 93, [ X=93 ] ), ( 94, [ X=94 ] ), ( 95, [ X=95 ] ), ( 96, [ X=96 ] ), ( 97, [ X=97 ] ), ( 98, [ X=98 ] ), ( 99, [ X=99 ] ), ( 100, [ X=100 ] ), ( 101, [ X=101 ] ), ( 102, [ X=102 ] ), ( 103, [ X=103 ] ), ( 104, [ X=104 ] ), ( 105, [ X=105 ] ), ( 106, [ X=106 ] ), ( 107, [ X=107 ] ), ( 108, [ X=108 ] ), ( 109, [ X=109 ] ), ( 110, [ X=110 ] ), ( 111, [ X=111 ] ), ( 112, [ X=112 ] ), ( 113, [ X=113 ] ), ( 114, [ X=114 ] ), ( 115, [ X=115 ] ), ( 116, [ X=116 ] ), ( 117, [ X=117 ] ), ( 118, [ X=118 ] ), ( 119, [ X=119 ] ), ( 120, [ X=120 ] ), ( 121, [ X=121 ] ), ( 122, [ X=122 ] ), ( 123, [ X=123 ] ), ( 124, [ X=124 ] ), ( 125, [ X=125 ] ), ( 126, [ X=126 ] ), ( 127, [ X=127 ] ), ( 128, [ X=128 ] ), ( 129, [ X=129 ] ), ( 130, [ X=130 ] ), ( 131, [ X=131 ] ), ( 132, [ X=132 ] ), ( 133, [ X=133 ] ), ( 134, [ X=134 ] ), ( 135, [ X=135 ] ), ( 136, [ X=136 ] ), ( 137, [ X=137 ] ), ( 138, [ X=138 ] ), ( 139, [ X=139 ] ), ( 140, [ X=140 ] ), ( 141, [ X=141 ] ), ( 142, [ X=142 ] ), ( 143, [ X=143 ] ), ( 144, [ X=144 ] ), ( 145, [ X=145 ] ), ( 146, [ X=146 ] ), ( 147, [ X=147 ] ), ( 148, [ X=148 ] ), ( 149, [ X=149 ] ), ( 150, [ X=150 ] ), ( 151, [ X=151 ] ), ( 152, [ X=152 ] ), ( 153, [ X=153 ] ), ( 154, [ X=154 ] ), ( 155, [ X=155 ] ), ( 156, [ X=156 ] ), ( 157, [ X=157 ] ), ( 158, [ X=158 ] ), ( 159, [ X=159 ] ), ( 160, [ X=160 ] ), ( 161, [ X=161 ] ), ( 162, [ X=162 ] ), ( 163, [ X=163 ] ), ( 164, [ X=164 ] ), ( 165, [ X=165 ] ), ( 166, [ X=166 ] ), ( 167, [ X=167 ] ), ( 168, [ X=168 ] ), ( 169, [ X=169 ] ), ( 170, [ X=170 ] ), ( 171, [ X=171 ] ), ( 172, [ X=172 ] ), ( 173, [ X=173 ] ), ( 174, [ X=174 ] ), ( 175, [ X=175 ] ), ( 176, [ X=176 ] ), ( 177, [ X=177 ] ), ( 178, [ X=178 ] ), ( 179, [ X=179 ] ), ( 180, [ X=180 ] ), ( 181, [ X=181 ] ), ( 182, [ X=182 ] ), ( 183, [ X=183 ] ), ( 184, [ X=184 ] ), ( 185, [ X=185 ] ), ( 186, [ X=186 ] ), ( 187, [ X=187 ] ), ( 188, [ X=188 ] ), ( 189, [ X=189 ] ), ( 190, [ X=190 ] ), ( 191, [ X=191 ] ), ( 192, [ X=192 ] ), ( 193, [ X=193 ] ), ( 194, [ X=194 ] ), ( 195, [ X=195 ] ), ( 196, [ X=196 ] ), ( 197, [ X=197 ] ), ( 198, [ X=198 ] ), ( 199, [ X=199 ] ), ( 200, [ X=200 ] ) ]).