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"("f"("f"(x3)))), "f"("f"(x3))), "P"("f"("f"(x3)), x3) -> "P"("f"("f"("f"("f"(x3)))), x3). % (C3)
"P"("f"("f"("f"("f"("a")))), "a") ->. % (C4)
end_of_list.
