%Here's an input file that gets a proof quickly. %Note that he has a cancellation rule for multiplication. set(auto). set(ur_res). assign(max_distinct_vars, 1). list(usable). x = x. m(1,x) = x. %identity m(x,1) = x. m(x,m(y,z)) = m(m(x,y),z). %associativity m(x,y) = m(y,x). %commutativity m(x,y) != m(x,z) | y = z. %cancellation -d(x,y) | m(x,f(x,y)) = y. %this and next line define divides m(x,z) != y | d(x,y). -d(2,m(x,y)) | d(2,x) | d(2,y). % 2 is prime (with 12) m(a,a) = m(2,m(b,b)). % a/b = sqrt(2) -d(x,a) | -d(x,b) | x = 1. % a/b is in lowest terms 2 != 1. % I almost forgot this! end_of_list.