% This input file is for EQP 0.9. % % Theorem. Robbins algebras satisfy % % exists C exists D, n(C+D)=n(C). % % This is the theorem that solves the Robbins problem. % It was first proved by EQP. % It takes about a week on an RS/6000 processor. assoc_comm(+). op(500, xfy, +). assign(max_weight, 70). assign(max_mem, 32000). assign(report_given, 5000). set(para_pairs). clear(print_given). set(basic_paramod). assign(pick_given_ratio, 1). assign(ac_superset_limit, 0). end_of_commands. list(sos). n(n(n(y)+x)+n(x+y))=x. % Robbins axiom end_of_list. list(passive). x+y != x. % denial of Winker condition 1 n(x+y) != n(x). % denial of Winker condition 2 end_of_list.