SYO882^1

DT2H2X---1.9.5.UNS-Ref.s Duper---1.0.UNS-Prf.s Satallax---3.5.UNS-Prf.s Vampire---5.0.1.UNS-Ref.s Vampire-SAT---5.0.1.UNS-Ref.s Zipperpin---2.1.9999.UNS-Ref.s cvc5---1.3.4.UNS-Prf.s