prop aux1001 := [[~ pc11_at_0] & [~ pc12_at_0]].
prop aux1002 := [pc11_at_0 & [~ pc12_at_0]].
prop aux1003 := [[~ pc11_at_0] & pc12_at_0].
prop aux1004 := [pc11_at_0 & pc12_at_0].
prop aux1005 := [[~ pc11_at_1] & [~ pc12_at_1]].
prop aux1006 := [pc11_at_1 & [~ pc12_at_1]].
prop aux1007 := [[~ pc11_at_1] & pc12_at_1].
prop aux1008 := [pc11_at_1 & pc12_at_1].
prop aux1009 := [[~ pc21_at_0] & [~ pc22_at_0]].
prop aux1010 := [pc21_at_0 & [~ pc22_at_0]].
prop aux1011 := [[~ pc21_at_0] & pc22_at_0].
prop aux1012 := [pc21_at_0 & pc22_at_0].
prop aux1013 := [[~ pc21_at_1] & [~ pc22_at_1]].
prop aux1014 := [pc21_at_1 & [~ pc22_at_1]].
prop aux1015 := [[~ pc21_at_1] & pc22_at_1].
prop aux1016 := [pc21_at_1 & pc22_at_1].
prop aux1017 := [[~ k1_at_0] & [~ k2_at_0]].
prop aux1018 := [k1_at_0 & [~ k2_at_0]].
prop aux1019 := [[~ k1_at_0] & k2_at_0].
prop aux1020 := [[~ k1_at_1] & [~ k2_at_1]].
prop aux1021 := [k1_at_1 & [~ k2_at_1]].
prop aux1022 := [[~ k1_at_1] & k2_at_1].
prop aux1023 := [[k1_at_1 <=> k1_at_0] & [k2_at_1 <=> k2_at_0]].
prop aux1024 := [aux1006 => [x_at_1 < a]].
prop aux1025 := [aux1014 => [y_at_1 < a]].
prop aux1026 := [[pc11_at_1 <=> pc11_at_0] & [pc12_at_1 <=> pc12_at_0]].
prop aux1027 := [[pc21_at_1 <=> pc21_at_0] & [pc22_at_1 <=> pc22_at_0]].
prop aux1028 := [aux1026 & [x_aux_at_1 = x_at_0]].
prop aux1029 := [aux1027 & [y_aux_at_1 = y_at_0]].
prop aux1030 := [[[[[[[[aux1001 & aux1006] & aux1017] & [x_aux_at_1 = 0]] & aux1023] | [[[aux1002 & aux1007] & [x_aux_at_1 = 0]] & aux1021]] | [[[[[aux1003 & aux1008] & [x_at_0 > b]] & aux1018] & [x_aux_at_1 = x_at_0]] & aux1023]] | [[[[[aux1003 & aux1006] & [x_at_0 > b]] & [~ aux1018]] & [x_aux_at_1 = x_at_0]] & aux1023]] | [[[aux1004 & aux1006] & [x_aux_at_1 = x_at_0]] & aux1020]].
prop aux1031 := [[[[[[[[aux1009 & aux1014] & aux1017] & [y_aux_at_1 = 0]] & aux1023] | [[[aux1010 & aux1015] & [y_aux_at_1 = 0]] & aux1022]] | [[[[[aux1011 & aux1016] & [y_at_0 > b]] & aux1019] & [y_aux_at_1 = y_at_0]] & aux1023]] | [[[[[aux1011 & aux1014] & [y_at_0 > b]] & [~ aux1019]] & [y_aux_at_1 = y_at_0]] & aux1023]] | [[[aux1012 & aux1014] & [y_aux_at_1 = y_at_0]] & aux1020]].
prop aux1032 := [[[d_at_1 >= 0] & [x_at_1 = (x_aux_at_1 + d_at_1)]] & [(10 * y_at_1) = ((10 * y_aux_at_1) + (11 * d_at_1))]].
prop aux1033 := [[aux1030 & aux1029] | [aux1031 & aux1028]].
prop aux1034 := [[~ pc11_at_1] & [~ pc12_at_1]].
prop aux1035 := [pc11_at_1 & [~ pc12_at_1]].
prop aux1036 := [[~ pc11_at_1] & pc12_at_1].
prop aux1037 := [pc11_at_1 & pc12_at_1].
prop aux1038 := [[~ pc11_at_2] & [~ pc12_at_2]].
prop aux1039 := [pc11_at_2 & [~ pc12_at_2]].
prop aux1040 := [[~ pc11_at_2] & pc12_at_2].
prop aux1041 := [pc11_at_2 & pc12_at_2].
prop aux1042 := [[~ pc21_at_1] & [~ pc22_at_1]].
prop aux1043 := [pc21_at_1 & [~ pc22_at_1]].
prop aux1044 := [[~ pc21_at_1] & pc22_at_1].
prop aux1045 := [pc21_at_1 & pc22_at_1].
prop aux1046 := [[~ pc21_at_2] & [~ pc22_at_2]].
prop aux1047 := [pc21_at_2 & [~ pc22_at_2]].
prop aux1048 := [[~ pc21_at_2] & pc22_at_2].
prop aux1049 := [pc21_at_2 & pc22_at_2].
prop aux1050 := [[~ k1_at_1] & [~ k2_at_1]].
prop aux1051 := [k1_at_1 & [~ k2_at_1]].
prop aux1052 := [[~ k1_at_1] & k2_at_1].
prop aux1053 := [[~ k1_at_2] & [~ k2_at_2]].
prop aux1054 := [k1_at_2 & [~ k2_at_2]].
prop aux1055 := [[~ k1_at_2] & k2_at_2].
prop aux1056 := [[k1_at_2 <=> k1_at_1] & [k2_at_2 <=> k2_at_1]].
prop aux1057 := [aux1039 => [x_at_2 < a]].
prop aux1058 := [aux1047 => [y_at_2 < a]].
prop aux1059 := [[pc11_at_2 <=> pc11_at_1] & [pc12_at_2 <=> pc12_at_1]].
prop aux1060 := [[pc21_at_2 <=> pc21_at_1] & [pc22_at_2 <=> pc22_at_1]].
prop aux1061 := [aux1059 & [x_aux_at_2 = x_at_1]].
prop aux1062 := [aux1060 & [y_aux_at_2 = y_at_1]].
prop aux1063 := [[[[[[[[aux1034 & aux1039] & aux1050] & [x_aux_at_2 = 0]] & aux1056] | [[[aux1035 & aux1040] & [x_aux_at_2 = 0]] & aux1054]] | [[[[[aux1036 & aux1041] & [x_at_1 > b]] & aux1051] & [x_aux_at_2 = x_at_1]] & aux1056]] | [[[[[aux1036 & aux1039] & [x_at_1 > b]] & [~ aux1051]] & [x_aux_at_2 = x_at_1]] & aux1056]] | [[[aux1037 & aux1039] & [x_aux_at_2 = x_at_1]] & aux1053]].
prop aux1064 := [[[[[[[[aux1042 & aux1047] & aux1050] & [y_aux_at_2 = 0]] & aux1056] | [[[aux1043 & aux1048] & [y_aux_at_2 = 0]] & aux1055]] | [[[[[aux1044 & aux1049] & [y_at_1 > b]] & aux1052] & [y_aux_at_2 = y_at_1]] & aux1056]] | [[[[[aux1044 & aux1047] & [y_at_1 > b]] & [~ aux1052]] & [y_aux_at_2 = y_at_1]] & aux1056]] | [[[aux1045 & aux1047] & [y_aux_at_2 = y_at_1]] & aux1053]].
prop aux1065 := [[[d_at_2 >= 0] & [x_at_2 = (x_aux_at_2 + d_at_2)]] & [(10 * y_at_2) = ((10 * y_aux_at_2) + (11 * d_at_2))]].
prop aux1066 := [[aux1063 & aux1062] | [aux1064 & aux1061]].
prop aux1067 := [[~ pc11_at_2] & [~ pc12_at_2]].
prop aux1068 := [pc11_at_2 & [~ pc12_at_2]].
prop aux1069 := [[~ pc11_at_2] & pc12_at_2].
prop aux1070 := [pc11_at_2 & pc12_at_2].
prop aux1071 := [[~ pc11_at_3] & [~ pc12_at_3]].
prop aux1072 := [pc11_at_3 & [~ pc12_at_3]].
prop aux1073 := [[~ pc11_at_3] & pc12_at_3].
prop aux1074 := [pc11_at_3 & pc12_at_3].
prop aux1075 := [[~ pc21_at_2] & [~ pc22_at_2]].
prop aux1076 := [pc21_at_2 & [~ pc22_at_2]].
prop aux1077 := [[~ pc21_at_2] & pc22_at_2].
prop aux1078 := [pc21_at_2 & pc22_at_2].
prop aux1079 := [[~ pc21_at_3] & [~ pc22_at_3]].
prop aux1080 := [pc21_at_3 & [~ pc22_at_3]].
prop aux1081 := [[~ pc21_at_3] & pc22_at_3].
prop aux1082 := [pc21_at_3 & pc22_at_3].
prop aux1083 := [[~ k1_at_2] & [~ k2_at_2]].
prop aux1084 := [k1_at_2 & [~ k2_at_2]].
prop aux1085 := [[~ k1_at_2] & k2_at_2].
prop aux1086 := [[~ k1_at_3] & [~ k2_at_3]].
prop aux1087 := [k1_at_3 & [~ k2_at_3]].
prop aux1088 := [[~ k1_at_3] & k2_at_3].
prop aux1089 := [[k1_at_3 <=> k1_at_2] & [k2_at_3 <=> k2_at_2]].
prop aux1090 := [aux1072 => [x_at_3 < a]].
prop aux1091 := [aux1080 => [y_at_3 < a]].
prop aux1092 := [[pc11_at_3 <=> pc11_at_2] & [pc12_at_3 <=> pc12_at_2]].
prop aux1093 := [[pc21_at_3 <=> pc21_at_2] & [pc22_at_3 <=> pc22_at_2]].
prop aux1094 := [aux1092 & [x_aux_at_3 = x_at_2]].
prop aux1095 := [aux1093 & [y_aux_at_3 = y_at_2]].
prop aux1096 := [[[[[[[[aux1067 & aux1072] & aux1083] & [x_aux_at_3 = 0]] & aux1089] | [[[aux1068 & aux1073] & [x_aux_at_3 = 0]] & aux1087]] | [[[[[aux1069 & aux1074] & [x_at_2 > b]] & aux1084] & [x_aux_at_3 = x_at_2]] & aux1089]] | [[[[[aux1069 & aux1072] & [x_at_2 > b]] & [~ aux1084]] & [x_aux_at_3 = x_at_2]] & aux1089]] | [[[aux1070 & aux1072] & [x_aux_at_3 = x_at_2]] & aux1086]].
prop aux1097 := [[[[[[[[aux1075 & aux1080] & aux1083] & [y_aux_at_3 = 0]] & aux1089] | [[[aux1076 & aux1081] & [y_aux_at_3 = 0]] & aux1088]] | [[[[[aux1077 & aux1082] & [y_at_2 > b]] & aux1085] & [y_aux_at_3 = y_at_2]] & aux1089]] | [[[[[aux1077 & aux1080] & [y_at_2 > b]] & [~ aux1085]] & [y_aux_at_3 = y_at_2]] & aux1089]] | [[[aux1078 & aux1080] & [y_aux_at_3 = y_at_2]] & aux1086]].
prop aux1098 := [[[d_at_3 >= 0] & [x_at_3 = (x_aux_at_3 + d_at_3)]] & [(10 * y_at_3) = ((10 * y_aux_at_3) + (11 * d_at_3))]].
prop aux1099 := [[aux1096 & aux1095] | [aux1097 & aux1094]].
prop aux1100 := [[~ pc11_at_3] & [~ pc12_at_3]].
prop aux1101 := [pc11_at_3 & [~ pc12_at_3]].
prop aux1102 := [[~ pc11_at_3] & pc12_at_3].
prop aux1103 := [pc11_at_3 & pc12_at_3].
prop aux1104 := [[~ pc11_at_4] & [~ pc12_at_4]].
prop aux1105 := [pc11_at_4 & [~ pc12_at_4]].
prop aux1106 := [[~ pc11_at_4] & pc12_at_4].
prop aux1107 := [pc11_at_4 & pc12_at_4].
prop aux1108 := [[~ pc21_at_3] & [~ pc22_at_3]].
prop aux1109 := [pc21_at_3 & [~ pc22_at_3]].
prop aux1110 := [[~ pc21_at_3] & pc22_at_3].
prop aux1111 := [pc21_at_3 & pc22_at_3].
prop aux1112 := [[~ pc21_at_4] & [~ pc22_at_4]].
prop aux1113 := [pc21_at_4 & [~ pc22_at_4]].
prop aux1114 := [[~ pc21_at_4] & pc22_at_4].
prop aux1115 := [pc21_at_4 & pc22_at_4].
prop aux1116 := [[~ k1_at_3] & [~ k2_at_3]].
prop aux1117 := [k1_at_3 & [~ k2_at_3]].
prop aux1118 := [[~ k1_at_3] & k2_at_3].
prop aux1119 := [[~ k1_at_4] & [~ k2_at_4]].
prop aux1120 := [k1_at_4 & [~ k2_at_4]].
prop aux1121 := [[~ k1_at_4] & k2_at_4].
prop aux1122 := [[k1_at_4 <=> k1_at_3] & [k2_at_4 <=> k2_at_3]].
prop aux1123 := [aux1105 => [x_at_4 < a]].
prop aux1124 := [aux1113 => [y_at_4 < a]].
prop aux1125 := [[pc11_at_4 <=> pc11_at_3] & [pc12_at_4 <=> pc12_at_3]].
prop aux1126 := [[pc21_at_4 <=> pc21_at_3] & [pc22_at_4 <=> pc22_at_3]].
prop aux1127 := [aux1125 & [x_aux_at_4 = x_at_3]].
prop aux1128 := [aux1126 & [y_aux_at_4 = y_at_3]].
prop aux1129 := [[[[[[[[aux1100 & aux1105] & aux1116] & [x_aux_at_4 = 0]] & aux1122] | [[[aux1101 & aux1106] & [x_aux_at_4 = 0]] & aux1120]] | [[[[[aux1102 & aux1107] & [x_at_3 > b]] & aux1117] & [x_aux_at_4 = x_at_3]] & aux1122]] | [[[[[aux1102 & aux1105] & [x_at_3 > b]] & [~ aux1117]] & [x_aux_at_4 = x_at_3]] & aux1122]] | [[[aux1103 & aux1105] & [x_aux_at_4 = x_at_3]] & aux1119]].
prop aux1130 := [[[[[[[[aux1108 & aux1113] & aux1116] & [y_aux_at_4 = 0]] & aux1122] | [[[aux1109 & aux1114] & [y_aux_at_4 = 0]] & aux1121]] | [[[[[aux1110 & aux1115] & [y_at_3 > b]] & aux1118] & [y_aux_at_4 = y_at_3]] & aux1122]] | [[[[[aux1110 & aux1113] & [y_at_3 > b]] & [~ aux1118]] & [y_aux_at_4 = y_at_3]] & aux1122]] | [[[aux1111 & aux1113] & [y_aux_at_4 = y_at_3]] & aux1119]].
prop aux1131 := [[[d_at_4 >= 0] & [x_at_4 = (x_aux_at_4 + d_at_4)]] & [(10 * y_at_4) = ((10 * y_aux_at_4) + (11 * d_at_4))]].
prop aux1132 := [[aux1129 & aux1128] | [aux1130 & aux1127]].
sat ~[
[[[[[[[[[~ pc11_at_0] & [~ pc12_at_0]] & [~ pc21_at_0]] & [~ pc22_at_0]] & [d_at_0 >= 0]] & [x_at_0 = d_at_0]] & [(10 * y_at_0) = (11 * d_at_0)]] & [[[[aux1033 & aux1032] & aux1024] & aux1025] & [[[aux1066 & aux1065] & aux1057] & aux1058] & [[[aux1099 & aux1098] & aux1090] & aux1091] & [[[aux1132 & aux1131] & aux1123] & aux1124]] & tt] => [[[(11 * a) < (10 * b)] => [~ [[[pc11_at_0 & pc12_at_0] & pc21_at_0] & pc22_at_0]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_1 & pc12_at_1] & pc21_at_1] & pc22_at_1]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_2 & pc12_at_2] & pc21_at_2] & pc22_at_2]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_3 & pc12_at_3] & pc21_at_3] & pc22_at_3]]] & [[(11 * a) < (10 * b)] => [~ [[[pc11_at_4 & pc12_at_4] & pc21_at_4] & pc22_at_4]]]]]].