Wrong TPTP output for arithmetic problems

[mezpusz]

The output should contain tff instead of fof commands when using -p tptp for these problems.

Known problem instances where it reproduces with the default strategy:

ARI496_1.p
ARI500_1.p
ARI501_1.p
ARI503_1.p
ARI504_1.p
ARI520_1.p
ARI523_1.p
ARI524_1.p

[mezpusz]

For ARI496_1.p, we start with a unit list of:

2. ~$is_int(6) [negated conjecture 1]

This is then normalized, and we get a unit list of:

3. ~$true [theory normalization 2]

In the first list, we scan properly that tff should be used, but in the second this information is lost.

The solution could be similar to how we retain information about pure literals or other stuff that is removed entirely during preprocessing.