prop a_0 := [~ [x_0 < 0]] .
prop a_1 := x_0 <= 2 .
prop a_2 := [~ [x_1 < 0]] .
prop a_3 := x_1 <= 2 .
prop a_4 := [~ [x_2 < 0]] .
prop a_5 := x_2 <= 2 .
prop a_6 := [~ [x_3 < 0]] .
prop a_7 := x_3 <= 2 .
prop a_8 := [[~ x_4]] | [[~ x_5]] | [x_2 = 1] .
prop a_9 := [[~ x_6]] | [[~ x_7]] | [x_2 = 2] .
prop a_10 := [[~ x_8]] | [[~ x_9]] | [x_1 = 1] .
prop a_11 := [[~ x_10]] | [[~ x_11]] | [x_1 = 2] .
prop a_12 := [[~ x_12]] | [[~ x_13]] | [x_0 = 1] .
prop a_13 := [[~ x_14]] | [[~ x_15]] | [x_0 = 2] .
prop x_16 := [[~ x_17]] | x_18 .
prop x_19 := [[~ x_20]] | x_21 .
prop x_22 := [[~ x_4]] | x_5 .
prop x_23 := [[~ x_6]] | x_7 .
prop x_24 := [[~ x_8]] | x_9 .
prop x_25 := [[~ x_10]] | x_11 .
prop x_26 := [[~ x_12]] | x_13 .
prop x_27 := [[~ x_14]] | x_15 .
prop a_14 := x_17 | [[~ x_18]] | [x_3 <> 1] | [[x_16 | [[~ [x_28 <= x_28]]]] & [x_19 | [[~ [x_28 <= x_29]]]]] .
prop a_15 := x_20 | [[~ x_21]] | [x_3 <> 2] | [[x_16 | [[~ [x_29 <= x_28]]]] & [x_19 | [[~ [x_29 <= x_29]]]]] .
prop a_16 := x_30 <= x_28 .
prop a_17 := x_30 <= x_29 .
prop a_18 := x_4 | [[~ x_5]] | [x_2 <> 1] | [[x_22 | [[~ [x_31 <= x_31]]]] & [x_23 | [[~ [x_31 <= x_32]]]]] .
prop a_19 := x_6 | [[~ x_7]] | [x_2 <> 2] | [[x_22 | [[~ [x_32 <= x_31]]]] & [x_23 | [[~ [x_32 <= x_32]]]]] .
prop a_20 := x_33 <= x_31 .
prop a_21 := x_33 <= x_32 .
prop a_22 := x_8 | [[~ x_9]] | [x_1 <> 1] | [[x_24 | [[~ [x_34 <= x_34]]]] & [x_25 | [[~ [x_34 <= x_35]]]]] .
prop a_23 := x_10 | [[~ x_11]] | [x_1 <> 2] | [[x_24 | [[~ [x_35 <= x_34]]]] & [x_25 | [[~ [x_35 <= x_35]]]]] .
prop a_24 := x_36 <= x_34 .
prop a_25 := x_36 <= x_35 .
prop a_26 := x_12 | [[~ x_13]] | [x_0 <> 1] | [[x_26 | [[~ [x_37 <= x_37]]]] & [x_27 | [[~ [x_37 <= x_38]]]]] .
prop a_27 := x_14 | [[~ x_15]] | [x_0 <> 2] | [[x_26 | [[~ [x_38 <= x_37]]]] & [x_27 | [[~ [x_38 <= x_38]]]]] .
prop a_28 := x_39 <= x_37 .
prop a_29 := x_39 <= x_38 .
prop x_40 := x_41 = 5 .
prop x_42 := x_3 = x_2 .
prop x_43 := x_3 = 0 .
prop x_44 := x_41 = 3 .
prop x_45 := x_41 = 1 .
prop x_46 := x_2 <> 0 .
prop x_47 := [[~ x_20]] & [[~ x_21]] .
prop x_48 := x_41 = 0 .
prop x_49 := x_41 = 4 .
prop x_50 := [[~ x_17]] & [[~ x_18]] .
prop x_51 := x_41 = 2 .
prop a_30 := x_52 = (x_33 + 2) .
prop x_53 := x_2 = 0 .
prop a_31 := x_54 = (x_33 + 3) .
prop x_55 := [[~ x_6]] & x_7 .
prop x_56 := x_29 = x_32 .
prop x_57 := x_33 < x_28 .
prop x_58 := x_28 = x_31 .
prop x_59 := [x_20 <=> x_6] & [x_21 <=> x_7] .
prop x_60 := x_33 < x_29 .
prop x_61 := [[~ x_4]] & [[~ x_5]] .
prop x_62 := x_33 = x_32 .
prop x_63 := x_33 = x_31 .
prop x_64 := [x_17 <=> x_4] & [x_18 <=> x_5] .
prop x_65 := [[~ x_4]] & x_5 .
prop x_66 := [[~ x_6]] & [[~ x_7]] .
prop a_32 := if [x_32 < x_31] then [x_67 = x_32] else [x_67 = x_31] end .
prop a_33 := x_68 = x_67 .
prop x_69 := x_70 = 5 .
prop x_71 := x_2 = x_1 .
prop x_72 := x_2 = 0 .
prop x_73 := x_70 = 3 .
prop x_74 := x_70 = 1 .
prop x_75 := x_1 <> 0 .
prop x_76 := [[~ x_6]] & [[~ x_7]] .
prop x_77 := x_70 = 0 .
prop x_78 := x_70 = 4 .
prop x_79 := [[~ x_4]] & [[~ x_5]] .
prop x_80 := x_70 = 2 .
prop a_34 := x_81 = (x_36 + 2) .
prop x_82 := x_1 = 0 .
prop a_35 := x_83 = (x_36 + 3) .
prop x_84 := [[~ x_10]] & x_11 .
prop x_85 := x_32 = x_35 .
prop x_86 := x_36 < x_31 .
prop x_87 := x_31 = x_34 .
prop x_88 := [x_6 <=> x_10] & [x_7 <=> x_11] .
prop x_89 := x_36 < x_32 .
prop x_90 := [[~ x_8]] & [[~ x_9]] .
prop x_91 := x_36 = x_35 .
prop x_92 := x_36 = x_34 .
prop x_93 := [x_4 <=> x_8] & [x_5 <=> x_9] .
prop x_94 := [[~ x_8]] & x_9 .
prop x_95 := [[~ x_10]] & [[~ x_11]] .
prop a_36 := if [x_35 < x_34] then [x_96 = x_35] else [x_96 = x_34] end .
prop a_37 := x_97 = x_96 .
prop x_98 := x_99 = 5 .
prop x_100 := x_1 = x_0 .
prop x_101 := x_1 = 0 .
prop x_102 := x_99 = 3 .
prop x_103 := x_99 = 1 .
prop x_104 := x_0 <> 0 .
prop x_105 := [[~ x_10]] & [[~ x_11]] .
prop x_106 := x_99 = 0 .
prop x_107 := x_99 = 4 .
prop x_108 := [[~ x_8]] & [[~ x_9]] .
prop x_109 := x_99 = 2 .
prop a_38 := x_110 = (x_39 + 2) .
prop x_111 := x_0 = 0 .
prop a_39 := x_112 = (x_39 + 3) .
prop x_113 := [[~ x_14]] & x_15 .
prop x_114 := x_35 = x_38 .
prop x_115 := x_39 < x_34 .
prop x_116 := x_34 = x_37 .
prop x_117 := [x_10 <=> x_14] & [x_11 <=> x_15] .
prop x_118 := x_39 < x_35 .
prop x_119 := [[~ x_12]] & [[~ x_13]] .
prop x_120 := x_39 = x_38 .
prop x_121 := x_39 = x_37 .
prop x_122 := [x_8 <=> x_12] & [x_9 <=> x_13] .
prop x_123 := [[~ x_12]] & x_13 .
prop x_124 := [[~ x_14]] & [[~ x_15]] .
prop a_40 := if [x_38 < x_37] then [x_125 = x_38] else [x_125 = x_37] end .
prop a_41 := x_126 = x_125 .
prop a_42 := [[x_127 = 0] & [x_33 < x_68] & [x_30 = x_68] & x_64 & x_59 & x_58 & x_56 & x_42] | [[x_127 = 1] & [[[x_128 = 1] & [[x_48 & x_61 & x_63 & x_53 & x_17 & [[~ x_18]] & [x_33 < x_28] & [x_28 <= x_52] & x_42] | [x_45 & x_61 & x_63 & x_46 & x_57 & x_42 & x_64] | [x_51 & x_4 & [[~ x_5]] & x_63 & [[~ x_17]] & x_18 & [x_3 = 1] & [x_54 <= x_28]] | [x_44 & x_65 & x_63 & [x_2 = 1] & x_17 & x_18 & x_57 & x_42] | [x_49 & x_65 & x_63 & [x_2 <> 1] & x_50 & x_57 & x_42] | [x_40 & x_4 & x_5 & x_63 & x_50 & x_43 & x_57]] & x_59 & x_56] | [[x_128 = 2] & [[x_48 & x_66 & x_62 & x_53 & x_20 & [[~ x_21]] & [x_33 < x_29] & [x_29 <= x_52] & x_42] | [x_45 & x_66 & x_62 & x_46 & x_60 & x_42 & x_59] | [x_51 & x_6 & [[~ x_7]] & x_62 & [[~ x_20]] & x_21 & [x_3 = 2] & [x_54 <= x_29]] | [x_44 & x_55 & x_62 & [x_2 = 2] & x_20 & x_21 & x_60 & x_42] | [x_49 & x_55 & x_62 & [x_2 <> 2] & x_47 & x_60 & x_42] | [x_40 & x_6 & x_7 & x_62 & x_47 & x_43 & x_60]] & x_64 & x_58]] & [x_30 = x_33]] .
prop a_43 := [[x_129 = 0] & [x_36 < x_97] & [x_33 = x_97] & x_93 & x_88 & x_87 & x_85 & x_71] | [[x_129 = 1] & [[[x_130 = 1] & [[x_77 & x_90 & x_92 & x_82 & x_4 & [[~ x_5]] & [x_36 < x_31] & [x_31 <= x_81] & x_71] | [x_74 & x_90 & x_92 & x_75 & x_86 & x_71 & x_93] | [x_80 & x_8 & [[~ x_9]] & x_92 & [[~ x_4]] & x_5 & [x_2 = 1] & [x_83 <= x_31]] | [x_73 & x_94 & x_92 & [x_1 = 1] & x_4 & x_5 & x_86 & x_71] | [x_78 & x_94 & x_92 & [x_1 <> 1] & x_79 & x_86 & x_71] | [x_69 & x_8 & x_9 & x_92 & x_79 & x_72 & x_86]] & x_88 & x_85] | [[x_130 = 2] & [[x_77 & x_95 & x_91 & x_82 & x_6 & [[~ x_7]] & [x_36 < x_32] & [x_32 <= x_81] & x_71] | [x_74 & x_95 & x_91 & x_75 & x_89 & x_71 & x_88] | [x_80 & x_10 & [[~ x_11]] & x_91 & [[~ x_6]] & x_7 & [x_2 = 2] & [x_83 <= x_32]] | [x_73 & x_84 & x_91 & [x_1 = 2] & x_6 & x_7 & x_89 & x_71] | [x_78 & x_84 & x_91 & [x_1 <> 2] & x_76 & x_89 & x_71] | [x_69 & x_10 & x_11 & x_91 & x_76 & x_72 & x_89]] & x_93 & x_87]] & [x_33 = x_36]] .
prop a_44 := [[x_131 = 0] & [x_39 < x_126] & [x_36 = x_126] & x_122 & x_117 & x_116 & x_114 & x_100] | [[x_131 = 1] & [[[x_132 = 1] & [[x_106 & x_119 & x_121 & x_111 & x_8 & [[~ x_9]] & [x_39 < x_34] & [x_34 <= x_110] & x_100] | [x_103 & x_119 & x_121 & x_104 & x_115 & x_100 & x_122] | [x_109 & x_12 & [[~ x_13]] & x_121 & [[~ x_8]] & x_9 & [x_1 = 1] & [x_112 <= x_34]] | [x_102 & x_123 & x_121 & [x_0 = 1] & x_8 & x_9 & x_115 & x_100] | [x_107 & x_123 & x_121 & [x_0 <> 1] & x_108 & x_115 & x_100] | [x_98 & x_12 & x_13 & x_121 & x_108 & x_101 & x_115]] & x_117 & x_114] | [[x_132 = 2] & [[x_106 & x_124 & x_120 & x_111 & x_10 & [[~ x_11]] & [x_39 < x_35] & [x_35 <= x_110] & x_100] | [x_103 & x_124 & x_120 & x_104 & x_118 & x_100 & x_117] | [x_109 & x_14 & [[~ x_15]] & x_120 & [[~ x_10]] & x_11 & [x_1 = 2] & [x_112 <= x_35]] | [x_102 & x_113 & x_120 & [x_0 = 2] & x_10 & x_11 & x_118 & x_100] | [x_107 & x_113 & x_120 & [x_0 <> 2] & x_105 & x_118 & x_100] | [x_98 & x_14 & x_15 & x_120 & x_105 & x_101 & x_118]] & x_122 & x_116]] & [x_36 = x_39]] .
prop a_45 := [x_17 & x_18 & [x_3 <> 1]] | [x_20 & x_21 & [x_3 <> 2]] .
prop a_46 := [x_2 <> x_3] | [x_4 # x_17] | [x_5 # x_18] | [x_6 # x_20] | [x_7 # x_21] | [x_33 <> x_30] | [x_31 <> x_28] | [x_32 <> x_29] .
prop a_47 := [x_1 <> x_3] | [x_8 # x_17] | [x_9 # x_18] | [x_10 # x_20] | [x_11 # x_21] | [x_36 <> x_30] | [x_34 <> x_28] | [x_35 <> x_29] .
prop a_48 := [x_1 <> x_2] | [x_8 # x_4] | [x_9 # x_5] | [x_10 # x_6] | [x_11 # x_7] | [x_36 <> x_33] | [x_34 <> x_31] | [x_35 <> x_32] .
prop a_49 := [x_0 <> x_3] | [x_12 # x_17] | [x_13 # x_18] | [x_14 # x_20] | [x_15 # x_21] | [x_39 <> x_30] | [x_37 <> x_28] | [x_38 <> x_29] .
prop a_50 := [x_0 <> x_2] | [x_12 # x_4] | [x_13 # x_5] | [x_14 # x_6] | [x_15 # x_7] | [x_39 <> x_33] | [x_37 <> x_31] | [x_38 <> x_32] .
prop a_51 := [x_0 <> x_1] | [x_12 # x_8] | [x_13 # x_9] | [x_14 # x_10] | [x_15 # x_11] | [x_39 <> x_36] | [x_37 <> x_34] | [x_38 <> x_35] .
prop bb := 
tt
.
sat 
bb & a_0 & a_1 & a_2 & a_3 & a_4 & a_5 & a_6 & a_7 & a_8 & a_9 & a_10 & a_11 & a_12 & a_13 & a_14 & a_15 & a_16 & a_17 & a_18 & a_19 & a_20 & a_21 & a_22 & a_23 & a_24 & a_25 & a_26 & a_27 & a_28 & a_29 & a_30 & a_31 & a_32 & a_33 & a_34 & a_35 & a_36 & a_37 & a_38 & a_39 & a_40 & a_41 & a_42 & a_43 & a_44 & a_45 & a_46 & a_47 & a_48 & a_49 & a_50 & a_51.