prop aux1001 := [[~ tpc1_at_0] & [~ tpc2_at_0]].
prop aux1002 := [[~ gpc1_at_0] & [~ gpc2_at_0]].
prop aux1003 := [[~ cpc1_at_0] & [~ cpc2_at_0]].
prop aux1004 := [[[~ act1_at_0] & [~ act2_at_0]] & [~ act3_at_0]].
prop aux1005 := [[act1_at_0 & [~ act2_at_0]] & [~ act3_at_0]].
prop aux1006 := [[[~ act1_at_0] & act2_at_0] & [~ act3_at_0]].
prop aux1007 := [[act1_at_0 & act2_at_0] & [~ act3_at_0]].
prop aux1008 := [[[~ act1_at_0] & [~ act2_at_0]] & act3_at_0].
prop aux1009 := [[act1_at_0 & [~ act2_at_0]] & act3_at_0].
prop aux1010 := [[[~ act1_at_0] & act2_at_0] & act3_at_0].
prop aux1011 := [[act1_at_0 & act2_at_0] & act3_at_0].
prop aux1012 := [[~ tpc1_at_0] & [~ tpc2_at_0]].
prop aux1013 := [tpc1_at_0 & [~ tpc2_at_0]].
prop aux1014 := [[~ tpc1_at_0] & tpc2_at_0].
prop aux1015 := [tpc1_at_0 & tpc2_at_0].
prop aux1016 := [[~ tpc1_at_1] & [~ tpc2_at_1]].
prop aux1017 := [tpc1_at_1 & [~ tpc2_at_1]].
prop aux1018 := [[~ tpc1_at_1] & tpc2_at_1].
prop aux1019 := [tpc1_at_1 & tpc2_at_1].
prop aux1020 := [[~ gpc1_at_0] & [~ gpc2_at_0]].
prop aux1021 := [gpc1_at_0 & [~ gpc2_at_0]].
prop aux1022 := [[~ gpc1_at_0] & gpc2_at_0].
prop aux1023 := [gpc1_at_0 & gpc2_at_0].
prop aux1024 := [[~ gpc1_at_1] & [~ gpc2_at_1]].
prop aux1025 := [gpc1_at_1 & [~ gpc2_at_1]].
prop aux1026 := [[~ gpc1_at_1] & gpc2_at_1].
prop aux1027 := [gpc1_at_1 & gpc2_at_1].
prop aux1028 := [[~ cpc1_at_0] & [~ cpc2_at_0]].
prop aux1029 := [cpc1_at_0 & [~ cpc2_at_0]].
prop aux1030 := [[~ cpc1_at_0] & cpc2_at_0].
prop aux1031 := [cpc1_at_0 & cpc2_at_0].
prop aux1032 := [[~ cpc1_at_1] & [~ cpc2_at_1]].
prop aux1033 := [cpc1_at_1 & [~ cpc2_at_1]].
prop aux1034 := [[~ cpc1_at_1] & cpc2_at_1].
prop aux1035 := [cpc1_at_1 & cpc2_at_1].
prop aux1036 := [aux1017 => [x_at_1 <= 5]].
prop aux1037 := [aux1018 => [x_at_1 <= 5]].
prop aux1038 := [aux1019 => [x_at_1 <= 5]].
prop aux1039 := [aux1025 => [y_at_1 <= 1]].
prop aux1040 := [aux1027 => [y_at_1 <= 2]].
prop aux1041 := [aux1033 => [z_at_1 <= 1]].
prop aux1042 := [aux1035 => [z_at_1 <= 1]].
prop aux1043 := [[tpc1_at_1 <=> tpc1_at_0] & [tpc2_at_1 <=> tpc2_at_0]].
prop aux1044 := [aux1043 & [x_at_1 = (x_at_0 + d_at_0)]].
prop aux1045 := [[[[[[[[aux1012 & aux1017] & aux1004] & [x_at_1 = d_at_0]] | [[[[aux1013 & aux1018] & aux1005] & [x_at_0 > 2]] & [x_at_1 = (x_at_0 + d_at_0)]]] | [[[aux1014 & aux1019] & aux1006] & [x_at_1 = (x_at_0 + d_at_0)]]] | [[[aux1015 & aux1016] & aux1007] & [x_at_1 = (x_at_0 + d_at_0)]]] | [[[[aux1044 & [~ aux1004]] & [~ aux1005]] & [~ aux1006]] & [~ aux1007]]] & [[aux1036 & aux1037] & aux1038]].
prop aux1046 := [[gpc1_at_1 <=> gpc1_at_0] & [gpc2_at_1 <=> gpc2_at_0]].
prop aux1047 := [aux1046 & [y_at_1 = (y_at_0 + d_at_0)]].
prop aux1048 := [[[[[[[[aux1020 & aux1025] & aux1008] & [y_at_1 = d_at_0]] | [[[aux1021 & aux1026] & aux1009] & [y_at_1 = (y_at_0 + d_at_0)]]] | [[[aux1022 & aux1027] & aux1010] & [y_at_1 = d_at_0]]] | [[[[aux1023 & aux1024] & aux1011] & [y_at_0 >= 1]] & [y_at_1 = (y_at_0 + d_at_0)]]] | [[[[aux1047 & [~ aux1008]] & [~ aux1009]] & [~ aux1010]] & [~ aux1011]]] & [aux1039 & aux1040]].
prop aux1049 := [[cpc1_at_1 <=> cpc1_at_0] & [cpc2_at_1 <=> cpc2_at_0]].
prop aux1050 := [aux1049 & [z_at_1 = (z_at_0 + d_at_0)]].
prop aux1051 := [[[[[[[[aux1028 & aux1033] & aux1004] & [z_at_1 = d_at_0]] | [[[[aux1029 & aux1034] & aux1008] & [z_at_0 = 1]] & [z_at_1 = (z_at_0 + d_at_0)]]] | [[[aux1030 & aux1035] & aux1007] & [z_at_1 = d_at_0]]] | [[[aux1031 & aux1032] & aux1010] & [z_at_1 = (z_at_0 + d_at_0)]]] | [[[[aux1050 & [~ aux1004]] & [~ aux1008]] & [~ aux1007]] & [~ aux1010]]] & [aux1041 & aux1042]].
prop aux1052 := [d_at_0 >= 0].
prop aux1053 := [[[~ act1_at_1] & [~ act2_at_1]] & [~ act3_at_1]].
prop aux1054 := [[act1_at_1 & [~ act2_at_1]] & [~ act3_at_1]].
prop aux1055 := [[[~ act1_at_1] & act2_at_1] & [~ act3_at_1]].
prop aux1056 := [[act1_at_1 & act2_at_1] & [~ act3_at_1]].
prop aux1057 := [[[~ act1_at_1] & [~ act2_at_1]] & act3_at_1].
prop aux1058 := [[act1_at_1 & [~ act2_at_1]] & act3_at_1].
prop aux1059 := [[[~ act1_at_1] & act2_at_1] & act3_at_1].
prop aux1060 := [[act1_at_1 & act2_at_1] & act3_at_1].
prop aux1061 := [[~ tpc1_at_1] & [~ tpc2_at_1]].
prop aux1062 := [tpc1_at_1 & [~ tpc2_at_1]].
prop aux1063 := [[~ tpc1_at_1] & tpc2_at_1].
prop aux1064 := [tpc1_at_1 & tpc2_at_1].
prop aux1065 := [[~ tpc1_at_2] & [~ tpc2_at_2]].
prop aux1066 := [tpc1_at_2 & [~ tpc2_at_2]].
prop aux1067 := [[~ tpc1_at_2] & tpc2_at_2].
prop aux1068 := [tpc1_at_2 & tpc2_at_2].
prop aux1069 := [[~ gpc1_at_1] & [~ gpc2_at_1]].
prop aux1070 := [gpc1_at_1 & [~ gpc2_at_1]].
prop aux1071 := [[~ gpc1_at_1] & gpc2_at_1].
prop aux1072 := [gpc1_at_1 & gpc2_at_1].
prop aux1073 := [[~ gpc1_at_2] & [~ gpc2_at_2]].
prop aux1074 := [gpc1_at_2 & [~ gpc2_at_2]].
prop aux1075 := [[~ gpc1_at_2] & gpc2_at_2].
prop aux1076 := [gpc1_at_2 & gpc2_at_2].
prop aux1077 := [[~ cpc1_at_1] & [~ cpc2_at_1]].
prop aux1078 := [cpc1_at_1 & [~ cpc2_at_1]].
prop aux1079 := [[~ cpc1_at_1] & cpc2_at_1].
prop aux1080 := [cpc1_at_1 & cpc2_at_1].
prop aux1081 := [[~ cpc1_at_2] & [~ cpc2_at_2]].
prop aux1082 := [cpc1_at_2 & [~ cpc2_at_2]].
prop aux1083 := [[~ cpc1_at_2] & cpc2_at_2].
prop aux1084 := [cpc1_at_2 & cpc2_at_2].
prop aux1085 := [aux1066 => [x_at_2 <= 5]].
prop aux1086 := [aux1067 => [x_at_2 <= 5]].
prop aux1087 := [aux1068 => [x_at_2 <= 5]].
prop aux1088 := [aux1074 => [y_at_2 <= 1]].
prop aux1089 := [aux1076 => [y_at_2 <= 2]].
prop aux1090 := [aux1082 => [z_at_2 <= 1]].
prop aux1091 := [aux1084 => [z_at_2 <= 1]].
prop aux1092 := [[tpc1_at_2 <=> tpc1_at_1] & [tpc2_at_2 <=> tpc2_at_1]].
prop aux1093 := [aux1092 & [x_at_2 = (x_at_1 + d_at_1)]].
prop aux1094 := [[[[[[[[aux1061 & aux1066] & aux1053] & [x_at_2 = d_at_1]] | [[[[aux1062 & aux1067] & aux1054] & [x_at_1 > 2]] & [x_at_2 = (x_at_1 + d_at_1)]]] | [[[aux1063 & aux1068] & aux1055] & [x_at_2 = (x_at_1 + d_at_1)]]] | [[[aux1064 & aux1065] & aux1056] & [x_at_2 = (x_at_1 + d_at_1)]]] | [[[[aux1093 & [~ aux1053]] & [~ aux1054]] & [~ aux1055]] & [~ aux1056]]] & [[aux1085 & aux1086] & aux1087]].
prop aux1095 := [[gpc1_at_2 <=> gpc1_at_1] & [gpc2_at_2 <=> gpc2_at_1]].
prop aux1096 := [aux1095 & [y_at_2 = (y_at_1 + d_at_1)]].
prop aux1097 := [[[[[[[[aux1069 & aux1074] & aux1057] & [y_at_2 = d_at_1]] | [[[aux1070 & aux1075] & aux1058] & [y_at_2 = (y_at_1 + d_at_1)]]] | [[[aux1071 & aux1076] & aux1059] & [y_at_2 = d_at_1]]] | [[[[aux1072 & aux1073] & aux1060] & [y_at_1 >= 1]] & [y_at_2 = (y_at_1 + d_at_1)]]] | [[[[aux1096 & [~ aux1057]] & [~ aux1058]] & [~ aux1059]] & [~ aux1060]]] & [aux1088 & aux1089]].
prop aux1098 := [[cpc1_at_2 <=> cpc1_at_1] & [cpc2_at_2 <=> cpc2_at_1]].
prop aux1099 := [aux1098 & [z_at_2 = (z_at_1 + d_at_1)]].
prop aux1100 := [[[[[[[[aux1077 & aux1082] & aux1053] & [z_at_2 = d_at_1]] | [[[[aux1078 & aux1083] & aux1057] & [z_at_1 = 1]] & [z_at_2 = (z_at_1 + d_at_1)]]] | [[[aux1079 & aux1084] & aux1056] & [z_at_2 = d_at_1]]] | [[[aux1080 & aux1081] & aux1059] & [z_at_2 = (z_at_1 + d_at_1)]]] | [[[[aux1099 & [~ aux1053]] & [~ aux1057]] & [~ aux1056]] & [~ aux1059]]] & [aux1090 & aux1091]].
prop aux1101 := [d_at_1 >= 0].
prop aux1102 := [[[~ act1_at_2] & [~ act2_at_2]] & [~ act3_at_2]].
prop aux1103 := [[act1_at_2 & [~ act2_at_2]] & [~ act3_at_2]].
prop aux1104 := [[[~ act1_at_2] & act2_at_2] & [~ act3_at_2]].
prop aux1105 := [[act1_at_2 & act2_at_2] & [~ act3_at_2]].
prop aux1106 := [[[~ act1_at_2] & [~ act2_at_2]] & act3_at_2].
prop aux1107 := [[act1_at_2 & [~ act2_at_2]] & act3_at_2].
prop aux1108 := [[[~ act1_at_2] & act2_at_2] & act3_at_2].
prop aux1109 := [[act1_at_2 & act2_at_2] & act3_at_2].
prop aux1110 := [[~ tpc1_at_2] & [~ tpc2_at_2]].
prop aux1111 := [tpc1_at_2 & [~ tpc2_at_2]].
prop aux1112 := [[~ tpc1_at_2] & tpc2_at_2].
prop aux1113 := [tpc1_at_2 & tpc2_at_2].
prop aux1114 := [[~ tpc1_at_3] & [~ tpc2_at_3]].
prop aux1115 := [tpc1_at_3 & [~ tpc2_at_3]].
prop aux1116 := [[~ tpc1_at_3] & tpc2_at_3].
prop aux1117 := [tpc1_at_3 & tpc2_at_3].
prop aux1118 := [[~ gpc1_at_2] & [~ gpc2_at_2]].
prop aux1119 := [gpc1_at_2 & [~ gpc2_at_2]].
prop aux1120 := [[~ gpc1_at_2] & gpc2_at_2].
prop aux1121 := [gpc1_at_2 & gpc2_at_2].
prop aux1122 := [[~ gpc1_at_3] & [~ gpc2_at_3]].
prop aux1123 := [gpc1_at_3 & [~ gpc2_at_3]].
prop aux1124 := [[~ gpc1_at_3] & gpc2_at_3].
prop aux1125 := [gpc1_at_3 & gpc2_at_3].
prop aux1126 := [[~ cpc1_at_2] & [~ cpc2_at_2]].
prop aux1127 := [cpc1_at_2 & [~ cpc2_at_2]].
prop aux1128 := [[~ cpc1_at_2] & cpc2_at_2].
prop aux1129 := [cpc1_at_2 & cpc2_at_2].
prop aux1130 := [[~ cpc1_at_3] & [~ cpc2_at_3]].
prop aux1131 := [cpc1_at_3 & [~ cpc2_at_3]].
prop aux1132 := [[~ cpc1_at_3] & cpc2_at_3].
prop aux1133 := [cpc1_at_3 & cpc2_at_3].
prop aux1134 := [aux1115 => [x_at_3 <= 5]].
prop aux1135 := [aux1116 => [x_at_3 <= 5]].
prop aux1136 := [aux1117 => [x_at_3 <= 5]].
prop aux1137 := [aux1123 => [y_at_3 <= 1]].
prop aux1138 := [aux1125 => [y_at_3 <= 2]].
prop aux1139 := [aux1131 => [z_at_3 <= 1]].
prop aux1140 := [aux1133 => [z_at_3 <= 1]].
prop aux1141 := [[tpc1_at_3 <=> tpc1_at_2] & [tpc2_at_3 <=> tpc2_at_2]].
prop aux1142 := [aux1141 & [x_at_3 = (x_at_2 + d_at_2)]].
prop aux1143 := [[[[[[[[aux1110 & aux1115] & aux1102] & [x_at_3 = d_at_2]] | [[[[aux1111 & aux1116] & aux1103] & [x_at_2 > 2]] & [x_at_3 = (x_at_2 + d_at_2)]]] | [[[aux1112 & aux1117] & aux1104] & [x_at_3 = (x_at_2 + d_at_2)]]] | [[[aux1113 & aux1114] & aux1105] & [x_at_3 = (x_at_2 + d_at_2)]]] | [[[[aux1142 & [~ aux1102]] & [~ aux1103]] & [~ aux1104]] & [~ aux1105]]] & [[aux1134 & aux1135] & aux1136]].
prop aux1144 := [[gpc1_at_3 <=> gpc1_at_2] & [gpc2_at_3 <=> gpc2_at_2]].
prop aux1145 := [aux1144 & [y_at_3 = (y_at_2 + d_at_2)]].
prop aux1146 := [[[[[[[[aux1118 & aux1123] & aux1106] & [y_at_3 = d_at_2]] | [[[aux1119 & aux1124] & aux1107] & [y_at_3 = (y_at_2 + d_at_2)]]] | [[[aux1120 & aux1125] & aux1108] & [y_at_3 = d_at_2]]] | [[[[aux1121 & aux1122] & aux1109] & [y_at_2 >= 1]] & [y_at_3 = (y_at_2 + d_at_2)]]] | [[[[aux1145 & [~ aux1106]] & [~ aux1107]] & [~ aux1108]] & [~ aux1109]]] & [aux1137 & aux1138]].
prop aux1147 := [[cpc1_at_3 <=> cpc1_at_2] & [cpc2_at_3 <=> cpc2_at_2]].
prop aux1148 := [aux1147 & [z_at_3 = (z_at_2 + d_at_2)]].
prop aux1149 := [[[[[[[[aux1126 & aux1131] & aux1102] & [z_at_3 = d_at_2]] | [[[[aux1127 & aux1132] & aux1106] & [z_at_2 = 1]] & [z_at_3 = (z_at_2 + d_at_2)]]] | [[[aux1128 & aux1133] & aux1105] & [z_at_3 = d_at_2]]] | [[[aux1129 & aux1130] & aux1108] & [z_at_3 = (z_at_2 + d_at_2)]]] | [[[[aux1148 & [~ aux1102]] & [~ aux1106]] & [~ aux1105]] & [~ aux1108]]] & [aux1139 & aux1140]].
prop aux1150 := [d_at_2 >= 0].
prop aux1151 := [[[~ act1_at_3] & [~ act2_at_3]] & [~ act3_at_3]].
prop aux1152 := [[act1_at_3 & [~ act2_at_3]] & [~ act3_at_3]].
prop aux1153 := [[[~ act1_at_3] & act2_at_3] & [~ act3_at_3]].
prop aux1154 := [[act1_at_3 & act2_at_3] & [~ act3_at_3]].
prop aux1155 := [[[~ act1_at_3] & [~ act2_at_3]] & act3_at_3].
prop aux1156 := [[act1_at_3 & [~ act2_at_3]] & act3_at_3].
prop aux1157 := [[[~ act1_at_3] & act2_at_3] & act3_at_3].
prop aux1158 := [[act1_at_3 & act2_at_3] & act3_at_3].
prop aux1159 := [[~ tpc1_at_3] & [~ tpc2_at_3]].
prop aux1160 := [tpc1_at_3 & [~ tpc2_at_3]].
prop aux1161 := [[~ tpc1_at_3] & tpc2_at_3].
prop aux1162 := [tpc1_at_3 & tpc2_at_3].
prop aux1163 := [[~ tpc1_at_4] & [~ tpc2_at_4]].
prop aux1164 := [tpc1_at_4 & [~ tpc2_at_4]].
prop aux1165 := [[~ tpc1_at_4] & tpc2_at_4].
prop aux1166 := [tpc1_at_4 & tpc2_at_4].
prop aux1167 := [[~ gpc1_at_3] & [~ gpc2_at_3]].
prop aux1168 := [gpc1_at_3 & [~ gpc2_at_3]].
prop aux1169 := [[~ gpc1_at_3] & gpc2_at_3].
prop aux1170 := [gpc1_at_3 & gpc2_at_3].
prop aux1171 := [[~ gpc1_at_4] & [~ gpc2_at_4]].
prop aux1172 := [gpc1_at_4 & [~ gpc2_at_4]].
prop aux1173 := [[~ gpc1_at_4] & gpc2_at_4].
prop aux1174 := [gpc1_at_4 & gpc2_at_4].
prop aux1175 := [[~ cpc1_at_3] & [~ cpc2_at_3]].
prop aux1176 := [cpc1_at_3 & [~ cpc2_at_3]].
prop aux1177 := [[~ cpc1_at_3] & cpc2_at_3].
prop aux1178 := [cpc1_at_3 & cpc2_at_3].
prop aux1179 := [[~ cpc1_at_4] & [~ cpc2_at_4]].
prop aux1180 := [cpc1_at_4 & [~ cpc2_at_4]].
prop aux1181 := [[~ cpc1_at_4] & cpc2_at_4].
prop aux1182 := [cpc1_at_4 & cpc2_at_4].
prop aux1183 := [aux1164 => [x_at_4 <= 5]].
prop aux1184 := [aux1165 => [x_at_4 <= 5]].
prop aux1185 := [aux1166 => [x_at_4 <= 5]].
prop aux1186 := [aux1172 => [y_at_4 <= 1]].
prop aux1187 := [aux1174 => [y_at_4 <= 2]].
prop aux1188 := [aux1180 => [z_at_4 <= 1]].
prop aux1189 := [aux1182 => [z_at_4 <= 1]].
prop aux1190 := [[tpc1_at_4 <=> tpc1_at_3] & [tpc2_at_4 <=> tpc2_at_3]].
prop aux1191 := [aux1190 & [x_at_4 = (x_at_3 + d_at_3)]].
prop aux1192 := [[[[[[[[aux1159 & aux1164] & aux1151] & [x_at_4 = d_at_3]] | [[[[aux1160 & aux1165] & aux1152] & [x_at_3 > 2]] & [x_at_4 = (x_at_3 + d_at_3)]]] | [[[aux1161 & aux1166] & aux1153] & [x_at_4 = (x_at_3 + d_at_3)]]] | [[[aux1162 & aux1163] & aux1154] & [x_at_4 = (x_at_3 + d_at_3)]]] | [[[[aux1191 & [~ aux1151]] & [~ aux1152]] & [~ aux1153]] & [~ aux1154]]] & [[aux1183 & aux1184] & aux1185]].
prop aux1193 := [[gpc1_at_4 <=> gpc1_at_3] & [gpc2_at_4 <=> gpc2_at_3]].
prop aux1194 := [aux1193 & [y_at_4 = (y_at_3 + d_at_3)]].
prop aux1195 := [[[[[[[[aux1167 & aux1172] & aux1155] & [y_at_4 = d_at_3]] | [[[aux1168 & aux1173] & aux1156] & [y_at_4 = (y_at_3 + d_at_3)]]] | [[[aux1169 & aux1174] & aux1157] & [y_at_4 = d_at_3]]] | [[[[aux1170 & aux1171] & aux1158] & [y_at_3 >= 1]] & [y_at_4 = (y_at_3 + d_at_3)]]] | [[[[aux1194 & [~ aux1155]] & [~ aux1156]] & [~ aux1157]] & [~ aux1158]]] & [aux1186 & aux1187]].
prop aux1196 := [[cpc1_at_4 <=> cpc1_at_3] & [cpc2_at_4 <=> cpc2_at_3]].
prop aux1197 := [aux1196 & [z_at_4 = (z_at_3 + d_at_3)]].
prop aux1198 := [[[[[[[[aux1175 & aux1180] & aux1151] & [z_at_4 = d_at_3]] | [[[[aux1176 & aux1181] & aux1155] & [z_at_3 = 1]] & [z_at_4 = (z_at_3 + d_at_3)]]] | [[[aux1177 & aux1182] & aux1154] & [z_at_4 = d_at_3]]] | [[[aux1178 & aux1179] & aux1157] & [z_at_4 = (z_at_3 + d_at_3)]]] | [[[[aux1197 & [~ aux1151]] & [~ aux1155]] & [~ aux1154]] & [~ aux1157]]] & [aux1188 & aux1189]].
prop aux1199 := [d_at_3 >= 0].
prop aux1200 := [[[~ act1_at_4] & [~ act2_at_4]] & [~ act3_at_4]].
prop aux1201 := [[act1_at_4 & [~ act2_at_4]] & [~ act3_at_4]].
prop aux1202 := [[[~ act1_at_4] & act2_at_4] & [~ act3_at_4]].
prop aux1203 := [[act1_at_4 & act2_at_4] & [~ act3_at_4]].
prop aux1204 := [[[~ act1_at_4] & [~ act2_at_4]] & act3_at_4].
prop aux1205 := [[act1_at_4 & [~ act2_at_4]] & act3_at_4].
prop aux1206 := [[[~ act1_at_4] & act2_at_4] & act3_at_4].
prop aux1207 := [[act1_at_4 & act2_at_4] & act3_at_4].
prop aux1208 := [[~ tpc1_at_4] & [~ tpc2_at_4]].
prop aux1209 := [tpc1_at_4 & [~ tpc2_at_4]].
prop aux1210 := [[~ tpc1_at_4] & tpc2_at_4].
prop aux1211 := [tpc1_at_4 & tpc2_at_4].
prop aux1212 := [[~ tpc1_at_5] & [~ tpc2_at_5]].
prop aux1213 := [tpc1_at_5 & [~ tpc2_at_5]].
prop aux1214 := [[~ tpc1_at_5] & tpc2_at_5].
prop aux1215 := [tpc1_at_5 & tpc2_at_5].
prop aux1216 := [[~ gpc1_at_4] & [~ gpc2_at_4]].
prop aux1217 := [gpc1_at_4 & [~ gpc2_at_4]].
prop aux1218 := [[~ gpc1_at_4] & gpc2_at_4].
prop aux1219 := [gpc1_at_4 & gpc2_at_4].
prop aux1220 := [[~ gpc1_at_5] & [~ gpc2_at_5]].
prop aux1221 := [gpc1_at_5 & [~ gpc2_at_5]].
prop aux1222 := [[~ gpc1_at_5] & gpc2_at_5].
prop aux1223 := [gpc1_at_5 & gpc2_at_5].
prop aux1224 := [[~ cpc1_at_4] & [~ cpc2_at_4]].
prop aux1225 := [cpc1_at_4 & [~ cpc2_at_4]].
prop aux1226 := [[~ cpc1_at_4] & cpc2_at_4].
prop aux1227 := [cpc1_at_4 & cpc2_at_4].
prop aux1228 := [[~ cpc1_at_5] & [~ cpc2_at_5]].
prop aux1229 := [cpc1_at_5 & [~ cpc2_at_5]].
prop aux1230 := [[~ cpc1_at_5] & cpc2_at_5].
prop aux1231 := [cpc1_at_5 & cpc2_at_5].
prop aux1232 := [aux1213 => [x_at_5 <= 5]].
prop aux1233 := [aux1214 => [x_at_5 <= 5]].
prop aux1234 := [aux1215 => [x_at_5 <= 5]].
prop aux1235 := [aux1221 => [y_at_5 <= 1]].
prop aux1236 := [aux1223 => [y_at_5 <= 2]].
prop aux1237 := [aux1229 => [z_at_5 <= 1]].
prop aux1238 := [aux1231 => [z_at_5 <= 1]].
prop aux1239 := [[tpc1_at_5 <=> tpc1_at_4] & [tpc2_at_5 <=> tpc2_at_4]].
prop aux1240 := [aux1239 & [x_at_5 = (x_at_4 + d_at_4)]].
prop aux1241 := [[[[[[[[aux1208 & aux1213] & aux1200] & [x_at_5 = d_at_4]] | [[[[aux1209 & aux1214] & aux1201] & [x_at_4 > 2]] & [x_at_5 = (x_at_4 + d_at_4)]]] | [[[aux1210 & aux1215] & aux1202] & [x_at_5 = (x_at_4 + d_at_4)]]] | [[[aux1211 & aux1212] & aux1203] & [x_at_5 = (x_at_4 + d_at_4)]]] | [[[[aux1240 & [~ aux1200]] & [~ aux1201]] & [~ aux1202]] & [~ aux1203]]] & [[aux1232 & aux1233] & aux1234]].
prop aux1242 := [[gpc1_at_5 <=> gpc1_at_4] & [gpc2_at_5 <=> gpc2_at_4]].
prop aux1243 := [aux1242 & [y_at_5 = (y_at_4 + d_at_4)]].
prop aux1244 := [[[[[[[[aux1216 & aux1221] & aux1204] & [y_at_5 = d_at_4]] | [[[aux1217 & aux1222] & aux1205] & [y_at_5 = (y_at_4 + d_at_4)]]] | [[[aux1218 & aux1223] & aux1206] & [y_at_5 = d_at_4]]] | [[[[aux1219 & aux1220] & aux1207] & [y_at_4 >= 1]] & [y_at_5 = (y_at_4 + d_at_4)]]] | [[[[aux1243 & [~ aux1204]] & [~ aux1205]] & [~ aux1206]] & [~ aux1207]]] & [aux1235 & aux1236]].
prop aux1245 := [[cpc1_at_5 <=> cpc1_at_4] & [cpc2_at_5 <=> cpc2_at_4]].
prop aux1246 := [aux1245 & [z_at_5 = (z_at_4 + d_at_4)]].
prop aux1247 := [[[[[[[[aux1224 & aux1229] & aux1200] & [z_at_5 = d_at_4]] | [[[[aux1225 & aux1230] & aux1204] & [z_at_4 = 1]] & [z_at_5 = (z_at_4 + d_at_4)]]] | [[[aux1226 & aux1231] & aux1203] & [z_at_5 = d_at_4]]] | [[[aux1227 & aux1228] & aux1206] & [z_at_5 = (z_at_4 + d_at_4)]]] | [[[[aux1246 & [~ aux1200]] & [~ aux1204]] & [~ aux1203]] & [~ aux1206]]] & [aux1237 & aux1238]].
prop aux1248 := [d_at_4 >= 0].
prop aux1249 := [[[~ act1_at_5] & [~ act2_at_5]] & [~ act3_at_5]].
prop aux1250 := [[act1_at_5 & [~ act2_at_5]] & [~ act3_at_5]].
prop aux1251 := [[[~ act1_at_5] & act2_at_5] & [~ act3_at_5]].
prop aux1252 := [[act1_at_5 & act2_at_5] & [~ act3_at_5]].
prop aux1253 := [[[~ act1_at_5] & [~ act2_at_5]] & act3_at_5].
prop aux1254 := [[act1_at_5 & [~ act2_at_5]] & act3_at_5].
prop aux1255 := [[[~ act1_at_5] & act2_at_5] & act3_at_5].
prop aux1256 := [[act1_at_5 & act2_at_5] & act3_at_5].
prop aux1257 := [[~ tpc1_at_5] & [~ tpc2_at_5]].
prop aux1258 := [tpc1_at_5 & [~ tpc2_at_5]].
prop aux1259 := [[~ tpc1_at_5] & tpc2_at_5].
prop aux1260 := [tpc1_at_5 & tpc2_at_5].
prop aux1261 := [[~ tpc1_at_6] & [~ tpc2_at_6]].
prop aux1262 := [tpc1_at_6 & [~ tpc2_at_6]].
prop aux1263 := [[~ tpc1_at_6] & tpc2_at_6].
prop aux1264 := [tpc1_at_6 & tpc2_at_6].
prop aux1265 := [[~ gpc1_at_5] & [~ gpc2_at_5]].
prop aux1266 := [gpc1_at_5 & [~ gpc2_at_5]].
prop aux1267 := [[~ gpc1_at_5] & gpc2_at_5].
prop aux1268 := [gpc1_at_5 & gpc2_at_5].
prop aux1269 := [[~ gpc1_at_6] & [~ gpc2_at_6]].
prop aux1270 := [gpc1_at_6 & [~ gpc2_at_6]].
prop aux1271 := [[~ gpc1_at_6] & gpc2_at_6].
prop aux1272 := [gpc1_at_6 & gpc2_at_6].
prop aux1273 := [[~ cpc1_at_5] & [~ cpc2_at_5]].
prop aux1274 := [cpc1_at_5 & [~ cpc2_at_5]].
prop aux1275 := [[~ cpc1_at_5] & cpc2_at_5].
prop aux1276 := [cpc1_at_5 & cpc2_at_5].
prop aux1277 := [[~ cpc1_at_6] & [~ cpc2_at_6]].
prop aux1278 := [cpc1_at_6 & [~ cpc2_at_6]].
prop aux1279 := [[~ cpc1_at_6] & cpc2_at_6].
prop aux1280 := [cpc1_at_6 & cpc2_at_6].
prop aux1281 := [aux1262 => [x_at_6 <= 5]].
prop aux1282 := [aux1263 => [x_at_6 <= 5]].
prop aux1283 := [aux1264 => [x_at_6 <= 5]].
prop aux1284 := [aux1270 => [y_at_6 <= 1]].
prop aux1285 := [aux1272 => [y_at_6 <= 2]].
prop aux1286 := [aux1278 => [z_at_6 <= 1]].
prop aux1287 := [aux1280 => [z_at_6 <= 1]].
prop aux1288 := [[tpc1_at_6 <=> tpc1_at_5] & [tpc2_at_6 <=> tpc2_at_5]].
prop aux1289 := [aux1288 & [x_at_6 = (x_at_5 + d_at_5)]].
prop aux1290 := [[[[[[[[aux1257 & aux1262] & aux1249] & [x_at_6 = d_at_5]] | [[[[aux1258 & aux1263] & aux1250] & [x_at_5 > 2]] & [x_at_6 = (x_at_5 + d_at_5)]]] | [[[aux1259 & aux1264] & aux1251] & [x_at_6 = (x_at_5 + d_at_5)]]] | [[[aux1260 & aux1261] & aux1252] & [x_at_6 = (x_at_5 + d_at_5)]]] | [[[[aux1289 & [~ aux1249]] & [~ aux1250]] & [~ aux1251]] & [~ aux1252]]] & [[aux1281 & aux1282] & aux1283]].
prop aux1291 := [[gpc1_at_6 <=> gpc1_at_5] & [gpc2_at_6 <=> gpc2_at_5]].
prop aux1292 := [aux1291 & [y_at_6 = (y_at_5 + d_at_5)]].
prop aux1293 := [[[[[[[[aux1265 & aux1270] & aux1253] & [y_at_6 = d_at_5]] | [[[aux1266 & aux1271] & aux1254] & [y_at_6 = (y_at_5 + d_at_5)]]] | [[[aux1267 & aux1272] & aux1255] & [y_at_6 = d_at_5]]] | [[[[aux1268 & aux1269] & aux1256] & [y_at_5 >= 1]] & [y_at_6 = (y_at_5 + d_at_5)]]] | [[[[aux1292 & [~ aux1253]] & [~ aux1254]] & [~ aux1255]] & [~ aux1256]]] & [aux1284 & aux1285]].
prop aux1294 := [[cpc1_at_6 <=> cpc1_at_5] & [cpc2_at_6 <=> cpc2_at_5]].
prop aux1295 := [aux1294 & [z_at_6 = (z_at_5 + d_at_5)]].
prop aux1296 := [[[[[[[[aux1273 & aux1278] & aux1249] & [z_at_6 = d_at_5]] | [[[[aux1274 & aux1279] & aux1253] & [z_at_5 = 1]] & [z_at_6 = (z_at_5 + d_at_5)]]] | [[[aux1275 & aux1280] & aux1252] & [z_at_6 = d_at_5]]] | [[[aux1276 & aux1277] & aux1255] & [z_at_6 = (z_at_5 + d_at_5)]]] | [[[[aux1295 & [~ aux1249]] & [~ aux1253]] & [~ aux1252]] & [~ aux1255]]] & [aux1286 & aux1287]].
prop aux1297 := [d_at_5 >= 0].
prop aux1298 := [[[~ act1_at_6] & [~ act2_at_6]] & [~ act3_at_6]].
prop aux1299 := [[act1_at_6 & [~ act2_at_6]] & [~ act3_at_6]].
prop aux1300 := [[[~ act1_at_6] & act2_at_6] & [~ act3_at_6]].
prop aux1301 := [[act1_at_6 & act2_at_6] & [~ act3_at_6]].
prop aux1302 := [[[~ act1_at_6] & [~ act2_at_6]] & act3_at_6].
prop aux1303 := [[act1_at_6 & [~ act2_at_6]] & act3_at_6].
prop aux1304 := [[[~ act1_at_6] & act2_at_6] & act3_at_6].
prop aux1305 := [[act1_at_6 & act2_at_6] & act3_at_6].
prop aux1306 := [[~ tpc1_at_6] & [~ tpc2_at_6]].
prop aux1307 := [tpc1_at_6 & [~ tpc2_at_6]].
prop aux1308 := [[~ tpc1_at_6] & tpc2_at_6].
prop aux1309 := [tpc1_at_6 & tpc2_at_6].
prop aux1310 := [[~ tpc1_at_7] & [~ tpc2_at_7]].
prop aux1311 := [tpc1_at_7 & [~ tpc2_at_7]].
prop aux1312 := [[~ tpc1_at_7] & tpc2_at_7].
prop aux1313 := [tpc1_at_7 & tpc2_at_7].
prop aux1314 := [[~ gpc1_at_6] & [~ gpc2_at_6]].
prop aux1315 := [gpc1_at_6 & [~ gpc2_at_6]].
prop aux1316 := [[~ gpc1_at_6] & gpc2_at_6].
prop aux1317 := [gpc1_at_6 & gpc2_at_6].
prop aux1318 := [[~ gpc1_at_7] & [~ gpc2_at_7]].
prop aux1319 := [gpc1_at_7 & [~ gpc2_at_7]].
prop aux1320 := [[~ gpc1_at_7] & gpc2_at_7].
prop aux1321 := [gpc1_at_7 & gpc2_at_7].
prop aux1322 := [[~ cpc1_at_6] & [~ cpc2_at_6]].
prop aux1323 := [cpc1_at_6 & [~ cpc2_at_6]].
prop aux1324 := [[~ cpc1_at_6] & cpc2_at_6].
prop aux1325 := [cpc1_at_6 & cpc2_at_6].
prop aux1326 := [[~ cpc1_at_7] & [~ cpc2_at_7]].
prop aux1327 := [cpc1_at_7 & [~ cpc2_at_7]].
prop aux1328 := [[~ cpc1_at_7] & cpc2_at_7].
prop aux1329 := [cpc1_at_7 & cpc2_at_7].
prop aux1330 := [aux1311 => [x_at_7 <= 5]].
prop aux1331 := [aux1312 => [x_at_7 <= 5]].
prop aux1332 := [aux1313 => [x_at_7 <= 5]].
prop aux1333 := [aux1319 => [y_at_7 <= 1]].
prop aux1334 := [aux1321 => [y_at_7 <= 2]].
prop aux1335 := [aux1327 => [z_at_7 <= 1]].
prop aux1336 := [aux1329 => [z_at_7 <= 1]].
prop aux1337 := [[tpc1_at_7 <=> tpc1_at_6] & [tpc2_at_7 <=> tpc2_at_6]].
prop aux1338 := [aux1337 & [x_at_7 = (x_at_6 + d_at_6)]].
prop aux1339 := [[[[[[[[aux1306 & aux1311] & aux1298] & [x_at_7 = d_at_6]] | [[[[aux1307 & aux1312] & aux1299] & [x_at_6 > 2]] & [x_at_7 = (x_at_6 + d_at_6)]]] | [[[aux1308 & aux1313] & aux1300] & [x_at_7 = (x_at_6 + d_at_6)]]] | [[[aux1309 & aux1310] & aux1301] & [x_at_7 = (x_at_6 + d_at_6)]]] | [[[[aux1338 & [~ aux1298]] & [~ aux1299]] & [~ aux1300]] & [~ aux1301]]] & [[aux1330 & aux1331] & aux1332]].
prop aux1340 := [[gpc1_at_7 <=> gpc1_at_6] & [gpc2_at_7 <=> gpc2_at_6]].
prop aux1341 := [aux1340 & [y_at_7 = (y_at_6 + d_at_6)]].
prop aux1342 := [[[[[[[[aux1314 & aux1319] & aux1302] & [y_at_7 = d_at_6]] | [[[aux1315 & aux1320] & aux1303] & [y_at_7 = (y_at_6 + d_at_6)]]] | [[[aux1316 & aux1321] & aux1304] & [y_at_7 = d_at_6]]] | [[[[aux1317 & aux1318] & aux1305] & [y_at_6 >= 1]] & [y_at_7 = (y_at_6 + d_at_6)]]] | [[[[aux1341 & [~ aux1302]] & [~ aux1303]] & [~ aux1304]] & [~ aux1305]]] & [aux1333 & aux1334]].
prop aux1343 := [[cpc1_at_7 <=> cpc1_at_6] & [cpc2_at_7 <=> cpc2_at_6]].
prop aux1344 := [aux1343 & [z_at_7 = (z_at_6 + d_at_6)]].
prop aux1345 := [[[[[[[[aux1322 & aux1327] & aux1298] & [z_at_7 = d_at_6]] | [[[[aux1323 & aux1328] & aux1302] & [z_at_6 = 1]] & [z_at_7 = (z_at_6 + d_at_6)]]] | [[[aux1324 & aux1329] & aux1301] & [z_at_7 = d_at_6]]] | [[[aux1325 & aux1326] & aux1304] & [z_at_7 = (z_at_6 + d_at_6)]]] | [[[[aux1344 & [~ aux1298]] & [~ aux1302]] & [~ aux1301]] & [~ aux1304]]] & [aux1335 & aux1336]].
prop aux1346 := [d_at_6 >= 0].
prop aux1347 := [[[~ act1_at_7] & [~ act2_at_7]] & [~ act3_at_7]].
prop aux1348 := [[act1_at_7 & [~ act2_at_7]] & [~ act3_at_7]].
prop aux1349 := [[[~ act1_at_7] & act2_at_7] & [~ act3_at_7]].
prop aux1350 := [[act1_at_7 & act2_at_7] & [~ act3_at_7]].
prop aux1351 := [[[~ act1_at_7] & [~ act2_at_7]] & act3_at_7].
prop aux1352 := [[act1_at_7 & [~ act2_at_7]] & act3_at_7].
prop aux1353 := [[[~ act1_at_7] & act2_at_7] & act3_at_7].
prop aux1354 := [[act1_at_7 & act2_at_7] & act3_at_7].
prop aux1355 := [[~ tpc1_at_7] & [~ tpc2_at_7]].
prop aux1356 := [tpc1_at_7 & [~ tpc2_at_7]].
prop aux1357 := [[~ tpc1_at_7] & tpc2_at_7].
prop aux1358 := [tpc1_at_7 & tpc2_at_7].
prop aux1359 := [[~ tpc1_at_8] & [~ tpc2_at_8]].
prop aux1360 := [tpc1_at_8 & [~ tpc2_at_8]].
prop aux1361 := [[~ tpc1_at_8] & tpc2_at_8].
prop aux1362 := [tpc1_at_8 & tpc2_at_8].
prop aux1363 := [[~ gpc1_at_7] & [~ gpc2_at_7]].
prop aux1364 := [gpc1_at_7 & [~ gpc2_at_7]].
prop aux1365 := [[~ gpc1_at_7] & gpc2_at_7].
prop aux1366 := [gpc1_at_7 & gpc2_at_7].
prop aux1367 := [[~ gpc1_at_8] & [~ gpc2_at_8]].
prop aux1368 := [gpc1_at_8 & [~ gpc2_at_8]].
prop aux1369 := [[~ gpc1_at_8] & gpc2_at_8].
prop aux1370 := [gpc1_at_8 & gpc2_at_8].
prop aux1371 := [[~ cpc1_at_7] & [~ cpc2_at_7]].
prop aux1372 := [cpc1_at_7 & [~ cpc2_at_7]].
prop aux1373 := [[~ cpc1_at_7] & cpc2_at_7].
prop aux1374 := [cpc1_at_7 & cpc2_at_7].
prop aux1375 := [[~ cpc1_at_8] & [~ cpc2_at_8]].
prop aux1376 := [cpc1_at_8 & [~ cpc2_at_8]].
prop aux1377 := [[~ cpc1_at_8] & cpc2_at_8].
prop aux1378 := [cpc1_at_8 & cpc2_at_8].
prop aux1379 := [aux1360 => [x_at_8 <= 5]].
prop aux1380 := [aux1361 => [x_at_8 <= 5]].
prop aux1381 := [aux1362 => [x_at_8 <= 5]].
prop aux1382 := [aux1368 => [y_at_8 <= 1]].
prop aux1383 := [aux1370 => [y_at_8 <= 2]].
prop aux1384 := [aux1376 => [z_at_8 <= 1]].
prop aux1385 := [aux1378 => [z_at_8 <= 1]].
prop aux1386 := [[tpc1_at_8 <=> tpc1_at_7] & [tpc2_at_8 <=> tpc2_at_7]].
prop aux1387 := [aux1386 & [x_at_8 = (x_at_7 + d_at_7)]].
prop aux1388 := [[[[[[[[aux1355 & aux1360] & aux1347] & [x_at_8 = d_at_7]] | [[[[aux1356 & aux1361] & aux1348] & [x_at_7 > 2]] & [x_at_8 = (x_at_7 + d_at_7)]]] | [[[aux1357 & aux1362] & aux1349] & [x_at_8 = (x_at_7 + d_at_7)]]] | [[[aux1358 & aux1359] & aux1350] & [x_at_8 = (x_at_7 + d_at_7)]]] | [[[[aux1387 & [~ aux1347]] & [~ aux1348]] & [~ aux1349]] & [~ aux1350]]] & [[aux1379 & aux1380] & aux1381]].
prop aux1389 := [[gpc1_at_8 <=> gpc1_at_7] & [gpc2_at_8 <=> gpc2_at_7]].
prop aux1390 := [aux1389 & [y_at_8 = (y_at_7 + d_at_7)]].
prop aux1391 := [[[[[[[[aux1363 & aux1368] & aux1351] & [y_at_8 = d_at_7]] | [[[aux1364 & aux1369] & aux1352] & [y_at_8 = (y_at_7 + d_at_7)]]] | [[[aux1365 & aux1370] & aux1353] & [y_at_8 = d_at_7]]] | [[[[aux1366 & aux1367] & aux1354] & [y_at_7 >= 1]] & [y_at_8 = (y_at_7 + d_at_7)]]] | [[[[aux1390 & [~ aux1351]] & [~ aux1352]] & [~ aux1353]] & [~ aux1354]]] & [aux1382 & aux1383]].
prop aux1392 := [[cpc1_at_8 <=> cpc1_at_7] & [cpc2_at_8 <=> cpc2_at_7]].
prop aux1393 := [aux1392 & [z_at_8 = (z_at_7 + d_at_7)]].
prop aux1394 := [[[[[[[[aux1371 & aux1376] & aux1347] & [z_at_8 = d_at_7]] | [[[[aux1372 & aux1377] & aux1351] & [z_at_7 = 1]] & [z_at_8 = (z_at_7 + d_at_7)]]] | [[[aux1373 & aux1378] & aux1350] & [z_at_8 = d_at_7]]] | [[[aux1374 & aux1375] & aux1353] & [z_at_8 = (z_at_7 + d_at_7)]]] | [[[[aux1393 & [~ aux1347]] & [~ aux1351]] & [~ aux1350]] & [~ aux1353]]] & [aux1384 & aux1385]].
prop aux1395 := [d_at_7 >= 0].
prop aux1396 := [[[~ act1_at_8] & [~ act2_at_8]] & [~ act3_at_8]].
prop aux1397 := [[act1_at_8 & [~ act2_at_8]] & [~ act3_at_8]].
prop aux1398 := [[[~ act1_at_8] & act2_at_8] & [~ act3_at_8]].
prop aux1399 := [[act1_at_8 & act2_at_8] & [~ act3_at_8]].
prop aux1400 := [[[~ act1_at_8] & [~ act2_at_8]] & act3_at_8].
prop aux1401 := [[act1_at_8 & [~ act2_at_8]] & act3_at_8].
prop aux1402 := [[[~ act1_at_8] & act2_at_8] & act3_at_8].
prop aux1403 := [[act1_at_8 & act2_at_8] & act3_at_8].
prop aux1404 := [[~ tpc1_at_8] & [~ tpc2_at_8]].
prop aux1405 := [tpc1_at_8 & [~ tpc2_at_8]].
prop aux1406 := [[~ tpc1_at_8] & tpc2_at_8].
prop aux1407 := [tpc1_at_8 & tpc2_at_8].
prop aux1408 := [[~ tpc1_at_9] & [~ tpc2_at_9]].
prop aux1409 := [tpc1_at_9 & [~ tpc2_at_9]].
prop aux1410 := [[~ tpc1_at_9] & tpc2_at_9].
prop aux1411 := [tpc1_at_9 & tpc2_at_9].
prop aux1412 := [[~ gpc1_at_8] & [~ gpc2_at_8]].
prop aux1413 := [gpc1_at_8 & [~ gpc2_at_8]].
prop aux1414 := [[~ gpc1_at_8] & gpc2_at_8].
prop aux1415 := [gpc1_at_8 & gpc2_at_8].
prop aux1416 := [[~ gpc1_at_9] & [~ gpc2_at_9]].
prop aux1417 := [gpc1_at_9 & [~ gpc2_at_9]].
prop aux1418 := [[~ gpc1_at_9] & gpc2_at_9].
prop aux1419 := [gpc1_at_9 & gpc2_at_9].
prop aux1420 := [[~ cpc1_at_8] & [~ cpc2_at_8]].
prop aux1421 := [cpc1_at_8 & [~ cpc2_at_8]].
prop aux1422 := [[~ cpc1_at_8] & cpc2_at_8].
prop aux1423 := [cpc1_at_8 & cpc2_at_8].
prop aux1424 := [[~ cpc1_at_9] & [~ cpc2_at_9]].
prop aux1425 := [cpc1_at_9 & [~ cpc2_at_9]].
prop aux1426 := [[~ cpc1_at_9] & cpc2_at_9].
prop aux1427 := [cpc1_at_9 & cpc2_at_9].
prop aux1428 := [aux1409 => [x_at_9 <= 5]].
prop aux1429 := [aux1410 => [x_at_9 <= 5]].
prop aux1430 := [aux1411 => [x_at_9 <= 5]].
prop aux1431 := [aux1417 => [y_at_9 <= 1]].
prop aux1432 := [aux1419 => [y_at_9 <= 2]].
prop aux1433 := [aux1425 => [z_at_9 <= 1]].
prop aux1434 := [aux1427 => [z_at_9 <= 1]].
prop aux1435 := [[tpc1_at_9 <=> tpc1_at_8] & [tpc2_at_9 <=> tpc2_at_8]].
prop aux1436 := [aux1435 & [x_at_9 = (x_at_8 + d_at_8)]].
prop aux1437 := [[[[[[[[aux1404 & aux1409] & aux1396] & [x_at_9 = d_at_8]] | [[[[aux1405 & aux1410] & aux1397] & [x_at_8 > 2]] & [x_at_9 = (x_at_8 + d_at_8)]]] | [[[aux1406 & aux1411] & aux1398] & [x_at_9 = (x_at_8 + d_at_8)]]] | [[[aux1407 & aux1408] & aux1399] & [x_at_9 = (x_at_8 + d_at_8)]]] | [[[[aux1436 & [~ aux1396]] & [~ aux1397]] & [~ aux1398]] & [~ aux1399]]] & [[aux1428 & aux1429] & aux1430]].
prop aux1438 := [[gpc1_at_9 <=> gpc1_at_8] & [gpc2_at_9 <=> gpc2_at_8]].
prop aux1439 := [aux1438 & [y_at_9 = (y_at_8 + d_at_8)]].
prop aux1440 := [[[[[[[[aux1412 & aux1417] & aux1400] & [y_at_9 = d_at_8]] | [[[aux1413 & aux1418] & aux1401] & [y_at_9 = (y_at_8 + d_at_8)]]] | [[[aux1414 & aux1419] & aux1402] & [y_at_9 = d_at_8]]] | [[[[aux1415 & aux1416] & aux1403] & [y_at_8 >= 1]] & [y_at_9 = (y_at_8 + d_at_8)]]] | [[[[aux1439 & [~ aux1400]] & [~ aux1401]] & [~ aux1402]] & [~ aux1403]]] & [aux1431 & aux1432]].
prop aux1441 := [[cpc1_at_9 <=> cpc1_at_8] & [cpc2_at_9 <=> cpc2_at_8]].
prop aux1442 := [aux1441 & [z_at_9 = (z_at_8 + d_at_8)]].
prop aux1443 := [[[[[[[[aux1420 & aux1425] & aux1396] & [z_at_9 = d_at_8]] | [[[[aux1421 & aux1426] & aux1400] & [z_at_8 = 1]] & [z_at_9 = (z_at_8 + d_at_8)]]] | [[[aux1422 & aux1427] & aux1399] & [z_at_9 = d_at_8]]] | [[[aux1423 & aux1424] & aux1402] & [z_at_9 = (z_at_8 + d_at_8)]]] | [[[[aux1442 & [~ aux1396]] & [~ aux1400]] & [~ aux1399]] & [~ aux1402]]] & [aux1433 & aux1434]].
prop aux1444 := [d_at_8 >= 0].
prop aux1445 := [[[~ act1_at_9] & [~ act2_at_9]] & [~ act3_at_9]].
prop aux1446 := [[act1_at_9 & [~ act2_at_9]] & [~ act3_at_9]].
prop aux1447 := [[[~ act1_at_9] & act2_at_9] & [~ act3_at_9]].
prop aux1448 := [[act1_at_9 & act2_at_9] & [~ act3_at_9]].
prop aux1449 := [[[~ act1_at_9] & [~ act2_at_9]] & act3_at_9].
prop aux1450 := [[act1_at_9 & [~ act2_at_9]] & act3_at_9].
prop aux1451 := [[[~ act1_at_9] & act2_at_9] & act3_at_9].
prop aux1452 := [[act1_at_9 & act2_at_9] & act3_at_9].
prop aux1453 := [[~ tpc1_at_9] & [~ tpc2_at_9]].
prop aux1454 := [tpc1_at_9 & [~ tpc2_at_9]].
prop aux1455 := [[~ tpc1_at_9] & tpc2_at_9].
prop aux1456 := [tpc1_at_9 & tpc2_at_9].
prop aux1457 := [[~ tpc1_at_10] & [~ tpc2_at_10]].
prop aux1458 := [tpc1_at_10 & [~ tpc2_at_10]].
prop aux1459 := [[~ tpc1_at_10] & tpc2_at_10].
prop aux1460 := [tpc1_at_10 & tpc2_at_10].
prop aux1461 := [[~ gpc1_at_9] & [~ gpc2_at_9]].
prop aux1462 := [gpc1_at_9 & [~ gpc2_at_9]].
prop aux1463 := [[~ gpc1_at_9] & gpc2_at_9].
prop aux1464 := [gpc1_at_9 & gpc2_at_9].
prop aux1465 := [[~ gpc1_at_10] & [~ gpc2_at_10]].
prop aux1466 := [gpc1_at_10 & [~ gpc2_at_10]].
prop aux1467 := [[~ gpc1_at_10] & gpc2_at_10].
prop aux1468 := [gpc1_at_10 & gpc2_at_10].
prop aux1469 := [[~ cpc1_at_9] & [~ cpc2_at_9]].
prop aux1470 := [cpc1_at_9 & [~ cpc2_at_9]].
prop aux1471 := [[~ cpc1_at_9] & cpc2_at_9].
prop aux1472 := [cpc1_at_9 & cpc2_at_9].
prop aux1473 := [[~ cpc1_at_10] & [~ cpc2_at_10]].
prop aux1474 := [cpc1_at_10 & [~ cpc2_at_10]].
prop aux1475 := [[~ cpc1_at_10] & cpc2_at_10].
prop aux1476 := [cpc1_at_10 & cpc2_at_10].
prop aux1477 := [aux1458 => [x_at_10 <= 5]].
prop aux1478 := [aux1459 => [x_at_10 <= 5]].
prop aux1479 := [aux1460 => [x_at_10 <= 5]].
prop aux1480 := [aux1466 => [y_at_10 <= 1]].
prop aux1481 := [aux1468 => [y_at_10 <= 2]].
prop aux1482 := [aux1474 => [z_at_10 <= 1]].
prop aux1483 := [aux1476 => [z_at_10 <= 1]].
prop aux1484 := [[tpc1_at_10 <=> tpc1_at_9] & [tpc2_at_10 <=> tpc2_at_9]].
prop aux1485 := [aux1484 & [x_at_10 = (x_at_9 + d_at_9)]].
prop aux1486 := [[[[[[[[aux1453 & aux1458] & aux1445] & [x_at_10 = d_at_9]] | [[[[aux1454 & aux1459] & aux1446] & [x_at_9 > 2]] & [x_at_10 = (x_at_9 + d_at_9)]]] | [[[aux1455 & aux1460] & aux1447] & [x_at_10 = (x_at_9 + d_at_9)]]] | [[[aux1456 & aux1457] & aux1448] & [x_at_10 = (x_at_9 + d_at_9)]]] | [[[[aux1485 & [~ aux1445]] & [~ aux1446]] & [~ aux1447]] & [~ aux1448]]] & [[aux1477 & aux1478] & aux1479]].
prop aux1487 := [[gpc1_at_10 <=> gpc1_at_9] & [gpc2_at_10 <=> gpc2_at_9]].
prop aux1488 := [aux1487 & [y_at_10 = (y_at_9 + d_at_9)]].
prop aux1489 := [[[[[[[[aux1461 & aux1466] & aux1449] & [y_at_10 = d_at_9]] | [[[aux1462 & aux1467] & aux1450] & [y_at_10 = (y_at_9 + d_at_9)]]] | [[[aux1463 & aux1468] & aux1451] & [y_at_10 = d_at_9]]] | [[[[aux1464 & aux1465] & aux1452] & [y_at_9 >= 1]] & [y_at_10 = (y_at_9 + d_at_9)]]] | [[[[aux1488 & [~ aux1449]] & [~ aux1450]] & [~ aux1451]] & [~ aux1452]]] & [aux1480 & aux1481]].
prop aux1490 := [[cpc1_at_10 <=> cpc1_at_9] & [cpc2_at_10 <=> cpc2_at_9]].
prop aux1491 := [aux1490 & [z_at_10 = (z_at_9 + d_at_9)]].
prop aux1492 := [[[[[[[[aux1469 & aux1474] & aux1445] & [z_at_10 = d_at_9]] | [[[[aux1470 & aux1475] & aux1449] & [z_at_9 = 1]] & [z_at_10 = (z_at_9 + d_at_9)]]] | [[[aux1471 & aux1476] & aux1448] & [z_at_10 = d_at_9]]] | [[[aux1472 & aux1473] & aux1451] & [z_at_10 = (z_at_9 + d_at_9)]]] | [[[[aux1491 & [~ aux1445]] & [~ aux1449]] & [~ aux1448]] & [~ aux1451]]] & [aux1482 & aux1483]].
prop aux1493 := [d_at_9 >= 0].
prop aux1494 := [[[~ act1_at_10] & [~ act2_at_10]] & [~ act3_at_10]].
prop aux1495 := [[act1_at_10 & [~ act2_at_10]] & [~ act3_at_10]].
prop aux1496 := [[[~ act1_at_10] & act2_at_10] & [~ act3_at_10]].
prop aux1497 := [[act1_at_10 & act2_at_10] & [~ act3_at_10]].
prop aux1498 := [[[~ act1_at_10] & [~ act2_at_10]] & act3_at_10].
prop aux1499 := [[act1_at_10 & [~ act2_at_10]] & act3_at_10].
prop aux1500 := [[[~ act1_at_10] & act2_at_10] & act3_at_10].
prop aux1501 := [[act1_at_10 & act2_at_10] & act3_at_10].
prop aux1502 := [[~ tpc1_at_10] & [~ tpc2_at_10]].
prop aux1503 := [tpc1_at_10 & [~ tpc2_at_10]].
prop aux1504 := [[~ tpc1_at_10] & tpc2_at_10].
prop aux1505 := [tpc1_at_10 & tpc2_at_10].
prop aux1506 := [[~ tpc1_at_11] & [~ tpc2_at_11]].
prop aux1507 := [tpc1_at_11 & [~ tpc2_at_11]].
prop aux1508 := [[~ tpc1_at_11] & tpc2_at_11].
prop aux1509 := [tpc1_at_11 & tpc2_at_11].
prop aux1510 := [[~ gpc1_at_10] & [~ gpc2_at_10]].
prop aux1511 := [gpc1_at_10 & [~ gpc2_at_10]].
prop aux1512 := [[~ gpc1_at_10] & gpc2_at_10].
prop aux1513 := [gpc1_at_10 & gpc2_at_10].
prop aux1514 := [[~ gpc1_at_11] & [~ gpc2_at_11]].
prop aux1515 := [gpc1_at_11 & [~ gpc2_at_11]].
prop aux1516 := [[~ gpc1_at_11] & gpc2_at_11].
prop aux1517 := [gpc1_at_11 & gpc2_at_11].
prop aux1518 := [[~ cpc1_at_10] & [~ cpc2_at_10]].
prop aux1519 := [cpc1_at_10 & [~ cpc2_at_10]].
prop aux1520 := [[~ cpc1_at_10] & cpc2_at_10].
prop aux1521 := [cpc1_at_10 & cpc2_at_10].
prop aux1522 := [[~ cpc1_at_11] & [~ cpc2_at_11]].
prop aux1523 := [cpc1_at_11 & [~ cpc2_at_11]].
prop aux1524 := [[~ cpc1_at_11] & cpc2_at_11].
prop aux1525 := [cpc1_at_11 & cpc2_at_11].
prop aux1526 := [aux1507 => [x_at_11 <= 5]].
prop aux1527 := [aux1508 => [x_at_11 <= 5]].
prop aux1528 := [aux1509 => [x_at_11 <= 5]].
prop aux1529 := [aux1515 => [y_at_11 <= 1]].
prop aux1530 := [aux1517 => [y_at_11 <= 2]].
prop aux1531 := [aux1523 => [z_at_11 <= 1]].
prop aux1532 := [aux1525 => [z_at_11 <= 1]].
prop aux1533 := [[tpc1_at_11 <=> tpc1_at_10] & [tpc2_at_11 <=> tpc2_at_10]].
prop aux1534 := [aux1533 & [x_at_11 = (x_at_10 + d_at_10)]].
prop aux1535 := [[[[[[[[aux1502 & aux1507] & aux1494] & [x_at_11 = d_at_10]] | [[[[aux1503 & aux1508] & aux1495] & [x_at_10 > 2]] & [x_at_11 = (x_at_10 + d_at_10)]]] | [[[aux1504 & aux1509] & aux1496] & [x_at_11 = (x_at_10 + d_at_10)]]] | [[[aux1505 & aux1506] & aux1497] & [x_at_11 = (x_at_10 + d_at_10)]]] | [[[[aux1534 & [~ aux1494]] & [~ aux1495]] & [~ aux1496]] & [~ aux1497]]] & [[aux1526 & aux1527] & aux1528]].
prop aux1536 := [[gpc1_at_11 <=> gpc1_at_10] & [gpc2_at_11 <=> gpc2_at_10]].
prop aux1537 := [aux1536 & [y_at_11 = (y_at_10 + d_at_10)]].
prop aux1538 := [[[[[[[[aux1510 & aux1515] & aux1498] & [y_at_11 = d_at_10]] | [[[aux1511 & aux1516] & aux1499] & [y_at_11 = (y_at_10 + d_at_10)]]] | [[[aux1512 & aux1517] & aux1500] & [y_at_11 = d_at_10]]] | [[[[aux1513 & aux1514] & aux1501] & [y_at_10 >= 1]] & [y_at_11 = (y_at_10 + d_at_10)]]] | [[[[aux1537 & [~ aux1498]] & [~ aux1499]] & [~ aux1500]] & [~ aux1501]]] & [aux1529 & aux1530]].
prop aux1539 := [[cpc1_at_11 <=> cpc1_at_10] & [cpc2_at_11 <=> cpc2_at_10]].
prop aux1540 := [aux1539 & [z_at_11 = (z_at_10 + d_at_10)]].
prop aux1541 := [[[[[[[[aux1518 & aux1523] & aux1494] & [z_at_11 = d_at_10]] | [[[[aux1519 & aux1524] & aux1498] & [z_at_10 = 1]] & [z_at_11 = (z_at_10 + d_at_10)]]] | [[[aux1520 & aux1525] & aux1497] & [z_at_11 = d_at_10]]] | [[[aux1521 & aux1522] & aux1500] & [z_at_11 = (z_at_10 + d_at_10)]]] | [[[[aux1540 & [~ aux1494]] & [~ aux1498]] & [~ aux1497]] & [~ aux1500]]] & [aux1531 & aux1532]].
prop aux1542 := [d_at_10 >= 0].
prop aux1543 := [[[~ act1_at_11] & [~ act2_at_11]] & [~ act3_at_11]].
prop aux1544 := [[act1_at_11 & [~ act2_at_11]] & [~ act3_at_11]].
prop aux1545 := [[[~ act1_at_11] & act2_at_11] & [~ act3_at_11]].
prop aux1546 := [[act1_at_11 & act2_at_11] & [~ act3_at_11]].
prop aux1547 := [[[~ act1_at_11] & [~ act2_at_11]] & act3_at_11].
prop aux1548 := [[act1_at_11 & [~ act2_at_11]] & act3_at_11].
prop aux1549 := [[[~ act1_at_11] & act2_at_11] & act3_at_11].
prop aux1550 := [[act1_at_11 & act2_at_11] & act3_at_11].
prop aux1551 := [[~ tpc1_at_11] & [~ tpc2_at_11]].
prop aux1552 := [tpc1_at_11 & [~ tpc2_at_11]].
prop aux1553 := [[~ tpc1_at_11] & tpc2_at_11].
prop aux1554 := [tpc1_at_11 & tpc2_at_11].
prop aux1555 := [[~ tpc1_at_12] & [~ tpc2_at_12]].
prop aux1556 := [tpc1_at_12 & [~ tpc2_at_12]].
prop aux1557 := [[~ tpc1_at_12] & tpc2_at_12].
prop aux1558 := [tpc1_at_12 & tpc2_at_12].
prop aux1559 := [[~ gpc1_at_11] & [~ gpc2_at_11]].
prop aux1560 := [gpc1_at_11 & [~ gpc2_at_11]].
prop aux1561 := [[~ gpc1_at_11] & gpc2_at_11].
prop aux1562 := [gpc1_at_11 & gpc2_at_11].
prop aux1563 := [[~ gpc1_at_12] & [~ gpc2_at_12]].
prop aux1564 := [gpc1_at_12 & [~ gpc2_at_12]].
prop aux1565 := [[~ gpc1_at_12] & gpc2_at_12].
prop aux1566 := [gpc1_at_12 & gpc2_at_12].
prop aux1567 := [[~ cpc1_at_11] & [~ cpc2_at_11]].
prop aux1568 := [cpc1_at_11 & [~ cpc2_at_11]].
prop aux1569 := [[~ cpc1_at_11] & cpc2_at_11].
prop aux1570 := [cpc1_at_11 & cpc2_at_11].
prop aux1571 := [[~ cpc1_at_12] & [~ cpc2_at_12]].
prop aux1572 := [cpc1_at_12 & [~ cpc2_at_12]].
prop aux1573 := [[~ cpc1_at_12] & cpc2_at_12].
prop aux1574 := [cpc1_at_12 & cpc2_at_12].
prop aux1575 := [aux1556 => [x_at_12 <= 5]].
prop aux1576 := [aux1557 => [x_at_12 <= 5]].
prop aux1577 := [aux1558 => [x_at_12 <= 5]].
prop aux1578 := [aux1564 => [y_at_12 <= 1]].
prop aux1579 := [aux1566 => [y_at_12 <= 2]].
prop aux1580 := [aux1572 => [z_at_12 <= 1]].
prop aux1581 := [aux1574 => [z_at_12 <= 1]].
prop aux1582 := [[tpc1_at_12 <=> tpc1_at_11] & [tpc2_at_12 <=> tpc2_at_11]].
prop aux1583 := [aux1582 & [x_at_12 = (x_at_11 + d_at_11)]].
prop aux1584 := [[[[[[[[aux1551 & aux1556] & aux1543] & [x_at_12 = d_at_11]] | [[[[aux1552 & aux1557] & aux1544] & [x_at_11 > 2]] & [x_at_12 = (x_at_11 + d_at_11)]]] | [[[aux1553 & aux1558] & aux1545] & [x_at_12 = (x_at_11 + d_at_11)]]] | [[[aux1554 & aux1555] & aux1546] & [x_at_12 = (x_at_11 + d_at_11)]]] | [[[[aux1583 & [~ aux1543]] & [~ aux1544]] & [~ aux1545]] & [~ aux1546]]] & [[aux1575 & aux1576] & aux1577]].
prop aux1585 := [[gpc1_at_12 <=> gpc1_at_11] & [gpc2_at_12 <=> gpc2_at_11]].
prop aux1586 := [aux1585 & [y_at_12 = (y_at_11 + d_at_11)]].
prop aux1587 := [[[[[[[[aux1559 & aux1564] & aux1547] & [y_at_12 = d_at_11]] | [[[aux1560 & aux1565] & aux1548] & [y_at_12 = (y_at_11 + d_at_11)]]] | [[[aux1561 & aux1566] & aux1549] & [y_at_12 = d_at_11]]] | [[[[aux1562 & aux1563] & aux1550] & [y_at_11 >= 1]] & [y_at_12 = (y_at_11 + d_at_11)]]] | [[[[aux1586 & [~ aux1547]] & [~ aux1548]] & [~ aux1549]] & [~ aux1550]]] & [aux1578 & aux1579]].
prop aux1588 := [[cpc1_at_12 <=> cpc1_at_11] & [cpc2_at_12 <=> cpc2_at_11]].
prop aux1589 := [aux1588 & [z_at_12 = (z_at_11 + d_at_11)]].
prop aux1590 := [[[[[[[[aux1567 & aux1572] & aux1543] & [z_at_12 = d_at_11]] | [[[[aux1568 & aux1573] & aux1547] & [z_at_11 = 1]] & [z_at_12 = (z_at_11 + d_at_11)]]] | [[[aux1569 & aux1574] & aux1546] & [z_at_12 = d_at_11]]] | [[[aux1570 & aux1571] & aux1549] & [z_at_12 = (z_at_11 + d_at_11)]]] | [[[[aux1589 & [~ aux1543]] & [~ aux1547]] & [~ aux1546]] & [~ aux1549]]] & [aux1580 & aux1581]].
prop aux1591 := [d_at_11 >= 0].
prop aux1592 := [[[~ act1_at_12] & [~ act2_at_12]] & [~ act3_at_12]].
prop aux1593 := [[act1_at_12 & [~ act2_at_12]] & [~ act3_at_12]].
prop aux1594 := [[[~ act1_at_12] & act2_at_12] & [~ act3_at_12]].
prop aux1595 := [[act1_at_12 & act2_at_12] & [~ act3_at_12]].
prop aux1596 := [[[~ act1_at_12] & [~ act2_at_12]] & act3_at_12].
prop aux1597 := [[act1_at_12 & [~ act2_at_12]] & act3_at_12].
prop aux1598 := [[[~ act1_at_12] & act2_at_12] & act3_at_12].
prop aux1599 := [[act1_at_12 & act2_at_12] & act3_at_12].
prop aux1600 := [[~ tpc1_at_12] & [~ tpc2_at_12]].
prop aux1601 := [tpc1_at_12 & [~ tpc2_at_12]].
prop aux1602 := [[~ tpc1_at_12] & tpc2_at_12].
prop aux1603 := [tpc1_at_12 & tpc2_at_12].
prop aux1604 := [[~ tpc1_at_13] & [~ tpc2_at_13]].
prop aux1605 := [tpc1_at_13 & [~ tpc2_at_13]].
prop aux1606 := [[~ tpc1_at_13] & tpc2_at_13].
prop aux1607 := [tpc1_at_13 & tpc2_at_13].
prop aux1608 := [[~ gpc1_at_12] & [~ gpc2_at_12]].
prop aux1609 := [gpc1_at_12 & [~ gpc2_at_12]].
prop aux1610 := [[~ gpc1_at_12] & gpc2_at_12].
prop aux1611 := [gpc1_at_12 & gpc2_at_12].
prop aux1612 := [[~ gpc1_at_13] & [~ gpc2_at_13]].
prop aux1613 := [gpc1_at_13 & [~ gpc2_at_13]].
prop aux1614 := [[~ gpc1_at_13] & gpc2_at_13].
prop aux1615 := [gpc1_at_13 & gpc2_at_13].
prop aux1616 := [[~ cpc1_at_12] & [~ cpc2_at_12]].
prop aux1617 := [cpc1_at_12 & [~ cpc2_at_12]].
prop aux1618 := [[~ cpc1_at_12] & cpc2_at_12].
prop aux1619 := [cpc1_at_12 & cpc2_at_12].
prop aux1620 := [[~ cpc1_at_13] & [~ cpc2_at_13]].
prop aux1621 := [cpc1_at_13 & [~ cpc2_at_13]].
prop aux1622 := [[~ cpc1_at_13] & cpc2_at_13].
prop aux1623 := [cpc1_at_13 & cpc2_at_13].
prop aux1624 := [aux1605 => [x_at_13 <= 5]].
prop aux1625 := [aux1606 => [x_at_13 <= 5]].
prop aux1626 := [aux1607 => [x_at_13 <= 5]].
prop aux1627 := [aux1613 => [y_at_13 <= 1]].
prop aux1628 := [aux1615 => [y_at_13 <= 2]].
prop aux1629 := [aux1621 => [z_at_13 <= 1]].
prop aux1630 := [aux1623 => [z_at_13 <= 1]].
prop aux1631 := [[tpc1_at_13 <=> tpc1_at_12] & [tpc2_at_13 <=> tpc2_at_12]].
prop aux1632 := [aux1631 & [x_at_13 = (x_at_12 + d_at_12)]].
prop aux1633 := [[[[[[[[aux1600 & aux1605] & aux1592] & [x_at_13 = d_at_12]] | [[[[aux1601 & aux1606] & aux1593] & [x_at_12 > 2]] & [x_at_13 = (x_at_12 + d_at_12)]]] | [[[aux1602 & aux1607] & aux1594] & [x_at_13 = (x_at_12 + d_at_12)]]] | [[[aux1603 & aux1604] & aux1595] & [x_at_13 = (x_at_12 + d_at_12)]]] | [[[[aux1632 & [~ aux1592]] & [~ aux1593]] & [~ aux1594]] & [~ aux1595]]] & [[aux1624 & aux1625] & aux1626]].
prop aux1634 := [[gpc1_at_13 <=> gpc1_at_12] & [gpc2_at_13 <=> gpc2_at_12]].
prop aux1635 := [aux1634 & [y_at_13 = (y_at_12 + d_at_12)]].
prop aux1636 := [[[[[[[[aux1608 & aux1613] & aux1596] & [y_at_13 = d_at_12]] | [[[aux1609 & aux1614] & aux1597] & [y_at_13 = (y_at_12 + d_at_12)]]] | [[[aux1610 & aux1615] & aux1598] & [y_at_13 = d_at_12]]] | [[[[aux1611 & aux1612] & aux1599] & [y_at_12 >= 1]] & [y_at_13 = (y_at_12 + d_at_12)]]] | [[[[aux1635 & [~ aux1596]] & [~ aux1597]] & [~ aux1598]] & [~ aux1599]]] & [aux1627 & aux1628]].
prop aux1637 := [[cpc1_at_13 <=> cpc1_at_12] & [cpc2_at_13 <=> cpc2_at_12]].
prop aux1638 := [aux1637 & [z_at_13 = (z_at_12 + d_at_12)]].
prop aux1639 := [[[[[[[[aux1616 & aux1621] & aux1592] & [z_at_13 = d_at_12]] | [[[[aux1617 & aux1622] & aux1596] & [z_at_12 = 1]] & [z_at_13 = (z_at_12 + d_at_12)]]] | [[[aux1618 & aux1623] & aux1595] & [z_at_13 = d_at_12]]] | [[[aux1619 & aux1620] & aux1598] & [z_at_13 = (z_at_12 + d_at_12)]]] | [[[[aux1638 & [~ aux1592]] & [~ aux1596]] & [~ aux1595]] & [~ aux1598]]] & [aux1629 & aux1630]].
prop aux1640 := [d_at_12 >= 0].
prop aux1641 := [[[~ act1_at_13] & [~ act2_at_13]] & [~ act3_at_13]].
prop aux1642 := [[act1_at_13 & [~ act2_at_13]] & [~ act3_at_13]].
prop aux1643 := [[[~ act1_at_13] & act2_at_13] & [~ act3_at_13]].
prop aux1644 := [[act1_at_13 & act2_at_13] & [~ act3_at_13]].
prop aux1645 := [[[~ act1_at_13] & [~ act2_at_13]] & act3_at_13].
prop aux1646 := [[act1_at_13 & [~ act2_at_13]] & act3_at_13].
prop aux1647 := [[[~ act1_at_13] & act2_at_13] & act3_at_13].
prop aux1648 := [[act1_at_13 & act2_at_13] & act3_at_13].
prop aux1649 := [[~ tpc1_at_13] & [~ tpc2_at_13]].
prop aux1650 := [tpc1_at_13 & [~ tpc2_at_13]].
prop aux1651 := [[~ tpc1_at_13] & tpc2_at_13].
prop aux1652 := [tpc1_at_13 & tpc2_at_13].
prop aux1653 := [[~ tpc1_at_14] & [~ tpc2_at_14]].
prop aux1654 := [tpc1_at_14 & [~ tpc2_at_14]].
prop aux1655 := [[~ tpc1_at_14] & tpc2_at_14].
prop aux1656 := [tpc1_at_14 & tpc2_at_14].
prop aux1657 := [[~ gpc1_at_13] & [~ gpc2_at_13]].
prop aux1658 := [gpc1_at_13 & [~ gpc2_at_13]].
prop aux1659 := [[~ gpc1_at_13] & gpc2_at_13].
prop aux1660 := [gpc1_at_13 & gpc2_at_13].
prop aux1661 := [[~ gpc1_at_14] & [~ gpc2_at_14]].
prop aux1662 := [gpc1_at_14 & [~ gpc2_at_14]].
prop aux1663 := [[~ gpc1_at_14] & gpc2_at_14].
prop aux1664 := [gpc1_at_14 & gpc2_at_14].
prop aux1665 := [[~ cpc1_at_13] & [~ cpc2_at_13]].
prop aux1666 := [cpc1_at_13 & [~ cpc2_at_13]].
prop aux1667 := [[~ cpc1_at_13] & cpc2_at_13].
prop aux1668 := [cpc1_at_13 & cpc2_at_13].
prop aux1669 := [[~ cpc1_at_14] & [~ cpc2_at_14]].
prop aux1670 := [cpc1_at_14 & [~ cpc2_at_14]].
prop aux1671 := [[~ cpc1_at_14] & cpc2_at_14].
prop aux1672 := [cpc1_at_14 & cpc2_at_14].
prop aux1673 := [aux1654 => [x_at_14 <= 5]].
prop aux1674 := [aux1655 => [x_at_14 <= 5]].
prop aux1675 := [aux1656 => [x_at_14 <= 5]].
prop aux1676 := [aux1662 => [y_at_14 <= 1]].
prop aux1677 := [aux1664 => [y_at_14 <= 2]].
prop aux1678 := [aux1670 => [z_at_14 <= 1]].
prop aux1679 := [aux1672 => [z_at_14 <= 1]].
prop aux1680 := [[tpc1_at_14 <=> tpc1_at_13] & [tpc2_at_14 <=> tpc2_at_13]].
prop aux1681 := [aux1680 & [x_at_14 = (x_at_13 + d_at_13)]].
prop aux1682 := [[[[[[[[aux1649 & aux1654] & aux1641] & [x_at_14 = d_at_13]] | [[[[aux1650 & aux1655] & aux1642] & [x_at_13 > 2]] & [x_at_14 = (x_at_13 + d_at_13)]]] | [[[aux1651 & aux1656] & aux1643] & [x_at_14 = (x_at_13 + d_at_13)]]] | [[[aux1652 & aux1653] & aux1644] & [x_at_14 = (x_at_13 + d_at_13)]]] | [[[[aux1681 & [~ aux1641]] & [~ aux1642]] & [~ aux1643]] & [~ aux1644]]] & [[aux1673 & aux1674] & aux1675]].
prop aux1683 := [[gpc1_at_14 <=> gpc1_at_13] & [gpc2_at_14 <=> gpc2_at_13]].
prop aux1684 := [aux1683 & [y_at_14 = (y_at_13 + d_at_13)]].
prop aux1685 := [[[[[[[[aux1657 & aux1662] & aux1645] & [y_at_14 = d_at_13]] | [[[aux1658 & aux1663] & aux1646] & [y_at_14 = (y_at_13 + d_at_13)]]] | [[[aux1659 & aux1664] & aux1647] & [y_at_14 = d_at_13]]] | [[[[aux1660 & aux1661] & aux1648] & [y_at_13 >= 1]] & [y_at_14 = (y_at_13 + d_at_13)]]] | [[[[aux1684 & [~ aux1645]] & [~ aux1646]] & [~ aux1647]] & [~ aux1648]]] & [aux1676 & aux1677]].
prop aux1686 := [[cpc1_at_14 <=> cpc1_at_13] & [cpc2_at_14 <=> cpc2_at_13]].
prop aux1687 := [aux1686 & [z_at_14 = (z_at_13 + d_at_13)]].
prop aux1688 := [[[[[[[[aux1665 & aux1670] & aux1641] & [z_at_14 = d_at_13]] | [[[[aux1666 & aux1671] & aux1645] & [z_at_13 = 1]] & [z_at_14 = (z_at_13 + d_at_13)]]] | [[[aux1667 & aux1672] & aux1644] & [z_at_14 = d_at_13]]] | [[[aux1668 & aux1669] & aux1647] & [z_at_14 = (z_at_13 + d_at_13)]]] | [[[[aux1687 & [~ aux1641]] & [~ aux1645]] & [~ aux1644]] & [~ aux1647]]] & [aux1678 & aux1679]].
prop aux1689 := [d_at_13 >= 0].
prop aux1690 := [[[~ act1_at_14] & [~ act2_at_14]] & [~ act3_at_14]].
prop aux1691 := [[act1_at_14 & [~ act2_at_14]] & [~ act3_at_14]].
prop aux1692 := [[[~ act1_at_14] & act2_at_14] & [~ act3_at_14]].
prop aux1693 := [[act1_at_14 & act2_at_14] & [~ act3_at_14]].
prop aux1694 := [[[~ act1_at_14] & [~ act2_at_14]] & act3_at_14].
prop aux1695 := [[act1_at_14 & [~ act2_at_14]] & act3_at_14].
prop aux1696 := [[[~ act1_at_14] & act2_at_14] & act3_at_14].
prop aux1697 := [[act1_at_14 & act2_at_14] & act3_at_14].
prop aux1698 := [[~ tpc1_at_14] & [~ tpc2_at_14]].
prop aux1699 := [tpc1_at_14 & [~ tpc2_at_14]].
prop aux1700 := [[~ tpc1_at_14] & tpc2_at_14].
prop aux1701 := [tpc1_at_14 & tpc2_at_14].
prop aux1702 := [[~ tpc1_at_15] & [~ tpc2_at_15]].
prop aux1703 := [tpc1_at_15 & [~ tpc2_at_15]].
prop aux1704 := [[~ tpc1_at_15] & tpc2_at_15].
prop aux1705 := [tpc1_at_15 & tpc2_at_15].
prop aux1706 := [[~ gpc1_at_14] & [~ gpc2_at_14]].
prop aux1707 := [gpc1_at_14 & [~ gpc2_at_14]].
prop aux1708 := [[~ gpc1_at_14] & gpc2_at_14].
prop aux1709 := [gpc1_at_14 & gpc2_at_14].
prop aux1710 := [[~ gpc1_at_15] & [~ gpc2_at_15]].
prop aux1711 := [gpc1_at_15 & [~ gpc2_at_15]].
prop aux1712 := [[~ gpc1_at_15] & gpc2_at_15].
prop aux1713 := [gpc1_at_15 & gpc2_at_15].
prop aux1714 := [[~ cpc1_at_14] & [~ cpc2_at_14]].
prop aux1715 := [cpc1_at_14 & [~ cpc2_at_14]].
prop aux1716 := [[~ cpc1_at_14] & cpc2_at_14].
prop aux1717 := [cpc1_at_14 & cpc2_at_14].
prop aux1718 := [[~ cpc1_at_15] & [~ cpc2_at_15]].
prop aux1719 := [cpc1_at_15 & [~ cpc2_at_15]].
prop aux1720 := [[~ cpc1_at_15] & cpc2_at_15].
prop aux1721 := [cpc1_at_15 & cpc2_at_15].
prop aux1722 := [aux1703 => [x_at_15 <= 5]].
prop aux1723 := [aux1704 => [x_at_15 <= 5]].
prop aux1724 := [aux1705 => [x_at_15 <= 5]].
prop aux1725 := [aux1711 => [y_at_15 <= 1]].
prop aux1726 := [aux1713 => [y_at_15 <= 2]].
prop aux1727 := [aux1719 => [z_at_15 <= 1]].
prop aux1728 := [aux1721 => [z_at_15 <= 1]].
prop aux1729 := [[tpc1_at_15 <=> tpc1_at_14] & [tpc2_at_15 <=> tpc2_at_14]].
prop aux1730 := [aux1729 & [x_at_15 = (x_at_14 + d_at_14)]].
prop aux1731 := [[[[[[[[aux1698 & aux1703] & aux1690] & [x_at_15 = d_at_14]] | [[[[aux1699 & aux1704] & aux1691] & [x_at_14 > 2]] & [x_at_15 = (x_at_14 + d_at_14)]]] | [[[aux1700 & aux1705] & aux1692] & [x_at_15 = (x_at_14 + d_at_14)]]] | [[[aux1701 & aux1702] & aux1693] & [x_at_15 = (x_at_14 + d_at_14)]]] | [[[[aux1730 & [~ aux1690]] & [~ aux1691]] & [~ aux1692]] & [~ aux1693]]] & [[aux1722 & aux1723] & aux1724]].
prop aux1732 := [[gpc1_at_15 <=> gpc1_at_14] & [gpc2_at_15 <=> gpc2_at_14]].
prop aux1733 := [aux1732 & [y_at_15 = (y_at_14 + d_at_14)]].
prop aux1734 := [[[[[[[[aux1706 & aux1711] & aux1694] & [y_at_15 = d_at_14]] | [[[aux1707 & aux1712] & aux1695] & [y_at_15 = (y_at_14 + d_at_14)]]] | [[[aux1708 & aux1713] & aux1696] & [y_at_15 = d_at_14]]] | [[[[aux1709 & aux1710] & aux1697] & [y_at_14 >= 1]] & [y_at_15 = (y_at_14 + d_at_14)]]] | [[[[aux1733 & [~ aux1694]] & [~ aux1695]] & [~ aux1696]] & [~ aux1697]]] & [aux1725 & aux1726]].
prop aux1735 := [[cpc1_at_15 <=> cpc1_at_14] & [cpc2_at_15 <=> cpc2_at_14]].
prop aux1736 := [aux1735 & [z_at_15 = (z_at_14 + d_at_14)]].
prop aux1737 := [[[[[[[[aux1714 & aux1719] & aux1690] & [z_at_15 = d_at_14]] | [[[[aux1715 & aux1720] & aux1694] & [z_at_14 = 1]] & [z_at_15 = (z_at_14 + d_at_14)]]] | [[[aux1716 & aux1721] & aux1693] & [z_at_15 = d_at_14]]] | [[[aux1717 & aux1718] & aux1696] & [z_at_15 = (z_at_14 + d_at_14)]]] | [[[[aux1736 & [~ aux1690]] & [~ aux1694]] & [~ aux1693]] & [~ aux1696]]] & [aux1727 & aux1728]].
prop aux1738 := [d_at_14 >= 0].
prop aux1739 := [[[~ act1_at_15] & [~ act2_at_15]] & [~ act3_at_15]].
prop aux1740 := [[act1_at_15 & [~ act2_at_15]] & [~ act3_at_15]].
prop aux1741 := [[[~ act1_at_15] & act2_at_15] & [~ act3_at_15]].
prop aux1742 := [[act1_at_15 & act2_at_15] & [~ act3_at_15]].
prop aux1743 := [[[~ act1_at_15] & [~ act2_at_15]] & act3_at_15].
prop aux1744 := [[act1_at_15 & [~ act2_at_15]] & act3_at_15].
prop aux1745 := [[[~ act1_at_15] & act2_at_15] & act3_at_15].
prop aux1746 := [[act1_at_15 & act2_at_15] & act3_at_15].
prop aux1747 := [[~ tpc1_at_15] & [~ tpc2_at_15]].
prop aux1748 := [tpc1_at_15 & [~ tpc2_at_15]].
prop aux1749 := [[~ tpc1_at_15] & tpc2_at_15].
prop aux1750 := [tpc1_at_15 & tpc2_at_15].
prop aux1751 := [[~ tpc1_at_16] & [~ tpc2_at_16]].
prop aux1752 := [tpc1_at_16 & [~ tpc2_at_16]].
prop aux1753 := [[~ tpc1_at_16] & tpc2_at_16].
prop aux1754 := [tpc1_at_16 & tpc2_at_16].
prop aux1755 := [[~ gpc1_at_15] & [~ gpc2_at_15]].
prop aux1756 := [gpc1_at_15 & [~ gpc2_at_15]].
prop aux1757 := [[~ gpc1_at_15] & gpc2_at_15].
prop aux1758 := [gpc1_at_15 & gpc2_at_15].
prop aux1759 := [[~ gpc1_at_16] & [~ gpc2_at_16]].
prop aux1760 := [gpc1_at_16 & [~ gpc2_at_16]].
prop aux1761 := [[~ gpc1_at_16] & gpc2_at_16].
prop aux1762 := [gpc1_at_16 & gpc2_at_16].
prop aux1763 := [[~ cpc1_at_15] & [~ cpc2_at_15]].
prop aux1764 := [cpc1_at_15 & [~ cpc2_at_15]].
prop aux1765 := [[~ cpc1_at_15] & cpc2_at_15].
prop aux1766 := [cpc1_at_15 & cpc2_at_15].
prop aux1767 := [[~ cpc1_at_16] & [~ cpc2_at_16]].
prop aux1768 := [cpc1_at_16 & [~ cpc2_at_16]].
prop aux1769 := [[~ cpc1_at_16] & cpc2_at_16].
prop aux1770 := [cpc1_at_16 & cpc2_at_16].
prop aux1771 := [aux1752 => [x_at_16 <= 5]].
prop aux1772 := [aux1753 => [x_at_16 <= 5]].
prop aux1773 := [aux1754 => [x_at_16 <= 5]].
prop aux1774 := [aux1760 => [y_at_16 <= 1]].
prop aux1775 := [aux1762 => [y_at_16 <= 2]].
prop aux1776 := [aux1768 => [z_at_16 <= 1]].
prop aux1777 := [aux1770 => [z_at_16 <= 1]].
prop aux1778 := [[tpc1_at_16 <=> tpc1_at_15] & [tpc2_at_16 <=> tpc2_at_15]].
prop aux1779 := [aux1778 & [x_at_16 = (x_at_15 + d_at_15)]].
prop aux1780 := [[[[[[[[aux1747 & aux1752] & aux1739] & [x_at_16 = d_at_15]] | [[[[aux1748 & aux1753] & aux1740] & [x_at_15 > 2]] & [x_at_16 = (x_at_15 + d_at_15)]]] | [[[aux1749 & aux1754] & aux1741] & [x_at_16 = (x_at_15 + d_at_15)]]] | [[[aux1750 & aux1751] & aux1742] & [x_at_16 = (x_at_15 + d_at_15)]]] | [[[[aux1779 & [~ aux1739]] & [~ aux1740]] & [~ aux1741]] & [~ aux1742]]] & [[aux1771 & aux1772] & aux1773]].
prop aux1781 := [[gpc1_at_16 <=> gpc1_at_15] & [gpc2_at_16 <=> gpc2_at_15]].
prop aux1782 := [aux1781 & [y_at_16 = (y_at_15 + d_at_15)]].
prop aux1783 := [[[[[[[[aux1755 & aux1760] & aux1743] & [y_at_16 = d_at_15]] | [[[aux1756 & aux1761] & aux1744] & [y_at_16 = (y_at_15 + d_at_15)]]] | [[[aux1757 & aux1762] & aux1745] & [y_at_16 = d_at_15]]] | [[[[aux1758 & aux1759] & aux1746] & [y_at_15 >= 1]] & [y_at_16 = (y_at_15 + d_at_15)]]] | [[[[aux1782 & [~ aux1743]] & [~ aux1744]] & [~ aux1745]] & [~ aux1746]]] & [aux1774 & aux1775]].
prop aux1784 := [[cpc1_at_16 <=> cpc1_at_15] & [cpc2_at_16 <=> cpc2_at_15]].
prop aux1785 := [aux1784 & [z_at_16 = (z_at_15 + d_at_15)]].
prop aux1786 := [[[[[[[[aux1763 & aux1768] & aux1739] & [z_at_16 = d_at_15]] | [[[[aux1764 & aux1769] & aux1743] & [z_at_15 = 1]] & [z_at_16 = (z_at_15 + d_at_15)]]] | [[[aux1765 & aux1770] & aux1742] & [z_at_16 = d_at_15]]] | [[[aux1766 & aux1767] & aux1745] & [z_at_16 = (z_at_15 + d_at_15)]]] | [[[[aux1785 & [~ aux1739]] & [~ aux1743]] & [~ aux1742]] & [~ aux1745]]] & [aux1776 & aux1777]].
prop aux1787 := [d_at_15 >= 0].
prop aux1788 := [[[~ act1_at_16] & [~ act2_at_16]] & [~ act3_at_16]].
prop aux1789 := [[act1_at_16 & [~ act2_at_16]] & [~ act3_at_16]].
prop aux1790 := [[[~ act1_at_16] & act2_at_16] & [~ act3_at_16]].
prop aux1791 := [[act1_at_16 & act2_at_16] & [~ act3_at_16]].
prop aux1792 := [[[~ act1_at_16] & [~ act2_at_16]] & act3_at_16].
prop aux1793 := [[act1_at_16 & [~ act2_at_16]] & act3_at_16].
prop aux1794 := [[[~ act1_at_16] & act2_at_16] & act3_at_16].
prop aux1795 := [[act1_at_16 & act2_at_16] & act3_at_16].
prop aux1796 := [[~ tpc1_at_16] & [~ tpc2_at_16]].
prop aux1797 := [tpc1_at_16 & [~ tpc2_at_16]].
prop aux1798 := [[~ tpc1_at_16] & tpc2_at_16].
prop aux1799 := [tpc1_at_16 & tpc2_at_16].
prop aux1800 := [[~ tpc1_at_17] & [~ tpc2_at_17]].
prop aux1801 := [tpc1_at_17 & [~ tpc2_at_17]].
prop aux1802 := [[~ tpc1_at_17] & tpc2_at_17].
prop aux1803 := [tpc1_at_17 & tpc2_at_17].
prop aux1804 := [[~ gpc1_at_16] & [~ gpc2_at_16]].
prop aux1805 := [gpc1_at_16 & [~ gpc2_at_16]].
prop aux1806 := [[~ gpc1_at_16] & gpc2_at_16].
prop aux1807 := [gpc1_at_16 & gpc2_at_16].
prop aux1808 := [[~ gpc1_at_17] & [~ gpc2_at_17]].
prop aux1809 := [gpc1_at_17 & [~ gpc2_at_17]].
prop aux1810 := [[~ gpc1_at_17] & gpc2_at_17].
prop aux1811 := [gpc1_at_17 & gpc2_at_17].
prop aux1812 := [[~ cpc1_at_16] & [~ cpc2_at_16]].
prop aux1813 := [cpc1_at_16 & [~ cpc2_at_16]].
prop aux1814 := [[~ cpc1_at_16] & cpc2_at_16].
prop aux1815 := [cpc1_at_16 & cpc2_at_16].
prop aux1816 := [[~ cpc1_at_17] & [~ cpc2_at_17]].
prop aux1817 := [cpc1_at_17 & [~ cpc2_at_17]].
prop aux1818 := [[~ cpc1_at_17] & cpc2_at_17].
prop aux1819 := [cpc1_at_17 & cpc2_at_17].
prop aux1820 := [aux1801 => [x_at_17 <= 5]].
prop aux1821 := [aux1802 => [x_at_17 <= 5]].
prop aux1822 := [aux1803 => [x_at_17 <= 5]].
prop aux1823 := [aux1809 => [y_at_17 <= 1]].
prop aux1824 := [aux1811 => [y_at_17 <= 2]].
prop aux1825 := [aux1817 => [z_at_17 <= 1]].
prop aux1826 := [aux1819 => [z_at_17 <= 1]].
prop aux1827 := [[tpc1_at_17 <=> tpc1_at_16] & [tpc2_at_17 <=> tpc2_at_16]].
prop aux1828 := [aux1827 & [x_at_17 = (x_at_16 + d_at_16)]].
prop aux1829 := [[[[[[[[aux1796 & aux1801] & aux1788] & [x_at_17 = d_at_16]] | [[[[aux1797 & aux1802] & aux1789] & [x_at_16 > 2]] & [x_at_17 = (x_at_16 + d_at_16)]]] | [[[aux1798 & aux1803] & aux1790] & [x_at_17 = (x_at_16 + d_at_16)]]] | [[[aux1799 & aux1800] & aux1791] & [x_at_17 = (x_at_16 + d_at_16)]]] | [[[[aux1828 & [~ aux1788]] & [~ aux1789]] & [~ aux1790]] & [~ aux1791]]] & [[aux1820 & aux1821] & aux1822]].
prop aux1830 := [[gpc1_at_17 <=> gpc1_at_16] & [gpc2_at_17 <=> gpc2_at_16]].
prop aux1831 := [aux1830 & [y_at_17 = (y_at_16 + d_at_16)]].
prop aux1832 := [[[[[[[[aux1804 & aux1809] & aux1792] & [y_at_17 = d_at_16]] | [[[aux1805 & aux1810] & aux1793] & [y_at_17 = (y_at_16 + d_at_16)]]] | [[[aux1806 & aux1811] & aux1794] & [y_at_17 = d_at_16]]] | [[[[aux1807 & aux1808] & aux1795] & [y_at_16 >= 1]] & [y_at_17 = (y_at_16 + d_at_16)]]] | [[[[aux1831 & [~ aux1792]] & [~ aux1793]] & [~ aux1794]] & [~ aux1795]]] & [aux1823 & aux1824]].
prop aux1833 := [[cpc1_at_17 <=> cpc1_at_16] & [cpc2_at_17 <=> cpc2_at_16]].
prop aux1834 := [aux1833 & [z_at_17 = (z_at_16 + d_at_16)]].
prop aux1835 := [[[[[[[[aux1812 & aux1817] & aux1788] & [z_at_17 = d_at_16]] | [[[[aux1813 & aux1818] & aux1792] & [z_at_16 = 1]] & [z_at_17 = (z_at_16 + d_at_16)]]] | [[[aux1814 & aux1819] & aux1791] & [z_at_17 = d_at_16]]] | [[[aux1815 & aux1816] & aux1794] & [z_at_17 = (z_at_16 + d_at_16)]]] | [[[[aux1834 & [~ aux1788]] & [~ aux1792]] & [~ aux1791]] & [~ aux1794]]] & [aux1825 & aux1826]].
prop aux1836 := [d_at_16 >= 0].
prop aux1837 := [[[~ act1_at_17] & [~ act2_at_17]] & [~ act3_at_17]].
prop aux1838 := [[act1_at_17 & [~ act2_at_17]] & [~ act3_at_17]].
prop aux1839 := [[[~ act1_at_17] & act2_at_17] & [~ act3_at_17]].
prop aux1840 := [[act1_at_17 & act2_at_17] & [~ act3_at_17]].
prop aux1841 := [[[~ act1_at_17] & [~ act2_at_17]] & act3_at_17].
prop aux1842 := [[act1_at_17 & [~ act2_at_17]] & act3_at_17].
prop aux1843 := [[[~ act1_at_17] & act2_at_17] & act3_at_17].
prop aux1844 := [[act1_at_17 & act2_at_17] & act3_at_17].
prop aux1845 := [[~ tpc1_at_17] & [~ tpc2_at_17]].
prop aux1846 := [tpc1_at_17 & [~ tpc2_at_17]].
prop aux1847 := [[~ tpc1_at_17] & tpc2_at_17].
prop aux1848 := [tpc1_at_17 & tpc2_at_17].
prop aux1849 := [[~ tpc1_at_18] & [~ tpc2_at_18]].
prop aux1850 := [tpc1_at_18 & [~ tpc2_at_18]].
prop aux1851 := [[~ tpc1_at_18] & tpc2_at_18].
prop aux1852 := [tpc1_at_18 & tpc2_at_18].
prop aux1853 := [[~ gpc1_at_17] & [~ gpc2_at_17]].
prop aux1854 := [gpc1_at_17 & [~ gpc2_at_17]].
prop aux1855 := [[~ gpc1_at_17] & gpc2_at_17].
prop aux1856 := [gpc1_at_17 & gpc2_at_17].
prop aux1857 := [[~ gpc1_at_18] & [~ gpc2_at_18]].
prop aux1858 := [gpc1_at_18 & [~ gpc2_at_18]].
prop aux1859 := [[~ gpc1_at_18] & gpc2_at_18].
prop aux1860 := [gpc1_at_18 & gpc2_at_18].
prop aux1861 := [[~ cpc1_at_17] & [~ cpc2_at_17]].
prop aux1862 := [cpc1_at_17 & [~ cpc2_at_17]].
prop aux1863 := [[~ cpc1_at_17] & cpc2_at_17].
prop aux1864 := [cpc1_at_17 & cpc2_at_17].
prop aux1865 := [[~ cpc1_at_18] & [~ cpc2_at_18]].
prop aux1866 := [cpc1_at_18 & [~ cpc2_at_18]].
prop aux1867 := [[~ cpc1_at_18] & cpc2_at_18].
prop aux1868 := [cpc1_at_18 & cpc2_at_18].
prop aux1869 := [aux1850 => [x_at_18 <= 5]].
prop aux1870 := [aux1851 => [x_at_18 <= 5]].
prop aux1871 := [aux1852 => [x_at_18 <= 5]].
prop aux1872 := [aux1858 => [y_at_18 <= 1]].
prop aux1873 := [aux1860 => [y_at_18 <= 2]].
prop aux1874 := [aux1866 => [z_at_18 <= 1]].
prop aux1875 := [aux1868 => [z_at_18 <= 1]].
prop aux1876 := [[tpc1_at_18 <=> tpc1_at_17] & [tpc2_at_18 <=> tpc2_at_17]].
prop aux1877 := [aux1876 & [x_at_18 = (x_at_17 + d_at_17)]].
prop aux1878 := [[[[[[[[aux1845 & aux1850] & aux1837] & [x_at_18 = d_at_17]] | [[[[aux1846 & aux1851] & aux1838] & [x_at_17 > 2]] & [x_at_18 = (x_at_17 + d_at_17)]]] | [[[aux1847 & aux1852] & aux1839] & [x_at_18 = (x_at_17 + d_at_17)]]] | [[[aux1848 & aux1849] & aux1840] & [x_at_18 = (x_at_17 + d_at_17)]]] | [[[[aux1877 & [~ aux1837]] & [~ aux1838]] & [~ aux1839]] & [~ aux1840]]] & [[aux1869 & aux1870] & aux1871]].
prop aux1879 := [[gpc1_at_18 <=> gpc1_at_17] & [gpc2_at_18 <=> gpc2_at_17]].
prop aux1880 := [aux1879 & [y_at_18 = (y_at_17 + d_at_17)]].
prop aux1881 := [[[[[[[[aux1853 & aux1858] & aux1841] & [y_at_18 = d_at_17]] | [[[aux1854 & aux1859] & aux1842] & [y_at_18 = (y_at_17 + d_at_17)]]] | [[[aux1855 & aux1860] & aux1843] & [y_at_18 = d_at_17]]] | [[[[aux1856 & aux1857] & aux1844] & [y_at_17 >= 1]] & [y_at_18 = (y_at_17 + d_at_17)]]] | [[[[aux1880 & [~ aux1841]] & [~ aux1842]] & [~ aux1843]] & [~ aux1844]]] & [aux1872 & aux1873]].
prop aux1882 := [[cpc1_at_18 <=> cpc1_at_17] & [cpc2_at_18 <=> cpc2_at_17]].
prop aux1883 := [aux1882 & [z_at_18 = (z_at_17 + d_at_17)]].
prop aux1884 := [[[[[[[[aux1861 & aux1866] & aux1837] & [z_at_18 = d_at_17]] | [[[[aux1862 & aux1867] & aux1841] & [z_at_17 = 1]] & [z_at_18 = (z_at_17 + d_at_17)]]] | [[[aux1863 & aux1868] & aux1840] & [z_at_18 = d_at_17]]] | [[[aux1864 & aux1865] & aux1843] & [z_at_18 = (z_at_17 + d_at_17)]]] | [[[[aux1883 & [~ aux1837]] & [~ aux1841]] & [~ aux1840]] & [~ aux1843]]] & [aux1874 & aux1875]].
prop aux1885 := [d_at_17 >= 0].
prop aux1886 := [[[~ act1_at_18] & [~ act2_at_18]] & [~ act3_at_18]].
prop aux1887 := [[act1_at_18 & [~ act2_at_18]] & [~ act3_at_18]].
prop aux1888 := [[[~ act1_at_18] & act2_at_18] & [~ act3_at_18]].
prop aux1889 := [[act1_at_18 & act2_at_18] & [~ act3_at_18]].
prop aux1890 := [[[~ act1_at_18] & [~ act2_at_18]] & act3_at_18].
prop aux1891 := [[act1_at_18 & [~ act2_at_18]] & act3_at_18].
prop aux1892 := [[[~ act1_at_18] & act2_at_18] & act3_at_18].
prop aux1893 := [[act1_at_18 & act2_at_18] & act3_at_18].
prop aux1894 := [[~ tpc1_at_18] & [~ tpc2_at_18]].
prop aux1895 := [tpc1_at_18 & [~ tpc2_at_18]].
prop aux1896 := [[~ tpc1_at_18] & tpc2_at_18].
prop aux1897 := [tpc1_at_18 & tpc2_at_18].
prop aux1898 := [[~ tpc1_at_19] & [~ tpc2_at_19]].
prop aux1899 := [tpc1_at_19 & [~ tpc2_at_19]].
prop aux1900 := [[~ tpc1_at_19] & tpc2_at_19].
prop aux1901 := [tpc1_at_19 & tpc2_at_19].
prop aux1902 := [[~ gpc1_at_18] & [~ gpc2_at_18]].
prop aux1903 := [gpc1_at_18 & [~ gpc2_at_18]].
prop aux1904 := [[~ gpc1_at_18] & gpc2_at_18].
prop aux1905 := [gpc1_at_18 & gpc2_at_18].
prop aux1906 := [[~ gpc1_at_19] & [~ gpc2_at_19]].
prop aux1907 := [gpc1_at_19 & [~ gpc2_at_19]].
prop aux1908 := [[~ gpc1_at_19] & gpc2_at_19].
prop aux1909 := [gpc1_at_19 & gpc2_at_19].
prop aux1910 := [[~ cpc1_at_18] & [~ cpc2_at_18]].
prop aux1911 := [cpc1_at_18 & [~ cpc2_at_18]].
prop aux1912 := [[~ cpc1_at_18] & cpc2_at_18].
prop aux1913 := [cpc1_at_18 & cpc2_at_18].
prop aux1914 := [[~ cpc1_at_19] & [~ cpc2_at_19]].
prop aux1915 := [cpc1_at_19 & [~ cpc2_at_19]].
prop aux1916 := [[~ cpc1_at_19] & cpc2_at_19].
prop aux1917 := [cpc1_at_19 & cpc2_at_19].
prop aux1918 := [aux1899 => [x_at_19 <= 5]].
prop aux1919 := [aux1900 => [x_at_19 <= 5]].
prop aux1920 := [aux1901 => [x_at_19 <= 5]].
prop aux1921 := [aux1907 => [y_at_19 <= 1]].
prop aux1922 := [aux1909 => [y_at_19 <= 2]].
prop aux1923 := [aux1915 => [z_at_19 <= 1]].
prop aux1924 := [aux1917 => [z_at_19 <= 1]].
prop aux1925 := [[tpc1_at_19 <=> tpc1_at_18] & [tpc2_at_19 <=> tpc2_at_18]].
prop aux1926 := [aux1925 & [x_at_19 = (x_at_18 + d_at_18)]].
prop aux1927 := [[[[[[[[aux1894 & aux1899] & aux1886] & [x_at_19 = d_at_18]] | [[[[aux1895 & aux1900] & aux1887] & [x_at_18 > 2]] & [x_at_19 = (x_at_18 + d_at_18)]]] | [[[aux1896 & aux1901] & aux1888] & [x_at_19 = (x_at_18 + d_at_18)]]] | [[[aux1897 & aux1898] & aux1889] & [x_at_19 = (x_at_18 + d_at_18)]]] | [[[[aux1926 & [~ aux1886]] & [~ aux1887]] & [~ aux1888]] & [~ aux1889]]] & [[aux1918 & aux1919] & aux1920]].
prop aux1928 := [[gpc1_at_19 <=> gpc1_at_18] & [gpc2_at_19 <=> gpc2_at_18]].
prop aux1929 := [aux1928 & [y_at_19 = (y_at_18 + d_at_18)]].
prop aux1930 := [[[[[[[[aux1902 & aux1907] & aux1890] & [y_at_19 = d_at_18]] | [[[aux1903 & aux1908] & aux1891] & [y_at_19 = (y_at_18 + d_at_18)]]] | [[[aux1904 & aux1909] & aux1892] & [y_at_19 = d_at_18]]] | [[[[aux1905 & aux1906] & aux1893] & [y_at_18 >= 1]] & [y_at_19 = (y_at_18 + d_at_18)]]] | [[[[aux1929 & [~ aux1890]] & [~ aux1891]] & [~ aux1892]] & [~ aux1893]]] & [aux1921 & aux1922]].
prop aux1931 := [[cpc1_at_19 <=> cpc1_at_18] & [cpc2_at_19 <=> cpc2_at_18]].
prop aux1932 := [aux1931 & [z_at_19 = (z_at_18 + d_at_18)]].
prop aux1933 := [[[[[[[[aux1910 & aux1915] & aux1886] & [z_at_19 = d_at_18]] | [[[[aux1911 & aux1916] & aux1890] & [z_at_18 = 1]] & [z_at_19 = (z_at_18 + d_at_18)]]] | [[[aux1912 & aux1917] & aux1889] & [z_at_19 = d_at_18]]] | [[[aux1913 & aux1914] & aux1892] & [z_at_19 = (z_at_18 + d_at_18)]]] | [[[[aux1932 & [~ aux1886]] & [~ aux1890]] & [~ aux1889]] & [~ aux1892]]] & [aux1923 & aux1924]].
prop aux1934 := [d_at_18 >= 0].
sat ~[
[[[[[[[aux1001 & aux1002] & aux1003] & [x_at_0 = 0]] & [y_at_0 = 0]] & [z_at_0 = 0]] & [[[[aux1045 & aux1048] & aux1051] & aux1052] & [[[aux1094 & aux1097] & aux1100] & aux1101] & [[[aux1143 & aux1146] & aux1149] & aux1150] & [[[aux1192 & aux1195] & aux1198] & aux1199] & [[[aux1241 & aux1244] & aux1247] & aux1248] & [[[aux1290 & aux1293] & aux1296] & aux1297] & [[[aux1339 & aux1342] & aux1345] & aux1346] & [[[aux1388 & aux1391] & aux1394] & aux1395] & [[[aux1437 & aux1440] & aux1443] & aux1444] & [[[aux1486 & aux1489] & aux1492] & aux1493] & [[[aux1535 & aux1538] & aux1541] & aux1542] & [[[aux1584 & aux1587] & aux1590] & aux1591] & [[[aux1633 & aux1636] & aux1639] & aux1640] & [[[aux1682 & aux1685] & aux1688] & aux1689] & [[[aux1731 & aux1734] & aux1737] & aux1738] & [[[aux1780 & aux1783] & aux1786] & aux1787] & [[[aux1829 & aux1832] & aux1835] & aux1836] & [[[aux1878 & aux1881] & aux1884] & aux1885] & [[[aux1927 & aux1930] & aux1933] & aux1934]] & tt] => [[[[~ tpc1_at_0] & tpc2_at_0] => [[~ gpc1_at_0] & gpc2_at_0]] & [[[~ tpc1_at_1] & tpc2_at_1] => [[~ gpc1_at_1] & gpc2_at_1]] & [[[~ tpc1_at_2] & tpc2_at_2] => [[~ gpc1_at_2] & gpc2_at_2]] & [[[~ tpc1_at_3] & tpc2_at_3] => [[~ gpc1_at_3] & gpc2_at_3]] & [[[~ tpc1_at_4] & tpc2_at_4] => [[~ gpc1_at_4] & gpc2_at_4]] & [[[~ tpc1_at_5] & tpc2_at_5] => [[~ gpc1_at_5] & gpc2_at_5]] & [[[~ tpc1_at_6] & tpc2_at_6] => [[~ gpc1_at_6] & gpc2_at_6]] & [[[~ tpc1_at_7] & tpc2_at_7] => [[~ gpc1_at_7] & gpc2_at_7]] & [[[~ tpc1_at_8] & tpc2_at_8] => [[~ gpc1_at_8] & gpc2_at_8]] & [[[~ tpc1_at_9] & tpc2_at_9] => [[~ gpc1_at_9] & gpc2_at_9]] & [[[~ tpc1_at_10] & tpc2_at_10] => [[~ gpc1_at_10] & gpc2_at_10]] & [[[~ tpc1_at_11] & tpc2_at_11] => [[~ gpc1_at_11] & gpc2_at_11]] & [[[~ tpc1_at_12] & tpc2_at_12] => [[~ gpc1_at_12] & gpc2_at_12]] & [[[~ tpc1_at_13] & tpc2_at_13] => [[~ gpc1_at_13] & gpc2_at_13]] & [[[~ tpc1_at_14] & tpc2_at_14] => [[~ gpc1_at_14] & gpc2_at_14]] & [[[~ tpc1_at_15] & tpc2_at_15] => [[~ gpc1_at_15] & gpc2_at_15]] & [[[~ tpc1_at_16] & tpc2_at_16] => [[~ gpc1_at_16] & gpc2_at_16]] & [[[~ tpc1_at_17] & tpc2_at_17] => [[~ gpc1_at_17] & gpc2_at_17]] & [[[~ tpc1_at_18] & tpc2_at_18] => [[~ gpc1_at_18] & gpc2_at_18]] & [[[~ tpc1_at_19] & tpc2_at_19] => [[~ gpc1_at_19] & gpc2_at_19]]]]].