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

list(usable).
% axiom set


% characteristic clause set

"P"(x1, x2) -> "Q"(x1, x2). % (C1)
-> "P"(x3, x1). % (C2)
"Q"(x3, x1) ->. % (C3)
end_of_list.