prop aux1001 := [~ pc_at_0].
prop aux1002 := [[[[d_at_0 >= 0] & [x_at_0 = d_at_0]] & [y_at_0 = d_at_0]] & [z_at_0 = d_at_0]].
prop aux1003 := [x_at_0 <= 1].
prop aux1004 := [~ pc_at_0].
prop aux1005 := pc_at_0.
prop aux1006 := [~ pc_at_1].
prop aux1007 := pc_at_1.
prop aux1008 := [[aux1004 & aux1007] & [x_aux_at_1 = 0]].
prop aux1009 := [[[aux1005 & aux1006] & [x_at_0 >= 30]] & [x_aux_at_1 = 0]].
prop aux1010 := [aux1008 | aux1009].
prop aux1011 := [[[[d_at_1 >= 0] & [x_at_1 = (x_aux_at_1 + d_at_1)]] & [y_at_1 = (y_at_0 + d_at_1)]] & [[aux1006 & [z_at_1 = (z_at_0 + d_at_1)]] | [aux1007 & [z_at_1 = z_at_0]]]].
prop aux1012 := [aux1006 => [x_at_1 <= 1]].
prop aux1013 := [~ pc_at_1].
prop aux1014 := pc_at_1.
prop aux1015 := [~ pc_at_2].
prop aux1016 := pc_at_2.
prop aux1017 := [[aux1013 & aux1016] & [x_aux_at_2 = 0]].
prop aux1018 := [[[aux1014 & aux1015] & [x_at_1 >= 30]] & [x_aux_at_2 = 0]].
prop aux1019 := [aux1017 | aux1018].
prop aux1020 := [[[[d_at_2 >= 0] & [x_at_2 = (x_aux_at_2 + d_at_2)]] & [y_at_2 = (y_at_1 + d_at_2)]] & [[aux1015 & [z_at_2 = (z_at_1 + d_at_2)]] | [aux1016 & [z_at_2 = z_at_1]]]].
prop aux1021 := [aux1015 => [x_at_2 <= 1]].
prop aux1022 := [~ pc_at_2].
prop aux1023 := pc_at_2.
prop aux1024 := [~ pc_at_3].
prop aux1025 := pc_at_3.
prop aux1026 := [[aux1022 & aux1025] & [x_aux_at_3 = 0]].
prop aux1027 := [[[aux1023 & aux1024] & [x_at_2 >= 30]] & [x_aux_at_3 = 0]].
prop aux1028 := [aux1026 | aux1027].
prop aux1029 := [[[[d_at_3 >= 0] & [x_at_3 = (x_aux_at_3 + d_at_3)]] & [y_at_3 = (y_at_2 + d_at_3)]] & [[aux1024 & [z_at_3 = (z_at_2 + d_at_3)]] | [aux1025 & [z_at_3 = z_at_2]]]].
prop aux1030 := [aux1024 => [x_at_3 <= 1]].
prop aux1031 := [~ pc_at_3].
prop aux1032 := pc_at_3.
prop aux1033 := [~ pc_at_4].
prop aux1034 := pc_at_4.
prop aux1035 := [[aux1031 & aux1034] & [x_aux_at_4 = 0]].
prop aux1036 := [[[aux1032 & aux1033] & [x_at_3 >= 30]] & [x_aux_at_4 = 0]].
prop aux1037 := [aux1035 | aux1036].
prop aux1038 := [[[[d_at_4 >= 0] & [x_at_4 = (x_aux_at_4 + d_at_4)]] & [y_at_4 = (y_at_3 + d_at_4)]] & [[aux1033 & [z_at_4 = (z_at_3 + d_at_4)]] | [aux1034 & [z_at_4 = z_at_3]]]].
prop aux1039 := [aux1033 => [x_at_4 <= 1]].
prop aux1040 := [~ pc_at_4].
prop aux1041 := pc_at_4.
prop aux1042 := [~ pc_at_5].
prop aux1043 := pc_at_5.
prop aux1044 := [[aux1040 & aux1043] & [x_aux_at_5 = 0]].
prop aux1045 := [[[aux1041 & aux1042] & [x_at_4 >= 30]] & [x_aux_at_5 = 0]].
prop aux1046 := [aux1044 | aux1045].
prop aux1047 := [[[[d_at_5 >= 0] & [x_at_5 = (x_aux_at_5 + d_at_5)]] & [y_at_5 = (y_at_4 + d_at_5)]] & [[aux1042 & [z_at_5 = (z_at_4 + d_at_5)]] | [aux1043 & [z_at_5 = z_at_4]]]].
prop aux1048 := [aux1042 => [x_at_5 <= 1]].
prop aux1049 := [~ pc_at_5].
prop aux1050 := pc_at_5.
prop aux1051 := [~ pc_at_6].
prop aux1052 := pc_at_6.
prop aux1053 := [[aux1049 & aux1052] & [x_aux_at_6 = 0]].
prop aux1054 := [[[aux1050 & aux1051] & [x_at_5 >= 30]] & [x_aux_at_6 = 0]].
prop aux1055 := [aux1053 | aux1054].
prop aux1056 := [[[[d_at_6 >= 0] & [x_at_6 = (x_aux_at_6 + d_at_6)]] & [y_at_6 = (y_at_5 + d_at_6)]] & [[aux1051 & [z_at_6 = (z_at_5 + d_at_6)]] | [aux1052 & [z_at_6 = z_at_5]]]].
prop aux1057 := [aux1051 => [x_at_6 <= 1]].
prop aux1058 := [~ pc_at_6].
prop aux1059 := pc_at_6.
prop aux1060 := [~ pc_at_7].
prop aux1061 := pc_at_7.
prop aux1062 := [[aux1058 & aux1061] & [x_aux_at_7 = 0]].
prop aux1063 := [[[aux1059 & aux1060] & [x_at_6 >= 30]] & [x_aux_at_7 = 0]].
prop aux1064 := [aux1062 | aux1063].
prop aux1065 := [[[[d_at_7 >= 0] & [x_at_7 = (x_aux_at_7 + d_at_7)]] & [y_at_7 = (y_at_6 + d_at_7)]] & [[aux1060 & [z_at_7 = (z_at_6 + d_at_7)]] | [aux1061 & [z_at_7 = z_at_6]]]].
prop aux1066 := [aux1060 => [x_at_7 <= 1]].
prop aux1067 := [~ pc_at_7].
prop aux1068 := pc_at_7.
prop aux1069 := [~ pc_at_8].
prop aux1070 := pc_at_8.
prop aux1071 := [[aux1067 & aux1070] & [x_aux_at_8 = 0]].
prop aux1072 := [[[aux1068 & aux1069] & [x_at_7 >= 30]] & [x_aux_at_8 = 0]].
prop aux1073 := [aux1071 | aux1072].
prop aux1074 := [[[[d_at_8 >= 0] & [x_at_8 = (x_aux_at_8 + d_at_8)]] & [y_at_8 = (y_at_7 + d_at_8)]] & [[aux1069 & [z_at_8 = (z_at_7 + d_at_8)]] | [aux1070 & [z_at_8 = z_at_7]]]].
prop aux1075 := [aux1069 => [x_at_8 <= 1]].
prop aux1076 := [~ pc_at_8].
prop aux1077 := pc_at_8.
prop aux1078 := [~ pc_at_9].
prop aux1079 := pc_at_9.
prop aux1080 := [[aux1076 & aux1079] & [x_aux_at_9 = 0]].
prop aux1081 := [[[aux1077 & aux1078] & [x_at_8 >= 30]] & [x_aux_at_9 = 0]].
prop aux1082 := [aux1080 | aux1081].
prop aux1083 := [[[[d_at_9 >= 0] & [x_at_9 = (x_aux_at_9 + d_at_9)]] & [y_at_9 = (y_at_8 + d_at_9)]] & [[aux1078 & [z_at_9 = (z_at_8 + d_at_9)]] | [aux1079 & [z_at_9 = z_at_8]]]].
prop aux1084 := [aux1078 => [x_at_9 <= 1]].
prop aux1085 := [~ pc_at_9].
prop aux1086 := pc_at_9.
prop aux1087 := [~ pc_at_10].
prop aux1088 := pc_at_10.
prop aux1089 := [[aux1085 & aux1088] & [x_aux_at_10 = 0]].
prop aux1090 := [[[aux1086 & aux1087] & [x_at_9 >= 30]] & [x_aux_at_10 = 0]].
prop aux1091 := [aux1089 | aux1090].
prop aux1092 := [[[[d_at_10 >= 0] & [x_at_10 = (x_aux_at_10 + d_at_10)]] & [y_at_10 = (y_at_9 + d_at_10)]] & [[aux1087 & [z_at_10 = (z_at_9 + d_at_10)]] | [aux1088 & [z_at_10 = z_at_9]]]].
prop aux1093 := [aux1087 => [x_at_10 <= 1]].
prop aux1094 := [~ pc_at_10].
prop aux1095 := pc_at_10.
prop aux1096 := [~ pc_at_11].
prop aux1097 := pc_at_11.
prop aux1098 := [[aux1094 & aux1097] & [x_aux_at_11 = 0]].
prop aux1099 := [[[aux1095 & aux1096] & [x_at_10 >= 30]] & [x_aux_at_11 = 0]].
prop aux1100 := [aux1098 | aux1099].
prop aux1101 := [[[[d_at_11 >= 0] & [x_at_11 = (x_aux_at_11 + d_at_11)]] & [y_at_11 = (y_at_10 + d_at_11)]] & [[aux1096 & [z_at_11 = (z_at_10 + d_at_11)]] | [aux1097 & [z_at_11 = z_at_10]]]].
prop aux1102 := [aux1096 => [x_at_11 <= 1]].
prop aux1103 := [~ pc_at_11].
prop aux1104 := pc_at_11.
prop aux1105 := [~ pc_at_12].
prop aux1106 := pc_at_12.
prop aux1107 := [[aux1103 & aux1106] & [x_aux_at_12 = 0]].
prop aux1108 := [[[aux1104 & aux1105] & [x_at_11 >= 30]] & [x_aux_at_12 = 0]].
prop aux1109 := [aux1107 | aux1108].
prop aux1110 := [[[[d_at_12 >= 0] & [x_at_12 = (x_aux_at_12 + d_at_12)]] & [y_at_12 = (y_at_11 + d_at_12)]] & [[aux1105 & [z_at_12 = (z_at_11 + d_at_12)]] | [aux1106 & [z_at_12 = z_at_11]]]].
prop aux1111 := [aux1105 => [x_at_12 <= 1]].
prop aux1112 := [~ pc_at_12].
prop aux1113 := pc_at_12.
prop aux1114 := [~ pc_at_13].
prop aux1115 := pc_at_13.
prop aux1116 := [[aux1112 & aux1115] & [x_aux_at_13 = 0]].
prop aux1117 := [[[aux1113 & aux1114] & [x_at_12 >= 30]] & [x_aux_at_13 = 0]].
prop aux1118 := [aux1116 | aux1117].
prop aux1119 := [[[[d_at_13 >= 0] & [x_at_13 = (x_aux_at_13 + d_at_13)]] & [y_at_13 = (y_at_12 + d_at_13)]] & [[aux1114 & [z_at_13 = (z_at_12 + d_at_13)]] | [aux1115 & [z_at_13 = z_at_12]]]].
prop aux1120 := [aux1114 => [x_at_13 <= 1]].
prop aux1121 := [~ pc_at_13].
prop aux1122 := pc_at_13.
prop aux1123 := [~ pc_at_14].
prop aux1124 := pc_at_14.
prop aux1125 := [[aux1121 & aux1124] & [x_aux_at_14 = 0]].
prop aux1126 := [[[aux1122 & aux1123] & [x_at_13 >= 30]] & [x_aux_at_14 = 0]].
prop aux1127 := [aux1125 | aux1126].
prop aux1128 := [[[[d_at_14 >= 0] & [x_at_14 = (x_aux_at_14 + d_at_14)]] & [y_at_14 = (y_at_13 + d_at_14)]] & [[aux1123 & [z_at_14 = (z_at_13 + d_at_14)]] | [aux1124 & [z_at_14 = z_at_13]]]].
prop aux1129 := [aux1123 => [x_at_14 <= 1]].
prop aux1130 := [~ pc_at_14].
prop aux1131 := pc_at_14.
prop aux1132 := [~ pc_at_15].
prop aux1133 := pc_at_15.
prop aux1134 := [[aux1130 & aux1133] & [x_aux_at_15 = 0]].
prop aux1135 := [[[aux1131 & aux1132] & [x_at_14 >= 30]] & [x_aux_at_15 = 0]].
prop aux1136 := [aux1134 | aux1135].
prop aux1137 := [[[[d_at_15 >= 0] & [x_at_15 = (x_aux_at_15 + d_at_15)]] & [y_at_15 = (y_at_14 + d_at_15)]] & [[aux1132 & [z_at_15 = (z_at_14 + d_at_15)]] | [aux1133 & [z_at_15 = z_at_14]]]].
prop aux1138 := [aux1132 => [x_at_15 <= 1]].
prop aux1139 := [~ pc_at_15].
prop aux1140 := pc_at_15.
prop aux1141 := [~ pc_at_16].
prop aux1142 := pc_at_16.
prop aux1143 := [[aux1139 & aux1142] & [x_aux_at_16 = 0]].
prop aux1144 := [[[aux1140 & aux1141] & [x_at_15 >= 30]] & [x_aux_at_16 = 0]].
prop aux1145 := [aux1143 | aux1144].
prop aux1146 := [[[[d_at_16 >= 0] & [x_at_16 = (x_aux_at_16 + d_at_16)]] & [y_at_16 = (y_at_15 + d_at_16)]] & [[aux1141 & [z_at_16 = (z_at_15 + d_at_16)]] | [aux1142 & [z_at_16 = z_at_15]]]].
prop aux1147 := [aux1141 => [x_at_16 <= 1]].
prop aux1148 := [~ pc_at_16].
prop aux1149 := pc_at_16.
prop aux1150 := [~ pc_at_17].
prop aux1151 := pc_at_17.
prop aux1152 := [[aux1148 & aux1151] & [x_aux_at_17 = 0]].
prop aux1153 := [[[aux1149 & aux1150] & [x_at_16 >= 30]] & [x_aux_at_17 = 0]].
prop aux1154 := [aux1152 | aux1153].
prop aux1155 := [[[[d_at_17 >= 0] & [x_at_17 = (x_aux_at_17 + d_at_17)]] & [y_at_17 = (y_at_16 + d_at_17)]] & [[aux1150 & [z_at_17 = (z_at_16 + d_at_17)]] | [aux1151 & [z_at_17 = z_at_16]]]].
prop aux1156 := [aux1150 => [x_at_17 <= 1]].
prop aux1157 := [~ pc_at_17].
prop aux1158 := pc_at_17.
prop aux1159 := [~ pc_at_18].
prop aux1160 := pc_at_18.
prop aux1161 := [[aux1157 & aux1160] & [x_aux_at_18 = 0]].
prop aux1162 := [[[aux1158 & aux1159] & [x_at_17 >= 30]] & [x_aux_at_18 = 0]].
prop aux1163 := [aux1161 | aux1162].
prop aux1164 := [[[[d_at_18 >= 0] & [x_at_18 = (x_aux_at_18 + d_at_18)]] & [y_at_18 = (y_at_17 + d_at_18)]] & [[aux1159 & [z_at_18 = (z_at_17 + d_at_18)]] | [aux1160 & [z_at_18 = z_at_17]]]].
prop aux1165 := [aux1159 => [x_at_18 <= 1]].
prop aux1166 := [~ pc_at_18].
prop aux1167 := pc_at_18.
prop aux1168 := [~ pc_at_19].
prop aux1169 := pc_at_19.
prop aux1170 := [[aux1166 & aux1169] & [x_aux_at_19 = 0]].
prop aux1171 := [[[aux1167 & aux1168] & [x_at_18 >= 30]] & [x_aux_at_19 = 0]].
prop aux1172 := [aux1170 | aux1171].
prop aux1173 := [[[[d_at_19 >= 0] & [x_at_19 = (x_aux_at_19 + d_at_19)]] & [y_at_19 = (y_at_18 + d_at_19)]] & [[aux1168 & [z_at_19 = (z_at_18 + d_at_19)]] | [aux1169 & [z_at_19 = z_at_18]]]].
prop aux1174 := [aux1168 => [x_at_19 <= 1]].
sat ~[
[[[[[aux1001 & aux1002] & aux1003] & [counter_at_0 = 0]] & [[[[aux1010 & aux1011] & aux1012] & [[[counter_at_0 < 4] & [counter_at_1 = (counter_at_0 + 1)]] | [[counter_at_0 >= 4] & [counter_at_1 = counter_at_0]]]] & [[[aux1019 & aux1020] & aux1021] & [[[counter_at_1 < 4] & [counter_at_2 = (counter_at_1 + 1)]] | [[counter_at_1 >= 4] & [counter_at_2 = counter_at_1]]]] & [[[aux1028 & aux1029] & aux1030] & [[[counter_at_2 < 4] & [counter_at_3 = (counter_at_2 + 1)]] | [[counter_at_2 >= 4] & [counter_at_3 = counter_at_2]]]] & [[[aux1037 & aux1038] & aux1039] & [[[counter_at_3 < 4] & [counter_at_4 = (counter_at_3 + 1)]] | [[counter_at_3 >= 4] & [counter_at_4 = counter_at_3]]]] & [[[aux1046 & aux1047] & aux1048] & [[[counter_at_4 < 4] & [counter_at_5 = (counter_at_4 + 1)]] | [[counter_at_4 >= 4] & [counter_at_5 = counter_at_4]]]] & [[[aux1055 & aux1056] & aux1057] & [[[counter_at_5 < 4] & [counter_at_6 = (counter_at_5 + 1)]] | [[counter_at_5 >= 4] & [counter_at_6 = counter_at_5]]]] & [[[aux1064 & aux1065] & aux1066] & [[[counter_at_6 < 4] & [counter_at_7 = (counter_at_6 + 1)]] | [[counter_at_6 >= 4] & [counter_at_7 = counter_at_6]]]] & [[[aux1073 & aux1074] & aux1075] & [[[counter_at_7 < 4] & [counter_at_8 = (counter_at_7 + 1)]] | [[counter_at_7 >= 4] & [counter_at_8 = counter_at_7]]]] & [[[aux1082 & aux1083] & aux1084] & [[[counter_at_8 < 4] & [counter_at_9 = (counter_at_8 + 1)]] | [[counter_at_8 >= 4] & [counter_at_9 = counter_at_8]]]] & [[[aux1091 & aux1092] & aux1093] & [[[counter_at_9 < 4] & [counter_at_10 = (counter_at_9 + 1)]] | [[counter_at_9 >= 4] & [counter_at_10 = counter_at_9]]]] & [[[aux1100 & aux1101] & aux1102] & [[[counter_at_10 < 4] & [counter_at_11 = (counter_at_10 + 1)]] | [[counter_at_10 >= 4] & [counter_at_11 = counter_at_10]]]] & [[[aux1109 & aux1110] & aux1111] & [[[counter_at_11 < 4] & [counter_at_12 = (counter_at_11 + 1)]] | [[counter_at_11 >= 4] & [counter_at_12 = counter_at_11]]]] & [[[aux1118 & aux1119] & aux1120] & [[[counter_at_12 < 4] & [counter_at_13 = (counter_at_12 + 1)]] | [[counter_at_12 >= 4] & [counter_at_13 = counter_at_12]]]] & [[[aux1127 & aux1128] & aux1129] & [[[counter_at_13 < 4] & [counter_at_14 = (counter_at_13 + 1)]] | [[counter_at_13 >= 4] & [counter_at_14 = counter_at_13]]]] & [[[aux1136 & aux1137] & aux1138] & [[[counter_at_14 < 4] & [counter_at_15 = (counter_at_14 + 1)]] | [[counter_at_14 >= 4] & [counter_at_15 = counter_at_14]]]] & [[[aux1145 & aux1146] & aux1147] & [[[counter_at_15 < 4] & [counter_at_16 = (counter_at_15 + 1)]] | [[counter_at_15 >= 4] & [counter_at_16 = counter_at_15]]]] & [[[aux1154 & aux1155] & aux1156] & [[[counter_at_16 < 4] & [counter_at_17 = (counter_at_16 + 1)]] | [[counter_at_16 >= 4] & [counter_at_17 = counter_at_16]]]] & [[[aux1163 & aux1164] & aux1165] & [[[counter_at_17 < 4] & [counter_at_18 = (counter_at_17 + 1)]] | [[counter_at_17 >= 4] & [counter_at_18 = counter_at_17]]]] & [[[aux1172 & aux1173] & aux1174] & [[[counter_at_18 < 4] & [counter_at_19 = (counter_at_18 + 1)]] | [[counter_at_18 >= 4] & [counter_at_19 = counter_at_18]]]]] & tt] => [[[y_at_0 >= 60] => [(20 * z_at_0) <= y_at_0]] & [[y_at_1 >= 60] => [(20 * z_at_1) <= y_at_1]] & [[y_at_2 >= 60] => [(20 * z_at_2) <= y_at_2]] & [[y_at_3 >= 60] => [(20 * z_at_3) <= y_at_3]] & [[y_at_4 >= 60] => [(20 * z_at_4) <= y_at_4]] & [[y_at_5 >= 60] => [(20 * z_at_5) <= y_at_5]] & [[y_at_6 >= 60] => [(20 * z_at_6) <= y_at_6]] & [[y_at_7 >= 60] => [(20 * z_at_7) <= y_at_7]] & [[y_at_8 >= 60] => [(20 * z_at_8) <= y_at_8]] & [[y_at_9 >= 60] => [(20 * z_at_9) <= y_at_9]] & [[y_at_10 >= 60] => [(20 * z_at_10) <= y_at_10]] & [[y_at_11 >= 60] => [(20 * z_at_11) <= y_at_11]] & [[y_at_12 >= 60] => [(20 * z_at_12) <= y_at_12]] & [[y_at_13 >= 60] => [(20 * z_at_13) <= y_at_13]] & [[y_at_14 >= 60] => [(20 * z_at_14) <= y_at_14]] & [[y_at_15 >= 60] => [(20 * z_at_15) <= y_at_15]] & [[y_at_16 >= 60] => [(20 * z_at_16) <= y_at_16]] & [[y_at_17 >= 60] => [(20 * z_at_17) <= y_at_17]] & [[y_at_18 >= 60] => [(20 * z_at_18) <= y_at_18]] & [[y_at_19 >= 60] => [(20 * z_at_19) <= y_at_19]]]]].