fix: deskolemization algorithm

[jrosain]

Bug fix

Closes: #16

Description

Rewrote the deskolemization algorithm to follow the one of the paper. Greatly simplified
the code while doing so, hopefully this is more easily modifiable in the future/more
easily debuggable.

During this process, I added a new type of debug: the interrupt debug. It works as the
others debugs, but instead of printing something, it awaits for the user input. This
probably won't be useful for the main proof search procedure unless we adapt it to
interrupt goroutines etc but for sequential algorithms like deskolemization or a proof
output, it's actually quite handy to be able to follow what the algorithm is doing step by
step and avoid looking at a super long log.

I've also adapted the GS3Sequent to implement a structure of IProof in order to make
the proof outputs more generic by simply taking the IProof instead of only accepting a
GS3Sequent.

I hope I've not broken any output. I've taken the occasion to generalize some common
operations between the Rocq and the TPTP output.

PR dependencies

• Add IProof interface with a tree structure and add relevant adapter for []Search.ProofStruct #64
• Improve formatting by using golines #69 (not a real dependency, see what to do before merging)

Test-suite update

• added % timeout command to a test file (followed by seconds). The test fails if the time is reached.
• the file running the test-suite now detect errors during proof search or proof output.
• test-suite/bugs/bug_16-1.p: previous problem that made deskolemization loop infinitely.
• test-suite/bugs/bug_16-2.p: the same kind of problem but for preinner Skolemization.
• test-suite/bugs/bug_46-n.p: all the problems that failed in inner Skolemization following the optional return of Lib.ListIndexOf.
• test-suite/bugs_no_chk/bug_46-4.p: this test actually also triggers a substitution bug (most of the time) which makes it impossible to have it formally in the test suite. I still put it here so that we can move it back to the bugs folder in the future.
• test-suite/bugs/bug_70-1/2.p: tests the output with a quantified variable that is not used in the formula.
• test-suite/bugs/bug_70-3.p: tests the output with a reintroduction rule.