Получить время выполнения только из команды gtime

Мне нужно выполнить команду и получить время ее выполнения. Я использую gtime, но результат немного отличается от того, что я хочу.

gtime возвращает результат выполнения, а затем время выполнения. Мне нужно сохранить вывод команды (мне нужно, чтобы это было только время) в переменной и использовать ее позже. Есть ли способ изменить команду, чтобы получить только время выполнения?

Итак, если я напишу команду ниже:

executiontime=$(gtime -f "%U" /Users/Desktop/SemanticLocality/optimathsat-1.6.2-macos-64-bit/bin/optimathsat < file.smt2)
echo "$executiontime"

то это пример вывода, который я получаю:

sat

(objectives
 (misses_80 1)
)
9.94