Wrong TPTP output for ITE(s) (and possibly other special terms)

[mezpusz]

GDV complains for the following examples:

-p tptp --decode ott+10_14_sil=8000:tgt=full:prc=on:random_seed=3219396785:i=2501:fsr=off_2914 $TPTP/Problems/ITP/ITP217_3.p
-p tptp --decode ott+10_1_sil=8000:drc=ordering:abs=on:urr=on:br=off:random_seed=891916334:cond=on:s2a=on:i=1197:gtg=position:ss=axioms:sgt=8_2977 $TPTP/Problems/ITP/ITP267_3.p

The problem seems to be that for an ITE $ite(condition,then,else) we first construct the head as $ite(condition, and then try to construct the rest as if the term wasn't special, adding all arguments in a pair of parenthesis, resulting in something like $ite(condition,(then,else)).

[MichaelRawson]

@shalashaska117 - did you fix this in #939, perhaps?

[shalashaska117]

Yes, #939 fixes this too. It removes the extra opening parenthesis from both term-printing paths and covers $ite, $let, and $match.

I reran both problems with the strategies above against current master prover code (af03e1547; the local build adds only testing scripts):

• ITP217_3.p: Theorem; the complete emitted TPTP proof reparses successfully, including all 3 $ite occurrences.
• ITP267_3.p: Theorem; the complete emitted TPTP proof reparses successfully, including all 12 $ite occurrences.

For the second command I removed abs=on, which was deleted in 4e2bab3. WSL could not enable the instruction counter, so the encoded instruction limits were inactive. Both runs finished in about 2-3 seconds.

Validation used --input_syntax tptp --mode profile on each complete proof; I did not run GDV. The TermOutput regression suite also passes. This confirms the reported parenthesis bug is fixed by #939.

@MichaelRawson, could you close this as fixed by #939? I don't have permission to close it.