%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.