prop aux1001 := [[~ pc11_at_0] & [~ pc12_at_0]].
prop aux1002 := [pc11_at_0 & [~ pc12_at_0]].
prop aux1003 := [[~ pc11_at_0] & pc12_at_0].
prop aux1004 := [pc11_at_0 & pc12_at_0].
prop aux1005 := [[~ pc11_at_1] & [~ pc12_at_1]].
prop aux1006 := [pc11_at_1 & [~ pc12_at_1]].
prop aux1007 := [[~ pc11_at_1] & pc12_at_1].
prop aux1008 := [pc11_at_1 & pc12_at_1].
prop aux1009 := [[~ pc21_at_0] & [~ pc22_at_0]].
prop aux1010 := [pc21_at_0 & [~ pc22_at_0]].
prop aux1011 := [[~ pc21_at_0] & pc22_at_0].
prop aux1012 := [pc21_at_0 & pc22_at_0].
prop aux1013 := [[~ pc21_at_1] & [~ pc22_at_1]].
prop aux1014 := [pc21_at_1 & [~ pc22_at_1]].
prop aux1015 := [[~ pc21_at_1] & pc22_at_1].
prop aux1016 := [pc21_at_1 & pc22_at_1].
prop aux1017 := [[~ k1_at_0] & [~ k2_at_0]].
prop aux1018 := [k1_at_0 & [~ k2_at_0]].
prop aux1019 := [[~ k1_at_0] & k2_at_0].
prop aux1020 := [[~ k1_at_1] & [~ k2_at_1]].
prop aux1021 := [k1_at_1 & [~ k2_at_1]].
prop aux1022 := [[~ k1_at_1] & k2_at_1].
prop aux1023 := [[k1_at_1 <=> k1_at_0] & [k2_at_1 <=> k2_at_0]].
prop aux1024 := [aux1006 => [x_at_1 < a]].
prop aux1025 := [aux1014 => [y_at_1 < a]].
prop aux1026 := [[pc11_at_1 <=> pc11_at_0] & [pc12_at_1 <=> pc12_at_0]].
prop aux1027 := [[pc21_at_1 <=> pc21_at_0] & [pc22_at_1 <=> pc22_at_0]].
prop aux1028 := [aux1026 & [x_aux_at_1 = x_at_0]].
prop aux1029 := [aux1027 & [y_aux_at_1 = y_at_0]].
prop aux1030 := [[[[[[[[aux1001 & aux1006] & aux1017] & [x_aux_at_1 = 0]] & aux1023] | [[[aux1002 & aux1007] & [x_aux_at_1 = 0]] & aux1021]] | [[[[[aux1003 & aux1008] & [x_at_0 > b]] & aux1018] & [x_aux_at_1 = x_at_0]] & aux1023]] | [[[[[aux1003 & aux1006] & [x_at_0 > b]] & [~ aux1018]] & [x_aux_at_1 = x_at_0]] & aux1023]] | [[[aux1004 & aux1006] & [x_aux_at_1 = x_at_0]] & aux1020]].
prop aux1031 := [[[[[[[[aux1009 & aux1014] & aux1017] & [y_aux_at_1 = 0]] & aux1023] | [[[aux1010 & aux1015] & [y_aux_at_1 = 0]] & aux1022]] | [[[[[aux1011 & aux1016] & [y_at_0 > b]] & aux1019] & [y_aux_at_1 = y_at_0]] & aux1023]] | [[[[[aux1011 & aux1014] & [y_at_0 > b]] & [~ aux1019]] & [y_aux_at_1 = y_at_0]] & aux1023]] | [[[aux1012 & aux1014] & [y_aux_at_1 = y_at_0]] & aux1020]].
prop aux1032 := [[[d_at_1 >= 0] & [x_at_1 = (x_aux_at_1 + d_at_1)]] & [(10 * y_at_1) = ((10 * y_aux_at_1) + (11 * d_at_1))]].
prop aux1033 := [[aux1030 & aux1029] | [aux1031 & aux1028]].
prop aux1034 := [[~ pc11_at_1] & [~ pc12_at_1]].
prop aux1035 := [pc11_at_1 & [~ pc12_at_1]].
prop aux1036 := [[~ pc11_at_1] & pc12_at_1].
prop aux1037 := [pc11_at_1 & pc12_at_1].
prop aux1038 := [[~ pc11_at_2] & [~ pc12_at_2]].
prop aux1039 := [pc11_at_2 & [~ pc12_at_2]].
prop aux1040 := [[~ pc11_at_2] & pc12_at_2].
prop aux1041 := [pc11_at_2 & pc12_at_2].
prop aux1042 := [[~ pc21_at_1] & [~ pc22_at_1]].
prop aux1043 := [pc21_at_1 & [~ pc22_at_1]].
prop aux1044 := [[~ pc21_at_1] & pc22_at_1].
prop aux1045 := [pc21_at_1 & pc22_at_1].
prop aux1046 := [[~ pc21_at_2] & [~ pc22_at_2]].
prop aux1047 := [pc21_at_2 & [~ pc22_at_2]].
prop aux1048 := [[~ pc21_at_2] & pc22_at_2].
prop aux1049 := [pc21_at_2 & pc22_at_2].
prop aux1050 := [[~ k1_at_1] & [~ k2_at_1]].
prop aux1051 := [k1_at_1 & [~ k2_at_1]].
prop aux1052 := [[~ k1_at_1] & k2_at_1].
prop aux1053 := [[~ k1_at_2] & [~ k2_at_2]].
prop aux1054 := [k1_at_2 & [~ k2_at_2]].
prop aux1055 := [[~ k1_at_2] & k2_at_2].
prop aux1056 := [[k1_at_2 <=> k1_at_1] & [k2_at_2 <=> k2_at_1]].
prop aux1057 := [aux1039 => [x_at_2 < a]].
prop aux1058 := [aux1047 => [y_at_2 < a]].
prop aux1059 := [[pc11_at_2 <=> pc11_at_1] & [pc12_at_2 <=> pc12_at_1]].
prop aux1060 := [[pc21_at_2 <=> pc21_at_1] & [pc22_at_2 <=> pc22_at_1]].
prop aux1061 := [aux1059 & [x_aux_at_2 = x_at_1]].
prop aux1062 := [aux1060 & [y_aux_at_2 = y_at_1]].
prop aux1063 := [[[[[[[[aux1034 & aux1039] & aux1050] & [x_aux_at_2 = 0]] & aux1056] | [[[aux1035 & aux1040] & [x_aux_at_2 = 0]] & aux1054]] | [[[[[aux1036 & aux1041] & [x_at_1 > b]] & aux1051] & [x_aux_at_2 = x_at_1]] & aux1056]] | [[[[[aux1036 & aux1039] & [x_at_1 > b]] & [~ aux1051]] & [x_aux_at_2 = x_at_1]] & aux1056]] | [[[aux1037 & aux1039] & [x_aux_at_2 = x_at_1]] & aux1053]].
prop aux1064 := [[[[[[[[aux1042 & aux1047] & aux1050] & [y_aux_at_2 = 0]] & aux1056] | [[[aux1043 & aux1048] & [y_aux_at_2 = 0]] & aux1055]] | [[[[[aux1044 & aux1049] & [y_at_1 > b]] & aux1052] & [y_aux_at_2 = y_at_1]] & aux1056]] | [[[[[aux1044 & aux1047] & [y_at_1 > b]] & [~ aux1052]] & [y_aux_at_2 = y_at_1]] & aux1056]] | [[[aux1045 & aux1047] & [y_aux_at_2 = y_at_1]] & aux1053]].
prop aux1065 := [[[d_at_2 >= 0] & [x_at_2 = (x_aux_at_2 + d_at_2)]] & [(10 * y_at_2) = ((10 * y_aux_at_2) + (11 * d_at_2))]].
prop aux1066 := [[aux1063 & aux1062] | [aux1064 & aux1061]].
prop aux1067 := [[~ pc11_at_2] & [~ pc12_at_2]].
prop aux1068 := [pc11_at_2 & [~ pc12_at_2]].
prop aux1069 := [[~ pc11_at_2] & pc12_at_2].
prop aux1070 := [pc11_at_2 & pc12_at_2].
prop aux1071 := [[~ pc11_at_3] & [~ pc12_at_3]].
prop aux1072 := [pc11_at_3 & [~ pc12_at_3]].
prop aux1073 := [[~ pc11_at_3] & pc12_at_3].
prop aux1074 := [pc11_at_3 & pc12_at_3].
prop aux1075 := [[~ pc21_at_2] & [~ pc22_at_2]].
prop aux1076 := [pc21_at_2 & [~ pc22_at_2]].
prop aux1077 := [[~ pc21_at_2] & pc22_at_2].
prop aux1078 := [pc21_at_2 & pc22_at_2].
prop aux1079 := [[~ pc21_at_3] & [~ pc22_at_3]].
prop aux1080 := [pc21_at_3 & [~ pc22_at_3]].
prop aux1081 := [[~ pc21_at_3] & pc22_at_3].
prop aux1082 := [pc21_at_3 & pc22_at_3].
prop aux1083 := [[~ k1_at_2] & [~ k2_at_2]].
prop aux1084 := [k1_at_2 & [~ k2_at_2]].
prop aux1085 := [[~ k1_at_2] & k2_at_2].
prop aux1086 := [[~ k1_at_3] & [~ k2_at_3]].
prop aux1087 := [k1_at_3 & [~ k2_at_3]].
prop aux1088 := [[~ k1_at_3] & k2_at_3].
prop aux1089 := [[k1_at_3 <=> k1_at_2] & [k2_at_3 <=> k2_at_2]].
prop aux1090 := [aux1072 => [x_at_3 < a]].
prop aux1091 := [aux1080 => [y_at_3 < a]].
prop aux1092 := [[pc11_at_3 <=> pc11_at_2] & [pc12_at_3 <=> pc12_at_2]].
prop aux1093 := [[pc21_at_3 <=> pc21_at_2] & [pc22_at_3 <=> pc22_at_2]].
prop aux1094 := [aux1092 & [x_aux_at_3 = x_at_2]].
prop aux1095 := [aux1093 & [y_aux_at_3 = y_at_2]].
prop aux1096 := [[[[[[[[aux1067 & aux1072] & aux1083] & [x_aux_at_3 = 0]] & aux1089] | [[[aux1068 & aux1073] & [x_aux_at_3 = 0]] & aux1087]] | [[[[[aux1069 & aux1074] & [x_at_2 > b]] & aux1084] & [x_aux_at_3 = x_at_2]] & aux1089]] | [[[[[aux1069 & aux1072] & [x_at_2 > b]] & [~ aux1084]] & [x_aux_at_3 = x_at_2]] & aux1089]] | [[[aux1070 & aux1072] & [x_aux_at_3 = x_at_2]] & aux1086]].
prop aux1097 := [[[[[[[[aux1075 & aux1080] & aux1083] & [y_aux_at_3 = 0]] & aux1089] | [[[aux1076 & aux1081] & [y_aux_at_3 = 0]] & aux1088]] | [[[[[aux1077 & aux1082] & [y_at_2 > b]] & aux1085] & [y_aux_at_3 = y_at_2]] & aux1089]] | [[[[[aux1077 & aux1080] & [y_at_2 > b]] & [~ aux1085]] & [y_aux_at_3 = y_at_2]] & aux1089]] | [[[aux1078 & aux1080] & [y_aux_at_3 = y_at_2]] & aux1086]].
prop aux1098 := [[[d_at_3 >= 0] & [x_at_3 = (x_aux_at_3 + d_at_3)]] & [(10 * y_at_3) = ((10 * y_aux_at_3) + (11 * d_at_3))]].
prop aux1099 := [[aux1096 & aux1095] | [aux1097 & aux1094]].
prop aux1100 := [[~ pc11_at_3] & [~ pc12_at_3]].
prop aux1101 := [pc11_at_3 & [~ pc12_at_3]].
prop aux1102 := [[~ pc11_at_3] & pc12_at_3].
prop aux1103 := [pc11_at_3 & pc12_at_3].
prop aux1104 := [[~ pc11_at_4] & [~ pc12_at_4]].
prop aux1105 := [pc11_at_4 & [~ pc12_at_4]].
prop aux1106 := [[~ pc11_at_4] & pc12_at_4].
prop aux1107 := [pc11_at_4 & pc12_at_4].
prop aux1108 := [[~ pc21_at_3] & [~ pc22_at_3]].
prop aux1109 := [pc21_at_3 & [~ pc22_at_3]].
prop aux1110 := [[~ pc21_at_3] & pc22_at_3].
prop aux1111 := [pc21_at_3 & pc22_at_3].
prop aux1112 := [[~ pc21_at_4] & [~ pc22_at_4]].
prop aux1113 := [pc21_at_4 & [~ pc22_at_4]].
prop aux1114 := [[~ pc21_at_4] & pc22_at_4].
prop aux1115 := [pc21_at_4 & pc22_at_4].
prop aux1116 := [[~ k1_at_3] & [~ k2_at_3]].
prop aux1117 := [k1_at_3 & [~ k2_at_3]].
prop aux1118 := [[~ k1_at_3] & k2_at_3].
prop aux1119 := [[~ k1_at_4] & [~ k2_at_4]].
prop aux1120 := [k1_at_4 & [~ k2_at_4]].
prop aux1121 := [[~ k1_at_4] & k2_at_4].
prop aux1122 := [[k1_at_4 <=> k1_at_3] & [k2_at_4 <=> k2_at_3]].
prop aux1123 := [aux1105 => [x_at_4 < a]].
prop aux1124 := [aux1113 => [y_at_4 < a]].
prop aux1125 := [[pc11_at_4 <=> pc11_at_3] & [pc12_at_4 <=> pc12_at_3]].
prop aux1126 := [[pc21_at_4 <=> pc21_at_3] & [pc22_at_4 <=> pc22_at_3]].
prop aux1127 := [aux1125 & [x_aux_at_4 = x_at_3]].
prop aux1128 := [aux1126 & [y_aux_at_4 = y_at_3]].
prop aux1129 := [[[[[[[[aux1100 & aux1105] & aux1116] & [x_aux_at_4 = 0]] & aux1122] | [[[aux1101 & aux1106] & [x_aux_at_4 = 0]] & aux1120]] | [[[[[aux1102 & aux1107] & [x_at_3 > b]] & aux1117] & [x_aux_at_4 = x_at_3]] & aux1122]] | [[[[[aux1102 & aux1105] & [x_at_3 > b]] & [~ aux1117]] & [x_aux_at_4 = x_at_3]] & aux1122]] | [[[aux1103 & aux1105] & [x_aux_at_4 = x_at_3]] & aux1119]].
prop aux1130 := [[[[[[[[aux1108 & aux1113] & aux1116] & [y_aux_at_4 = 0]] & aux1122] | [[[aux1109 & aux1114] & [y_aux_at_4 = 0]] & aux1121]] | [[[[[aux1110 & aux1115] & [y_at_3 > b]] & aux1118] & [y_aux_at_4 = y_at_3]] & aux1122]] | [[[[[aux1110 & aux1113] & [y_at_3 > b]] & [~ aux1118]] & [y_aux_at_4 = y_at_3]] & aux1122]] | [[[aux1111 & aux1113] & [y_aux_at_4 = y_at_3]] & aux1119]].
prop aux1131 := [[[d_at_4 >= 0] & [x_at_4 = (x_aux_at_4 + d_at_4)]] & [(10 * y_at_4) = ((10 * y_aux_at_4) + (11 * d_at_4))]].
prop aux1132 := [[aux1129 & aux1128] | [aux1130 & aux1127]].
prop aux1133 := [[~ pc11_at_4] & [~ pc12_at_4]].
prop aux1134 := [pc11_at_4 & [~ pc12_at_4]].
prop aux1135 := [[~ pc11_at_4] & pc12_at_4].
prop aux1136 := [pc11_at_4 & pc12_at_4].
prop aux1137 := [[~ pc11_at_5] & [~ pc12_at_5]].
prop aux1138 := [pc11_at_5 & [~ pc12_at_5]].
prop aux1139 := [[~ pc11_at_5] & pc12_at_5].
prop aux1140 := [pc11_at_5 & pc12_at_5].
prop aux1141 := [[~ pc21_at_4] & [~ pc22_at_4]].
prop aux1142 := [pc21_at_4 & [~ pc22_at_4]].
prop aux1143 := [[~ pc21_at_4] & pc22_at_4].
prop aux1144 := [pc21_at_4 & pc22_at_4].
prop aux1145 := [[~ pc21_at_5] & [~ pc22_at_5]].
prop aux1146 := [pc21_at_5 & [~ pc22_at_5]].
prop aux1147 := [[~ pc21_at_5] & pc22_at_5].
prop aux1148 := [pc21_at_5 & pc22_at_5].
prop aux1149 := [[~ k1_at_4] & [~ k2_at_4]].
prop aux1150 := [k1_at_4 & [~ k2_at_4]].
prop aux1151 := [[~ k1_at_4] & k2_at_4].
prop aux1152 := [[~ k1_at_5] & [~ k2_at_5]].
prop aux1153 := [k1_at_5 & [~ k2_at_5]].
prop aux1154 := [[~ k1_at_5] & k2_at_5].
prop aux1155 := [[k1_at_5 <=> k1_at_4] & [k2_at_5 <=> k2_at_4]].
prop aux1156 := [aux1138 => [x_at_5 < a]].
prop aux1157 := [aux1146 => [y_at_5 < a]].
prop aux1158 := [[pc11_at_5 <=> pc11_at_4] & [pc12_at_5 <=> pc12_at_4]].
prop aux1159 := [[pc21_at_5 <=> pc21_at_4] & [pc22_at_5 <=> pc22_at_4]].
prop aux1160 := [aux1158 & [x_aux_at_5 = x_at_4]].
prop aux1161 := [aux1159 & [y_aux_at_5 = y_at_4]].
prop aux1162 := [[[[[[[[aux1133 & aux1138] & aux1149] & [x_aux_at_5 = 0]] & aux1155] | [[[aux1134 & aux1139] & [x_aux_at_5 = 0]] & aux1153]] | [[[[[aux1135 & aux1140] & [x_at_4 > b]] & aux1150] & [x_aux_at_5 = x_at_4]] & aux1155]] | [[[[[aux1135 & aux1138] & [x_at_4 > b]] & [~ aux1150]] & [x_aux_at_5 = x_at_4]] & aux1155]] | [[[aux1136 & aux1138] & [x_aux_at_5 = x_at_4]] & aux1152]].
prop aux1163 := [[[[[[[[aux1141 & aux1146] & aux1149] & [y_aux_at_5 = 0]] & aux1155] | [[[aux1142 & aux1147] & [y_aux_at_5 = 0]] & aux1154]] | [[[[[aux1143 & aux1148] & [y_at_4 > b]] & aux1151] & [y_aux_at_5 = y_at_4]] & aux1155]] | [[[[[aux1143 & aux1146] & [y_at_4 > b]] & [~ aux1151]] & [y_aux_at_5 = y_at_4]] & aux1155]] | [[[aux1144 & aux1146] & [y_aux_at_5 = y_at_4]] & aux1152]].
prop aux1164 := [[[d_at_5 >= 0] & [x_at_5 = (x_aux_at_5 + d_at_5)]] & [(10 * y_at_5) = ((10 * y_aux_at_5) + (11 * d_at_5))]].
prop aux1165 := [[aux1162 & aux1161] | [aux1163 & aux1160]].
prop aux1166 := [[~ pc11_at_5] & [~ pc12_at_5]].
prop aux1167 := [pc11_at_5 & [~ pc12_at_5]].
prop aux1168 := [[~ pc11_at_5] & pc12_at_5].
prop aux1169 := [pc11_at_5 & pc12_at_5].
prop aux1170 := [[~ pc11_at_6] & [~ pc12_at_6]].
prop aux1171 := [pc11_at_6 & [~ pc12_at_6]].
prop aux1172 := [[~ pc11_at_6] & pc12_at_6].
prop aux1173 := [pc11_at_6 & pc12_at_6].
prop aux1174 := [[~ pc21_at_5] & [~ pc22_at_5]].
prop aux1175 := [pc21_at_5 & [~ pc22_at_5]].
prop aux1176 := [[~ pc21_at_5] & pc22_at_5].
prop aux1177 := [pc21_at_5 & pc22_at_5].
prop aux1178 := [[~ pc21_at_6] & [~ pc22_at_6]].
prop aux1179 := [pc21_at_6 & [~ pc22_at_6]].
prop aux1180 := [[~ pc21_at_6] & pc22_at_6].
prop aux1181 := [pc21_at_6 & pc22_at_6].
prop aux1182 := [[~ k1_at_5] & [~ k2_at_5]].
prop aux1183 := [k1_at_5 & [~ k2_at_5]].
prop aux1184 := [[~ k1_at_5] & k2_at_5].
prop aux1185 := [[~ k1_at_6] & [~ k2_at_6]].
prop aux1186 := [k1_at_6 & [~ k2_at_6]].
prop aux1187 := [[~ k1_at_6] & k2_at_6].
prop aux1188 := [[k1_at_6 <=> k1_at_5] & [k2_at_6 <=> k2_at_5]].
prop aux1189 := [aux1171 => [x_at_6 < a]].
prop aux1190 := [aux1179 => [y_at_6 < a]].
prop aux1191 := [[pc11_at_6 <=> pc11_at_5] & [pc12_at_6 <=> pc12_at_5]].
prop aux1192 := [[pc21_at_6 <=> pc21_at_5] & [pc22_at_6 <=> pc22_at_5]].
prop aux1193 := [aux1191 & [x_aux_at_6 = x_at_5]].
prop aux1194 := [aux1192 & [y_aux_at_6 = y_at_5]].
prop aux1195 := [[[[[[[[aux1166 & aux1171] & aux1182] & [x_aux_at_6 = 0]] & aux1188] | [[[aux1167 & aux1172] & [x_aux_at_6 = 0]] & aux1186]] | [[[[[aux1168 & aux1173] & [x_at_5 > b]] & aux1183] & [x_aux_at_6 = x_at_5]] & aux1188]] | [[[[[aux1168 & aux1171] & [x_at_5 > b]] & [~ aux1183]] & [x_aux_at_6 = x_at_5]] & aux1188]] | [[[aux1169 & aux1171] & [x_aux_at_6 = x_at_5]] & aux1185]].
prop aux1196 := [[[[[[[[aux1174 & aux1179] & aux1182] & [y_aux_at_6 = 0]] & aux1188] | [[[aux1175 & aux1180] & [y_aux_at_6 = 0]] & aux1187]] | [[[[[aux1176 & aux1181] & [y_at_5 > b]] & aux1184] & [y_aux_at_6 = y_at_5]] & aux1188]] | [[[[[aux1176 & aux1179] & [y_at_5 > b]] & [~ aux1184]] & [y_aux_at_6 = y_at_5]] & aux1188]] | [[[aux1177 & aux1179] & [y_aux_at_6 = y_at_5]] & aux1185]].
prop aux1197 := [[[d_at_6 >= 0] & [x_at_6 = (x_aux_at_6 + d_at_6)]] & [(10 * y_at_6) = ((10 * y_aux_at_6) + (11 * d_at_6))]].
prop aux1198 := [[aux1195 & aux1194] | [aux1196 & aux1193]].
prop aux1199 := [[~ pc11_at_6] & [~ pc12_at_6]].
prop aux1200 := [pc11_at_6 & [~ pc12_at_6]].
prop aux1201 := [[~ pc11_at_6] & pc12_at_6].
prop aux1202 := [pc11_at_6 & pc12_at_6].
prop aux1203 := [[~ pc11_at_7] & [~ pc12_at_7]].
prop aux1204 := [pc11_at_7 & [~ pc12_at_7]].
prop aux1205 := [[~ pc11_at_7] & pc12_at_7].
prop aux1206 := [pc11_at_7 & pc12_at_7].
prop aux1207 := [[~ pc21_at_6] & [~ pc22_at_6]].
prop aux1208 := [pc21_at_6 & [~ pc22_at_6]].
prop aux1209 := [[~ pc21_at_6] & pc22_at_6].
prop aux1210 := [pc21_at_6 & pc22_at_6].
prop aux1211 := [[~ pc21_at_7] & [~ pc22_at_7]].
prop aux1212 := [pc21_at_7 & [~ pc22_at_7]].
prop aux1213 := [[~ pc21_at_7] & pc22_at_7].
prop aux1214 := [pc21_at_7 & pc22_at_7].
prop aux1215 := [[~ k1_at_6] & [~ k2_at_6]].
prop aux1216 := [k1_at_6 & [~ k2_at_6]].
prop aux1217 := [[~ k1_at_6] & k2_at_6].
prop aux1218 := [[~ k1_at_7] & [~ k2_at_7]].
prop aux1219 := [k1_at_7 & [~ k2_at_7]].
prop aux1220 := [[~ k1_at_7] & k2_at_7].
prop aux1221 := [[k1_at_7 <=> k1_at_6] & [k2_at_7 <=> k2_at_6]].
prop aux1222 := [aux1204 => [x_at_7 < a]].
prop aux1223 := [aux1212 => [y_at_7 < a]].
prop aux1224 := [[pc11_at_7 <=> pc11_at_6] & [pc12_at_7 <=> pc12_at_6]].
prop aux1225 := [[pc21_at_7 <=> pc21_at_6] & [pc22_at_7 <=> pc22_at_6]].
prop aux1226 := [aux1224 & [x_aux_at_7 = x_at_6]].
prop aux1227 := [aux1225 & [y_aux_at_7 = y_at_6]].
prop aux1228 := [[[[[[[[aux1199 & aux1204] & aux1215] & [x_aux_at_7 = 0]] & aux1221] | [[[aux1200 & aux1205] & [x_aux_at_7 = 0]] & aux1219]] | [[[[[aux1201 & aux1206] & [x_at_6 > b]] & aux1216] & [x_aux_at_7 = x_at_6]] & aux1221]] | [[[[[aux1201 & aux1204] & [x_at_6 > b]] & [~ aux1216]] & [x_aux_at_7 = x_at_6]] & aux1221]] | [[[aux1202 & aux1204] & [x_aux_at_7 = x_at_6]] & aux1218]].
prop aux1229 := [[[[[[[[aux1207 & aux1212] & aux1215] & [y_aux_at_7 = 0]] & aux1221] | [[[aux1208 & aux1213] & [y_aux_at_7 = 0]] & aux1220]] | [[[[[aux1209 & aux1214] & [y_at_6 > b]] & aux1217] & [y_aux_at_7 = y_at_6]] & aux1221]] | [[[[[aux1209 & aux1212] & [y_at_6 > b]] & [~ aux1217]] & [y_aux_at_7 = y_at_6]] & aux1221]] | [[[aux1210 & aux1212] & [y_aux_at_7 = y_at_6]] & aux1218]].
prop aux1230 := [[[d_at_7 >= 0] & [x_at_7 = (x_aux_at_7 + d_at_7)]] & [(10 * y_at_7) = ((10 * y_aux_at_7) + (11 * d_at_7))]].
prop aux1231 := [[aux1228 & aux1227] | [aux1229 & aux1226]].
prop aux1232 := [[~ pc11_at_7] & [~ pc12_at_7]].
prop aux1233 := [pc11_at_7 & [~ pc12_at_7]].
prop aux1234 := [[~ pc11_at_7] & pc12_at_7].
prop aux1235 := [pc11_at_7 & pc12_at_7].
prop aux1236 := [[~ pc11_at_8] & [~ pc12_at_8]].
prop aux1237 := [pc11_at_8 & [~ pc12_at_8]].
prop aux1238 := [[~ pc11_at_8] & pc12_at_8].
prop aux1239 := [pc11_at_8 & pc12_at_8].
prop aux1240 := [[~ pc21_at_7] & [~ pc22_at_7]].
prop aux1241 := [pc21_at_7 & [~ pc22_at_7]].
prop aux1242 := [[~ pc21_at_7] & pc22_at_7].
prop aux1243 := [pc21_at_7 & pc22_at_7].
prop aux1244 := [[~ pc21_at_8] & [~ pc22_at_8]].
prop aux1245 := [pc21_at_8 & [~ pc22_at_8]].
prop aux1246 := [[~ pc21_at_8] & pc22_at_8].
prop aux1247 := [pc21_at_8 & pc22_at_8].
prop aux1248 := [[~ k1_at_7] & [~ k2_at_7]].
prop aux1249 := [k1_at_7 & [~ k2_at_7]].
prop aux1250 := [[~ k1_at_7] & k2_at_7].
prop aux1251 := [[~ k1_at_8] & [~ k2_at_8]].
prop aux1252 := [k1_at_8 & [~ k2_at_8]].
prop aux1253 := [[~ k1_at_8] & k2_at_8].
prop aux1254 := [[k1_at_8 <=> k1_at_7] & [k2_at_8 <=> k2_at_7]].
prop aux1255 := [aux1237 => [x_at_8 < a]].
prop aux1256 := [aux1245 => [y_at_8 < a]].
prop aux1257 := [[pc11_at_8 <=> pc11_at_7] & [pc12_at_8 <=> pc12_at_7]].
prop aux1258 := [[pc21_at_8 <=> pc21_at_7] & [pc22_at_8 <=> pc22_at_7]].
prop aux1259 := [aux1257 & [x_aux_at_8 = x_at_7]].
prop aux1260 := [aux1258 & [y_aux_at_8 = y_at_7]].
prop aux1261 := [[[[[[[[aux1232 & aux1237] & aux1248] & [x_aux_at_8 = 0]] & aux1254] | [[[aux1233 & aux1238] & [x_aux_at_8 = 0]] & aux1252]] | [[[[[aux1234 & aux1239] & [x_at_7 > b]] & aux1249] & [x_aux_at_8 = x_at_7]] & aux1254]] | [[[[[aux1234 & aux1237] & [x_at_7 > b]] & [~ aux1249]] & [x_aux_at_8 = x_at_7]] & aux1254]] | [[[aux1235 & aux1237] & [x_aux_at_8 = x_at_7]] & aux1251]].
prop aux1262 := [[[[[[[[aux1240 & aux1245] & aux1248] & [y_aux_at_8 = 0]] & aux1254] | [[[aux1241 & aux1246] & [y_aux_at_8 = 0]] & aux1253]] | [[[[[aux1242 & aux1247] & [y_at_7 > b]] & aux1250] & [y_aux_at_8 = y_at_7]] & aux1254]] | [[[[[aux1242 & aux1245] & [y_at_7 > b]] & [~ aux1250]] & [y_aux_at_8 = y_at_7]] & aux1254]] | [[[aux1243 & aux1245] & [y_aux_at_8 = y_at_7]] & aux1251]].
prop aux1263 := [[[d_at_8 >= 0] & [x_at_8 = (x_aux_at_8 + d_at_8)]] & [(10 * y_at_8) = ((10 * y_aux_at_8) + (11 * d_at_8))]].
prop aux1264 := [[aux1261 & aux1260] | [aux1262 & aux1259]].
prop aux1265 := [[~ pc11_at_8] & [~ pc12_at_8]].
prop aux1266 := [pc11_at_8 & [~ pc12_at_8]].
prop aux1267 := [[~ pc11_at_8] & pc12_at_8].
prop aux1268 := [pc11_at_8 & pc12_at_8].
prop aux1269 := [[~ pc11_at_9] & [~ pc12_at_9]].
prop aux1270 := [pc11_at_9 & [~ pc12_at_9]].
prop aux1271 := [[~ pc11_at_9] & pc12_at_9].
prop aux1272 := [pc11_at_9 & pc12_at_9].
prop aux1273 := [[~ pc21_at_8] & [~ pc22_at_8]].
prop aux1274 := [pc21_at_8 & [~ pc22_at_8]].
prop aux1275 := [[~ pc21_at_8] & pc22_at_8].
prop aux1276 := [pc21_at_8 & pc22_at_8].
prop aux1277 := [[~ pc21_at_9] & [~ pc22_at_9]].
prop aux1278 := [pc21_at_9 & [~ pc22_at_9]].
prop aux1279 := [[~ pc21_at_9] & pc22_at_9].
prop aux1280 := [pc21_at_9 & pc22_at_9].
prop aux1281 := [[~ k1_at_8] & [~ k2_at_8]].
prop aux1282 := [k1_at_8 & [~ k2_at_8]].
prop aux1283 := [[~ k1_at_8] & k2_at_8].
prop aux1284 := [[~ k1_at_9] & [~ k2_at_9]].
prop aux1285 := [k1_at_9 & [~ k2_at_9]].
prop aux1286 := [[~ k1_at_9] & k2_at_9].
prop aux1287 := [[k1_at_9 <=> k1_at_8] & [k2_at_9 <=> k2_at_8]].
prop aux1288 := [aux1270 => [x_at_9 < a]].
prop aux1289 := [aux1278 => [y_at_9 < a]].
prop aux1290 := [[pc11_at_9 <=> pc11_at_8] & [pc12_at_9 <=> pc12_at_8]].
prop aux1291 := [[pc21_at_9 <=> pc21_at_8] & [pc22_at_9 <=> pc22_at_8]].
prop aux1292 := [aux1290 & [x_aux_at_9 = x_at_8]].
prop aux1293 := [aux1291 & [y_aux_at_9 = y_at_8]].
prop aux1294 := [[[[[[[[aux1265 & aux1270] & aux1281] & [x_aux_at_9 = 0]] & aux1287] | [[[aux1266 & aux1271] & [x_aux_at_9 = 0]] & aux1285]] | [[[[[aux1267 & aux1272] & [x_at_8 > b]] & aux1282] & [x_aux_at_9 = x_at_8]] & aux1287]] | [[[[[aux1267 & aux1270] & [x_at_8 > b]] & [~ aux1282]] & [x_aux_at_9 = x_at_8]] & aux1287]] | [[[aux1268 & aux1270] & [x_aux_at_9 = x_at_8]] & aux1284]].
prop aux1295 := [[[[[[[[aux1273 & aux1278] & aux1281] & [y_aux_at_9 = 0]] & aux1287] | [[[aux1274 & aux1279] & [y_aux_at_9 = 0]] & aux1286]] | [[[[[aux1275 & aux1280] & [y_at_8 > b]] & aux1283] & [y_aux_at_9 = y_at_8]] & aux1287]] | [[[[[aux1275 & aux1278] & [y_at_8 > b]] & [~ aux1283]] & [y_aux_at_9 = y_at_8]] & aux1287]] | [[[aux1276 & aux1278] & [y_aux_at_9 = y_at_8]] & aux1284]].
prop aux1296 := [[[d_at_9 >= 0] & [x_at_9 = (x_aux_at_9 + d_at_9)]] & [(10 * y_at_9) = ((10 * y_aux_at_9) + (11 * d_at_9))]].
prop aux1297 := [[aux1294 & aux1293] | [aux1295 & aux1292]].
prop aux1298 := [[~ pc11_at_9] & [~ pc12_at_9]].
prop aux1299 := [pc11_at_9 & [~ pc12_at_9]].
prop aux1300 := [[~ pc11_at_9] & pc12_at_9].
prop aux1301 := [pc11_at_9 & pc12_at_9].
prop aux1302 := [[~ pc11_at_10] & [~ pc12_at_10]].
prop aux1303 := [pc11_at_10 & [~ pc12_at_10]].
prop aux1304 := [[~ pc11_at_10] & pc12_at_10].
prop aux1305 := [pc11_at_10 & pc12_at_10].
prop aux1306 := [[~ pc21_at_9] & [~ pc22_at_9]].
prop aux1307 := [pc21_at_9 & [~ pc22_at_9]].
prop aux1308 := [[~ pc21_at_9] & pc22_at_9].
prop aux1309 := [pc21_at_9 & pc22_at_9].
prop aux1310 := [[~ pc21_at_10] & [~ pc22_at_10]].
prop aux1311 := [pc21_at_10 & [~ pc22_at_10]].
prop aux1312 := [[~ pc21_at_10] & pc22_at_10].
prop aux1313 := [pc21_at_10 & pc22_at_10].
prop aux1314 := [[~ k1_at_9] & [~ k2_at_9]].
prop aux1315 := [k1_at_9 & [~ k2_at_9]].
prop aux1316 := [[~ k1_at_9] & k2_at_9].
prop aux1317 := [[~ k1_at_10] & [~ k2_at_10]].
prop aux1318 := [k1_at_10 & [~ k2_at_10]].
prop aux1319 := [[~ k1_at_10] & k2_at_10].
prop aux1320 := [[k1_at_10 <=> k1_at_9] & [k2_at_10 <=> k2_at_9]].
prop aux1321 := [aux1303 => [x_at_10 < a]].
prop aux1322 := [aux1311 => [y_at_10 < a]].
prop aux1323 := [[pc11_at_10 <=> pc11_at_9] & [pc12_at_10 <=> pc12_at_9]].
prop aux1324 := [[pc21_at_10 <=> pc21_at_9] & [pc22_at_10 <=> pc22_at_9]].
prop aux1325 := [aux1323 & [x_aux_at_10 = x_at_9]].
prop aux1326 := [aux1324 & [y_aux_at_10 = y_at_9]].
prop aux1327 := [[[[[[[[aux1298 & aux1303] & aux1314] & [x_aux_at_10 = 0]] & aux1320] | [[[aux1299 & aux1304] & [x_aux_at_10 = 0]] & aux1318]] | [[[[[aux1300 & aux1305] & [x_at_9 > b]] & aux1315] & [x_aux_at_10 = x_at_9]] & aux1320]] | [[[[[aux1300 & aux1303] & [x_at_9 > b]] & [~ aux1315]] & [x_aux_at_10 = x_at_9]] & aux1320]] | [[[aux1301 & aux1303] & [x_aux_at_10 = x_at_9]] & aux1317]].
prop aux1328 := [[[[[[[[aux1306 & aux1311] & aux1314] & [y_aux_at_10 = 0]] & aux1320] | [[[aux1307 & aux1312] & [y_aux_at_10 = 0]] & aux1319]] | [[[[[aux1308 & aux1313] & [y_at_9 > b]] & aux1316] & [y_aux_at_10 = y_at_9]] & aux1320]] | [[[[[aux1308 & aux1311] & [y_at_9 > b]] & [~ aux1316]] & [y_aux_at_10 = y_at_9]] & aux1320]] | [[[aux1309 & aux1311] & [y_aux_at_10 = y_at_9]] & aux1317]].
prop aux1329 := [[[d_at_10 >= 0] & [x_at_10 = (x_aux_at_10 + d_at_10)]] & [(10 * y_at_10) = ((10 * y_aux_at_10) + (11 * d_at_10))]].
prop aux1330 := [[aux1327 & aux1326] | [aux1328 & aux1325]].
prop aux1331 := [[~ pc11_at_10] & [~ pc12_at_10]].
prop aux1332 := [pc11_at_10 & [~ pc12_at_10]].
prop aux1333 := [[~ pc11_at_10] & pc12_at_10].
prop aux1334 := [pc11_at_10 & pc12_at_10].
prop aux1335 := [[~ pc11_at_11] & [~ pc12_at_11]].
prop aux1336 := [pc11_at_11 & [~ pc12_at_11]].
prop aux1337 := [[~ pc11_at_11] & pc12_at_11].
prop aux1338 := [pc11_at_11 & pc12_at_11].
prop aux1339 := [[~ pc21_at_10] & [~ pc22_at_10]].
prop aux1340 := [pc21_at_10 & [~ pc22_at_10]].
prop aux1341 := [[~ pc21_at_10] & pc22_at_10].
prop aux1342 := [pc21_at_10 & pc22_at_10].
prop aux1343 := [[~ pc21_at_11] & [~ pc22_at_11]].
prop aux1344 := [pc21_at_11 & [~ pc22_at_11]].
prop aux1345 := [[~ pc21_at_11] & pc22_at_11].
prop aux1346 := [pc21_at_11 & pc22_at_11].
prop aux1347 := [[~ k1_at_10] & [~ k2_at_10]].
prop aux1348 := [k1_at_10 & [~ k2_at_10]].
prop aux1349 := [[~ k1_at_10] & k2_at_10].
prop aux1350 := [[~ k1_at_11] & [~ k2_at_11]].
prop aux1351 := [k1_at_11 & [~ k2_at_11]].
prop aux1352 := [[~ k1_at_11] & k2_at_11].
prop aux1353 := [[k1_at_11 <=> k1_at_10] & [k2_at_11 <=> k2_at_10]].
prop aux1354 := [aux1336 => [x_at_11 < a]].
prop aux1355 := [aux1344 => [y_at_11 < a]].
prop aux1356 := [[pc11_at_11 <=> pc11_at_10] & [pc12_at_11 <=> pc12_at_10]].
prop aux1357 := [[pc21_at_11 <=> pc21_at_10] & [pc22_at_11 <=> pc22_at_10]].
prop aux1358 := [aux1356 & [x_aux_at_11 = x_at_10]].
prop aux1359 := [aux1357 & [y_aux_at_11 = y_at_10]].
prop aux1360 := [[[[[[[[aux1331 & aux1336] & aux1347] & [x_aux_at_11 = 0]] & aux1353] | [[[aux1332 & aux1337] & [x_aux_at_11 = 0]] & aux1351]] | [[[[[aux1333 & aux1338] & [x_at_10 > b]] & aux1348] & [x_aux_at_11 = x_at_10]] & aux1353]] | [[[[[aux1333 & aux1336] & [x_at_10 > b]] & [~ aux1348]] & [x_aux_at_11 = x_at_10]] & aux1353]] | [[[aux1334 & aux1336] & [x_aux_at_11 = x_at_10]] & aux1350]].
prop aux1361 := [[[[[[[[aux1339 & aux1344] & aux1347] & [y_aux_at_11 = 0]] & aux1353] | [[[aux1340 & aux1345] & [y_aux_at_11 = 0]] & aux1352]] | [[[[[aux1341 & aux1346] & [y_at_10 > b]] & aux1349] & [y_aux_at_11 = y_at_10]] & aux1353]] | [[[[[aux1341 & aux1344] & [y_at_10 > b]] & [~ aux1349]] & [y_aux_at_11 = y_at_10]] & aux1353]] | [[[aux1342 & aux1344] & [y_aux_at_11 = y_at_10]] & aux1350]].
prop aux1362 := [[[d_at_11 >= 0] & [x_at_11 = (x_aux_at_11 + d_at_11)]] & [(10 * y_at_11) = ((10 * y_aux_at_11) + (11 * d_at_11))]].
prop aux1363 := [[aux1360 & aux1359] | [aux1361 & aux1358]].
prop aux1364 := [[~ pc11_at_11] & [~ pc12_at_11]].
prop aux1365 := [pc11_at_11 & [~ pc12_at_11]].
prop aux1366 := [[~ pc11_at_11] & pc12_at_11].
prop aux1367 := [pc11_at_11 & pc12_at_11].
prop aux1368 := [[~ pc11_at_12] & [~ pc12_at_12]].
prop aux1369 := [pc11_at_12 & [~ pc12_at_12]].
prop aux1370 := [[~ pc11_at_12] & pc12_at_12].
prop aux1371 := [pc11_at_12 & pc12_at_12].
prop aux1372 := [[~ pc21_at_11] & [~ pc22_at_11]].
prop aux1373 := [pc21_at_11 & [~ pc22_at_11]].
prop aux1374 := [[~ pc21_at_11] & pc22_at_11].
prop aux1375 := [pc21_at_11 & pc22_at_11].
prop aux1376 := [[~ pc21_at_12] & [~ pc22_at_12]].
prop aux1377 := [pc21_at_12 & [~ pc22_at_12]].
prop aux1378 := [[~ pc21_at_12] & pc22_at_12].
prop aux1379 := [pc21_at_12 & pc22_at_12].
prop aux1380 := [[~ k1_at_11] & [~ k2_at_11]].
prop aux1381 := [k1_at_11 & [~ k2_at_11]].
prop aux1382 := [[~ k1_at_11] & k2_at_11].
prop aux1383 := [[~ k1_at_12] & [~ k2_at_12]].
prop aux1384 := [k1_at_12 & [~ k2_at_12]].
prop aux1385 := [[~ k1_at_12] & k2_at_12].
prop aux1386 := [[k1_at_12 <=> k1_at_11] & [k2_at_12 <=> k2_at_11]].
prop aux1387 := [aux1369 => [x_at_12 < a]].
prop aux1388 := [aux1377 => [y_at_12 < a]].
prop aux1389 := [[pc11_at_12 <=> pc11_at_11] & [pc12_at_12 <=> pc12_at_11]].
prop aux1390 := [[pc21_at_12 <=> pc21_at_11] & [pc22_at_12 <=> pc22_at_11]].
prop aux1391 := [aux1389 & [x_aux_at_12 = x_at_11]].
prop aux1392 := [aux1390 & [y_aux_at_12 = y_at_11]].
prop aux1393 := [[[[[[[[aux1364 & aux1369] & aux1380] & [x_aux_at_12 = 0]] & aux1386] | [[[aux1365 & aux1370] & [x_aux_at_12 = 0]] & aux1384]] | [[[[[aux1366 & aux1371] & [x_at_11 > b]] & aux1381] & [x_aux_at_12 = x_at_11]] & aux1386]] | [[[[[aux1366 & aux1369] & [x_at_11 > b]] & [~ aux1381]] & [x_aux_at_12 = x_at_11]] & aux1386]] | [[[aux1367 & aux1369] & [x_aux_at_12 = x_at_11]] & aux1383]].
prop aux1394 := [[[[[[[[aux1372 & aux1377] & aux1380] & [y_aux_at_12 = 0]] & aux1386] | [[[aux1373 & aux1378] & [y_aux_at_12 = 0]] & aux1385]] | [[[[[aux1374 & aux1379] & [y_at_11 > b]] & aux1382] & [y_aux_at_12 = y_at_11]] & aux1386]] | [[[[[aux1374 & aux1377] & [y_at_11 > b]] & [~ aux1382]] & [y_aux_at_12 = y_at_11]] & aux1386]] | [[[aux1375 & aux1377] & [y_aux_at_12 = y_at_11]] & aux1383]].
prop aux1395 := [[[d_at_12 >= 0] & [x_at_12 = (x_aux_at_12 + d_at_12)]] & [(10 * y_at_12) = ((10 * y_aux_at_12) + (11 * d_at_12))]].
prop aux1396 := [[aux1393 & aux1392] | [aux1394 & aux1391]].
prop aux1397 := [[~ pc11_at_12] & [~ pc12_at_12]].
prop aux1398 := [pc11_at_12 & [~ pc12_at_12]].
prop aux1399 := [[~ pc11_at_12] & pc12_at_12].
prop aux1400 := [pc11_at_12 & pc12_at_12].
prop aux1401 := [[~ pc11_at_13] & [~ pc12_at_13]].
prop aux1402 := [pc11_at_13 & [~ pc12_at_13]].
prop aux1403 := [[~ pc11_at_13] & pc12_at_13].
prop aux1404 := [pc11_at_13 & pc12_at_13].
prop aux1405 := [[~ pc21_at_12] & [~ pc22_at_12]].
prop aux1406 := [pc21_at_12 & [~ pc22_at_12]].
prop aux1407 := [[~ pc21_at_12] & pc22_at_12].
prop aux1408 := [pc21_at_12 & pc22_at_12].
prop aux1409 := [[~ pc21_at_13] & [~ pc22_at_13]].
prop aux1410 := [pc21_at_13 & [~ pc22_at_13]].
prop aux1411 := [[~ pc21_at_13] & pc22_at_13].
prop aux1412 := [pc21_at_13 & pc22_at_13].
prop aux1413 := [[~ k1_at_12] & [~ k2_at_12]].
prop aux1414 := [k1_at_12 & [~ k2_at_12]].
prop aux1415 := [[~ k1_at_12] & k2_at_12].
prop aux1416 := [[~ k1_at_13] & [~ k2_at_13]].
prop aux1417 := [k1_at_13 & [~ k2_at_13]].
prop aux1418 := [[~ k1_at_13] & k2_at_13].
prop aux1419 := [[k1_at_13 <=> k1_at_12] & [k2_at_13 <=> k2_at_12]].
prop aux1420 := [aux1402 => [x_at_13 < a]].
prop aux1421 := [aux1410 => [y_at_13 < a]].
prop aux1422 := [[pc11_at_13 <=> pc11_at_12] & [pc12_at_13 <=> pc12_at_12]].
prop aux1423 := [[pc21_at_13 <=> pc21_at_12] & [pc22_at_13 <=> pc22_at_12]].
prop aux1424 := [aux1422 & [x_aux_at_13 = x_at_12]].
prop aux1425 := [aux1423 & [y_aux_at_13 = y_at_12]].
prop aux1426 := [[[[[[[[aux1397 & aux1402] & aux1413] & [x_aux_at_13 = 0]] & aux1419] | [[[aux1398 & aux1403] & [x_aux_at_13 = 0]] & aux1417]] | [[[[[aux1399 & aux1404] & [x_at_12 > b]] & aux1414] & [x_aux_at_13 = x_at_12]] & aux1419]] | [[[[[aux1399 & aux1402] & [x_at_12 > b]] & [~ aux1414]] & [x_aux_at_13 = x_at_12]] & aux1419]] | [[[aux1400 & aux1402] & [x_aux_at_13 = x_at_12]] & aux1416]].
prop aux1427 := [[[[[[[[aux1405 & aux1410] & aux1413] & [y_aux_at_13 = 0]] & aux1419] | [[[aux1406 & aux1411] & [y_aux_at_13 = 0]] & aux1418]] | [[[[[aux1407 & aux1412] & [y_at_12 > b]] & aux1415] & [y_aux_at_13 = y_at_12]] & aux1419]] | [[[[[aux1407 & aux1410] & [y_at_12 > b]] & [~ aux1415]] & [y_aux_at_13 = y_at_12]] & aux1419]] | [[[aux1408 & aux1410] & [y_aux_at_13 = y_at_12]] & aux1416]].
prop aux1428 := [[[d_at_13 >= 0] & [x_at_13 = (x_aux_at_13 + d_at_13)]] & [(10 * y_at_13) = ((10 * y_aux_at_13) + (11 * d_at_13))]].
prop aux1429 := [[aux1426 & aux1425] | [aux1427 & aux1424]].
prop aux1430 := [[~ pc11_at_13] & [~ pc12_at_13]].
prop aux1431 := [pc11_at_13 & [~ pc12_at_13]].
prop aux1432 := [[~ pc11_at_13] & pc12_at_13].
prop aux1433 := [pc11_at_13 & pc12_at_13].
prop aux1434 := [[~ pc11_at_14] & [~ pc12_at_14]].
prop aux1435 := [pc11_at_14 & [~ pc12_at_14]].
prop aux1436 := [[~ pc11_at_14] & pc12_at_14].
prop aux1437 := [pc11_at_14 & pc12_at_14].
prop aux1438 := [[~ pc21_at_13] & [~ pc22_at_13]].
prop aux1439 := [pc21_at_13 & [~ pc22_at_13]].
prop aux1440 := [[~ pc21_at_13] & pc22_at_13].
prop aux1441 := [pc21_at_13 & pc22_at_13].
prop aux1442 := [[~ pc21_at_14] & [~ pc22_at_14]].
prop aux1443 := [pc21_at_14 & [~ pc22_at_14]].
prop aux1444 := [[~ pc21_at_14] & pc22_at_14].
prop aux1445 := [pc21_at_14 & pc22_at_14].
prop aux1446 := [[~ k1_at_13] & [~ k2_at_13]].
prop aux1447 := [k1_at_13 & [~ k2_at_13]].
prop aux1448 := [[~ k1_at_13] & k2_at_13].
prop aux1449 := [[~ k1_at_14] & [~ k2_at_14]].
prop aux1450 := [k1_at_14 & [~ k2_at_14]].
prop aux1451 := [[~ k1_at_14] & k2_at_14].
prop aux1452 := [[k1_at_14 <=> k1_at_13] & [k2_at_14 <=> k2_at_13]].
prop aux1453 := [aux1435 => [x_at_14 < a]].
prop aux1454 := [aux1443 => [y_at_14 < a]].
prop aux1455 := [[pc11_at_14 <=> pc11_at_13] & [pc12_at_14 <=> pc12_at_13]].
prop aux1456 := [[pc21_at_14 <=> pc21_at_13] & [pc22_at_14 <=> pc22_at_13]].
prop aux1457 := [aux1455 & [x_aux_at_14 = x_at_13]].
prop aux1458 := [aux1456 & [y_aux_at_14 = y_at_13]].
prop aux1459 := [[[[[[[[aux1430 & aux1435] & aux1446] & [x_aux_at_14 = 0]] & aux1452] | [[[aux1431 & aux1436] & [x_aux_at_14 = 0]] & aux1450]] | [[[[[aux1432 & aux1437] & [x_at_13 > b]] & aux1447] & [x_aux_at_14 = x_at_13]] & aux1452]] | [[[[[aux1432 & aux1435] & [x_at_13 > b]] & [~ aux1447]] & [x_aux_at_14 = x_at_13]] & aux1452]] | [[[aux1433 & aux1435] & [x_aux_at_14 = x_at_13]] & aux1449]].
prop aux1460 := [[[[[[[[aux1438 & aux1443] & aux1446] & [y_aux_at_14 = 0]] & aux1452] | [[[aux1439 & aux1444] & [y_aux_at_14 = 0]] & aux1451]] | [[[[[aux1440 & aux1445] & [y_at_13 > b]] & aux1448] & [y_aux_at_14 = y_at_13]] & aux1452]] | [[[[[aux1440 & aux1443] & [y_at_13 > b]] & [~ aux1448]] & [y_aux_at_14 = y_at_13]] & aux1452]] | [[[aux1441 & aux1443] & [y_aux_at_14 = y_at_13]] & aux1449]].
prop aux1461 := [[[d_at_14 >= 0] & [x_at_14 = (x_aux_at_14 + d_at_14)]] & [(10 * y_at_14) = ((10 * y_aux_at_14) + (11 * d_at_14))]].
prop aux1462 := [[aux1459 & aux1458] | [aux1460 & aux1457]].
prop aux1463 := [[~ pc11_at_14] & [~ pc12_at_14]].
prop aux1464 := [pc11_at_14 & [~ pc12_at_14]].
prop aux1465 := [[~ pc11_at_14] & pc12_at_14].
prop aux1466 := [pc11_at_14 & pc12_at_14].
prop aux1467 := [[~ pc11_at_15] & [~ pc12_at_15]].
prop aux1468 := [pc11_at_15 & [~ pc12_at_15]].
prop aux1469 := [[~ pc11_at_15] & pc12_at_15].
prop aux1470 := [pc11_at_15 & pc12_at_15].
prop aux1471 := [[~ pc21_at_14] & [~ pc22_at_14]].
prop aux1472 := [pc21_at_14 & [~ pc22_at_14]].
prop aux1473 := [[~ pc21_at_14] & pc22_at_14].
prop aux1474 := [pc21_at_14 & pc22_at_14].
prop aux1475 := [[~ pc21_at_15] & [~ pc22_at_15]].
prop aux1476 := [pc21_at_15 & [~ pc22_at_15]].
prop aux1477 := [[~ pc21_at_15] & pc22_at_15].
prop aux1478 := [pc21_at_15 & pc22_at_15].
prop aux1479 := [[~ k1_at_14] & [~ k2_at_14]].
prop aux1480 := [k1_at_14 & [~ k2_at_14]].
prop aux1481 := [[~ k1_at_14] & k2_at_14].
prop aux1482 := [[~ k1_at_15] & [~ k2_at_15]].
prop aux1483 := [k1_at_15 & [~ k2_at_15]].
prop aux1484 := [[~ k1_at_15] & k2_at_15].
prop aux1485 := [[k1_at_15 <=> k1_at_14] & [k2_at_15 <=> k2_at_14]].
prop aux1486 := [aux1468 => [x_at_15 < a]].
prop aux1487 := [aux1476 => [y_at_15 < a]].
prop aux1488 := [[pc11_at_15 <=> pc11_at_14] & [pc12_at_15 <=> pc12_at_14]].
prop aux1489 := [[pc21_at_15 <=> pc21_at_14] & [pc22_at_15 <=> pc22_at_14]].
prop aux1490 := [aux1488 & [x_aux_at_15 = x_at_14]].
prop aux1491 := [aux1489 & [y_aux_at_15 = y_at_14]].
prop aux1492 := [[[[[[[[aux1463 & aux1468] & aux1479] & [x_aux_at_15 = 0]] & aux1485] | [[[aux1464 & aux1469] & [x_aux_at_15 = 0]] & aux1483]] | [[[[[aux1465 & aux1470] & [x_at_14 > b]] & aux1480] & [x_aux_at_15 = x_at_14]] & aux1485]] | [[[[[aux1465 & aux1468] & [x_at_14 > b]] & [~ aux1480]] & [x_aux_at_15 = x_at_14]] & aux1485]] | [[[aux1466 & aux1468] & [x_aux_at_15 = x_at_14]] & aux1482]].
prop aux1493 := [[[[[[[[aux1471 & aux1476] & aux1479] & [y_aux_at_15 = 0]] & aux1485] | [[[aux1472 & aux1477] & [y_aux_at_15 = 0]] & aux1484]] | [[[[[aux1473 & aux1478] & [y_at_14 > b]] & aux1481] & [y_aux_at_15 = y_at_14]] & aux1485]] | [[[[[aux1473 & aux1476] & [y_at_14 > b]] & [~ aux1481]] & [y_aux_at_15 = y_at_14]] & aux1485]] | [[[aux1474 & aux1476] & [y_aux_at_15 = y_at_14]] & aux1482]].
prop aux1494 := [[[d_at_15 >= 0] & [x_at_15 = (x_aux_at_15 + d_at_15)]] & [(10 * y_at_15) = ((10 * y_aux_at_15) + (11 * d_at_15))]].
prop aux1495 := [[aux1492 & aux1491] | [aux1493 & aux1490]].
prop aux1496 := [[~ pc11_at_15] & [~ pc12_at_15]].
prop aux1497 := [pc11_at_15 & [~ pc12_at_15]].
prop aux1498 := [[~ pc11_at_15] & pc12_at_15].
prop aux1499 := [pc11_at_15 & pc12_at_15].
prop aux1500 := [[~ pc11_at_16] & [~ pc12_at_16]].
prop aux1501 := [pc11_at_16 & [~ pc12_at_16]].
prop aux1502 := [[~ pc11_at_16] & pc12_at_16].
prop aux1503 := [pc11_at_16 & pc12_at_16].
prop aux1504 := [[~ pc21_at_15] & [~ pc22_at_15]].
prop aux1505 := [pc21_at_15 & [~ pc22_at_15]].
prop aux1506 := [[~ pc21_at_15] & pc22_at_15].
prop aux1507 := [pc21_at_15 & pc22_at_15].
prop aux1508 := [[~ pc21_at_16] & [~ pc22_at_16]].
prop aux1509 := [pc21_at_16 & [~ pc22_at_16]].
prop aux1510 := [[~ pc21_at_16] & pc22_at_16].
prop aux1511 := [pc21_at_16 & pc22_at_16].
prop aux1512 := [[~ k1_at_15] & [~ k2_at_15]].
prop aux1513 := [k1_at_15 & [~ k2_at_15]].
prop aux1514 := [[~ k1_at_15] & k2_at_15].
prop aux1515 := [[~ k1_at_16] & [~ k2_at_16]].
prop aux1516 := [k1_at_16 & [~ k2_at_16]].
prop aux1517 := [[~ k1_at_16] & k2_at_16].
prop aux1518 := [[k1_at_16 <=> k1_at_15] & [k2_at_16 <=> k2_at_15]].
prop aux1519 := [aux1501 => [x_at_16 < a]].
prop aux1520 := [aux1509 => [y_at_16 < a]].
prop aux1521 := [[pc11_at_16 <=> pc11_at_15] & [pc12_at_16 <=> pc12_at_15]].
prop aux1522 := [[pc21_at_16 <=> pc21_at_15] & [pc22_at_16 <=> pc22_at_15]].
prop aux1523 := [aux1521 & [x_aux_at_16 = x_at_15]].
prop aux1524 := [aux1522 & [y_aux_at_16 = y_at_15]].
prop aux1525 := [[[[[[[[aux1496 & aux1501] & aux1512] & [x_aux_at_16 = 0]] & aux1518] | [[[aux1497 & aux1502] & [x_aux_at_16 = 0]] & aux1516]] | [[[[[aux1498 & aux1503] & [x_at_15 > b]] & aux1513] & [x_aux_at_16 = x_at_15]] & aux1518]] | [[[[[aux1498 & aux1501] & [x_at_15 > b]] & [~ aux1513]] & [x_aux_at_16 = x_at_15]] & aux1518]] | [[[aux1499 & aux1501] & [x_aux_at_16 = x_at_15]] & aux1515]].
prop aux1526 := [[[[[[[[aux1504 & aux1509] & aux1512] & [y_aux_at_16 = 0]] & aux1518] | [[[aux1505 & aux1510] & [y_aux_at_16 = 0]] & aux1517]] | [[[[[aux1506 & aux1511] & [y_at_15 > b]] & aux1514] & [y_aux_at_16 = y_at_15]] & aux1518]] | [[[[[aux1506 & aux1509] & [y_at_15 > b]] & [~ aux1514]] & [y_aux_at_16 = y_at_15]] & aux1518]] | [[[aux1507 & aux1509] & [y_aux_at_16 = y_at_15]] & aux1515]].
prop aux1527 := [[[d_at_16 >= 0] & [x_at_16 = (x_aux_at_16 + d_at_16)]] & [(10 * y_at_16) = ((10 * y_aux_at_16) + (11 * d_at_16))]].
prop aux1528 := [[aux1525 & aux1524] | [aux1526 & aux1523]].
prop aux1529 := [[~ pc11_at_16] & [~ pc12_at_16]].
prop aux1530 := [pc11_at_16 & [~ pc12_at_16]].
prop aux1531 := [[~ pc11_at_16] & pc12_at_16].
prop aux1532 := [pc11_at_16 & pc12_at_16].
prop aux1533 := [[~ pc11_at_17] & [~ pc12_at_17]].
prop aux1534 := [pc11_at_17 & [~ pc12_at_17]].
prop aux1535 := [[~ pc11_at_17] & pc12_at_17].
prop aux1536 := [pc11_at_17 & pc12_at_17].
prop aux1537 := [[~ pc21_at_16] & [~ pc22_at_16]].
prop aux1538 := [pc21_at_16 & [~ pc22_at_16]].
prop aux1539 := [[~ pc21_at_16] & pc22_at_16].
prop aux1540 := [pc21_at_16 & pc22_at_16].
prop aux1541 := [[~ pc21_at_17] & [~ pc22_at_17]].
prop aux1542 := [pc21_at_17 & [~ pc22_at_17]].
prop aux1543 := [[~ pc21_at_17] & pc22_at_17].
prop aux1544 := [pc21_at_17 & pc22_at_17].
prop aux1545 := [[~ k1_at_16] & [~ k2_at_16]].
prop aux1546 := [k1_at_16 & [~ k2_at_16]].
prop aux1547 := [[~ k1_at_16] & k2_at_16].
prop aux1548 := [[~ k1_at_17] & [~ k2_at_17]].
prop aux1549 := [k1_at_17 & [~ k2_at_17]].
prop aux1550 := [[~ k1_at_17] & k2_at_17].
prop aux1551 := [[k1_at_17 <=> k1_at_16] & [k2_at_17 <=> k2_at_16]].
prop aux1552 := [aux1534 => [x_at_17 < a]].
prop aux1553 := [aux1542 => [y_at_17 < a]].
prop aux1554 := [[pc11_at_17 <=> pc11_at_16] & [pc12_at_17 <=> pc12_at_16]].
prop aux1555 := [[pc21_at_17 <=> pc21_at_16] & [pc22_at_17 <=> pc22_at_16]].
prop aux1556 := [aux1554 & [x_aux_at_17 = x_at_16]].
prop aux1557 := [aux1555 & [y_aux_at_17 = y_at_16]].
prop aux1558 := [[[[[[[[aux1529 & aux1534] & aux1545] & [x_aux_at_17 = 0]] & aux1551] | [[[aux1530 & aux1535] & [x_aux_at_17 = 0]] & aux1549]] | [[[[[aux1531 & aux1536] & [x_at_16 > b]] & aux1546] & [x_aux_at_17 = x_at_16]] & aux1551]] | [[[[[aux1531 & aux1534] & [x_at_16 > b]] & [~ aux1546]] & [x_aux_at_17 = x_at_16]] & aux1551]] | [[[aux1532 & aux1534] & [x_aux_at_17 = x_at_16]] & aux1548]].
prop aux1559 := [[[[[[[[aux1537 & aux1542] & aux1545] & [y_aux_at_17 = 0]] & aux1551] | [[[aux1538 & aux1543] & [y_aux_at_17 = 0]] & aux1550]] | [[[[[aux1539 & aux1544] & [y_at_16 > b]] & aux1547] & [y_aux_at_17 = y_at_16]] & aux1551]] | [[[[[aux1539 & aux1542] & [y_at_16 > b]] & [~ aux1547]] & [y_aux_at_17 = y_at_16]] & aux1551]] | [[[aux1540 & aux1542] & [y_aux_at_17 = y_at_16]] & aux1548]].
prop aux1560 := [[[d_at_17 >= 0] & [x_at_17 = (x_aux_at_17 + d_at_17)]] & [(10 * y_at_17) = ((10 * y_aux_at_17) + (11 * d_at_17))]].
prop aux1561 := [[aux1558 & aux1557] | [aux1559 & aux1556]].
prop aux1562 := [[~ pc11_at_17] & [~ pc12_at_17]].
prop aux1563 := [pc11_at_17 & [~ pc12_at_17]].
prop aux1564 := [[~ pc11_at_17] & pc12_at_17].
prop aux1565 := [pc11_at_17 & pc12_at_17].
prop aux1566 := [[~ pc11_at_18] & [~ pc12_at_18]].
prop aux1567 := [pc11_at_18 & [~ pc12_at_18]].
prop aux1568 := [[~ pc11_at_18] & pc12_at_18].
prop aux1569 := [pc11_at_18 & pc12_at_18].
prop aux1570 := [[~ pc21_at_17] & [~ pc22_at_17]].
prop aux1571 := [pc21_at_17 & [~ pc22_at_17]].
prop aux1572 := [[~ pc21_at_17] & pc22_at_17].
prop aux1573 := [pc21_at_17 & pc22_at_17].
prop aux1574 := [[~ pc21_at_18] & [~ pc22_at_18]].
prop aux1575 := [pc21_at_18 & [~ pc22_at_18]].
prop aux1576 := [[~ pc21_at_18] & pc22_at_18].
prop aux1577 := [pc21_at_18 & pc22_at_18].
prop aux1578 := [[~ k1_at_17] & [~ k2_at_17]].
prop aux1579 := [k1_at_17 & [~ k2_at_17]].
prop aux1580 := [[~ k1_at_17] & k2_at_17].
prop aux1581 := [[~ k1_at_18] & [~ k2_at_18]].
prop aux1582 := [k1_at_18 & [~ k2_at_18]].
prop aux1583 := [[~ k1_at_18] & k2_at_18].
prop aux1584 := [[k1_at_18 <=> k1_at_17] & [k2_at_18 <=> k2_at_17]].
prop aux1585 := [aux1567 => [x_at_18 < a]].
prop aux1586 := [aux1575 => [y_at_18 < a]].
prop aux1587 := [[pc11_at_18 <=> pc11_at_17] & [pc12_at_18 <=> pc12_at_17]].
prop aux1588 := [[pc21_at_18 <=> pc21_at_17] & [pc22_at_18 <=> pc22_at_17]].
prop aux1589 := [aux1587 & [x_aux_at_18 = x_at_17]].
prop aux1590 := [aux1588 & [y_aux_at_18 = y_at_17]].
prop aux1591 := [[[[[[[[aux1562 & aux1567] & aux1578] & [x_aux_at_18 = 0]] & aux1584] | [[[aux1563 & aux1568] & [x_aux_at_18 = 0]] & aux1582]] | [[[[[aux1564 & aux1569] & [x_at_17 > b]] & aux1579] & [x_aux_at_18 = x_at_17]] & aux1584]] | [[[[[aux1564 & aux1567] & [x_at_17 > b]] & [~ aux1579]] & [x_aux_at_18 = x_at_17]] & aux1584]] | [[[aux1565 & aux1567] & [x_aux_at_18 = x_at_17]] & aux1581]].
prop aux1592 := [[[[[[[[aux1570 & aux1575] & aux1578] & [y_aux_at_18 = 0]] & aux1584] | [[[aux1571 & aux1576] & [y_aux_at_18 = 0]] & aux1583]] | [[[[[aux1572 & aux1577] & [y_at_17 > b]] & aux1580] & [y_aux_at_18 = y_at_17]] & aux1584]] | [[[[[aux1572 & aux1575] & [y_at_17 > b]] & [~ aux1580]] & [y_aux_at_18 = y_at_17]] & aux1584]] | [[[aux1573 & aux1575] & [y_aux_at_18 = y_at_17]] & aux1581]].
prop aux1593 := [[[d_at_18 >= 0] & [x_at_18 = (x_aux_at_18 + d_at_18)]] & [(10 * y_at_18) = ((10 * y_aux_at_18) + (11 * d_at_18))]].
prop aux1594 := [[aux1591 & aux1590] | [aux1592 & aux1589]].
prop aux1595 := [[~ pc11_at_18] & [~ pc12_at_18]].
prop aux1596 := [pc11_at_18 & [~ pc12_at_18]].
prop aux1597 := [[~ pc11_at_18] & pc12_at_18].
prop aux1598 := [pc11_at_18 & pc12_at_18].
prop aux1599 := [[~ pc11_at_19] & [~ pc12_at_19]].
prop aux1600 := [pc11_at_19 & [~ pc12_at_19]].
prop aux1601 := [[~ pc11_at_19] & pc12_at_19].
prop aux1602 := [pc11_at_19 & pc12_at_19].
prop aux1603 := [[~ pc21_at_18] & [~ pc22_at_18]].
prop aux1604 := [pc21_at_18 & [~ pc22_at_18]].
prop aux1605 := [[~ pc21_at_18] & pc22_at_18].
prop aux1606 := [pc21_at_18 & pc22_at_18].
prop aux1607 := [[~ pc21_at_19] & [~ pc22_at_19]].
prop aux1608 := [pc21_at_19 & [~ pc22_at_19]].
prop aux1609 := [[~ pc21_at_19] & pc22_at_19].
prop aux1610 := [pc21_at_19 & pc22_at_19].
prop aux1611 := [[~ k1_at_18] & [~ k2_at_18]].
prop aux1612 := [k1_at_18 & [~ k2_at_18]].
prop aux1613 := [[~ k1_at_18] & k2_at_18].
prop aux1614 := [[~ k1_at_19] & [~ k2_at_19]].
prop aux1615 := [k1_at_19 & [~ k2_at_19]].
prop aux1616 := [[~ k1_at_19] & k2_at_19].
prop aux1617 := [[k1_at_19 <=> k1_at_18] & [k2_at_19 <=> k2_at_18]].
prop aux1618 := [aux1600 => [x_at_19 < a]].
prop aux1619 := [aux1608 => [y_at_19 < a]].
prop aux1620 := [[pc11_at_19 <=> pc11_at_18] & [pc12_at_19 <=> pc12_at_18]].
prop aux1621 := [[pc21_at_19 <=> pc21_at_18] & [pc22_at_19 <=> pc22_at_18]].
prop aux1622 := [aux1620 & [x_aux_at_19 = x_at_18]].
prop aux1623 := [aux1621 & [y_aux_at_19 = y_at_18]].
prop aux1624 := [[[[[[[[aux1595 & aux1600] & aux1611] & [x_aux_at_19 = 0]] & aux1617] | [[[aux1596 & aux1601] & [x_aux_at_19 = 0]] & aux1615]] | [[[[[aux1597 & aux1602] & [x_at_18 > b]] & aux1612] & [x_aux_at_19 = x_at_18]] & aux1617]] | [[[[[aux1597 & aux1600] & [x_at_18 > b]] & [~ aux1612]] & [x_aux_at_19 = x_at_18]] & aux1617]] | [[[aux1598 & aux1600] & [x_aux_at_19 = x_at_18]] & aux1614]].
prop aux1625 := [[[[[[[[aux1603 & aux1608] & aux1611] & [y_aux_at_19 = 0]] & aux1617] | [[[aux1604 & aux1609] & [y_aux_at_19 = 0]] & aux1616]] | [[[[[aux1605 & aux1610] & [y_at_18 > b]] & aux1613] & [y_aux_at_19 = y_at_18]] & aux1617]] | [[[[[aux1605 & aux1608] & [y_at_18 > b]] & [~ aux1613]] & [y_aux_at_19 = y_at_18]] & aux1617]] | [[[aux1606 & aux1608] & [y_aux_at_19 = y_at_18]] & aux1614]].
prop aux1626 := [[[d_at_19 >= 0] & [x_at_19 = (x_aux_at_19 + d_at_19)]] & [(10 * y_at_19) = ((10 * y_aux_at_19) + (11 * d_at_19))]].
prop aux1627 := [[aux1624 & aux1623] | [aux1625 & aux1622]].
sat ~[
[[[[[[[[[~ pc11_at_0] & [~ pc12_at_0]] & [~ pc21_at_0]] & [~ pc22_at_0]] & [d_at_0 >= 0]] & [x_at_0 = d_at_0]] & [(10 * y_at_0) = (11 * d_at_0)]] & [[[[aux1033 & aux1032] & aux1024] & aux1025] & [[[aux1066 & aux1065] & aux1057] & aux1058] & [[[aux1099 & aux1098] & aux1090] & aux1091] & [[[aux1132 & aux1131] & aux1123] & aux1124] & [[[aux1165 & aux1164] & aux1156] & aux1157] & [[[aux1198 & aux1197] & aux1189] & aux1190] & [[[aux1231 & aux1230] & aux1222] & aux1223] & [[[aux1264 & aux1263] & aux1255] & aux1256] & [[[aux1297 & aux1296] & aux1288] & aux1289] & [[[aux1330 & aux1329] & aux1321] & aux1322] & [[[aux1363 & aux1362] & aux1354] & aux1355] & [[[aux1396 & aux1395] & aux1387] & aux1388] & [[[aux1429 & aux1428] & aux1420] & aux1421] & [[[aux1462 & aux1461] & aux1453] & aux1454] & [[[aux1495 & aux1494] & aux1486] & aux1487] & [[[aux1528 & aux1527] & aux1519] & aux1520] & [[[aux1561 & aux1560] & aux1552] & aux1553] & [[[aux1594 & aux1593] & aux1585] & aux1586] & [[[aux1627 & aux1626] & aux1618] & aux1619]] & tt] => [[[(11 * a) < (10 * b)] => [~ [[[pc11_at_0 & pc12_at_0] & pc21_at_0] & pc22_at_0]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_1 & pc12_at_1] & pc21_at_1] & pc22_at_1]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_2 & pc12_at_2] & pc21_at_2] & pc22_at_2]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_3 & pc12_at_3] & pc21_at_3] & pc22_at_3]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_4 & pc12_at_4] & pc21_at_4] & pc22_at_4]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_5 & pc12_at_5] & pc21_at_5] & pc22_at_5]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_6 & pc12_at_6] & pc21_at_6] & pc22_at_6]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_7 & pc12_at_7] & pc21_at_7] & pc22_at_7]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_8 & pc12_at_8] & pc21_at_8] & pc22_at_8]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_9 & pc12_at_9] & pc21_at_9] & pc22_at_9]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_10 & pc12_at_10] & pc21_at_10] & pc22_at_10]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_11 & pc12_at_11] & pc21_at_11] & pc22_at_11]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_12 & pc12_at_12] & pc21_at_12] & pc22_at_12]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_13 & pc12_at_13] & pc21_at_13] & pc22_at_13]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_14 & pc12_at_14] & pc21_at_14] & pc22_at_14]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_15 & pc12_at_15] & pc21_at_15] & pc22_at_15]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_16 & pc12_at_16] & pc21_at_16] & pc22_at_16]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_17 & pc12_at_17] & pc21_at_17] & pc22_at_17]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_18 & pc12_at_18] & pc21_at_18] & pc22_at_18]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_19 & pc12_at_19] & pc21_at_19] & pc22_at_19]]]]]].