(define x_a_0::int)
(define x_a__pa_q1_0::int)
(define x_a_1::int)
(define x_a__pa_q1_1::int)
(define y_1_0::int)
(define z_p_0::int)
(define y_3_1::int)
(define y_6_1::int)
(define y_2_1::int)
(define y_7_1::int)
(define y_9_1::int)
(define z_pa_1::int)
(define z_q_1::int)
(define z_q1_1::int)
(define alpha_a::int)
(define alpha_a__pa_q1::int)
(assert 
  ( and 
    ( >= (+ x_a_0  0 ) 0 ) 

    ( >= (+ x_a__pa_q1_0  0 ) 0 ) 

    ( >= (+ y_1_0  0 ) 0 ) 

    ( >= (+ z_p_0  0 ) 0 ) 

    ( >= (+ x_a_1  0 ) 0 ) 

    ( >= (+ x_a__pa_q1_1  0 ) 0 ) 

    ( >= (+ y_3_1  0 ) 0 ) 

    ( >= (+ y_6_1  0 ) 0 ) 

    ( >= (+ y_2_1  0 ) 0 ) 

    ( >= (+ y_7_1  0 ) 0 ) 

    ( >= (+ y_9_1  0 ) 0 ) 

    ( >= (+ z_pa_1  0 ) 0 ) 

    ( >= (+ z_q_1  0 ) 0 ) 

    ( >= (+ z_q1_1  0 ) 0 ) 

    ( = 0 (+ (- 0 y_1_0)  1 )) 

    ( = 0 (+ (- 0 x_a_0)  0 )) 

    ( = 0 (+ (- 0 x_a__pa_q1_0)  0 )) 

    ( = 0 (+ z_p_0  0 )) 

    ( or 
      ( = 0 (+ z_p_0  0 )) 
    ) 

    ( = 0 (+ (- 0 y_6_1) (+ y_9_1 (+ (- 0 y_3_1)  0 ) ) )) 

    ( = 0 (+ y_9_1 (+ (- 0 y_2_1)  0 ) )) 

    ( = 0 (+ (- 0 y_7_1) (+ (- 0 y_9_1)  1 ) )) 

    ( = 0 (+ (- 0 x_a_1) (+ y_3_1  0 ) )) 

    ( = 0 (+ y_6_1 (+ y_7_1 (+ (- 0 x_a__pa_q1_1)  0 ) ) )) 

    ( or 
      ( = 0 (+ y_3_1  0 )) 

      ( >= (+ z_pa_1  (- 0 1) ) 0 ) 
    ) 

    ( or 
      ( = 0 (+ y_6_1  0 )) 

      ( >= (+ z_pa_1  (- 0 1) ) 0 ) 
    ) 

    ( or 
      ( = 0 (+ y_2_1  0 )) 

      ( >= (+ z_q_1  (- 0 1) ) 0 ) 
    ) 

    ( = 0 (+ z_q1_1  0 )) 

    ( = 0 (+ z_q1_1  0 )) 

    ( or 
      ( = 0 (+ z_pa_1  0 )) 

      ( and 
        ( = 0 (+ z_pa_1  (- 0 1) )) 

        ( >= (+ y_9_1  (- 0 1) ) 0 ) 
      ) 
    ) 

    ( or 
      ( = 0 (+ z_q_1  0 )) 

      ( and 
        ( = 0 (+ z_q_1  (- 0 1) )) 

        ( >= (+ y_9_1  (- 0 1) ) 0 ) 
      ) 
    ) 

    ( or 
      ( = 0 (+ z_q1_1  0 )) 
    ) 

    ( = 0 (+ (- 0 (+ alpha_a alpha_a )) (+ x_a_0 (+ x_a_1  0 ) ) )) 

    ( = 0 (+ (- 0 (+ alpha_a__pa_q1 alpha_a__pa_q1 )) (+ x_a__pa_q1_0 (+ x_a__pa_q1_1  0 ) ) ))
    
))
(check)