op(400, xfx, [*,+,#]). % infix operators 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: x + y = y + x. (x + y) + z = x + (y + z). (x + y@)@ + (x@ + y@)@ = y. % lemmas % From Huntington axioms we can derive x + x@ = y + y@. This allows % us to include the following lemma, which speeds up the proof. % % x + x@ = 1. list(sos). % Denial of single axiom (weight 131, 6 variables) ((((X + X@)@ + ((X + Y)@ + (X@ + Y)@))@ + (((((Z + U)@ + V)@ + (V + Z)@)@ + W@ )@ + (((((Z + U)@ + V)@ + (V + Z)@)@ + V)@ + (W@ + V)@))@ @)@ + ((((X + X@ )@ + ((X + Y)@ + (X@ + Y)@))@ + V)@ + ((((((Z + U)@ + V)@ + (V + Z)@)@ + W@)@ + (((((Z + U)@ + V)@ + (V + Z)@)@ + V)@ + (W@ + V)@))@ @ + V)@))@ != Y. end_of_list.