Exception Type_error on TPTP4X-accepted tptp file

[etienneparent]

Running zenon_modulo version 0.5.0 on this tptp file, I got the following error :

zenon_modulo -itptp problem.txt
Fatal error: exception Typetptp.Type_error("Contradictory types for 'prod_0'")
Raised at Stdlib__Weak.Make.find.(fun) in file "weak.ml", line 297, characters 47-62
Called from Expr.he_merge in file "expr.ml", line 493, characters 6-19

This file is yet valid according to TPTP4X and accepted by other automated theorem provers.
problem.txt

[gburel]

It looks like the type of prod_0 is declared twice :

tff(prod_0_type, type, prod_0 : $tType).

and

tff(prod_0_insert, type, prod_0 : ($int * $int) > prod_0).

I suspect that the second one should declare the type of prod_0_insert.