%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.
set(build_proof_object_2).