Decision procedures for variable-inactive theories and two polynomial T-satisfiability procedures (Position paper)