updated formulas to use De Bruijn indexes;
updated other modules to use those, fixed lots of bugs in Cnf