forall( lambda : ( ( exists( lambdaprime : 0<=lambdaprime and lambdaprime<=lambda and ( ( not ( ( ( ( ( not ( ( not ( ( not ( ( -1 * ( x3 + ( 5/32 * lambdaprime ) ) ) <= -30 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -405/2 ) ) ) ) and ( ( not $b1 ) and $b5 ) ) ) and ( not ( ( not ( ( not ( ( -1 * ( x3 + ( 5/32 * lambdaprime ) ) ) <= -20 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -220 ) ) ) ) and ( $b1 and $b5 ) ) ) ) and ( not ( ( not ( ( not ( ( -1 * ( x3 + ( 5/32 * lambdaprime ) ) ) <= -20 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -445/2 ) ) ) ) and ( ( not $b1 ) and $b4 ) ) ) ) and ( not ( ( not ( ( not ( ( -1 * ( x3 + ( 5/32 * lambdaprime ) ) ) <= -15 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -235 ) ) ) ) and ( $b1 and $b4 ) ) ) ) and ( not ( ( not ( ( not ( ( -1 * ( x3 + ( 5/32 * lambdaprime ) ) ) <= -15 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -475/2 ) ) ) ) and ( ( not $b1 ) and $b3 ) ) ) ) ) ) ) ) or lambda<0 or ( ( ( ( not ( ( not ( ( 1 * ( x4 + ( 1/2 * lambda ) ) ) <= 207 ) ) and ( ( -1 * ( x3 + ( 5/32 * lambda ) ) ) <= -30 ) ) ) and ( not ( ( not ( ( 1 * ( x4 + ( 1/2 * lambda ) ) ) <= 227 ) ) and ( ( -1 * ( x3 + ( 5/32 * lambda ) ) ) <= -20 ) ) ) ) and ( not ( ( not ( ( 1 * ( x4 + ( 1/2 * lambda ) ) ) <= 242 ) ) and ( ( -1 * ( x3 + ( 5/32 * lambda ) ) ) <= -15 ) ) ) ) ) ) )