op(400, xfx, [*,+,#]). % infix operators op(300, yf, @). % postfix operator lex([p(_,_,_), f1(_,_,_), f2(_,_), _#_]). % see demodulators below set(knuth_bendix). set(back_unit_deletion). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). assign(max_mem, 100000). assign(pick_given_ratio, 4). list(usable). x = x. end_of_list. list(sos). % Single axiom for BA in terms of Sheffer stroke (weight 185, 8 variables) (((((x#y)# (x# (z#y)))# (x# (x# ((u#v)# (v#v)))))# ((x# (x# ((x#y)# (x# (z#y)))))# ((u#v)# (v#v))))# (v# (v# ((w# (v6# (v6# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))# ((v6# (v6#w))# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))))# ((v# (v# ((((x#y)# (x# (z#y)))# (x# (x# ((u#v)# (v#v)))))# ((x# (x# ((x#y)# (x# (z#y)))))# ((u#v)# (v#v))))))# ((w# (v6# (v6# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))# ((v6# (v6#w))# ((w# (v7# (v7#v7)))# ((v7# (v7#w))#v7)))))=w. end_of_list. list(demodulators). % These 3 demodulators are definitions that are designed to contract % the single axiom on input. The important part of the proof, deriving % G and W17, happens in terms of f1, f2, and p. % Since they are equational definitions, they don't change the theory. (x # (y # (y # z))) # ((y # (y # x)) # z) = p(x,y,z). % Pixley-4 (x # z) # (x # (y # z)) = f1(x,y,z). % related to Veroff-27a (y # x) # (x # x) = f2(x,y). % related to Meredith-1c end_of_list. list(usable). % This is the denial of the McCune 2-basis. (X # Z) # (X # (Y # Z)) != X | (Y # X) # (X # X) != X. end_of_list.