1 files changed, 129 insertions, 0 deletions
diff --git a/test/regress/regress2/quantifiers/syn874-1.smt2 b/test/regress/regress2/quantifiers/syn874-1.smt2
new file mode 100644
index 000000000..93de3aca6
--- /dev/null
+++ b/test/regress/regress2/quantifiers/syn874-1.smt2
@@ -0,0 +1,129 @@
+; COMMAND-LINE: --full-saturate-quant --fs-stratify
+; EXPECT: unsat
+(set-logic ALL)
+(declare-sort $$unsorted 0)
+(declare-fun ssNder1_0 () Bool)
+(declare-fun ssNder1_1r1 ($$unsorted) Bool)
+(declare-fun ssNder1_2r1r1 ($$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_3r1r1r1 ($$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_4r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc30 () $$unsorted)
+(declare-fun ssPv16_5r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc31 () $$unsorted)
+(declare-fun ssNder1_5r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc28 () $$unsorted)
+(declare-fun ssPv15_6r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc29 () $$unsorted)
+(declare-fun ssNder1_6r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc26 () $$unsorted)
+(declare-fun ssPv14_7r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc27 () $$unsorted)
+(declare-fun ssNder1_7r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc24 () $$unsorted)
+(declare-fun ssPv13_8r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc25 () $$unsorted)
+(declare-fun ssNder1_8r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_9r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_10r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc22 () $$unsorted)
+(declare-fun ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc23 () $$unsorted)
+(declare-fun ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc20 () $$unsorted)
+(declare-fun ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc21 () $$unsorted)
+(declare-fun ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc18 () $$unsorted)
+(declare-fun ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc19 () $$unsorted)
+(declare-fun ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv20_1r1 ($$unsorted) Bool)
+(declare-fun ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc16 () $$unsorted)
+(declare-fun ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun skc17 () $$unsorted)
+(declare-fun ssPv12_9r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv19_2r1r1 ($$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv17_4r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv18_3r1r1r1 ($$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv11_10r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(declare-fun ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 ($$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted $$unsorted) Bool)
+(meta-info :filename "SYN874-1")
+(assert true)
+(assert (forall ((U $$unsorted)) (ssNder1_1r1 U) ))
+(assert (forall ((U $$unsorted) (V $$unsorted)) (or (not (ssNder1_1r1 U)) (ssNder1_2r1r1 U V)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted)) (or (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_3r1r1r1 U V W)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_4r1r1r1r1 U V W X)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv16_5r1r1r1r1r1 U V W X skc30)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted)) (or (not (ssPv16_5r1r1r1r1r1 U V W X skc31)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv15_6r1r1r1r1r1r1 U V W X Y skc28)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted)) (or (not (ssPv15_6r1r1r1r1r1r1 U V W X Y skc29)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z skc26)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted)) (or (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z skc27)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 skc24)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted)) (or (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 skc25)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted)) (or (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted)) (or (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted)) (or (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted)) (or (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 skc22)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted)) (or (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 skc23)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 skc20)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 skc21)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 skc18)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 skc19)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv20_1r1 U)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 skc16)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 skc17)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv16_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted)) (or (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted)) (or (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssPv19_2r1r1 U V)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv19_2r1r1 U V)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv17_4r1r1r1r1 U V W X)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted)) (or (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv20_1r1 U)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted)) (or (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U))) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssPv19_2r1r1 U V)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv16_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2) (ssPv18_3r1r1r1 U V W)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssPv18_3r1r1r1 U V W)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted)) (or (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv16_5r1r1r1r1r1 U V W X Y)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv17_4r1r1r1r1 U V W X)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssPv16_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8) (ssPv15_6r1r1r1r1r1r1 U V W X Y Z) (ssPv20_1r1 U)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted)) (or (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssPv20_1r1 U)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssPv18_3r1r1r1 U V W)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv11_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssPv17_4r1r1r1r1 U V W X)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssPv15_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11) (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted)) (or (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted) (X14 $$unsorted)) (or (not (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14)) (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssPv12_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssPv14_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv13_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) ))
+(assert (forall ((U $$unsorted) (V $$unsorted) (W $$unsorted) (X $$unsorted) (Y $$unsorted) (Z $$unsorted) (X1 $$unsorted) (X2 $$unsorted) (X3 $$unsorted) (X4 $$unsorted) (X5 $$unsorted) (X6 $$unsorted) (X7 $$unsorted) (X8 $$unsorted) (X9 $$unsorted) (X10 $$unsorted) (X11 $$unsorted) (X12 $$unsorted) (X13 $$unsorted) (X14 $$unsorted)) (or (not (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13)) (not (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12 X13 X14)) (not (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11 X12)) (not (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10 X11)) (not (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10)) (not (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9)) (not (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8)) (not (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7)) (not (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6)) (not (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5)) (not (ssNder1_10r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4)) (not (ssNder1_9r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3)) (not (ssNder1_8r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2)) (not (ssNder1_7r1r1r1r1r1r1r1 U V W X Y Z X1)) (not (ssNder1_6r1r1r1r1r1r1 U V W X Y Z)) (not (ssNder1_5r1r1r1r1r1 U V W X Y)) (not (ssNder1_4r1r1r1r1 U V W X)) (not (ssNder1_3r1r1r1 U V W)) (not (ssNder1_2r1r1 U V)) (not (ssNder1_1r1 U)) (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9 X10) (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 U V W X Y Z X1 X2 X3 X4 X5 X6 X7 X8 X9) (ssPv19_2r1r1 U V)) ))
+(assert true)
+(check-sat)