__ _ _ _ ___ ___ _ __ / _(_) __ _| |_ ___ ___ | |___ ___ _ __ __ _ / __/ _ \| '_ \| |_| |/ _` | __/ _ \ / _ \| / __| / _ \| '__/ _` | | (_| (_) | | | | _| | (_| | || (_) | (_) | \__ \| (_) | | | (_| | \___\___/|_| |_|_| |_|\__, |\__\___/ \___/|_|___(_)___/|_| \__, | |___/ |___/Kmax, Kclause, and Klocalizer