op(400, xfx, +). op(300, fy, ~). set(knuth_bendix). assign(pick_given_ratio, 3). set(hyper_res). set(unit_deletion). assign(neg_weight, -10). assign(max_mem, 200000). assign(max_weight, 30). % assign(max_seconds, 120). clear(print_kept). clear(print_new_demod). clear(print_back_demod). clear(print_back_sub). list(usable). x = x. % Denial of the Robbins basis. B + A != A + B | (A + B) + C != A + (B + C) | ~ (~ (A + B) + ~ (~ A + B)) != B | $Ans(Robbins_basis). end_of_list. list(sos). % Each of the following 10 equations is a single axiom for % Boolean algebra in terms of {OR,NOT}. In particular, % each is equivalent to the Robbins basis. % % It's easy to check that these are valid in Boolean algebra. % To prove completeness, we derive the Robbins basis. % This input file should work for all but the first of these axioms. % ~ (~ (x + y) + ~ z) + ~ (~ (~ u + u) + (~ z + x)) = z. % 13345 685 sec ~ (~ (~ (x + y) + z) + ~ (x + ~ (~ z + ~ (z + u)))) = z. % 20615 6 sec % ~ (~ (x + y) + ~ z) + ~ (x + ~ (z + ~ (~ z + u))) = z. % 20629 19 sec % ~ (~ (x + y) + ~ (~ (x + z) + ~ (~ y + ~ (y + u)))) = y. % 20775 18 sec % ~ (x + ~ y) + ~ (~ (x + z) + ~ (y + ~ (~ y + u))) = y. % 20787 80 sec % ~ (~ (x + y) + ~ (~ (~ y + ~ (z + y)) + ~ (x + u))) = y. % 24070 28 sec % ~ (x + ~ y) + ~ (~ (y + ~ (z + ~ y)) + ~ (x + u)) = y. % 24086 44 sec % ~ (~ (x + y) + ~ (~ (~ y + ~ (z + y)) + ~ (u + x))) = y. % 24412 40 sec % ~ (x + ~ y) + ~ (~ (y + ~ (z + ~ y)) + ~ (u + x)) = y. % 24429 36 sec % ~ (~ (~ (x + y) + z) + ~ (~ (~ z + ~ (u + z)) + y)) = z. % 24970 47 sec end_of_list. % Include the following line to get a proof for 13345. % % assign(max_weight, 42). assign(change_limit_after, 100). assign(new_max_weight, 22).