diff --git a/tests/ravi_sls.smt2 b/tests/ravi_sls.smt2
new file mode 100644
index 000000000..7db65dc40
--- /dev/null
+++ b/tests/ravi_sls.smt2
@@ -0,0 +1,443 @@
+(set-option :smt.relevancy 0)
+(set-option :smt.pb.conflict_frequency 10000)
+(set-option :opt.pb.compile_equality true)
+(set-option :smt.pb.enable_simplex true)
+; declare an integer variable for each mini-pathlet's multiplicity
+(declare-const A0_2_3_10 Int)
+(declare-const A0_2_3_5_4_7_9 Int)
+(declare-const A0_2_3_5_4_8_9 Int)
+(declare-const A0_1_3_10 Int)
+(declare-const A0_1_3_5_4_7_9 Int)
+(declare-const A0_1_3_5_4_8_9 Int)
+(declare-const A1_3_10 Int)
+(declare-const A1_3_5_4_7_9 Int)
+(declare-const A1_3_5_4_8_9 Int)
+(declare-const A2_3_10 Int)
+(declare-const A2_3_5_4_7_9 Int)
+(declare-const A2_3_5_4_8_9 Int)
+(declare-const A3_10 Int)
+(declare-const A3_5_4_7_9_12_13 Int)
+(declare-const A3_5_4_7_9_11_13 Int)
+(declare-const A3_5_4_8_9_12_13 Int)
+(declare-const A3_5_4_8_9_11_13 Int)
+(declare-const A4_7_9_12_13 Int)
+(declare-const A4_7_9_11_13 Int)
+(declare-const A4_8_9_12_13 Int)
+(declare-const A4_8_9_11_13 Int)
+(declare-const A5_4_7_9_12_13 Int)
+(declare-const A5_4_7_9_11_13 Int)
+(declare-const A5_4_8_9_12_13 Int)
+(declare-const A5_4_8_9_11_13 Int)
+(declare-const A6_21_10 Int)
+(declare-const A6_4_7_9_12_13 Int)
+(declare-const A6_4_7_9_11_13 Int)
+(declare-const A6_4_8_9_12_13 Int)
+(declare-const A6_4_8_9_11_13 Int)
+(declare-const A7_9_12_13 Int)
+(declare-const A7_9_11_13 Int)
+(declare-const A8_9_12_13 Int)
+(declare-const A8_9_11_13 Int)
+(declare-const A9_12_13_15_17_18 Int)
+(declare-const A9_12_13_15_17_16_19 Int)
+(declare-const A9_12_13_14_17_18 Int)
+(declare-const A9_12_13_14_17_16_19 Int)
+(declare-const A9_11_13_15_17_18 Int)
+(declare-const A9_11_13_15_17_16_19 Int)
+(declare-const A9_11_13_14_17_18 Int)
+(declare-const A9_11_13_14_17_16_19 Int)
+(declare-const A11_13_15_17_18_19 Int)
+(declare-const A11_13_15_17_16_19 Int)
+(declare-const A11_13_14_17_18_19 Int)
+(declare-const A11_13_14_17_16_19 Int)
+(declare-const A12_13_15_17_18_19 Int)
+(declare-const A12_13_15_17_16_19 Int)
+(declare-const A12_13_14_17_18_19 Int)
+(declare-const A12_13_14_17_16_19 Int)
+(declare-const A13_15_17_18_19 Int)
+(declare-const A13_15_17_16_19 Int)
+(declare-const A13_14_17_18_19 Int)
+(declare-const A13_14_17_16_19 Int)
+(declare-const A20_6_21_10 Int)
+(declare-const A20_6_4_7_9_12 Int)
+(declare-const A20_6_4_7_9_11 Int)
+(declare-const A20_6_4_8_9_12 Int)
+(declare-const A20_6_4_8_9_11 Int)
+(declare-const A21_10 Int)
+; positive mult for each minipathlet
+(assert (<= 0 A0_2_3_10))
+(assert (<= A0_2_3_10 4))
+(assert (<= 0 A0_2_3_5_4_7_9))
+(assert (<= A0_2_3_5_4_7_9 4))
+(assert (<= 0 A0_2_3_5_4_8_9))
+(assert (<= A0_2_3_5_4_8_9 4))
+(assert (<= 0 A0_1_3_10))
+(assert (<= A0_1_3_10 4))
+(assert (<= 0 A0_1_3_5_4_7_9))
+(assert (<= A0_1_3_5_4_7_9 4))
+(assert (<= 0 A0_1_3_5_4_8_9))
+(assert (<= A0_1_3_5_4_8_9 4))
+(assert (<= 0 A1_3_10))
+(assert (<= A1_3_10 4))
+(assert (<= 0 A1_3_5_4_7_9))
+(assert (<= A1_3_5_4_7_9 4))
+(assert (<= 0 A1_3_5_4_8_9))
+(assert (<= A1_3_5_4_8_9 4))
+(assert (<= 0 A2_3_10))
+(assert (<= A2_3_10 4))
+(assert (<= 0 A2_3_5_4_7_9))
+(assert (<= A2_3_5_4_7_9 4))
+(assert (<= 0 A2_3_5_4_8_9))
+(assert (<= A2_3_5_4_8_9 4))
+(assert (<= 0 A3_10))
+(assert (<= A3_10 4))
+(assert (<= 0 A3_5_4_7_9_12_13))
+(assert (<= A3_5_4_7_9_12_13 4))
+(assert (<= 0 A3_5_4_7_9_11_13))
+(assert (<= A3_5_4_7_9_11_13 4))
+(assert (<= 0 A3_5_4_8_9_12_13))
+(assert (<= A3_5_4_8_9_12_13 4))
+(assert (<= 0 A3_5_4_8_9_11_13))
+(assert (<= A3_5_4_8_9_11_13 4))
+(assert (<= 0 A4_7_9_12_13))
+(assert (<= A4_7_9_12_13 4))
+(assert (<= 0 A4_7_9_11_13))
+(assert (<= A4_7_9_11_13 4))
+(assert (<= 0 A4_8_9_12_13))
+(assert (<= A4_8_9_12_13 4))
+(assert (<= 0 A4_8_9_11_13))
+(assert (<= A4_8_9_11_13 4))
+(assert (<= 0 A5_4_7_9_12_13))
+(assert (<= A5_4_7_9_12_13 4))
+(assert (<= 0 A5_4_7_9_11_13))
+(assert (<= A5_4_7_9_11_13 4))
+(assert (<= 0 A5_4_8_9_12_13))
+(assert (<= A5_4_8_9_12_13 4))
+(assert (<= 0 A5_4_8_9_11_13))
+(assert (<= A5_4_8_9_11_13 4))
+(assert (<= 0 A6_21_10))
+(assert (<= A6_21_10 4))
+(assert (<= 0 A6_4_7_9_12_13))
+(assert (<= A6_4_7_9_12_13 4))
+(assert (<= 0 A6_4_7_9_11_13))
+(assert (<= A6_4_7_9_11_13 4))
+(assert (<= 0 A6_4_8_9_12_13))
+(assert (<= A6_4_8_9_12_13 4))
+(assert (<= 0 A6_4_8_9_11_13))
+(assert (<= A6_4_8_9_11_13 4))
+(assert (<= 0 A7_9_12_13))
+(assert (<= A7_9_12_13 4))
+(assert (<= 0 A7_9_11_13))
+(assert (<= A7_9_11_13 4))
+(assert (<= 0 A8_9_12_13))
+(assert (<= A8_9_12_13 4))
+(assert (<= 0 A8_9_11_13))
+(assert (<= A8_9_11_13 4))
+(assert (<= 0 A9_12_13_15_17_18))
+(assert (<= A9_12_13_15_17_18 4))
+(assert (<= 0 A9_12_13_15_17_16_19))
+(assert (<= A9_12_13_15_17_16_19 4))
+(assert (<= 0 A9_12_13_14_17_18))
+(assert (<= A9_12_13_14_17_18 4))
+(assert (<= 0 A9_12_13_14_17_16_19))
+(assert (<= A9_12_13_14_17_16_19 4))
+(assert (<= 0 A9_11_13_15_17_18))
+(assert (<= A9_11_13_15_17_18 4))
+(assert (<= 0 A9_11_13_15_17_16_19))
+(assert (<= A9_11_13_15_17_16_19 4))
+(assert (<= 0 A9_11_13_14_17_18))
+(assert (<= A9_11_13_14_17_18 4))
+(assert (<= 0 A9_11_13_14_17_16_19))
+(assert (<= A9_11_13_14_17_16_19 4))
+(assert (<= 0 A11_13_15_17_18_19))
+(assert (<= A11_13_15_17_18_19 4))
+(assert (<= 0 A11_13_15_17_16_19))
+(assert (<= A11_13_15_17_16_19 4))
+(assert (<= 0 A11_13_14_17_18_19))
+(assert (<= A11_13_14_17_18_19 4))
+(assert (<= 0 A11_13_14_17_16_19))
+(assert (<= A11_13_14_17_16_19 4))
+(assert (<= 0 A12_13_15_17_18_19))
+(assert (<= A12_13_15_17_18_19 4))
+(assert (<= 0 A12_13_15_17_16_19))
+(assert (<= A12_13_15_17_16_19 4))
+(assert (<= 0 A12_13_14_17_18_19))
+(assert (<= A12_13_14_17_18_19 4))
+(assert (<= 0 A12_13_14_17_16_19))
+(assert (<= A12_13_14_17_16_19 4))
+(assert (<= 0 A13_15_17_18_19))
+(assert (<= A13_15_17_18_19 4))
+(assert (<= 0 A13_15_17_16_19))
+(assert (<= A13_15_17_16_19 4))
+(assert (<= 0 A13_14_17_18_19))
+(assert (<= A13_14_17_18_19 4))
+(assert (<= 0 A13_14_17_16_19))
+(assert (<= A13_14_17_16_19 4))
+(assert (<= 0 A20_6_21_10))
+(assert (<= A20_6_21_10 4))
+(assert (<= 0 A20_6_4_7_9_12))
+(assert (<= A20_6_4_7_9_12 4))
+(assert (<= 0 A20_6_4_7_9_11))
+(assert (<= A20_6_4_7_9_11 4))
+(assert (<= 0 A20_6_4_8_9_12))
+(assert (<= A20_6_4_8_9_12 4))
+(assert (<= 0 A20_6_4_8_9_11))
+(assert (<= A20_6_4_8_9_11 4))
+(assert (<= 0 A21_10))
+(assert (<= A21_10 4))
+; range of multiplicities for each contig-pair
+; contigs 0 1, #pairs 7, dist 8.36
+(assert (and (<= 0 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) (<= (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9) 4)))
+(assert-soft (= 0 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 2.852312) ; p=0001405
+(assert-soft (= 1 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 0.852312) ; p=0140504
+(assert-soft (= 2 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 1.408176) ; p=0039068
+(assert-soft (= 3 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 2.838611) ; p=0001450
+(assert-soft (= 4 (+ A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 4.627113) ; p=0000024
+; contigs 1 3, #pairs 5, dist 1.07
+(assert (and (<= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) (<= (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9) 4)))
+(assert-soft (= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 4.168291) ; p=0000068
+(assert-soft (= 1 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 2.168291) ; p=0006787
+(assert-soft (= 2 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.195873) ; p=0063698
+(assert-soft (= 3 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 0.848149) ; p=0141857
+(assert-soft (= 4 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 0.756187) ; p=0175313
+; contigs 2 3, #pairs 4, dist 1.07
+(assert (and (<= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) (<= (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9) 4)))
+(assert-soft (= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 3.535379) ; p=0000291
+(assert-soft (= 1 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.535379) ; p=0029149
+(assert-soft (= 2 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 0.874154) ; p=0133612
+(assert-soft (= 3 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 0.712685) ; p=0193783
+(assert-soft (= 4 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 0.755826) ; p=0175458
+; contigs 3 4, #pairs 3, dist 2.77
+(assert (and (<= 0 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) (<= (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 5.564238) ; p=0000003
+(assert-soft (= 1 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 3.564238) ; p=0000273
+(assert-soft (= 2 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 2.714464) ; p=0001930
+(assert-soft (= 3 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 2.239507) ; p=0005761
+(assert-soft (= 4 (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.918007) ; p=0012078
+; contigs 4 9, #pairs 2, dist 1.24
+(assert (and (<= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) (<= (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 4.280499) ; p=0000052
+(assert-soft (= 1 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 2.280499) ; p=0005242
+(assert-soft (= 2 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.725376) ; p=0018820
+(assert-soft (= 3 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.420131) ; p=0038007
+(assert-soft (= 4 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.217191) ; p=0060647
+; contigs 5 9, #pairs 1, dist 1.46
+(assert (and (<= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) (<= (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 6.000000) ; p=0000001
+(assert-soft (= 1 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 4.000000) ; p=0000100
+(assert-soft (= 2 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 6.000000) ; p=0000001
+(assert-soft (= 3 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 8.000000) ; p=0000000
+(assert-soft (= 4 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 1.0000000) ; p=0000000
+; contigs 6 9, #pairs 0, dist 2.79
+(assert (and (<= 0 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) (<= (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
+(assert-soft (= 1 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
+(assert-soft (= 2 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
+(assert-soft (= 3 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
+(assert-soft (= 4 (+ A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.100798) ; p=0079287
+; contigs 7 9, #pairs 4, dist 1.08
+(assert (and (<= 0 (+ A7_9_12_13 A7_9_11_13)) (<= (+ A7_9_12_13 A7_9_11_13) 4)))
+(assert-soft (= 0 (+ A7_9_12_13 A7_9_11_13)) :dweight 4.830293) ; p=0000015
+(assert-soft (= 1 (+ A7_9_12_13 A7_9_11_13)) :dweight 2.830293) ; p=0001478
+(assert-soft (= 2 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.839248) ; p=0014479
+(assert-soft (= 3 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.347958) ; p=0044879
+(assert-soft (= 4 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.061278) ; p=0086840
+; contigs 8 9, #pairs 2, dist 1.10
+(assert (and (<= 0 (+ A8_9_12_13 A8_9_11_13)) (<= (+ A8_9_12_13 A8_9_11_13) 4)))
+(assert-soft (= 0 (+ A8_9_12_13 A8_9_11_13)) :dweight 3.085052) ; p=0000822
+(assert-soft (= 1 (+ A8_9_12_13 A8_9_11_13)) :dweight 1.085052) ; p=0082214
+(assert-soft (= 2 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.712306) ; p=0193952
+(assert-soft (= 3 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.589437) ; p=0257373
+(assert-soft (= 4 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.568873) ; p=0269853
+; contigs 9 12, #pairs 1, dist 1.77
+(assert (and (<= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) (<= (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 2.518279) ; p=0003032
+(assert-soft (= 1 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.518279) ; p=0303195
+(assert-soft (= 2 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.434295) ; p=0367879
+(assert-soft (= 3 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.475249) ; p=0334773
+(assert-soft (= 4 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)) :dweight 0.567356) ; p=0270797
+; contigs 11 13, #pairs 2, dist 1.00
+(assert (and (<= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) (<= (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 2.755831) ; p=0001755
+(assert-soft (= 1 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.755831) ; p=0175456
+(assert-soft (= 2 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.568471) ; p=0270103
+(assert-soft (= 3 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.630988) ; p=0233890
+(assert-soft (= 4 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.795810) ; p=0160026
+; contigs 12 13, #pairs 2, dist 1.01
+(assert (and (<= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) (<= (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 2.662349) ; p=0002176
+(assert-soft (= 1 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 0.662349) ; p=0217596
+(assert-soft (= 2 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 0.583662) ; p=0260818
+(assert-soft (= 3 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 0.754853) ; p=0175852
+(assert-soft (= 4 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 1.028349) ; p=0093681
+; contigs 13 15, #pairs 1, dist 2.58
+(assert (and (<= 0 (+ A13_15_17_18_19 A13_15_17_16_19)) (<= (+ A13_15_17_18_19 A13_15_17_16_19) 4)))
+(assert-soft (= 0 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 2.434616) ; p=0003676
+(assert-soft (= 1 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 0.434616) ; p=0367607
+(assert-soft (= 2 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 0.584809) ; p=0260130
+(assert-soft (= 3 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 0.859941) ; p=0138057
+(assert-soft (= 4 (+ A13_15_17_18_19 A13_15_17_16_19)) :dweight 1.186226) ; p=0065129
+; contigs 20 6, #pairs 7, dist 1.085
+(assert (and (<= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) (<= (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11) 4)))
+(assert-soft (= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 2.850723) ; p=0001410
+(assert-soft (= 1 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 0.850723) ; p=0141019
+(assert-soft (= 2 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 2.181023) ; p=0006591
+(assert-soft (= 3 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 4.385894) ; p=0000041
+(assert-soft (= 4 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 6.948833) ; p=0000000
+; contigs 21 10, #pairs 1, dist 1.2
+(assert (and (<= 0 (+ A21_10)) (<= (+ A21_10) 4)))
+(assert-soft (= 0 (+ A21_10)) :dweight 2.629839) ; p=0002345
+(assert-soft (= 1 (+ A21_10)) :dweight 0.629839) ; p=0234510
+(assert-soft (= 2 (+ A21_10)) :dweight 0.469677) ; p=0339096
+(assert-soft (= 3 (+ A21_10)) :dweight 0.434455) ; p=0367744
+(assert-soft (= 4 (+ A21_10)) :dweight 0.450384) ; p=0354499
+; range of multiplicities for each contig
+; contig 0, length 931, #reads 41, min 0, max 4
+(assert (and (<= 0 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) (<= (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9) 4)))
+(assert-soft (= 0 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 4.060041) ; p=0000087
+(assert-soft (= 1 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 2.060041) ; p=0008709
+(assert-soft (= 2 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 1.3620829) ; p=0000000
+(assert-soft (= 3 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 3.0304105) ; p=0000000
+(assert-soft (= 4 (+ A0_2_3_10 A0_2_3_5_4_7_9 A0_2_3_5_4_8_9 A0_1_3_10 A0_1_3_5_4_7_9 A0_1_3_5_4_8_9)) :dweight 4.9084634) ; p=0000000
+; contig 1, length 195, #reads 16, min 0, max 4
+(assert (and (<= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) (<= (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9) 4)))
+(assert-soft (= 0 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 5.312217) ; p=0000005
+(assert-soft (= 1 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 3.312217) ; p=0000487
+(assert-soft (= 2 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.202826) ; p=0062686
+(assert-soft (= 3 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.092455) ; p=0080825
+(assert-soft (= 4 (+ A1_3_10 A1_3_5_4_7_9 A1_3_5_4_8_9)) :dweight 1.800524) ; p=0015830
+; contig 2, length 198, #reads 21, min 0, max 4
+(assert (and (<= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) (<= (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9) 4)))
+(assert-soft (= 0 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 7.526226) ; p=0000000
+(assert-soft (= 1 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 5.526226) ; p=0000003
+(assert-soft (= 2 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.998081) ; p=0010044
+(assert-soft (= 3 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.093650) ; p=0080603
+(assert-soft (= 4 (+ A2_3_10 A2_3_5_4_7_9 A2_3_5_4_8_9)) :dweight 1.263422) ; p=0054523
+; contig 3, length 347, #reads 56, min 0, max 4
+(assert (and (<= 0 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) (<= (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.6034953) ; p=0000000
+(assert-soft (= 1 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.4034953) ; p=0000000
+(assert-soft (= 2 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 4.261782) ; p=0000055
+(assert-soft (= 3 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.485181) ; p=0032720
+(assert-soft (= 4 (+ A3_10 A3_5_4_7_9_12_13 A3_5_4_7_9_11_13 A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)) :dweight 1.573120) ; p=0026723
+; contig 4, length 113, #reads 8, min 0, max 4
+(assert (and (<= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) (<= (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 7.744934) ; p=0000000
+(assert-soft (= 1 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 5.744934) ; p=0000002
+(assert-soft (= 2 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 3.682280) ; p=0000208
+(assert-soft (= 3 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 2.619135) ; p=0002404
+(assert-soft (= 4 (+ A4_7_9_12_13 A4_7_9_11_13 A4_8_9_12_13 A4_8_9_11_13)) :dweight 1.965211) ; p=0010834
+; contig 5, length 101, #reads 2, min 0, max 4
+(assert (and (<= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) (<= (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 4.686648) ; p=0000021
+(assert-soft (= 1 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 2.686648) ; p=0002058
+(assert-soft (= 2 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 2.113387) ; p=0007702
+(assert-soft (= 3 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 1.790003) ; p=0016218
+(assert-soft (= 4 (+ A5_4_7_9_12_13 A5_4_7_9_11_13 A5_4_8_9_12_13 A5_4_8_9_11_13)) :dweight 1.568925) ; p=0026982
+; contig 6, length 223, #reads 24, min 0, max 4
+(assert (and (<= 0 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) (<= (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13) 4)))
+(assert-soft (= 0 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 7.515357) ; p=0000000
+(assert-soft (= 1 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 5.515357) ; p=0000003
+(assert-soft (= 2 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.804093) ; p=0015700
+(assert-soft (= 3 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.091359) ; p=0081029
+(assert-soft (= 4 (+ A6_21_10 A6_4_7_9_12_13 A6_4_7_9_11_13 A6_4_8_9_12_13 A6_4_8_9_11_13)) :dweight 1.606284) ; p=0024758
+; contig 7, length 191, #reads 9, min 0, max 4
+(assert (and (<= 0 (+ A7_9_12_13 A7_9_11_13)) (<= (+ A7_9_12_13 A7_9_11_13) 4)))
+(assert-soft (= 0 (+ A7_9_12_13 A7_9_11_13)) :dweight 3.169161) ; p=0000677
+(assert-soft (= 1 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.169161) ; p=0067739
+(assert-soft (= 2 (+ A7_9_12_13 A7_9_11_13)) :dweight 1.051784) ; p=0088760
+(assert-soft (= 3 (+ A7_9_12_13 A7_9_11_13)) :dweight 2.058857) ; p=0008733
+(assert-soft (= 4 (+ A7_9_12_13 A7_9_11_13)) :dweight 3.526301) ; p=0000298
+; contig 8, length 200, #reads 12, min 0, max 4
+(assert (and (<= 0 (+ A8_9_12_13 A8_9_11_13)) (<= (+ A8_9_12_13 A8_9_11_13) 4)))
+(assert-soft (= 0 (+ A8_9_12_13 A8_9_11_13)) :dweight 3.724714) ; p=0000188
+(assert-soft (= 1 (+ A8_9_12_13 A8_9_11_13)) :dweight 1.724714) ; p=0018849
+(assert-soft (= 2 (+ A8_9_12_13 A8_9_11_13)) :dweight 0.963436) ; p=0108784
+(assert-soft (= 3 (+ A8_9_12_13 A8_9_11_13)) :dweight 1.701424) ; p=0019887
+(assert-soft (= 4 (+ A8_9_12_13 A8_9_11_13)) :dweight 3.053242) ; p=0000885
+; contig 9, length 269, #reads 32, min 0, max 4
+(assert (and (<= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) (<= (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 8.757585) ; p=0000000
+(assert-soft (= 1 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 6.757585) ; p=0000000
+(assert-soft (= 2 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 1.962827) ; p=0010894
+(assert-soft (= 3 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 1.166108) ; p=0068217
+(assert-soft (= 4 (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19 A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)) :dweight 2.006269) ; p=0009857
+; contig 11, length 170, #reads 7, min 0, max 4
+(assert (and (<= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) (<= (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 3.066473) ; p=0000858
+(assert-soft (= 1 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 1.066473) ; p=0085808
+(assert-soft (= 2 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 0.946381) ; p=0113141
+(assert-soft (= 3 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 1.700861) ; p=0019913
+(assert-soft (= 4 (+ A11_13_15_17_18_19 A11_13_15_17_16_19 A11_13_14_17_18_19 A11_13_14_17_16_19)) :dweight 2.813408) ; p=0001537
+; contig 12, length 198, #reads 15, min 0, max 4
+(assert (and (<= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) (<= (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 4.784554) ; p=0000016
+(assert-soft (= 1 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 2.784554) ; p=0001642
+(assert-soft (= 2 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 1.062589) ; p=0086579
+(assert-soft (= 3 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 1.214705) ; p=0060995
+(assert-soft (= 4 (+ A12_13_15_17_18_19 A12_13_15_17_16_19 A12_13_14_17_18_19 A12_13_14_17_16_19)) :dweight 2.134110) ; p=0007343
+; contig 13, length 349, #reads 28, min 0, max 4
+(assert (and (<= 0 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) (<= (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19) 4)))
+(assert-soft (= 0 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 4.577071) ; p=0000026
+(assert-soft (= 1 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 2.577071) ; p=0002648
+(assert-soft (= 2 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 1.290338) ; p=0051246
+(assert-soft (= 3 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 3.501889) ; p=0000315
+(assert-soft (= 4 (+ A13_15_17_18_19 A13_15_17_16_19 A13_14_17_18_19 A13_14_17_16_19)) :dweight 7.145711) ; p=0000000
+; contig 20, length 1151, #reads 32, min 0, max 4
+(assert (and (<= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) (<= (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11) 4)))
+(assert-soft (= 0 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 8.689981) ; p=0000000
+(assert-soft (= 1 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 6.689981) ; p=0000000
+(assert-soft (= 2 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 2.7295778) ; p=0000000
+(assert-soft (= 3 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 5.1899615) ; p=0000000
+(assert-soft (= 4 (+ A20_6_21_10 A20_6_4_7_9_12 A20_6_4_7_9_11 A20_6_4_8_9_12 A20_6_4_8_9_11)) :dweight 7.8140332) ; p=0000000
+; contig 21, length 107, #reads 4, min 0, max 4
+(assert (and (<= 0 (+ A21_10)) (<= (+ A21_10) 4)))
+(assert-soft (= 0 (+ A21_10)) :dweight 5.154038) ; p=0000007
+(assert-soft (= 1 (+ A21_10)) :dweight 3.154038) ; p=0000701
+(assert-soft (= 2 (+ A21_10)) :dweight 2.122711) ; p=0007539
+(assert-soft (= 3 (+ A21_10)) :dweight 1.591139) ; p=0025637
+(assert-soft (= 4 (+ A21_10)) :dweight 1.264177) ; p=0054428
+; consistency of minipathlet multiplicities
+(assert (= (+ A9_12_13_15_17_18) (+ A12_13_15_17_18_19)))
+(assert (= (+ A5_4_7_9_11_13 A6_4_7_9_11_13) (+ A4_7_9_11_13)))
+(assert (= (+ A0_2_3_5_4_8_9) (+ A2_3_5_4_8_9)))
+(assert (= (+ A1_3_5_4_8_9 A2_3_5_4_8_9) (+ A3_5_4_8_9_12_13 A3_5_4_8_9_11_13)))
+(assert (= (+ A9_11_13_14_17_16_19) (+ A11_13_14_17_16_19)))
+(assert (= (+ A11_13_14_17_16_19 A12_13_14_17_16_19) (+ A13_14_17_16_19)))
+(assert (= (+ A20_6_21_10) (+ A6_21_10)))
+(assert (= (+ A11_13_14_17_18_19 A12_13_14_17_18_19) (+ A13_14_17_18_19)))
+(assert (= (+ A0_1_3_5_4_7_9) (+ A1_3_5_4_7_9)))
+(assert (= (+ A9_12_13_14_17_18) (+ A12_13_14_17_18_19)))
+(assert (= (+ A1_3_10 A2_3_10) (+ A3_10)))
+(assert (= (+ A11_13_15_17_18_19 A12_13_15_17_18_19) (+ A13_15_17_18_19)))
+(assert (= (+ A11_13_15_17_16_19 A12_13_15_17_16_19) (+ A13_15_17_16_19)))
+(assert (= (+ A9_12_13_14_17_16_19) (+ A12_13_14_17_16_19)))
+(assert (= (+ A7_9_11_13 A8_9_11_13) (+ A9_11_13_15_17_18 A9_11_13_15_17_16_19 A9_11_13_14_17_18 A9_11_13_14_17_16_19)))
+(assert (= (+ A0_2_3_5_4_7_9) (+ A2_3_5_4_7_9)))
+(assert (= (+ A4_8_9_11_13) (+ A8_9_11_13)))
+(assert (= (+ A0_1_3_10) (+ A1_3_10)))
+(assert (= (+ A20_6_4_8_9_12) (+ A6_4_8_9_12_13)))
+(assert (= (+ A3_5_4_8_9_11_13) (+ A5_4_8_9_11_13)))
+(assert (= (+ A0_1_3_5_4_8_9) (+ A1_3_5_4_8_9)))
+(assert (= (+ A5_4_8_9_11_13 A6_4_8_9_11_13) (+ A4_8_9_11_13)))
+(assert (= (+ A20_6_4_7_9_12) (+ A6_4_7_9_12_13)))
+(assert (= (+ A20_6_4_7_9_11) (+ A6_4_7_9_11_13)))
+(assert (= (+ A3_5_4_8_9_12_13) (+ A5_4_8_9_12_13)))
+(assert (= (+ A4_7_9_12_13) (+ A7_9_12_13)))
+(assert (= (+ A9_12_13_15_17_16_19) (+ A12_13_15_17_16_19)))
+(assert (= (+ A9_11_13_15_17_16_19) (+ A11_13_15_17_16_19)))
+(assert (= (+ A1_3_5_4_7_9 A2_3_5_4_7_9) (+ A3_5_4_7_9_12_13 A3_5_4_7_9_11_13)))
+(assert (= (+ A3_5_4_7_9_12_13) (+ A5_4_7_9_12_13)))
+(assert (= (+ A7_9_12_13 A8_9_12_13) (+ A9_12_13_15_17_18 A9_12_13_15_17_16_19 A9_12_13_14_17_18 A9_12_13_14_17_16_19)))
+(assert (= (+ A0_2_3_10) (+ A2_3_10)))
+(assert (= (+ A9_11_13_14_17_18) (+ A11_13_14_17_18_19)))
+(assert (= (+ A4_8_9_12_13) (+ A8_9_12_13)))
+(assert (= (+ A5_4_7_9_12_13 A6_4_7_9_12_13) (+ A4_7_9_12_13)))
+(assert (= (+ A9_11_13_15_17_18) (+ A11_13_15_17_18_19)))
+(assert (= (+ A6_21_10) (+ A21_10)))
+(assert (= (+ A20_6_4_8_9_11) (+ A6_4_8_9_11_13)))
+(assert (= (+ A3_5_4_7_9_11_13) (+ A5_4_7_9_11_13)))
+(assert (= (+ A5_4_8_9_12_13 A6_4_8_9_12_13) (+ A4_8_9_12_13)))
+(assert (= (+ A4_7_9_11_13) (+ A7_9_11_13)))
+(optimize :print_statistics true
+ :wmaxsat_engine sls
+ :maxsat_engine weighted_maxsat)