forall( lambda : ( ( exists( lambdaprime : 0<=lambdaprime and lambdaprime<=lambda and ( ( not ( ( ( ( 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 ) ) ) ) and ( not ( ( not ( ( not ( ( 1 * ( x3 + ( -5/32 * lambdaprime ) ) ) <= 0 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -335 ) ) ) ) and ( $b1 and $b3 ) ) ) ) and ( not ( $b2 and ( not ( ( not ( ( 1 * ( x3 + ( -5/32 * lambdaprime ) ) ) <= 0 ) ) and ( not ( ( -1 * ( x4 + ( 1/2 * lambdaprime ) ) ) <= -340 ) ) ) ) ) ) ) ) ) ) ) or lambda<0 or ( ( ( 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 ) ) ) ) ) ) )