それもIUTに違和感が出る理由だよね。
まるでabc予想を解くための不等式の導出が目標になって構築されてる。