2nビットの数xに対してab=xとなるような1でない自然数a,bが存在するか？という命題をCNF(連言標準形)に直す。
そうするとレゾリューション（融合原理）はこの式に対して多項式サイズの証明を持つ。

証明は出来てない。