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

list(usable).
% axiom set


% characteristic clause set

-> "P"("f"(x1), x1). % (C1)
"P"("f"("f"(x2)), "f"(x2)), "P"("f"(x2), x2) -> "P"("f"("f"(x2)), x2). % (C2)
"P"("f"("f"("a")), "a") ->. % (C3)
end_of_list.