s = Solver()
s_0 = Real('s_0')
s_1 = Real('s_1')
s_2 = Real('s_2')
s_3 = Real('s_3')
s_0_1 = Int('s_0_1')
s_0_2 = Int('s_0_2')
s_0_3 = Int('s_0_3')
s_1_0 = Int('s_1_0')
s_1_2 = Int('s_1_2')
s_1_3 = Int('s_1_3')
s_2_0 = Int('s_2_0')
s_2_1 = Int('s_2_1')
s_2_3 = Int('s_2_3')
s_3_0 = Int('s_3_0')
s_3_1 = Int('s_3_1')
s_3_2 = Int('s_3_2')
s.add(Or(s_0_1==0,s_0_1==1))
s.add(Or(s_0_2==0,s_0_2==1))
s.add(Or(s_0_3==0,s_0_3==1))
s.add(Or(s_1_0==0,s_1_0==1))
s.add(Or(s_1_2==0,s_1_2==1))
s.add(Or(s_1_3==0,s_1_3==1))
s.add(Or(s_2_0==0,s_2_0==1))
s.add(Or(s_2_1==0,s_2_1==1))
s.add(Or(s_2_3==0,s_2_3==1))
s.add(Or(s_3_0==0,s_3_0==1))
s.add(Or(s_3_1==0,s_3_1==1))
s.add(Or(s_3_2==0,s_3_2==1))
s.add(s_0 == s_0_1 * s_1 + s_0_2 * s_2 + s_0_3 * s_3)
s.add(s_1 == s_1_0 * s_0 + s_1_2 * s_2 + s_1_3 * s_3)
s.add(s_2 == s_2_0 * s_0 + s_2_1 * s_1 + s_2_3 * s_3)
s.add(s_3 == 2)
s.add(s_0 + s_1 + s_2 == 0)
print s.check()