forall( lambda : ( ( exists( lambdaprime : 0<=lambdaprime and lambdaprime<=lambda and ( ( not ( ( ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambdaprime ) ) ) <= -4100 ) ) ) and ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( not ( ( not ( ( -1 * ( x5 + ( 1 * lambdaprime ) ) ) <= -12 ) ) and ( not ( ( -1 * ( x3 + ( 30 * lambdaprime ) ) ) <= -4500 ) ) ) ) ) ) ) and ( not ( ( $b3 and ( $b1 and $b4 ) ) and ( ( -1 * ( x3 + ( 30 * lambdaprime ) ) ) <= -5820 ) ) ) ) ) ) ) ) or lambda<0 or ( ( ( not ( ( not $b4 ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 4820 ) ) ) ) ) and ( ( not ( ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 4820 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 4820 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not ( $b6 and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 4820 ) ) and ( ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( ( not ( $b6 and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) and ( ( ( not ( ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) and ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( -1 * ( x3 + ( 30 * lambda ) ) ) + ( -15 * ( x5 + ( 1 * lambda ) ) ) <= -4500 ) ) ) ) and ( not ( ( not ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) and ( not ( ( not $b6 ) and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( ( ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( not ( ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 4820 ) ) and ( ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 4820 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 4820 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) and ( not ( ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( ( not ( $b6 and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) and ( ( ( not ( ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) and ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( -1 * ( x3 + ( 30 * lambda ) ) ) + ( -15 * ( x5 + ( 1 * lambda ) ) ) <= -4500 ) ) ) ) and ( not ( ( not ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) and ( not ( ( not $b6 ) and ( ( ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( not ( ( not ( ( not ( ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) and ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) + ( 15 * ( x5 + ( 1 * lambda ) ) ) <= 2930 ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) and ( ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) and ( not ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( ( ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) and ( not ( ( ( not ( ( not $b1 ) and ( not ( ( ( not $b3 ) and ( ( not $b1 ) and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4100 ) ) ) ) ) and ( ( not ( ( not $b3 ) and ( ( ( ( not ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x3 + ( 30 * lambda ) ) ) <= -4500 ) ) ) and ( not ( ( not $b6 ) and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) and ( not ( ( not ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) ) and ( ( not $b3 ) and $b4 ) ) ) ) and ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) ) ) ) and ( ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) and ( not ( $b4 and ( ( not ( ( ( 1 * ( x3 + ( 30 * lambda ) ) ) <= 2930 ) and ( ( not $b3 ) and $b4 ) ) ) and ( not ( $b6 and ( ( ( not $b3 ) and ( $b1 and ( not $b4 ) ) ) and ( ( -1 * ( x5 + ( 1 * lambda ) ) ) <= -12 ) ) ) ) ) ) ) ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) and ( not ( ( $b1 and ( $b3 and ( not $b4 ) ) ) and ( ( ( 1 * ( x4 + ( 0 * lambda ) ) ) <= 0 ) and ( not ( ( 1 * ( x5 + ( 1 * lambda ) ) ) <= 0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) )