const zero = () => () => false;
const one = () => () => true;
const variable = (name) => (vars) => vars[name];

const un_op = op => f1 => (vars) => op(f1(vars));
const bin_op = op => (f1, f2) => (vars) => op(f1(vars), f2(vars));

const negate = un_op(a => !a);
const and = bin_op((a, b) => (a && b));
const or = bin_op((a, b) => (a || b));

const dnf = function(str) {
    if (str == '') {
        return "Undefined result!";
    }
    const skipWhitespaces = function() {
        while (pos < len && str[pos] == ' ') {
            ++pos;
        }
    }
    const level_3 = function() {
        skipWhitespaces();
        switch (str[pos]) {
            case '~': {
                ++pos;
                return negate(level_3());
            }
            case '0': {
                ++pos;
                return zero();
            }
            case '1': {
                ++pos;
                return one();
            }
            case '(': {
                ++pos;
                const res = level_1();
                ++pos;
                return res;
            }
        }
        if (str[pos] >= 'a' && str[pos] <= 'z') {
            return variable(str[pos++]);
        }
    }
    const bin_op_levels = function(symb, func, up) {
        return function() {
            let result = up();
            while (pos < len) {
                skipWhitespaces();
                if (pos < len && str[pos] == symb) {
                    ++pos;
                    result = func(result, up());
                } else {
                    break;
                }
            }
            return result;
        }
    }
    const level_2 = bin_op_levels('&', and, level_3);
    const level_1 = bin_op_levels('|', or, level_2);

    let pos = 0;
    const len = str.length;
    const expression = level_1();

    let list_variables = [];
    let str_has_letters = false;
    for (let i = 0; i < len; ++i) {
        if (str[i] >= 'a' && str[i] <= 'z') {
            list_variables[str[i]] = true;
            str_has_letters = true;
        }
    }
    if (!str_has_letters) {
        return expression() ? '1' : '0';
    }

    let variable_values = {};
    let g_result = [];
    const gen_block_from_current_state = function() {
        let result = [];
        for (let index in variable_values) {
            const value = variable_values[index];
            if (value == false) {
                result.push('~' + index);
            } else if (value == true) {
                result.push(index);
            }
        };
        return result.join(' & ');
    };
    const add_current_state_to_string = function() {
        g_result.push('(' + gen_block_from_current_state() + ')');
    }
    const nxt_letter = (letter) => String.fromCharCode(letter.charCodeAt(0) + 1);
    const stop_letter = nxt_letter('z');
    const recursive_search_answer = function(letter) {
        if (letter == stop_letter) {
            const res = expression(variable_values);
            if (res == true) {
                add_current_state_to_string();
            }
            return;
        }
        if (list_variables[letter] == true) {
            variable_values[letter] = false;
            recursive_search_answer(nxt_letter(letter));
            variable_values[letter] = true;
            recursive_search_answer(nxt_letter(letter));
        } else {
            recursive_search_answer(nxt_letter(letter));
        }
    }
    recursive_search_answer('a');
    return g_result.length > 0 ? g_result.join(' | ') : '0';
}