H(start,0)
--->E(performed(a1),Ta1).

H(performed(a1),Ta1)
--->E(performed(a2),Ta2)/\Ta2>Ta1
\/E(performed(a3),Ta3)/\Ta3>Ta1.

H(performed(a2),Ta2)
--->E(performed(a4),Ta4)/\Ta4>Ta2
\/E(performed(a5),Ta5)/\Ta5>Ta2.

H(performed(a3),Ta3)
--->E(performed(a6),Ta6)/\Ta6>Ta3
\/E(performed(a7),Ta7)/\Ta7>Ta3.

H(performed(a4),Ta4)
--->E(performed(a8),Ta8)/\Ta8>Ta4
\/E(performed(a9),Ta9)/\Ta9>Ta4.

H(performed(a5),Ta5)
--->E(performed(a10),Ta10)/\Ta10>Ta5
\/E(performed(a11),Ta11)/\Ta11>Ta5.

H(performed(a6),Ta6)
--->E(performed(a12),Ta12)/\Ta12>Ta6
\/E(performed(a13),Ta13)/\Ta13>Ta6.

H(performed(a7),Ta7)
--->E(performed(a14),Ta14)/\Ta14>Ta7
\/E(performed(a15),Ta15)/\Ta15>Ta7.

H(performed(a8),Ta8)
--->E(performed(a16),Ta16)/\Ta16>Ta8
\/E(performed(a17),Ta17)/\Ta17>Ta8.

H(performed(a9),Ta9)
--->E(performed(a18),Ta18)/\Ta18>Ta9
\/E(performed(a19),Ta19)/\Ta19>Ta9.

H(performed(a10),Ta10)
--->E(performed(a20),Ta20)/\Ta20>Ta10
\/E(performed(a21),Ta21)/\Ta21>Ta10.

H(performed(a11),Ta11)
--->E(performed(a22),Ta22)/\Ta22>Ta11
\/E(performed(a23),Ta23)/\Ta23>Ta11.

H(performed(a12),Ta12)
--->E(performed(a24),Ta24)/\Ta24>Ta12
\/E(performed(a25),Ta25)/\Ta25>Ta12.

H(performed(a13),Ta13)
--->E(performed(a26),Ta26)/\Ta26>Ta13
\/E(performed(a27),Ta27)/\Ta27>Ta13.

H(performed(a14),Ta14)
--->E(performed(a28),Ta28)/\Ta28>Ta14
\/E(performed(a29),Ta29)/\Ta29>Ta14.

H(performed(a15),Ta15)
--->E(performed(a30),Ta30)/\Ta30>Ta15
\/E(performed(a31),Ta31)/\Ta31>Ta15.

H(performed(a16),Ta16)
--->E(performed(a32),Ta32)/\Ta32>Ta16
\/E(performed(a33),Ta33)/\Ta33>Ta16.

H(performed(a17),Ta17)
--->E(performed(a34),Ta34)/\Ta34>Ta17
\/E(performed(a35),Ta35)/\Ta35>Ta17.

H(performed(a18),Ta18)
--->E(performed(a36),Ta36)/\Ta36>Ta18
\/E(performed(a37),Ta37)/\Ta37>Ta18.

H(performed(a19),Ta19)
--->E(performed(a38),Ta38)/\Ta38>Ta19
\/E(performed(a39),Ta39)/\Ta39>Ta19.

H(performed(a20),Ta20)
--->E(performed(a40),Ta40)/\Ta40>Ta20
\/E(performed(a41),Ta41)/\Ta41>Ta20.

H(performed(a21),Ta21)
--->E(performed(a42),Ta42)/\Ta42>Ta21
\/E(performed(a43),Ta43)/\Ta43>Ta21.

H(performed(a22),Ta22)
--->E(performed(a44),Ta44)/\Ta44>Ta22
\/E(performed(a45),Ta45)/\Ta45>Ta22.

H(performed(a23),Ta23)
--->E(performed(a46),Ta46)/\Ta46>Ta23
\/E(performed(a47),Ta47)/\Ta47>Ta23.

H(performed(a24),Ta24)
--->E(performed(a48),Ta48)/\Ta48>Ta24
\/E(performed(a49),Ta49)/\Ta49>Ta24.

H(performed(a25),Ta25)
--->E(performed(a50),Ta50)/\Ta50>Ta25
\/E(performed(a51),Ta51)/\Ta51>Ta25.

H(performed(a26),Ta26)
--->E(performed(a52),Ta52)/\Ta52>Ta26
\/E(performed(a53),Ta53)/\Ta53>Ta26.

H(performed(a27),Ta27)
--->E(performed(a54),Ta54)/\Ta54>Ta27
\/E(performed(a55),Ta55)/\Ta55>Ta27.

H(performed(a28),Ta28)
--->E(performed(a56),Ta56)/\Ta56>Ta28
\/E(performed(a57),Ta57)/\Ta57>Ta28.

H(performed(a29),Ta29)
--->E(performed(a58),Ta58)/\Ta58>Ta29
\/E(performed(a59),Ta59)/\Ta59>Ta29.

H(performed(a30),Ta30)
--->E(performed(a60),Ta60)/\Ta60>Ta30
\/E(performed(a61),Ta61)/\Ta61>Ta30.

H(performed(a31),Ta31)
--->E(performed(a62),Ta62)/\Ta62>Ta31
\/E(performed(a63),Ta63)/\Ta63>Ta31.

H(performed(a32),Ta32)
--->E(performed(a64),Ta64)/\Ta64>Ta32
\/E(performed(a65),Ta65)/\Ta65>Ta32.

H(performed(a33),Ta33)
--->E(performed(a66),Ta66)/\Ta66>Ta33
\/E(performed(a67),Ta67)/\Ta67>Ta33.

H(performed(a34),Ta34)
--->E(performed(a68),Ta68)/\Ta68>Ta34
\/E(performed(a69),Ta69)/\Ta69>Ta34.

H(performed(a35),Ta35)
--->E(performed(a70),Ta70)/\Ta70>Ta35
\/E(performed(a71),Ta71)/\Ta71>Ta35.

H(performed(a36),Ta36)
--->E(performed(a72),Ta72)/\Ta72>Ta36
\/E(performed(a73),Ta73)/\Ta73>Ta36.

H(performed(a37),Ta37)
--->E(performed(a74),Ta74)/\Ta74>Ta37
\/E(performed(a75),Ta75)/\Ta75>Ta37.

H(performed(a38),Ta38)
--->E(performed(a76),Ta76)/\Ta76>Ta38
\/E(performed(a77),Ta77)/\Ta77>Ta38.

H(performed(a39),Ta39)
--->E(performed(a78),Ta78)/\Ta78>Ta39
\/E(performed(a79),Ta79)/\Ta79>Ta39.

H(performed(a40),Ta40)
--->E(performed(a80),Ta80)/\Ta80>Ta40
\/E(performed(a81),Ta81)/\Ta81>Ta40.

H(performed(a41),Ta41)
--->E(performed(a82),Ta82)/\Ta82>Ta41
\/E(performed(a83),Ta83)/\Ta83>Ta41.

H(performed(a42),Ta42)
--->E(performed(a84),Ta84)/\Ta84>Ta42
\/E(performed(a85),Ta85)/\Ta85>Ta42.

H(performed(a43),Ta43)
--->E(performed(a86),Ta86)/\Ta86>Ta43
\/E(performed(a87),Ta87)/\Ta87>Ta43.

H(performed(a44),Ta44)
--->E(performed(a88),Ta88)/\Ta88>Ta44
\/E(performed(a89),Ta89)/\Ta89>Ta44.

H(performed(a45),Ta45)
--->E(performed(a90),Ta90)/\Ta90>Ta45
\/E(performed(a91),Ta91)/\Ta91>Ta45.

H(performed(a46),Ta46)
--->E(performed(a92),Ta92)/\Ta92>Ta46
\/E(performed(a93),Ta93)/\Ta93>Ta46.

H(performed(a47),Ta47)
--->E(performed(a94),Ta94)/\Ta94>Ta47
\/E(performed(a95),Ta95)/\Ta95>Ta47.

H(performed(a48),Ta48)
--->E(performed(a96),Ta96)/\Ta96>Ta48
\/E(performed(a97),Ta97)/\Ta97>Ta48.

H(performed(a49),Ta49)
--->E(performed(a98),Ta98)/\Ta98>Ta49
\/E(performed(a99),Ta99)/\Ta99>Ta49.

H(performed(a50),Ta50)
--->E(performed(a100),Ta100)/\Ta100>Ta50
\/E(performed(a101),Ta101)/\Ta101>Ta50.

H(performed(a51),Ta51)
--->E(performed(a102),Ta102)/\Ta102>Ta51
\/E(performed(a103),Ta103)/\Ta103>Ta51.

H(performed(a52),Ta52)
--->E(performed(a104),Ta104)/\Ta104>Ta52
\/E(performed(a105),Ta105)/\Ta105>Ta52.

H(performed(a53),Ta53)
--->E(performed(a106),Ta106)/\Ta106>Ta53
\/E(performed(a107),Ta107)/\Ta107>Ta53.

H(performed(a54),Ta54)
--->E(performed(a108),Ta108)/\Ta108>Ta54
\/E(performed(a109),Ta109)/\Ta109>Ta54.

H(performed(a55),Ta55)
--->E(performed(a110),Ta110)/\Ta110>Ta55
\/E(performed(a111),Ta111)/\Ta111>Ta55.

H(performed(a56),Ta56)
--->E(performed(a112),Ta112)/\Ta112>Ta56
\/E(performed(a113),Ta113)/\Ta113>Ta56.

H(performed(a57),Ta57)
--->E(performed(a114),Ta114)/\Ta114>Ta57
\/E(performed(a115),Ta115)/\Ta115>Ta57.

H(performed(a58),Ta58)
--->E(performed(a116),Ta116)/\Ta116>Ta58
\/E(performed(a117),Ta117)/\Ta117>Ta58.

H(performed(a59),Ta59)
--->E(performed(a118),Ta118)/\Ta118>Ta59
\/E(performed(a119),Ta119)/\Ta119>Ta59.

H(performed(a60),Ta60)
--->E(performed(a120),Ta120)/\Ta120>Ta60
\/E(performed(a121),Ta121)/\Ta121>Ta60.

H(performed(a61),Ta61)
--->E(performed(a122),Ta122)/\Ta122>Ta61
\/E(performed(a123),Ta123)/\Ta123>Ta61.

H(performed(a62),Ta62)
--->E(performed(a124),Ta124)/\Ta124>Ta62
\/E(performed(a125),Ta125)/\Ta125>Ta62.

H(performed(a63),Ta63)
--->E(performed(a126),Ta126)/\Ta126>Ta63
\/E(performed(a127),Ta127)/\Ta127>Ta63.

H(performed(a64),Ta64)
--->EN(performed(a1),Ta1)/\Ta1<Ta64.

H(performed(a65),Ta65)
--->EN(performed(a1),Ta1)/\Ta1<Ta65.

H(performed(a66),Ta66)
--->EN(performed(a1),Ta1)/\Ta1<Ta66.

H(performed(a67),Ta67)
--->EN(performed(a1),Ta1)/\Ta1<Ta67.

H(performed(a68),Ta68)
--->EN(performed(a1),Ta1)/\Ta1<Ta68.

H(performed(a69),Ta69)
--->EN(performed(a1),Ta1)/\Ta1<Ta69.

H(performed(a70),Ta70)
--->EN(performed(a1),Ta1)/\Ta1<Ta70.

H(performed(a71),Ta71)
--->EN(performed(a1),Ta1)/\Ta1<Ta71.

H(performed(a72),Ta72)
--->EN(performed(a1),Ta1)/\Ta1<Ta72.

H(performed(a73),Ta73)
--->EN(performed(a1),Ta1)/\Ta1<Ta73.

H(performed(a74),Ta74)
--->EN(performed(a1),Ta1)/\Ta1<Ta74.

H(performed(a75),Ta75)
--->EN(performed(a1),Ta1)/\Ta1<Ta75.

H(performed(a76),Ta76)
--->EN(performed(a1),Ta1)/\Ta1<Ta76.

H(performed(a77),Ta77)
--->EN(performed(a1),Ta1)/\Ta1<Ta77.

H(performed(a78),Ta78)
--->EN(performed(a1),Ta1)/\Ta1<Ta78.

H(performed(a79),Ta79)
--->EN(performed(a1),Ta1)/\Ta1<Ta79.

H(performed(a80),Ta80)
--->EN(performed(a1),Ta1)/\Ta1<Ta80.

H(performed(a81),Ta81)
--->EN(performed(a1),Ta1)/\Ta1<Ta81.

H(performed(a82),Ta82)
--->EN(performed(a1),Ta1)/\Ta1<Ta82.

H(performed(a83),Ta83)
--->EN(performed(a1),Ta1)/\Ta1<Ta83.

H(performed(a84),Ta84)
--->EN(performed(a1),Ta1)/\Ta1<Ta84.

H(performed(a85),Ta85)
--->EN(performed(a1),Ta1)/\Ta1<Ta85.

H(performed(a86),Ta86)
--->EN(performed(a1),Ta1)/\Ta1<Ta86.

H(performed(a87),Ta87)
--->EN(performed(a1),Ta1)/\Ta1<Ta87.

H(performed(a88),Ta88)
--->EN(performed(a1),Ta1)/\Ta1<Ta88.

H(performed(a89),Ta89)
--->EN(performed(a1),Ta1)/\Ta1<Ta89.

H(performed(a90),Ta90)
--->EN(performed(a1),Ta1)/\Ta1<Ta90.

H(performed(a91),Ta91)
--->EN(performed(a1),Ta1)/\Ta1<Ta91.

H(performed(a92),Ta92)
--->EN(performed(a1),Ta1)/\Ta1<Ta92.

H(performed(a93),Ta93)
--->EN(performed(a1),Ta1)/\Ta1<Ta93.

H(performed(a94),Ta94)
--->EN(performed(a1),Ta1)/\Ta1<Ta94.

H(performed(a95),Ta95)
--->EN(performed(a1),Ta1)/\Ta1<Ta95.

H(performed(a96),Ta96)
--->EN(performed(a1),Ta1)/\Ta1<Ta96.

H(performed(a97),Ta97)
--->EN(performed(a1),Ta1)/\Ta1<Ta97.

H(performed(a98),Ta98)
--->EN(performed(a1),Ta1)/\Ta1<Ta98.

H(performed(a99),Ta99)
--->EN(performed(a1),Ta1)/\Ta1<Ta99.

H(performed(a100),Ta100)
--->EN(performed(a1),Ta1)/\Ta1<Ta100.

H(performed(a101),Ta101)
--->EN(performed(a1),Ta1)/\Ta1<Ta101.

H(performed(a102),Ta102)
--->EN(performed(a1),Ta1)/\Ta1<Ta102.

H(performed(a103),Ta103)
--->EN(performed(a1),Ta1)/\Ta1<Ta103.

H(performed(a104),Ta104)
--->EN(performed(a1),Ta1)/\Ta1<Ta104.

H(performed(a105),Ta105)
--->EN(performed(a1),Ta1)/\Ta1<Ta105.

H(performed(a106),Ta106)
--->EN(performed(a1),Ta1)/\Ta1<Ta106.

H(performed(a107),Ta107)
--->EN(performed(a1),Ta1)/\Ta1<Ta107.

H(performed(a108),Ta108)
--->EN(performed(a1),Ta1)/\Ta1<Ta108.

H(performed(a109),Ta109)
--->EN(performed(a1),Ta1)/\Ta1<Ta109.

H(performed(a110),Ta110)
--->EN(performed(a1),Ta1)/\Ta1<Ta110.

H(performed(a111),Ta111)
--->EN(performed(a1),Ta1)/\Ta1<Ta111.

H(performed(a112),Ta112)
--->EN(performed(a1),Ta1)/\Ta1<Ta112.

H(performed(a113),Ta113)
--->EN(performed(a1),Ta1)/\Ta1<Ta113.

H(performed(a114),Ta114)
--->EN(performed(a1),Ta1)/\Ta1<Ta114.

H(performed(a115),Ta115)
--->EN(performed(a1),Ta1)/\Ta1<Ta115.

H(performed(a116),Ta116)
--->EN(performed(a1),Ta1)/\Ta1<Ta116.

H(performed(a117),Ta117)
--->EN(performed(a1),Ta1)/\Ta1<Ta117.

H(performed(a118),Ta118)
--->EN(performed(a1),Ta1)/\Ta1<Ta118.

H(performed(a119),Ta119)
--->EN(performed(a1),Ta1)/\Ta1<Ta119.

H(performed(a120),Ta120)
--->EN(performed(a1),Ta1)/\Ta1<Ta120.

H(performed(a121),Ta121)
--->EN(performed(a1),Ta1)/\Ta1<Ta121.

H(performed(a122),Ta122)
--->EN(performed(a1),Ta1)/\Ta1<Ta122.

H(performed(a123),Ta123)
--->EN(performed(a1),Ta1)/\Ta1<Ta123.

H(performed(a124),Ta124)
--->EN(performed(a1),Ta1)/\Ta1<Ta124.

H(performed(a125),Ta125)
--->EN(performed(a1),Ta1)/\Ta1<Ta125.

H(performed(a126),Ta126)
--->EN(performed(a1),Ta1)/\Ta1<Ta126.

H(performed(a127),Ta127)
--->EN(performed(a1),Ta1)/\Ta1<Ta127.

