% This is Theorem 4 from the appendix of "Automated Reasoning about Cubic % Curves", by R. Padmanabhan and W. McCune, to appear in _Computers and % Mathematics with Applications_. set(para_from). set(para_into). % set(para_from_vars). % set(para_into_vars). set(order_eq). set(geometric_rule). set(geometric_rewrite). set(lrpo). lex([A,B,C,D,E,F,e,f(x,x),g(x)]). assign(pick_given_ratio, 1). assign(max_weight, 17). assign(max_mem, 1500). clear(print_kept). list(usable). x = x. end_of_list. list(sos). % f(e,e)=e. f(x,f(e,x)) = e. % f(f(x,e),x) = e. end_of_list. list(passive). f(f(A,B),f(C,D)) != f(f(A,C),f(B,D)). end_of_list.