** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic ALL) ; NB. User specified.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] (declare-fun q1 (Bool) Bool)
[GOOD] (declare-fun q2 (Bool Bool) Bool)
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s0 () Bool (q1 false))
[GOOD] (define-fun s1 () Bool (q2 false false))
*** Checking Satisfiability, all solutions..
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
Looking for solution 1
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false)))
[GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model1_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model1 x!0))))
[GOOD] (define-fun q2_model1 ((x!0 Bool) (x!1 Bool)) Bool
          false
       )
[GOOD] (define-fun q2_model1_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model1 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_1 () Bool 
               (or q1_model1_reject
                   q2_model1_reject
               ))
[GOOD] (assert uiFunRejector_model_1)
Looking for solution 2
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false)))
[GOOD] (define-fun q1_model2 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model2_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model2 x!0))))
[GOOD] (define-fun q2_model2 ((x!0 Bool) (x!1 Bool)) Bool
          false
       )
[GOOD] (define-fun q2_model2_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model2 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_2 () Bool 
               (or q1_model2_reject
                   q2_model2_reject
               ))
[GOOD] (assert uiFunRejector_model_2)
Looking for solution 3
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true)))
[GOOD] (define-fun q1_model3 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model3_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model3 x!0))))
[GOOD] (define-fun q2_model3 ((x!0 Bool) (x!1 Bool)) Bool
          true
       )
[GOOD] (define-fun q2_model3_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model3 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_3 () Bool 
               (or q1_model3_reject
                   q2_model3_reject
               ))
[GOOD] (assert uiFunRejector_model_3)
Looking for solution 4
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model4 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model4_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model4 x!0))))
[GOOD] (define-fun q2_model4 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model4_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model4 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_4 () Bool 
               (or q1_model4_reject
                   q2_model4_reject
               ))
[GOOD] (assert uiFunRejector_model_4)
Looking for solution 5
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model5 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model5_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model5 x!0))))
[GOOD] (define-fun q2_model5 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model5_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model5 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_5 () Bool 
               (or q1_model5_reject
                   q2_model5_reject
               ))
[GOOD] (assert uiFunRejector_model_5)
Looking for solution 6
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2)))))
[GOOD] (define-fun q1_model6 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model6_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model6 x!0))))
[GOOD] (define-fun q2_model6 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model6_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model6 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_6 () Bool 
               (or q1_model6_reject
                   q2_model6_reject
               ))
[GOOD] (assert uiFunRejector_model_6)
Looking for solution 7
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model7 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model7_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model7 x!0))))
[GOOD] (define-fun q2_model7 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model7_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model7 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_7 () Bool 
               (or q1_model7_reject
                   q2_model7_reject
               ))
[GOOD] (assert uiFunRejector_model_7)
Looking for solution 8
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model8 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model8_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model8 x!0))))
[GOOD] (define-fun q2_model8 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model8_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model8 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_8 () Bool 
               (or q1_model8_reject
                   q2_model8_reject
               ))
[GOOD] (assert uiFunRejector_model_8)
Looking for solution 9
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model9 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model9_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model9 x!0))))
[GOOD] (define-fun q2_model9 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model9_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model9 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_9 () Bool 
               (or q1_model9_reject
                   q2_model9_reject
               ))
[GOOD] (assert uiFunRejector_model_9)
Looking for solution 10
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and (not x!1) x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model10 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model10_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model10 x!0))))
[GOOD] (define-fun q2_model10 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model10_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model10 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_10 () Bool 
               (or q1_model10_reject
                   q2_model10_reject
               ))
[GOOD] (assert uiFunRejector_model_10)
Looking for solution 11
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and (not x!1) x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model11 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model11_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model11 x!0))))
[GOOD] (define-fun q2_model11 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model11_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model11 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_11 () Bool 
               (or q1_model11_reject
                   q2_model11_reject
               ))
[GOOD] (assert uiFunRejector_model_11)
Looking for solution 12
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and (not x!1) x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model12 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model12_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model12 x!0))))
[GOOD] (define-fun q2_model12 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model12_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model12 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_12 () Bool 
               (or q1_model12_reject
                   q2_model12_reject
               ))
[GOOD] (assert uiFunRejector_model_12)
Looking for solution 13
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and (not x!1) x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model13 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model13_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model13 x!0))))
[GOOD] (define-fun q2_model13 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model13_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model13 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_13 () Bool 
               (or q1_model13_reject
                   q2_model13_reject
               ))
[GOOD] (assert uiFunRejector_model_13)
Looking for solution 14
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model14 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model14_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model14 x!0))))
[GOOD] (define-fun q2_model14 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model14_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model14 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_14 () Bool 
               (or q1_model14_reject
                   q2_model14_reject
               ))
[GOOD] (assert uiFunRejector_model_14)
Looking for solution 15
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model15 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model15_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model15 x!0))))
[GOOD] (define-fun q2_model15 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model15_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model15 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_15 () Bool 
               (or q1_model15_reject
                   q2_model15_reject
               ))
[GOOD] (assert uiFunRejector_model_15)
Looking for solution 16
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model16 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model16_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model16 x!0))))
[GOOD] (define-fun q2_model16 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model16_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model16 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_16 () Bool 
               (or q1_model16_reject
                   q2_model16_reject
               ))
[GOOD] (assert uiFunRejector_model_16)
Looking for solution 17
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model17 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model17_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model17 x!0))))
[GOOD] (define-fun q2_model17 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model17_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model17 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_17 () Bool 
               (or q1_model17_reject
                   q2_model17_reject
               ))
[GOOD] (assert uiFunRejector_model_17)
Looking for solution 18
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true)))
[GOOD] (define-fun q1_model18 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model18_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model18 x!0))))
[GOOD] (define-fun q2_model18 ((x!0 Bool) (x!1 Bool)) Bool
          true
       )
[GOOD] (define-fun q2_model18_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model18 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_18 () Bool 
               (or q1_model18_reject
                   q2_model18_reject
               ))
[GOOD] (assert uiFunRejector_model_18)
Looking for solution 19
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true)))
[GOOD] (define-fun q1_model19 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model19_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model19 x!0))))
[GOOD] (define-fun q2_model19 ((x!0 Bool) (x!1 Bool)) Bool
          true
       )
[GOOD] (define-fun q2_model19_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model19 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_19 () Bool 
               (or q1_model19_reject
                   q2_model19_reject
               ))
[GOOD] (assert uiFunRejector_model_19)
Looking for solution 20
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) true)))
[GOOD] (define-fun q1_model20 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model20_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model20 x!0))))
[GOOD] (define-fun q2_model20 ((x!0 Bool) (x!1 Bool)) Bool
          true
       )
[GOOD] (define-fun q2_model20_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model20 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_20 () Bool 
               (or q1_model20_reject
                   q2_model20_reject
               ))
[GOOD] (assert uiFunRejector_model_20)
Looking for solution 21
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model21 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model21_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model21 x!0))))
[GOOD] (define-fun q2_model21 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model21_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model21 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_21 () Bool 
               (or q1_model21_reject
                   q2_model21_reject
               ))
[GOOD] (assert uiFunRejector_model_21)
Looking for solution 22
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model22 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model22_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model22 x!0))))
[GOOD] (define-fun q2_model22 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model22_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model22 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_22 () Bool 
               (or q1_model22_reject
                   q2_model22_reject
               ))
[GOOD] (assert uiFunRejector_model_22)
Looking for solution 23
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model23 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model23_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model23 x!0))))
[GOOD] (define-fun q2_model23 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model23_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model23 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_23 () Bool 
               (or q1_model23_reject
                   q2_model23_reject
               ))
[GOOD] (assert uiFunRejector_model_23)
Looking for solution 24
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false)))
[GOOD] (define-fun q1_model24 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model24_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model24 x!0))))
[GOOD] (define-fun q2_model24 ((x!0 Bool) (x!1 Bool)) Bool
          false
       )
[GOOD] (define-fun q2_model24_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model24 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_24 () Bool 
               (or q1_model24_reject
                   q2_model24_reject
               ))
[GOOD] (assert uiFunRejector_model_24)
Looking for solution 25
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2)))))
[GOOD] (define-fun q1_model25 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model25_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model25 x!0))))
[GOOD] (define-fun q2_model25 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model25_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model25 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_25 () Bool 
               (or q1_model25_reject
                   q2_model25_reject
               ))
[GOOD] (assert uiFunRejector_model_25)
Looking for solution 26
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model26 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model26_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model26 x!0))))
[GOOD] (define-fun q2_model26 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model26_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model26 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_26 () Bool 
               (or q1_model26_reject
                   q2_model26_reject
               ))
[GOOD] (assert uiFunRejector_model_26)
Looking for solution 27
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and (not x!1) x!2)) (not (and (not x!1) (not x!2)))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model27 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model27_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model27 x!0))))
[GOOD] (define-fun q2_model27 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model27_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model27 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_27 () Bool 
               (or q1_model27_reject
                   q2_model27_reject
               ))
[GOOD] (assert uiFunRejector_model_27)
Looking for solution 28
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2))))
[GOOD] (define-fun q1_model28 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model28_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model28 x!0))))
[GOOD] (define-fun q2_model28 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model28_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model28 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_28 () Bool 
               (or q1_model28_reject
                   q2_model28_reject
               ))
[GOOD] (assert uiFunRejector_model_28)
Looking for solution 29
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2))))
[GOOD] (define-fun q1_model29 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model29_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model29 x!0))))
[GOOD] (define-fun q2_model29 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model29_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model29 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_29 () Bool 
               (or q1_model29_reject
                   q2_model29_reject
               ))
[GOOD] (assert uiFunRejector_model_29)
Looking for solution 30
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2)))))
[GOOD] (define-fun q1_model30 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model30_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model30 x!0))))
[GOOD] (define-fun q2_model30 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model30_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model30 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_30 () Bool 
               (or q1_model30_reject
                   q2_model30_reject
               ))
[GOOD] (assert uiFunRejector_model_30)
Looking for solution 31
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2))))
[GOOD] (define-fun q1_model31 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model31_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model31 x!0))))
[GOOD] (define-fun q2_model31 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model31_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model31 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_31 () Bool 
               (or q1_model31_reject
                   q2_model31_reject
               ))
[GOOD] (assert uiFunRejector_model_31)
Looking for solution 32
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model32 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model32_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model32 x!0))))
[GOOD] (define-fun q2_model32 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model32_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model32 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_32 () Bool 
               (or q1_model32_reject
                   q2_model32_reject
               ))
[GOOD] (assert uiFunRejector_model_32)
Looking for solution 33
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 (not x!2)) (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model33 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model33_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model33 x!0))))
[GOOD] (define-fun q2_model33 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model33_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model33 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_33 () Bool 
               (or q1_model33_reject
                   q2_model33_reject
               ))
[GOOD] (assert uiFunRejector_model_33)
Looking for solution 34
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2))))
[GOOD] (define-fun q1_model34 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model34_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model34 x!0))))
[GOOD] (define-fun q2_model34 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model34_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model34 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_34 () Bool 
               (or q1_model34_reject
                   q2_model34_reject
               ))
[GOOD] (assert uiFunRejector_model_34)
Looking for solution 35
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 (not x!2)) (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model35 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model35_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model35 x!0))))
[GOOD] (define-fun q2_model35 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model35_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model35 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_35 () Bool 
               (or q1_model35_reject
                   q2_model35_reject
               ))
[GOOD] (assert uiFunRejector_model_35)
Looking for solution 36
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model36 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model36_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model36 x!0))))
[GOOD] (define-fun q2_model36 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model36_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model36 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_36 () Bool 
               (or q1_model36_reject
                   q2_model36_reject
               ))
[GOOD] (assert uiFunRejector_model_36)
Looking for solution 37
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2))))
[GOOD] (define-fun q1_model37 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model37_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model37 x!0))))
[GOOD] (define-fun q2_model37 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model37_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model37 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_37 () Bool 
               (or q1_model37_reject
                   q2_model37_reject
               ))
[GOOD] (assert uiFunRejector_model_37)
Looking for solution 38
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model38 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model38_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model38 x!0))))
[GOOD] (define-fun q2_model38 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model38_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model38 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_38 () Bool 
               (or q1_model38_reject
                   q2_model38_reject
               ))
[GOOD] (assert uiFunRejector_model_38)
Looking for solution 39
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and (not x!1) (not x!2)))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model39 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model39_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model39 x!0))))
[GOOD] (define-fun q2_model39 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model39_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model39 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_39 () Bool 
               (or q1_model39_reject
                   q2_model39_reject
               ))
[GOOD] (assert uiFunRejector_model_39)
Looking for solution 40
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and (not x!1) (not x!2)))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model40 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model40_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model40 x!0))))
[GOOD] (define-fun q2_model40 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model40_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model40 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_40 () Bool 
               (or q1_model40_reject
                   q2_model40_reject
               ))
[GOOD] (assert uiFunRejector_model_40)
Looking for solution 41
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model41 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model41_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model41 x!0))))
[GOOD] (define-fun q2_model41 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model41_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model41 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_41 () Bool 
               (or q1_model41_reject
                   q2_model41_reject
               ))
[GOOD] (assert uiFunRejector_model_41)
Looking for solution 42
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2))))
[GOOD] (define-fun q1_model42 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model42_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model42 x!0))))
[GOOD] (define-fun q2_model42 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model42_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model42 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_42 () Bool 
               (or q1_model42_reject
                   q2_model42_reject
               ))
[GOOD] (assert uiFunRejector_model_42)
Looking for solution 43
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model43 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model43_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model43 x!0))))
[GOOD] (define-fun q2_model43 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model43_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model43 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_43 () Bool 
               (or q1_model43_reject
                   q2_model43_reject
               ))
[GOOD] (assert uiFunRejector_model_43)
Looking for solution 44
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 (not x!2))) (not (and (not x!1) (not x!2)))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model44 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model44_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model44 x!0))))
[GOOD] (define-fun q2_model44 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model44_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model44 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_44 () Bool 
               (or q1_model44_reject
                   q2_model44_reject
               ))
[GOOD] (assert uiFunRejector_model_44)
Looking for solution 45
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model45 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model45_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model45 x!0))))
[GOOD] (define-fun q2_model45 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model45_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model45 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_45 () Bool 
               (or q1_model45_reject
                   q2_model45_reject
               ))
[GOOD] (assert uiFunRejector_model_45)
Looking for solution 46
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model46 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model46_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model46 x!0))))
[GOOD] (define-fun q2_model46 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model46_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model46 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_46 () Bool 
               (or q1_model46_reject
                   q2_model46_reject
               ))
[GOOD] (assert uiFunRejector_model_46)
Looking for solution 47
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 x!2)) (not (and x!1 (not x!2)))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model47 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model47_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model47 x!0))))
[GOOD] (define-fun q2_model47 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 false) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model47_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model47 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_47 () Bool 
               (or q1_model47_reject
                   q2_model47_reject
               ))
[GOOD] (assert uiFunRejector_model_47)
Looking for solution 48
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2)))))
[GOOD] (define-fun q1_model48 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model48_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model48 x!0))))
[GOOD] (define-fun q2_model48 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model48_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model48 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_48 () Bool 
               (or q1_model48_reject
                   q2_model48_reject
               ))
[GOOD] (assert uiFunRejector_model_48)
Looking for solution 49
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model49 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model49_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model49 x!0))))
[GOOD] (define-fun q2_model49 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model49_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model49 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_49 () Bool 
               (or q1_model49_reject
                   q2_model49_reject
               ))
[GOOD] (assert uiFunRejector_model_49)
Looking for solution 50
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model50 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model50_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model50 x!0))))
[GOOD] (define-fun q2_model50 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model50_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model50 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_50 () Bool 
               (or q1_model50_reject
                   q2_model50_reject
               ))
[GOOD] (assert uiFunRejector_model_50)
Looking for solution 51
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2)))))
[GOOD] (define-fun q1_model51 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model51_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model51 x!0))))
[GOOD] (define-fun q2_model51 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model51_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model51 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_51 () Bool 
               (or q1_model51_reject
                   q2_model51_reject
               ))
[GOOD] (assert uiFunRejector_model_51)
Looking for solution 52
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (or (and (not x!1) x!2) (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model52 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model52_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model52 x!0))))
[GOOD] (define-fun q2_model52 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 false) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model52_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model52 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_52 () Bool 
               (or q1_model52_reject
                   q2_model52_reject
               ))
[GOOD] (assert uiFunRejector_model_52)
Looking for solution 53
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2))))
[GOOD] (define-fun q1_model53 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model53_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model53 x!0))))
[GOOD] (define-fun q2_model53 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model53_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model53 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_53 () Bool 
               (or q1_model53_reject
                   q2_model53_reject
               ))
[GOOD] (assert uiFunRejector_model_53)
Looking for solution 54
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and (not x!1) (not x!2))) (not (and x!1 x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model54 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model54_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model54 x!0))))
[GOOD] (define-fun q2_model54 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model54_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model54 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_54 () Bool 
               (or q1_model54_reject
                   q2_model54_reject
               ))
[GOOD] (assert uiFunRejector_model_54)
Looking for solution 55
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2))))
[GOOD] (define-fun q1_model55 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model55_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model55 x!0))))
[GOOD] (define-fun q2_model55 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model55_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model55 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_55 () Bool 
               (or q1_model55_reject
                   q2_model55_reject
               ))
[GOOD] (assert uiFunRejector_model_55)
Looking for solution 56
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2)))))
[GOOD] (define-fun q1_model56 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model56_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model56 x!0))))
[GOOD] (define-fun q2_model56 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model56_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model56 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_56 () Bool 
               (or q1_model56_reject
                   q2_model56_reject
               ))
[GOOD] (assert uiFunRejector_model_56)
Looking for solution 57
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2)))))
[GOOD] (define-fun q1_model57 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model57_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model57 x!0))))
[GOOD] (define-fun q2_model57 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model57_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model57 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_57 () Bool 
               (or q1_model57_reject
                   q2_model57_reject
               ))
[GOOD] (assert uiFunRejector_model_57)
Looking for solution 58
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) true)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model58 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model58_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model58 x!0))))
[GOOD] (define-fun q2_model58 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model58_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model58 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_58 () Bool 
               (or q1_model58_reject
                   q2_model58_reject
               ))
[GOOD] (assert uiFunRejector_model_58)
Looking for solution 59
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model59 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model59_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model59 x!0))))
[GOOD] (define-fun q2_model59 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model59_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model59 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_59 () Bool 
               (or q1_model59_reject
                   q2_model59_reject
               ))
[GOOD] (assert uiFunRejector_model_59)
Looking for solution 60
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) (not x!1))))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) false)))
[GOOD] (define-fun q1_model60 ((x!0 Bool)) Bool
          (ite (and (= x!0 false)) true
          false)
       )
[GOOD] (define-fun q1_model60_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model60 x!0))))
[GOOD] (define-fun q2_model60 ((x!0 Bool) (x!1 Bool)) Bool
          false
       )
[GOOD] (define-fun q2_model60_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model60 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_60 () Bool 
               (or q1_model60_reject
                   q2_model60_reject
               ))
[GOOD] (assert uiFunRejector_model_60)
Looking for solution 61
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2)))))
[GOOD] (define-fun q1_model61 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model61_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model61 x!0))))
[GOOD] (define-fun q2_model61 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model61_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model61 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_61 () Bool 
               (or q1_model61_reject
                   q2_model61_reject
               ))
[GOOD] (assert uiFunRejector_model_61)
Looking for solution 62
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (or (and (not x!1) (not x!2)) (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model62 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model62_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model62 x!0))))
[GOOD] (define-fun q2_model62 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 false) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model62_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model62 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_62 () Bool 
               (or q1_model62_reject
                   q2_model62_reject
               ))
[GOOD] (assert uiFunRejector_model_62)
Looking for solution 63
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (or (and (not x!1) (not x!2)) (and (not x!1) x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q1_model63 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model63_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model63 x!0))))
[GOOD] (define-fun q2_model63 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 false) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model63_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model63 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_63 () Bool 
               (or q1_model63_reject
                   q2_model63_reject
               ))
[GOOD] (assert uiFunRejector_model_63)
Looking for solution 64
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) false)))
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 x!2) (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q1_model64 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model64_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1         x!0)
                            (q1_model64 x!0))))
[GOOD] (define-fun q2_model64 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model64_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model64 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_64 () Bool 
               (or q1_model64_reject
                   q2_model64_reject
               ))
[GOOD] (assert uiFunRejector_model_64)
Looking for solution 65
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess

RESULT: Solution #1:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = False
Solution #2:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = False
Solution #3:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = True
Solution #4:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = False
  q2 _    _     = True 
Solution #5:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = False
  q2 _    _     = True 
Solution #6:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 _     _     = False
Solution #7:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  True  = True 
  q2 _     _     = False
Solution #8:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = False
  q2 _     _    = True 
Solution #9:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = False
  q2 _     _    = True 
Solution #10:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #11:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #12:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #13:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #14:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False True = False
  q2 _     _    = True 
Solution #15:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = False
  q2 _     _    = True 
Solution #16:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 True True = False
  q2 _    _    = True 
Solution #17:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 True True = False
  q2 _    _    = True 
Solution #18:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = True
Solution #19:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = True
Solution #20:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = True
Solution #21:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 True True = False
  q2 _    _    = True 
Solution #22:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 True True = False
  q2 _    _    = True 
Solution #23:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = False
  q2 _     _     = True 
Solution #24:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = False
Solution #25:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 _    _     = False
Solution #26:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = False
  q2 _     _     = True 
Solution #27:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 True True  = True 
  q2 _    _     = False
Solution #28:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 _     _    = False
Solution #29:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 True True = True 
  q2 _    _    = False
Solution #30:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 _    _     = False
Solution #31:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 _     _    = False
Solution #32:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 True  True = True 
  q2 _     _    = False
Solution #33:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False True  = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #34:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 True True = True 
  q2 _    _    = False
Solution #35:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 True True  = True 
  q2 _    _     = False
Solution #36:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 True  True = True 
  q2 _     _    = False
Solution #37:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 _     _    = False
Solution #38:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = False
  q2 _     _     = True 
Solution #39:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False True  = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #40:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False True  = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #41:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False False = False
  q2 _     _     = True 
Solution #42:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 _     _    = False
Solution #43:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 True  True = True 
  q2 _     _    = False
Solution #44:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 True  True = True 
  q2 _     _    = False
Solution #45:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = False
  q2 _    _     = True 
Solution #46:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 True False = False
  q2 _    _     = True 
Solution #47:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 False True  = True 
  q2 _     _     = False
Solution #48:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 _     _     = False
Solution #49:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  True  = True 
  q2 _     _     = False
Solution #50:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  True  = True 
  q2 _     _     = False
Solution #51:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 _     _     = False
Solution #52:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 False True  = True 
  q2 _     _     = False
Solution #53:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 True True = True 
  q2 _    _    = False
Solution #54:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False True  = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #55:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 True True = True 
  q2 _    _    = False
Solution #56:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 _    _     = False
Solution #57:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 _    _     = False
Solution #58:
  q1 :: Bool -> Bool
  q1 _ = True

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 True True  = True 
  q2 _    _     = False
Solution #59:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 True True  = True 
  q2 _    _     = False
Solution #60:
  q1 :: Bool -> Bool
  q1 False = True 
  q1 _     = False

  q2 :: Bool -> Bool -> Bool
  q2 _ _ = False
Solution #61:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 _     _     = False
Solution #62:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 False True  = True 
  q2 _     _     = False
Solution #63:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 False True  = True 
  q2 _     _     = False
Solution #64:
  q1 :: Bool -> Bool
  q1 _ = False

  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  True  = True 
  q2 _     _     = False
Found 64 different solutions.