diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c
index 9b7f90307..f6a038f23 100644
--- a/src/frontend/smt2/smt2_commands.c
+++ b/src/frontend/smt2/smt2_commands.c
@@ -6283,6 +6283,10 @@ void smt2_set_option(const char *name, aval_t value) {
     set_boolean_option(g, name, value, &g->dump_models);
     break;
 
+  case SMT2_KW_TIMEOUT:
+    set_uint32_option(g, name, value, &g->timeout);
+    break;
+
   case SMT2_KW_PRODUCE_UNSAT_ASSUMPTIONS:
     // optional: if true, get-unsat-assumptions can be used
     if (option_can_be_set(name)) {
diff --git a/src/frontend/smt2/smt2_commands.h b/src/frontend/smt2/smt2_commands.h
index 3f5570859..9fea4ee96 100644
--- a/src/frontend/smt2/smt2_commands.h
+++ b/src/frontend/smt2/smt2_commands.h
@@ -402,7 +402,7 @@ typedef struct smt2_globals_s {
   uint32_t nthreads;           // default = 0 (single threaded)
 
   // timeout
-  uint32_t timeout;           // default = 0 (no timeout)
+  uint32_t timeout;           // default = 0 (no timeout); global timeout used for every check-sat
   timeout_t *to;              // initially NULL. Non-NULL once init_timeout is called
   bool interrupted;           // true if the most recent call to check_sat timed out
 
diff --git a/src/frontend/smt2/smt2_keywords.txt b/src/frontend/smt2/smt2_keywords.txt
index 20ad58844..e78a4c15f 100644
--- a/src/frontend/smt2/smt2_keywords.txt
+++ b/src/frontend/smt2/smt2_keywords.txt
@@ -37,4 +37,5 @@ struct keyword_s;
 :category,                    SMT2_KW_CATEGORY
 :difficulty,                  SMT2_KW_DIFFICULTY
 :notes,                       SMT2_KW_NOTES
-:dump-models,                 SMT2_KW_DUMP_MODELS
\ No newline at end of file
+:dump-models,                 SMT2_KW_DUMP_MODELS
+:timeout,                     SMT2_KW_TIMEOUT
diff --git a/src/frontend/smt2/smt2_lexer.c b/src/frontend/smt2/smt2_lexer.c
index 3efb06a6c..ae3faacd5 100644
--- a/src/frontend/smt2/smt2_lexer.c
+++ b/src/frontend/smt2/smt2_lexer.c
@@ -116,6 +116,7 @@ static const char * const smt2_keyword_string[NUM_SMT2_KEYWORDS] = {
   ":reproducible-resource-limit",  // SMT2_KW_REPRODUCIBLE_RESOURCE_LIMIT
   ":verbosity",               // SMT2_KW_VERBOSITY
   ":dump-models",             // SMT2_KW_DUMP_MODELS
+  ":timeout",                 // SMT2_KW_TIMEOUT
 
   ":all-statistics",          // SMT2_KW_ALL_STATISTICS
   ":assertion-stack-levesl",  // SMT2_KM_ASSERTIONS_STACK_LEVELS
diff --git a/src/frontend/smt2/smt2_lexer.h b/src/frontend/smt2/smt2_lexer.h
index 865fd48fc..d555972fd 100644
--- a/src/frontend/smt2/smt2_lexer.h
+++ b/src/frontend/smt2/smt2_lexer.h
@@ -136,6 +136,7 @@ enum smt2_keyword {
   SMT2_KW_REPRODUCIBLE_RESOURCE_LIMIT,
   SMT2_KW_VERBOSITY,
   SMT2_KW_DUMP_MODELS,
+  SMT2_KW_TIMEOUT,
 
   // Predefined keywords for (get-info ...)
   SMT2_KW_ALL_STATISTICS,
diff --git a/tests/regress/set-timeout.smt2 b/tests/regress/set-timeout.smt2
new file mode 100644
index 000000000..227d74dc6
--- /dev/null
+++ b/tests/regress/set-timeout.smt2
@@ -0,0 +1,3 @@
+ (set-option :timeout 1)
+ (set-logic QF_UF)
+ (exit)
\ No newline at end of file
diff --git a/tests/regress/set-timeout.smt2.gold b/tests/regress/set-timeout.smt2.gold
new file mode 100644
index 000000000..e69de29bb
diff --git a/tests/regress/wd/issue401b.smt2 b/tests/regress/wd/issue401b.smt2
new file mode 100644
index 000000000..0781898a4
--- /dev/null
+++ b/tests/regress/wd/issue401b.smt2
@@ -0,0 +1,2834 @@
+; 
+(set-option :timeout 1)
+(set-option :produce-models true)
+(set-logic QF_LIA)
+(declare-fun sudoku<24><24> () Int)
+(declare-fun sudoku<24><23> () Int)
+(declare-fun sudoku<24><22> () Int)
+(declare-fun sudoku<24><21> () Int)
+(declare-fun sudoku<24><20> () Int)
+(declare-fun sudoku<23><24> () Int)
+(declare-fun sudoku<23><23> () Int)
+(declare-fun sudoku<23><22> () Int)
+(declare-fun sudoku<23><21> () Int)
+(declare-fun sudoku<23><20> () Int)
+(declare-fun sudoku<22><24> () Int)
+(declare-fun sudoku<22><23> () Int)
+(declare-fun sudoku<22><22> () Int)
+(declare-fun sudoku<22><21> () Int)
+(declare-fun sudoku<22><20> () Int)
+(declare-fun sudoku<21><24> () Int)
+(declare-fun sudoku<21><23> () Int)
+(declare-fun sudoku<21><22> () Int)
+(declare-fun sudoku<21><21> () Int)
+(declare-fun sudoku<21><20> () Int)
+(declare-fun sudoku<20><24> () Int)
+(declare-fun sudoku<20><23> () Int)
+(declare-fun sudoku<20><22> () Int)
+(declare-fun sudoku<20><21> () Int)
+(declare-fun sudoku<20><20> () Int)
+(declare-fun sudoku<19><24> () Int)
+(declare-fun sudoku<19><23> () Int)
+(declare-fun sudoku<19><22> () Int)
+(declare-fun sudoku<19><21> () Int)
+(declare-fun sudoku<19><20> () Int)
+(declare-fun sudoku<18><24> () Int)
+(declare-fun sudoku<18><23> () Int)
+(declare-fun sudoku<18><22> () Int)
+(declare-fun sudoku<18><21> () Int)
+(declare-fun sudoku<18><20> () Int)
+(declare-fun sudoku<17><24> () Int)
+(declare-fun sudoku<17><23> () Int)
+(declare-fun sudoku<17><22> () Int)
+(declare-fun sudoku<17><21> () Int)
+(declare-fun sudoku<17><20> () Int)
+(declare-fun sudoku<16><24> () Int)
+(declare-fun sudoku<16><23> () Int)
+(declare-fun sudoku<16><22> () Int)
+(declare-fun sudoku<16><21> () Int)
+(declare-fun sudoku<16><20> () Int)
+(declare-fun sudoku<15><24> () Int)
+(declare-fun sudoku<15><23> () Int)
+(declare-fun sudoku<15><22> () Int)
+(declare-fun sudoku<15><21> () Int)
+(declare-fun sudoku<15><20> () Int)
+(declare-fun sudoku<14><24> () Int)
+(declare-fun sudoku<14><23> () Int)
+(declare-fun sudoku<14><22> () Int)
+(declare-fun sudoku<14><21> () Int)
+(declare-fun sudoku<14><20> () Int)
+(declare-fun sudoku<13><24> () Int)
+(declare-fun sudoku<13><23> () Int)
+(declare-fun sudoku<13><22> () Int)
+(declare-fun sudoku<13><21> () Int)
+(declare-fun sudoku<13><20> () Int)
+(declare-fun sudoku<12><24> () Int)
+(declare-fun sudoku<12><23> () Int)
+(declare-fun sudoku<12><22> () Int)
+(declare-fun sudoku<12><21> () Int)
+(declare-fun sudoku<12><20> () Int)
+(declare-fun sudoku<11><24> () Int)
+(declare-fun sudoku<11><23> () Int)
+(declare-fun sudoku<11><22> () Int)
+(declare-fun sudoku<11><21> () Int)
+(declare-fun sudoku<11><20> () Int)
+(declare-fun sudoku<10><24> () Int)
+(declare-fun sudoku<10><23> () Int)
+(declare-fun sudoku<10><22> () Int)
+(declare-fun sudoku<10><21> () Int)
+(declare-fun sudoku<10><20> () Int)
+(declare-fun sudoku<9><24> () Int)
+(declare-fun sudoku<9><23> () Int)
+(declare-fun sudoku<9><22> () Int)
+(declare-fun sudoku<9><21> () Int)
+(declare-fun sudoku<9><20> () Int)
+(declare-fun sudoku<8><24> () Int)
+(declare-fun sudoku<8><23> () Int)
+(declare-fun sudoku<8><22> () Int)
+(declare-fun sudoku<8><21> () Int)
+(declare-fun sudoku<8><20> () Int)
+(declare-fun sudoku<7><24> () Int)
+(declare-fun sudoku<7><23> () Int)
+(declare-fun sudoku<7><22> () Int)
+(declare-fun sudoku<7><21> () Int)
+(declare-fun sudoku<7><20> () Int)
+(declare-fun sudoku<6><24> () Int)
+(declare-fun sudoku<6><23> () Int)
+(declare-fun sudoku<6><22> () Int)
+(declare-fun sudoku<6><21> () Int)
+(declare-fun sudoku<6><20> () Int)
+(declare-fun sudoku<5><24> () Int)
+(declare-fun sudoku<5><23> () Int)
+(declare-fun sudoku<5><22> () Int)
+(declare-fun sudoku<5><21> () Int)
+(declare-fun sudoku<5><20> () Int)
+(declare-fun sudoku<4><24> () Int)
+(declare-fun sudoku<4><23> () Int)
+(declare-fun sudoku<4><22> () Int)
+(declare-fun sudoku<4><21> () Int)
+(declare-fun sudoku<4><20> () Int)
+(declare-fun sudoku<3><24> () Int)
+(declare-fun sudoku<3><23> () Int)
+(declare-fun sudoku<3><22> () Int)
+(declare-fun sudoku<3><21> () Int)
+(declare-fun sudoku<3><20> () Int)
+(declare-fun sudoku<2><24> () Int)
+(declare-fun sudoku<2><23> () Int)
+(declare-fun sudoku<2><22> () Int)
+(declare-fun sudoku<2><21> () Int)
+(declare-fun sudoku<2><20> () Int)
+(declare-fun sudoku<1><24> () Int)
+(declare-fun sudoku<1><23> () Int)
+(declare-fun sudoku<1><22> () Int)
+(declare-fun sudoku<1><21> () Int)
+(declare-fun sudoku<1><20> () Int)
+(declare-fun sudoku<0><24> () Int)
+(declare-fun sudoku<0><23> () Int)
+(declare-fun sudoku<0><22> () Int)
+(declare-fun sudoku<0><21> () Int)
+(declare-fun sudoku<0><20> () Int)
+(declare-fun sudoku<24><19> () Int)
+(declare-fun sudoku<24><18> () Int)
+(declare-fun sudoku<24><17> () Int)
+(declare-fun sudoku<24><16> () Int)
+(declare-fun sudoku<24><15> () Int)
+(declare-fun sudoku<23><19> () Int)
+(declare-fun sudoku<23><18> () Int)
+(declare-fun sudoku<23><17> () Int)
+(declare-fun sudoku<23><16> () Int)
+(declare-fun sudoku<23><15> () Int)
+(declare-fun sudoku<22><19> () Int)
+(declare-fun sudoku<22><18> () Int)
+(declare-fun sudoku<22><17> () Int)
+(declare-fun sudoku<22><16> () Int)
+(declare-fun sudoku<22><15> () Int)
+(declare-fun sudoku<21><19> () Int)
+(declare-fun sudoku<21><18> () Int)
+(declare-fun sudoku<21><17> () Int)
+(declare-fun sudoku<21><16> () Int)
+(declare-fun sudoku<21><15> () Int)
+(declare-fun sudoku<20><19> () Int)
+(declare-fun sudoku<20><18> () Int)
+(declare-fun sudoku<20><17> () Int)
+(declare-fun sudoku<20><16> () Int)
+(declare-fun sudoku<20><15> () Int)
+(declare-fun sudoku<19><19> () Int)
+(declare-fun sudoku<19><18> () Int)
+(declare-fun sudoku<19><17> () Int)
+(declare-fun sudoku<19><16> () Int)
+(declare-fun sudoku<19><15> () Int)
+(declare-fun sudoku<18><19> () Int)
+(declare-fun sudoku<18><18> () Int)
+(declare-fun sudoku<18><17> () Int)
+(declare-fun sudoku<18><16> () Int)
+(declare-fun sudoku<18><15> () Int)
+(declare-fun sudoku<17><19> () Int)
+(declare-fun sudoku<17><18> () Int)
+(declare-fun sudoku<17><17> () Int)
+(declare-fun sudoku<17><16> () Int)
+(declare-fun sudoku<17><15> () Int)
+(declare-fun sudoku<16><19> () Int)
+(declare-fun sudoku<16><18> () Int)
+(declare-fun sudoku<16><17> () Int)
+(declare-fun sudoku<16><16> () Int)
+(declare-fun sudoku<16><15> () Int)
+(declare-fun sudoku<15><19> () Int)
+(declare-fun sudoku<15><18> () Int)
+(declare-fun sudoku<15><17> () Int)
+(declare-fun sudoku<15><16> () Int)
+(declare-fun sudoku<15><15> () Int)
+(declare-fun sudoku<14><19> () Int)
+(declare-fun sudoku<14><18> () Int)
+(declare-fun sudoku<14><17> () Int)
+(declare-fun sudoku<14><16> () Int)
+(declare-fun sudoku<14><15> () Int)
+(declare-fun sudoku<13><19> () Int)
+(declare-fun sudoku<13><18> () Int)
+(declare-fun sudoku<13><17> () Int)
+(declare-fun sudoku<13><16> () Int)
+(declare-fun sudoku<13><15> () Int)
+(declare-fun sudoku<12><19> () Int)
+(declare-fun sudoku<12><18> () Int)
+(declare-fun sudoku<12><17> () Int)
+(declare-fun sudoku<12><16> () Int)
+(declare-fun sudoku<12><15> () Int)
+(declare-fun sudoku<11><19> () Int)
+(declare-fun sudoku<11><18> () Int)
+(declare-fun sudoku<11><17> () Int)
+(declare-fun sudoku<11><16> () Int)
+(declare-fun sudoku<11><15> () Int)
+(declare-fun sudoku<10><19> () Int)
+(declare-fun sudoku<10><18> () Int)
+(declare-fun sudoku<10><17> () Int)
+(declare-fun sudoku<10><16> () Int)
+(declare-fun sudoku<10><15> () Int)
+(declare-fun sudoku<9><19> () Int)
+(declare-fun sudoku<9><18> () Int)
+(declare-fun sudoku<9><17> () Int)
+(declare-fun sudoku<9><16> () Int)
+(declare-fun sudoku<9><15> () Int)
+(declare-fun sudoku<8><19> () Int)
+(declare-fun sudoku<8><18> () Int)
+(declare-fun sudoku<8><17> () Int)
+(declare-fun sudoku<8><16> () Int)
+(declare-fun sudoku<8><15> () Int)
+(declare-fun sudoku<7><19> () Int)
+(declare-fun sudoku<7><18> () Int)
+(declare-fun sudoku<7><17> () Int)
+(declare-fun sudoku<7><16> () Int)
+(declare-fun sudoku<7><15> () Int)
+(declare-fun sudoku<6><19> () Int)
+(declare-fun sudoku<6><18> () Int)
+(declare-fun sudoku<6><17> () Int)
+(declare-fun sudoku<6><16> () Int)
+(declare-fun sudoku<6><15> () Int)
+(declare-fun sudoku<5><19> () Int)
+(declare-fun sudoku<5><18> () Int)
+(declare-fun sudoku<5><17> () Int)
+(declare-fun sudoku<5><16> () Int)
+(declare-fun sudoku<5><15> () Int)
+(declare-fun sudoku<4><19> () Int)
+(declare-fun sudoku<4><18> () Int)
+(declare-fun sudoku<4><17> () Int)
+(declare-fun sudoku<4><16> () Int)
+(declare-fun sudoku<4><15> () Int)
+(declare-fun sudoku<3><19> () Int)
+(declare-fun sudoku<3><18> () Int)
+(declare-fun sudoku<3><17> () Int)
+(declare-fun sudoku<3><16> () Int)
+(declare-fun sudoku<3><15> () Int)
+(declare-fun sudoku<2><19> () Int)
+(declare-fun sudoku<2><18> () Int)
+(declare-fun sudoku<2><17> () Int)
+(declare-fun sudoku<2><16> () Int)
+(declare-fun sudoku<2><15> () Int)
+(declare-fun sudoku<1><19> () Int)
+(declare-fun sudoku<1><18> () Int)
+(declare-fun sudoku<1><17> () Int)
+(declare-fun sudoku<1><16> () Int)
+(declare-fun sudoku<1><15> () Int)
+(declare-fun sudoku<0><19> () Int)
+(declare-fun sudoku<0><18> () Int)
+(declare-fun sudoku<0><17> () Int)
+(declare-fun sudoku<0><16> () Int)
+(declare-fun sudoku<0><15> () Int)
+(declare-fun sudoku<24><14> () Int)
+(declare-fun sudoku<24><13> () Int)
+(declare-fun sudoku<24><12> () Int)
+(declare-fun sudoku<24><11> () Int)
+(declare-fun sudoku<24><10> () Int)
+(declare-fun sudoku<23><14> () Int)
+(declare-fun sudoku<23><13> () Int)
+(declare-fun sudoku<23><12> () Int)
+(declare-fun sudoku<23><11> () Int)
+(declare-fun sudoku<23><10> () Int)
+(declare-fun sudoku<22><14> () Int)
+(declare-fun sudoku<22><13> () Int)
+(declare-fun sudoku<22><12> () Int)
+(declare-fun sudoku<22><11> () Int)
+(declare-fun sudoku<22><10> () Int)
+(declare-fun sudoku<21><14> () Int)
+(declare-fun sudoku<21><13> () Int)
+(declare-fun sudoku<21><12> () Int)
+(declare-fun sudoku<21><11> () Int)
+(declare-fun sudoku<21><10> () Int)
+(declare-fun sudoku<20><14> () Int)
+(declare-fun sudoku<20><13> () Int)
+(declare-fun sudoku<20><12> () Int)
+(declare-fun sudoku<20><11> () Int)
+(declare-fun sudoku<20><10> () Int)
+(declare-fun sudoku<19><14> () Int)
+(declare-fun sudoku<19><13> () Int)
+(declare-fun sudoku<19><12> () Int)
+(declare-fun sudoku<19><11> () Int)
+(declare-fun sudoku<19><10> () Int)
+(declare-fun sudoku<18><14> () Int)
+(declare-fun sudoku<18><13> () Int)
+(declare-fun sudoku<18><12> () Int)
+(declare-fun sudoku<18><11> () Int)
+(declare-fun sudoku<18><10> () Int)
+(declare-fun sudoku<17><14> () Int)
+(declare-fun sudoku<17><13> () Int)
+(declare-fun sudoku<17><12> () Int)
+(declare-fun sudoku<17><11> () Int)
+(declare-fun sudoku<17><10> () Int)
+(declare-fun sudoku<16><14> () Int)
+(declare-fun sudoku<16><13> () Int)
+(declare-fun sudoku<16><12> () Int)
+(declare-fun sudoku<16><11> () Int)
+(declare-fun sudoku<16><10> () Int)
+(declare-fun sudoku<15><14> () Int)
+(declare-fun sudoku<15><13> () Int)
+(declare-fun sudoku<15><12> () Int)
+(declare-fun sudoku<15><11> () Int)
+(declare-fun sudoku<15><10> () Int)
+(declare-fun sudoku<14><14> () Int)
+(declare-fun sudoku<14><13> () Int)
+(declare-fun sudoku<14><12> () Int)
+(declare-fun sudoku<14><11> () Int)
+(declare-fun sudoku<14><10> () Int)
+(declare-fun sudoku<13><14> () Int)
+(declare-fun sudoku<13><13> () Int)
+(declare-fun sudoku<13><12> () Int)
+(declare-fun sudoku<13><11> () Int)
+(declare-fun sudoku<13><10> () Int)
+(declare-fun sudoku<12><14> () Int)
+(declare-fun sudoku<12><13> () Int)
+(declare-fun sudoku<12><12> () Int)
+(declare-fun sudoku<12><11> () Int)
+(declare-fun sudoku<12><10> () Int)
+(declare-fun sudoku<11><14> () Int)
+(declare-fun sudoku<11><13> () Int)
+(declare-fun sudoku<11><12> () Int)
+(declare-fun sudoku<11><11> () Int)
+(declare-fun sudoku<11><10> () Int)
+(declare-fun sudoku<10><14> () Int)
+(declare-fun sudoku<10><13> () Int)
+(declare-fun sudoku<10><12> () Int)
+(declare-fun sudoku<10><11> () Int)
+(declare-fun sudoku<10><10> () Int)
+(declare-fun sudoku<9><14> () Int)
+(declare-fun sudoku<9><13> () Int)
+(declare-fun sudoku<9><12> () Int)
+(declare-fun sudoku<9><11> () Int)
+(declare-fun sudoku<9><10> () Int)
+(declare-fun sudoku<8><14> () Int)
+(declare-fun sudoku<8><13> () Int)
+(declare-fun sudoku<8><12> () Int)
+(declare-fun sudoku<8><11> () Int)
+(declare-fun sudoku<8><10> () Int)
+(declare-fun sudoku<7><14> () Int)
+(declare-fun sudoku<7><13> () Int)
+(declare-fun sudoku<7><12> () Int)
+(declare-fun sudoku<7><11> () Int)
+(declare-fun sudoku<7><10> () Int)
+(declare-fun sudoku<6><14> () Int)
+(declare-fun sudoku<6><13> () Int)
+(declare-fun sudoku<6><12> () Int)
+(declare-fun sudoku<6><11> () Int)
+(declare-fun sudoku<6><10> () Int)
+(declare-fun sudoku<5><14> () Int)
+(declare-fun sudoku<5><13> () Int)
+(declare-fun sudoku<5><12> () Int)
+(declare-fun sudoku<5><11> () Int)
+(declare-fun sudoku<5><10> () Int)
+(declare-fun sudoku<4><14> () Int)
+(declare-fun sudoku<4><13> () Int)
+(declare-fun sudoku<4><12> () Int)
+(declare-fun sudoku<4><11> () Int)
+(declare-fun sudoku<4><10> () Int)
+(declare-fun sudoku<3><14> () Int)
+(declare-fun sudoku<3><13> () Int)
+(declare-fun sudoku<3><12> () Int)
+(declare-fun sudoku<3><11> () Int)
+(declare-fun sudoku<3><10> () Int)
+(declare-fun sudoku<2><14> () Int)
+(declare-fun sudoku<2><13> () Int)
+(declare-fun sudoku<2><12> () Int)
+(declare-fun sudoku<2><11> () Int)
+(declare-fun sudoku<2><10> () Int)
+(declare-fun sudoku<1><14> () Int)
+(declare-fun sudoku<1><13> () Int)
+(declare-fun sudoku<1><12> () Int)
+(declare-fun sudoku<1><11> () Int)
+(declare-fun sudoku<1><10> () Int)
+(declare-fun sudoku<0><14> () Int)
+(declare-fun sudoku<0><13> () Int)
+(declare-fun sudoku<0><12> () Int)
+(declare-fun sudoku<0><11> () Int)
+(declare-fun sudoku<0><10> () Int)
+(declare-fun sudoku<24><9> () Int)
+(declare-fun sudoku<24><8> () Int)
+(declare-fun sudoku<24><7> () Int)
+(declare-fun sudoku<24><6> () Int)
+(declare-fun sudoku<24><5> () Int)
+(declare-fun sudoku<23><9> () Int)
+(declare-fun sudoku<23><8> () Int)
+(declare-fun sudoku<23><7> () Int)
+(declare-fun sudoku<23><6> () Int)
+(declare-fun sudoku<23><5> () Int)
+(declare-fun sudoku<22><9> () Int)
+(declare-fun sudoku<22><8> () Int)
+(declare-fun sudoku<22><7> () Int)
+(declare-fun sudoku<22><6> () Int)
+(declare-fun sudoku<22><5> () Int)
+(declare-fun sudoku<21><9> () Int)
+(declare-fun sudoku<21><8> () Int)
+(declare-fun sudoku<21><7> () Int)
+(declare-fun sudoku<21><6> () Int)
+(declare-fun sudoku<21><5> () Int)
+(declare-fun sudoku<20><9> () Int)
+(declare-fun sudoku<20><8> () Int)
+(declare-fun sudoku<20><7> () Int)
+(declare-fun sudoku<20><6> () Int)
+(declare-fun sudoku<20><5> () Int)
+(declare-fun sudoku<19><9> () Int)
+(declare-fun sudoku<19><8> () Int)
+(declare-fun sudoku<19><7> () Int)
+(declare-fun sudoku<19><6> () Int)
+(declare-fun sudoku<19><5> () Int)
+(declare-fun sudoku<18><9> () Int)
+(declare-fun sudoku<18><8> () Int)
+(declare-fun sudoku<18><7> () Int)
+(declare-fun sudoku<18><6> () Int)
+(declare-fun sudoku<18><5> () Int)
+(declare-fun sudoku<17><9> () Int)
+(declare-fun sudoku<17><8> () Int)
+(declare-fun sudoku<17><7> () Int)
+(declare-fun sudoku<17><6> () Int)
+(declare-fun sudoku<17><5> () Int)
+(declare-fun sudoku<16><9> () Int)
+(declare-fun sudoku<16><8> () Int)
+(declare-fun sudoku<16><7> () Int)
+(declare-fun sudoku<16><6> () Int)
+(declare-fun sudoku<16><5> () Int)
+(declare-fun sudoku<15><9> () Int)
+(declare-fun sudoku<15><8> () Int)
+(declare-fun sudoku<15><7> () Int)
+(declare-fun sudoku<15><6> () Int)
+(declare-fun sudoku<15><5> () Int)
+(declare-fun sudoku<14><9> () Int)
+(declare-fun sudoku<14><8> () Int)
+(declare-fun sudoku<14><7> () Int)
+(declare-fun sudoku<14><6> () Int)
+(declare-fun sudoku<14><5> () Int)
+(declare-fun sudoku<13><9> () Int)
+(declare-fun sudoku<13><8> () Int)
+(declare-fun sudoku<13><7> () Int)
+(declare-fun sudoku<13><6> () Int)
+(declare-fun sudoku<13><5> () Int)
+(declare-fun sudoku<12><9> () Int)
+(declare-fun sudoku<12><8> () Int)
+(declare-fun sudoku<12><7> () Int)
+(declare-fun sudoku<12><6> () Int)
+(declare-fun sudoku<12><5> () Int)
+(declare-fun sudoku<11><9> () Int)
+(declare-fun sudoku<11><8> () Int)
+(declare-fun sudoku<11><7> () Int)
+(declare-fun sudoku<11><6> () Int)
+(declare-fun sudoku<11><5> () Int)
+(declare-fun sudoku<10><9> () Int)
+(declare-fun sudoku<10><8> () Int)
+(declare-fun sudoku<10><7> () Int)
+(declare-fun sudoku<10><6> () Int)
+(declare-fun sudoku<10><5> () Int)
+(declare-fun sudoku<9><9> () Int)
+(declare-fun sudoku<9><8> () Int)
+(declare-fun sudoku<9><7> () Int)
+(declare-fun sudoku<9><6> () Int)
+(declare-fun sudoku<9><5> () Int)
+(declare-fun sudoku<8><9> () Int)
+(declare-fun sudoku<8><8> () Int)
+(declare-fun sudoku<8><7> () Int)
+(declare-fun sudoku<8><6> () Int)
+(declare-fun sudoku<8><5> () Int)
+(declare-fun sudoku<7><9> () Int)
+(declare-fun sudoku<7><8> () Int)
+(declare-fun sudoku<7><7> () Int)
+(declare-fun sudoku<7><6> () Int)
+(declare-fun sudoku<7><5> () Int)
+(declare-fun sudoku<6><9> () Int)
+(declare-fun sudoku<6><8> () Int)
+(declare-fun sudoku<6><7> () Int)
+(declare-fun sudoku<6><6> () Int)
+(declare-fun sudoku<6><5> () Int)
+(declare-fun sudoku<5><9> () Int)
+(declare-fun sudoku<5><8> () Int)
+(declare-fun sudoku<5><7> () Int)
+(declare-fun sudoku<5><6> () Int)
+(declare-fun sudoku<5><5> () Int)
+(declare-fun sudoku<4><9> () Int)
+(declare-fun sudoku<4><8> () Int)
+(declare-fun sudoku<4><7> () Int)
+(declare-fun sudoku<4><6> () Int)
+(declare-fun sudoku<4><5> () Int)
+(declare-fun sudoku<3><9> () Int)
+(declare-fun sudoku<3><8> () Int)
+(declare-fun sudoku<3><7> () Int)
+(declare-fun sudoku<3><6> () Int)
+(declare-fun sudoku<3><5> () Int)
+(declare-fun sudoku<2><9> () Int)
+(declare-fun sudoku<2><8> () Int)
+(declare-fun sudoku<2><7> () Int)
+(declare-fun sudoku<2><6> () Int)
+(declare-fun sudoku<2><5> () Int)
+(declare-fun sudoku<1><9> () Int)
+(declare-fun sudoku<1><8> () Int)
+(declare-fun sudoku<1><7> () Int)
+(declare-fun sudoku<1><6> () Int)
+(declare-fun sudoku<1><5> () Int)
+(declare-fun sudoku<0><9> () Int)
+(declare-fun sudoku<0><8> () Int)
+(declare-fun sudoku<0><7> () Int)
+(declare-fun sudoku<0><6> () Int)
+(declare-fun sudoku<0><5> () Int)
+(declare-fun sudoku<24><4> () Int)
+(declare-fun sudoku<24><3> () Int)
+(declare-fun sudoku<24><2> () Int)
+(declare-fun sudoku<24><1> () Int)
+(declare-fun sudoku<24><0> () Int)
+(declare-fun sudoku<23><4> () Int)
+(declare-fun sudoku<23><3> () Int)
+(declare-fun sudoku<23><2> () Int)
+(declare-fun sudoku<23><1> () Int)
+(declare-fun sudoku<23><0> () Int)
+(declare-fun sudoku<22><4> () Int)
+(declare-fun sudoku<22><3> () Int)
+(declare-fun sudoku<22><2> () Int)
+(declare-fun sudoku<22><1> () Int)
+(declare-fun sudoku<22><0> () Int)
+(declare-fun sudoku<21><4> () Int)
+(declare-fun sudoku<21><3> () Int)
+(declare-fun sudoku<21><2> () Int)
+(declare-fun sudoku<21><1> () Int)
+(declare-fun sudoku<21><0> () Int)
+(declare-fun sudoku<20><4> () Int)
+(declare-fun sudoku<20><3> () Int)
+(declare-fun sudoku<20><2> () Int)
+(declare-fun sudoku<20><1> () Int)
+(declare-fun sudoku<20><0> () Int)
+(declare-fun sudoku<19><4> () Int)
+(declare-fun sudoku<19><3> () Int)
+(declare-fun sudoku<19><2> () Int)
+(declare-fun sudoku<19><1> () Int)
+(declare-fun sudoku<19><0> () Int)
+(declare-fun sudoku<18><4> () Int)
+(declare-fun sudoku<18><3> () Int)
+(declare-fun sudoku<18><2> () Int)
+(declare-fun sudoku<18><1> () Int)
+(declare-fun sudoku<18><0> () Int)
+(declare-fun sudoku<17><4> () Int)
+(declare-fun sudoku<17><3> () Int)
+(declare-fun sudoku<17><2> () Int)
+(declare-fun sudoku<17><1> () Int)
+(declare-fun sudoku<17><0> () Int)
+(declare-fun sudoku<16><4> () Int)
+(declare-fun sudoku<16><3> () Int)
+(declare-fun sudoku<16><2> () Int)
+(declare-fun sudoku<16><1> () Int)
+(declare-fun sudoku<16><0> () Int)
+(declare-fun sudoku<15><4> () Int)
+(declare-fun sudoku<15><3> () Int)
+(declare-fun sudoku<15><2> () Int)
+(declare-fun sudoku<15><1> () Int)
+(declare-fun sudoku<15><0> () Int)
+(declare-fun sudoku<14><4> () Int)
+(declare-fun sudoku<14><3> () Int)
+(declare-fun sudoku<14><2> () Int)
+(declare-fun sudoku<14><1> () Int)
+(declare-fun sudoku<14><0> () Int)
+(declare-fun sudoku<13><4> () Int)
+(declare-fun sudoku<13><3> () Int)
+(declare-fun sudoku<13><2> () Int)
+(declare-fun sudoku<13><1> () Int)
+(declare-fun sudoku<13><0> () Int)
+(declare-fun sudoku<12><4> () Int)
+(declare-fun sudoku<12><3> () Int)
+(declare-fun sudoku<12><2> () Int)
+(declare-fun sudoku<12><1> () Int)
+(declare-fun sudoku<12><0> () Int)
+(declare-fun sudoku<11><4> () Int)
+(declare-fun sudoku<11><3> () Int)
+(declare-fun sudoku<11><2> () Int)
+(declare-fun sudoku<11><1> () Int)
+(declare-fun sudoku<11><0> () Int)
+(declare-fun sudoku<10><4> () Int)
+(declare-fun sudoku<10><3> () Int)
+(declare-fun sudoku<10><2> () Int)
+(declare-fun sudoku<10><1> () Int)
+(declare-fun sudoku<10><0> () Int)
+(declare-fun sudoku<9><4> () Int)
+(declare-fun sudoku<9><3> () Int)
+(declare-fun sudoku<9><2> () Int)
+(declare-fun sudoku<9><1> () Int)
+(declare-fun sudoku<9><0> () Int)
+(declare-fun sudoku<8><4> () Int)
+(declare-fun sudoku<8><3> () Int)
+(declare-fun sudoku<8><2> () Int)
+(declare-fun sudoku<8><1> () Int)
+(declare-fun sudoku<8><0> () Int)
+(declare-fun sudoku<7><4> () Int)
+(declare-fun sudoku<7><3> () Int)
+(declare-fun sudoku<7><2> () Int)
+(declare-fun sudoku<7><1> () Int)
+(declare-fun sudoku<7><0> () Int)
+(declare-fun sudoku<6><4> () Int)
+(declare-fun sudoku<6><3> () Int)
+(declare-fun sudoku<6><2> () Int)
+(declare-fun sudoku<6><1> () Int)
+(declare-fun sudoku<6><0> () Int)
+(declare-fun sudoku<5><4> () Int)
+(declare-fun sudoku<5><3> () Int)
+(declare-fun sudoku<5><2> () Int)
+(declare-fun sudoku<5><1> () Int)
+(declare-fun sudoku<5><0> () Int)
+(declare-fun sudoku<4><4> () Int)
+(declare-fun sudoku<4><3> () Int)
+(declare-fun sudoku<4><2> () Int)
+(declare-fun sudoku<4><1> () Int)
+(declare-fun sudoku<4><0> () Int)
+(declare-fun sudoku<3><4> () Int)
+(declare-fun sudoku<3><3> () Int)
+(declare-fun sudoku<3><2> () Int)
+(declare-fun sudoku<3><1> () Int)
+(declare-fun sudoku<3><0> () Int)
+(declare-fun sudoku<2><4> () Int)
+(declare-fun sudoku<2><3> () Int)
+(declare-fun sudoku<2><2> () Int)
+(declare-fun sudoku<2><1> () Int)
+(declare-fun sudoku<2><0> () Int)
+(declare-fun sudoku<1><4> () Int)
+(declare-fun sudoku<1><3> () Int)
+(declare-fun sudoku<1><2> () Int)
+(declare-fun sudoku<1><1> () Int)
+(declare-fun sudoku<1><0> () Int)
+(declare-fun sudoku<0><4> () Int)
+(declare-fun sudoku<0><3> () Int)
+(declare-fun sudoku<0><2> () Int)
+(declare-fun sudoku<0><1> () Int)
+(declare-fun sudoku<0><0> () Int)
+(assert
+ (let (($x2873 (and (distinct sudoku<20><20> sudoku<20><21> sudoku<20><22> sudoku<20><23> sudoku<20><24> sudoku<21><20> sudoku<21><21> sudoku<21><22> sudoku<21><23> sudoku<21><24> sudoku<22><20> sudoku<22><21> sudoku<22><22> sudoku<22><23> sudoku<22><24> sudoku<23><20> sudoku<23><21> sudoku<23><22> sudoku<23><23> sudoku<23><24> sudoku<24><20> sudoku<24><21> sudoku<24><22> sudoku<24><23> sudoku<24><24>) true)))
+ (let (($x2872 (and (distinct sudoku<15><20> sudoku<15><21> sudoku<15><22> sudoku<15><23> sudoku<15><24> sudoku<16><20> sudoku<16><21> sudoku<16><22> sudoku<16><23> sudoku<16><24> sudoku<17><20> sudoku<17><21> sudoku<17><22> sudoku<17><23> sudoku<17><24> sudoku<18><20> sudoku<18><21> sudoku<18><22> sudoku<18><23> sudoku<18><24> sudoku<19><20> sudoku<19><21> sudoku<19><22> sudoku<19><23> sudoku<19><24>) true)))
+ (let (($x2871 (and (distinct sudoku<10><20> sudoku<10><21> sudoku<10><22> sudoku<10><23> sudoku<10><24> sudoku<11><20> sudoku<11><21> sudoku<11><22> sudoku<11><23> sudoku<11><24> sudoku<12><20> sudoku<12><21> sudoku<12><22> sudoku<12><23> sudoku<12><24> sudoku<13><20> sudoku<13><21> sudoku<13><22> sudoku<13><23> sudoku<13><24> sudoku<14><20> sudoku<14><21> sudoku<14><22> sudoku<14><23> sudoku<14><24>) true)))
+ (let (($x2870 (and (distinct sudoku<5><20> sudoku<5><21> sudoku<5><22> sudoku<5><23> sudoku<5><24> sudoku<6><20> sudoku<6><21> sudoku<6><22> sudoku<6><23> sudoku<6><24> sudoku<7><20> sudoku<7><21> sudoku<7><22> sudoku<7><23> sudoku<7><24> sudoku<8><20> sudoku<8><21> sudoku<8><22> sudoku<8><23> sudoku<8><24> sudoku<9><20> sudoku<9><21> sudoku<9><22> sudoku<9><23> sudoku<9><24>) true)))
+ (let (($x2869 (and (distinct sudoku<0><20> sudoku<0><21> sudoku<0><22> sudoku<0><23> sudoku<0><24> sudoku<1><20> sudoku<1><21> sudoku<1><22> sudoku<1><23> sudoku<1><24> sudoku<2><20> sudoku<2><21> sudoku<2><22> sudoku<2><23> sudoku<2><24> sudoku<3><20> sudoku<3><21> sudoku<3><22> sudoku<3><23> sudoku<3><24> sudoku<4><20> sudoku<4><21> sudoku<4><22> sudoku<4><23> sudoku<4><24>) true)))
+ (let (($x2868 (and (distinct sudoku<20><15> sudoku<20><16> sudoku<20><17> sudoku<20><18> sudoku<20><19> sudoku<21><15> sudoku<21><16> sudoku<21><17> sudoku<21><18> sudoku<21><19> sudoku<22><15> sudoku<22><16> sudoku<22><17> sudoku<22><18> sudoku<22><19> sudoku<23><15> sudoku<23><16> sudoku<23><17> sudoku<23><18> sudoku<23><19> sudoku<24><15> sudoku<24><16> sudoku<24><17> sudoku<24><18> sudoku<24><19>) true)))
+ (let (($x2867 (and (distinct sudoku<15><15> sudoku<15><16> sudoku<15><17> sudoku<15><18> sudoku<15><19> sudoku<16><15> sudoku<16><16> sudoku<16><17> sudoku<16><18> sudoku<16><19> sudoku<17><15> sudoku<17><16> sudoku<17><17> sudoku<17><18> sudoku<17><19> sudoku<18><15> sudoku<18><16> sudoku<18><17> sudoku<18><18> sudoku<18><19> sudoku<19><15> sudoku<19><16> sudoku<19><17> sudoku<19><18> sudoku<19><19>) true)))
+ (let (($x2866 (and (distinct sudoku<10><15> sudoku<10><16> sudoku<10><17> sudoku<10><18> sudoku<10><19> sudoku<11><15> sudoku<11><16> sudoku<11><17> sudoku<11><18> sudoku<11><19> sudoku<12><15> sudoku<12><16> sudoku<12><17> sudoku<12><18> sudoku<12><19> sudoku<13><15> sudoku<13><16> sudoku<13><17> sudoku<13><18> sudoku<13><19> sudoku<14><15> sudoku<14><16> sudoku<14><17> sudoku<14><18> sudoku<14><19>) true)))
+ (let (($x2865 (and (distinct sudoku<5><15> sudoku<5><16> sudoku<5><17> sudoku<5><18> sudoku<5><19> sudoku<6><15> sudoku<6><16> sudoku<6><17> sudoku<6><18> sudoku<6><19> sudoku<7><15> sudoku<7><16> sudoku<7><17> sudoku<7><18> sudoku<7><19> sudoku<8><15> sudoku<8><16> sudoku<8><17> sudoku<8><18> sudoku<8><19> sudoku<9><15> sudoku<9><16> sudoku<9><17> sudoku<9><18> sudoku<9><19>) true)))
+ (let (($x2864 (and (distinct sudoku<0><15> sudoku<0><16> sudoku<0><17> sudoku<0><18> sudoku<0><19> sudoku<1><15> sudoku<1><16> sudoku<1><17> sudoku<1><18> sudoku<1><19> sudoku<2><15> sudoku<2><16> sudoku<2><17> sudoku<2><18> sudoku<2><19> sudoku<3><15> sudoku<3><16> sudoku<3><17> sudoku<3><18> sudoku<3><19> sudoku<4><15> sudoku<4><16> sudoku<4><17> sudoku<4><18> sudoku<4><19>) true)))
+ (let (($x2863 (and (distinct sudoku<20><10> sudoku<20><11> sudoku<20><12> sudoku<20><13> sudoku<20><14> sudoku<21><10> sudoku<21><11> sudoku<21><12> sudoku<21><13> sudoku<21><14> sudoku<22><10> sudoku<22><11> sudoku<22><12> sudoku<22><13> sudoku<22><14> sudoku<23><10> sudoku<23><11> sudoku<23><12> sudoku<23><13> sudoku<23><14> sudoku<24><10> sudoku<24><11> sudoku<24><12> sudoku<24><13> sudoku<24><14>) true)))
+ (let (($x2862 (and (distinct sudoku<15><10> sudoku<15><11> sudoku<15><12> sudoku<15><13> sudoku<15><14> sudoku<16><10> sudoku<16><11> sudoku<16><12> sudoku<16><13> sudoku<16><14> sudoku<17><10> sudoku<17><11> sudoku<17><12> sudoku<17><13> sudoku<17><14> sudoku<18><10> sudoku<18><11> sudoku<18><12> sudoku<18><13> sudoku<18><14> sudoku<19><10> sudoku<19><11> sudoku<19><12> sudoku<19><13> sudoku<19><14>) true)))
+ (let (($x2861 (and (distinct sudoku<10><10> sudoku<10><11> sudoku<10><12> sudoku<10><13> sudoku<10><14> sudoku<11><10> sudoku<11><11> sudoku<11><12> sudoku<11><13> sudoku<11><14> sudoku<12><10> sudoku<12><11> sudoku<12><12> sudoku<12><13> sudoku<12><14> sudoku<13><10> sudoku<13><11> sudoku<13><12> sudoku<13><13> sudoku<13><14> sudoku<14><10> sudoku<14><11> sudoku<14><12> sudoku<14><13> sudoku<14><14>) true)))
+ (let (($x2860 (and (distinct sudoku<5><10> sudoku<5><11> sudoku<5><12> sudoku<5><13> sudoku<5><14> sudoku<6><10> sudoku<6><11> sudoku<6><12> sudoku<6><13> sudoku<6><14> sudoku<7><10> sudoku<7><11> sudoku<7><12> sudoku<7><13> sudoku<7><14> sudoku<8><10> sudoku<8><11> sudoku<8><12> sudoku<8><13> sudoku<8><14> sudoku<9><10> sudoku<9><11> sudoku<9><12> sudoku<9><13> sudoku<9><14>) true)))
+ (let (($x2859 (and (distinct sudoku<0><10> sudoku<0><11> sudoku<0><12> sudoku<0><13> sudoku<0><14> sudoku<1><10> sudoku<1><11> sudoku<1><12> sudoku<1><13> sudoku<1><14> sudoku<2><10> sudoku<2><11> sudoku<2><12> sudoku<2><13> sudoku<2><14> sudoku<3><10> sudoku<3><11> sudoku<3><12> sudoku<3><13> sudoku<3><14> sudoku<4><10> sudoku<4><11> sudoku<4><12> sudoku<4><13> sudoku<4><14>) true)))
+ (let (($x2858 (and (distinct sudoku<20><5> sudoku<20><6> sudoku<20><7> sudoku<20><8> sudoku<20><9> sudoku<21><5> sudoku<21><6> sudoku<21><7> sudoku<21><8> sudoku<21><9> sudoku<22><5> sudoku<22><6> sudoku<22><7> sudoku<22><8> sudoku<22><9> sudoku<23><5> sudoku<23><6> sudoku<23><7> sudoku<23><8> sudoku<23><9> sudoku<24><5> sudoku<24><6> sudoku<24><7> sudoku<24><8> sudoku<24><9>) true)))
+ (let (($x2857 (and (distinct sudoku<15><5> sudoku<15><6> sudoku<15><7> sudoku<15><8> sudoku<15><9> sudoku<16><5> sudoku<16><6> sudoku<16><7> sudoku<16><8> sudoku<16><9> sudoku<17><5> sudoku<17><6> sudoku<17><7> sudoku<17><8> sudoku<17><9> sudoku<18><5> sudoku<18><6> sudoku<18><7> sudoku<18><8> sudoku<18><9> sudoku<19><5> sudoku<19><6> sudoku<19><7> sudoku<19><8> sudoku<19><9>) true)))
+ (let (($x2856 (and (distinct sudoku<10><5> sudoku<10><6> sudoku<10><7> sudoku<10><8> sudoku<10><9> sudoku<11><5> sudoku<11><6> sudoku<11><7> sudoku<11><8> sudoku<11><9> sudoku<12><5> sudoku<12><6> sudoku<12><7> sudoku<12><8> sudoku<12><9> sudoku<13><5> sudoku<13><6> sudoku<13><7> sudoku<13><8> sudoku<13><9> sudoku<14><5> sudoku<14><6> sudoku<14><7> sudoku<14><8> sudoku<14><9>) true)))
+ (let (($x2855 (and (distinct sudoku<5><5> sudoku<5><6> sudoku<5><7> sudoku<5><8> sudoku<5><9> sudoku<6><5> sudoku<6><6> sudoku<6><7> sudoku<6><8> sudoku<6><9> sudoku<7><5> sudoku<7><6> sudoku<7><7> sudoku<7><8> sudoku<7><9> sudoku<8><5> sudoku<8><6> sudoku<8><7> sudoku<8><8> sudoku<8><9> sudoku<9><5> sudoku<9><6> sudoku<9><7> sudoku<9><8> sudoku<9><9>) true)))
+ (let (($x2854 (and (distinct sudoku<0><5> sudoku<0><6> sudoku<0><7> sudoku<0><8> sudoku<0><9> sudoku<1><5> sudoku<1><6> sudoku<1><7> sudoku<1><8> sudoku<1><9> sudoku<2><5> sudoku<2><6> sudoku<2><7> sudoku<2><8> sudoku<2><9> sudoku<3><5> sudoku<3><6> sudoku<3><7> sudoku<3><8> sudoku<3><9> sudoku<4><5> sudoku<4><6> sudoku<4><7> sudoku<4><8> sudoku<4><9>) true)))
+ (let (($x2853 (and (distinct sudoku<20><0> sudoku<20><1> sudoku<20><2> sudoku<20><3> sudoku<20><4> sudoku<21><0> sudoku<21><1> sudoku<21><2> sudoku<21><3> sudoku<21><4> sudoku<22><0> sudoku<22><1> sudoku<22><2> sudoku<22><3> sudoku<22><4> sudoku<23><0> sudoku<23><1> sudoku<23><2> sudoku<23><3> sudoku<23><4> sudoku<24><0> sudoku<24><1> sudoku<24><2> sudoku<24><3> sudoku<24><4>) true)))
+ (let (($x2852 (and (distinct sudoku<15><0> sudoku<15><1> sudoku<15><2> sudoku<15><3> sudoku<15><4> sudoku<16><0> sudoku<16><1> sudoku<16><2> sudoku<16><3> sudoku<16><4> sudoku<17><0> sudoku<17><1> sudoku<17><2> sudoku<17><3> sudoku<17><4> sudoku<18><0> sudoku<18><1> sudoku<18><2> sudoku<18><3> sudoku<18><4> sudoku<19><0> sudoku<19><1> sudoku<19><2> sudoku<19><3> sudoku<19><4>) true)))
+ (let (($x2851 (and (distinct sudoku<10><0> sudoku<10><1> sudoku<10><2> sudoku<10><3> sudoku<10><4> sudoku<11><0> sudoku<11><1> sudoku<11><2> sudoku<11><3> sudoku<11><4> sudoku<12><0> sudoku<12><1> sudoku<12><2> sudoku<12><3> sudoku<12><4> sudoku<13><0> sudoku<13><1> sudoku<13><2> sudoku<13><3> sudoku<13><4> sudoku<14><0> sudoku<14><1> sudoku<14><2> sudoku<14><3> sudoku<14><4>) true)))
+ (let (($x2850 (and (distinct sudoku<5><0> sudoku<5><1> sudoku<5><2> sudoku<5><3> sudoku<5><4> sudoku<6><0> sudoku<6><1> sudoku<6><2> sudoku<6><3> sudoku<6><4> sudoku<7><0> sudoku<7><1> sudoku<7><2> sudoku<7><3> sudoku<7><4> sudoku<8><0> sudoku<8><1> sudoku<8><2> sudoku<8><3> sudoku<8><4> sudoku<9><0> sudoku<9><1> sudoku<9><2> sudoku<9><3> sudoku<9><4>) true)))
+ (let (($x2849 (and (distinct sudoku<0><0> sudoku<0><1> sudoku<0><2> sudoku<0><3> sudoku<0><4> sudoku<1><0> sudoku<1><1> sudoku<1><2> sudoku<1><3> sudoku<1><4> sudoku<2><0> sudoku<2><1> sudoku<2><2> sudoku<2><3> sudoku<2><4> sudoku<3><0> sudoku<3><1> sudoku<3><2> sudoku<3><3> sudoku<3><4> sudoku<4><0> sudoku<4><1> sudoku<4><2> sudoku<4><3> sudoku<4><4>) true)))
+ (let (($x2848 (and (distinct sudoku<0><24> sudoku<1><24> sudoku<2><24> sudoku<3><24> sudoku<4><24> sudoku<5><24> sudoku<6><24> sudoku<7><24> sudoku<8><24> sudoku<9><24> sudoku<10><24> sudoku<11><24> sudoku<12><24> sudoku<13><24> sudoku<14><24> sudoku<15><24> sudoku<16><24> sudoku<17><24> sudoku<18><24> sudoku<19><24> sudoku<20><24> sudoku<21><24> sudoku<22><24> sudoku<23><24> sudoku<24><24>) true)))
+ (let (($x2847 (and (distinct sudoku<24><0> sudoku<24><1> sudoku<24><2> sudoku<24><3> sudoku<24><4> sudoku<24><5> sudoku<24><6> sudoku<24><7> sudoku<24><8> sudoku<24><9> sudoku<24><10> sudoku<24><11> sudoku<24><12> sudoku<24><13> sudoku<24><14> sudoku<24><15> sudoku<24><16> sudoku<24><17> sudoku<24><18> sudoku<24><19> sudoku<24><20> sudoku<24><21> sudoku<24><22> sudoku<24><23> sudoku<24><24>) true)))
+ (let (($x2846 (and (distinct sudoku<0><23> sudoku<1><23> sudoku<2><23> sudoku<3><23> sudoku<4><23> sudoku<5><23> sudoku<6><23> sudoku<7><23> sudoku<8><23> sudoku<9><23> sudoku<10><23> sudoku<11><23> sudoku<12><23> sudoku<13><23> sudoku<14><23> sudoku<15><23> sudoku<16><23> sudoku<17><23> sudoku<18><23> sudoku<19><23> sudoku<20><23> sudoku<21><23> sudoku<22><23> sudoku<23><23> sudoku<24><23>) true)))
+ (let (($x2845 (and (distinct sudoku<23><0> sudoku<23><1> sudoku<23><2> sudoku<23><3> sudoku<23><4> sudoku<23><5> sudoku<23><6> sudoku<23><7> sudoku<23><8> sudoku<23><9> sudoku<23><10> sudoku<23><11> sudoku<23><12> sudoku<23><13> sudoku<23><14> sudoku<23><15> sudoku<23><16> sudoku<23><17> sudoku<23><18> sudoku<23><19> sudoku<23><20> sudoku<23><21> sudoku<23><22> sudoku<23><23> sudoku<23><24>) true)))
+ (let (($x2844 (and (distinct sudoku<0><22> sudoku<1><22> sudoku<2><22> sudoku<3><22> sudoku<4><22> sudoku<5><22> sudoku<6><22> sudoku<7><22> sudoku<8><22> sudoku<9><22> sudoku<10><22> sudoku<11><22> sudoku<12><22> sudoku<13><22> sudoku<14><22> sudoku<15><22> sudoku<16><22> sudoku<17><22> sudoku<18><22> sudoku<19><22> sudoku<20><22> sudoku<21><22> sudoku<22><22> sudoku<23><22> sudoku<24><22>) true)))
+ (let (($x2843 (and (distinct sudoku<22><0> sudoku<22><1> sudoku<22><2> sudoku<22><3> sudoku<22><4> sudoku<22><5> sudoku<22><6> sudoku<22><7> sudoku<22><8> sudoku<22><9> sudoku<22><10> sudoku<22><11> sudoku<22><12> sudoku<22><13> sudoku<22><14> sudoku<22><15> sudoku<22><16> sudoku<22><17> sudoku<22><18> sudoku<22><19> sudoku<22><20> sudoku<22><21> sudoku<22><22> sudoku<22><23> sudoku<22><24>) true)))
+ (let (($x2842 (and (distinct sudoku<0><21> sudoku<1><21> sudoku<2><21> sudoku<3><21> sudoku<4><21> sudoku<5><21> sudoku<6><21> sudoku<7><21> sudoku<8><21> sudoku<9><21> sudoku<10><21> sudoku<11><21> sudoku<12><21> sudoku<13><21> sudoku<14><21> sudoku<15><21> sudoku<16><21> sudoku<17><21> sudoku<18><21> sudoku<19><21> sudoku<20><21> sudoku<21><21> sudoku<22><21> sudoku<23><21> sudoku<24><21>) true)))
+ (let (($x2841 (and (distinct sudoku<21><0> sudoku<21><1> sudoku<21><2> sudoku<21><3> sudoku<21><4> sudoku<21><5> sudoku<21><6> sudoku<21><7> sudoku<21><8> sudoku<21><9> sudoku<21><10> sudoku<21><11> sudoku<21><12> sudoku<21><13> sudoku<21><14> sudoku<21><15> sudoku<21><16> sudoku<21><17> sudoku<21><18> sudoku<21><19> sudoku<21><20> sudoku<21><21> sudoku<21><22> sudoku<21><23> sudoku<21><24>) true)))
+ (let (($x2840 (and (distinct sudoku<0><20> sudoku<1><20> sudoku<2><20> sudoku<3><20> sudoku<4><20> sudoku<5><20> sudoku<6><20> sudoku<7><20> sudoku<8><20> sudoku<9><20> sudoku<10><20> sudoku<11><20> sudoku<12><20> sudoku<13><20> sudoku<14><20> sudoku<15><20> sudoku<16><20> sudoku<17><20> sudoku<18><20> sudoku<19><20> sudoku<20><20> sudoku<21><20> sudoku<22><20> sudoku<23><20> sudoku<24><20>) true)))
+ (let (($x2839 (and (distinct sudoku<20><0> sudoku<20><1> sudoku<20><2> sudoku<20><3> sudoku<20><4> sudoku<20><5> sudoku<20><6> sudoku<20><7> sudoku<20><8> sudoku<20><9> sudoku<20><10> sudoku<20><11> sudoku<20><12> sudoku<20><13> sudoku<20><14> sudoku<20><15> sudoku<20><16> sudoku<20><17> sudoku<20><18> sudoku<20><19> sudoku<20><20> sudoku<20><21> sudoku<20><22> sudoku<20><23> sudoku<20><24>) true)))
+ (let (($x2838 (and (distinct sudoku<0><19> sudoku<1><19> sudoku<2><19> sudoku<3><19> sudoku<4><19> sudoku<5><19> sudoku<6><19> sudoku<7><19> sudoku<8><19> sudoku<9><19> sudoku<10><19> sudoku<11><19> sudoku<12><19> sudoku<13><19> sudoku<14><19> sudoku<15><19> sudoku<16><19> sudoku<17><19> sudoku<18><19> sudoku<19><19> sudoku<20><19> sudoku<21><19> sudoku<22><19> sudoku<23><19> sudoku<24><19>) true)))
+ (let (($x2837 (and (distinct sudoku<19><0> sudoku<19><1> sudoku<19><2> sudoku<19><3> sudoku<19><4> sudoku<19><5> sudoku<19><6> sudoku<19><7> sudoku<19><8> sudoku<19><9> sudoku<19><10> sudoku<19><11> sudoku<19><12> sudoku<19><13> sudoku<19><14> sudoku<19><15> sudoku<19><16> sudoku<19><17> sudoku<19><18> sudoku<19><19> sudoku<19><20> sudoku<19><21> sudoku<19><22> sudoku<19><23> sudoku<19><24>) true)))
+ (let (($x2836 (and (distinct sudoku<0><18> sudoku<1><18> sudoku<2><18> sudoku<3><18> sudoku<4><18> sudoku<5><18> sudoku<6><18> sudoku<7><18> sudoku<8><18> sudoku<9><18> sudoku<10><18> sudoku<11><18> sudoku<12><18> sudoku<13><18> sudoku<14><18> sudoku<15><18> sudoku<16><18> sudoku<17><18> sudoku<18><18> sudoku<19><18> sudoku<20><18> sudoku<21><18> sudoku<22><18> sudoku<23><18> sudoku<24><18>) true)))
+ (let (($x2835 (and (distinct sudoku<18><0> sudoku<18><1> sudoku<18><2> sudoku<18><3> sudoku<18><4> sudoku<18><5> sudoku<18><6> sudoku<18><7> sudoku<18><8> sudoku<18><9> sudoku<18><10> sudoku<18><11> sudoku<18><12> sudoku<18><13> sudoku<18><14> sudoku<18><15> sudoku<18><16> sudoku<18><17> sudoku<18><18> sudoku<18><19> sudoku<18><20> sudoku<18><21> sudoku<18><22> sudoku<18><23> sudoku<18><24>) true)))
+ (let (($x2834 (and (distinct sudoku<0><17> sudoku<1><17> sudoku<2><17> sudoku<3><17> sudoku<4><17> sudoku<5><17> sudoku<6><17> sudoku<7><17> sudoku<8><17> sudoku<9><17> sudoku<10><17> sudoku<11><17> sudoku<12><17> sudoku<13><17> sudoku<14><17> sudoku<15><17> sudoku<16><17> sudoku<17><17> sudoku<18><17> sudoku<19><17> sudoku<20><17> sudoku<21><17> sudoku<22><17> sudoku<23><17> sudoku<24><17>) true)))
+ (let (($x2833 (and (distinct sudoku<17><0> sudoku<17><1> sudoku<17><2> sudoku<17><3> sudoku<17><4> sudoku<17><5> sudoku<17><6> sudoku<17><7> sudoku<17><8> sudoku<17><9> sudoku<17><10> sudoku<17><11> sudoku<17><12> sudoku<17><13> sudoku<17><14> sudoku<17><15> sudoku<17><16> sudoku<17><17> sudoku<17><18> sudoku<17><19> sudoku<17><20> sudoku<17><21> sudoku<17><22> sudoku<17><23> sudoku<17><24>) true)))
+ (let (($x2832 (and (distinct sudoku<0><16> sudoku<1><16> sudoku<2><16> sudoku<3><16> sudoku<4><16> sudoku<5><16> sudoku<6><16> sudoku<7><16> sudoku<8><16> sudoku<9><16> sudoku<10><16> sudoku<11><16> sudoku<12><16> sudoku<13><16> sudoku<14><16> sudoku<15><16> sudoku<16><16> sudoku<17><16> sudoku<18><16> sudoku<19><16> sudoku<20><16> sudoku<21><16> sudoku<22><16> sudoku<23><16> sudoku<24><16>) true)))
+ (let (($x2831 (and (distinct sudoku<16><0> sudoku<16><1> sudoku<16><2> sudoku<16><3> sudoku<16><4> sudoku<16><5> sudoku<16><6> sudoku<16><7> sudoku<16><8> sudoku<16><9> sudoku<16><10> sudoku<16><11> sudoku<16><12> sudoku<16><13> sudoku<16><14> sudoku<16><15> sudoku<16><16> sudoku<16><17> sudoku<16><18> sudoku<16><19> sudoku<16><20> sudoku<16><21> sudoku<16><22> sudoku<16><23> sudoku<16><24>) true)))
+ (let (($x2830 (and (distinct sudoku<0><15> sudoku<1><15> sudoku<2><15> sudoku<3><15> sudoku<4><15> sudoku<5><15> sudoku<6><15> sudoku<7><15> sudoku<8><15> sudoku<9><15> sudoku<10><15> sudoku<11><15> sudoku<12><15> sudoku<13><15> sudoku<14><15> sudoku<15><15> sudoku<16><15> sudoku<17><15> sudoku<18><15> sudoku<19><15> sudoku<20><15> sudoku<21><15> sudoku<22><15> sudoku<23><15> sudoku<24><15>) true)))
+ (let (($x2829 (and (distinct sudoku<15><0> sudoku<15><1> sudoku<15><2> sudoku<15><3> sudoku<15><4> sudoku<15><5> sudoku<15><6> sudoku<15><7> sudoku<15><8> sudoku<15><9> sudoku<15><10> sudoku<15><11> sudoku<15><12> sudoku<15><13> sudoku<15><14> sudoku<15><15> sudoku<15><16> sudoku<15><17> sudoku<15><18> sudoku<15><19> sudoku<15><20> sudoku<15><21> sudoku<15><22> sudoku<15><23> sudoku<15><24>) true)))
+ (let (($x2828 (and (distinct sudoku<0><14> sudoku<1><14> sudoku<2><14> sudoku<3><14> sudoku<4><14> sudoku<5><14> sudoku<6><14> sudoku<7><14> sudoku<8><14> sudoku<9><14> sudoku<10><14> sudoku<11><14> sudoku<12><14> sudoku<13><14> sudoku<14><14> sudoku<15><14> sudoku<16><14> sudoku<17><14> sudoku<18><14> sudoku<19><14> sudoku<20><14> sudoku<21><14> sudoku<22><14> sudoku<23><14> sudoku<24><14>) true)))
+ (let (($x2827 (and (distinct sudoku<14><0> sudoku<14><1> sudoku<14><2> sudoku<14><3> sudoku<14><4> sudoku<14><5> sudoku<14><6> sudoku<14><7> sudoku<14><8> sudoku<14><9> sudoku<14><10> sudoku<14><11> sudoku<14><12> sudoku<14><13> sudoku<14><14> sudoku<14><15> sudoku<14><16> sudoku<14><17> sudoku<14><18> sudoku<14><19> sudoku<14><20> sudoku<14><21> sudoku<14><22> sudoku<14><23> sudoku<14><24>) true)))
+ (let (($x2826 (and (distinct sudoku<0><13> sudoku<1><13> sudoku<2><13> sudoku<3><13> sudoku<4><13> sudoku<5><13> sudoku<6><13> sudoku<7><13> sudoku<8><13> sudoku<9><13> sudoku<10><13> sudoku<11><13> sudoku<12><13> sudoku<13><13> sudoku<14><13> sudoku<15><13> sudoku<16><13> sudoku<17><13> sudoku<18><13> sudoku<19><13> sudoku<20><13> sudoku<21><13> sudoku<22><13> sudoku<23><13> sudoku<24><13>) true)))
+ (let (($x2825 (and (distinct sudoku<13><0> sudoku<13><1> sudoku<13><2> sudoku<13><3> sudoku<13><4> sudoku<13><5> sudoku<13><6> sudoku<13><7> sudoku<13><8> sudoku<13><9> sudoku<13><10> sudoku<13><11> sudoku<13><12> sudoku<13><13> sudoku<13><14> sudoku<13><15> sudoku<13><16> sudoku<13><17> sudoku<13><18> sudoku<13><19> sudoku<13><20> sudoku<13><21> sudoku<13><22> sudoku<13><23> sudoku<13><24>) true)))
+ (let (($x2824 (and (distinct sudoku<0><12> sudoku<1><12> sudoku<2><12> sudoku<3><12> sudoku<4><12> sudoku<5><12> sudoku<6><12> sudoku<7><12> sudoku<8><12> sudoku<9><12> sudoku<10><12> sudoku<11><12> sudoku<12><12> sudoku<13><12> sudoku<14><12> sudoku<15><12> sudoku<16><12> sudoku<17><12> sudoku<18><12> sudoku<19><12> sudoku<20><12> sudoku<21><12> sudoku<22><12> sudoku<23><12> sudoku<24><12>) true)))
+ (let (($x2823 (and (distinct sudoku<12><0> sudoku<12><1> sudoku<12><2> sudoku<12><3> sudoku<12><4> sudoku<12><5> sudoku<12><6> sudoku<12><7> sudoku<12><8> sudoku<12><9> sudoku<12><10> sudoku<12><11> sudoku<12><12> sudoku<12><13> sudoku<12><14> sudoku<12><15> sudoku<12><16> sudoku<12><17> sudoku<12><18> sudoku<12><19> sudoku<12><20> sudoku<12><21> sudoku<12><22> sudoku<12><23> sudoku<12><24>) true)))
+ (let (($x2822 (and (distinct sudoku<0><11> sudoku<1><11> sudoku<2><11> sudoku<3><11> sudoku<4><11> sudoku<5><11> sudoku<6><11> sudoku<7><11> sudoku<8><11> sudoku<9><11> sudoku<10><11> sudoku<11><11> sudoku<12><11> sudoku<13><11> sudoku<14><11> sudoku<15><11> sudoku<16><11> sudoku<17><11> sudoku<18><11> sudoku<19><11> sudoku<20><11> sudoku<21><11> sudoku<22><11> sudoku<23><11> sudoku<24><11>) true)))
+ (let (($x2821 (and (distinct sudoku<11><0> sudoku<11><1> sudoku<11><2> sudoku<11><3> sudoku<11><4> sudoku<11><5> sudoku<11><6> sudoku<11><7> sudoku<11><8> sudoku<11><9> sudoku<11><10> sudoku<11><11> sudoku<11><12> sudoku<11><13> sudoku<11><14> sudoku<11><15> sudoku<11><16> sudoku<11><17> sudoku<11><18> sudoku<11><19> sudoku<11><20> sudoku<11><21> sudoku<11><22> sudoku<11><23> sudoku<11><24>) true)))
+ (let (($x2820 (and (distinct sudoku<0><10> sudoku<1><10> sudoku<2><10> sudoku<3><10> sudoku<4><10> sudoku<5><10> sudoku<6><10> sudoku<7><10> sudoku<8><10> sudoku<9><10> sudoku<10><10> sudoku<11><10> sudoku<12><10> sudoku<13><10> sudoku<14><10> sudoku<15><10> sudoku<16><10> sudoku<17><10> sudoku<18><10> sudoku<19><10> sudoku<20><10> sudoku<21><10> sudoku<22><10> sudoku<23><10> sudoku<24><10>) true)))
+ (let (($x2819 (and (distinct sudoku<10><0> sudoku<10><1> sudoku<10><2> sudoku<10><3> sudoku<10><4> sudoku<10><5> sudoku<10><6> sudoku<10><7> sudoku<10><8> sudoku<10><9> sudoku<10><10> sudoku<10><11> sudoku<10><12> sudoku<10><13> sudoku<10><14> sudoku<10><15> sudoku<10><16> sudoku<10><17> sudoku<10><18> sudoku<10><19> sudoku<10><20> sudoku<10><21> sudoku<10><22> sudoku<10><23> sudoku<10><24>) true)))
+ (let (($x2818 (and (distinct sudoku<0><9> sudoku<1><9> sudoku<2><9> sudoku<3><9> sudoku<4><9> sudoku<5><9> sudoku<6><9> sudoku<7><9> sudoku<8><9> sudoku<9><9> sudoku<10><9> sudoku<11><9> sudoku<12><9> sudoku<13><9> sudoku<14><9> sudoku<15><9> sudoku<16><9> sudoku<17><9> sudoku<18><9> sudoku<19><9> sudoku<20><9> sudoku<21><9> sudoku<22><9> sudoku<23><9> sudoku<24><9>) true)))
+ (let (($x2817 (and (distinct sudoku<9><0> sudoku<9><1> sudoku<9><2> sudoku<9><3> sudoku<9><4> sudoku<9><5> sudoku<9><6> sudoku<9><7> sudoku<9><8> sudoku<9><9> sudoku<9><10> sudoku<9><11> sudoku<9><12> sudoku<9><13> sudoku<9><14> sudoku<9><15> sudoku<9><16> sudoku<9><17> sudoku<9><18> sudoku<9><19> sudoku<9><20> sudoku<9><21> sudoku<9><22> sudoku<9><23> sudoku<9><24>) true)))
+ (let (($x2816 (and (distinct sudoku<0><8> sudoku<1><8> sudoku<2><8> sudoku<3><8> sudoku<4><8> sudoku<5><8> sudoku<6><8> sudoku<7><8> sudoku<8><8> sudoku<9><8> sudoku<10><8> sudoku<11><8> sudoku<12><8> sudoku<13><8> sudoku<14><8> sudoku<15><8> sudoku<16><8> sudoku<17><8> sudoku<18><8> sudoku<19><8> sudoku<20><8> sudoku<21><8> sudoku<22><8> sudoku<23><8> sudoku<24><8>) true)))
+ (let (($x2815 (and (distinct sudoku<8><0> sudoku<8><1> sudoku<8><2> sudoku<8><3> sudoku<8><4> sudoku<8><5> sudoku<8><6> sudoku<8><7> sudoku<8><8> sudoku<8><9> sudoku<8><10> sudoku<8><11> sudoku<8><12> sudoku<8><13> sudoku<8><14> sudoku<8><15> sudoku<8><16> sudoku<8><17> sudoku<8><18> sudoku<8><19> sudoku<8><20> sudoku<8><21> sudoku<8><22> sudoku<8><23> sudoku<8><24>) true)))
+ (let (($x2814 (and (distinct sudoku<0><7> sudoku<1><7> sudoku<2><7> sudoku<3><7> sudoku<4><7> sudoku<5><7> sudoku<6><7> sudoku<7><7> sudoku<8><7> sudoku<9><7> sudoku<10><7> sudoku<11><7> sudoku<12><7> sudoku<13><7> sudoku<14><7> sudoku<15><7> sudoku<16><7> sudoku<17><7> sudoku<18><7> sudoku<19><7> sudoku<20><7> sudoku<21><7> sudoku<22><7> sudoku<23><7> sudoku<24><7>) true)))
+ (let (($x2813 (and (distinct sudoku<7><0> sudoku<7><1> sudoku<7><2> sudoku<7><3> sudoku<7><4> sudoku<7><5> sudoku<7><6> sudoku<7><7> sudoku<7><8> sudoku<7><9> sudoku<7><10> sudoku<7><11> sudoku<7><12> sudoku<7><13> sudoku<7><14> sudoku<7><15> sudoku<7><16> sudoku<7><17> sudoku<7><18> sudoku<7><19> sudoku<7><20> sudoku<7><21> sudoku<7><22> sudoku<7><23> sudoku<7><24>) true)))
+ (let (($x2812 (and (distinct sudoku<0><6> sudoku<1><6> sudoku<2><6> sudoku<3><6> sudoku<4><6> sudoku<5><6> sudoku<6><6> sudoku<7><6> sudoku<8><6> sudoku<9><6> sudoku<10><6> sudoku<11><6> sudoku<12><6> sudoku<13><6> sudoku<14><6> sudoku<15><6> sudoku<16><6> sudoku<17><6> sudoku<18><6> sudoku<19><6> sudoku<20><6> sudoku<21><6> sudoku<22><6> sudoku<23><6> sudoku<24><6>) true)))
+ (let (($x2811 (and (distinct sudoku<6><0> sudoku<6><1> sudoku<6><2> sudoku<6><3> sudoku<6><4> sudoku<6><5> sudoku<6><6> sudoku<6><7> sudoku<6><8> sudoku<6><9> sudoku<6><10> sudoku<6><11> sudoku<6><12> sudoku<6><13> sudoku<6><14> sudoku<6><15> sudoku<6><16> sudoku<6><17> sudoku<6><18> sudoku<6><19> sudoku<6><20> sudoku<6><21> sudoku<6><22> sudoku<6><23> sudoku<6><24>) true)))
+ (let (($x2810 (and (distinct sudoku<0><5> sudoku<1><5> sudoku<2><5> sudoku<3><5> sudoku<4><5> sudoku<5><5> sudoku<6><5> sudoku<7><5> sudoku<8><5> sudoku<9><5> sudoku<10><5> sudoku<11><5> sudoku<12><5> sudoku<13><5> sudoku<14><5> sudoku<15><5> sudoku<16><5> sudoku<17><5> sudoku<18><5> sudoku<19><5> sudoku<20><5> sudoku<21><5> sudoku<22><5> sudoku<23><5> sudoku<24><5>) true)))
+ (let (($x2809 (and (distinct sudoku<5><0> sudoku<5><1> sudoku<5><2> sudoku<5><3> sudoku<5><4> sudoku<5><5> sudoku<5><6> sudoku<5><7> sudoku<5><8> sudoku<5><9> sudoku<5><10> sudoku<5><11> sudoku<5><12> sudoku<5><13> sudoku<5><14> sudoku<5><15> sudoku<5><16> sudoku<5><17> sudoku<5><18> sudoku<5><19> sudoku<5><20> sudoku<5><21> sudoku<5><22> sudoku<5><23> sudoku<5><24>) true)))
+ (let (($x2808 (and (distinct sudoku<0><4> sudoku<1><4> sudoku<2><4> sudoku<3><4> sudoku<4><4> sudoku<5><4> sudoku<6><4> sudoku<7><4> sudoku<8><4> sudoku<9><4> sudoku<10><4> sudoku<11><4> sudoku<12><4> sudoku<13><4> sudoku<14><4> sudoku<15><4> sudoku<16><4> sudoku<17><4> sudoku<18><4> sudoku<19><4> sudoku<20><4> sudoku<21><4> sudoku<22><4> sudoku<23><4> sudoku<24><4>) true)))
+ (let (($x2807 (and (distinct sudoku<4><0> sudoku<4><1> sudoku<4><2> sudoku<4><3> sudoku<4><4> sudoku<4><5> sudoku<4><6> sudoku<4><7> sudoku<4><8> sudoku<4><9> sudoku<4><10> sudoku<4><11> sudoku<4><12> sudoku<4><13> sudoku<4><14> sudoku<4><15> sudoku<4><16> sudoku<4><17> sudoku<4><18> sudoku<4><19> sudoku<4><20> sudoku<4><21> sudoku<4><22> sudoku<4><23> sudoku<4><24>) true)))
+ (let (($x2806 (and (distinct sudoku<0><3> sudoku<1><3> sudoku<2><3> sudoku<3><3> sudoku<4><3> sudoku<5><3> sudoku<6><3> sudoku<7><3> sudoku<8><3> sudoku<9><3> sudoku<10><3> sudoku<11><3> sudoku<12><3> sudoku<13><3> sudoku<14><3> sudoku<15><3> sudoku<16><3> sudoku<17><3> sudoku<18><3> sudoku<19><3> sudoku<20><3> sudoku<21><3> sudoku<22><3> sudoku<23><3> sudoku<24><3>) true)))
+ (let (($x2805 (and (distinct sudoku<3><0> sudoku<3><1> sudoku<3><2> sudoku<3><3> sudoku<3><4> sudoku<3><5> sudoku<3><6> sudoku<3><7> sudoku<3><8> sudoku<3><9> sudoku<3><10> sudoku<3><11> sudoku<3><12> sudoku<3><13> sudoku<3><14> sudoku<3><15> sudoku<3><16> sudoku<3><17> sudoku<3><18> sudoku<3><19> sudoku<3><20> sudoku<3><21> sudoku<3><22> sudoku<3><23> sudoku<3><24>) true)))
+ (let (($x2804 (and (distinct sudoku<0><2> sudoku<1><2> sudoku<2><2> sudoku<3><2> sudoku<4><2> sudoku<5><2> sudoku<6><2> sudoku<7><2> sudoku<8><2> sudoku<9><2> sudoku<10><2> sudoku<11><2> sudoku<12><2> sudoku<13><2> sudoku<14><2> sudoku<15><2> sudoku<16><2> sudoku<17><2> sudoku<18><2> sudoku<19><2> sudoku<20><2> sudoku<21><2> sudoku<22><2> sudoku<23><2> sudoku<24><2>) true)))
+ (let (($x2803 (and (distinct sudoku<2><0> sudoku<2><1> sudoku<2><2> sudoku<2><3> sudoku<2><4> sudoku<2><5> sudoku<2><6> sudoku<2><7> sudoku<2><8> sudoku<2><9> sudoku<2><10> sudoku<2><11> sudoku<2><12> sudoku<2><13> sudoku<2><14> sudoku<2><15> sudoku<2><16> sudoku<2><17> sudoku<2><18> sudoku<2><19> sudoku<2><20> sudoku<2><21> sudoku<2><22> sudoku<2><23> sudoku<2><24>) true)))
+ (let (($x2802 (and (distinct sudoku<0><1> sudoku<1><1> sudoku<2><1> sudoku<3><1> sudoku<4><1> sudoku<5><1> sudoku<6><1> sudoku<7><1> sudoku<8><1> sudoku<9><1> sudoku<10><1> sudoku<11><1> sudoku<12><1> sudoku<13><1> sudoku<14><1> sudoku<15><1> sudoku<16><1> sudoku<17><1> sudoku<18><1> sudoku<19><1> sudoku<20><1> sudoku<21><1> sudoku<22><1> sudoku<23><1> sudoku<24><1>) true)))
+ (let (($x2801 (and (distinct sudoku<1><0> sudoku<1><1> sudoku<1><2> sudoku<1><3> sudoku<1><4> sudoku<1><5> sudoku<1><6> sudoku<1><7> sudoku<1><8> sudoku<1><9> sudoku<1><10> sudoku<1><11> sudoku<1><12> sudoku<1><13> sudoku<1><14> sudoku<1><15> sudoku<1><16> sudoku<1><17> sudoku<1><18> sudoku<1><19> sudoku<1><20> sudoku<1><21> sudoku<1><22> sudoku<1><23> sudoku<1><24>) true)))
+ (let (($x2800 (and (distinct sudoku<0><0> sudoku<1><0> sudoku<2><0> sudoku<3><0> sudoku<4><0> sudoku<5><0> sudoku<6><0> sudoku<7><0> sudoku<8><0> sudoku<9><0> sudoku<10><0> sudoku<11><0> sudoku<12><0> sudoku<13><0> sudoku<14><0> sudoku<15><0> sudoku<16><0> sudoku<17><0> sudoku<18><0> sudoku<19><0> sudoku<20><0> sudoku<21><0> sudoku<22><0> sudoku<23><0> sudoku<24><0>) true)))
+ (let (($x2799 (and (distinct sudoku<0><0> sudoku<0><1> sudoku<0><2> sudoku<0><3> sudoku<0><4> sudoku<0><5> sudoku<0><6> sudoku<0><7> sudoku<0><8> sudoku<0><9> sudoku<0><10> sudoku<0><11> sudoku<0><12> sudoku<0><13> sudoku<0><14> sudoku<0><15> sudoku<0><16> sudoku<0><17> sudoku<0><18> sudoku<0><19> sudoku<0><20> sudoku<0><21> sudoku<0><22> sudoku<0><23> sudoku<0><24>) true)))
+ (let (($x2797 (<= sudoku<24><24> 25)))
+ (let (($x2796 (>= sudoku<24><24> 1)))
+ (let (($x2798 (and $x2796 $x2797)))
+ (let (($x2794 (<= sudoku<24><23> 25)))
+ (let (($x2793 (>= sudoku<24><23> 1)))
+ (let (($x2795 (and $x2793 $x2794)))
+ (let (($x2791 (<= sudoku<24><22> 25)))
+ (let (($x2790 (>= sudoku<24><22> 1)))
+ (let (($x2792 (and $x2790 $x2791)))
+ (let (($x2788 (<= sudoku<24><21> 25)))
+ (let (($x2787 (>= sudoku<24><21> 1)))
+ (let (($x2789 (and $x2787 $x2788)))
+ (let (($x2785 (<= sudoku<24><20> 25)))
+ (let (($x2784 (>= sudoku<24><20> 1)))
+ (let (($x2786 (and $x2784 $x2785)))
+ (let (($x2782 (<= sudoku<24><19> 25)))
+ (let (($x2781 (>= sudoku<24><19> 1)))
+ (let (($x2783 (and $x2781 $x2782)))
+ (let (($x2779 (<= sudoku<24><18> 25)))
+ (let (($x2778 (>= sudoku<24><18> 1)))
+ (let (($x2780 (and $x2778 $x2779)))
+ (let (($x2776 (<= sudoku<24><17> 25)))
+ (let (($x2775 (>= sudoku<24><17> 1)))
+ (let (($x2777 (and $x2775 $x2776)))
+ (let (($x2773 (<= sudoku<24><16> 25)))
+ (let (($x2772 (>= sudoku<24><16> 1)))
+ (let (($x2774 (and $x2772 $x2773)))
+ (let (($x2770 (<= sudoku<24><15> 25)))
+ (let (($x2769 (>= sudoku<24><15> 1)))
+ (let (($x2771 (and $x2769 $x2770)))
+ (let (($x2767 (<= sudoku<24><14> 25)))
+ (let (($x2766 (>= sudoku<24><14> 1)))
+ (let (($x2768 (and $x2766 $x2767)))
+ (let (($x2764 (<= sudoku<24><13> 25)))
+ (let (($x2763 (>= sudoku<24><13> 1)))
+ (let (($x2765 (and $x2763 $x2764)))
+ (let (($x2761 (<= sudoku<24><12> 25)))
+ (let (($x2760 (>= sudoku<24><12> 1)))
+ (let (($x2762 (and $x2760 $x2761)))
+ (let (($x2758 (<= sudoku<24><11> 25)))
+ (let (($x2757 (>= sudoku<24><11> 1)))
+ (let (($x2759 (and $x2757 $x2758)))
+ (let (($x2755 (<= sudoku<24><10> 25)))
+ (let (($x2754 (>= sudoku<24><10> 1)))
+ (let (($x2756 (and $x2754 $x2755)))
+ (let (($x2752 (<= sudoku<24><9> 25)))
+ (let (($x2751 (>= sudoku<24><9> 1)))
+ (let (($x2753 (and $x2751 $x2752)))
+ (let (($x2749 (<= sudoku<24><8> 25)))
+ (let (($x2748 (>= sudoku<24><8> 1)))
+ (let (($x2750 (and $x2748 $x2749)))
+ (let (($x2746 (<= sudoku<24><7> 25)))
+ (let (($x2745 (>= sudoku<24><7> 1)))
+ (let (($x2747 (and $x2745 $x2746)))
+ (let (($x2743 (<= sudoku<24><6> 25)))
+ (let (($x2742 (>= sudoku<24><6> 1)))
+ (let (($x2744 (and $x2742 $x2743)))
+ (let (($x2740 (<= sudoku<24><5> 25)))
+ (let (($x2739 (>= sudoku<24><5> 1)))
+ (let (($x2741 (and $x2739 $x2740)))
+ (let (($x2737 (<= sudoku<24><4> 25)))
+ (let (($x2736 (>= sudoku<24><4> 1)))
+ (let (($x2738 (and $x2736 $x2737)))
+ (let (($x2734 (<= sudoku<24><3> 25)))
+ (let (($x2733 (>= sudoku<24><3> 1)))
+ (let (($x2735 (and $x2733 $x2734)))
+ (let (($x2731 (<= sudoku<24><2> 25)))
+ (let (($x2730 (>= sudoku<24><2> 1)))
+ (let (($x2732 (and $x2730 $x2731)))
+ (let (($x2728 (<= sudoku<24><1> 25)))
+ (let (($x2727 (>= sudoku<24><1> 1)))
+ (let (($x2729 (and $x2727 $x2728)))
+ (let (($x2725 (<= sudoku<24><0> 25)))
+ (let (($x2724 (>= sudoku<24><0> 1)))
+ (let (($x2726 (and $x2724 $x2725)))
+ (let (($x2722 (<= sudoku<23><24> 25)))
+ (let (($x2721 (>= sudoku<23><24> 1)))
+ (let (($x2723 (and $x2721 $x2722)))
+ (let (($x2719 (<= sudoku<23><23> 25)))
+ (let (($x2718 (>= sudoku<23><23> 1)))
+ (let (($x2720 (and $x2718 $x2719)))
+ (let (($x2716 (<= sudoku<23><22> 25)))
+ (let (($x2715 (>= sudoku<23><22> 1)))
+ (let (($x2717 (and $x2715 $x2716)))
+ (let (($x2713 (<= sudoku<23><21> 25)))
+ (let (($x2712 (>= sudoku<23><21> 1)))
+ (let (($x2714 (and $x2712 $x2713)))
+ (let (($x2710 (<= sudoku<23><20> 25)))
+ (let (($x2709 (>= sudoku<23><20> 1)))
+ (let (($x2711 (and $x2709 $x2710)))
+ (let (($x2707 (<= sudoku<23><19> 25)))
+ (let (($x2706 (>= sudoku<23><19> 1)))
+ (let (($x2708 (and $x2706 $x2707)))
+ (let (($x2704 (<= sudoku<23><18> 25)))
+ (let (($x2703 (>= sudoku<23><18> 1)))
+ (let (($x2705 (and $x2703 $x2704)))
+ (let (($x2701 (<= sudoku<23><17> 25)))
+ (let (($x2700 (>= sudoku<23><17> 1)))
+ (let (($x2702 (and $x2700 $x2701)))
+ (let (($x2698 (<= sudoku<23><16> 25)))
+ (let (($x2697 (>= sudoku<23><16> 1)))
+ (let (($x2699 (and $x2697 $x2698)))
+ (let (($x2695 (<= sudoku<23><15> 25)))
+ (let (($x2694 (>= sudoku<23><15> 1)))
+ (let (($x2696 (and $x2694 $x2695)))
+ (let (($x2692 (<= sudoku<23><14> 25)))
+ (let (($x2691 (>= sudoku<23><14> 1)))
+ (let (($x2693 (and $x2691 $x2692)))
+ (let (($x2689 (<= sudoku<23><13> 25)))
+ (let (($x2688 (>= sudoku<23><13> 1)))
+ (let (($x2690 (and $x2688 $x2689)))
+ (let (($x2686 (<= sudoku<23><12> 25)))
+ (let (($x2685 (>= sudoku<23><12> 1)))
+ (let (($x2687 (and $x2685 $x2686)))
+ (let (($x2683 (<= sudoku<23><11> 25)))
+ (let (($x2682 (>= sudoku<23><11> 1)))
+ (let (($x2684 (and $x2682 $x2683)))
+ (let (($x2680 (<= sudoku<23><10> 25)))
+ (let (($x2679 (>= sudoku<23><10> 1)))
+ (let (($x2681 (and $x2679 $x2680)))
+ (let (($x2677 (<= sudoku<23><9> 25)))
+ (let (($x2676 (>= sudoku<23><9> 1)))
+ (let (($x2678 (and $x2676 $x2677)))
+ (let (($x2674 (<= sudoku<23><8> 25)))
+ (let (($x2673 (>= sudoku<23><8> 1)))
+ (let (($x2675 (and $x2673 $x2674)))
+ (let (($x2671 (<= sudoku<23><7> 25)))
+ (let (($x2670 (>= sudoku<23><7> 1)))
+ (let (($x2672 (and $x2670 $x2671)))
+ (let (($x2668 (<= sudoku<23><6> 25)))
+ (let (($x2667 (>= sudoku<23><6> 1)))
+ (let (($x2669 (and $x2667 $x2668)))
+ (let (($x2665 (<= sudoku<23><5> 25)))
+ (let (($x2664 (>= sudoku<23><5> 1)))
+ (let (($x2666 (and $x2664 $x2665)))
+ (let (($x2662 (<= sudoku<23><4> 25)))
+ (let (($x2661 (>= sudoku<23><4> 1)))
+ (let (($x2663 (and $x2661 $x2662)))
+ (let (($x2659 (<= sudoku<23><3> 25)))
+ (let (($x2658 (>= sudoku<23><3> 1)))
+ (let (($x2660 (and $x2658 $x2659)))
+ (let (($x2656 (<= sudoku<23><2> 25)))
+ (let (($x2655 (>= sudoku<23><2> 1)))
+ (let (($x2657 (and $x2655 $x2656)))
+ (let (($x2653 (<= sudoku<23><1> 25)))
+ (let (($x2652 (>= sudoku<23><1> 1)))
+ (let (($x2654 (and $x2652 $x2653)))
+ (let (($x2650 (<= sudoku<23><0> 25)))
+ (let (($x2649 (>= sudoku<23><0> 1)))
+ (let (($x2651 (and $x2649 $x2650)))
+ (let (($x2647 (<= sudoku<22><24> 25)))
+ (let (($x2646 (>= sudoku<22><24> 1)))
+ (let (($x2648 (and $x2646 $x2647)))
+ (let (($x2644 (<= sudoku<22><23> 25)))
+ (let (($x2643 (>= sudoku<22><23> 1)))
+ (let (($x2645 (and $x2643 $x2644)))
+ (let (($x2641 (<= sudoku<22><22> 25)))
+ (let (($x2640 (>= sudoku<22><22> 1)))
+ (let (($x2642 (and $x2640 $x2641)))
+ (let (($x2638 (<= sudoku<22><21> 25)))
+ (let (($x2637 (>= sudoku<22><21> 1)))
+ (let (($x2639 (and $x2637 $x2638)))
+ (let (($x2635 (<= sudoku<22><20> 25)))
+ (let (($x2634 (>= sudoku<22><20> 1)))
+ (let (($x2636 (and $x2634 $x2635)))
+ (let (($x2632 (<= sudoku<22><19> 25)))
+ (let (($x2631 (>= sudoku<22><19> 1)))
+ (let (($x2633 (and $x2631 $x2632)))
+ (let (($x2629 (<= sudoku<22><18> 25)))
+ (let (($x2628 (>= sudoku<22><18> 1)))
+ (let (($x2630 (and $x2628 $x2629)))
+ (let (($x2626 (<= sudoku<22><17> 25)))
+ (let (($x2625 (>= sudoku<22><17> 1)))
+ (let (($x2627 (and $x2625 $x2626)))
+ (let (($x2623 (<= sudoku<22><16> 25)))
+ (let (($x2622 (>= sudoku<22><16> 1)))
+ (let (($x2624 (and $x2622 $x2623)))
+ (let (($x2620 (<= sudoku<22><15> 25)))
+ (let (($x2619 (>= sudoku<22><15> 1)))
+ (let (($x2621 (and $x2619 $x2620)))
+ (let (($x2617 (<= sudoku<22><14> 25)))
+ (let (($x2616 (>= sudoku<22><14> 1)))
+ (let (($x2618 (and $x2616 $x2617)))
+ (let (($x2614 (<= sudoku<22><13> 25)))
+ (let (($x2613 (>= sudoku<22><13> 1)))
+ (let (($x2615 (and $x2613 $x2614)))
+ (let (($x2611 (<= sudoku<22><12> 25)))
+ (let (($x2610 (>= sudoku<22><12> 1)))
+ (let (($x2612 (and $x2610 $x2611)))
+ (let (($x2608 (<= sudoku<22><11> 25)))
+ (let (($x2607 (>= sudoku<22><11> 1)))
+ (let (($x2609 (and $x2607 $x2608)))
+ (let (($x2605 (<= sudoku<22><10> 25)))
+ (let (($x2604 (>= sudoku<22><10> 1)))
+ (let (($x2606 (and $x2604 $x2605)))
+ (let (($x2602 (<= sudoku<22><9> 25)))
+ (let (($x2601 (>= sudoku<22><9> 1)))
+ (let (($x2603 (and $x2601 $x2602)))
+ (let (($x2599 (<= sudoku<22><8> 25)))
+ (let (($x2598 (>= sudoku<22><8> 1)))
+ (let (($x2600 (and $x2598 $x2599)))
+ (let (($x2596 (<= sudoku<22><7> 25)))
+ (let (($x2595 (>= sudoku<22><7> 1)))
+ (let (($x2597 (and $x2595 $x2596)))
+ (let (($x2593 (<= sudoku<22><6> 25)))
+ (let (($x2592 (>= sudoku<22><6> 1)))
+ (let (($x2594 (and $x2592 $x2593)))
+ (let (($x2590 (<= sudoku<22><5> 25)))
+ (let (($x2589 (>= sudoku<22><5> 1)))
+ (let (($x2591 (and $x2589 $x2590)))
+ (let (($x2587 (<= sudoku<22><4> 25)))
+ (let (($x2586 (>= sudoku<22><4> 1)))
+ (let (($x2588 (and $x2586 $x2587)))
+ (let (($x2584 (<= sudoku<22><3> 25)))
+ (let (($x2583 (>= sudoku<22><3> 1)))
+ (let (($x2585 (and $x2583 $x2584)))
+ (let (($x2581 (<= sudoku<22><2> 25)))
+ (let (($x2580 (>= sudoku<22><2> 1)))
+ (let (($x2582 (and $x2580 $x2581)))
+ (let (($x2578 (<= sudoku<22><1> 25)))
+ (let (($x2577 (>= sudoku<22><1> 1)))
+ (let (($x2579 (and $x2577 $x2578)))
+ (let (($x2575 (<= sudoku<22><0> 25)))
+ (let (($x2574 (>= sudoku<22><0> 1)))
+ (let (($x2576 (and $x2574 $x2575)))
+ (let (($x2572 (<= sudoku<21><24> 25)))
+ (let (($x2571 (>= sudoku<21><24> 1)))
+ (let (($x2573 (and $x2571 $x2572)))
+ (let (($x2569 (<= sudoku<21><23> 25)))
+ (let (($x2568 (>= sudoku<21><23> 1)))
+ (let (($x2570 (and $x2568 $x2569)))
+ (let (($x2566 (<= sudoku<21><22> 25)))
+ (let (($x2565 (>= sudoku<21><22> 1)))
+ (let (($x2567 (and $x2565 $x2566)))
+ (let (($x2563 (<= sudoku<21><21> 25)))
+ (let (($x2562 (>= sudoku<21><21> 1)))
+ (let (($x2564 (and $x2562 $x2563)))
+ (let (($x2560 (<= sudoku<21><20> 25)))
+ (let (($x2559 (>= sudoku<21><20> 1)))
+ (let (($x2561 (and $x2559 $x2560)))
+ (let (($x2557 (<= sudoku<21><19> 25)))
+ (let (($x2556 (>= sudoku<21><19> 1)))
+ (let (($x2558 (and $x2556 $x2557)))
+ (let (($x2554 (<= sudoku<21><18> 25)))
+ (let (($x2553 (>= sudoku<21><18> 1)))
+ (let (($x2555 (and $x2553 $x2554)))
+ (let (($x2551 (<= sudoku<21><17> 25)))
+ (let (($x2550 (>= sudoku<21><17> 1)))
+ (let (($x2552 (and $x2550 $x2551)))
+ (let (($x2548 (<= sudoku<21><16> 25)))
+ (let (($x2547 (>= sudoku<21><16> 1)))
+ (let (($x2549 (and $x2547 $x2548)))
+ (let (($x2545 (<= sudoku<21><15> 25)))
+ (let (($x2544 (>= sudoku<21><15> 1)))
+ (let (($x2546 (and $x2544 $x2545)))
+ (let (($x2542 (<= sudoku<21><14> 25)))
+ (let (($x2541 (>= sudoku<21><14> 1)))
+ (let (($x2543 (and $x2541 $x2542)))
+ (let (($x2539 (<= sudoku<21><13> 25)))
+ (let (($x2538 (>= sudoku<21><13> 1)))
+ (let (($x2540 (and $x2538 $x2539)))
+ (let (($x2536 (<= sudoku<21><12> 25)))
+ (let (($x2535 (>= sudoku<21><12> 1)))
+ (let (($x2537 (and $x2535 $x2536)))
+ (let (($x2533 (<= sudoku<21><11> 25)))
+ (let (($x2532 (>= sudoku<21><11> 1)))
+ (let (($x2534 (and $x2532 $x2533)))
+ (let (($x2530 (<= sudoku<21><10> 25)))
+ (let (($x2529 (>= sudoku<21><10> 1)))
+ (let (($x2531 (and $x2529 $x2530)))
+ (let (($x2527 (<= sudoku<21><9> 25)))
+ (let (($x2526 (>= sudoku<21><9> 1)))
+ (let (($x2528 (and $x2526 $x2527)))
+ (let (($x2524 (<= sudoku<21><8> 25)))
+ (let (($x2523 (>= sudoku<21><8> 1)))
+ (let (($x2525 (and $x2523 $x2524)))
+ (let (($x2521 (<= sudoku<21><7> 25)))
+ (let (($x2520 (>= sudoku<21><7> 1)))
+ (let (($x2522 (and $x2520 $x2521)))
+ (let (($x2518 (<= sudoku<21><6> 25)))
+ (let (($x2517 (>= sudoku<21><6> 1)))
+ (let (($x2519 (and $x2517 $x2518)))
+ (let (($x2515 (<= sudoku<21><5> 25)))
+ (let (($x2514 (>= sudoku<21><5> 1)))
+ (let (($x2516 (and $x2514 $x2515)))
+ (let (($x2512 (<= sudoku<21><4> 25)))
+ (let (($x2511 (>= sudoku<21><4> 1)))
+ (let (($x2513 (and $x2511 $x2512)))
+ (let (($x2509 (<= sudoku<21><3> 25)))
+ (let (($x2508 (>= sudoku<21><3> 1)))
+ (let (($x2510 (and $x2508 $x2509)))
+ (let (($x2506 (<= sudoku<21><2> 25)))
+ (let (($x2505 (>= sudoku<21><2> 1)))
+ (let (($x2507 (and $x2505 $x2506)))
+ (let (($x2503 (<= sudoku<21><1> 25)))
+ (let (($x2502 (>= sudoku<21><1> 1)))
+ (let (($x2504 (and $x2502 $x2503)))
+ (let (($x2500 (<= sudoku<21><0> 25)))
+ (let (($x2499 (>= sudoku<21><0> 1)))
+ (let (($x2501 (and $x2499 $x2500)))
+ (let (($x2497 (<= sudoku<20><24> 25)))
+ (let (($x2496 (>= sudoku<20><24> 1)))
+ (let (($x2498 (and $x2496 $x2497)))
+ (let (($x2494 (<= sudoku<20><23> 25)))
+ (let (($x2493 (>= sudoku<20><23> 1)))
+ (let (($x2495 (and $x2493 $x2494)))
+ (let (($x2491 (<= sudoku<20><22> 25)))
+ (let (($x2490 (>= sudoku<20><22> 1)))
+ (let (($x2492 (and $x2490 $x2491)))
+ (let (($x2488 (<= sudoku<20><21> 25)))
+ (let (($x2487 (>= sudoku<20><21> 1)))
+ (let (($x2489 (and $x2487 $x2488)))
+ (let (($x2485 (<= sudoku<20><20> 25)))
+ (let (($x2484 (>= sudoku<20><20> 1)))
+ (let (($x2486 (and $x2484 $x2485)))
+ (let (($x2482 (<= sudoku<20><19> 25)))
+ (let (($x2481 (>= sudoku<20><19> 1)))
+ (let (($x2483 (and $x2481 $x2482)))
+ (let (($x2479 (<= sudoku<20><18> 25)))
+ (let (($x2478 (>= sudoku<20><18> 1)))
+ (let (($x2480 (and $x2478 $x2479)))
+ (let (($x2476 (<= sudoku<20><17> 25)))
+ (let (($x2475 (>= sudoku<20><17> 1)))
+ (let (($x2477 (and $x2475 $x2476)))
+ (let (($x2473 (<= sudoku<20><16> 25)))
+ (let (($x2472 (>= sudoku<20><16> 1)))
+ (let (($x2474 (and $x2472 $x2473)))
+ (let (($x2470 (<= sudoku<20><15> 25)))
+ (let (($x2469 (>= sudoku<20><15> 1)))
+ (let (($x2471 (and $x2469 $x2470)))
+ (let (($x2467 (<= sudoku<20><14> 25)))
+ (let (($x2466 (>= sudoku<20><14> 1)))
+ (let (($x2468 (and $x2466 $x2467)))
+ (let (($x2464 (<= sudoku<20><13> 25)))
+ (let (($x2463 (>= sudoku<20><13> 1)))
+ (let (($x2465 (and $x2463 $x2464)))
+ (let (($x2461 (<= sudoku<20><12> 25)))
+ (let (($x2460 (>= sudoku<20><12> 1)))
+ (let (($x2462 (and $x2460 $x2461)))
+ (let (($x2458 (<= sudoku<20><11> 25)))
+ (let (($x2457 (>= sudoku<20><11> 1)))
+ (let (($x2459 (and $x2457 $x2458)))
+ (let (($x2455 (<= sudoku<20><10> 25)))
+ (let (($x2454 (>= sudoku<20><10> 1)))
+ (let (($x2456 (and $x2454 $x2455)))
+ (let (($x2452 (<= sudoku<20><9> 25)))
+ (let (($x2451 (>= sudoku<20><9> 1)))
+ (let (($x2453 (and $x2451 $x2452)))
+ (let (($x2449 (<= sudoku<20><8> 25)))
+ (let (($x2448 (>= sudoku<20><8> 1)))
+ (let (($x2450 (and $x2448 $x2449)))
+ (let (($x2446 (<= sudoku<20><7> 25)))
+ (let (($x2445 (>= sudoku<20><7> 1)))
+ (let (($x2447 (and $x2445 $x2446)))
+ (let (($x2443 (<= sudoku<20><6> 25)))
+ (let (($x2442 (>= sudoku<20><6> 1)))
+ (let (($x2444 (and $x2442 $x2443)))
+ (let (($x2440 (<= sudoku<20><5> 25)))
+ (let (($x2439 (>= sudoku<20><5> 1)))
+ (let (($x2441 (and $x2439 $x2440)))
+ (let (($x2437 (<= sudoku<20><4> 25)))
+ (let (($x2436 (>= sudoku<20><4> 1)))
+ (let (($x2438 (and $x2436 $x2437)))
+ (let (($x2434 (<= sudoku<20><3> 25)))
+ (let (($x2433 (>= sudoku<20><3> 1)))
+ (let (($x2435 (and $x2433 $x2434)))
+ (let (($x2431 (<= sudoku<20><2> 25)))
+ (let (($x2430 (>= sudoku<20><2> 1)))
+ (let (($x2432 (and $x2430 $x2431)))
+ (let (($x2428 (<= sudoku<20><1> 25)))
+ (let (($x2427 (>= sudoku<20><1> 1)))
+ (let (($x2429 (and $x2427 $x2428)))
+ (let (($x2425 (<= sudoku<20><0> 25)))
+ (let (($x2424 (>= sudoku<20><0> 1)))
+ (let (($x2426 (and $x2424 $x2425)))
+ (let (($x2422 (<= sudoku<19><24> 25)))
+ (let (($x2421 (>= sudoku<19><24> 1)))
+ (let (($x2423 (and $x2421 $x2422)))
+ (let (($x2419 (<= sudoku<19><23> 25)))
+ (let (($x2418 (>= sudoku<19><23> 1)))
+ (let (($x2420 (and $x2418 $x2419)))
+ (let (($x2416 (<= sudoku<19><22> 25)))
+ (let (($x2415 (>= sudoku<19><22> 1)))
+ (let (($x2417 (and $x2415 $x2416)))
+ (let (($x2413 (<= sudoku<19><21> 25)))
+ (let (($x2412 (>= sudoku<19><21> 1)))
+ (let (($x2414 (and $x2412 $x2413)))
+ (let (($x2410 (<= sudoku<19><20> 25)))
+ (let (($x2409 (>= sudoku<19><20> 1)))
+ (let (($x2411 (and $x2409 $x2410)))
+ (let (($x2407 (<= sudoku<19><19> 25)))
+ (let (($x2406 (>= sudoku<19><19> 1)))
+ (let (($x2408 (and $x2406 $x2407)))
+ (let (($x2404 (<= sudoku<19><18> 25)))
+ (let (($x2403 (>= sudoku<19><18> 1)))
+ (let (($x2405 (and $x2403 $x2404)))
+ (let (($x2401 (<= sudoku<19><17> 25)))
+ (let (($x2400 (>= sudoku<19><17> 1)))
+ (let (($x2402 (and $x2400 $x2401)))
+ (let (($x2398 (<= sudoku<19><16> 25)))
+ (let (($x2397 (>= sudoku<19><16> 1)))
+ (let (($x2399 (and $x2397 $x2398)))
+ (let (($x2395 (<= sudoku<19><15> 25)))
+ (let (($x2394 (>= sudoku<19><15> 1)))
+ (let (($x2396 (and $x2394 $x2395)))
+ (let (($x2392 (<= sudoku<19><14> 25)))
+ (let (($x2391 (>= sudoku<19><14> 1)))
+ (let (($x2393 (and $x2391 $x2392)))
+ (let (($x2389 (<= sudoku<19><13> 25)))
+ (let (($x2388 (>= sudoku<19><13> 1)))
+ (let (($x2390 (and $x2388 $x2389)))
+ (let (($x2386 (<= sudoku<19><12> 25)))
+ (let (($x2385 (>= sudoku<19><12> 1)))
+ (let (($x2387 (and $x2385 $x2386)))
+ (let (($x2383 (<= sudoku<19><11> 25)))
+ (let (($x2382 (>= sudoku<19><11> 1)))
+ (let (($x2384 (and $x2382 $x2383)))
+ (let (($x2380 (<= sudoku<19><10> 25)))
+ (let (($x2379 (>= sudoku<19><10> 1)))
+ (let (($x2381 (and $x2379 $x2380)))
+ (let (($x2377 (<= sudoku<19><9> 25)))
+ (let (($x2376 (>= sudoku<19><9> 1)))
+ (let (($x2378 (and $x2376 $x2377)))
+ (let (($x2374 (<= sudoku<19><8> 25)))
+ (let (($x2373 (>= sudoku<19><8> 1)))
+ (let (($x2375 (and $x2373 $x2374)))
+ (let (($x2371 (<= sudoku<19><7> 25)))
+ (let (($x2370 (>= sudoku<19><7> 1)))
+ (let (($x2372 (and $x2370 $x2371)))
+ (let (($x2368 (<= sudoku<19><6> 25)))
+ (let (($x2367 (>= sudoku<19><6> 1)))
+ (let (($x2369 (and $x2367 $x2368)))
+ (let (($x2365 (<= sudoku<19><5> 25)))
+ (let (($x2364 (>= sudoku<19><5> 1)))
+ (let (($x2366 (and $x2364 $x2365)))
+ (let (($x2362 (<= sudoku<19><4> 25)))
+ (let (($x2361 (>= sudoku<19><4> 1)))
+ (let (($x2363 (and $x2361 $x2362)))
+ (let (($x2359 (<= sudoku<19><3> 25)))
+ (let (($x2358 (>= sudoku<19><3> 1)))
+ (let (($x2360 (and $x2358 $x2359)))
+ (let (($x2356 (<= sudoku<19><2> 25)))
+ (let (($x2355 (>= sudoku<19><2> 1)))
+ (let (($x2357 (and $x2355 $x2356)))
+ (let (($x2353 (<= sudoku<19><1> 25)))
+ (let (($x2352 (>= sudoku<19><1> 1)))
+ (let (($x2354 (and $x2352 $x2353)))
+ (let (($x2350 (<= sudoku<19><0> 25)))
+ (let (($x2349 (>= sudoku<19><0> 1)))
+ (let (($x2351 (and $x2349 $x2350)))
+ (let (($x2347 (<= sudoku<18><24> 25)))
+ (let (($x2346 (>= sudoku<18><24> 1)))
+ (let (($x2348 (and $x2346 $x2347)))
+ (let (($x2344 (<= sudoku<18><23> 25)))
+ (let (($x2343 (>= sudoku<18><23> 1)))
+ (let (($x2345 (and $x2343 $x2344)))
+ (let (($x2341 (<= sudoku<18><22> 25)))
+ (let (($x2340 (>= sudoku<18><22> 1)))
+ (let (($x2342 (and $x2340 $x2341)))
+ (let (($x2338 (<= sudoku<18><21> 25)))
+ (let (($x2337 (>= sudoku<18><21> 1)))
+ (let (($x2339 (and $x2337 $x2338)))
+ (let (($x2335 (<= sudoku<18><20> 25)))
+ (let (($x2334 (>= sudoku<18><20> 1)))
+ (let (($x2336 (and $x2334 $x2335)))
+ (let (($x2332 (<= sudoku<18><19> 25)))
+ (let (($x2331 (>= sudoku<18><19> 1)))
+ (let (($x2333 (and $x2331 $x2332)))
+ (let (($x2329 (<= sudoku<18><18> 25)))
+ (let (($x2328 (>= sudoku<18><18> 1)))
+ (let (($x2330 (and $x2328 $x2329)))
+ (let (($x2326 (<= sudoku<18><17> 25)))
+ (let (($x2325 (>= sudoku<18><17> 1)))
+ (let (($x2327 (and $x2325 $x2326)))
+ (let (($x2323 (<= sudoku<18><16> 25)))
+ (let (($x2322 (>= sudoku<18><16> 1)))
+ (let (($x2324 (and $x2322 $x2323)))
+ (let (($x2320 (<= sudoku<18><15> 25)))
+ (let (($x2319 (>= sudoku<18><15> 1)))
+ (let (($x2321 (and $x2319 $x2320)))
+ (let (($x2317 (<= sudoku<18><14> 25)))
+ (let (($x2316 (>= sudoku<18><14> 1)))
+ (let (($x2318 (and $x2316 $x2317)))
+ (let (($x2314 (<= sudoku<18><13> 25)))
+ (let (($x2313 (>= sudoku<18><13> 1)))
+ (let (($x2315 (and $x2313 $x2314)))
+ (let (($x2311 (<= sudoku<18><12> 25)))
+ (let (($x2310 (>= sudoku<18><12> 1)))
+ (let (($x2312 (and $x2310 $x2311)))
+ (let (($x2308 (<= sudoku<18><11> 25)))
+ (let (($x2307 (>= sudoku<18><11> 1)))
+ (let (($x2309 (and $x2307 $x2308)))
+ (let (($x2305 (<= sudoku<18><10> 25)))
+ (let (($x2304 (>= sudoku<18><10> 1)))
+ (let (($x2306 (and $x2304 $x2305)))
+ (let (($x2302 (<= sudoku<18><9> 25)))
+ (let (($x2301 (>= sudoku<18><9> 1)))
+ (let (($x2303 (and $x2301 $x2302)))
+ (let (($x2299 (<= sudoku<18><8> 25)))
+ (let (($x2298 (>= sudoku<18><8> 1)))
+ (let (($x2300 (and $x2298 $x2299)))
+ (let (($x2296 (<= sudoku<18><7> 25)))
+ (let (($x2295 (>= sudoku<18><7> 1)))
+ (let (($x2297 (and $x2295 $x2296)))
+ (let (($x2293 (<= sudoku<18><6> 25)))
+ (let (($x2292 (>= sudoku<18><6> 1)))
+ (let (($x2294 (and $x2292 $x2293)))
+ (let (($x2290 (<= sudoku<18><5> 25)))
+ (let (($x2289 (>= sudoku<18><5> 1)))
+ (let (($x2291 (and $x2289 $x2290)))
+ (let (($x2287 (<= sudoku<18><4> 25)))
+ (let (($x2286 (>= sudoku<18><4> 1)))
+ (let (($x2288 (and $x2286 $x2287)))
+ (let (($x2284 (<= sudoku<18><3> 25)))
+ (let (($x2283 (>= sudoku<18><3> 1)))
+ (let (($x2285 (and $x2283 $x2284)))
+ (let (($x2281 (<= sudoku<18><2> 25)))
+ (let (($x2280 (>= sudoku<18><2> 1)))
+ (let (($x2282 (and $x2280 $x2281)))
+ (let (($x2278 (<= sudoku<18><1> 25)))
+ (let (($x2277 (>= sudoku<18><1> 1)))
+ (let (($x2279 (and $x2277 $x2278)))
+ (let (($x2275 (<= sudoku<18><0> 25)))
+ (let (($x2274 (>= sudoku<18><0> 1)))
+ (let (($x2276 (and $x2274 $x2275)))
+ (let (($x2272 (<= sudoku<17><24> 25)))
+ (let (($x2271 (>= sudoku<17><24> 1)))
+ (let (($x2273 (and $x2271 $x2272)))
+ (let (($x2269 (<= sudoku<17><23> 25)))
+ (let (($x2268 (>= sudoku<17><23> 1)))
+ (let (($x2270 (and $x2268 $x2269)))
+ (let (($x2266 (<= sudoku<17><22> 25)))
+ (let (($x2265 (>= sudoku<17><22> 1)))
+ (let (($x2267 (and $x2265 $x2266)))
+ (let (($x2263 (<= sudoku<17><21> 25)))
+ (let (($x2262 (>= sudoku<17><21> 1)))
+ (let (($x2264 (and $x2262 $x2263)))
+ (let (($x2260 (<= sudoku<17><20> 25)))
+ (let (($x2259 (>= sudoku<17><20> 1)))
+ (let (($x2261 (and $x2259 $x2260)))
+ (let (($x2257 (<= sudoku<17><19> 25)))
+ (let (($x2256 (>= sudoku<17><19> 1)))
+ (let (($x2258 (and $x2256 $x2257)))
+ (let (($x2254 (<= sudoku<17><18> 25)))
+ (let (($x2253 (>= sudoku<17><18> 1)))
+ (let (($x2255 (and $x2253 $x2254)))
+ (let (($x2251 (<= sudoku<17><17> 25)))
+ (let (($x2250 (>= sudoku<17><17> 1)))
+ (let (($x2252 (and $x2250 $x2251)))
+ (let (($x2248 (<= sudoku<17><16> 25)))
+ (let (($x2247 (>= sudoku<17><16> 1)))
+ (let (($x2249 (and $x2247 $x2248)))
+ (let (($x2245 (<= sudoku<17><15> 25)))
+ (let (($x2244 (>= sudoku<17><15> 1)))
+ (let (($x2246 (and $x2244 $x2245)))
+ (let (($x2242 (<= sudoku<17><14> 25)))
+ (let (($x2241 (>= sudoku<17><14> 1)))
+ (let (($x2243 (and $x2241 $x2242)))
+ (let (($x2239 (<= sudoku<17><13> 25)))
+ (let (($x2238 (>= sudoku<17><13> 1)))
+ (let (($x2240 (and $x2238 $x2239)))
+ (let (($x2236 (<= sudoku<17><12> 25)))
+ (let (($x2235 (>= sudoku<17><12> 1)))
+ (let (($x2237 (and $x2235 $x2236)))
+ (let (($x2233 (<= sudoku<17><11> 25)))
+ (let (($x2232 (>= sudoku<17><11> 1)))
+ (let (($x2234 (and $x2232 $x2233)))
+ (let (($x2230 (<= sudoku<17><10> 25)))
+ (let (($x2229 (>= sudoku<17><10> 1)))
+ (let (($x2231 (and $x2229 $x2230)))
+ (let (($x2227 (<= sudoku<17><9> 25)))
+ (let (($x2226 (>= sudoku<17><9> 1)))
+ (let (($x2228 (and $x2226 $x2227)))
+ (let (($x2224 (<= sudoku<17><8> 25)))
+ (let (($x2223 (>= sudoku<17><8> 1)))
+ (let (($x2225 (and $x2223 $x2224)))
+ (let (($x2221 (<= sudoku<17><7> 25)))
+ (let (($x2220 (>= sudoku<17><7> 1)))
+ (let (($x2222 (and $x2220 $x2221)))
+ (let (($x2218 (<= sudoku<17><6> 25)))
+ (let (($x2217 (>= sudoku<17><6> 1)))
+ (let (($x2219 (and $x2217 $x2218)))
+ (let (($x2215 (<= sudoku<17><5> 25)))
+ (let (($x2214 (>= sudoku<17><5> 1)))
+ (let (($x2216 (and $x2214 $x2215)))
+ (let (($x2212 (<= sudoku<17><4> 25)))
+ (let (($x2211 (>= sudoku<17><4> 1)))
+ (let (($x2213 (and $x2211 $x2212)))
+ (let (($x2209 (<= sudoku<17><3> 25)))
+ (let (($x2208 (>= sudoku<17><3> 1)))
+ (let (($x2210 (and $x2208 $x2209)))
+ (let (($x2206 (<= sudoku<17><2> 25)))
+ (let (($x2205 (>= sudoku<17><2> 1)))
+ (let (($x2207 (and $x2205 $x2206)))
+ (let (($x2203 (<= sudoku<17><1> 25)))
+ (let (($x2202 (>= sudoku<17><1> 1)))
+ (let (($x2204 (and $x2202 $x2203)))
+ (let (($x2200 (<= sudoku<17><0> 25)))
+ (let (($x2199 (>= sudoku<17><0> 1)))
+ (let (($x2201 (and $x2199 $x2200)))
+ (let (($x2197 (<= sudoku<16><24> 25)))
+ (let (($x2196 (>= sudoku<16><24> 1)))
+ (let (($x2198 (and $x2196 $x2197)))
+ (let (($x2194 (<= sudoku<16><23> 25)))
+ (let (($x2193 (>= sudoku<16><23> 1)))
+ (let (($x2195 (and $x2193 $x2194)))
+ (let (($x2191 (<= sudoku<16><22> 25)))
+ (let (($x2190 (>= sudoku<16><22> 1)))
+ (let (($x2192 (and $x2190 $x2191)))
+ (let (($x2188 (<= sudoku<16><21> 25)))
+ (let (($x2187 (>= sudoku<16><21> 1)))
+ (let (($x2189 (and $x2187 $x2188)))
+ (let (($x2185 (<= sudoku<16><20> 25)))
+ (let (($x2184 (>= sudoku<16><20> 1)))
+ (let (($x2186 (and $x2184 $x2185)))
+ (let (($x2182 (<= sudoku<16><19> 25)))
+ (let (($x2181 (>= sudoku<16><19> 1)))
+ (let (($x2183 (and $x2181 $x2182)))
+ (let (($x2179 (<= sudoku<16><18> 25)))
+ (let (($x2178 (>= sudoku<16><18> 1)))
+ (let (($x2180 (and $x2178 $x2179)))
+ (let (($x2176 (<= sudoku<16><17> 25)))
+ (let (($x2175 (>= sudoku<16><17> 1)))
+ (let (($x2177 (and $x2175 $x2176)))
+ (let (($x2173 (<= sudoku<16><16> 25)))
+ (let (($x2172 (>= sudoku<16><16> 1)))
+ (let (($x2174 (and $x2172 $x2173)))
+ (let (($x2170 (<= sudoku<16><15> 25)))
+ (let (($x2169 (>= sudoku<16><15> 1)))
+ (let (($x2171 (and $x2169 $x2170)))
+ (let (($x2167 (<= sudoku<16><14> 25)))
+ (let (($x2166 (>= sudoku<16><14> 1)))
+ (let (($x2168 (and $x2166 $x2167)))
+ (let (($x2164 (<= sudoku<16><13> 25)))
+ (let (($x2163 (>= sudoku<16><13> 1)))
+ (let (($x2165 (and $x2163 $x2164)))
+ (let (($x2161 (<= sudoku<16><12> 25)))
+ (let (($x2160 (>= sudoku<16><12> 1)))
+ (let (($x2162 (and $x2160 $x2161)))
+ (let (($x2158 (<= sudoku<16><11> 25)))
+ (let (($x2157 (>= sudoku<16><11> 1)))
+ (let (($x2159 (and $x2157 $x2158)))
+ (let (($x2155 (<= sudoku<16><10> 25)))
+ (let (($x2154 (>= sudoku<16><10> 1)))
+ (let (($x2156 (and $x2154 $x2155)))
+ (let (($x2152 (<= sudoku<16><9> 25)))
+ (let (($x2151 (>= sudoku<16><9> 1)))
+ (let (($x2153 (and $x2151 $x2152)))
+ (let (($x2149 (<= sudoku<16><8> 25)))
+ (let (($x2148 (>= sudoku<16><8> 1)))
+ (let (($x2150 (and $x2148 $x2149)))
+ (let (($x2146 (<= sudoku<16><7> 25)))
+ (let (($x2145 (>= sudoku<16><7> 1)))
+ (let (($x2147 (and $x2145 $x2146)))
+ (let (($x2143 (<= sudoku<16><6> 25)))
+ (let (($x2142 (>= sudoku<16><6> 1)))
+ (let (($x2144 (and $x2142 $x2143)))
+ (let (($x2140 (<= sudoku<16><5> 25)))
+ (let (($x2139 (>= sudoku<16><5> 1)))
+ (let (($x2141 (and $x2139 $x2140)))
+ (let (($x2137 (<= sudoku<16><4> 25)))
+ (let (($x2136 (>= sudoku<16><4> 1)))
+ (let (($x2138 (and $x2136 $x2137)))
+ (let (($x2134 (<= sudoku<16><3> 25)))
+ (let (($x2133 (>= sudoku<16><3> 1)))
+ (let (($x2135 (and $x2133 $x2134)))
+ (let (($x2131 (<= sudoku<16><2> 25)))
+ (let (($x2130 (>= sudoku<16><2> 1)))
+ (let (($x2132 (and $x2130 $x2131)))
+ (let (($x2128 (<= sudoku<16><1> 25)))
+ (let (($x2127 (>= sudoku<16><1> 1)))
+ (let (($x2129 (and $x2127 $x2128)))
+ (let (($x2125 (<= sudoku<16><0> 25)))
+ (let (($x2124 (>= sudoku<16><0> 1)))
+ (let (($x2126 (and $x2124 $x2125)))
+ (let (($x2122 (<= sudoku<15><24> 25)))
+ (let (($x2121 (>= sudoku<15><24> 1)))
+ (let (($x2123 (and $x2121 $x2122)))
+ (let (($x2119 (<= sudoku<15><23> 25)))
+ (let (($x2118 (>= sudoku<15><23> 1)))
+ (let (($x2120 (and $x2118 $x2119)))
+ (let (($x2116 (<= sudoku<15><22> 25)))
+ (let (($x2115 (>= sudoku<15><22> 1)))
+ (let (($x2117 (and $x2115 $x2116)))
+ (let (($x2113 (<= sudoku<15><21> 25)))
+ (let (($x2112 (>= sudoku<15><21> 1)))
+ (let (($x2114 (and $x2112 $x2113)))
+ (let (($x2110 (<= sudoku<15><20> 25)))
+ (let (($x2109 (>= sudoku<15><20> 1)))
+ (let (($x2111 (and $x2109 $x2110)))
+ (let (($x2107 (<= sudoku<15><19> 25)))
+ (let (($x2106 (>= sudoku<15><19> 1)))
+ (let (($x2108 (and $x2106 $x2107)))
+ (let (($x2104 (<= sudoku<15><18> 25)))
+ (let (($x2103 (>= sudoku<15><18> 1)))
+ (let (($x2105 (and $x2103 $x2104)))
+ (let (($x2101 (<= sudoku<15><17> 25)))
+ (let (($x2100 (>= sudoku<15><17> 1)))
+ (let (($x2102 (and $x2100 $x2101)))
+ (let (($x2098 (<= sudoku<15><16> 25)))
+ (let (($x2097 (>= sudoku<15><16> 1)))
+ (let (($x2099 (and $x2097 $x2098)))
+ (let (($x2095 (<= sudoku<15><15> 25)))
+ (let (($x2094 (>= sudoku<15><15> 1)))
+ (let (($x2096 (and $x2094 $x2095)))
+ (let (($x2092 (<= sudoku<15><14> 25)))
+ (let (($x2091 (>= sudoku<15><14> 1)))
+ (let (($x2093 (and $x2091 $x2092)))
+ (let (($x2089 (<= sudoku<15><13> 25)))
+ (let (($x2088 (>= sudoku<15><13> 1)))
+ (let (($x2090 (and $x2088 $x2089)))
+ (let (($x2086 (<= sudoku<15><12> 25)))
+ (let (($x2085 (>= sudoku<15><12> 1)))
+ (let (($x2087 (and $x2085 $x2086)))
+ (let (($x2083 (<= sudoku<15><11> 25)))
+ (let (($x2082 (>= sudoku<15><11> 1)))
+ (let (($x2084 (and $x2082 $x2083)))
+ (let (($x2080 (<= sudoku<15><10> 25)))
+ (let (($x2079 (>= sudoku<15><10> 1)))
+ (let (($x2081 (and $x2079 $x2080)))
+ (let (($x2077 (<= sudoku<15><9> 25)))
+ (let (($x2076 (>= sudoku<15><9> 1)))
+ (let (($x2078 (and $x2076 $x2077)))
+ (let (($x2074 (<= sudoku<15><8> 25)))
+ (let (($x2073 (>= sudoku<15><8> 1)))
+ (let (($x2075 (and $x2073 $x2074)))
+ (let (($x2071 (<= sudoku<15><7> 25)))
+ (let (($x2070 (>= sudoku<15><7> 1)))
+ (let (($x2072 (and $x2070 $x2071)))
+ (let (($x2068 (<= sudoku<15><6> 25)))
+ (let (($x2067 (>= sudoku<15><6> 1)))
+ (let (($x2069 (and $x2067 $x2068)))
+ (let (($x2065 (<= sudoku<15><5> 25)))
+ (let (($x2064 (>= sudoku<15><5> 1)))
+ (let (($x2066 (and $x2064 $x2065)))
+ (let (($x2062 (<= sudoku<15><4> 25)))
+ (let (($x2061 (>= sudoku<15><4> 1)))
+ (let (($x2063 (and $x2061 $x2062)))
+ (let (($x2059 (<= sudoku<15><3> 25)))
+ (let (($x2058 (>= sudoku<15><3> 1)))
+ (let (($x2060 (and $x2058 $x2059)))
+ (let (($x2056 (<= sudoku<15><2> 25)))
+ (let (($x2055 (>= sudoku<15><2> 1)))
+ (let (($x2057 (and $x2055 $x2056)))
+ (let (($x2053 (<= sudoku<15><1> 25)))
+ (let (($x2052 (>= sudoku<15><1> 1)))
+ (let (($x2054 (and $x2052 $x2053)))
+ (let (($x2050 (<= sudoku<15><0> 25)))
+ (let (($x2049 (>= sudoku<15><0> 1)))
+ (let (($x2051 (and $x2049 $x2050)))
+ (let (($x2047 (<= sudoku<14><24> 25)))
+ (let (($x2046 (>= sudoku<14><24> 1)))
+ (let (($x2048 (and $x2046 $x2047)))
+ (let (($x2044 (<= sudoku<14><23> 25)))
+ (let (($x2043 (>= sudoku<14><23> 1)))
+ (let (($x2045 (and $x2043 $x2044)))
+ (let (($x2041 (<= sudoku<14><22> 25)))
+ (let (($x2040 (>= sudoku<14><22> 1)))
+ (let (($x2042 (and $x2040 $x2041)))
+ (let (($x2038 (<= sudoku<14><21> 25)))
+ (let (($x2037 (>= sudoku<14><21> 1)))
+ (let (($x2039 (and $x2037 $x2038)))
+ (let (($x2035 (<= sudoku<14><20> 25)))
+ (let (($x2034 (>= sudoku<14><20> 1)))
+ (let (($x2036 (and $x2034 $x2035)))
+ (let (($x2032 (<= sudoku<14><19> 25)))
+ (let (($x2031 (>= sudoku<14><19> 1)))
+ (let (($x2033 (and $x2031 $x2032)))
+ (let (($x2029 (<= sudoku<14><18> 25)))
+ (let (($x2028 (>= sudoku<14><18> 1)))
+ (let (($x2030 (and $x2028 $x2029)))
+ (let (($x2026 (<= sudoku<14><17> 25)))
+ (let (($x2025 (>= sudoku<14><17> 1)))
+ (let (($x2027 (and $x2025 $x2026)))
+ (let (($x2023 (<= sudoku<14><16> 25)))
+ (let (($x2022 (>= sudoku<14><16> 1)))
+ (let (($x2024 (and $x2022 $x2023)))
+ (let (($x2020 (<= sudoku<14><15> 25)))
+ (let (($x2019 (>= sudoku<14><15> 1)))
+ (let (($x2021 (and $x2019 $x2020)))
+ (let (($x2017 (<= sudoku<14><14> 25)))
+ (let (($x2016 (>= sudoku<14><14> 1)))
+ (let (($x2018 (and $x2016 $x2017)))
+ (let (($x2014 (<= sudoku<14><13> 25)))
+ (let (($x2013 (>= sudoku<14><13> 1)))
+ (let (($x2015 (and $x2013 $x2014)))
+ (let (($x2011 (<= sudoku<14><12> 25)))
+ (let (($x2010 (>= sudoku<14><12> 1)))
+ (let (($x2012 (and $x2010 $x2011)))
+ (let (($x2008 (<= sudoku<14><11> 25)))
+ (let (($x2007 (>= sudoku<14><11> 1)))
+ (let (($x2009 (and $x2007 $x2008)))
+ (let (($x2005 (<= sudoku<14><10> 25)))
+ (let (($x2004 (>= sudoku<14><10> 1)))
+ (let (($x2006 (and $x2004 $x2005)))
+ (let (($x2002 (<= sudoku<14><9> 25)))
+ (let (($x2001 (>= sudoku<14><9> 1)))
+ (let (($x2003 (and $x2001 $x2002)))
+ (let (($x1999 (<= sudoku<14><8> 25)))
+ (let (($x1998 (>= sudoku<14><8> 1)))
+ (let (($x2000 (and $x1998 $x1999)))
+ (let (($x1996 (<= sudoku<14><7> 25)))
+ (let (($x1995 (>= sudoku<14><7> 1)))
+ (let (($x1997 (and $x1995 $x1996)))
+ (let (($x1993 (<= sudoku<14><6> 25)))
+ (let (($x1992 (>= sudoku<14><6> 1)))
+ (let (($x1994 (and $x1992 $x1993)))
+ (let (($x1990 (<= sudoku<14><5> 25)))
+ (let (($x1989 (>= sudoku<14><5> 1)))
+ (let (($x1991 (and $x1989 $x1990)))
+ (let (($x1987 (<= sudoku<14><4> 25)))
+ (let (($x1986 (>= sudoku<14><4> 1)))
+ (let (($x1988 (and $x1986 $x1987)))
+ (let (($x1984 (<= sudoku<14><3> 25)))
+ (let (($x1983 (>= sudoku<14><3> 1)))
+ (let (($x1985 (and $x1983 $x1984)))
+ (let (($x1981 (<= sudoku<14><2> 25)))
+ (let (($x1980 (>= sudoku<14><2> 1)))
+ (let (($x1982 (and $x1980 $x1981)))
+ (let (($x1978 (<= sudoku<14><1> 25)))
+ (let (($x1977 (>= sudoku<14><1> 1)))
+ (let (($x1979 (and $x1977 $x1978)))
+ (let (($x1975 (<= sudoku<14><0> 25)))
+ (let (($x1974 (>= sudoku<14><0> 1)))
+ (let (($x1976 (and $x1974 $x1975)))
+ (let (($x1972 (<= sudoku<13><24> 25)))
+ (let (($x1971 (>= sudoku<13><24> 1)))
+ (let (($x1973 (and $x1971 $x1972)))
+ (let (($x1969 (<= sudoku<13><23> 25)))
+ (let (($x1968 (>= sudoku<13><23> 1)))
+ (let (($x1970 (and $x1968 $x1969)))
+ (let (($x1966 (<= sudoku<13><22> 25)))
+ (let (($x1965 (>= sudoku<13><22> 1)))
+ (let (($x1967 (and $x1965 $x1966)))
+ (let (($x1963 (<= sudoku<13><21> 25)))
+ (let (($x1962 (>= sudoku<13><21> 1)))
+ (let (($x1964 (and $x1962 $x1963)))
+ (let (($x1960 (<= sudoku<13><20> 25)))
+ (let (($x1959 (>= sudoku<13><20> 1)))
+ (let (($x1961 (and $x1959 $x1960)))
+ (let (($x1957 (<= sudoku<13><19> 25)))
+ (let (($x1956 (>= sudoku<13><19> 1)))
+ (let (($x1958 (and $x1956 $x1957)))
+ (let (($x1954 (<= sudoku<13><18> 25)))
+ (let (($x1953 (>= sudoku<13><18> 1)))
+ (let (($x1955 (and $x1953 $x1954)))
+ (let (($x1951 (<= sudoku<13><17> 25)))
+ (let (($x1950 (>= sudoku<13><17> 1)))
+ (let (($x1952 (and $x1950 $x1951)))
+ (let (($x1948 (<= sudoku<13><16> 25)))
+ (let (($x1947 (>= sudoku<13><16> 1)))
+ (let (($x1949 (and $x1947 $x1948)))
+ (let (($x1945 (<= sudoku<13><15> 25)))
+ (let (($x1944 (>= sudoku<13><15> 1)))
+ (let (($x1946 (and $x1944 $x1945)))
+ (let (($x1942 (<= sudoku<13><14> 25)))
+ (let (($x1941 (>= sudoku<13><14> 1)))
+ (let (($x1943 (and $x1941 $x1942)))
+ (let (($x1939 (<= sudoku<13><13> 25)))
+ (let (($x1938 (>= sudoku<13><13> 1)))
+ (let (($x1940 (and $x1938 $x1939)))
+ (let (($x1936 (<= sudoku<13><12> 25)))
+ (let (($x1935 (>= sudoku<13><12> 1)))
+ (let (($x1937 (and $x1935 $x1936)))
+ (let (($x1933 (<= sudoku<13><11> 25)))
+ (let (($x1932 (>= sudoku<13><11> 1)))
+ (let (($x1934 (and $x1932 $x1933)))
+ (let (($x1930 (<= sudoku<13><10> 25)))
+ (let (($x1929 (>= sudoku<13><10> 1)))
+ (let (($x1931 (and $x1929 $x1930)))
+ (let (($x1927 (<= sudoku<13><9> 25)))
+ (let (($x1926 (>= sudoku<13><9> 1)))
+ (let (($x1928 (and $x1926 $x1927)))
+ (let (($x1924 (<= sudoku<13><8> 25)))
+ (let (($x1923 (>= sudoku<13><8> 1)))
+ (let (($x1925 (and $x1923 $x1924)))
+ (let (($x1921 (<= sudoku<13><7> 25)))
+ (let (($x1920 (>= sudoku<13><7> 1)))
+ (let (($x1922 (and $x1920 $x1921)))
+ (let (($x1918 (<= sudoku<13><6> 25)))
+ (let (($x1917 (>= sudoku<13><6> 1)))
+ (let (($x1919 (and $x1917 $x1918)))
+ (let (($x1915 (<= sudoku<13><5> 25)))
+ (let (($x1914 (>= sudoku<13><5> 1)))
+ (let (($x1916 (and $x1914 $x1915)))
+ (let (($x1912 (<= sudoku<13><4> 25)))
+ (let (($x1911 (>= sudoku<13><4> 1)))
+ (let (($x1913 (and $x1911 $x1912)))
+ (let (($x1909 (<= sudoku<13><3> 25)))
+ (let (($x1908 (>= sudoku<13><3> 1)))
+ (let (($x1910 (and $x1908 $x1909)))
+ (let (($x1906 (<= sudoku<13><2> 25)))
+ (let (($x1905 (>= sudoku<13><2> 1)))
+ (let (($x1907 (and $x1905 $x1906)))
+ (let (($x1903 (<= sudoku<13><1> 25)))
+ (let (($x1902 (>= sudoku<13><1> 1)))
+ (let (($x1904 (and $x1902 $x1903)))
+ (let (($x1900 (<= sudoku<13><0> 25)))
+ (let (($x1899 (>= sudoku<13><0> 1)))
+ (let (($x1901 (and $x1899 $x1900)))
+ (let (($x1897 (<= sudoku<12><24> 25)))
+ (let (($x1896 (>= sudoku<12><24> 1)))
+ (let (($x1898 (and $x1896 $x1897)))
+ (let (($x1894 (<= sudoku<12><23> 25)))
+ (let (($x1893 (>= sudoku<12><23> 1)))
+ (let (($x1895 (and $x1893 $x1894)))
+ (let (($x1891 (<= sudoku<12><22> 25)))
+ (let (($x1890 (>= sudoku<12><22> 1)))
+ (let (($x1892 (and $x1890 $x1891)))
+ (let (($x1888 (<= sudoku<12><21> 25)))
+ (let (($x1887 (>= sudoku<12><21> 1)))
+ (let (($x1889 (and $x1887 $x1888)))
+ (let (($x1885 (<= sudoku<12><20> 25)))
+ (let (($x1884 (>= sudoku<12><20> 1)))
+ (let (($x1886 (and $x1884 $x1885)))
+ (let (($x1882 (<= sudoku<12><19> 25)))
+ (let (($x1881 (>= sudoku<12><19> 1)))
+ (let (($x1883 (and $x1881 $x1882)))
+ (let (($x1879 (<= sudoku<12><18> 25)))
+ (let (($x1878 (>= sudoku<12><18> 1)))
+ (let (($x1880 (and $x1878 $x1879)))
+ (let (($x1876 (<= sudoku<12><17> 25)))
+ (let (($x1875 (>= sudoku<12><17> 1)))
+ (let (($x1877 (and $x1875 $x1876)))
+ (let (($x1873 (<= sudoku<12><16> 25)))
+ (let (($x1872 (>= sudoku<12><16> 1)))
+ (let (($x1874 (and $x1872 $x1873)))
+ (let (($x1870 (<= sudoku<12><15> 25)))
+ (let (($x1869 (>= sudoku<12><15> 1)))
+ (let (($x1871 (and $x1869 $x1870)))
+ (let (($x1867 (<= sudoku<12><14> 25)))
+ (let (($x1866 (>= sudoku<12><14> 1)))
+ (let (($x1868 (and $x1866 $x1867)))
+ (let (($x1864 (<= sudoku<12><13> 25)))
+ (let (($x1863 (>= sudoku<12><13> 1)))
+ (let (($x1865 (and $x1863 $x1864)))
+ (let (($x1861 (<= sudoku<12><12> 25)))
+ (let (($x1860 (>= sudoku<12><12> 1)))
+ (let (($x1862 (and $x1860 $x1861)))
+ (let (($x1858 (<= sudoku<12><11> 25)))
+ (let (($x1857 (>= sudoku<12><11> 1)))
+ (let (($x1859 (and $x1857 $x1858)))
+ (let (($x1855 (<= sudoku<12><10> 25)))
+ (let (($x1854 (>= sudoku<12><10> 1)))
+ (let (($x1856 (and $x1854 $x1855)))
+ (let (($x1852 (<= sudoku<12><9> 25)))
+ (let (($x1851 (>= sudoku<12><9> 1)))
+ (let (($x1853 (and $x1851 $x1852)))
+ (let (($x1849 (<= sudoku<12><8> 25)))
+ (let (($x1848 (>= sudoku<12><8> 1)))
+ (let (($x1850 (and $x1848 $x1849)))
+ (let (($x1846 (<= sudoku<12><7> 25)))
+ (let (($x1845 (>= sudoku<12><7> 1)))
+ (let (($x1847 (and $x1845 $x1846)))
+ (let (($x1843 (<= sudoku<12><6> 25)))
+ (let (($x1842 (>= sudoku<12><6> 1)))
+ (let (($x1844 (and $x1842 $x1843)))
+ (let (($x1840 (<= sudoku<12><5> 25)))
+ (let (($x1839 (>= sudoku<12><5> 1)))
+ (let (($x1841 (and $x1839 $x1840)))
+ (let (($x1837 (<= sudoku<12><4> 25)))
+ (let (($x1836 (>= sudoku<12><4> 1)))
+ (let (($x1838 (and $x1836 $x1837)))
+ (let (($x1834 (<= sudoku<12><3> 25)))
+ (let (($x1833 (>= sudoku<12><3> 1)))
+ (let (($x1835 (and $x1833 $x1834)))
+ (let (($x1831 (<= sudoku<12><2> 25)))
+ (let (($x1830 (>= sudoku<12><2> 1)))
+ (let (($x1832 (and $x1830 $x1831)))
+ (let (($x1828 (<= sudoku<12><1> 25)))
+ (let (($x1827 (>= sudoku<12><1> 1)))
+ (let (($x1829 (and $x1827 $x1828)))
+ (let (($x1825 (<= sudoku<12><0> 25)))
+ (let (($x1824 (>= sudoku<12><0> 1)))
+ (let (($x1826 (and $x1824 $x1825)))
+ (let (($x1822 (<= sudoku<11><24> 25)))
+ (let (($x1821 (>= sudoku<11><24> 1)))
+ (let (($x1823 (and $x1821 $x1822)))
+ (let (($x1819 (<= sudoku<11><23> 25)))
+ (let (($x1818 (>= sudoku<11><23> 1)))
+ (let (($x1820 (and $x1818 $x1819)))
+ (let (($x1816 (<= sudoku<11><22> 25)))
+ (let (($x1815 (>= sudoku<11><22> 1)))
+ (let (($x1817 (and $x1815 $x1816)))
+ (let (($x1813 (<= sudoku<11><21> 25)))
+ (let (($x1812 (>= sudoku<11><21> 1)))
+ (let (($x1814 (and $x1812 $x1813)))
+ (let (($x1810 (<= sudoku<11><20> 25)))
+ (let (($x1809 (>= sudoku<11><20> 1)))
+ (let (($x1811 (and $x1809 $x1810)))
+ (let (($x1807 (<= sudoku<11><19> 25)))
+ (let (($x1806 (>= sudoku<11><19> 1)))
+ (let (($x1808 (and $x1806 $x1807)))
+ (let (($x1804 (<= sudoku<11><18> 25)))
+ (let (($x1803 (>= sudoku<11><18> 1)))
+ (let (($x1805 (and $x1803 $x1804)))
+ (let (($x1801 (<= sudoku<11><17> 25)))
+ (let (($x1800 (>= sudoku<11><17> 1)))
+ (let (($x1802 (and $x1800 $x1801)))
+ (let (($x1798 (<= sudoku<11><16> 25)))
+ (let (($x1797 (>= sudoku<11><16> 1)))
+ (let (($x1799 (and $x1797 $x1798)))
+ (let (($x1795 (<= sudoku<11><15> 25)))
+ (let (($x1794 (>= sudoku<11><15> 1)))
+ (let (($x1796 (and $x1794 $x1795)))
+ (let (($x1792 (<= sudoku<11><14> 25)))
+ (let (($x1791 (>= sudoku<11><14> 1)))
+ (let (($x1793 (and $x1791 $x1792)))
+ (let (($x1789 (<= sudoku<11><13> 25)))
+ (let (($x1788 (>= sudoku<11><13> 1)))
+ (let (($x1790 (and $x1788 $x1789)))
+ (let (($x1786 (<= sudoku<11><12> 25)))
+ (let (($x1785 (>= sudoku<11><12> 1)))
+ (let (($x1787 (and $x1785 $x1786)))
+ (let (($x1783 (<= sudoku<11><11> 25)))
+ (let (($x1782 (>= sudoku<11><11> 1)))
+ (let (($x1784 (and $x1782 $x1783)))
+ (let (($x1780 (<= sudoku<11><10> 25)))
+ (let (($x1779 (>= sudoku<11><10> 1)))
+ (let (($x1781 (and $x1779 $x1780)))
+ (let (($x1777 (<= sudoku<11><9> 25)))
+ (let (($x1776 (>= sudoku<11><9> 1)))
+ (let (($x1778 (and $x1776 $x1777)))
+ (let (($x1774 (<= sudoku<11><8> 25)))
+ (let (($x1773 (>= sudoku<11><8> 1)))
+ (let (($x1775 (and $x1773 $x1774)))
+ (let (($x1771 (<= sudoku<11><7> 25)))
+ (let (($x1770 (>= sudoku<11><7> 1)))
+ (let (($x1772 (and $x1770 $x1771)))
+ (let (($x1768 (<= sudoku<11><6> 25)))
+ (let (($x1767 (>= sudoku<11><6> 1)))
+ (let (($x1769 (and $x1767 $x1768)))
+ (let (($x1765 (<= sudoku<11><5> 25)))
+ (let (($x1764 (>= sudoku<11><5> 1)))
+ (let (($x1766 (and $x1764 $x1765)))
+ (let (($x1762 (<= sudoku<11><4> 25)))
+ (let (($x1761 (>= sudoku<11><4> 1)))
+ (let (($x1763 (and $x1761 $x1762)))
+ (let (($x1759 (<= sudoku<11><3> 25)))
+ (let (($x1758 (>= sudoku<11><3> 1)))
+ (let (($x1760 (and $x1758 $x1759)))
+ (let (($x1756 (<= sudoku<11><2> 25)))
+ (let (($x1755 (>= sudoku<11><2> 1)))
+ (let (($x1757 (and $x1755 $x1756)))
+ (let (($x1753 (<= sudoku<11><1> 25)))
+ (let (($x1752 (>= sudoku<11><1> 1)))
+ (let (($x1754 (and $x1752 $x1753)))
+ (let (($x1750 (<= sudoku<11><0> 25)))
+ (let (($x1749 (>= sudoku<11><0> 1)))
+ (let (($x1751 (and $x1749 $x1750)))
+ (let (($x1747 (<= sudoku<10><24> 25)))
+ (let (($x1746 (>= sudoku<10><24> 1)))
+ (let (($x1748 (and $x1746 $x1747)))
+ (let (($x1744 (<= sudoku<10><23> 25)))
+ (let (($x1743 (>= sudoku<10><23> 1)))
+ (let (($x1745 (and $x1743 $x1744)))
+ (let (($x1741 (<= sudoku<10><22> 25)))
+ (let (($x1740 (>= sudoku<10><22> 1)))
+ (let (($x1742 (and $x1740 $x1741)))
+ (let (($x1738 (<= sudoku<10><21> 25)))
+ (let (($x1737 (>= sudoku<10><21> 1)))
+ (let (($x1739 (and $x1737 $x1738)))
+ (let (($x1735 (<= sudoku<10><20> 25)))
+ (let (($x1734 (>= sudoku<10><20> 1)))
+ (let (($x1736 (and $x1734 $x1735)))
+ (let (($x1732 (<= sudoku<10><19> 25)))
+ (let (($x1731 (>= sudoku<10><19> 1)))
+ (let (($x1733 (and $x1731 $x1732)))
+ (let (($x1729 (<= sudoku<10><18> 25)))
+ (let (($x1728 (>= sudoku<10><18> 1)))
+ (let (($x1730 (and $x1728 $x1729)))
+ (let (($x1726 (<= sudoku<10><17> 25)))
+ (let (($x1725 (>= sudoku<10><17> 1)))
+ (let (($x1727 (and $x1725 $x1726)))
+ (let (($x1723 (<= sudoku<10><16> 25)))
+ (let (($x1722 (>= sudoku<10><16> 1)))
+ (let (($x1724 (and $x1722 $x1723)))
+ (let (($x1720 (<= sudoku<10><15> 25)))
+ (let (($x1719 (>= sudoku<10><15> 1)))
+ (let (($x1721 (and $x1719 $x1720)))
+ (let (($x1717 (<= sudoku<10><14> 25)))
+ (let (($x1716 (>= sudoku<10><14> 1)))
+ (let (($x1718 (and $x1716 $x1717)))
+ (let (($x1714 (<= sudoku<10><13> 25)))
+ (let (($x1713 (>= sudoku<10><13> 1)))
+ (let (($x1715 (and $x1713 $x1714)))
+ (let (($x1711 (<= sudoku<10><12> 25)))
+ (let (($x1710 (>= sudoku<10><12> 1)))
+ (let (($x1712 (and $x1710 $x1711)))
+ (let (($x1708 (<= sudoku<10><11> 25)))
+ (let (($x1707 (>= sudoku<10><11> 1)))
+ (let (($x1709 (and $x1707 $x1708)))
+ (let (($x1705 (<= sudoku<10><10> 25)))
+ (let (($x1704 (>= sudoku<10><10> 1)))
+ (let (($x1706 (and $x1704 $x1705)))
+ (let (($x1702 (<= sudoku<10><9> 25)))
+ (let (($x1701 (>= sudoku<10><9> 1)))
+ (let (($x1703 (and $x1701 $x1702)))
+ (let (($x1699 (<= sudoku<10><8> 25)))
+ (let (($x1698 (>= sudoku<10><8> 1)))
+ (let (($x1700 (and $x1698 $x1699)))
+ (let (($x1696 (<= sudoku<10><7> 25)))
+ (let (($x1695 (>= sudoku<10><7> 1)))
+ (let (($x1697 (and $x1695 $x1696)))
+ (let (($x1693 (<= sudoku<10><6> 25)))
+ (let (($x1692 (>= sudoku<10><6> 1)))
+ (let (($x1694 (and $x1692 $x1693)))
+ (let (($x1690 (<= sudoku<10><5> 25)))
+ (let (($x1689 (>= sudoku<10><5> 1)))
+ (let (($x1691 (and $x1689 $x1690)))
+ (let (($x1687 (<= sudoku<10><4> 25)))
+ (let (($x1686 (>= sudoku<10><4> 1)))
+ (let (($x1688 (and $x1686 $x1687)))
+ (let (($x1684 (<= sudoku<10><3> 25)))
+ (let (($x1683 (>= sudoku<10><3> 1)))
+ (let (($x1685 (and $x1683 $x1684)))
+ (let (($x1681 (<= sudoku<10><2> 25)))
+ (let (($x1680 (>= sudoku<10><2> 1)))
+ (let (($x1682 (and $x1680 $x1681)))
+ (let (($x1678 (<= sudoku<10><1> 25)))
+ (let (($x1677 (>= sudoku<10><1> 1)))
+ (let (($x1679 (and $x1677 $x1678)))
+ (let (($x1675 (<= sudoku<10><0> 25)))
+ (let (($x1674 (>= sudoku<10><0> 1)))
+ (let (($x1676 (and $x1674 $x1675)))
+ (let (($x1672 (<= sudoku<9><24> 25)))
+ (let (($x1671 (>= sudoku<9><24> 1)))
+ (let (($x1673 (and $x1671 $x1672)))
+ (let (($x1669 (<= sudoku<9><23> 25)))
+ (let (($x1668 (>= sudoku<9><23> 1)))
+ (let (($x1670 (and $x1668 $x1669)))
+ (let (($x1666 (<= sudoku<9><22> 25)))
+ (let (($x1665 (>= sudoku<9><22> 1)))
+ (let (($x1667 (and $x1665 $x1666)))
+ (let (($x1663 (<= sudoku<9><21> 25)))
+ (let (($x1662 (>= sudoku<9><21> 1)))
+ (let (($x1664 (and $x1662 $x1663)))
+ (let (($x1660 (<= sudoku<9><20> 25)))
+ (let (($x1659 (>= sudoku<9><20> 1)))
+ (let (($x1661 (and $x1659 $x1660)))
+ (let (($x1657 (<= sudoku<9><19> 25)))
+ (let (($x1656 (>= sudoku<9><19> 1)))
+ (let (($x1658 (and $x1656 $x1657)))
+ (let (($x1654 (<= sudoku<9><18> 25)))
+ (let (($x1653 (>= sudoku<9><18> 1)))
+ (let (($x1655 (and $x1653 $x1654)))
+ (let (($x1651 (<= sudoku<9><17> 25)))
+ (let (($x1650 (>= sudoku<9><17> 1)))
+ (let (($x1652 (and $x1650 $x1651)))
+ (let (($x1648 (<= sudoku<9><16> 25)))
+ (let (($x1647 (>= sudoku<9><16> 1)))
+ (let (($x1649 (and $x1647 $x1648)))
+ (let (($x1645 (<= sudoku<9><15> 25)))
+ (let (($x1644 (>= sudoku<9><15> 1)))
+ (let (($x1646 (and $x1644 $x1645)))
+ (let (($x1642 (<= sudoku<9><14> 25)))
+ (let (($x1641 (>= sudoku<9><14> 1)))
+ (let (($x1643 (and $x1641 $x1642)))
+ (let (($x1639 (<= sudoku<9><13> 25)))
+ (let (($x1638 (>= sudoku<9><13> 1)))
+ (let (($x1640 (and $x1638 $x1639)))
+ (let (($x1636 (<= sudoku<9><12> 25)))
+ (let (($x1635 (>= sudoku<9><12> 1)))
+ (let (($x1637 (and $x1635 $x1636)))
+ (let (($x1633 (<= sudoku<9><11> 25)))
+ (let (($x1632 (>= sudoku<9><11> 1)))
+ (let (($x1634 (and $x1632 $x1633)))
+ (let (($x1630 (<= sudoku<9><10> 25)))
+ (let (($x1629 (>= sudoku<9><10> 1)))
+ (let (($x1631 (and $x1629 $x1630)))
+ (let (($x1627 (<= sudoku<9><9> 25)))
+ (let (($x1626 (>= sudoku<9><9> 1)))
+ (let (($x1628 (and $x1626 $x1627)))
+ (let (($x1624 (<= sudoku<9><8> 25)))
+ (let (($x1623 (>= sudoku<9><8> 1)))
+ (let (($x1625 (and $x1623 $x1624)))
+ (let (($x1621 (<= sudoku<9><7> 25)))
+ (let (($x1620 (>= sudoku<9><7> 1)))
+ (let (($x1622 (and $x1620 $x1621)))
+ (let (($x1618 (<= sudoku<9><6> 25)))
+ (let (($x1617 (>= sudoku<9><6> 1)))
+ (let (($x1619 (and $x1617 $x1618)))
+ (let (($x1615 (<= sudoku<9><5> 25)))
+ (let (($x1614 (>= sudoku<9><5> 1)))
+ (let (($x1616 (and $x1614 $x1615)))
+ (let (($x1612 (<= sudoku<9><4> 25)))
+ (let (($x1611 (>= sudoku<9><4> 1)))
+ (let (($x1613 (and $x1611 $x1612)))
+ (let (($x1609 (<= sudoku<9><3> 25)))
+ (let (($x1608 (>= sudoku<9><3> 1)))
+ (let (($x1610 (and $x1608 $x1609)))
+ (let (($x1606 (<= sudoku<9><2> 25)))
+ (let (($x1605 (>= sudoku<9><2> 1)))
+ (let (($x1607 (and $x1605 $x1606)))
+ (let (($x1603 (<= sudoku<9><1> 25)))
+ (let (($x1602 (>= sudoku<9><1> 1)))
+ (let (($x1604 (and $x1602 $x1603)))
+ (let (($x1600 (<= sudoku<9><0> 25)))
+ (let (($x1599 (>= sudoku<9><0> 1)))
+ (let (($x1601 (and $x1599 $x1600)))
+ (let (($x1597 (<= sudoku<8><24> 25)))
+ (let (($x1596 (>= sudoku<8><24> 1)))
+ (let (($x1598 (and $x1596 $x1597)))
+ (let (($x1594 (<= sudoku<8><23> 25)))
+ (let (($x1593 (>= sudoku<8><23> 1)))
+ (let (($x1595 (and $x1593 $x1594)))
+ (let (($x1591 (<= sudoku<8><22> 25)))
+ (let (($x1590 (>= sudoku<8><22> 1)))
+ (let (($x1592 (and $x1590 $x1591)))
+ (let (($x1588 (<= sudoku<8><21> 25)))
+ (let (($x1587 (>= sudoku<8><21> 1)))
+ (let (($x1589 (and $x1587 $x1588)))
+ (let (($x1585 (<= sudoku<8><20> 25)))
+ (let (($x1584 (>= sudoku<8><20> 1)))
+ (let (($x1586 (and $x1584 $x1585)))
+ (let (($x1582 (<= sudoku<8><19> 25)))
+ (let (($x1581 (>= sudoku<8><19> 1)))
+ (let (($x1583 (and $x1581 $x1582)))
+ (let (($x1579 (<= sudoku<8><18> 25)))
+ (let (($x1578 (>= sudoku<8><18> 1)))
+ (let (($x1580 (and $x1578 $x1579)))
+ (let (($x1576 (<= sudoku<8><17> 25)))
+ (let (($x1575 (>= sudoku<8><17> 1)))
+ (let (($x1577 (and $x1575 $x1576)))
+ (let (($x1573 (<= sudoku<8><16> 25)))
+ (let (($x1572 (>= sudoku<8><16> 1)))
+ (let (($x1574 (and $x1572 $x1573)))
+ (let (($x1570 (<= sudoku<8><15> 25)))
+ (let (($x1569 (>= sudoku<8><15> 1)))
+ (let (($x1571 (and $x1569 $x1570)))
+ (let (($x1567 (<= sudoku<8><14> 25)))
+ (let (($x1566 (>= sudoku<8><14> 1)))
+ (let (($x1568 (and $x1566 $x1567)))
+ (let (($x1564 (<= sudoku<8><13> 25)))
+ (let (($x1563 (>= sudoku<8><13> 1)))
+ (let (($x1565 (and $x1563 $x1564)))
+ (let (($x1561 (<= sudoku<8><12> 25)))
+ (let (($x1560 (>= sudoku<8><12> 1)))
+ (let (($x1562 (and $x1560 $x1561)))
+ (let (($x1558 (<= sudoku<8><11> 25)))
+ (let (($x1557 (>= sudoku<8><11> 1)))
+ (let (($x1559 (and $x1557 $x1558)))
+ (let (($x1555 (<= sudoku<8><10> 25)))
+ (let (($x1554 (>= sudoku<8><10> 1)))
+ (let (($x1556 (and $x1554 $x1555)))
+ (let (($x1552 (<= sudoku<8><9> 25)))
+ (let (($x1551 (>= sudoku<8><9> 1)))
+ (let (($x1553 (and $x1551 $x1552)))
+ (let (($x1549 (<= sudoku<8><8> 25)))
+ (let (($x1548 (>= sudoku<8><8> 1)))
+ (let (($x1550 (and $x1548 $x1549)))
+ (let (($x1546 (<= sudoku<8><7> 25)))
+ (let (($x1545 (>= sudoku<8><7> 1)))
+ (let (($x1547 (and $x1545 $x1546)))
+ (let (($x1543 (<= sudoku<8><6> 25)))
+ (let (($x1542 (>= sudoku<8><6> 1)))
+ (let (($x1544 (and $x1542 $x1543)))
+ (let (($x1540 (<= sudoku<8><5> 25)))
+ (let (($x1539 (>= sudoku<8><5> 1)))
+ (let (($x1541 (and $x1539 $x1540)))
+ (let (($x1537 (<= sudoku<8><4> 25)))
+ (let (($x1536 (>= sudoku<8><4> 1)))
+ (let (($x1538 (and $x1536 $x1537)))
+ (let (($x1534 (<= sudoku<8><3> 25)))
+ (let (($x1533 (>= sudoku<8><3> 1)))
+ (let (($x1535 (and $x1533 $x1534)))
+ (let (($x1531 (<= sudoku<8><2> 25)))
+ (let (($x1530 (>= sudoku<8><2> 1)))
+ (let (($x1532 (and $x1530 $x1531)))
+ (let (($x1528 (<= sudoku<8><1> 25)))
+ (let (($x1527 (>= sudoku<8><1> 1)))
+ (let (($x1529 (and $x1527 $x1528)))
+ (let (($x1525 (<= sudoku<8><0> 25)))
+ (let (($x1524 (>= sudoku<8><0> 1)))
+ (let (($x1526 (and $x1524 $x1525)))
+ (let (($x1522 (<= sudoku<7><24> 25)))
+ (let (($x1521 (>= sudoku<7><24> 1)))
+ (let (($x1523 (and $x1521 $x1522)))
+ (let (($x1519 (<= sudoku<7><23> 25)))
+ (let (($x1518 (>= sudoku<7><23> 1)))
+ (let (($x1520 (and $x1518 $x1519)))
+ (let (($x1516 (<= sudoku<7><22> 25)))
+ (let (($x1515 (>= sudoku<7><22> 1)))
+ (let (($x1517 (and $x1515 $x1516)))
+ (let (($x1513 (<= sudoku<7><21> 25)))
+ (let (($x1512 (>= sudoku<7><21> 1)))
+ (let (($x1514 (and $x1512 $x1513)))
+ (let (($x1510 (<= sudoku<7><20> 25)))
+ (let (($x1509 (>= sudoku<7><20> 1)))
+ (let (($x1511 (and $x1509 $x1510)))
+ (let (($x1507 (<= sudoku<7><19> 25)))
+ (let (($x1506 (>= sudoku<7><19> 1)))
+ (let (($x1508 (and $x1506 $x1507)))
+ (let (($x1504 (<= sudoku<7><18> 25)))
+ (let (($x1503 (>= sudoku<7><18> 1)))
+ (let (($x1505 (and $x1503 $x1504)))
+ (let (($x1501 (<= sudoku<7><17> 25)))
+ (let (($x1500 (>= sudoku<7><17> 1)))
+ (let (($x1502 (and $x1500 $x1501)))
+ (let (($x1498 (<= sudoku<7><16> 25)))
+ (let (($x1497 (>= sudoku<7><16> 1)))
+ (let (($x1499 (and $x1497 $x1498)))
+ (let (($x1495 (<= sudoku<7><15> 25)))
+ (let (($x1494 (>= sudoku<7><15> 1)))
+ (let (($x1496 (and $x1494 $x1495)))
+ (let (($x1492 (<= sudoku<7><14> 25)))
+ (let (($x1491 (>= sudoku<7><14> 1)))
+ (let (($x1493 (and $x1491 $x1492)))
+ (let (($x1489 (<= sudoku<7><13> 25)))
+ (let (($x1488 (>= sudoku<7><13> 1)))
+ (let (($x1490 (and $x1488 $x1489)))
+ (let (($x1486 (<= sudoku<7><12> 25)))
+ (let (($x1485 (>= sudoku<7><12> 1)))
+ (let (($x1487 (and $x1485 $x1486)))
+ (let (($x1483 (<= sudoku<7><11> 25)))
+ (let (($x1482 (>= sudoku<7><11> 1)))
+ (let (($x1484 (and $x1482 $x1483)))
+ (let (($x1480 (<= sudoku<7><10> 25)))
+ (let (($x1479 (>= sudoku<7><10> 1)))
+ (let (($x1481 (and $x1479 $x1480)))
+ (let (($x1477 (<= sudoku<7><9> 25)))
+ (let (($x1476 (>= sudoku<7><9> 1)))
+ (let (($x1478 (and $x1476 $x1477)))
+ (let (($x1474 (<= sudoku<7><8> 25)))
+ (let (($x1473 (>= sudoku<7><8> 1)))
+ (let (($x1475 (and $x1473 $x1474)))
+ (let (($x1471 (<= sudoku<7><7> 25)))
+ (let (($x1470 (>= sudoku<7><7> 1)))
+ (let (($x1472 (and $x1470 $x1471)))
+ (let (($x1468 (<= sudoku<7><6> 25)))
+ (let (($x1467 (>= sudoku<7><6> 1)))
+ (let (($x1469 (and $x1467 $x1468)))
+ (let (($x1465 (<= sudoku<7><5> 25)))
+ (let (($x1464 (>= sudoku<7><5> 1)))
+ (let (($x1466 (and $x1464 $x1465)))
+ (let (($x1462 (<= sudoku<7><4> 25)))
+ (let (($x1461 (>= sudoku<7><4> 1)))
+ (let (($x1463 (and $x1461 $x1462)))
+ (let (($x1459 (<= sudoku<7><3> 25)))
+ (let (($x1458 (>= sudoku<7><3> 1)))
+ (let (($x1460 (and $x1458 $x1459)))
+ (let (($x1456 (<= sudoku<7><2> 25)))
+ (let (($x1455 (>= sudoku<7><2> 1)))
+ (let (($x1457 (and $x1455 $x1456)))
+ (let (($x1453 (<= sudoku<7><1> 25)))
+ (let (($x1452 (>= sudoku<7><1> 1)))
+ (let (($x1454 (and $x1452 $x1453)))
+ (let (($x1450 (<= sudoku<7><0> 25)))
+ (let (($x1449 (>= sudoku<7><0> 1)))
+ (let (($x1451 (and $x1449 $x1450)))
+ (let (($x1447 (<= sudoku<6><24> 25)))
+ (let (($x1446 (>= sudoku<6><24> 1)))
+ (let (($x1448 (and $x1446 $x1447)))
+ (let (($x1444 (<= sudoku<6><23> 25)))
+ (let (($x1443 (>= sudoku<6><23> 1)))
+ (let (($x1445 (and $x1443 $x1444)))
+ (let (($x1441 (<= sudoku<6><22> 25)))
+ (let (($x1440 (>= sudoku<6><22> 1)))
+ (let (($x1442 (and $x1440 $x1441)))
+ (let (($x1438 (<= sudoku<6><21> 25)))
+ (let (($x1437 (>= sudoku<6><21> 1)))
+ (let (($x1439 (and $x1437 $x1438)))
+ (let (($x1435 (<= sudoku<6><20> 25)))
+ (let (($x1434 (>= sudoku<6><20> 1)))
+ (let (($x1436 (and $x1434 $x1435)))
+ (let (($x1432 (<= sudoku<6><19> 25)))
+ (let (($x1431 (>= sudoku<6><19> 1)))
+ (let (($x1433 (and $x1431 $x1432)))
+ (let (($x1429 (<= sudoku<6><18> 25)))
+ (let (($x1428 (>= sudoku<6><18> 1)))
+ (let (($x1430 (and $x1428 $x1429)))
+ (let (($x1426 (<= sudoku<6><17> 25)))
+ (let (($x1425 (>= sudoku<6><17> 1)))
+ (let (($x1427 (and $x1425 $x1426)))
+ (let (($x1423 (<= sudoku<6><16> 25)))
+ (let (($x1422 (>= sudoku<6><16> 1)))
+ (let (($x1424 (and $x1422 $x1423)))
+ (let (($x1420 (<= sudoku<6><15> 25)))
+ (let (($x1419 (>= sudoku<6><15> 1)))
+ (let (($x1421 (and $x1419 $x1420)))
+ (let (($x1417 (<= sudoku<6><14> 25)))
+ (let (($x1416 (>= sudoku<6><14> 1)))
+ (let (($x1418 (and $x1416 $x1417)))
+ (let (($x1414 (<= sudoku<6><13> 25)))
+ (let (($x1413 (>= sudoku<6><13> 1)))
+ (let (($x1415 (and $x1413 $x1414)))
+ (let (($x1411 (<= sudoku<6><12> 25)))
+ (let (($x1410 (>= sudoku<6><12> 1)))
+ (let (($x1412 (and $x1410 $x1411)))
+ (let (($x1408 (<= sudoku<6><11> 25)))
+ (let (($x1407 (>= sudoku<6><11> 1)))
+ (let (($x1409 (and $x1407 $x1408)))
+ (let (($x1405 (<= sudoku<6><10> 25)))
+ (let (($x1404 (>= sudoku<6><10> 1)))
+ (let (($x1406 (and $x1404 $x1405)))
+ (let (($x1402 (<= sudoku<6><9> 25)))
+ (let (($x1401 (>= sudoku<6><9> 1)))
+ (let (($x1403 (and $x1401 $x1402)))
+ (let (($x1399 (<= sudoku<6><8> 25)))
+ (let (($x1398 (>= sudoku<6><8> 1)))
+ (let (($x1400 (and $x1398 $x1399)))
+ (let (($x1396 (<= sudoku<6><7> 25)))
+ (let (($x1395 (>= sudoku<6><7> 1)))
+ (let (($x1397 (and $x1395 $x1396)))
+ (let (($x1393 (<= sudoku<6><6> 25)))
+ (let (($x1392 (>= sudoku<6><6> 1)))
+ (let (($x1394 (and $x1392 $x1393)))
+ (let (($x1390 (<= sudoku<6><5> 25)))
+ (let (($x1389 (>= sudoku<6><5> 1)))
+ (let (($x1391 (and $x1389 $x1390)))
+ (let (($x1387 (<= sudoku<6><4> 25)))
+ (let (($x1386 (>= sudoku<6><4> 1)))
+ (let (($x1388 (and $x1386 $x1387)))
+ (let (($x1384 (<= sudoku<6><3> 25)))
+ (let (($x1383 (>= sudoku<6><3> 1)))
+ (let (($x1385 (and $x1383 $x1384)))
+ (let (($x1381 (<= sudoku<6><2> 25)))
+ (let (($x1380 (>= sudoku<6><2> 1)))
+ (let (($x1382 (and $x1380 $x1381)))
+ (let (($x1378 (<= sudoku<6><1> 25)))
+ (let (($x1377 (>= sudoku<6><1> 1)))
+ (let (($x1379 (and $x1377 $x1378)))
+ (let (($x1375 (<= sudoku<6><0> 25)))
+ (let (($x1374 (>= sudoku<6><0> 1)))
+ (let (($x1376 (and $x1374 $x1375)))
+ (let (($x1372 (<= sudoku<5><24> 25)))
+ (let (($x1371 (>= sudoku<5><24> 1)))
+ (let (($x1373 (and $x1371 $x1372)))
+ (let (($x1369 (<= sudoku<5><23> 25)))
+ (let (($x1368 (>= sudoku<5><23> 1)))
+ (let (($x1370 (and $x1368 $x1369)))
+ (let (($x1366 (<= sudoku<5><22> 25)))
+ (let (($x1365 (>= sudoku<5><22> 1)))
+ (let (($x1367 (and $x1365 $x1366)))
+ (let (($x1363 (<= sudoku<5><21> 25)))
+ (let (($x1362 (>= sudoku<5><21> 1)))
+ (let (($x1364 (and $x1362 $x1363)))
+ (let (($x1360 (<= sudoku<5><20> 25)))
+ (let (($x1359 (>= sudoku<5><20> 1)))
+ (let (($x1361 (and $x1359 $x1360)))
+ (let (($x1357 (<= sudoku<5><19> 25)))
+ (let (($x1356 (>= sudoku<5><19> 1)))
+ (let (($x1358 (and $x1356 $x1357)))
+ (let (($x1354 (<= sudoku<5><18> 25)))
+ (let (($x1353 (>= sudoku<5><18> 1)))
+ (let (($x1355 (and $x1353 $x1354)))
+ (let (($x1351 (<= sudoku<5><17> 25)))
+ (let (($x1350 (>= sudoku<5><17> 1)))
+ (let (($x1352 (and $x1350 $x1351)))
+ (let (($x1348 (<= sudoku<5><16> 25)))
+ (let (($x1347 (>= sudoku<5><16> 1)))
+ (let (($x1349 (and $x1347 $x1348)))
+ (let (($x1345 (<= sudoku<5><15> 25)))
+ (let (($x1344 (>= sudoku<5><15> 1)))
+ (let (($x1346 (and $x1344 $x1345)))
+ (let (($x1342 (<= sudoku<5><14> 25)))
+ (let (($x1341 (>= sudoku<5><14> 1)))
+ (let (($x1343 (and $x1341 $x1342)))
+ (let (($x1339 (<= sudoku<5><13> 25)))
+ (let (($x1338 (>= sudoku<5><13> 1)))
+ (let (($x1340 (and $x1338 $x1339)))
+ (let (($x1336 (<= sudoku<5><12> 25)))
+ (let (($x1335 (>= sudoku<5><12> 1)))
+ (let (($x1337 (and $x1335 $x1336)))
+ (let (($x1333 (<= sudoku<5><11> 25)))
+ (let (($x1332 (>= sudoku<5><11> 1)))
+ (let (($x1334 (and $x1332 $x1333)))
+ (let (($x1330 (<= sudoku<5><10> 25)))
+ (let (($x1329 (>= sudoku<5><10> 1)))
+ (let (($x1331 (and $x1329 $x1330)))
+ (let (($x1327 (<= sudoku<5><9> 25)))
+ (let (($x1326 (>= sudoku<5><9> 1)))
+ (let (($x1328 (and $x1326 $x1327)))
+ (let (($x1324 (<= sudoku<5><8> 25)))
+ (let (($x1323 (>= sudoku<5><8> 1)))
+ (let (($x1325 (and $x1323 $x1324)))
+ (let (($x1321 (<= sudoku<5><7> 25)))
+ (let (($x1320 (>= sudoku<5><7> 1)))
+ (let (($x1322 (and $x1320 $x1321)))
+ (let (($x1318 (<= sudoku<5><6> 25)))
+ (let (($x1317 (>= sudoku<5><6> 1)))
+ (let (($x1319 (and $x1317 $x1318)))
+ (let (($x1315 (<= sudoku<5><5> 25)))
+ (let (($x1314 (>= sudoku<5><5> 1)))
+ (let (($x1316 (and $x1314 $x1315)))
+ (let (($x1312 (<= sudoku<5><4> 25)))
+ (let (($x1311 (>= sudoku<5><4> 1)))
+ (let (($x1313 (and $x1311 $x1312)))
+ (let (($x1309 (<= sudoku<5><3> 25)))
+ (let (($x1308 (>= sudoku<5><3> 1)))
+ (let (($x1310 (and $x1308 $x1309)))
+ (let (($x1306 (<= sudoku<5><2> 25)))
+ (let (($x1305 (>= sudoku<5><2> 1)))
+ (let (($x1307 (and $x1305 $x1306)))
+ (let (($x1303 (<= sudoku<5><1> 25)))
+ (let (($x1302 (>= sudoku<5><1> 1)))
+ (let (($x1304 (and $x1302 $x1303)))
+ (let (($x1300 (<= sudoku<5><0> 25)))
+ (let (($x1299 (>= sudoku<5><0> 1)))
+ (let (($x1301 (and $x1299 $x1300)))
+ (let (($x1297 (<= sudoku<4><24> 25)))
+ (let (($x1296 (>= sudoku<4><24> 1)))
+ (let (($x1298 (and $x1296 $x1297)))
+ (let (($x1294 (<= sudoku<4><23> 25)))
+ (let (($x1293 (>= sudoku<4><23> 1)))
+ (let (($x1295 (and $x1293 $x1294)))
+ (let (($x1291 (<= sudoku<4><22> 25)))
+ (let (($x1290 (>= sudoku<4><22> 1)))
+ (let (($x1292 (and $x1290 $x1291)))
+ (let (($x1288 (<= sudoku<4><21> 25)))
+ (let (($x1287 (>= sudoku<4><21> 1)))
+ (let (($x1289 (and $x1287 $x1288)))
+ (let (($x1285 (<= sudoku<4><20> 25)))
+ (let (($x1284 (>= sudoku<4><20> 1)))
+ (let (($x1286 (and $x1284 $x1285)))
+ (let (($x1282 (<= sudoku<4><19> 25)))
+ (let (($x1281 (>= sudoku<4><19> 1)))
+ (let (($x1283 (and $x1281 $x1282)))
+ (let (($x1279 (<= sudoku<4><18> 25)))
+ (let (($x1278 (>= sudoku<4><18> 1)))
+ (let (($x1280 (and $x1278 $x1279)))
+ (let (($x1276 (<= sudoku<4><17> 25)))
+ (let (($x1275 (>= sudoku<4><17> 1)))
+ (let (($x1277 (and $x1275 $x1276)))
+ (let (($x1273 (<= sudoku<4><16> 25)))
+ (let (($x1272 (>= sudoku<4><16> 1)))
+ (let (($x1274 (and $x1272 $x1273)))
+ (let (($x1270 (<= sudoku<4><15> 25)))
+ (let (($x1269 (>= sudoku<4><15> 1)))
+ (let (($x1271 (and $x1269 $x1270)))
+ (let (($x1267 (<= sudoku<4><14> 25)))
+ (let (($x1266 (>= sudoku<4><14> 1)))
+ (let (($x1268 (and $x1266 $x1267)))
+ (let (($x1264 (<= sudoku<4><13> 25)))
+ (let (($x1263 (>= sudoku<4><13> 1)))
+ (let (($x1265 (and $x1263 $x1264)))
+ (let (($x1261 (<= sudoku<4><12> 25)))
+ (let (($x1260 (>= sudoku<4><12> 1)))
+ (let (($x1262 (and $x1260 $x1261)))
+ (let (($x1258 (<= sudoku<4><11> 25)))
+ (let (($x1257 (>= sudoku<4><11> 1)))
+ (let (($x1259 (and $x1257 $x1258)))
+ (let (($x1255 (<= sudoku<4><10> 25)))
+ (let (($x1254 (>= sudoku<4><10> 1)))
+ (let (($x1256 (and $x1254 $x1255)))
+ (let (($x1252 (<= sudoku<4><9> 25)))
+ (let (($x1251 (>= sudoku<4><9> 1)))
+ (let (($x1253 (and $x1251 $x1252)))
+ (let (($x1249 (<= sudoku<4><8> 25)))
+ (let (($x1248 (>= sudoku<4><8> 1)))
+ (let (($x1250 (and $x1248 $x1249)))
+ (let (($x1246 (<= sudoku<4><7> 25)))
+ (let (($x1245 (>= sudoku<4><7> 1)))
+ (let (($x1247 (and $x1245 $x1246)))
+ (let (($x1243 (<= sudoku<4><6> 25)))
+ (let (($x1242 (>= sudoku<4><6> 1)))
+ (let (($x1244 (and $x1242 $x1243)))
+ (let (($x1240 (<= sudoku<4><5> 25)))
+ (let (($x1239 (>= sudoku<4><5> 1)))
+ (let (($x1241 (and $x1239 $x1240)))
+ (let (($x1237 (<= sudoku<4><4> 25)))
+ (let (($x1236 (>= sudoku<4><4> 1)))
+ (let (($x1238 (and $x1236 $x1237)))
+ (let (($x1234 (<= sudoku<4><3> 25)))
+ (let (($x1233 (>= sudoku<4><3> 1)))
+ (let (($x1235 (and $x1233 $x1234)))
+ (let (($x1231 (<= sudoku<4><2> 25)))
+ (let (($x1230 (>= sudoku<4><2> 1)))
+ (let (($x1232 (and $x1230 $x1231)))
+ (let (($x1228 (<= sudoku<4><1> 25)))
+ (let (($x1227 (>= sudoku<4><1> 1)))
+ (let (($x1229 (and $x1227 $x1228)))
+ (let (($x1225 (<= sudoku<4><0> 25)))
+ (let (($x1224 (>= sudoku<4><0> 1)))
+ (let (($x1226 (and $x1224 $x1225)))
+ (let (($x1222 (<= sudoku<3><24> 25)))
+ (let (($x1221 (>= sudoku<3><24> 1)))
+ (let (($x1223 (and $x1221 $x1222)))
+ (let (($x1219 (<= sudoku<3><23> 25)))
+ (let (($x1218 (>= sudoku<3><23> 1)))
+ (let (($x1220 (and $x1218 $x1219)))
+ (let (($x1216 (<= sudoku<3><22> 25)))
+ (let (($x1215 (>= sudoku<3><22> 1)))
+ (let (($x1217 (and $x1215 $x1216)))
+ (let (($x1213 (<= sudoku<3><21> 25)))
+ (let (($x1212 (>= sudoku<3><21> 1)))
+ (let (($x1214 (and $x1212 $x1213)))
+ (let (($x1210 (<= sudoku<3><20> 25)))
+ (let (($x1209 (>= sudoku<3><20> 1)))
+ (let (($x1211 (and $x1209 $x1210)))
+ (let (($x1207 (<= sudoku<3><19> 25)))
+ (let (($x1206 (>= sudoku<3><19> 1)))
+ (let (($x1208 (and $x1206 $x1207)))
+ (let (($x1204 (<= sudoku<3><18> 25)))
+ (let (($x1203 (>= sudoku<3><18> 1)))
+ (let (($x1205 (and $x1203 $x1204)))
+ (let (($x1201 (<= sudoku<3><17> 25)))
+ (let (($x1200 (>= sudoku<3><17> 1)))
+ (let (($x1202 (and $x1200 $x1201)))
+ (let (($x1198 (<= sudoku<3><16> 25)))
+ (let (($x1197 (>= sudoku<3><16> 1)))
+ (let (($x1199 (and $x1197 $x1198)))
+ (let (($x1195 (<= sudoku<3><15> 25)))
+ (let (($x1194 (>= sudoku<3><15> 1)))
+ (let (($x1196 (and $x1194 $x1195)))
+ (let (($x1192 (<= sudoku<3><14> 25)))
+ (let (($x1191 (>= sudoku<3><14> 1)))
+ (let (($x1193 (and $x1191 $x1192)))
+ (let (($x1189 (<= sudoku<3><13> 25)))
+ (let (($x1188 (>= sudoku<3><13> 1)))
+ (let (($x1190 (and $x1188 $x1189)))
+ (let (($x1186 (<= sudoku<3><12> 25)))
+ (let (($x1185 (>= sudoku<3><12> 1)))
+ (let (($x1187 (and $x1185 $x1186)))
+ (let (($x1183 (<= sudoku<3><11> 25)))
+ (let (($x1182 (>= sudoku<3><11> 1)))
+ (let (($x1184 (and $x1182 $x1183)))
+ (let (($x1180 (<= sudoku<3><10> 25)))
+ (let (($x1179 (>= sudoku<3><10> 1)))
+ (let (($x1181 (and $x1179 $x1180)))
+ (let (($x1177 (<= sudoku<3><9> 25)))
+ (let (($x1176 (>= sudoku<3><9> 1)))
+ (let (($x1178 (and $x1176 $x1177)))
+ (let (($x1174 (<= sudoku<3><8> 25)))
+ (let (($x1173 (>= sudoku<3><8> 1)))
+ (let (($x1175 (and $x1173 $x1174)))
+ (let (($x1171 (<= sudoku<3><7> 25)))
+ (let (($x1170 (>= sudoku<3><7> 1)))
+ (let (($x1172 (and $x1170 $x1171)))
+ (let (($x1168 (<= sudoku<3><6> 25)))
+ (let (($x1167 (>= sudoku<3><6> 1)))
+ (let (($x1169 (and $x1167 $x1168)))
+ (let (($x1165 (<= sudoku<3><5> 25)))
+ (let (($x1164 (>= sudoku<3><5> 1)))
+ (let (($x1166 (and $x1164 $x1165)))
+ (let (($x1162 (<= sudoku<3><4> 25)))
+ (let (($x1161 (>= sudoku<3><4> 1)))
+ (let (($x1163 (and $x1161 $x1162)))
+ (let (($x1159 (<= sudoku<3><3> 25)))
+ (let (($x1158 (>= sudoku<3><3> 1)))
+ (let (($x1160 (and $x1158 $x1159)))
+ (let (($x1156 (<= sudoku<3><2> 25)))
+ (let (($x1155 (>= sudoku<3><2> 1)))
+ (let (($x1157 (and $x1155 $x1156)))
+ (let (($x1153 (<= sudoku<3><1> 25)))
+ (let (($x1152 (>= sudoku<3><1> 1)))
+ (let (($x1154 (and $x1152 $x1153)))
+ (let (($x1150 (<= sudoku<3><0> 25)))
+ (let (($x1149 (>= sudoku<3><0> 1)))
+ (let (($x1151 (and $x1149 $x1150)))
+ (let (($x1147 (<= sudoku<2><24> 25)))
+ (let (($x1146 (>= sudoku<2><24> 1)))
+ (let (($x1148 (and $x1146 $x1147)))
+ (let (($x1144 (<= sudoku<2><23> 25)))
+ (let (($x1143 (>= sudoku<2><23> 1)))
+ (let (($x1145 (and $x1143 $x1144)))
+ (let (($x1141 (<= sudoku<2><22> 25)))
+ (let (($x1140 (>= sudoku<2><22> 1)))
+ (let (($x1142 (and $x1140 $x1141)))
+ (let (($x1138 (<= sudoku<2><21> 25)))
+ (let (($x1137 (>= sudoku<2><21> 1)))
+ (let (($x1139 (and $x1137 $x1138)))
+ (let (($x1135 (<= sudoku<2><20> 25)))
+ (let (($x1134 (>= sudoku<2><20> 1)))
+ (let (($x1136 (and $x1134 $x1135)))
+ (let (($x1132 (<= sudoku<2><19> 25)))
+ (let (($x1131 (>= sudoku<2><19> 1)))
+ (let (($x1133 (and $x1131 $x1132)))
+ (let (($x1129 (<= sudoku<2><18> 25)))
+ (let (($x1128 (>= sudoku<2><18> 1)))
+ (let (($x1130 (and $x1128 $x1129)))
+ (let (($x1126 (<= sudoku<2><17> 25)))
+ (let (($x1125 (>= sudoku<2><17> 1)))
+ (let (($x1127 (and $x1125 $x1126)))
+ (let (($x1123 (<= sudoku<2><16> 25)))
+ (let (($x1122 (>= sudoku<2><16> 1)))
+ (let (($x1124 (and $x1122 $x1123)))
+ (let (($x1120 (<= sudoku<2><15> 25)))
+ (let (($x1119 (>= sudoku<2><15> 1)))
+ (let (($x1121 (and $x1119 $x1120)))
+ (let (($x1117 (<= sudoku<2><14> 25)))
+ (let (($x1116 (>= sudoku<2><14> 1)))
+ (let (($x1118 (and $x1116 $x1117)))
+ (let (($x1114 (<= sudoku<2><13> 25)))
+ (let (($x1113 (>= sudoku<2><13> 1)))
+ (let (($x1115 (and $x1113 $x1114)))
+ (let (($x1111 (<= sudoku<2><12> 25)))
+ (let (($x1110 (>= sudoku<2><12> 1)))
+ (let (($x1112 (and $x1110 $x1111)))
+ (let (($x1108 (<= sudoku<2><11> 25)))
+ (let (($x1107 (>= sudoku<2><11> 1)))
+ (let (($x1109 (and $x1107 $x1108)))
+ (let (($x1105 (<= sudoku<2><10> 25)))
+ (let (($x1104 (>= sudoku<2><10> 1)))
+ (let (($x1106 (and $x1104 $x1105)))
+ (let (($x1102 (<= sudoku<2><9> 25)))
+ (let (($x1101 (>= sudoku<2><9> 1)))
+ (let (($x1103 (and $x1101 $x1102)))
+ (let (($x1099 (<= sudoku<2><8> 25)))
+ (let (($x1098 (>= sudoku<2><8> 1)))
+ (let (($x1100 (and $x1098 $x1099)))
+ (let (($x1096 (<= sudoku<2><7> 25)))
+ (let (($x1095 (>= sudoku<2><7> 1)))
+ (let (($x1097 (and $x1095 $x1096)))
+ (let (($x1093 (<= sudoku<2><6> 25)))
+ (let (($x1092 (>= sudoku<2><6> 1)))
+ (let (($x1094 (and $x1092 $x1093)))
+ (let (($x1090 (<= sudoku<2><5> 25)))
+ (let (($x1089 (>= sudoku<2><5> 1)))
+ (let (($x1091 (and $x1089 $x1090)))
+ (let (($x1087 (<= sudoku<2><4> 25)))
+ (let (($x1086 (>= sudoku<2><4> 1)))
+ (let (($x1088 (and $x1086 $x1087)))
+ (let (($x1084 (<= sudoku<2><3> 25)))
+ (let (($x1083 (>= sudoku<2><3> 1)))
+ (let (($x1085 (and $x1083 $x1084)))
+ (let (($x1081 (<= sudoku<2><2> 25)))
+ (let (($x1080 (>= sudoku<2><2> 1)))
+ (let (($x1082 (and $x1080 $x1081)))
+ (let (($x1078 (<= sudoku<2><1> 25)))
+ (let (($x1077 (>= sudoku<2><1> 1)))
+ (let (($x1079 (and $x1077 $x1078)))
+ (let (($x1075 (<= sudoku<2><0> 25)))
+ (let (($x1074 (>= sudoku<2><0> 1)))
+ (let (($x1076 (and $x1074 $x1075)))
+ (let (($x1072 (<= sudoku<1><24> 25)))
+ (let (($x1071 (>= sudoku<1><24> 1)))
+ (let (($x1073 (and $x1071 $x1072)))
+ (let (($x1069 (<= sudoku<1><23> 25)))
+ (let (($x1068 (>= sudoku<1><23> 1)))
+ (let (($x1070 (and $x1068 $x1069)))
+ (let (($x1066 (<= sudoku<1><22> 25)))
+ (let (($x1065 (>= sudoku<1><22> 1)))
+ (let (($x1067 (and $x1065 $x1066)))
+ (let (($x1063 (<= sudoku<1><21> 25)))
+ (let (($x1062 (>= sudoku<1><21> 1)))
+ (let (($x1064 (and $x1062 $x1063)))
+ (let (($x1060 (<= sudoku<1><20> 25)))
+ (let (($x1059 (>= sudoku<1><20> 1)))
+ (let (($x1061 (and $x1059 $x1060)))
+ (let (($x1057 (<= sudoku<1><19> 25)))
+ (let (($x1056 (>= sudoku<1><19> 1)))
+ (let (($x1058 (and $x1056 $x1057)))
+ (let (($x1054 (<= sudoku<1><18> 25)))
+ (let (($x1053 (>= sudoku<1><18> 1)))
+ (let (($x1055 (and $x1053 $x1054)))
+ (let (($x1051 (<= sudoku<1><17> 25)))
+ (let (($x1050 (>= sudoku<1><17> 1)))
+ (let (($x1052 (and $x1050 $x1051)))
+ (let (($x1048 (<= sudoku<1><16> 25)))
+ (let (($x1047 (>= sudoku<1><16> 1)))
+ (let (($x1049 (and $x1047 $x1048)))
+ (let (($x1045 (<= sudoku<1><15> 25)))
+ (let (($x1044 (>= sudoku<1><15> 1)))
+ (let (($x1046 (and $x1044 $x1045)))
+ (let (($x1042 (<= sudoku<1><14> 25)))
+ (let (($x1041 (>= sudoku<1><14> 1)))
+ (let (($x1043 (and $x1041 $x1042)))
+ (let (($x1039 (<= sudoku<1><13> 25)))
+ (let (($x1038 (>= sudoku<1><13> 1)))
+ (let (($x1040 (and $x1038 $x1039)))
+ (let (($x1036 (<= sudoku<1><12> 25)))
+ (let (($x1035 (>= sudoku<1><12> 1)))
+ (let (($x1037 (and $x1035 $x1036)))
+ (let (($x1033 (<= sudoku<1><11> 25)))
+ (let (($x1032 (>= sudoku<1><11> 1)))
+ (let (($x1034 (and $x1032 $x1033)))
+ (let (($x1030 (<= sudoku<1><10> 25)))
+ (let (($x1029 (>= sudoku<1><10> 1)))
+ (let (($x1031 (and $x1029 $x1030)))
+ (let (($x1027 (<= sudoku<1><9> 25)))
+ (let (($x1026 (>= sudoku<1><9> 1)))
+ (let (($x1028 (and $x1026 $x1027)))
+ (let (($x1024 (<= sudoku<1><8> 25)))
+ (let (($x1023 (>= sudoku<1><8> 1)))
+ (let (($x1025 (and $x1023 $x1024)))
+ (let (($x1021 (<= sudoku<1><7> 25)))
+ (let (($x1020 (>= sudoku<1><7> 1)))
+ (let (($x1022 (and $x1020 $x1021)))
+ (let (($x1018 (<= sudoku<1><6> 25)))
+ (let (($x1017 (>= sudoku<1><6> 1)))
+ (let (($x1019 (and $x1017 $x1018)))
+ (let (($x1015 (<= sudoku<1><5> 25)))
+ (let (($x1014 (>= sudoku<1><5> 1)))
+ (let (($x1016 (and $x1014 $x1015)))
+ (let (($x1012 (<= sudoku<1><4> 25)))
+ (let (($x1011 (>= sudoku<1><4> 1)))
+ (let (($x1013 (and $x1011 $x1012)))
+ (let (($x1009 (<= sudoku<1><3> 25)))
+ (let (($x1008 (>= sudoku<1><3> 1)))
+ (let (($x1010 (and $x1008 $x1009)))
+ (let (($x1006 (<= sudoku<1><2> 25)))
+ (let (($x1005 (>= sudoku<1><2> 1)))
+ (let (($x1007 (and $x1005 $x1006)))
+ (let (($x1003 (<= sudoku<1><1> 25)))
+ (let (($x1002 (>= sudoku<1><1> 1)))
+ (let (($x1004 (and $x1002 $x1003)))
+ (let (($x1000 (<= sudoku<1><0> 25)))
+ (let (($x999 (>= sudoku<1><0> 1)))
+ (let (($x1001 (and $x999 $x1000)))
+ (let (($x997 (<= sudoku<0><24> 25)))
+ (let (($x996 (>= sudoku<0><24> 1)))
+ (let (($x998 (and $x996 $x997)))
+ (let (($x994 (<= sudoku<0><23> 25)))
+ (let (($x993 (>= sudoku<0><23> 1)))
+ (let (($x995 (and $x993 $x994)))
+ (let (($x991 (<= sudoku<0><22> 25)))
+ (let (($x990 (>= sudoku<0><22> 1)))
+ (let (($x992 (and $x990 $x991)))
+ (let (($x988 (<= sudoku<0><21> 25)))
+ (let (($x987 (>= sudoku<0><21> 1)))
+ (let (($x989 (and $x987 $x988)))
+ (let (($x985 (<= sudoku<0><20> 25)))
+ (let (($x984 (>= sudoku<0><20> 1)))
+ (let (($x986 (and $x984 $x985)))
+ (let (($x982 (<= sudoku<0><19> 25)))
+ (let (($x981 (>= sudoku<0><19> 1)))
+ (let (($x983 (and $x981 $x982)))
+ (let (($x979 (<= sudoku<0><18> 25)))
+ (let (($x978 (>= sudoku<0><18> 1)))
+ (let (($x980 (and $x978 $x979)))
+ (let (($x976 (<= sudoku<0><17> 25)))
+ (let (($x975 (>= sudoku<0><17> 1)))
+ (let (($x977 (and $x975 $x976)))
+ (let (($x973 (<= sudoku<0><16> 25)))
+ (let (($x972 (>= sudoku<0><16> 1)))
+ (let (($x974 (and $x972 $x973)))
+ (let (($x970 (<= sudoku<0><15> 25)))
+ (let (($x969 (>= sudoku<0><15> 1)))
+ (let (($x971 (and $x969 $x970)))
+ (let (($x967 (<= sudoku<0><14> 25)))
+ (let (($x966 (>= sudoku<0><14> 1)))
+ (let (($x968 (and $x966 $x967)))
+ (let (($x964 (<= sudoku<0><13> 25)))
+ (let (($x963 (>= sudoku<0><13> 1)))
+ (let (($x965 (and $x963 $x964)))
+ (let (($x961 (<= sudoku<0><12> 25)))
+ (let (($x960 (>= sudoku<0><12> 1)))
+ (let (($x962 (and $x960 $x961)))
+ (let (($x958 (<= sudoku<0><11> 25)))
+ (let (($x957 (>= sudoku<0><11> 1)))
+ (let (($x959 (and $x957 $x958)))
+ (let (($x955 (<= sudoku<0><10> 25)))
+ (let (($x954 (>= sudoku<0><10> 1)))
+ (let (($x956 (and $x954 $x955)))
+ (let (($x952 (<= sudoku<0><9> 25)))
+ (let (($x951 (>= sudoku<0><9> 1)))
+ (let (($x953 (and $x951 $x952)))
+ (let (($x949 (<= sudoku<0><8> 25)))
+ (let (($x948 (>= sudoku<0><8> 1)))
+ (let (($x950 (and $x948 $x949)))
+ (let (($x946 (<= sudoku<0><7> 25)))
+ (let (($x945 (>= sudoku<0><7> 1)))
+ (let (($x947 (and $x945 $x946)))
+ (let (($x943 (<= sudoku<0><6> 25)))
+ (let (($x942 (>= sudoku<0><6> 1)))
+ (let (($x944 (and $x942 $x943)))
+ (let (($x940 (<= sudoku<0><5> 25)))
+ (let (($x939 (>= sudoku<0><5> 1)))
+ (let (($x941 (and $x939 $x940)))
+ (let (($x937 (<= sudoku<0><4> 25)))
+ (let (($x936 (>= sudoku<0><4> 1)))
+ (let (($x938 (and $x936 $x937)))
+ (let (($x934 (<= sudoku<0><3> 25)))
+ (let (($x933 (>= sudoku<0><3> 1)))
+ (let (($x935 (and $x933 $x934)))
+ (let (($x931 (<= sudoku<0><2> 25)))
+ (let (($x930 (>= sudoku<0><2> 1)))
+ (let (($x932 (and $x930 $x931)))
+ (let (($x928 (<= sudoku<0><1> 25)))
+ (let (($x927 (>= sudoku<0><1> 1)))
+ (let (($x929 (and $x927 $x928)))
+ (let (($x925 (<= sudoku<0><0> 25)))
+ (let (($x924 (>= sudoku<0><0> 1)))
+ (let (($x926 (and $x924 $x925)))
+ (let (($x923 (= sudoku<24><24> 19)))
+ (let (($x922 (= sudoku<24><19> 14)))
+ (let (($x921 (= sudoku<24><15> 16)))
+ (let (($x920 (= sudoku<24><13> 10)))
+ (let (($x919 (= sudoku<24><10> 18)))
+ (let (($x918 (= sudoku<24><9> 4)))
+ (let (($x917 (= sudoku<24><7> 3)))
+ (let (($x916 (= sudoku<24><4> 23)))
+ (let (($x915 (= sudoku<23><23> 2)))
+ (let (($x914 (= sudoku<23><18> 10)))
+ (let (($x913 (= sudoku<23><15> 18)))
+ (let (($x912 (= sudoku<23><14> 4)))
+ (let (($x911 (= sudoku<23><5> 7)))
+ (let (($x910 (= sudoku<23><3> 24)))
+ (let (($x909 (= sudoku<23><1> 15)))
+ (let (($x908 (= sudoku<22><24> 25)))
+ (let (($x907 (= sudoku<22><23> 10)))
+ (let (($x906 (= sudoku<22><21> 12)))
+ (let (($x905 (= sudoku<22><18> 22)))
+ (let (($x904 (= sudoku<22><17> 3)))
+ (let (($x903 (= sudoku<22><14> 23)))
+ (let (($x902 (= sudoku<22><13> 11)))
+ (let (($x901 (= sudoku<22><9> 19)))
+ (let (($x900 (= sudoku<22><6> 15)))
+ (let (($x899 (= sudoku<22><2> 9)))
+ (let (($x898 (= sudoku<21><24> 4)))
+ (let (($x897 (= sudoku<21><23> 22)))
+ (let (($x896 (= sudoku<21><20> 21)))
+ (let (($x895 (= sudoku<21><19> 23)))
+ (let (($x894 (= sudoku<21><14> 19)))
+ (let (($x893 (= sudoku<21><10> 13)))
+ (let (($x892 (= sudoku<21><6> 17)))
+ (let (($x891 (= sudoku<21><3> 10)))
+ (let (($x890 (= sudoku<20><18> 24)))
+ (let (($x889 (= sudoku<20><15> 13)))
+ (let (($x888 (= sudoku<20><14> 14)))
+ (let (($x887 (= sudoku<20><13> 2)))
+ (let (($x886 (= sudoku<20><9> 25)))
+ (let (($x885 (= sudoku<20><7> 20)))
+ (let (($x884 (= sudoku<20><6> 12)))
+ (let (($x883 (= sudoku<20><5> 18)))
+ (let (($x882 (= sudoku<20><1> 5)))
+ (let (($x881 (= sudoku<19><24> 11)))
+ (let (($x880 (= sudoku<19><20> 19)))
+ (let (($x879 (= sudoku<19><19> 24)))
+ (let (($x878 (= sudoku<19><14> 2)))
+ (let (($x877 (= sudoku<19><13> 9)))
+ (let (($x876 (= sudoku<19><10> 25)))
+ (let (($x875 (= sudoku<19><8> 20)))
+ (let (($x874 (= sudoku<19><7> 12)))
+ (let (($x873 (= sudoku<19><0> 23)))
+ (let (($x872 (= sudoku<18><24> 24)))
+ (let (($x871 (= sudoku<18><23> 1)))
+ (let (($x870 (= sudoku<18><21> 13)))
+ (let (($x869 (= sudoku<18><18> 9)))
+ (let (($x868 (= sudoku<18><17> 17)))
+ (let (($x867 (= sudoku<18><14> 10)))
+ (let (($x866 (= sudoku<18><13> 20)))
+ (let (($x865 (= sudoku<18><7> 5)))
+ (let (($x864 (= sudoku<18><6> 21)))
+ (let (($x863 (= sudoku<18><5> 23)))
+ (let (($x862 (= sudoku<18><4> 11)))
+ (let (($x861 (= sudoku<18><0> 19)))
+ (let (($x860 (= sudoku<17><24> 2)))
+ (let (($x859 (= sudoku<17><23> 9)))
+ (let (($x858 (= sudoku<17><21> 16)))
+ (let (($x857 (= sudoku<17><18> 20)))
+ (let (($x856 (= sudoku<17><16> 18)))
+ (let (($x855 (= sudoku<17><14> 22)))
+ (let (($x854 (= sudoku<17><12> 5)))
+ (let (($x853 (= sudoku<17><10> 23)))
+ (let (($x852 (= sudoku<17><9> 11)))
+ (let (($x851 (= sudoku<17><8> 8)))
+ (let (($x850 (= sudoku<17><7> 6)))
+ (let (($x849 (= sudoku<17><6> 7)))
+ (let (($x848 (= sudoku<17><5> 19)))
+ (let (($x847 (= sudoku<17><3> 1)))
+ (let (($x846 (= sudoku<17><2> 15)))
+ (let (($x845 (= sudoku<17><1> 13)))
+ (let (($x844 (= sudoku<16><23> 20)))
+ (let (($x843 (= sudoku<16><21> 18)))
+ (let (($x842 (= sudoku<16><20> 4)))
+ (let (($x841 (= sudoku<16><18> 3)))
+ (let (($x840 (= sudoku<16><13> 8)))
+ (let (($x839 (= sudoku<16><12> 6)))
+ (let (($x838 (= sudoku<16><6> 13)))
+ (let (($x837 (= sudoku<16><4> 2)))
+ (let (($x836 (= sudoku<16><2> 17)))
+ (let (($x835 (= sudoku<16><1> 16)))
+ (let (($x834 (= sudoku<16><0> 25)))
+ (let (($x833 (= sudoku<15><20> 23)))
+ (let (($x832 (= sudoku<15><17> 6)))
+ (let (($x831 (= sudoku<15><15> 19)))
+ (let (($x830 (= sudoku<15><12> 15)))
+ (let (($x829 (= sudoku<15><11> 13)))
+ (let (($x828 (= sudoku<15><5> 25)))
+ (let (($x827 (= sudoku<15><4> 10)))
+ (let (($x826 (= sudoku<15><3> 20)))
+ (let (($x825 (= sudoku<15><0> 4)))
+ (let (($x824 (= sudoku<14><23> 5)))
+ (let (($x823 (= sudoku<14><19> 8)))
+ (let (($x822 (= sudoku<14><18> 6)))
+ (let (($x821 (= sudoku<14><17> 7)))
+ (let (($x820 (= sudoku<14><16> 19)))
+ (let (($x819 (= sudoku<14><15> 24)))
+ (let (($x818 (= sudoku<14><14> 1)))
+ (let (($x817 (= sudoku<14><11> 14)))
+ (let (($x816 (= sudoku<14><9> 9)))
+ (let (($x815 (= sudoku<14><8> 17)))
+ (let (($x814 (= sudoku<14><4> 20)))
+ (let (($x813 (= sudoku<13><24> 8)))
+ (let (($x812 (= sudoku<13><21> 19)))
+ (let (($x811 (= sudoku<13><20> 24)))
+ (let (($x810 (= sudoku<13><18> 15)))
+ (let (($x809 (= sudoku<13><17> 13)))
+ (let (($x808 (= sudoku<13><13> 17)))
+ (let (($x807 (= sudoku<13><12> 16)))
+ (let (($x806 (= sudoku<13><11> 25)))
+ (let (($x805 (= sudoku<13><8> 12)))
+ (let (($x804 (= sudoku<13><6> 4)))
+ (let (($x803 (= sudoku<13><2> 21)))
+ (let (($x802 (= sudoku<13><0> 11)))
+ (let (($x801 (= sudoku<12><24> 1)))
+ (let (($x800 (= sudoku<12><21> 14)))
+ (let (($x799 (= sudoku<12><20> 2)))
+ (let (($x798 (= sudoku<12><13> 12)))
+ (let (($x797 (= sudoku<12><8> 5)))
+ (let (($x796 (= sudoku<12><6> 23)))
+ (let (($x795 (= sudoku<12><5> 11)))
+ (let (($x794 (= sudoku<12><4> 8)))
+ (let (($x793 (= sudoku<12><0> 24)))
+ (let (($x792 (= sudoku<11><23> 17)))
+ (let (($x791 (= sudoku<11><20> 10)))
+ (let (($x790 (= sudoku<11><12> 21)))
+ (let (($x789 (= sudoku<11><9> 8)))
+ (let (($x788 (= sudoku<11><8> 6)))
+ (let (($x787 (= sudoku<11><6> 19)))
+ (let (($x786 (= sudoku<11><5> 24)))
+ (let (($x785 (= sudoku<11><4> 1)))
+ (let (($x784 (= sudoku<11><3> 15)))
+ (let (($x783 (= sudoku<11><0> 2)))
+ (let (($x782 (= sudoku<10><22> 18)))
+ (let (($x781 (= sudoku<10><21> 4)))
+ (let (($x780 (= sudoku<10><19> 3)))
+ (let (($x779 (= sudoku<10><4> 9)))
+ (let (($x778 (= sudoku<10><1> 25)))
+ (let (($x777 (= sudoku<9><24> 12)))
+ (let (($x776 (= sudoku<9><23> 18)))
+ (let (($x775 (= sudoku<9><15> 8)))
+ (let (($x774 (= sudoku<9><14> 6)))
+ (let (($x773 (= sudoku<9><13> 7)))
+ (let (($x772 (= sudoku<9><12> 19)))
+ (let (($x771 (= sudoku<9><11> 24)))
+ (let (($x770 (= sudoku<9><10> 1)))
+ (let (($x769 (= sudoku<9><8> 13)))
+ (let (($x768 (= sudoku<9><7> 14)))
+ (let (($x767 (= sudoku<9><6> 2)))
+ (let (($x766 (= sudoku<9><4> 17)))
+ (let (($x765 (= sudoku<9><0> 20)))
+ (let (($x764 (= sudoku<8><23> 21)))
+ (let (($x763 (= sudoku<8><20> 8)))
+ (let (($x762 (= sudoku<8><19> 6)))
+ (let (($x761 (= sudoku<8><14> 15)))
+ (let (($x760 (= sudoku<8><12> 14)))
+ (let (($x759 (= sudoku<8><10> 9)))
+ (let (($x758 (= sudoku<8><9> 17)))
+ (let (($x757 (= sudoku<8><5> 20)))
+ (let (($x756 (= sudoku<8><3> 18)))
+ (let (($x755 (= sudoku<8><0> 3)))
+ (let (($x754 (= sudoku<7><23> 7)))
+ (let (($x753 (= sudoku<7><22> 19)))
+ (let (($x752 (= sudoku<7><20> 1)))
+ (let (($x751 (= sudoku<7><19> 15)))
+ (let (($x750 (= sudoku<7><17> 14)))
+ (let (($x749 (= sudoku<7><16> 2)))
+ (let (($x748 (= sudoku<7><15> 9)))
+ (let (($x747 (= sudoku<7><11> 10)))
+ (let (($x746 (= sudoku<7><10> 20)))
+ (let (($x745 (= sudoku<7><2> 23)))
+ (let (($x744 (= sudoku<7><0> 8)))
+ (let (($x743 (= sudoku<6><21> 2)))
+ (let (($x742 (= sudoku<6><19> 17)))
+ (let (($x741 (= sudoku<6><14> 12)))
+ (let (($x740 (= sudoku<6><11> 22)))
+ (let (($x739 (= sudoku<6><10> 3)))
+ (let (($x738 (= sudoku<6><9> 5)))
+ (let (($x737 (= sudoku<6><8> 21)))
+ (let (($x736 (= sudoku<6><4> 6)))
+ (let (($x735 (= sudoku<5><24> 17)))
+ (let (($x734 (= sudoku<5><20> 20)))
+ (let (($x733 (= sudoku<5><8> 7)))
+ (let (($x732 (= sudoku<5><7> 19)))
+ (let (($x730 (= sudoku<5><5> 1)))
+ (let (($x729 (= sudoku<5><4> 15)))
+ (let (($x728 (= sudoku<5><2> 14)))
+ (let (($x727 (= sudoku<5><1> 2)))
+ (let (($x726 (= sudoku<5><0> 9)))
+ (let (($x725 (= sudoku<4><22> 10)))
+ (let (($x724 (= sudoku<4><16> 3)))
+ (let (($x723 (= sudoku<4><10> 6)))
+ (let (($x722 (= sudoku<4><9> 7)))
+ (let (($x721 (= sudoku<4><5> 15)))
+ (let (($x720 (= sudoku<4><2> 2)))
+ (let (($x719 (= sudoku<3><23> 4)))
+ (let (($x717 (= sudoku<3><22> 22)))
+ (let (($x716 (= sudoku<3><20> 5)))
+ (let (($x715 (= sudoku<3><18> 23)))
+ (let (($x714 (= sudoku<3><15> 6)))
+ (let (($x712 (= sudoku<3><12> 24)))
+ (let (($x711 (= sudoku<3><10> 15)))
+ (let (($x710 (= sudoku<3><7> 2)))
+ (let (($x709 (= sudoku<3><5> 17)))
+ (let (($x708 (= sudoku<3><4> 16)))
+ (let (($x707 (= sudoku<3><2> 10)))
+ (let (($x706 (= sudoku<3><0> 12)))
+ (let (($x705 (= sudoku<2><24> 21)))
+ (let (($x704 (= sudoku<2><23> 23)))
+ (let (($x703 (= sudoku<2><22> 11)))
+ (let (($x702 (= sudoku<2><19> 7)))
+ (let (($x700 (= sudoku<2><17> 24)))
+ (let (($x699 (= sudoku<2><16> 1)))
+ (let (($x698 (= sudoku<2><15> 15)))
+ (let (($x697 (= sudoku<2><13> 14)))
+ (let (($x695 (= sudoku<2><10> 17)))
+ (let (($x693 (= sudoku<2><9> 16)))
+ (let (($x692 (= sudoku<2><8> 25)))
+ (let (($x691 (= sudoku<2><7> 10)))
+ (let (($x690 (= sudoku<2><6> 20)))
+ (let (($x688 (= sudoku<2><5> 12)))
+ (let (($x687 (= sudoku<2><2> 22)))
+ (let (($x686 (= sudoku<2><1> 3)))
+ (let (($x684 (= sudoku<1><17> 2)))
+ (let (($x682 (= sudoku<1><16> 9)))
+ (let (($x681 (= sudoku<1><14> 16)))
+ (let (($x679 (= sudoku<1><12> 10)))
+ (let (($x678 (= sudoku<1><9> 18)))
+ (let (($x676 (= sudoku<1><4> 21)))
+ (let (($x674 (= sudoku<1><3> 23)))
+ (let (($x673 (= sudoku<0><24> 13)))
+ (let (($x671 (= sudoku<0><21> 9)))
+ (let (($x669 (= sudoku<0><18> 25)))
+ (let (($x667 (= sudoku<0><17> 10)))
+ (let (($x665 (= sudoku<0><15> 12)))
+ (let (($x663 (= sudoku<0><12> 22)))
+ (let (($x661 (= sudoku<0><10> 5)))
+ (let (($x659 (= sudoku<0><8> 23)))
+ (let (($x657 (= sudoku<0><7> 11)))
+ (let (($x655 (= sudoku<0><6> 8)))
+ (let (($x653 (= sudoku<0><2> 24)))
+ (let (($x651 (= sudoku<0><1> 1)))
+ (let (($x631 (= sudoku<0><0> 15)))
+ (and $x631 $x651 $x653 $x655 $x657 $x659 $x661 $x663 $x665 $x667 $x669 $x671 $x673 $x674 $x676 $x678 $x679 $x681 $x682 $x684 $x686 $x687 $x688 $x690 $x691 $x692 $x693 $x695 $x697 $x698 $x699 $x700 $x702 $x703 $x704 $x705 $x706 $x707 $x708 $x709 $x710 $x711 $x712 $x714 $x715 $x716 $x717 $x719 $x720 $x721 $x722 $x723 $x724 $x725 $x726 $x727 $x728 $x729 $x730 $x732 $x733 $x734 $x735 $x736 $x737 $x738 $x739 $x740 $x741 $x742 $x743 $x744 $x745 $x746 $x747 $x748 $x749 $x750 $x751 $x752 $x753 $x754 $x755 $x756 $x757 $x758 $x759 $x760 $x761 $x762 $x763 $x764 $x765 $x766 $x767 $x768 $x769 $x770 $x771 $x772 $x773 $x774 $x775 $x776 $x777 $x778 $x779 $x780 $x781 $x782 $x783 $x784 $x785 $x786 $x787 $x788 $x789 $x790 $x791 $x792 $x793 $x794 $x795 $x796 $x797 $x798 $x799 $x800 $x801 $x802 $x803 $x804 $x805 $x806 $x807 $x808 $x809 $x810 $x811 $x812 $x813 $x814 $x815 $x816 $x817 $x818 $x819 $x820 $x821 $x822 $x823 $x824 $x825 $x826 $x827 $x828 $x829 $x830 $x831 $x832 $x833 $x834 $x835 $x836 $x837 $x838 $x839 $x840 $x841 $x842 $x843 $x844 $x845 $x846 $x847 $x848 $x849 $x850 $x851 $x852 $x853 $x854 $x855 $x856 $x857 $x858 $x859 $x860 $x861 $x862 $x863 $x864 $x865 $x866 $x867 $x868 $x869 $x870 $x871 $x872 $x873 $x874 $x875 $x876 $x877 $x878 $x879 $x880 $x881 $x882 $x883 $x884 $x885 $x886 $x887 $x888 $x889 $x890 $x891 $x892 $x893 $x894 $x895 $x896 $x897 $x898 $x899 $x900 $x901 $x902 $x903 $x904 $x905 $x906 $x907 $x908 $x909 $x910 $x911 $x912 $x913 $x914 $x915 $x916 $x917 $x918 $x919 $x920 $x921 $x922 $x923 $x926 $x929 $x932 $x935 $x938 $x941 $x944 $x947 $x950 $x953 $x956 $x959 $x962 $x965 $x968 $x971 $x974 $x977 $x980 $x983 $x986 $x989 $x992 $x995 $x998 $x1001 $x1004 $x1007 $x1010 $x1013 $x1016 $x1019 $x1022 $x1025 $x1028 $x1031 $x1034 $x1037 $x1040 $x1043 $x1046 $x1049 $x1052 $x1055 $x1058 $x1061 $x1064 $x1067 $x1070 $x1073 $x1076 $x1079 $x1082 $x1085 $x1088 $x1091 $x1094 $x1097 $x1100 $x1103 $x1106 $x1109 $x1112 $x1115 $x1118 $x1121 $x1124 $x1127 $x1130 $x1133 $x1136 $x1139 $x1142 $x1145 $x1148 $x1151 $x1154 $x1157 $x1160 $x1163 $x1166 $x1169 $x1172 $x1175 $x1178 $x1181 $x1184 $x1187 $x1190 $x1193 $x1196 $x1199 $x1202 $x1205 $x1208 $x1211 $x1214 $x1217 $x1220 $x1223 $x1226 $x1229 $x1232 $x1235 $x1238 $x1241 $x1244 $x1247 $x1250 $x1253 $x1256 $x1259 $x1262 $x1265 $x1268 $x1271 $x1274 $x1277 $x1280 $x1283 $x1286 $x1289 $x1292 $x1295 $x1298 $x1301 $x1304 $x1307 $x1310 $x1313 $x1316 $x1319 $x1322 $x1325 $x1328 $x1331 $x1334 $x1337 $x1340 $x1343 $x1346 $x1349 $x1352 $x1355 $x1358 $x1361 $x1364 $x1367 $x1370 $x1373 $x1376 $x1379 $x1382 $x1385 $x1388 $x1391 $x1394 $x1397 $x1400 $x1403 $x1406 $x1409 $x1412 $x1415 $x1418 $x1421 $x1424 $x1427 $x1430 $x1433 $x1436 $x1439 $x1442 $x1445 $x1448 $x1451 $x1454 $x1457 $x1460 $x1463 $x1466 $x1469 $x1472 $x1475 $x1478 $x1481 $x1484 $x1487 $x1490 $x1493 $x1496 $x1499 $x1502 $x1505 $x1508 $x1511 $x1514 $x1517 $x1520 $x1523 $x1526 $x1529 $x1532 $x1535 $x1538 $x1541 $x1544 $x1547 $x1550 $x1553 $x1556 $x1559 $x1562 $x1565 $x1568 $x1571 $x1574 $x1577 $x1580 $x1583 $x1586 $x1589 $x1592 $x1595 $x1598 $x1601 $x1604 $x1607 $x1610 $x1613 $x1616 $x1619 $x1622 $x1625 $x1628 $x1631 $x1634 $x1637 $x1640 $x1643 $x1646 $x1649 $x1652 $x1655 $x1658 $x1661 $x1664 $x1667 $x1670 $x1673 $x1676 $x1679 $x1682 $x1685 $x1688 $x1691 $x1694 $x1697 $x1700 $x1703 $x1706 $x1709 $x1712 $x1715 $x1718 $x1721 $x1724 $x1727 $x1730 $x1733 $x1736 $x1739 $x1742 $x1745 $x1748 $x1751 $x1754 $x1757 $x1760 $x1763 $x1766 $x1769 $x1772 $x1775 $x1778 $x1781 $x1784 $x1787 $x1790 $x1793 $x1796 $x1799 $x1802 $x1805 $x1808 $x1811 $x1814 $x1817 $x1820 $x1823 $x1826 $x1829 $x1832 $x1835 $x1838 $x1841 $x1844 $x1847 $x1850 $x1853 $x1856 $x1859 $x1862 $x1865 $x1868 $x1871 $x1874 $x1877 $x1880 $x1883 $x1886 $x1889 $x1892 $x1895 $x1898 $x1901 $x1904 $x1907 $x1910 $x1913 $x1916 $x1919 $x1922 $x1925 $x1928 $x1931 $x1934 $x1937 $x1940 $x1943 $x1946 $x1949 $x1952 $x1955 $x1958 $x1961 $x1964 $x1967 $x1970 $x1973 $x1976 $x1979 $x1982 $x1985 $x1988 $x1991 $x1994 $x1997 $x2000 $x2003 $x2006 $x2009 $x2012 $x2015 $x2018 $x2021 $x2024 $x2027 $x2030 $x2033 $x2036 $x2039 $x2042 $x2045 $x2048 $x2051 $x2054 $x2057 $x2060 $x2063 $x2066 $x2069 $x2072 $x2075 $x2078 $x2081 $x2084 $x2087 $x2090 $x2093 $x2096 $x2099 $x2102 $x2105 $x2108 $x2111 $x2114 $x2117 $x2120 $x2123 $x2126 $x2129 $x2132 $x2135 $x2138 $x2141 $x2144 $x2147 $x2150 $x2153 $x2156 $x2159 $x2162 $x2165 $x2168 $x2171 $x2174 $x2177 $x2180 $x2183 $x2186 $x2189 $x2192 $x2195 $x2198 $x2201 $x2204 $x2207 $x2210 $x2213 $x2216 $x2219 $x2222 $x2225 $x2228 $x2231 $x2234 $x2237 $x2240 $x2243 $x2246 $x2249 $x2252 $x2255 $x2258 $x2261 $x2264 $x2267 $x2270 $x2273 $x2276 $x2279 $x2282 $x2285 $x2288 $x2291 $x2294 $x2297 $x2300 $x2303 $x2306 $x2309 $x2312 $x2315 $x2318 $x2321 $x2324 $x2327 $x2330 $x2333 $x2336 $x2339 $x2342 $x2345 $x2348 $x2351 $x2354 $x2357 $x2360 $x2363 $x2366 $x2369 $x2372 $x2375 $x2378 $x2381 $x2384 $x2387 $x2390 $x2393 $x2396 $x2399 $x2402 $x2405 $x2408 $x2411 $x2414 $x2417 $x2420 $x2423 $x2426 $x2429 $x2432 $x2435 $x2438 $x2441 $x2444 $x2447 $x2450 $x2453 $x2456 $x2459 $x2462 $x2465 $x2468 $x2471 $x2474 $x2477 $x2480 $x2483 $x2486 $x2489 $x2492 $x2495 $x2498 $x2501 $x2504 $x2507 $x2510 $x2513 $x2516 $x2519 $x2522 $x2525 $x2528 $x2531 $x2534 $x2537 $x2540 $x2543 $x2546 $x2549 $x2552 $x2555 $x2558 $x2561 $x2564 $x2567 $x2570 $x2573 $x2576 $x2579 $x2582 $x2585 $x2588 $x2591 $x2594 $x2597 $x2600 $x2603 $x2606 $x2609 $x2612 $x2615 $x2618 $x2621 $x2624 $x2627 $x2630 $x2633 $x2636 $x2639 $x2642 $x2645 $x2648 $x2651 $x2654 $x2657 $x2660 $x2663 $x2666 $x2669 $x2672 $x2675 $x2678 $x2681 $x2684 $x2687 $x2690 $x2693 $x2696 $x2699 $x2702 $x2705 $x2708 $x2711 $x2714 $x2717 $x2720 $x2723 $x2726 $x2729 $x2732 $x2735 $x2738 $x2741 $x2744 $x2747 $x2750 $x2753 $x2756 $x2759 $x2762 $x2765 $x2768 $x2771 $x2774 $x2777 $x2780 $x2783 $x2786 $x2789 $x2792 $x2795 $x2798 $x2799 $x2800 $x2801 $x2802 $x2803 $x2804 $x2805 $x2806 $x2807 $x2808 $x2809 $x2810 $x2811 $x2812 $x2813 $x2814 $x2815 $x2816 $x2817 $x2818 $x2819 $x2820 $x2821 $x2822 $x2823 $x2824 $x2825 $x2826 $x2827 $x2828 $x2829 $x2830 $x2831 $x2832 $x2833 $x2834 $x2835 $x2836 $x2837 $x2838 $x2839 $x2840 $x2841 $x2842 $x2843 $x2844 $x2845 $x2846 $x2847 $x2848 $x2849 $x2850 $x2851 $x2852 $x2853 $x2854 $x2855 $x2856 $x2857 $x2858 $x2859 $x2860 $x2861 $x2862 $x2863 $x2864 $x2865 $x2866 $x2867 $x2868 $x2869 $x2870 $x2871 $x2872 $x2873)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+ (check-sat)
+ (get-model)
diff --git a/tests/regress/wd/issue401b.smt2.gold b/tests/regress/wd/issue401b.smt2.gold
new file mode 100644
index 000000000..f2171cc1f
--- /dev/null
+++ b/tests/regress/wd/issue401b.smt2.gold
@@ -0,0 +1,2 @@
+unknown
+(error "the search was interrupted. No model is available")