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].
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]] & 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]]]]].