set(auto).
set(input_sequent).
set(output_sequent).
set(process_input).
set(build_proof_object_2).

list(usable).
% axiom set

-> =(+(x1, x2), +(x2, x1)). % (A1)
-> =(x1, x1). % (A2)
-> =(+(x1, +(x2, x3)), +(+(x1, x2), x3)). % (A3)
=(x1, +(x1, +("1", x2))) ->. % (A4)

% characteristic clause set

-> =("f"(+(x4, x5)), "0"), =("f"(+(x5, x4)), "1"). % (C1)
=("f"(+(x4, x6)), "0"), =("f"(+(+(+(x4, x6), "1"), x7)), "0") ->. % (C2)
=("f"(+(x4, x6)), "1"), =("f"(+(+(+(x4, x6), "1"), x7)), "1") ->. % (C3)
end_of_list.