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"("f"("f"("f"("f"("f"("f"("f"("f"(x5)))))))))))))))), "f"("f"("f"("f"("f"("f"("f"("f"(x5))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"(x5)))))))), x5) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x5)))))))))))))))), x5). % (C5)
"P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6)))))))))))))))))))))))))))))))), "f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6))))))))))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6)))))))))))))))), x6) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x6)))))))))))))))))))))))))))))))), x6). % (C6)
"P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), "f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x7))))))))))))))))))))))))))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x7)))))))))))))))))))))))))))))))), x7) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), x7). % (C7)
"P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x8)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), "f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x8))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x8)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), x8) -> "P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"(x8)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), x8). % (C8)
"P"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("f"("a")))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))), "a") ->. % (C9)
end_of_list.
