[Termtools] TermComp2020 is running
Johannes Waldmann
johannes.waldmann at htwk-leipzig.de
Mon Jun 22 22:20:19 CEST 2020
thanks, Akihisa, for doing the work here!
> participation in debugging!
SRS_Relative/Waldmann_19 random problems are missing?
(they were used last year).
I think I have them here
https://gitlab.imn.htwk-leipzig.de/waldmann/tpdb/
Same for SRS_Standard/Waldmann_19 ?
Matchbox's proofs in SRS-Relative are wrong,
as they use the SRS-Standard method
(with inapplicable RFC matchbounds, DP transform)
(I already told Akihisa - probably the configuration Id was mistyped,
this is just in case others were wondering)
Also, I am currently not printing proofs, is this a problem?
https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/-/issues/264
Best regards, Johannes.
More information about the Termtools
mailing list