Parallel analysis of polymorphic viral code using automated deduction system