(G((f0)=>(~(f1)))) & ((~(u))) & ((f0)) & ((~(b0))) & ((~(b1))) & ((~(up))) & ((G(((u)=>(~(X(u))))&((~(X(u)))=>(u))))) & ((G((((u)=>((((f0)=>(X(f0)))&((X(f0))=>(f0)))&(((f1)=>(X(f1)))&((X(f1))=>(f1)))))&((f0)=>(X((f0)|(f1)))))&((f1)=>(X((f0)|(f1))))))) & ((G((((~(u))=>((((b0)=>(X(b0)))&((X(b0))=>(b0)))&(((b1)=>(X(b1)))&((X(b1))=>(b1)))))&(((b0)&(~(f0)))=>(X(b0))))&(((b1)&(~(f1)))=>(X(b1)))))) & ((G((((((f0)&(X(f0)))=>(((up)=>(X(up)))&((X(up))=>(up))))&(((f1)&(X(f1)))=>(((up)=>(X(up)))&((X(up))=>(up)))))&(((f0)&(X(f1)))=>(up)))&(((f1)&(X(f0)))=>(~(up)))))) & ((G(((sb)=>((b0)|(b1)))&(((b0)|(b1))=>(sb))))) & ((G((((f0)&(~(sb)))=>((f0)U(~((~(sb))U(~((F(f0))&(~(up))))))))&(((f1)&(~(sb)))=>((f1)U(~((~(sb))U(~((F(f0))&(~(up))))))))))) & ((G(((b0)=>(F(f0)))&((b1)=>(F(f1)))))) & ((G(F(b0)))) & ((G(F(b1))))