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