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