Розглянуто процедуру логічного виводу у С-класичному обчисленні предикатів першого порядку, яка відноситься до класу методів паралельної обробки й є одним із можливих шляхів вирішення проблеми "комбінаторного вибуху" завдяки сполученню процесу редукції та одиничної резолюції.