assign(new_constants, 1).

lex([ ', ^, v, f ]).  % We will get warning about skolem constants not being here.

assign(max_weight, 40).

clauses(sos).

f(f(f(f(y,x),f(x,z)),u),f(x,f(f(x,f(f(y,y),y)),z))) = x # label(OL_Sh).

x v y = f(f(x,x),f(y,y)).   % DEF_J
x ^ y = f(f(x,y),f(x,y)).   % DEF_M
x' = f(x,x).                % DEF_C

end_of_list.

clauses(goals).

f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))) # answer(A_SS).
f(f(x,x),f(x,y)) = x # answer(B_SS).
f(x,f(x,x)) = f(y,f(y,y)) # answer(ONE_SS).

end_of_list.