(set-info :smt-lib-version 2.6)
(set-logic QF_DT)
(set-info :source |
Generated by: Pierre Bouvier
Generated on: 2021-03-12
Application: Automatic decomposition of Petri Nets into Automata Networks
Target solver: CVC4, Z3
Publications:
[1] Pierre Bouvier, Hubert Garavel, and Hernan Ponce de Leon.
"Automatic Decomposition of Petri Nets into Automata Networks -
A Synthetic Account". Proceedings PETRI NETS 2020, LNCS 12152,
Springer. https://doi.org/10.1007/978-3-030-51831-8_1
[2] Hubert Garavel. "Nested-Unit Petri Nets". Journal of Logical
and Algebraic Methods in Programming, vol. 104, Elsevier, 2019.
https://doi.org/10.1016/j.jlamp.2018.11.005
In [1], several methods for decomposing an ordinary, safe Petri net
into a flat, unit-safe NUPN [2], have been proposed. These methods
are implemented in a complete tool chain involving SAT solvers, SMT
solvers, and tools for graph coloring and finding maximal cliques.
From a data set of 12,000+ NUPN models, 51,000+ SMT formulas have
been generated, out of which a subset of 1200 interesting formulas
to be used as SMT-LIB 2.6 benchmarks was carefully selected.
Original filename: vlsat3_b10.smt2
Specific parameters for the present benchmark:
- number of places: 56
- number of units: 17
- number of edges in the concurrency graph: 1407
- number of variables: 56
- number of uninterpreted functions: 0
- number of asserts: 1423
- total number of operators in asserts: 4539
|)
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status unsat)
(declare-datatype Unit ((u0) (u1) (u2) (u3) (u4) (u5) (u6) (u7) (u8) (u9) (u10) (u11) (u12) (u13) (u14) (u15) (u16)))
(declare-fun p1 () Unit)
(declare-fun p2 () Unit)
(declare-fun p3 () Unit)
(declare-fun p4 () Unit)
(declare-fun p5 () Unit)
(declare-fun p6 () Unit)
(declare-fun p7 () Unit)
(declare-fun p8 () Unit)
(declare-fun p9 () Unit)
(declare-fun p10 () Unit)
(declare-fun p11 () Unit)
(declare-fun p12 () Unit)
(declare-fun p13 () Unit)
(declare-fun p14 () Unit)
(declare-fun p15 () Unit)
(declare-fun p16 () Unit)
(declare-fun p17 () Unit)
(declare-fun p18 () Unit)
(declare-fun p19 () Unit)
(declare-fun p20 () Unit)
(declare-fun p21 () Unit)
(declare-fun p22 () Unit)
(declare-fun p23 () Unit)
(declare-fun p24 () Unit)
(declare-fun p25 () Unit)
(declare-fun p26 () Unit)
(declare-fun p27 () Unit)
(declare-fun p28 () Unit)
(declare-fun p29 () Unit)
(declare-fun p30 () Unit)
(declare-fun p31 () Unit)
(declare-fun p32 () Unit)
(declare-fun p33 () Unit)
(declare-fun p34 () Unit)
(declare-fun p35 () Unit)
(declare-fun p36 () Unit)
(declare-fun p37 () Unit)
(declare-fun p38 () Unit)
(declare-fun p39 () Unit)
(declare-fun p40 () Unit)
(declare-fun p41 () Unit)
(declare-fun p42 () Unit)
(declare-fun p43 () Unit)
(declare-fun p44 () Unit)
(declare-fun p45 () Unit)
(declare-fun p46 () Unit)
(declare-fun p47 () Unit)
(declare-fun p48 () Unit)
(declare-fun p49 () Unit)
(declare-fun p50 () Unit)
(declare-fun p51 () Unit)
(declare-fun p52 () Unit)
(declare-fun p53 () Unit)
(declare-fun p54 () Unit)
(declare-fun p55 () Unit)
(declare-fun p56 () Unit)
(assert (= p1 u0))
(assert (or (= p2 u0) (= p2 u1)))
(assert (or (= p3 u0) (= p3 u1) (= p3 u2)))
(assert (or (= p4 u0) (= p4 u1) (= p4 u2) (= p4 u3)))
(assert (or (= p5 u0) (= p5 u1) (= p5 u2) (= p5 u3) (= p5 u4)))
(assert (or (= p6 u0) (= p6 u1) (= p6 u2) (= p6 u3) (= p6 u4) (= p6 u5)))
(assert (or (= p7 u0) (= p7 u1) (= p7 u2) (= p7 u3) (= p7 u4) (= p7 u5) (= p7 u6)))
(assert (or (= p8 u0) (= p8 u1) (= p8 u2) (= p8 u3) (= p8 u4) (= p8 u5) (= p8 u6) (= p8 u7)))
(assert (or (= p9 u0) (= p9 u1) (= p9 u2) (= p9 u3) (= p9 u4) (= p9 u5) (= p9 u6) (= p9 u7) (= p9 u8)))
(assert (or (= p10 u0) (= p10 u1) (= p10 u2) (= p10 u3) (= p10 u4) (= p10 u5) (= p10 u6) (= p10 u7) (= p10 u8) (= p10 u9)))
(assert (or (= p11 u0) (= p11 u1) (= p11 u2) (= p11 u3) (= p11 u4) (= p11 u5) (= p11 u6) (= p11 u7) (= p11 u8) (= p11 u9) (= p11 u10)))
(assert (or (= p12 u0) (= p12 u1) (= p12 u2) (= p12 u3) (= p12 u4) (= p12 u5) (= p12 u6) (= p12 u7) (= p12 u8) (= p12 u9) (= p12 u10) (= p12 u11)))
(assert (or (= p13 u0) (= p13 u1) (= p13 u2) (= p13 u3) (= p13 u4) (= p13 u5) (= p13 u6) (= p13 u7) (= p13 u8) (= p13 u9) (= p13 u10) (= p13 u11) (= p13 u12)))
(assert (or (= p14 u0) (= p14 u1) (= p14 u2) (= p14 u3) (= p14 u4) (= p14 u5) (= p14 u6) (= p14 u7) (= p14 u8) (= p14 u9) (= p14 u10) (= p14 u11) (= p14 u12) (= p14 u13)))
(assert (or (= p15 u0) (= p15 u1) (= p15 u2) (= p15 u3) (= p15 u4) (= p15 u5) (= p15 u6) (= p15 u7) (= p15 u8) (= p15 u9) (= p15 u10) (= p15 u11) (= p15 u12) (= p15 u13) (= p15 u14)))
(assert (or (= p16 u0) (= p16 u1) (= p16 u2) (= p16 u3) (= p16 u4) (= p16 u5) (= p16 u6) (= p16 u7) (= p16 u8) (= p16 u9) (= p16 u10) (= p16 u11) (= p16 u12) (= p16 u13) (= p16 u14) (= p16 u15)))
(assert (distinct p33 p55))
(assert (distinct p22 p29))
(assert (distinct p5 p37))
(assert (distinct p8 p26))
(assert (distinct p30 p45))
(assert (distinct p34 p42))
(assert (distinct p17 p48))
(assert (distinct p16 p31))
(assert (distinct p14 p21))
(assert (distinct p1 p56))
(assert (distinct p26 p50))
(assert (distinct p2 p41))
(assert (distinct p22 p38))
(assert (distinct p5 p36))
(assert (distinct p9 p39))
(assert (distinct p8 p23))
(assert (distinct p30 p38))
(assert (distinct p34 p35))
(assert (distinct p17 p39))
(assert (distinct p37 p42))
(assert (distinct p13 p51))
(assert (distinct p38 p55))
(assert (distinct p46 p55))
(assert (distinct p50 p52))
(assert (distinct p1 p15))
(assert (distinct p4 p12))
(assert (distinct p2 p34))
(assert (distinct p22 p47))
(assert (distinct p5 p43))
(assert (distinct p9 p46))
(assert (distinct p8 p16))
(assert (distinct p17 p30))
(assert (distinct p42 p44))
(assert (distinct p6 p54))
(assert (distinct p10 p51))
(assert (distinct p13 p42))
(assert (distinct p18 p51))
(assert (distinct p11 p20))
(assert (distinct p22 p56))
(assert (distinct p5 p18))
(assert (distinct p27 p35))
(assert (distinct p30 p56))
(assert (distinct p23 p31))
(assert (distinct p13 p33))
(assert (distinct p18 p44))
(assert (distinct p43 p54))
(assert (distinct p11 p27))
(assert (distinct p1 p29))
(assert (distinct p15 p39))
(assert (distinct p2 p52))
(assert (distinct p22 p49))
(assert (distinct p5 p25))
(assert (distinct p27 p46))
(assert (distinct p30 p49))
(assert (distinct p34 p54))
(assert (distinct p6 p40))
(assert (distinct p31 p50))
(assert (distinct p35 p45))
(assert (distinct p18 p45))
(assert (distinct p1 p20))
(assert (distinct p15 p42))
(assert (distinct p2 p53))
(assert (distinct p27 p53))
(assert (distinct p47 p52))
(assert (distinct p3 p46))
(assert (distinct p23 p41))
(assert (distinct p6 p33))
(assert (distinct p10 p38))
(assert (distinct p18 p38))
(assert (distinct p38 p43))
(assert (distinct p14 p50))
(assert (distinct p15 p49))
(assert (distinct p2 p14))
(assert (distinct p5 p15))
(assert (distinct p3 p37))
(assert (distinct p23 p36))
(assert (distinct p6 p42))
(assert (distinct p10 p47))
(assert (distinct p31 p36))
(assert (distinct p18 p31))
(assert (distinct p11 p56))
(assert (distinct p14 p43))
(assert (distinct p19 p56))
(assert (distinct p39 p51))
(assert (distinct p12 p29))
(assert (distinct p20 p30))
(assert (distinct p6 p19))
(assert (distinct p28 p46))
(assert (distinct p31 p43))
(assert (distinct p24 p26))
(assert (distinct p7 p52))
(assert (distinct p14 p36))
(assert (distinct p19 p47))
(assert (distinct p39 p54))
(assert (distinct p12 p22))
(assert (distinct p2 p32))
(assert (distinct p16 p34))
(assert (distinct p20 p35))
(assert (distinct p3 p55))
(assert (distinct p6 p28))
(assert (distinct p28 p35))
(assert (distinct p31 p46))
(assert (distinct p35 p49))
(assert (distinct p7 p43))
(assert (distinct p32 p55))
(assert (distinct p36 p52))
(assert (distinct p19 p42))
(assert (distinct p39 p45))
(assert (distinct p44 p52))
(assert (distinct p2 p17))
(assert (distinct p16 p47))
(assert (distinct p20 p44))
(assert (distinct p3 p50))
(assert (distinct p23 p53))
(assert (distinct p48 p53))
(assert (distinct p4 p51))
(assert (distinct p24 p48))
(assert (distinct p7 p46))
(assert (distinct p11 p33))
(assert (distinct p19 p33))
(assert (distinct p9 p23))
(assert (distinct p16 p56))
(assert (distinct p20 p49))
(assert (distinct p3 p9))
(assert (distinct p25 p38))
(assert (distinct p6 p14))
(assert (distinct p28 p49))
(assert (distinct p24 p37))
(assert (distinct p7 p37))
(assert (distinct p11 p44))
(assert (distinct p32 p37))
(assert (distinct p19 p28))
(assert (distinct p41 p53))
(assert (distinct p9 p30))
(assert (distinct p15 p24))
(assert (distinct p40 p54))
(assert (distinct p13 p26))
(assert (distinct p3 p4))
(assert (distinct p25 p45))
(assert (distinct p21 p25))
(assert (distinct p4 p33))
(assert (distinct p7 p32))
(assert (distinct p29 p41))
(assert (distinct p33 p44))
(assert (distinct p32 p46))
(assert (distinct p8 p53))
(assert (distinct p12 p50))
(assert (distinct p15 p31))
(assert (distinct p40 p51))
(assert (distinct p13 p17))
(assert (distinct p3 p27))
(assert (distinct p25 p52))
(assert (distinct p1 p45))
(assert (distinct p21 p40))
(assert (distinct p4 p42))
(assert (distinct p7 p23))
(assert (distinct p29 p40))
(assert (distinct p33 p35))
(assert (distinct p32 p43))
(assert (distinct p36 p48))
(assert (distinct p9 p12))
(assert (distinct p8 p46))
(assert (distinct p12 p55))
(assert (distinct p37 p55))
(assert (distinct p40 p44))
(assert (distinct p45 p55))
(assert (distinct p49 p50))
(assert (distinct p3 p22))
(assert (distinct p1 p36))
(assert (distinct p21 p47))
(assert (distinct p4 p47))
(assert (distinct p24 p52))
(assert (distinct p7 p10))
(assert (distinct p41 p42))
(assert (distinct p5 p56))
(assert (distinct p9 p51))
(assert (distinct p8 p43))
(assert (distinct p12 p48))
(assert (distinct p17 p51))
(assert (distinct p45 p46))
(assert (distinct p10 p22))
(assert (distinct p21 p54))
(assert (distinct p4 p24))
(assert (distinct p26 p39))
(assert (distinct p29 p54))
(assert (distinct p33 p49))
(assert (distinct p8 p36))
(assert (distinct p12 p37))
(assert (distinct p17 p42))
(assert (distinct p42 p56))
(assert (distinct p10 p31))
(assert (distinct p16 p17))
(assert (distinct p14 p27))
(assert (distinct p1 p50))
(assert (distinct p4 p29))
(assert (distinct p26 p48))
(assert (distinct p33 p56))
(assert (distinct p22 p28))
(assert (distinct p5 p38))
(assert (distinct p9 p33))
(assert (distinct p8 p25))
(assert (distinct p30 p44))
(assert (distinct p34 p41))
(assert (distinct p17 p33))
(assert (distinct p13 p53))
(assert (distinct p16 p26))
(assert (distinct p14 p20))
(assert (distinct p1 p9))
(assert (distinct p26 p49))
(assert (distinct p2 p48))
(assert (distinct p22 p37))
(assert (distinct p5 p45))
(assert (distinct p9 p40))
(assert (distinct p8 p18))
(assert (distinct p30 p37))
(assert (distinct p17 p40))
(assert (distinct p37 p43))
(assert (distinct p13 p52))
(assert (distinct p38 p54))
(assert (distinct p46 p54))
(assert (distinct p50 p51))
(assert (distinct p1 p16))
(assert (distinct p4 p11))
(assert (distinct p2 p33))
(assert (distinct p22 p46))
(assert (distinct p5 p44))
(assert (distinct p9 p47))
(assert (distinct p8 p15))
(assert (distinct p17 p31))
(assert (distinct p42 p43))
(assert (distinct p6 p53))
(assert (distinct p10 p50))
(assert (distinct p13 p43))
(assert (distinct p18 p50))
(assert (distinct p46 p47))
(assert (distinct p11 p17))
(assert (distinct p22 p55))
(assert (distinct p5 p19))
(assert (distinct p27 p36))
(assert (distinct p30 p55))
(assert (distinct p34 p52))
(assert (distinct p23 p32))
(assert (distinct p13 p34))
(assert (distinct p18 p43))
(assert (distinct p43 p51))
(assert (distinct p11 p28))
(assert (distinct p1 p30))
(assert (distinct p15 p40))
(assert (distinct p2 p51))
(assert (distinct p5 p26))
(assert (distinct p27 p43))
(assert (distinct p34 p53))
(assert (distinct p6 p39))
(assert (distinct p10 p36))
(assert (distinct p31 p55))
(assert (distinct p35 p46))
(assert (distinct p18 p36))
(assert (distinct p14 p56))
(assert (distinct p1 p21))
(assert (distinct p15 p47))
(assert (distinct p2 p12))
(assert (distinct p27 p54))
(assert (distinct p47 p49))
(assert (distinct p3 p43))
(assert (distinct p23 p42))
(assert (distinct p6 p48))
(assert (distinct p10 p37))
(assert (distinct p18 p37))
(assert (distinct p38 p42))
(assert (distinct p14 p49))
(assert (distinct p15 p50))
(assert (distinct p2 p13))
(assert (distinct p5 p16))
(assert (distinct p3 p38))
(assert (distinct p23 p33))
(assert (distinct p6 p41))
(assert (distinct p10 p46))
(assert (distinct p31 p33))
(assert (distinct p18 p30))
(assert (distinct p11 p53))
(assert (distinct p14 p42))
(assert (distinct p19 p53))
(assert (distinct p39 p52))
(assert (distinct p12 p32))
(assert (distinct p20 p29))
(assert (distinct p6 p18))
(assert (distinct p28 p45))
(assert (distinct p31 p44))
(assert (distinct p35 p55))
(assert (distinct p24 p25))
(assert (distinct p7 p49))
(assert (distinct p14 p35))
(assert (distinct p19 p48))
(assert (distinct p39 p43))
(assert (distinct p12 p21))
(assert (distinct p2 p31))
(assert (distinct p16 p33))
(assert (distinct p20 p38))
(assert (distinct p3 p56))
(assert (distinct p23 p51))
(assert (distinct p6 p27))
(assert (distinct p28 p38))
(assert (distinct p35 p50))
(assert (distinct p7 p44))
(assert (distinct p11 p39))
(assert (distinct p32 p50))
(assert (distinct p36 p51))
(assert (distinct p19 p39))
(assert (distinct p39 p46))
(assert (distinct p44 p51))
(assert (distinct p9 p17))
(assert (distinct p2 p24))
(assert (distinct p16 p42))
(assert (distinct p20 p43))
(assert (distinct p3 p15))
(assert (distinct p23 p54))
(assert (distinct p48 p56))
(assert (distinct p4 p54))
(assert (distinct p24 p47))
(assert (distinct p7 p35))
(assert (distinct p11 p34))
(assert (distinct p19 p34))
(assert (distinct p9 p24))
(assert (distinct p16 p55))
(assert (distinct p20 p52))
(assert (distinct p3 p10))
(assert (distinct p25 p39))
(assert (distinct p6 p13))
(assert (distinct p28 p52))
(assert (distinct p24 p40))
(assert (distinct p7 p38))
(assert (distinct p11 p41))
(assert (distinct p32 p40))
(assert (distinct p19 p25))
(assert (distinct p41 p54))
(assert (distinct p9 p31))
(assert (distinct p15 p21))
(assert (distinct p40 p53))
(assert (distinct p27 p28))
(assert (distinct p13 p27))
(assert (distinct p25 p46))
(assert (distinct p21 p26))
(assert (distinct p4 p36))
(assert (distinct p7 p29))
(assert (distinct p29 p42))
(assert (distinct p33 p45))
(assert (distinct p32 p45))
(assert (distinct p36 p42))
(assert (distinct p19 p20))
(assert (distinct p8 p56))
(assert (distinct p12 p49))
(assert (distinct p15 p32))
(assert (distinct p40 p46))
(assert (distinct p13 p18))
(assert (distinct p3 p28))
(assert (distinct p25 p53))
(assert (distinct p1 p46))
(assert (distinct p21 p33))
(assert (distinct p4 p41))
(assert (distinct p24 p54))
(assert (distinct p7 p24))
(assert (distinct p29 p33))
(assert (distinct p33 p36))
(assert (distinct p36 p47))
(assert (distinct p8 p45))
(assert (distinct p12 p42))
(assert (distinct p37 p56))
(assert (distinct p40 p43))
(assert (distinct p45 p56))
(assert (distinct p10 p20))
(assert (distinct p49 p51))
(assert (distinct p3 p19))
(assert (distinct p1 p37))
(assert (distinct p21 p48))
(assert (distinct p4 p18))
(assert (distinct p24 p51))
(assert (distinct p7 p15))
(assert (distinct p41 p43))
(assert (distinct p5 p49))
(assert (distinct p9 p52))
(assert (distinct p8 p38))
(assert (distinct p12 p47))
(assert (distinct p17 p52))
(assert (distinct p45 p47))
(assert (distinct p10 p21))
(assert (distinct p21 p55))
(assert (distinct p4 p23))
(assert (distinct p26 p38))
(assert (distinct p29 p55))
(assert (distinct p33 p50))
(assert (distinct p8 p35))
(assert (distinct p12 p40))
(assert (distinct p17 p43))
(assert (distinct p37 p38))
(assert (distinct p42 p55))
(assert (distinct p10 p30))
(assert (distinct p16 p20))
(assert (distinct p14 p26))
(assert (distinct p1 p51))
(assert (distinct p4 p32))
(assert (distinct p26 p47))
(assert (distinct p22 p27))
(assert (distinct p5 p39))
(assert (distinct p9 p34))
(assert (distinct p8 p28))
(assert (distinct p30 p43))
(assert (distinct p34 p48))
(assert (distinct p17 p34))
(assert (distinct p37 p45))
(assert (distinct p13 p54))
(assert (distinct p16 p25))
(assert (distinct p14 p19))
(assert (distinct p1 p10))
(assert (distinct p26 p56))
(assert (distinct p2 p47))
(assert (distinct p22 p36))
(assert (distinct p5 p46))
(assert (distinct p9 p41))
(assert (distinct p8 p17))
(assert (distinct p30 p36))
(assert (distinct p17 p25))
(assert (distinct p37 p44))
(assert (distinct p13 p45))
(assert (distinct p38 p53))
(assert (distinct p46 p53))
(assert (distinct p11 p23))
(assert (distinct p4 p14))
(assert (distinct p2 p40))
(assert (distinct p22 p45))
(assert (distinct p5 p21))
(assert (distinct p9 p48))
(assert (distinct p8 p10))
(assert (distinct p17 p32))
(assert (distinct p6 p52))
(assert (distinct p10 p49))
(assert (distinct p13 p44))
(assert (distinct p18 p49))
(assert (distinct p11 p18))
(assert (distinct p22 p54))
(assert (distinct p5 p20))
(assert (distinct p27 p33))
(assert (distinct p30 p54))
(assert (distinct p34 p51))
(assert (distinct p23 p29))
(assert (distinct p13 p35))
(assert (distinct p18 p42))
(assert (distinct p38 p39))
(assert (distinct p43 p52))
(assert (distinct p11 p25))
(assert (distinct p1 p31))
(assert (distinct p15 p37))
(assert (distinct p2 p50))
(assert (distinct p5 p27))
(assert (distinct p27 p44))
(assert (distinct p6 p38))
(assert (distinct p10 p35))
(assert (distinct p31 p56))
(assert (distinct p35 p43))
(assert (distinct p18 p35))
(assert (distinct p38 p48))
(assert (distinct p14 p55))
(assert (distinct p1 p22))
(assert (distinct p15 p48))
(assert (distinct p2 p11))
(assert (distinct p27 p51))
(assert (distinct p47 p50))
(assert (distinct p3 p44))
(assert (distinct p23 p47))
(assert (distinct p6 p47))
(assert (distinct p10 p44))
(assert (distinct p18 p28))
(assert (distinct p38 p41))
(assert (distinct p14 p48))
(assert (distinct p12 p26))
(assert (distinct p15 p55))
(assert (distinct p2 p4))
(assert (distinct p5 p9))
(assert (distinct p3 p35))
(assert (distinct p23 p34))
(assert (distinct p6 p24))
(assert (distinct p10 p45))
(assert (distinct p31 p34))
(assert (distinct p18 p29))
(assert (distinct p11 p54))
(assert (distinct p14 p41))
(assert (distinct p19 p54))
(assert (distinct p39 p49))
(assert (distinct p12 p31))
(assert (distinct p20 p32))
(assert (distinct p6 p17))
(assert (distinct p28 p48))
(assert (distinct p31 p41))
(assert (distinct p35 p56))
(assert (distinct p24 p28))
(assert (distinct p7 p50))
(assert (distinct p14 p34))
(assert (distinct p19 p45))
(assert (distinct p39 p44))
(assert (distinct p12 p24))
(assert (distinct p2 p30))
(assert (distinct p16 p36))
(assert (distinct p20 p37))
(assert (distinct p3 p53))
(assert (distinct p23 p52))
(assert (distinct p6 p26))
(assert (distinct p28 p37))
(assert (distinct p7 p41))
(assert (distinct p11 p40))
(assert (distinct p32 p49))
(assert (distinct p36 p54))
(assert (distinct p19 p40))
(assert (distinct p44 p54))
(assert (distinct p9 p18))
(assert (distinct p2 p23))
(assert (distinct p16 p41))
(assert (distinct p20 p46))
(assert (distinct p3 p16))
(assert (distinct p25 p33))
(assert (distinct p48 p55))
(assert (distinct p4 p53))
(assert (distinct p24 p42))
(assert (distinct p7 p36))
(assert (distinct p11 p47))
(assert (distinct p19 p31))
(assert (distinct p9 p25))
(assert (distinct p15 p19))
(assert (distinct p13 p29))
(assert (distinct p16 p50))
(assert (distinct p20 p51))
(assert (distinct p25 p40))
(assert (distinct p6 p12))
(assert (distinct p28 p51))
(assert (distinct p24 p39))
(assert (distinct p7 p27))
(assert (distinct p11 p42))
(assert (distinct p32 p39))
(assert (distinct p19 p26))
(assert (distinct p41 p55))
(assert (distinct p9 p32))
(assert (distinct p15 p22))
(assert (distinct p40 p56))
(assert (distinct p13 p28))
(assert (distinct p25 p47))
(assert (distinct p21 p27))
(assert (distinct p4 p35))
(assert (distinct p7 p30))
(assert (distinct p29 p43))
(assert (distinct p33 p46))
(assert (distinct p32 p48))
(assert (distinct p36 p41))
(assert (distinct p8 p55))
(assert (distinct p12 p52))
(assert (distinct p15 p29))
(assert (distinct p40 p45))
(assert (distinct p13 p19))
(assert (distinct p3 p25))
(assert (distinct p25 p54))
(assert (distinct p1 p47))
(assert (distinct p21 p34))
(assert (distinct p4 p44))
(assert (distinct p24 p53))
(assert (distinct p7 p21))
(assert (distinct p29 p34))
(assert (distinct p8 p48))
(assert (distinct p12 p41))
(assert (distinct p37 p49))
(assert (distinct p45 p49))
(assert (distinct p10 p19))
(assert (distinct p49 p52))
(assert (distinct p3 p20))
(assert (distinct p1 p38))
(assert (distinct p21 p41))
(assert (distinct p4 p17))
(assert (distinct p26 p36))
(assert (distinct p7 p16))
(assert (distinct p41 p44))
(assert (distinct p5 p50))
(assert (distinct p9 p53))
(assert (distinct p8 p37))
(assert (distinct p12 p34))
(assert (distinct p17 p53))
(assert (distinct p10 p28))
(assert (distinct p16 p22))
(assert (distinct p14 p32))
(assert (distinct p21 p56))
(assert (distinct p4 p26))
(assert (distinct p26 p37))
(assert (distinct p29 p56))
(assert (distinct p33 p51))
(assert (distinct p8 p30))
(assert (distinct p12 p39))
(assert (distinct p17 p44))
(assert (distinct p37 p39))
(assert (distinct p42 p54))
(assert (distinct p10 p29))
(assert (distinct p16 p19))
(assert (distinct p14 p25))
(assert (distinct p1 p52))
(assert (distinct p4 p31))
(assert (distinct p26 p46))
(assert (distinct p22 p26))
(assert (distinct p5 p40))
(assert (distinct p9 p35))
(assert (distinct p8 p27))
(assert (distinct p30 p42))
(assert (distinct p34 p47))
(assert (distinct p17 p35))
(assert (distinct p37 p46))
(assert (distinct p13 p55))
(assert (distinct p16 p28))
(assert (distinct p14 p18))
(assert (distinct p1 p11))
(assert (distinct p26 p55))
(assert (distinct p2 p46))
(assert (distinct p22 p35))
(assert (distinct p5 p47))
(assert (distinct p9 p42))
(assert (distinct p8 p20))
(assert (distinct p30 p35))
(assert (distinct p17 p26))
(assert (distinct p13 p46))
(assert (distinct p38 p52))
(assert (distinct p46 p52))
(assert (distinct p11 p24))
(assert (distinct p1 p2))
(assert (distinct p4 p13))
(assert (distinct p2 p39))
(assert (distinct p22 p44))
(assert (distinct p5 p22))
(assert (distinct p27 p39))
(assert (distinct p8 p9))
(assert (distinct p23 p27))
(assert (distinct p6 p51))
(assert (distinct p10 p56))
(assert (distinct p13 p37))
(assert (distinct p18 p56))
(assert (distinct p11 p31))
(assert (distinct p1 p25))
(assert (distinct p15 p35))
(assert (distinct p22 p53))
(assert (distinct p5 p29))
(assert (distinct p27 p34))
(assert (distinct p30 p53))
(assert (distinct p34 p50))
(assert (distinct p23 p30))
(assert (distinct p13 p36))
(assert (distinct p18 p41))
(assert (distinct p43 p49))
(assert (distinct p11 p26))
(assert (distinct p1 p32))
(assert (distinct p15 p38))
(assert (distinct p2 p49))
(assert (distinct p5 p28))
(assert (distinct p27 p41))
(assert (distinct p6 p37))
(assert (distinct p10 p34))
(assert (distinct p31 p53))
(assert (distinct p35 p44))
(assert (distinct p18 p34))
(assert (distinct p38 p47))
(assert (distinct p14 p54))
(assert (distinct p1 p23))
(assert (distinct p15 p45))
(assert (distinct p2 p10))
(assert (distinct p27 p52))
(assert (distinct p47 p55))
(assert (distinct p3 p41))
(assert (distinct p23 p48))
(assert (distinct p6 p46))
(assert (distinct p10 p43))
(assert (distinct p18 p27))
(assert (distinct p11 p12))
(assert (distinct p14 p47))
(assert (distinct p26 p28))
(assert (distinct p12 p25))
(assert (distinct p15 p56))
(assert (distinct p2 p3))
(assert (distinct p5 p10))
(assert (distinct p20 p26))
(assert (distinct p3 p36))
(assert (distinct p23 p39))
(assert (distinct p6 p23))
(assert (distinct p28 p42))
(assert (distinct p31 p39))
(assert (distinct p18 p20))
(assert (distinct p24 p30))
(assert (distinct p11 p51))
(assert (distinct p14 p40))
(assert (distinct p19 p51))
(assert (distinct p39 p50))
(assert (distinct p12 p18))
(assert (distinct p2 p28))
(assert (distinct p16 p38))
(assert (distinct p20 p31))
(assert (distinct p6 p32))
(assert (distinct p28 p47))
(assert (distinct p31 p42))
(assert (distinct p35 p53))
(assert (distinct p24 p27))
(assert (distinct p7 p55))
(assert (distinct p14 p33))
(assert (distinct p19 p46))
(assert (distinct p39 p41))
(assert (distinct p12 p23))
(assert (distinct p2 p29))
(assert (distinct p16 p35))
(assert (distinct p20 p40))
(assert (distinct p3 p54))
(assert (distinct p23 p49))
(assert (distinct p6 p25))
(assert (distinct p28 p40))
(assert (distinct p7 p42))
(assert (distinct p11 p37))
(assert (distinct p32 p52))
(assert (distinct p36 p53))
(assert (distinct p19 p37))
(assert (distinct p44 p53))
(assert (distinct p9 p19))
(assert (distinct p2 p22))
(assert (distinct p16 p44))
(assert (distinct p20 p45))
(assert (distinct p3 p13))
(assert (distinct p25 p34))
(assert (distinct p48 p50))
(assert (distinct p21 p22))
(assert (distinct p4 p56))
(assert (distinct p24 p41))
(assert (distinct p7 p33))
(assert (distinct p11 p48))
(assert (distinct p19 p32))
(assert (distinct p41 p49))
(assert (distinct p9 p26))
(assert (distinct p15 p20))
(assert (distinct p13 p30))
(assert (distinct p16 p49))
(assert (distinct p20 p54))
(assert (distinct p25 p41))
(assert (distinct p6 p11))
(assert (distinct p28 p54))
(assert (distinct p21 p29))
(assert (distinct p24 p34))
(assert (distinct p7 p28))
(assert (distinct p29 p45))
(assert (distinct p32 p34))
(assert (distinct p41 p56))
(assert (distinct p15 p27))
(assert (distinct p40 p55))
(assert (distinct p13 p21))
(assert (distinct p3 p31))
(assert (distinct p25 p48))
(assert (distinct p1 p41))
(assert (distinct p21 p28))
(assert (distinct p4 p38))
(assert (distinct p7 p19))
(assert (distinct p29 p44))
(assert (distinct p33 p47))
(assert (distinct p32 p47))
(assert (distinct p36 p44))
(assert (distinct p8 p50))
(assert (distinct p12 p51))
(assert (distinct p15 p30))
(assert (distinct p40 p48))
(assert (distinct p13 p20))
(assert (distinct p3 p26))
(assert (distinct p25 p55))
(assert (distinct p1 p48))
(assert (distinct p21 p35))
(assert (distinct p4 p43))
(assert (distinct p24 p56))
(assert (distinct p7 p22))
(assert (distinct p29 p35))
(assert (distinct p8 p47))
(assert (distinct p12 p44))
(assert (distinct p37 p50))
(assert (distinct p45 p50))
(assert (distinct p10 p18))
(assert (distinct p3 p17))
(assert (distinct p1 p39))
(assert (distinct p21 p42))
(assert (distinct p4 p20))
(assert (distinct p26 p35))
(assert (distinct p7 p13))
(assert (distinct p22 p23))
(assert (distinct p5 p51))
(assert (distinct p9 p54))
(assert (distinct p8 p40))
(assert (distinct p12 p33))
(assert (distinct p17 p54))
(assert (distinct p42 p52))
(assert (distinct p10 p27))
(assert (distinct p16 p21))
(assert (distinct p14 p31))
(assert (distinct p21 p49))
(assert (distinct p4 p25))
(assert (distinct p26 p44))
(assert (distinct p29 p49))
(assert (distinct p33 p52))
(assert (distinct p22 p32))
(assert (distinct p8 p29))
(assert (distinct p30 p48))
(assert (distinct p17 p45))
(assert (distinct p42 p53))
(assert (distinct p16 p30))
(assert (distinct p14 p24))
(assert (distinct p1 p53))
(assert (distinct p26 p45))
(assert (distinct p2 p44))
(assert (distinct p22 p25))
(assert (distinct p5 p33))
(assert (distinct p9 p36))
(assert (distinct p8 p22))
(assert (distinct p30 p41))
(assert (distinct p34 p46))
(assert (distinct p17 p36))
(assert (distinct p37 p47))
(assert (distinct p13 p56))
(assert (distinct p16 p27))
(assert (distinct p14 p17))
(assert (distinct p1 p12))
(assert (distinct p26 p54))
(assert (distinct p2 p45))
(assert (distinct p22 p34))
(assert (distinct p5 p48))
(assert (distinct p9 p43))
(assert (distinct p8 p19))
(assert (distinct p30 p34))
(assert (distinct p17 p27))
(assert (distinct p13 p47))
(assert (distinct p38 p51))
(assert (distinct p25 p26))
(assert (distinct p46 p51))
(assert (distinct p11 p21))
(assert (distinct p1 p3))
(assert (distinct p4 p16))
(assert (distinct p29 p30))
(assert (distinct p2 p38))
(assert (distinct p22 p43))
(assert (distinct p5 p23))
(assert (distinct p27 p40))
(assert (distinct p8 p12))
(assert (distinct p17 p18))
(assert (distinct p23 p28))
(assert (distinct p6 p50))
(assert (distinct p10 p55))
(assert (distinct p13 p38))
(assert (distinct p18 p55))
(assert (distinct p43 p55))
(assert (distinct p11 p32))
(assert (distinct p1 p26))
(assert (distinct p15 p36))
(assert (distinct p22 p52))
(assert (distinct p5 p30))
(assert (distinct p27 p47))
(assert (distinct p30 p52))
(assert (distinct p34 p49))
(assert (distinct p31 p51))
(assert (distinct p18 p48))
(assert (distinct p43 p50))
(assert (distinct p1 p17))
(assert (distinct p15 p43))
(assert (distinct p2 p56))
(assert (distinct p27 p42))
(assert (distinct p3 p47))
(assert (distinct p6 p36))
(assert (distinct p10 p33))
(assert (distinct p31 p54))
(assert (distinct p35 p41))
(assert (distinct p18 p33))
(assert (distinct p38 p46))
(assert (distinct p14 p53))
(assert (distinct p1 p24))
(assert (distinct p15 p46))
(assert (distinct p2 p9))
(assert (distinct p27 p49))
(assert (distinct p47 p56))
(assert (distinct p3 p42))
(assert (distinct p23 p45))
(assert (distinct p6 p45))
(assert (distinct p10 p42))
(assert (distinct p35 p36))
(assert (distinct p18 p26))
(assert (distinct p14 p46))
(assert (distinct p26 p27))
(assert (distinct p12 p28))
(assert (distinct p15 p53))
(assert (distinct p5 p11))
(assert (distinct p30 p31))
(assert (distinct p20 p25))
(assert (distinct p3 p33))
(assert (distinct p23 p40))
(assert (distinct p6 p22))
(assert (distinct p28 p41))
(assert (distinct p31 p40))
(assert (distinct p18 p19))
(assert (distinct p24 p29))
(assert (distinct p11 p52))
(assert (distinct p14 p39))
(assert (distinct p19 p52))
(assert (distinct p39 p55))
(assert (distinct p12 p17))
(assert (distinct p2 p27))
(assert (distinct p16 p37))
(assert (distinct p20 p34))
(assert (distinct p6 p31))
(assert (distinct p28 p34))
(assert (distinct p31 p47))
(assert (distinct p35 p54))
(assert (distinct p7 p56))
(assert (distinct p32 p54))
(assert (distinct p19 p43))
(assert (distinct p39 p42))
(assert (distinct p2 p20))
(assert (distinct p16 p46))
(assert (distinct p20 p39))
(assert (distinct p3 p51))
(assert (distinct p23 p50))
(assert (distinct p28 p39))
(assert (distinct p4 p50))
(assert (distinct p7 p47))
(assert (distinct p11 p38))
(assert (distinct p32 p51))
(assert (distinct p36 p56))
(assert (distinct p19 p38))
(assert (distinct p44 p56))
(assert (distinct p9 p20))
(assert (distinct p2 p21))
(assert (distinct p16 p43))
(assert (distinct p20 p48))
(assert (distinct p3 p14))
(assert (distinct p25 p35))
(assert (distinct p48 p49))
(assert (distinct p21 p23))
(assert (distinct p4 p55))
(assert (distinct p24 p44))
(assert (distinct p7 p34))
(assert (distinct p11 p45))
(assert (distinct p19 p29))
(assert (distinct p41 p50))
(assert (distinct p9 p27))
(assert (distinct p15 p17))
(assert (distinct p13 p31))
(assert (distinct p16 p52))
(assert (distinct p20 p53))
(assert (distinct p25 p42))
(assert (distinct p6 p10))
(assert (distinct p28 p53))
(assert (distinct p21 p30))
(assert (distinct p24 p33))
(assert (distinct p7 p25))
(assert (distinct p29 p46))
(assert (distinct p33 p41))
(assert (distinct p32 p33))
(assert (distinct p15 p28))
(assert (distinct p40 p50))
(assert (distinct p13 p22))
(assert (distinct p3 p32))
(assert (distinct p25 p49))
(assert (distinct p1 p42))
(assert (distinct p21 p37))
(assert (distinct p4 p37))
(assert (distinct p7 p20))
(assert (distinct p29 p37))
(assert (distinct p33 p48))
(assert (distinct p32 p42))
(assert (distinct p36 p43))
(assert (distinct p8 p49))
(assert (distinct p12 p54))
(assert (distinct p40 p47))
(assert (distinct p3 p23))
(assert (distinct p25 p56))
(assert (distinct p1 p33))
(assert (distinct p21 p36))
(assert (distinct p4 p46))
(assert (distinct p24 p55))
(assert (distinct p7 p11))
(assert (distinct p29 p36))
(assert (distinct p5 p53))
(assert (distinct p8 p42))
(assert (distinct p12 p43))
(assert (distinct p37 p51))
(assert (distinct p45 p51))
(assert (distinct p10 p17))
(assert (distinct p3 p18))
(assert (distinct p1 p40))
(assert (distinct p21 p43))
(assert (distinct p4 p19))
(assert (distinct p26 p34))
(assert (distinct p7 p14))
(assert (distinct p5 p52))
(assert (distinct p9 p55))
(assert (distinct p8 p39))
(assert (distinct p12 p36))
(assert (distinct p17 p55))
(assert (distinct p42 p51))
(assert (distinct p10 p26))
(assert (distinct p16 p24))
(assert (distinct p14 p30))
(assert (distinct p21 p50))
(assert (distinct p4 p28))
(assert (distinct p26 p43))
(assert (distinct p29 p50))
(assert (distinct p33 p53))
(assert (distinct p22 p31))
(assert (distinct p8 p32))
(assert (distinct p30 p47))
(assert (distinct p34 p44))
(assert (distinct p17 p46))
(assert (distinct p16 p29))
(assert (distinct p14 p23))
(assert (distinct p1 p54))
(assert (distinct p26 p52))
(assert (distinct p2 p43))
(assert (distinct p22 p40))
(assert (distinct p5 p34))
(assert (distinct p9 p37))
(assert (distinct p8 p21))
(assert (distinct p30 p40))
(assert (distinct p34 p45))
(assert (distinct p17 p37))
(assert (distinct p37 p48))
(assert (distinct p10 p12))
(assert (distinct p13 p49))
(assert (distinct p1 p13))
(assert (distinct p4 p10))
(assert (distinct p26 p53))
(assert (distinct p2 p36))
(assert (distinct p22 p33))
(assert (distinct p5 p41))
(assert (distinct p9 p44))
(assert (distinct p8 p14))
(assert (distinct p30 p33))
(assert (distinct p17 p28))
(assert (distinct p6 p56))
(assert (distinct p13 p48))
(assert (distinct p38 p50))
(assert (distinct p25 p27))
(assert (distinct p46 p50))
(assert (distinct p11 p22))
(assert (distinct p1 p4))
(assert (distinct p4 p15))
(assert (distinct p29 p31))
(assert (distinct p2 p37))
(assert (distinct p22 p42))
(assert (distinct p5 p24))
(assert (distinct p27 p37))
(assert (distinct p8 p11))
(assert (distinct p17 p19))
(assert (distinct p23 p25))
(assert (distinct p6 p49))
(assert (distinct p10 p54))
(assert (distinct p13 p39))
(assert (distinct p18 p54))
(assert (distinct p43 p56))
(assert (distinct p11 p29))
(assert (distinct p1 p27))
(assert (distinct p15 p33))
(assert (distinct p22 p51))
(assert (distinct p5 p31))
(assert (distinct p27 p48))
(assert (distinct p30 p51))
(assert (distinct p34 p56))
(assert (distinct p31 p52))
(assert (distinct p35 p47))
(assert (distinct p18 p47))
(assert (distinct p1 p18))
(assert (distinct p15 p44))
(assert (distinct p2 p55))
(assert (distinct p5 p6))
(assert (distinct p27 p55))
(assert (distinct p3 p48))
(assert (distinct p23 p43))
(assert (distinct p6 p35))
(assert (distinct p10 p40))
(assert (distinct p35 p42))
(assert (distinct p18 p40))
(assert (distinct p38 p45))
(assert (distinct p14 p52))
(assert (distinct p15 p51))
(assert (distinct p2 p16))
(assert (distinct p5 p13))
(assert (distinct p27 p50))
(assert (distinct p47 p53))
(assert (distinct p3 p39))
(assert (distinct p23 p46))
(assert (distinct p6 p44))
(assert (distinct p10 p41))
(assert (distinct p18 p25))
(assert (distinct p14 p45))
(assert (distinct p12 p27))
(assert (distinct p51 p52))
(assert (distinct p15 p54))
(assert (distinct p5 p12))
(assert (distinct p20 p28))
(assert (distinct p3 p34))
(assert (distinct p23 p37))
(assert (distinct p6 p21))
(assert (distinct p28 p44))
(assert (distinct p31 p37))
(assert (distinct p43 p44))
(assert (distinct p24 p32))
(assert (distinct p11 p49))
(assert (distinct p14 p38))
(assert (distinct p19 p49))
(assert (distinct p39 p56))
(assert (distinct p12 p20))
(assert (distinct p2 p26))
(assert (distinct p16 p40))
(assert (distinct p20 p33))
(assert (distinct p6 p30))
(assert (distinct p28 p33))
(assert (distinct p31 p48))
(assert (distinct p35 p51))
(assert (distinct p7 p53))
(assert (distinct p32 p53))
(assert (distinct p36 p50))
(assert (distinct p19 p44))
(assert (distinct p39 p47))
(assert (distinct p44 p50))
(assert (distinct p2 p19))
(assert (distinct p16 p45))
(assert (distinct p20 p42))
(assert (distinct p3 p52))
(assert (distinct p23 p55))
(assert (distinct p6 p7))
(assert (distinct p4 p49))
(assert (distinct p24 p46))
(assert (distinct p7 p48))
(assert (distinct p11 p35))
(assert (distinct p36 p55))
(assert (distinct p19 p35))
(assert (distinct p44 p55))
(assert (distinct p9 p21))
(assert (distinct p16 p54))
(assert (distinct p20 p47))
(assert (distinct p3 p11))
(assert (distinct p25 p36))
(assert (distinct p6 p16))
(assert (distinct p48 p52))
(assert (distinct p24 p43))
(assert (distinct p7 p39))
(assert (distinct p11 p46))
(assert (distinct p19 p30))
(assert (distinct p41 p51))
(assert (distinct p9 p28))
(assert (distinct p15 p18))
(assert (distinct p13 p32))
(assert (distinct p16 p51))
(assert (distinct p20 p56))
(assert (distinct p25 p43))
(assert (distinct p6 p9))
(assert (distinct p28 p56))
(assert (distinct p53 p54))
(assert (distinct p21 p31))
(assert (distinct p24 p36))
(assert (distinct p7 p26))
(assert (distinct p29 p47))
(assert (distinct p33 p42))
(assert (distinct p32 p36))
(assert (distinct p15 p25))
(assert (distinct p40 p49))
(assert (distinct p13 p23))
(assert (distinct p3 p29))
(assert (distinct p25 p50))
(assert (distinct p1 p43))
(assert (distinct p21 p38))
(assert (distinct p4 p40))
(assert (distinct p7 p17))
(assert (distinct p29 p38))
(assert (distinct p32 p41))
(assert (distinct p36 p46))
(assert (distinct p9 p10))
(assert (distinct p8 p52))
(assert (distinct p12 p53))
(assert (distinct p37 p53))
(assert (distinct p40 p42))
(assert (distinct p45 p53))
(assert (distinct p13 p14))
(assert (distinct p3 p24))
(assert (distinct p1 p34))
(assert (distinct p21 p45))
(assert (distinct p4 p45))
(assert (distinct p24 p50))
(assert (distinct p7 p12))
(assert (distinct p5 p54))
(assert (distinct p9 p49))
(assert (distinct p8 p41))
(assert (distinct p12 p46))
(assert (distinct p17 p49))
(assert (distinct p37 p52))
(assert (distinct p45 p52))
(assert (distinct p10 p24))
(assert (distinct p21 p44))
(assert (distinct p4 p22))
(assert (distinct p26 p33))
(assert (distinct p9 p56))
(assert (distinct p8 p34))
(assert (distinct p12 p35))
(assert (distinct p17 p56))
(assert (distinct p42 p50))
(assert (distinct p10 p25))
(assert (distinct p16 p23))
(assert (distinct p14 p29))
(assert (distinct p21 p51))
(assert (distinct p4 p27))
(assert (distinct p26 p42))
(assert (distinct p29 p51))
(assert (distinct p33 p54))
(assert (distinct p54 p55))
(assert (distinct p22 p30))
(assert (distinct p8 p31))
(assert (distinct p30 p46))
(assert (distinct p34 p43))
(assert (distinct p17 p47))
(assert (distinct p16 p32))
(assert (distinct p14 p22))
(assert (distinct p1 p55))
(assert (distinct p26 p51))
(assert (distinct p2 p42))
(assert (distinct p22 p39))
(assert (distinct p5 p35))
(assert (distinct p9 p38))
(assert (distinct p8 p24))
(assert (distinct p30 p39))
(assert (distinct p34 p36))
(assert (distinct p17 p38))
(assert (distinct p37 p41))
(assert (distinct p10 p11))
(assert (distinct p13 p50))
(assert (distinct p38 p56))
(assert (distinct p46 p56))
(assert (distinct p14 p15))
(assert (distinct p1 p14))
(assert (distinct p4 p9))
(assert (distinct p2 p35))
(assert (distinct p22 p48))
(assert (distinct p5 p42))
(assert (distinct p9 p45))
(assert (distinct p8 p13))
(assert (distinct p17 p29))
(assert (distinct p6 p55))
(assert (distinct p10 p52))
(assert (distinct p13 p41))
(assert (distinct p18 p52))
(assert (distinct p38 p49))
(assert (distinct p25 p28))
(assert (distinct p46 p49))
(assert (distinct p11 p19))
(assert (distinct p22 p41))
(assert (distinct p5 p17))
(assert (distinct p27 p38))
(assert (distinct p17 p20))
(assert (distinct p23 p26))
(assert (distinct p10 p53))
(assert (distinct p13 p40))
(assert (distinct p18 p53))
(assert (distinct p43 p53))
(assert (distinct p11 p30))
(assert (distinct p1 p28))
(assert (distinct p15 p34))
(assert (distinct p22 p50))
(assert (distinct p5 p32))
(assert (distinct p27 p45))
(assert (distinct p30 p50))
(assert (distinct p34 p55))
(assert (distinct p31 p49))
(assert (distinct p35 p48))
(assert (distinct p18 p46))
(assert (distinct p1 p19))
(assert (distinct p15 p41))
(assert (distinct p2 p54))
(assert (distinct p5 p7))
(assert (distinct p27 p56))
(assert (distinct p47 p51))
(assert (distinct p3 p45))
(assert (distinct p23 p44))
(assert (distinct p6 p34))
(assert (distinct p10 p39))
(assert (distinct p18 p39))
(assert (distinct p38 p44))
(assert (distinct p14 p51))
(assert (distinct p15 p52))
(assert (distinct p2 p15))
(assert (distinct p5 p14))
(assert (distinct p47 p54))
(assert (distinct p3 p40))
(assert (distinct p23 p35))
(assert (distinct p6 p43))
(assert (distinct p10 p48))
(assert (distinct p31 p35))
(assert (distinct p18 p32))
(assert (distinct p11 p55))
(assert (distinct p14 p44))
(assert (distinct p19 p55))
(assert (distinct p12 p30))
(assert (distinct p20 p27))
(assert (distinct p23 p38))
(assert (distinct p6 p20))
(assert (distinct p28 p43))
(assert (distinct p31 p38))
(assert (distinct p24 p31))
(assert (distinct p7 p51))
(assert (distinct p11 p50))
(assert (distinct p14 p37))
(assert (distinct p19 p50))
(assert (distinct p39 p53))
(assert (distinct p12 p19))
(assert (distinct p2 p25))
(assert (distinct p16 p39))
(assert (distinct p20 p36))
(assert (distinct p6 p29))
(assert (distinct p28 p36))
(assert (distinct p31 p45))
(assert (distinct p35 p52))
(assert (distinct p7 p54))
(assert (distinct p32 p56))
(assert (distinct p36 p49))
(assert (distinct p19 p41))
(assert (distinct p39 p48))
(assert (distinct p44 p49))
(assert (distinct p2 p18))
(assert (distinct p16 p48))
(assert (distinct p20 p41))
(assert (distinct p3 p49))
(assert (distinct p23 p56))
(assert (distinct p48 p54))
(assert (distinct p4 p52))
(assert (distinct p24 p45))
(assert (distinct p7 p45))
(assert (distinct p11 p36))
(assert (distinct p19 p36))
(assert (distinct p9 p22))
(assert (distinct p16 p53))
(assert (distinct p20 p50))
(assert (distinct p3 p12))
(assert (distinct p25 p37))
(assert (distinct p6 p15))
(assert (distinct p28 p50))
(assert (distinct p48 p51))
(assert (distinct p24 p38))
(assert (distinct p7 p40))
(assert (distinct p11 p43))
(assert (distinct p32 p38))
(assert (distinct p19 p27))
(assert (distinct p41 p52))
(assert (distinct p9 p29))
(assert (distinct p15 p23))
(assert (distinct p13 p25))
(assert (distinct p20 p55))
(assert (distinct p25 p44))
(assert (distinct p28 p55))
(assert (distinct p53 p55))
(assert (distinct p21 p32))
(assert (distinct p4 p34))
(assert (distinct p24 p35))
(assert (distinct p7 p31))
(assert (distinct p29 p48))
(assert (distinct p33 p43))
(assert (distinct p32 p35))
(assert (distinct p8 p54))
(assert (distinct p15 p26))
(assert (distinct p40 p52))
(assert (distinct p13 p24))
(assert (distinct p3 p30))
(assert (distinct p25 p51))
(assert (distinct p1 p44))
(assert (distinct p21 p39))
(assert (distinct p4 p39))
(assert (distinct p7 p18))
(assert (distinct p29 p39))
(assert (distinct p33 p34))
(assert (distinct p32 p44))
(assert (distinct p36 p45))
(assert (distinct p9 p11))
(assert (distinct p8 p51))
(assert (distinct p12 p56))
(assert (distinct p37 p54))
(assert (distinct p40 p41))
(assert (distinct p45 p54))
(assert (distinct p13 p15))
(assert (distinct p3 p21))
(assert (distinct p1 p35))
(assert (distinct p21 p46))
(assert (distinct p4 p48))
(assert (distinct p24 p49))
(assert (distinct p7 p9))
(assert (distinct p5 p55))
(assert (distinct p9 p50))
(assert (distinct p8 p44))
(assert (distinct p12 p45))
(assert (distinct p17 p50))
(assert (distinct p10 p23))
(assert (distinct p21 p53))
(assert (distinct p4 p21))
(assert (distinct p26 p40))
(assert (distinct p29 p53))
(assert (distinct p8 p33))
(assert (distinct p12 p38))
(assert (distinct p17 p41))
(assert (distinct p42 p49))
(assert (distinct p10 p32))
(assert (distinct p16 p18))
(assert (distinct p14 p28))
(assert (distinct p1 p49))
(assert (distinct p21 p52))
(assert (distinct p4 p30))
(assert (distinct p26 p41))
(assert (distinct p29 p52))
(check-sat)
(exit)