2019-07-04 14:17:22 (GMT)
Oops, we missed the deadline to register at CASC. I hope we can still get in. http://www.tptp.org/CASC/27/Schedule.html
What should I put as System Version Number in the registration?
What are "Competition Divisions" and "Demonstration Divisions"?
I think the main "Entrant" should be Petar. Who should we list as associates? I'd suggest anyone who contributed to the code this year. I think that would be Petar, Simon, Sophie and I, right?
There is also a field for "Any special software requirements. Do we have any?
2019-07-04 14:32:56 (GMT)
No particular software requirement beyond the normal linux stuff, I think, but you know how painful it is to compile and deploy to Starexec.
For the version number, we can make a 1.5-casc-19 or something like that (so there's a fixed tag and "release" on github, for future reference). I think you're right about the list of associates.
2019-07-04 14:41:2 (GMT)
The official name is CASC-27, so I'll call it version 1.5-casc-27, ok?
2019-07-04 14:52:29 (GMT)
Ok, registered!
2019-07-05 7:34:17 (GMT)
Yes! Geoff says it's ok.
2019-07-13 19:20:27 (GMT)
I see a lot of work on new and improved heuristics :grinning_face_with_smiling_eyes:
2019-08-28 17:44:2 (GMT)
It is on: real time results !
2019-08-29 18:42:9 (GMT)
Pascal is currently winning the bet
2019-08-29 18:42:38 (GMT)
However the betting rankings are misleading! They also take a while to estabilize
2019-08-29 18:43:1 (GMT)
Zipperposition is doing very well! Very good :)
2019-08-29 18:43:42 (GMT)
I hope such a good performance on thf does not come at the expense of performance at sledgehammer problems!!
2019-08-29 18:43:51 (GMT)
(as it does for leo and satallax)
2019-08-29 18:44:3 (GMT)
Heh, it's all about graceful degradation! Look at the FOF category :smile:
2019-08-29 18:44:18 (GMT)
and Leo-3 is excellent, kudos to @Alex Steen !
2019-08-30 6:0:56 (GMT)
Hi guys :)
2019-08-30 6:1:41 (GMT)
Well the heuristics have been tuned for CASC specially
2019-08-30 6:4:24 (GMT)
@Simon Cruanes I think that this year's FOF was harder than the one where Zip took place. It is still better than leanCop and prover9, but indeed solved less problems (like E)
2019-08-30 13:30:24 (GMT)
I think so too, but we've done significantly better than prover9, which is great! :clap:
2019-08-31 19:19:21 (GMT)
Thank you for all the help :)
If it was not for it we would have not done it :)
2019-08-31 19:19:41 (GMT)
By the way, now that the CASC is over and I am flying back to Amsterdam tomorrow
2019-08-31 19:20:22 (GMT)
I have compiled my todo list:
2019-08-31 19:20:40 (GMT)
1. Finish unification paper (should take no more than 2 months)
2019-08-31 19:20:53 (GMT)
2. Clean up ZIp and release 1.6 (should take no more than 1 month)
2019-08-31 19:22:45 (GMT)
3. Work on E-avatar (will take the rest of my life and all the hair left)
2019-08-31 19:23:30 (GMT)
But there is one more thing that I have to ask @Simon Cruanes
2019-08-31 19:23:40 (GMT)
I stumbled upon some benchmark set that has 11000+ problems
2019-08-31 19:24:6 (GMT)
But in it equalities are encoded as = @ lhs @ rhs
2019-08-31 19:24:24 (GMT)
But this is not parseable by Zip
2019-08-31 19:24:31 (GMT)
Is it going to be a big change to include this
2019-08-31 19:25:15 (GMT)
I have no idea how Zip's parser works
2019-08-31 19:25:34 (GMT)
and I think I would break so many things by trying to implement this easy feature
2019-09-01 16:53:47 (GMT)
I can explain things about that if you want, the parser is generated, it might be possible to modify the grammar (it'll tell you if it's ambiguous).
2019-09-10 20:19:11 (GMT)
Apparently there was a grammar change that broke Satallax 3's parser (…) and it got retroactively fixed. It now has 399 problems, ranking second. :shrug:
2019-09-11 17:54:45 (GMT)
I wish we'd just convert all of TPTP to a S-expr syntax…