x19Complexity_2.in

% Unsat OK
assign(max_weight, 100).
%assign(max_seconds, 1).
set(raw).
clear(back_subsume). 
set(back_demod).
set(cac_redundancy).
%clear(auto_inference).
set(prolog_style_variables).
%set(print_gen).
set(random_given).
set(binary_resolution).
set(paramodulation).
%clear(ordered_res).
assign(max_given, 40).
assign(literal_selection, none).
%predicate_order([N,>]).
clear(predicate_elim).
list(kbo_weights).
 s = 5.
end_of_list.
formulas(sos).
N(X) | (t(X) != f(a,Z) & t(X) != f(Z,a) ).
t(X) != f(Z,Y) | (g(t(X)) = f(Z,Y) | g(t(X)) = f(Y,Z)).
t(s(X)) = g(t(X)). 
t(0) = f(a,Z).
end_of_list.