The Present

Changes since CASC-J9

• New FEW category of the FOF division, WC time limit
• Return of the UEQ division
• Multi-language LTB division

The LTB Division

• Problems exported from HOL4
• Multiple versions of each problem provided
  • Syntactic export FOF, TF0, TF1, TH0, TH1
  • Semantic (set based) export FOF, TF0, TH0
• Attempt any versions
• Attempt problems and versions in any order
• Any solution accepted
• As usual, training data provided