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]]].
sat ~[
[[[aux1001 & aux1002] & [[[aux1005 & aux1004] | [aux1006 & aux1003]] & [[aux1009 & aux1008] | [aux1010 & aux1007]] & [[aux1013 & aux1012] | [aux1014 & aux1011]] & [[aux1017 & aux1016] | [aux1018 & aux1015]]] & 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]]]]]].