open main
pred idjCdcSrxTsH6w5gHCj_prop10 {
  always (all f : Protected | always f in Protected)
}
pred __repair { idjCdcSrxTsH6w5gHCj_prop10 }
check __repair { idjCdcSrxTsH6w5gHCj_prop10 <=> prop10o }