op(400, xfx, +). % infix operator op(300, yf, @). % postfix operator set(knuth_bendix). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). assign(max_mem, 100000). assign(pick_given_ratio, 6). list(usable). x = x. end_of_list. list(sos). % Huntington axioms for Boolean algebra: x + y = y + x. (x + y) + z = x + (y + z). (x + y@)@ + (x@ + y@)@ = y. % Definition of conjunction: (x * y) = (x@ + y@)@. end_of_list. list(sos). % Denial of single axiom (weight 111, 6 variables) (((X * X@) + ((X * Y) + (X@ * Y))) * ((((Z + (U + V)@)@ + (Z + V)@ )@ * W@) + ((((Z + (U + V)@)@ + (Z + V)@)@ * Z) + (W@ * Z)))@) + ((((X * X@) + ((X * Y) + (X@ * Y))) * Z) + (((((Z + (U + V)@)@ + (Z + V)@)@ * W@) + ((((Z + (U + V)@)@ + (Z + V)@)@ * Z) + (W@ * Z)))@ * Z)) != Y. end_of_list.