You do not have permission to delete messages in this group
Copy link
Report message
Show original message
Either email addresses are anonymous for this group or you need the view member email addresses permission to view the original message
to Shen
I've been running THORN on problems in RCC; problems which in many cases are too hard for it. I recently attempted a theorem which was resistant to THORN proof. I broke it down to a series of subproblems which were solvable and one of them holds the record for the most 'distant' proof yet obtained by THORN. Over 200 million inferences needed to secure it. Rather like a celestial object that exists at the very limit of the resolution of a large telescope. This proof was 32 steps long, took 476 lines to print and constructed in 8.9 seconds.
How long would it take to find the whole proof by THORN? Extrapolating from the analysis of the sum of the parts, about 817 years, or about the time separating us from the signing of the Magna Carta.