prop aux1001 := [[[[~ Wa_at_0] & [~ b_at_0]] & [~ pcw1_at_0]] & [~ pcw2_at_0]].
prop aux1002 := [[[[~ Rb_at_0] & [~ a_at_0]] & [~ pcr1_at_0]] & [~ pcr2_at_0]].
prop aux1003 := [[[[pcw1_at_1 <=> pcw1_at_0] & [pcw2_at_1 <=> pcw2_at_0]] & [Wa_at_1 <=> Wa_at_0]] & [b_at_1 <=> b_at_0]].
prop aux1004 := [[[[pcr1_at_1 <=> pcr1_at_0] & [pcr2_at_1 <=> pcr2_at_0]] & [Rb_at_1 <=> Rb_at_0]] & [a_at_1 <=> a_at_0]].
prop aux1005 := [[[[[[[[~ pcw1_at_0] & [~ pcw2_at_0]] & [Wa_at_1 <=> [~ a_at_0]]] & pcw1_at_1] & [~ pcw2_at_1]] & [b_at_1 <=> b_at_0]] | [[[[[pcw1_at_0 & [~ pcw2_at_0]] & [~ pcw1_at_1]] & pcw2_at_1] & [Wa_at_1 <=> Wa_at_0]] & [b_at_1 <=> b_at_0]]] | [[[[[[~ pcw1_at_0] & pcw2_at_0] & [b_at_1 <=> [~ b_at_0]]] & [~ pcw1_at_1]] & [~ pcw2_at_1]] & [Wa_at_1 <=> Wa_at_0]]].
prop aux1006 := [[[[[[[[~ pcr1_at_0] & [~ pcr2_at_0]] & [a_at_1 <=> [~ a_at_0]]] & pcr1_at_1] & [~ pcr2_at_1]] & [Rb_at_1 <=> Rb_at_0]] | [[[[[pcr1_at_0 & [~ pcr2_at_0]] & [Rb_at_1 <=> [~ b_at_0]]] & [~ pcr1_at_1]] & pcr2_at_1] & [a_at_1 <=> a_at_0]]] | [[[[[[~ pcr1_at_0] & pcr2_at_0] & [~ pcr1_at_1]] & [~ pcr2_at_1]] & [Rb_at_1 <=> Rb_at_0]] & [a_at_1 <=> a_at_0]]].
prop aux1007 := [[[[pcw1_at_2 <=> pcw1_at_1] & [pcw2_at_2 <=> pcw2_at_1]] & [Wa_at_2 <=> Wa_at_1]] & [b_at_2 <=> b_at_1]].
prop aux1008 := [[[[pcr1_at_2 <=> pcr1_at_1] & [pcr2_at_2 <=> pcr2_at_1]] & [Rb_at_2 <=> Rb_at_1]] & [a_at_2 <=> a_at_1]].
prop aux1009 := [[[[[[[[~ pcw1_at_1] & [~ pcw2_at_1]] & [Wa_at_2 <=> [~ a_at_1]]] & pcw1_at_2] & [~ pcw2_at_2]] & [b_at_2 <=> b_at_1]] | [[[[[pcw1_at_1 & [~ pcw2_at_1]] & [~ pcw1_at_2]] & pcw2_at_2] & [Wa_at_2 <=> Wa_at_1]] & [b_at_2 <=> b_at_1]]] | [[[[[[~ pcw1_at_1] & pcw2_at_1] & [b_at_2 <=> [~ b_at_1]]] & [~ pcw1_at_2]] & [~ pcw2_at_2]] & [Wa_at_2 <=> Wa_at_1]]].
prop aux1010 := [[[[[[[[~ pcr1_at_1] & [~ pcr2_at_1]] & [a_at_2 <=> [~ a_at_1]]] & pcr1_at_2] & [~ pcr2_at_2]] & [Rb_at_2 <=> Rb_at_1]] | [[[[[pcr1_at_1 & [~ pcr2_at_1]] & [Rb_at_2 <=> [~ b_at_1]]] & [~ pcr1_at_2]] & pcr2_at_2] & [a_at_2 <=> a_at_1]]] | [[[[[[~ pcr1_at_1] & pcr2_at_1] & [~ pcr1_at_2]] & [~ pcr2_at_2]] & [Rb_at_2 <=> Rb_at_1]] & [a_at_2 <=> a_at_1]]].
prop aux1011 := [[[[pcw1_at_3 <=> pcw1_at_2] & [pcw2_at_3 <=> pcw2_at_2]] & [Wa_at_3 <=> Wa_at_2]] & [b_at_3 <=> b_at_2]].
prop aux1012 := [[[[pcr1_at_3 <=> pcr1_at_2] & [pcr2_at_3 <=> pcr2_at_2]] & [Rb_at_3 <=> Rb_at_2]] & [a_at_3 <=> a_at_2]].
prop aux1013 := [[[[[[[[~ pcw1_at_2] & [~ pcw2_at_2]] & [Wa_at_3 <=> [~ a_at_2]]] & pcw1_at_3] & [~ pcw2_at_3]] & [b_at_3 <=> b_at_2]] | [[[[[pcw1_at_2 & [~ pcw2_at_2]] & [~ pcw1_at_3]] & pcw2_at_3] & [Wa_at_3 <=> Wa_at_2]] & [b_at_3 <=> b_at_2]]] | [[[[[[~ pcw1_at_2] & pcw2_at_2] & [b_at_3 <=> [~ b_at_2]]] & [~ pcw1_at_3]] & [~ pcw2_at_3]] & [Wa_at_3 <=> Wa_at_2]]].
prop aux1014 := [[[[[[[[~ pcr1_at_2] & [~ pcr2_at_2]] & [a_at_3 <=> [~ a_at_2]]] & pcr1_at_3] & [~ pcr2_at_3]] & [Rb_at_3 <=> Rb_at_2]] | [[[[[pcr1_at_2 & [~ pcr2_at_2]] & [Rb_at_3 <=> [~ b_at_2]]] & [~ pcr1_at_3]] & pcr2_at_3] & [a_at_3 <=> a_at_2]]] | [[[[[[~ pcr1_at_2] & pcr2_at_2] & [~ pcr1_at_3]] & [~ pcr2_at_3]] & [Rb_at_3 <=> Rb_at_2]] & [a_at_3 <=> a_at_2]]].
prop aux1015 := [[[[pcw1_at_4 <=> pcw1_at_3] & [pcw2_at_4 <=> pcw2_at_3]] & [Wa_at_4 <=> Wa_at_3]] & [b_at_4 <=> b_at_3]].
prop aux1016 := [[[[pcr1_at_4 <=> pcr1_at_3] & [pcr2_at_4 <=> pcr2_at_3]] & [Rb_at_4 <=> Rb_at_3]] & [a_at_4 <=> a_at_3]].
prop aux1017 := [[[[[[[[~ pcw1_at_3] & [~ pcw2_at_3]] & [Wa_at_4 <=> [~ a_at_3]]] & pcw1_at_4] & [~ pcw2_at_4]] & [b_at_4 <=> b_at_3]] | [[[[[pcw1_at_3 & [~ pcw2_at_3]] & [~ pcw1_at_4]] & pcw2_at_4] & [Wa_at_4 <=> Wa_at_3]] & [b_at_4 <=> b_at_3]]] | [[[[[[~ pcw1_at_3] & pcw2_at_3] & [b_at_4 <=> [~ b_at_3]]] & [~ pcw1_at_4]] & [~ pcw2_at_4]] & [Wa_at_4 <=> Wa_at_3]]].
prop aux1018 := [[[[[[[[~ pcr1_at_3] & [~ pcr2_at_3]] & [a_at_4 <=> [~ a_at_3]]] & pcr1_at_4] & [~ pcr2_at_4]] & [Rb_at_4 <=> Rb_at_3]] | [[[[[pcr1_at_3 & [~ pcr2_at_3]] & [Rb_at_4 <=> [~ b_at_3]]] & [~ pcr1_at_4]] & pcr2_at_4] & [a_at_4 <=> a_at_3]]] | [[[[[[~ pcr1_at_3] & pcr2_at_3] & [~ pcr1_at_4]] & [~ pcr2_at_4]] & [Rb_at_4 <=> Rb_at_3]] & [a_at_4 <=> a_at_3]]].
prop aux1019 := [[[[pcw1_at_5 <=> pcw1_at_4] & [pcw2_at_5 <=> pcw2_at_4]] & [Wa_at_5 <=> Wa_at_4]] & [b_at_5 <=> b_at_4]].
prop aux1020 := [[[[pcr1_at_5 <=> pcr1_at_4] & [pcr2_at_5 <=> pcr2_at_4]] & [Rb_at_5 <=> Rb_at_4]] & [a_at_5 <=> a_at_4]].
prop aux1021 := [[[[[[[[~ pcw1_at_4] & [~ pcw2_at_4]] & [Wa_at_5 <=> [~ a_at_4]]] & pcw1_at_5] & [~ pcw2_at_5]] & [b_at_5 <=> b_at_4]] | [[[[[pcw1_at_4 & [~ pcw2_at_4]] & [~ pcw1_at_5]] & pcw2_at_5] & [Wa_at_5 <=> Wa_at_4]] & [b_at_5 <=> b_at_4]]] | [[[[[[~ pcw1_at_4] & pcw2_at_4] & [b_at_5 <=> [~ b_at_4]]] & [~ pcw1_at_5]] & [~ pcw2_at_5]] & [Wa_at_5 <=> Wa_at_4]]].
prop aux1022 := [[[[[[[[~ pcr1_at_4] & [~ pcr2_at_4]] & [a_at_5 <=> [~ a_at_4]]] & pcr1_at_5] & [~ pcr2_at_5]] & [Rb_at_5 <=> Rb_at_4]] | [[[[[pcr1_at_4 & [~ pcr2_at_4]] & [Rb_at_5 <=> [~ b_at_4]]] & [~ pcr1_at_5]] & pcr2_at_5] & [a_at_5 <=> a_at_4]]] | [[[[[[~ pcr1_at_4] & pcr2_at_4] & [~ pcr1_at_5]] & [~ pcr2_at_5]] & [Rb_at_5 <=> Rb_at_4]] & [a_at_5 <=> a_at_4]]].
prop aux1023 := [[[[pcw1_at_6 <=> pcw1_at_5] & [pcw2_at_6 <=> pcw2_at_5]] & [Wa_at_6 <=> Wa_at_5]] & [b_at_6 <=> b_at_5]].
prop aux1024 := [[[[pcr1_at_6 <=> pcr1_at_5] & [pcr2_at_6 <=> pcr2_at_5]] & [Rb_at_6 <=> Rb_at_5]] & [a_at_6 <=> a_at_5]].
prop aux1025 := [[[[[[[[~ pcw1_at_5] & [~ pcw2_at_5]] & [Wa_at_6 <=> [~ a_at_5]]] & pcw1_at_6] & [~ pcw2_at_6]] & [b_at_6 <=> b_at_5]] | [[[[[pcw1_at_5 & [~ pcw2_at_5]] & [~ pcw1_at_6]] & pcw2_at_6] & [Wa_at_6 <=> Wa_at_5]] & [b_at_6 <=> b_at_5]]] | [[[[[[~ pcw1_at_5] & pcw2_at_5] & [b_at_6 <=> [~ b_at_5]]] & [~ pcw1_at_6]] & [~ pcw2_at_6]] & [Wa_at_6 <=> Wa_at_5]]].
prop aux1026 := [[[[[[[[~ pcr1_at_5] & [~ pcr2_at_5]] & [a_at_6 <=> [~ a_at_5]]] & pcr1_at_6] & [~ pcr2_at_6]] & [Rb_at_6 <=> Rb_at_5]] | [[[[[pcr1_at_5 & [~ pcr2_at_5]] & [Rb_at_6 <=> [~ b_at_5]]] & [~ pcr1_at_6]] & pcr2_at_6] & [a_at_6 <=> a_at_5]]] | [[[[[[~ pcr1_at_5] & pcr2_at_5] & [~ pcr1_at_6]] & [~ pcr2_at_6]] & [Rb_at_6 <=> Rb_at_5]] & [a_at_6 <=> a_at_5]]].
prop aux1027 := [[[[pcw1_at_7 <=> pcw1_at_6] & [pcw2_at_7 <=> pcw2_at_6]] & [Wa_at_7 <=> Wa_at_6]] & [b_at_7 <=> b_at_6]].
prop aux1028 := [[[[pcr1_at_7 <=> pcr1_at_6] & [pcr2_at_7 <=> pcr2_at_6]] & [Rb_at_7 <=> Rb_at_6]] & [a_at_7 <=> a_at_6]].
prop aux1029 := [[[[[[[[~ pcw1_at_6] & [~ pcw2_at_6]] & [Wa_at_7 <=> [~ a_at_6]]] & pcw1_at_7] & [~ pcw2_at_7]] & [b_at_7 <=> b_at_6]] | [[[[[pcw1_at_6 & [~ pcw2_at_6]] & [~ pcw1_at_7]] & pcw2_at_7] & [Wa_at_7 <=> Wa_at_6]] & [b_at_7 <=> b_at_6]]] | [[[[[[~ pcw1_at_6] & pcw2_at_6] & [b_at_7 <=> [~ b_at_6]]] & [~ pcw1_at_7]] & [~ pcw2_at_7]] & [Wa_at_7 <=> Wa_at_6]]].
prop aux1030 := [[[[[[[[~ pcr1_at_6] & [~ pcr2_at_6]] & [a_at_7 <=> [~ a_at_6]]] & pcr1_at_7] & [~ pcr2_at_7]] & [Rb_at_7 <=> Rb_at_6]] | [[[[[pcr1_at_6 & [~ pcr2_at_6]] & [Rb_at_7 <=> [~ b_at_6]]] & [~ pcr1_at_7]] & pcr2_at_7] & [a_at_7 <=> a_at_6]]] | [[[[[[~ pcr1_at_6] & pcr2_at_6] & [~ pcr1_at_7]] & [~ pcr2_at_7]] & [Rb_at_7 <=> Rb_at_6]] & [a_at_7 <=> a_at_6]]].
prop aux1031 := [[[[pcw1_at_8 <=> pcw1_at_7] & [pcw2_at_8 <=> pcw2_at_7]] & [Wa_at_8 <=> Wa_at_7]] & [b_at_8 <=> b_at_7]].
prop aux1032 := [[[[pcr1_at_8 <=> pcr1_at_7] & [pcr2_at_8 <=> pcr2_at_7]] & [Rb_at_8 <=> Rb_at_7]] & [a_at_8 <=> a_at_7]].
prop aux1033 := [[[[[[[[~ pcw1_at_7] & [~ pcw2_at_7]] & [Wa_at_8 <=> [~ a_at_7]]] & pcw1_at_8] & [~ pcw2_at_8]] & [b_at_8 <=> b_at_7]] | [[[[[pcw1_at_7 & [~ pcw2_at_7]] & [~ pcw1_at_8]] & pcw2_at_8] & [Wa_at_8 <=> Wa_at_7]] & [b_at_8 <=> b_at_7]]] | [[[[[[~ pcw1_at_7] & pcw2_at_7] & [b_at_8 <=> [~ b_at_7]]] & [~ pcw1_at_8]] & [~ pcw2_at_8]] & [Wa_at_8 <=> Wa_at_7]]].
prop aux1034 := [[[[[[[[~ pcr1_at_7] & [~ pcr2_at_7]] & [a_at_8 <=> [~ a_at_7]]] & pcr1_at_8] & [~ pcr2_at_8]] & [Rb_at_8 <=> Rb_at_7]] | [[[[[pcr1_at_7 & [~ pcr2_at_7]] & [Rb_at_8 <=> [~ b_at_7]]] & [~ pcr1_at_8]] & pcr2_at_8] & [a_at_8 <=> a_at_7]]] | [[[[[[~ pcr1_at_7] & pcr2_at_7] & [~ pcr1_at_8]] & [~ pcr2_at_8]] & [Rb_at_8 <=> Rb_at_7]] & [a_at_8 <=> a_at_7]]].
prop aux1035 := [[[[pcw1_at_9 <=> pcw1_at_8] & [pcw2_at_9 <=> pcw2_at_8]] & [Wa_at_9 <=> Wa_at_8]] & [b_at_9 <=> b_at_8]].
prop aux1036 := [[[[pcr1_at_9 <=> pcr1_at_8] & [pcr2_at_9 <=> pcr2_at_8]] & [Rb_at_9 <=> Rb_at_8]] & [a_at_9 <=> a_at_8]].
prop aux1037 := [[[[[[[[~ pcw1_at_8] & [~ pcw2_at_8]] & [Wa_at_9 <=> [~ a_at_8]]] & pcw1_at_9] & [~ pcw2_at_9]] & [b_at_9 <=> b_at_8]] | [[[[[pcw1_at_8 & [~ pcw2_at_8]] & [~ pcw1_at_9]] & pcw2_at_9] & [Wa_at_9 <=> Wa_at_8]] & [b_at_9 <=> b_at_8]]] | [[[[[[~ pcw1_at_8] & pcw2_at_8] & [b_at_9 <=> [~ b_at_8]]] & [~ pcw1_at_9]] & [~ pcw2_at_9]] & [Wa_at_9 <=> Wa_at_8]]].
prop aux1038 := [[[[[[[[~ pcr1_at_8] & [~ pcr2_at_8]] & [a_at_9 <=> [~ a_at_8]]] & pcr1_at_9] & [~ pcr2_at_9]] & [Rb_at_9 <=> Rb_at_8]] | [[[[[pcr1_at_8 & [~ pcr2_at_8]] & [Rb_at_9 <=> [~ b_at_8]]] & [~ pcr1_at_9]] & pcr2_at_9] & [a_at_9 <=> a_at_8]]] | [[[[[[~ pcr1_at_8] & pcr2_at_8] & [~ pcr1_at_9]] & [~ pcr2_at_9]] & [Rb_at_9 <=> Rb_at_8]] & [a_at_9 <=> a_at_8]]].
prop aux1039 := [[[[pcw1_at_10 <=> pcw1_at_9] & [pcw2_at_10 <=> pcw2_at_9]] & [Wa_at_10 <=> Wa_at_9]] & [b_at_10 <=> b_at_9]].
prop aux1040 := [[[[pcr1_at_10 <=> pcr1_at_9] & [pcr2_at_10 <=> pcr2_at_9]] & [Rb_at_10 <=> Rb_at_9]] & [a_at_10 <=> a_at_9]].
prop aux1041 := [[[[[[[[~ pcw1_at_9] & [~ pcw2_at_9]] & [Wa_at_10 <=> [~ a_at_9]]] & pcw1_at_10] & [~ pcw2_at_10]] & [b_at_10 <=> b_at_9]] | [[[[[pcw1_at_9 & [~ pcw2_at_9]] & [~ pcw1_at_10]] & pcw2_at_10] & [Wa_at_10 <=> Wa_at_9]] & [b_at_10 <=> b_at_9]]] | [[[[[[~ pcw1_at_9] & pcw2_at_9] & [b_at_10 <=> [~ b_at_9]]] & [~ pcw1_at_10]] & [~ pcw2_at_10]] & [Wa_at_10 <=> Wa_at_9]]].
prop aux1042 := [[[[[[[[~ pcr1_at_9] & [~ pcr2_at_9]] & [a_at_10 <=> [~ a_at_9]]] & pcr1_at_10] & [~ pcr2_at_10]] & [Rb_at_10 <=> Rb_at_9]] | [[[[[pcr1_at_9 & [~ pcr2_at_9]] & [Rb_at_10 <=> [~ b_at_9]]] & [~ pcr1_at_10]] & pcr2_at_10] & [a_at_10 <=> a_at_9]]] | [[[[[[~ pcr1_at_9] & pcr2_at_9] & [~ pcr1_at_10]] & [~ pcr2_at_10]] & [Rb_at_10 <=> Rb_at_9]] & [a_at_10 <=> a_at_9]]].
prop aux1043 := [[[[pcw1_at_11 <=> pcw1_at_10] & [pcw2_at_11 <=> pcw2_at_10]] & [Wa_at_11 <=> Wa_at_10]] & [b_at_11 <=> b_at_10]].
prop aux1044 := [[[[pcr1_at_11 <=> pcr1_at_10] & [pcr2_at_11 <=> pcr2_at_10]] & [Rb_at_11 <=> Rb_at_10]] & [a_at_11 <=> a_at_10]].
prop aux1045 := [[[[[[[[~ pcw1_at_10] & [~ pcw2_at_10]] & [Wa_at_11 <=> [~ a_at_10]]] & pcw1_at_11] & [~ pcw2_at_11]] & [b_at_11 <=> b_at_10]] | [[[[[pcw1_at_10 & [~ pcw2_at_10]] & [~ pcw1_at_11]] & pcw2_at_11] & [Wa_at_11 <=> Wa_at_10]] & [b_at_11 <=> b_at_10]]] | [[[[[[~ pcw1_at_10] & pcw2_at_10] & [b_at_11 <=> [~ b_at_10]]] & [~ pcw1_at_11]] & [~ pcw2_at_11]] & [Wa_at_11 <=> Wa_at_10]]].
prop aux1046 := [[[[[[[[~ pcr1_at_10] & [~ pcr2_at_10]] & [a_at_11 <=> [~ a_at_10]]] & pcr1_at_11] & [~ pcr2_at_11]] & [Rb_at_11 <=> Rb_at_10]] | [[[[[pcr1_at_10 & [~ pcr2_at_10]] & [Rb_at_11 <=> [~ b_at_10]]] & [~ pcr1_at_11]] & pcr2_at_11] & [a_at_11 <=> a_at_10]]] | [[[[[[~ pcr1_at_10] & pcr2_at_10] & [~ pcr1_at_11]] & [~ pcr2_at_11]] & [Rb_at_11 <=> Rb_at_10]] & [a_at_11 <=> a_at_10]]].
prop aux1047 := [[[[pcw1_at_12 <=> pcw1_at_11] & [pcw2_at_12 <=> pcw2_at_11]] & [Wa_at_12 <=> Wa_at_11]] & [b_at_12 <=> b_at_11]].
prop aux1048 := [[[[pcr1_at_12 <=> pcr1_at_11] & [pcr2_at_12 <=> pcr2_at_11]] & [Rb_at_12 <=> Rb_at_11]] & [a_at_12 <=> a_at_11]].
prop aux1049 := [[[[[[[[~ pcw1_at_11] & [~ pcw2_at_11]] & [Wa_at_12 <=> [~ a_at_11]]] & pcw1_at_12] & [~ pcw2_at_12]] & [b_at_12 <=> b_at_11]] | [[[[[pcw1_at_11 & [~ pcw2_at_11]] & [~ pcw1_at_12]] & pcw2_at_12] & [Wa_at_12 <=> Wa_at_11]] & [b_at_12 <=> b_at_11]]] | [[[[[[~ pcw1_at_11] & pcw2_at_11] & [b_at_12 <=> [~ b_at_11]]] & [~ pcw1_at_12]] & [~ pcw2_at_12]] & [Wa_at_12 <=> Wa_at_11]]].
prop aux1050 := [[[[[[[[~ pcr1_at_11] & [~ pcr2_at_11]] & [a_at_12 <=> [~ a_at_11]]] & pcr1_at_12] & [~ pcr2_at_12]] & [Rb_at_12 <=> Rb_at_11]] | [[[[[pcr1_at_11 & [~ pcr2_at_11]] & [Rb_at_12 <=> [~ b_at_11]]] & [~ pcr1_at_12]] & pcr2_at_12] & [a_at_12 <=> a_at_11]]] | [[[[[[~ pcr1_at_11] & pcr2_at_11] & [~ pcr1_at_12]] & [~ pcr2_at_12]] & [Rb_at_12 <=> Rb_at_11]] & [a_at_12 <=> a_at_11]]].
prop aux1051 := [[[[pcw1_at_13 <=> pcw1_at_12] & [pcw2_at_13 <=> pcw2_at_12]] & [Wa_at_13 <=> Wa_at_12]] & [b_at_13 <=> b_at_12]].
prop aux1052 := [[[[pcr1_at_13 <=> pcr1_at_12] & [pcr2_at_13 <=> pcr2_at_12]] & [Rb_at_13 <=> Rb_at_12]] & [a_at_13 <=> a_at_12]].
prop aux1053 := [[[[[[[[~ pcw1_at_12] & [~ pcw2_at_12]] & [Wa_at_13 <=> [~ a_at_12]]] & pcw1_at_13] & [~ pcw2_at_13]] & [b_at_13 <=> b_at_12]] | [[[[[pcw1_at_12 & [~ pcw2_at_12]] & [~ pcw1_at_13]] & pcw2_at_13] & [Wa_at_13 <=> Wa_at_12]] & [b_at_13 <=> b_at_12]]] | [[[[[[~ pcw1_at_12] & pcw2_at_12] & [b_at_13 <=> [~ b_at_12]]] & [~ pcw1_at_13]] & [~ pcw2_at_13]] & [Wa_at_13 <=> Wa_at_12]]].
prop aux1054 := [[[[[[[[~ pcr1_at_12] & [~ pcr2_at_12]] & [a_at_13 <=> [~ a_at_12]]] & pcr1_at_13] & [~ pcr2_at_13]] & [Rb_at_13 <=> Rb_at_12]] | [[[[[pcr1_at_12 & [~ pcr2_at_12]] & [Rb_at_13 <=> [~ b_at_12]]] & [~ pcr1_at_13]] & pcr2_at_13] & [a_at_13 <=> a_at_12]]] | [[[[[[~ pcr1_at_12] & pcr2_at_12] & [~ pcr1_at_13]] & [~ pcr2_at_13]] & [Rb_at_13 <=> Rb_at_12]] & [a_at_13 <=> a_at_12]]].
prop aux1055 := [[[[pcw1_at_14 <=> pcw1_at_13] & [pcw2_at_14 <=> pcw2_at_13]] & [Wa_at_14 <=> Wa_at_13]] & [b_at_14 <=> b_at_13]].
prop aux1056 := [[[[pcr1_at_14 <=> pcr1_at_13] & [pcr2_at_14 <=> pcr2_at_13]] & [Rb_at_14 <=> Rb_at_13]] & [a_at_14 <=> a_at_13]].
prop aux1057 := [[[[[[[[~ pcw1_at_13] & [~ pcw2_at_13]] & [Wa_at_14 <=> [~ a_at_13]]] & pcw1_at_14] & [~ pcw2_at_14]] & [b_at_14 <=> b_at_13]] | [[[[[pcw1_at_13 & [~ pcw2_at_13]] & [~ pcw1_at_14]] & pcw2_at_14] & [Wa_at_14 <=> Wa_at_13]] & [b_at_14 <=> b_at_13]]] | [[[[[[~ pcw1_at_13] & pcw2_at_13] & [b_at_14 <=> [~ b_at_13]]] & [~ pcw1_at_14]] & [~ pcw2_at_14]] & [Wa_at_14 <=> Wa_at_13]]].
prop aux1058 := [[[[[[[[~ pcr1_at_13] & [~ pcr2_at_13]] & [a_at_14 <=> [~ a_at_13]]] & pcr1_at_14] & [~ pcr2_at_14]] & [Rb_at_14 <=> Rb_at_13]] | [[[[[pcr1_at_13 & [~ pcr2_at_13]] & [Rb_at_14 <=> [~ b_at_13]]] & [~ pcr1_at_14]] & pcr2_at_14] & [a_at_14 <=> a_at_13]]] | [[[[[[~ pcr1_at_13] & pcr2_at_13] & [~ pcr1_at_14]] & [~ pcr2_at_14]] & [Rb_at_14 <=> Rb_at_13]] & [a_at_14 <=> a_at_13]]].
prop aux1059 := [[[[pcw1_at_15 <=> pcw1_at_14] & [pcw2_at_15 <=> pcw2_at_14]] & [Wa_at_15 <=> Wa_at_14]] & [b_at_15 <=> b_at_14]].
prop aux1060 := [[[[pcr1_at_15 <=> pcr1_at_14] & [pcr2_at_15 <=> pcr2_at_14]] & [Rb_at_15 <=> Rb_at_14]] & [a_at_15 <=> a_at_14]].
prop aux1061 := [[[[[[[[~ pcw1_at_14] & [~ pcw2_at_14]] & [Wa_at_15 <=> [~ a_at_14]]] & pcw1_at_15] & [~ pcw2_at_15]] & [b_at_15 <=> b_at_14]] | [[[[[pcw1_at_14 & [~ pcw2_at_14]] & [~ pcw1_at_15]] & pcw2_at_15] & [Wa_at_15 <=> Wa_at_14]] & [b_at_15 <=> b_at_14]]] | [[[[[[~ pcw1_at_14] & pcw2_at_14] & [b_at_15 <=> [~ b_at_14]]] & [~ pcw1_at_15]] & [~ pcw2_at_15]] & [Wa_at_15 <=> Wa_at_14]]].
prop aux1062 := [[[[[[[[~ pcr1_at_14] & [~ pcr2_at_14]] & [a_at_15 <=> [~ a_at_14]]] & pcr1_at_15] & [~ pcr2_at_15]] & [Rb_at_15 <=> Rb_at_14]] | [[[[[pcr1_at_14 & [~ pcr2_at_14]] & [Rb_at_15 <=> [~ b_at_14]]] & [~ pcr1_at_15]] & pcr2_at_15] & [a_at_15 <=> a_at_14]]] | [[[[[[~ pcr1_at_14] & pcr2_at_14] & [~ pcr1_at_15]] & [~ pcr2_at_15]] & [Rb_at_15 <=> Rb_at_14]] & [a_at_15 <=> a_at_14]]].
prop aux1063 := [[[[pcw1_at_16 <=> pcw1_at_15] & [pcw2_at_16 <=> pcw2_at_15]] & [Wa_at_16 <=> Wa_at_15]] & [b_at_16 <=> b_at_15]].
prop aux1064 := [[[[pcr1_at_16 <=> pcr1_at_15] & [pcr2_at_16 <=> pcr2_at_15]] & [Rb_at_16 <=> Rb_at_15]] & [a_at_16 <=> a_at_15]].
prop aux1065 := [[[[[[[[~ pcw1_at_15] & [~ pcw2_at_15]] & [Wa_at_16 <=> [~ a_at_15]]] & pcw1_at_16] & [~ pcw2_at_16]] & [b_at_16 <=> b_at_15]] | [[[[[pcw1_at_15 & [~ pcw2_at_15]] & [~ pcw1_at_16]] & pcw2_at_16] & [Wa_at_16 <=> Wa_at_15]] & [b_at_16 <=> b_at_15]]] | [[[[[[~ pcw1_at_15] & pcw2_at_15] & [b_at_16 <=> [~ b_at_15]]] & [~ pcw1_at_16]] & [~ pcw2_at_16]] & [Wa_at_16 <=> Wa_at_15]]].
prop aux1066 := [[[[[[[[~ pcr1_at_15] & [~ pcr2_at_15]] & [a_at_16 <=> [~ a_at_15]]] & pcr1_at_16] & [~ pcr2_at_16]] & [Rb_at_16 <=> Rb_at_15]] | [[[[[pcr1_at_15 & [~ pcr2_at_15]] & [Rb_at_16 <=> [~ b_at_15]]] & [~ pcr1_at_16]] & pcr2_at_16] & [a_at_16 <=> a_at_15]]] | [[[[[[~ pcr1_at_15] & pcr2_at_15] & [~ pcr1_at_16]] & [~ pcr2_at_16]] & [Rb_at_16 <=> Rb_at_15]] & [a_at_16 <=> a_at_15]]].
prop aux1067 := [[[[pcw1_at_17 <=> pcw1_at_16] & [pcw2_at_17 <=> pcw2_at_16]] & [Wa_at_17 <=> Wa_at_16]] & [b_at_17 <=> b_at_16]].
prop aux1068 := [[[[pcr1_at_17 <=> pcr1_at_16] & [pcr2_at_17 <=> pcr2_at_16]] & [Rb_at_17 <=> Rb_at_16]] & [a_at_17 <=> a_at_16]].
prop aux1069 := [[[[[[[[~ pcw1_at_16] & [~ pcw2_at_16]] & [Wa_at_17 <=> [~ a_at_16]]] & pcw1_at_17] & [~ pcw2_at_17]] & [b_at_17 <=> b_at_16]] | [[[[[pcw1_at_16 & [~ pcw2_at_16]] & [~ pcw1_at_17]] & pcw2_at_17] & [Wa_at_17 <=> Wa_at_16]] & [b_at_17 <=> b_at_16]]] | [[[[[[~ pcw1_at_16] & pcw2_at_16] & [b_at_17 <=> [~ b_at_16]]] & [~ pcw1_at_17]] & [~ pcw2_at_17]] & [Wa_at_17 <=> Wa_at_16]]].
prop aux1070 := [[[[[[[[~ pcr1_at_16] & [~ pcr2_at_16]] & [a_at_17 <=> [~ a_at_16]]] & pcr1_at_17] & [~ pcr2_at_17]] & [Rb_at_17 <=> Rb_at_16]] | [[[[[pcr1_at_16 & [~ pcr2_at_16]] & [Rb_at_17 <=> [~ b_at_16]]] & [~ pcr1_at_17]] & pcr2_at_17] & [a_at_17 <=> a_at_16]]] | [[[[[[~ pcr1_at_16] & pcr2_at_16] & [~ pcr1_at_17]] & [~ pcr2_at_17]] & [Rb_at_17 <=> Rb_at_16]] & [a_at_17 <=> a_at_16]]].
prop aux1071 := [[[[pcw1_at_18 <=> pcw1_at_17] & [pcw2_at_18 <=> pcw2_at_17]] & [Wa_at_18 <=> Wa_at_17]] & [b_at_18 <=> b_at_17]].
prop aux1072 := [[[[pcr1_at_18 <=> pcr1_at_17] & [pcr2_at_18 <=> pcr2_at_17]] & [Rb_at_18 <=> Rb_at_17]] & [a_at_18 <=> a_at_17]].
prop aux1073 := [[[[[[[[~ pcw1_at_17] & [~ pcw2_at_17]] & [Wa_at_18 <=> [~ a_at_17]]] & pcw1_at_18] & [~ pcw2_at_18]] & [b_at_18 <=> b_at_17]] | [[[[[pcw1_at_17 & [~ pcw2_at_17]] & [~ pcw1_at_18]] & pcw2_at_18] & [Wa_at_18 <=> Wa_at_17]] & [b_at_18 <=> b_at_17]]] | [[[[[[~ pcw1_at_17] & pcw2_at_17] & [b_at_18 <=> [~ b_at_17]]] & [~ pcw1_at_18]] & [~ pcw2_at_18]] & [Wa_at_18 <=> Wa_at_17]]].
prop aux1074 := [[[[[[[[~ pcr1_at_17] & [~ pcr2_at_17]] & [a_at_18 <=> [~ a_at_17]]] & pcr1_at_18] & [~ pcr2_at_18]] & [Rb_at_18 <=> Rb_at_17]] | [[[[[pcr1_at_17 & [~ pcr2_at_17]] & [Rb_at_18 <=> [~ b_at_17]]] & [~ pcr1_at_18]] & pcr2_at_18] & [a_at_18 <=> a_at_17]]] | [[[[[[~ pcr1_at_17] & pcr2_at_17] & [~ pcr1_at_18]] & [~ pcr2_at_18]] & [Rb_at_18 <=> Rb_at_17]] & [a_at_18 <=> a_at_17]]].
prop aux1075 := [[[[pcw1_at_19 <=> pcw1_at_18] & [pcw2_at_19 <=> pcw2_at_18]] & [Wa_at_19 <=> Wa_at_18]] & [b_at_19 <=> b_at_18]].
prop aux1076 := [[[[pcr1_at_19 <=> pcr1_at_18] & [pcr2_at_19 <=> pcr2_at_18]] & [Rb_at_19 <=> Rb_at_18]] & [a_at_19 <=> a_at_18]].
prop aux1077 := [[[[[[[[~ pcw1_at_18] & [~ pcw2_at_18]] & [Wa_at_19 <=> [~ a_at_18]]] & pcw1_at_19] & [~ pcw2_at_19]] & [b_at_19 <=> b_at_18]] | [[[[[pcw1_at_18 & [~ pcw2_at_18]] & [~ pcw1_at_19]] & pcw2_at_19] & [Wa_at_19 <=> Wa_at_18]] & [b_at_19 <=> b_at_18]]] | [[[[[[~ pcw1_at_18] & pcw2_at_18] & [b_at_19 <=> [~ b_at_18]]] & [~ pcw1_at_19]] & [~ pcw2_at_19]] & [Wa_at_19 <=> Wa_at_18]]].
prop aux1078 := [[[[[[[[~ pcr1_at_18] & [~ pcr2_at_18]] & [a_at_19 <=> [~ a_at_18]]] & pcr1_at_19] & [~ pcr2_at_19]] & [Rb_at_19 <=> Rb_at_18]] | [[[[[pcr1_at_18 & [~ pcr2_at_18]] & [Rb_at_19 <=> [~ b_at_18]]] & [~ pcr1_at_19]] & pcr2_at_19] & [a_at_19 <=> a_at_18]]] | [[[[[[~ pcr1_at_18] & pcr2_at_18] & [~ pcr1_at_19]] & [~ pcr2_at_19]] & [Rb_at_19 <=> Rb_at_18]] & [a_at_19 <=> a_at_18]]].
sat ~[
[[[aux1001 & aux1002] & [[[aux1005 & aux1004] | [aux1006 & aux1003]] & [[aux1009 & aux1008] | [aux1010 & aux1007]] & [[aux1013 & aux1012] | [aux1014 & aux1011]] & [[aux1017 & aux1016] | [aux1018 & aux1015]] & [[aux1021 & aux1020] | [aux1022 & aux1019]] & [[aux1025 & aux1024] | [aux1026 & aux1023]] & [[aux1029 & aux1028] | [aux1030 & aux1027]] & [[aux1033 & aux1032] | [aux1034 & aux1031]] & [[aux1037 & aux1036] | [aux1038 & aux1035]] & [[aux1041 & aux1040] | [aux1042 & aux1039]] & [[aux1045 & aux1044] | [aux1046 & aux1043]] & [[aux1049 & aux1048] | [aux1050 & aux1047]] & [[aux1053 & aux1052] | [aux1054 & aux1051]] & [[aux1057 & aux1056] | [aux1058 & aux1055]] & [[aux1061 & aux1060] | [aux1062 & aux1059]] & [[aux1065 & aux1064] | [aux1066 & aux1063]] & [[aux1069 & aux1068] | [aux1070 & aux1067]] & [[aux1073 & aux1072] | [aux1074 & aux1071]] & [[aux1077 & aux1076] | [aux1078 & aux1075]]] & tt] => [[[[[pcw1_at_0 & [~ pcw2_at_0]] & [~ pcr1_at_0]] & pcr2_at_0] => [[a_at_0 # Wa_at_0] | [b_at_0 # Rb_at_0]]] & [[[[pcw1_at_1 & [~ pcw2_at_1]] & [~ pcr1_at_1]] & pcr2_at_1] => [[a_at_1 # Wa_at_1] | [b_at_1 # Rb_at_1]]] & [[[[pcw1_at_2 & [~ pcw2_at_2]] & [~ pcr1_at_2]] & pcr2_at_2] => [[a_at_2 # Wa_at_2] | [b_at_2 # Rb_at_2]]] & [[[[pcw1_at_3 & [~ pcw2_at_3]] & [~ pcr1_at_3]] & pcr2_at_3] => [[a_at_3 # Wa_at_3] | [b_at_3 # Rb_at_3]]] & [[[[pcw1_at_4 & [~ pcw2_at_4]] & [~ pcr1_at_4]] & pcr2_at_4] => [[a_at_4 # Wa_at_4] | [b_at_4 # Rb_at_4]]] & [[[[pcw1_at_5 & [~ pcw2_at_5]] & [~ pcr1_at_5]] & pcr2_at_5] => [[a_at_5 # Wa_at_5] | [b_at_5 # Rb_at_5]]] & [[[[pcw1_at_6 & [~ pcw2_at_6]] & [~ pcr1_at_6]] & pcr2_at_6] => [[a_at_6 # Wa_at_6] | [b_at_6 # Rb_at_6]]] & [[[[pcw1_at_7 & [~ pcw2_at_7]] & [~ pcr1_at_7]] & pcr2_at_7] => [[a_at_7 # Wa_at_7] | [b_at_7 # Rb_at_7]]] & [[[[pcw1_at_8 & [~ pcw2_at_8]] & [~ pcr1_at_8]] & pcr2_at_8] => [[a_at_8 # Wa_at_8] | [b_at_8 # Rb_at_8]]] & [[[[pcw1_at_9 & [~ pcw2_at_9]] & [~ pcr1_at_9]] & pcr2_at_9] => [[a_at_9 # Wa_at_9] | [b_at_9 # Rb_at_9]]] & [[[[pcw1_at_10 & [~ pcw2_at_10]] & [~ pcr1_at_10]] & pcr2_at_10] => [[a_at_10 # Wa_at_10] | [b_at_10 # Rb_at_10]]] & [[[[pcw1_at_11 & [~ pcw2_at_11]] & [~ pcr1_at_11]] & pcr2_at_11] => [[a_at_11 # Wa_at_11] | [b_at_11 # Rb_at_11]]] & [[[[pcw1_at_12 & [~ pcw2_at_12]] & [~ pcr1_at_12]] & pcr2_at_12] => [[a_at_12 # Wa_at_12] | [b_at_12 # Rb_at_12]]] & [[[[pcw1_at_13 & [~ pcw2_at_13]] & [~ pcr1_at_13]] & pcr2_at_13] => [[a_at_13 # Wa_at_13] | [b_at_13 # Rb_at_13]]] & [[[[pcw1_at_14 & [~ pcw2_at_14]] & [~ pcr1_at_14]] & pcr2_at_14] => [[a_at_14 # Wa_at_14] | [b_at_14 # Rb_at_14]]] & [[[[pcw1_at_15 & [~ pcw2_at_15]] & [~ pcr1_at_15]] & pcr2_at_15] => [[a_at_15 # Wa_at_15] | [b_at_15 # Rb_at_15]]] & [[[[pcw1_at_16 & [~ pcw2_at_16]] & [~ pcr1_at_16]] & pcr2_at_16] => [[a_at_16 # Wa_at_16] | [b_at_16 # Rb_at_16]]] & [[[[pcw1_at_17 & [~ pcw2_at_17]] & [~ pcr1_at_17]] & pcr2_at_17] => [[a_at_17 # Wa_at_17] | [b_at_17 # Rb_at_17]]] & [[[[pcw1_at_18 & [~ pcw2_at_18]] & [~ pcr1_at_18]] & pcr2_at_18] => [[a_at_18 # Wa_at_18] | [b_at_18 # Rb_at_18]]] & [[[[pcw1_at_19 & [~ pcw2_at_19]] & [~ pcr1_at_19]] & pcr2_at_19] => [[a_at_19 # Wa_at_19] | [b_at_19 # Rb_at_19]]]]]].