prop aux1001 := [[[~ pc1_at_0] & [~ pc2_at_0]] & [y_aux_at_0 = 1]].
prop aux1002 := [[[d_at_0 >= 0] & [x_at_0 = (x_aux_at_0 + d_at_0)]] & [y_at_0 = (y_aux_at_0 + d_at_0)]].
prop aux1003 := [y_at_0 <= 10].
prop aux1004 := [[~ pc1_at_0] & [~ pc2_at_0]].
prop aux1005 := [pc1_at_0 & [~ pc2_at_0]].
prop aux1006 := [[~ pc1_at_0] & pc2_at_0].
prop aux1007 := [pc1_at_0 & pc2_at_0].
prop aux1008 := [[~ pc1_at_1] & [~ pc2_at_1]].
prop aux1009 := [pc1_at_1 & [~ pc2_at_1]].
prop aux1010 := [[~ pc1_at_1] & pc2_at_1].
prop aux1011 := [pc1_at_1 & pc2_at_1].
prop aux1012 := [[x_aux_at_1 = 0] & [y_aux_at_1 = y_at_0]].
prop aux1013 := [[x_aux_at_1 = x_at_0] & [y_aux_at_1 = y_at_0]].
prop aux1014 := [[[aux1004 & aux1009] & [y_at_0 = 10]] & aux1012].
prop aux1015 := [[[aux1005 & aux1010] & [x_at_0 = 2]] & aux1013].
prop aux1016 := [[[aux1006 & aux1011] & [y_at_0 = 5]] & aux1012].
prop aux1017 := [[[aux1007 & aux1008] & [x_at_0 = 2]] & aux1013].
prop aux1018 := [[[aux1014 | aux1015] | aux1016] | aux1017].
prop aux1019 := [[[d_at_1 >= 0] & [x_at_1 = (x_aux_at_1 + d_at_1)]] & [[[aux1008 | aux1009] & [y_at_1 = (y_aux_at_1 + d_at_1)]] | [[aux1010 | aux1011] & [y_at_1 = (y_aux_at_1 - (2 * d_at_1))]]]].
prop aux1020 := [aux1008 => [y_at_1 <= 10]].
prop aux1021 := [aux1009 => [x_at_1 <= 2]].
prop aux1022 := [aux1010 => [y_at_1 >= 5]].
prop aux1023 := [aux1011 => [x_at_1 <= 2]].
prop aux1024 := [[~ pc1_at_1] & [~ pc2_at_1]].
prop aux1025 := [pc1_at_1 & [~ pc2_at_1]].
prop aux1026 := [[~ pc1_at_1] & pc2_at_1].
prop aux1027 := [pc1_at_1 & pc2_at_1].
prop aux1028 := [[~ pc1_at_2] & [~ pc2_at_2]].
prop aux1029 := [pc1_at_2 & [~ pc2_at_2]].
prop aux1030 := [[~ pc1_at_2] & pc2_at_2].
prop aux1031 := [pc1_at_2 & pc2_at_2].
prop aux1032 := [[x_aux_at_2 = 0] & [y_aux_at_2 = y_at_1]].
prop aux1033 := [[x_aux_at_2 = x_at_1] & [y_aux_at_2 = y_at_1]].
prop aux1034 := [[[aux1024 & aux1029] & [y_at_1 = 10]] & aux1032].
prop aux1035 := [[[aux1025 & aux1030] & [x_at_1 = 2]] & aux1033].
prop aux1036 := [[[aux1026 & aux1031] & [y_at_1 = 5]] & aux1032].
prop aux1037 := [[[aux1027 & aux1028] & [x_at_1 = 2]] & aux1033].
prop aux1038 := [[[aux1034 | aux1035] | aux1036] | aux1037].
prop aux1039 := [[[d_at_2 >= 0] & [x_at_2 = (x_aux_at_2 + d_at_2)]] & [[[aux1028 | aux1029] & [y_at_2 = (y_aux_at_2 + d_at_2)]] | [[aux1030 | aux1031] & [y_at_2 = (y_aux_at_2 - (2 * d_at_2))]]]].
prop aux1040 := [aux1028 => [y_at_2 <= 10]].
prop aux1041 := [aux1029 => [x_at_2 <= 2]].
prop aux1042 := [aux1030 => [y_at_2 >= 5]].
prop aux1043 := [aux1031 => [x_at_2 <= 2]].
prop aux1044 := [[~ pc1_at_2] & [~ pc2_at_2]].
prop aux1045 := [pc1_at_2 & [~ pc2_at_2]].
prop aux1046 := [[~ pc1_at_2] & pc2_at_2].
prop aux1047 := [pc1_at_2 & pc2_at_2].
prop aux1048 := [[~ pc1_at_3] & [~ pc2_at_3]].
prop aux1049 := [pc1_at_3 & [~ pc2_at_3]].
prop aux1050 := [[~ pc1_at_3] & pc2_at_3].
prop aux1051 := [pc1_at_3 & pc2_at_3].
prop aux1052 := [[x_aux_at_3 = 0] & [y_aux_at_3 = y_at_2]].
prop aux1053 := [[x_aux_at_3 = x_at_2] & [y_aux_at_3 = y_at_2]].
prop aux1054 := [[[aux1044 & aux1049] & [y_at_2 = 10]] & aux1052].
prop aux1055 := [[[aux1045 & aux1050] & [x_at_2 = 2]] & aux1053].
prop aux1056 := [[[aux1046 & aux1051] & [y_at_2 = 5]] & aux1052].
prop aux1057 := [[[aux1047 & aux1048] & [x_at_2 = 2]] & aux1053].
prop aux1058 := [[[aux1054 | aux1055] | aux1056] | aux1057].
prop aux1059 := [[[d_at_3 >= 0] & [x_at_3 = (x_aux_at_3 + d_at_3)]] & [[[aux1048 | aux1049] & [y_at_3 = (y_aux_at_3 + d_at_3)]] | [[aux1050 | aux1051] & [y_at_3 = (y_aux_at_3 - (2 * d_at_3))]]]].
prop aux1060 := [aux1048 => [y_at_3 <= 10]].
prop aux1061 := [aux1049 => [x_at_3 <= 2]].
prop aux1062 := [aux1050 => [y_at_3 >= 5]].
prop aux1063 := [aux1051 => [x_at_3 <= 2]].
prop aux1064 := [[~ pc1_at_3] & [~ pc2_at_3]].
prop aux1065 := [pc1_at_3 & [~ pc2_at_3]].
prop aux1066 := [[~ pc1_at_3] & pc2_at_3].
prop aux1067 := [pc1_at_3 & pc2_at_3].
prop aux1068 := [[~ pc1_at_4] & [~ pc2_at_4]].
prop aux1069 := [pc1_at_4 & [~ pc2_at_4]].
prop aux1070 := [[~ pc1_at_4] & pc2_at_4].
prop aux1071 := [pc1_at_4 & pc2_at_4].
prop aux1072 := [[x_aux_at_4 = 0] & [y_aux_at_4 = y_at_3]].
prop aux1073 := [[x_aux_at_4 = x_at_3] & [y_aux_at_4 = y_at_3]].
prop aux1074 := [[[aux1064 & aux1069] & [y_at_3 = 10]] & aux1072].
prop aux1075 := [[[aux1065 & aux1070] & [x_at_3 = 2]] & aux1073].
prop aux1076 := [[[aux1066 & aux1071] & [y_at_3 = 5]] & aux1072].
prop aux1077 := [[[aux1067 & aux1068] & [x_at_3 = 2]] & aux1073].
prop aux1078 := [[[aux1074 | aux1075] | aux1076] | aux1077].
prop aux1079 := [[[d_at_4 >= 0] & [x_at_4 = (x_aux_at_4 + d_at_4)]] & [[[aux1068 | aux1069] & [y_at_4 = (y_aux_at_4 + d_at_4)]] | [[aux1070 | aux1071] & [y_at_4 = (y_aux_at_4 - (2 * d_at_4))]]]].
prop aux1080 := [aux1068 => [y_at_4 <= 10]].
prop aux1081 := [aux1069 => [x_at_4 <= 2]].
prop aux1082 := [aux1070 => [y_at_4 >= 5]].
prop aux1083 := [aux1071 => [x_at_4 <= 2]].
sat ~[
[[[[aux1001 & aux1002] & aux1003] & [[[[[[aux1018 & aux1019] & aux1020] & aux1021] & aux1022] & aux1023] & [[[[[aux1038 & aux1039] & aux1040] & aux1041] & aux1042] & aux1043] & [[[[[aux1058 & aux1059] & aux1060] & aux1061] & aux1062] & aux1063] & [[[[[aux1078 & aux1079] & aux1080] & aux1081] & aux1082] & aux1083]] & tt] => [[[y_at_0 >= 1] & [y_at_0 <= 12]] & [[y_at_1 >= 1] & [y_at_1 <= 12]] & [[y_at_2 >= 1] & [y_at_2 <= 12]] & [[y_at_3 >= 1] & [y_at_3 <= 12]] & [[y_at_4 >= 1] & [y_at_4 <= 12]]]]].