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]].
prop aux1084 := [[~ pc1_at_4] & [~ pc2_at_4]].
prop aux1085 := [pc1_at_4 & [~ pc2_at_4]].
prop aux1086 := [[~ pc1_at_4] & pc2_at_4].
prop aux1087 := [pc1_at_4 & pc2_at_4].
prop aux1088 := [[~ pc1_at_5] & [~ pc2_at_5]].
prop aux1089 := [pc1_at_5 & [~ pc2_at_5]].
prop aux1090 := [[~ pc1_at_5] & pc2_at_5].
prop aux1091 := [pc1_at_5 & pc2_at_5].
prop aux1092 := [[x_aux_at_5 = 0] & [y_aux_at_5 = y_at_4]].
prop aux1093 := [[x_aux_at_5 = x_at_4] & [y_aux_at_5 = y_at_4]].
prop aux1094 := [[[aux1084 & aux1089] & [y_at_4 = 10]] & aux1092].
prop aux1095 := [[[aux1085 & aux1090] & [x_at_4 = 2]] & aux1093].
prop aux1096 := [[[aux1086 & aux1091] & [y_at_4 = 5]] & aux1092].
prop aux1097 := [[[aux1087 & aux1088] & [x_at_4 = 2]] & aux1093].
prop aux1098 := [[[aux1094 | aux1095] | aux1096] | aux1097].
prop aux1099 := [[[d_at_5 >= 0] & [x_at_5 = (x_aux_at_5 + d_at_5)]] & [[[aux1088 | aux1089] & [y_at_5 = (y_aux_at_5 + d_at_5)]] | [[aux1090 | aux1091] & [y_at_5 = (y_aux_at_5 - (2 * d_at_5))]]]].
prop aux1100 := [aux1088 => [y_at_5 <= 10]].
prop aux1101 := [aux1089 => [x_at_5 <= 2]].
prop aux1102 := [aux1090 => [y_at_5 >= 5]].
prop aux1103 := [aux1091 => [x_at_5 <= 2]].
prop aux1104 := [[~ pc1_at_5] & [~ pc2_at_5]].
prop aux1105 := [pc1_at_5 & [~ pc2_at_5]].
prop aux1106 := [[~ pc1_at_5] & pc2_at_5].
prop aux1107 := [pc1_at_5 & pc2_at_5].
prop aux1108 := [[~ pc1_at_6] & [~ pc2_at_6]].
prop aux1109 := [pc1_at_6 & [~ pc2_at_6]].
prop aux1110 := [[~ pc1_at_6] & pc2_at_6].
prop aux1111 := [pc1_at_6 & pc2_at_6].
prop aux1112 := [[x_aux_at_6 = 0] & [y_aux_at_6 = y_at_5]].
prop aux1113 := [[x_aux_at_6 = x_at_5] & [y_aux_at_6 = y_at_5]].
prop aux1114 := [[[aux1104 & aux1109] & [y_at_5 = 10]] & aux1112].
prop aux1115 := [[[aux1105 & aux1110] & [x_at_5 = 2]] & aux1113].
prop aux1116 := [[[aux1106 & aux1111] & [y_at_5 = 5]] & aux1112].
prop aux1117 := [[[aux1107 & aux1108] & [x_at_5 = 2]] & aux1113].
prop aux1118 := [[[aux1114 | aux1115] | aux1116] | aux1117].
prop aux1119 := [[[d_at_6 >= 0] & [x_at_6 = (x_aux_at_6 + d_at_6)]] & [[[aux1108 | aux1109] & [y_at_6 = (y_aux_at_6 + d_at_6)]] | [[aux1110 | aux1111] & [y_at_6 = (y_aux_at_6 - (2 * d_at_6))]]]].
prop aux1120 := [aux1108 => [y_at_6 <= 10]].
prop aux1121 := [aux1109 => [x_at_6 <= 2]].
prop aux1122 := [aux1110 => [y_at_6 >= 5]].
prop aux1123 := [aux1111 => [x_at_6 <= 2]].
prop aux1124 := [[~ pc1_at_6] & [~ pc2_at_6]].
prop aux1125 := [pc1_at_6 & [~ pc2_at_6]].
prop aux1126 := [[~ pc1_at_6] & pc2_at_6].
prop aux1127 := [pc1_at_6 & pc2_at_6].
prop aux1128 := [[~ pc1_at_7] & [~ pc2_at_7]].
prop aux1129 := [pc1_at_7 & [~ pc2_at_7]].
prop aux1130 := [[~ pc1_at_7] & pc2_at_7].
prop aux1131 := [pc1_at_7 & pc2_at_7].
prop aux1132 := [[x_aux_at_7 = 0] & [y_aux_at_7 = y_at_6]].
prop aux1133 := [[x_aux_at_7 = x_at_6] & [y_aux_at_7 = y_at_6]].
prop aux1134 := [[[aux1124 & aux1129] & [y_at_6 = 10]] & aux1132].
prop aux1135 := [[[aux1125 & aux1130] & [x_at_6 = 2]] & aux1133].
prop aux1136 := [[[aux1126 & aux1131] & [y_at_6 = 5]] & aux1132].
prop aux1137 := [[[aux1127 & aux1128] & [x_at_6 = 2]] & aux1133].
prop aux1138 := [[[aux1134 | aux1135] | aux1136] | aux1137].
prop aux1139 := [[[d_at_7 >= 0] & [x_at_7 = (x_aux_at_7 + d_at_7)]] & [[[aux1128 | aux1129] & [y_at_7 = (y_aux_at_7 + d_at_7)]] | [[aux1130 | aux1131] & [y_at_7 = (y_aux_at_7 - (2 * d_at_7))]]]].
prop aux1140 := [aux1128 => [y_at_7 <= 10]].
prop aux1141 := [aux1129 => [x_at_7 <= 2]].
prop aux1142 := [aux1130 => [y_at_7 >= 5]].
prop aux1143 := [aux1131 => [x_at_7 <= 2]].
prop aux1144 := [[~ pc1_at_7] & [~ pc2_at_7]].
prop aux1145 := [pc1_at_7 & [~ pc2_at_7]].
prop aux1146 := [[~ pc1_at_7] & pc2_at_7].
prop aux1147 := [pc1_at_7 & pc2_at_7].
prop aux1148 := [[~ pc1_at_8] & [~ pc2_at_8]].
prop aux1149 := [pc1_at_8 & [~ pc2_at_8]].
prop aux1150 := [[~ pc1_at_8] & pc2_at_8].
prop aux1151 := [pc1_at_8 & pc2_at_8].
prop aux1152 := [[x_aux_at_8 = 0] & [y_aux_at_8 = y_at_7]].
prop aux1153 := [[x_aux_at_8 = x_at_7] & [y_aux_at_8 = y_at_7]].
prop aux1154 := [[[aux1144 & aux1149] & [y_at_7 = 10]] & aux1152].
prop aux1155 := [[[aux1145 & aux1150] & [x_at_7 = 2]] & aux1153].
prop aux1156 := [[[aux1146 & aux1151] & [y_at_7 = 5]] & aux1152].
prop aux1157 := [[[aux1147 & aux1148] & [x_at_7 = 2]] & aux1153].
prop aux1158 := [[[aux1154 | aux1155] | aux1156] | aux1157].
prop aux1159 := [[[d_at_8 >= 0] & [x_at_8 = (x_aux_at_8 + d_at_8)]] & [[[aux1148 | aux1149] & [y_at_8 = (y_aux_at_8 + d_at_8)]] | [[aux1150 | aux1151] & [y_at_8 = (y_aux_at_8 - (2 * d_at_8))]]]].
prop aux1160 := [aux1148 => [y_at_8 <= 10]].
prop aux1161 := [aux1149 => [x_at_8 <= 2]].
prop aux1162 := [aux1150 => [y_at_8 >= 5]].
prop aux1163 := [aux1151 => [x_at_8 <= 2]].
prop aux1164 := [[~ pc1_at_8] & [~ pc2_at_8]].
prop aux1165 := [pc1_at_8 & [~ pc2_at_8]].
prop aux1166 := [[~ pc1_at_8] & pc2_at_8].
prop aux1167 := [pc1_at_8 & pc2_at_8].
prop aux1168 := [[~ pc1_at_9] & [~ pc2_at_9]].
prop aux1169 := [pc1_at_9 & [~ pc2_at_9]].
prop aux1170 := [[~ pc1_at_9] & pc2_at_9].
prop aux1171 := [pc1_at_9 & pc2_at_9].
prop aux1172 := [[x_aux_at_9 = 0] & [y_aux_at_9 = y_at_8]].
prop aux1173 := [[x_aux_at_9 = x_at_8] & [y_aux_at_9 = y_at_8]].
prop aux1174 := [[[aux1164 & aux1169] & [y_at_8 = 10]] & aux1172].
prop aux1175 := [[[aux1165 & aux1170] & [x_at_8 = 2]] & aux1173].
prop aux1176 := [[[aux1166 & aux1171] & [y_at_8 = 5]] & aux1172].
prop aux1177 := [[[aux1167 & aux1168] & [x_at_8 = 2]] & aux1173].
prop aux1178 := [[[aux1174 | aux1175] | aux1176] | aux1177].
prop aux1179 := [[[d_at_9 >= 0] & [x_at_9 = (x_aux_at_9 + d_at_9)]] & [[[aux1168 | aux1169] & [y_at_9 = (y_aux_at_9 + d_at_9)]] | [[aux1170 | aux1171] & [y_at_9 = (y_aux_at_9 - (2 * d_at_9))]]]].
prop aux1180 := [aux1168 => [y_at_9 <= 10]].
prop aux1181 := [aux1169 => [x_at_9 <= 2]].
prop aux1182 := [aux1170 => [y_at_9 >= 5]].
prop aux1183 := [aux1171 => [x_at_9 <= 2]].
prop aux1184 := [[~ pc1_at_9] & [~ pc2_at_9]].
prop aux1185 := [pc1_at_9 & [~ pc2_at_9]].
prop aux1186 := [[~ pc1_at_9] & pc2_at_9].
prop aux1187 := [pc1_at_9 & pc2_at_9].
prop aux1188 := [[~ pc1_at_10] & [~ pc2_at_10]].
prop aux1189 := [pc1_at_10 & [~ pc2_at_10]].
prop aux1190 := [[~ pc1_at_10] & pc2_at_10].
prop aux1191 := [pc1_at_10 & pc2_at_10].
prop aux1192 := [[x_aux_at_10 = 0] & [y_aux_at_10 = y_at_9]].
prop aux1193 := [[x_aux_at_10 = x_at_9] & [y_aux_at_10 = y_at_9]].
prop aux1194 := [[[aux1184 & aux1189] & [y_at_9 = 10]] & aux1192].
prop aux1195 := [[[aux1185 & aux1190] & [x_at_9 = 2]] & aux1193].
prop aux1196 := [[[aux1186 & aux1191] & [y_at_9 = 5]] & aux1192].
prop aux1197 := [[[aux1187 & aux1188] & [x_at_9 = 2]] & aux1193].
prop aux1198 := [[[aux1194 | aux1195] | aux1196] | aux1197].
prop aux1199 := [[[d_at_10 >= 0] & [x_at_10 = (x_aux_at_10 + d_at_10)]] & [[[aux1188 | aux1189] & [y_at_10 = (y_aux_at_10 + d_at_10)]] | [[aux1190 | aux1191] & [y_at_10 = (y_aux_at_10 - (2 * d_at_10))]]]].
prop aux1200 := [aux1188 => [y_at_10 <= 10]].
prop aux1201 := [aux1189 => [x_at_10 <= 2]].
prop aux1202 := [aux1190 => [y_at_10 >= 5]].
prop aux1203 := [aux1191 => [x_at_10 <= 2]].
prop aux1204 := [[~ pc1_at_10] & [~ pc2_at_10]].
prop aux1205 := [pc1_at_10 & [~ pc2_at_10]].
prop aux1206 := [[~ pc1_at_10] & pc2_at_10].
prop aux1207 := [pc1_at_10 & pc2_at_10].
prop aux1208 := [[~ pc1_at_11] & [~ pc2_at_11]].
prop aux1209 := [pc1_at_11 & [~ pc2_at_11]].
prop aux1210 := [[~ pc1_at_11] & pc2_at_11].
prop aux1211 := [pc1_at_11 & pc2_at_11].
prop aux1212 := [[x_aux_at_11 = 0] & [y_aux_at_11 = y_at_10]].
prop aux1213 := [[x_aux_at_11 = x_at_10] & [y_aux_at_11 = y_at_10]].
prop aux1214 := [[[aux1204 & aux1209] & [y_at_10 = 10]] & aux1212].
prop aux1215 := [[[aux1205 & aux1210] & [x_at_10 = 2]] & aux1213].
prop aux1216 := [[[aux1206 & aux1211] & [y_at_10 = 5]] & aux1212].
prop aux1217 := [[[aux1207 & aux1208] & [x_at_10 = 2]] & aux1213].
prop aux1218 := [[[aux1214 | aux1215] | aux1216] | aux1217].
prop aux1219 := [[[d_at_11 >= 0] & [x_at_11 = (x_aux_at_11 + d_at_11)]] & [[[aux1208 | aux1209] & [y_at_11 = (y_aux_at_11 + d_at_11)]] | [[aux1210 | aux1211] & [y_at_11 = (y_aux_at_11 - (2 * d_at_11))]]]].
prop aux1220 := [aux1208 => [y_at_11 <= 10]].
prop aux1221 := [aux1209 => [x_at_11 <= 2]].
prop aux1222 := [aux1210 => [y_at_11 >= 5]].
prop aux1223 := [aux1211 => [x_at_11 <= 2]].
prop aux1224 := [[~ pc1_at_11] & [~ pc2_at_11]].
prop aux1225 := [pc1_at_11 & [~ pc2_at_11]].
prop aux1226 := [[~ pc1_at_11] & pc2_at_11].
prop aux1227 := [pc1_at_11 & pc2_at_11].
prop aux1228 := [[~ pc1_at_12] & [~ pc2_at_12]].
prop aux1229 := [pc1_at_12 & [~ pc2_at_12]].
prop aux1230 := [[~ pc1_at_12] & pc2_at_12].
prop aux1231 := [pc1_at_12 & pc2_at_12].
prop aux1232 := [[x_aux_at_12 = 0] & [y_aux_at_12 = y_at_11]].
prop aux1233 := [[x_aux_at_12 = x_at_11] & [y_aux_at_12 = y_at_11]].
prop aux1234 := [[[aux1224 & aux1229] & [y_at_11 = 10]] & aux1232].
prop aux1235 := [[[aux1225 & aux1230] & [x_at_11 = 2]] & aux1233].
prop aux1236 := [[[aux1226 & aux1231] & [y_at_11 = 5]] & aux1232].
prop aux1237 := [[[aux1227 & aux1228] & [x_at_11 = 2]] & aux1233].
prop aux1238 := [[[aux1234 | aux1235] | aux1236] | aux1237].
prop aux1239 := [[[d_at_12 >= 0] & [x_at_12 = (x_aux_at_12 + d_at_12)]] & [[[aux1228 | aux1229] & [y_at_12 = (y_aux_at_12 + d_at_12)]] | [[aux1230 | aux1231] & [y_at_12 = (y_aux_at_12 - (2 * d_at_12))]]]].
prop aux1240 := [aux1228 => [y_at_12 <= 10]].
prop aux1241 := [aux1229 => [x_at_12 <= 2]].
prop aux1242 := [aux1230 => [y_at_12 >= 5]].
prop aux1243 := [aux1231 => [x_at_12 <= 2]].
prop aux1244 := [[~ pc1_at_12] & [~ pc2_at_12]].
prop aux1245 := [pc1_at_12 & [~ pc2_at_12]].
prop aux1246 := [[~ pc1_at_12] & pc2_at_12].
prop aux1247 := [pc1_at_12 & pc2_at_12].
prop aux1248 := [[~ pc1_at_13] & [~ pc2_at_13]].
prop aux1249 := [pc1_at_13 & [~ pc2_at_13]].
prop aux1250 := [[~ pc1_at_13] & pc2_at_13].
prop aux1251 := [pc1_at_13 & pc2_at_13].
prop aux1252 := [[x_aux_at_13 = 0] & [y_aux_at_13 = y_at_12]].
prop aux1253 := [[x_aux_at_13 = x_at_12] & [y_aux_at_13 = y_at_12]].
prop aux1254 := [[[aux1244 & aux1249] & [y_at_12 = 10]] & aux1252].
prop aux1255 := [[[aux1245 & aux1250] & [x_at_12 = 2]] & aux1253].
prop aux1256 := [[[aux1246 & aux1251] & [y_at_12 = 5]] & aux1252].
prop aux1257 := [[[aux1247 & aux1248] & [x_at_12 = 2]] & aux1253].
prop aux1258 := [[[aux1254 | aux1255] | aux1256] | aux1257].
prop aux1259 := [[[d_at_13 >= 0] & [x_at_13 = (x_aux_at_13 + d_at_13)]] & [[[aux1248 | aux1249] & [y_at_13 = (y_aux_at_13 + d_at_13)]] | [[aux1250 | aux1251] & [y_at_13 = (y_aux_at_13 - (2 * d_at_13))]]]].
prop aux1260 := [aux1248 => [y_at_13 <= 10]].
prop aux1261 := [aux1249 => [x_at_13 <= 2]].
prop aux1262 := [aux1250 => [y_at_13 >= 5]].
prop aux1263 := [aux1251 => [x_at_13 <= 2]].
prop aux1264 := [[~ pc1_at_13] & [~ pc2_at_13]].
prop aux1265 := [pc1_at_13 & [~ pc2_at_13]].
prop aux1266 := [[~ pc1_at_13] & pc2_at_13].
prop aux1267 := [pc1_at_13 & pc2_at_13].
prop aux1268 := [[~ pc1_at_14] & [~ pc2_at_14]].
prop aux1269 := [pc1_at_14 & [~ pc2_at_14]].
prop aux1270 := [[~ pc1_at_14] & pc2_at_14].
prop aux1271 := [pc1_at_14 & pc2_at_14].
prop aux1272 := [[x_aux_at_14 = 0] & [y_aux_at_14 = y_at_13]].
prop aux1273 := [[x_aux_at_14 = x_at_13] & [y_aux_at_14 = y_at_13]].
prop aux1274 := [[[aux1264 & aux1269] & [y_at_13 = 10]] & aux1272].
prop aux1275 := [[[aux1265 & aux1270] & [x_at_13 = 2]] & aux1273].
prop aux1276 := [[[aux1266 & aux1271] & [y_at_13 = 5]] & aux1272].
prop aux1277 := [[[aux1267 & aux1268] & [x_at_13 = 2]] & aux1273].
prop aux1278 := [[[aux1274 | aux1275] | aux1276] | aux1277].
prop aux1279 := [[[d_at_14 >= 0] & [x_at_14 = (x_aux_at_14 + d_at_14)]] & [[[aux1268 | aux1269] & [y_at_14 = (y_aux_at_14 + d_at_14)]] | [[aux1270 | aux1271] & [y_at_14 = (y_aux_at_14 - (2 * d_at_14))]]]].
prop aux1280 := [aux1268 => [y_at_14 <= 10]].
prop aux1281 := [aux1269 => [x_at_14 <= 2]].
prop aux1282 := [aux1270 => [y_at_14 >= 5]].
prop aux1283 := [aux1271 => [x_at_14 <= 2]].
prop aux1284 := [[~ pc1_at_14] & [~ pc2_at_14]].
prop aux1285 := [pc1_at_14 & [~ pc2_at_14]].
prop aux1286 := [[~ pc1_at_14] & pc2_at_14].
prop aux1287 := [pc1_at_14 & pc2_at_14].
prop aux1288 := [[~ pc1_at_15] & [~ pc2_at_15]].
prop aux1289 := [pc1_at_15 & [~ pc2_at_15]].
prop aux1290 := [[~ pc1_at_15] & pc2_at_15].
prop aux1291 := [pc1_at_15 & pc2_at_15].
prop aux1292 := [[x_aux_at_15 = 0] & [y_aux_at_15 = y_at_14]].
prop aux1293 := [[x_aux_at_15 = x_at_14] & [y_aux_at_15 = y_at_14]].
prop aux1294 := [[[aux1284 & aux1289] & [y_at_14 = 10]] & aux1292].
prop aux1295 := [[[aux1285 & aux1290] & [x_at_14 = 2]] & aux1293].
prop aux1296 := [[[aux1286 & aux1291] & [y_at_14 = 5]] & aux1292].
prop aux1297 := [[[aux1287 & aux1288] & [x_at_14 = 2]] & aux1293].
prop aux1298 := [[[aux1294 | aux1295] | aux1296] | aux1297].
prop aux1299 := [[[d_at_15 >= 0] & [x_at_15 = (x_aux_at_15 + d_at_15)]] & [[[aux1288 | aux1289] & [y_at_15 = (y_aux_at_15 + d_at_15)]] | [[aux1290 | aux1291] & [y_at_15 = (y_aux_at_15 - (2 * d_at_15))]]]].
prop aux1300 := [aux1288 => [y_at_15 <= 10]].
prop aux1301 := [aux1289 => [x_at_15 <= 2]].
prop aux1302 := [aux1290 => [y_at_15 >= 5]].
prop aux1303 := [aux1291 => [x_at_15 <= 2]].
prop aux1304 := [[~ pc1_at_15] & [~ pc2_at_15]].
prop aux1305 := [pc1_at_15 & [~ pc2_at_15]].
prop aux1306 := [[~ pc1_at_15] & pc2_at_15].
prop aux1307 := [pc1_at_15 & pc2_at_15].
prop aux1308 := [[~ pc1_at_16] & [~ pc2_at_16]].
prop aux1309 := [pc1_at_16 & [~ pc2_at_16]].
prop aux1310 := [[~ pc1_at_16] & pc2_at_16].
prop aux1311 := [pc1_at_16 & pc2_at_16].
prop aux1312 := [[x_aux_at_16 = 0] & [y_aux_at_16 = y_at_15]].
prop aux1313 := [[x_aux_at_16 = x_at_15] & [y_aux_at_16 = y_at_15]].
prop aux1314 := [[[aux1304 & aux1309] & [y_at_15 = 10]] & aux1312].
prop aux1315 := [[[aux1305 & aux1310] & [x_at_15 = 2]] & aux1313].
prop aux1316 := [[[aux1306 & aux1311] & [y_at_15 = 5]] & aux1312].
prop aux1317 := [[[aux1307 & aux1308] & [x_at_15 = 2]] & aux1313].
prop aux1318 := [[[aux1314 | aux1315] | aux1316] | aux1317].
prop aux1319 := [[[d_at_16 >= 0] & [x_at_16 = (x_aux_at_16 + d_at_16)]] & [[[aux1308 | aux1309] & [y_at_16 = (y_aux_at_16 + d_at_16)]] | [[aux1310 | aux1311] & [y_at_16 = (y_aux_at_16 - (2 * d_at_16))]]]].
prop aux1320 := [aux1308 => [y_at_16 <= 10]].
prop aux1321 := [aux1309 => [x_at_16 <= 2]].
prop aux1322 := [aux1310 => [y_at_16 >= 5]].
prop aux1323 := [aux1311 => [x_at_16 <= 2]].
prop aux1324 := [[~ pc1_at_16] & [~ pc2_at_16]].
prop aux1325 := [pc1_at_16 & [~ pc2_at_16]].
prop aux1326 := [[~ pc1_at_16] & pc2_at_16].
prop aux1327 := [pc1_at_16 & pc2_at_16].
prop aux1328 := [[~ pc1_at_17] & [~ pc2_at_17]].
prop aux1329 := [pc1_at_17 & [~ pc2_at_17]].
prop aux1330 := [[~ pc1_at_17] & pc2_at_17].
prop aux1331 := [pc1_at_17 & pc2_at_17].
prop aux1332 := [[x_aux_at_17 = 0] & [y_aux_at_17 = y_at_16]].
prop aux1333 := [[x_aux_at_17 = x_at_16] & [y_aux_at_17 = y_at_16]].
prop aux1334 := [[[aux1324 & aux1329] & [y_at_16 = 10]] & aux1332].
prop aux1335 := [[[aux1325 & aux1330] & [x_at_16 = 2]] & aux1333].
prop aux1336 := [[[aux1326 & aux1331] & [y_at_16 = 5]] & aux1332].
prop aux1337 := [[[aux1327 & aux1328] & [x_at_16 = 2]] & aux1333].
prop aux1338 := [[[aux1334 | aux1335] | aux1336] | aux1337].
prop aux1339 := [[[d_at_17 >= 0] & [x_at_17 = (x_aux_at_17 + d_at_17)]] & [[[aux1328 | aux1329] & [y_at_17 = (y_aux_at_17 + d_at_17)]] | [[aux1330 | aux1331] & [y_at_17 = (y_aux_at_17 - (2 * d_at_17))]]]].
prop aux1340 := [aux1328 => [y_at_17 <= 10]].
prop aux1341 := [aux1329 => [x_at_17 <= 2]].
prop aux1342 := [aux1330 => [y_at_17 >= 5]].
prop aux1343 := [aux1331 => [x_at_17 <= 2]].
prop aux1344 := [[~ pc1_at_17] & [~ pc2_at_17]].
prop aux1345 := [pc1_at_17 & [~ pc2_at_17]].
prop aux1346 := [[~ pc1_at_17] & pc2_at_17].
prop aux1347 := [pc1_at_17 & pc2_at_17].
prop aux1348 := [[~ pc1_at_18] & [~ pc2_at_18]].
prop aux1349 := [pc1_at_18 & [~ pc2_at_18]].
prop aux1350 := [[~ pc1_at_18] & pc2_at_18].
prop aux1351 := [pc1_at_18 & pc2_at_18].
prop aux1352 := [[x_aux_at_18 = 0] & [y_aux_at_18 = y_at_17]].
prop aux1353 := [[x_aux_at_18 = x_at_17] & [y_aux_at_18 = y_at_17]].
prop aux1354 := [[[aux1344 & aux1349] & [y_at_17 = 10]] & aux1352].
prop aux1355 := [[[aux1345 & aux1350] & [x_at_17 = 2]] & aux1353].
prop aux1356 := [[[aux1346 & aux1351] & [y_at_17 = 5]] & aux1352].
prop aux1357 := [[[aux1347 & aux1348] & [x_at_17 = 2]] & aux1353].
prop aux1358 := [[[aux1354 | aux1355] | aux1356] | aux1357].
prop aux1359 := [[[d_at_18 >= 0] & [x_at_18 = (x_aux_at_18 + d_at_18)]] & [[[aux1348 | aux1349] & [y_at_18 = (y_aux_at_18 + d_at_18)]] | [[aux1350 | aux1351] & [y_at_18 = (y_aux_at_18 - (2 * d_at_18))]]]].
prop aux1360 := [aux1348 => [y_at_18 <= 10]].
prop aux1361 := [aux1349 => [x_at_18 <= 2]].
prop aux1362 := [aux1350 => [y_at_18 >= 5]].
prop aux1363 := [aux1351 => [x_at_18 <= 2]].
prop aux1364 := [[~ pc1_at_18] & [~ pc2_at_18]].
prop aux1365 := [pc1_at_18 & [~ pc2_at_18]].
prop aux1366 := [[~ pc1_at_18] & pc2_at_18].
prop aux1367 := [pc1_at_18 & pc2_at_18].
prop aux1368 := [[~ pc1_at_19] & [~ pc2_at_19]].
prop aux1369 := [pc1_at_19 & [~ pc2_at_19]].
prop aux1370 := [[~ pc1_at_19] & pc2_at_19].
prop aux1371 := [pc1_at_19 & pc2_at_19].
prop aux1372 := [[x_aux_at_19 = 0] & [y_aux_at_19 = y_at_18]].
prop aux1373 := [[x_aux_at_19 = x_at_18] & [y_aux_at_19 = y_at_18]].
prop aux1374 := [[[aux1364 & aux1369] & [y_at_18 = 10]] & aux1372].
prop aux1375 := [[[aux1365 & aux1370] & [x_at_18 = 2]] & aux1373].
prop aux1376 := [[[aux1366 & aux1371] & [y_at_18 = 5]] & aux1372].
prop aux1377 := [[[aux1367 & aux1368] & [x_at_18 = 2]] & aux1373].
prop aux1378 := [[[aux1374 | aux1375] | aux1376] | aux1377].
prop aux1379 := [[[d_at_19 >= 0] & [x_at_19 = (x_aux_at_19 + d_at_19)]] & [[[aux1368 | aux1369] & [y_at_19 = (y_aux_at_19 + d_at_19)]] | [[aux1370 | aux1371] & [y_at_19 = (y_aux_at_19 - (2 * d_at_19))]]]].
prop aux1380 := [aux1368 => [y_at_19 <= 10]].
prop aux1381 := [aux1369 => [x_at_19 <= 2]].
prop aux1382 := [aux1370 => [y_at_19 >= 5]].
prop aux1383 := [aux1371 => [x_at_19 <= 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] & [[[[[aux1098 & aux1099] & aux1100] & aux1101] & aux1102] & aux1103] & [[[[[aux1118 & aux1119] & aux1120] & aux1121] & aux1122] & aux1123] & [[[[[aux1138 & aux1139] & aux1140] & aux1141] & aux1142] & aux1143] & [[[[[aux1158 & aux1159] & aux1160] & aux1161] & aux1162] & aux1163] & [[[[[aux1178 & aux1179] & aux1180] & aux1181] & aux1182] & aux1183] & [[[[[aux1198 & aux1199] & aux1200] & aux1201] & aux1202] & aux1203] & [[[[[aux1218 & aux1219] & aux1220] & aux1221] & aux1222] & aux1223] & [[[[[aux1238 & aux1239] & aux1240] & aux1241] & aux1242] & aux1243] & [[[[[aux1258 & aux1259] & aux1260] & aux1261] & aux1262] & aux1263] & [[[[[aux1278 & aux1279] & aux1280] & aux1281] & aux1282] & aux1283] & [[[[[aux1298 & aux1299] & aux1300] & aux1301] & aux1302] & aux1303] & [[[[[aux1318 & aux1319] & aux1320] & aux1321] & aux1322] & aux1323] & [[[[[aux1338 & aux1339] & aux1340] & aux1341] & aux1342] & aux1343] & [[[[[aux1358 & aux1359] & aux1360] & aux1361] & aux1362] & aux1363] & [[[[[aux1378 & aux1379] & aux1380] & aux1381] & aux1382] & aux1383]] & 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]] & [[y_at_5 >= 1] & [y_at_5 <= 12]] & [[y_at_6 >= 1] & [y_at_6 <= 12]] & [[y_at_7 >= 1] & [y_at_7 <= 12]] & [[y_at_8 >= 1] & [y_at_8 <= 12]] & [[y_at_9 >= 1] & [y_at_9 <= 12]] & [[y_at_10 >= 1] & [y_at_10 <= 12]] & [[y_at_11 >= 1] & [y_at_11 <= 12]] & [[y_at_12 >= 1] & [y_at_12 <= 12]] & [[y_at_13 >= 1] & [y_at_13 <= 12]] & [[y_at_14 >= 1] & [y_at_14 <= 12]] & [[y_at_15 >= 1] & [y_at_15 <= 12]] & [[y_at_16 >= 1] & [y_at_16 <= 12]] & [[y_at_17 >= 1] & [y_at_17 <= 12]] & [[y_at_18 >= 1] & [y_at_18 <= 12]] & [[y_at_19 >= 1] & [y_at_19 <= 12]]]]].