YSITD_TG_Bot1 says to #ysitd <seadog007>: (koru1130: Z3的原理...) https://en.wikipedia.org/wiki/Davis%E2%80%93Putnam_algorithm