Вы можете запустить САД на примерах из библиотеки TPTP или ввести ваше собственное задание во TPTP-формате. Выберите в каталоге заданий интересующую вас проблему и введите ее код в поле ввода внизу. Код задания должен соответствовать стандартной схеме именования заданий (например, FLD037-1.p, MSC007-2.005.p, SET027+3.p, и т.д.). Затем командой [Load] загрузите задание в окно редактирования Также вы можете ввести задание в окно редактирования вручную.

Мы не храним на этом сайте локальную копию библиотеки TPTP: задания и аксиомы загружаются напрямую с web-страницы TPTP. Поэтому мы накладываем некоторые ограничения на инструкции включения аксиом в задания: каждая инструкция включения должна занимать отдельную строку во входном тексте, включение разрешено только для наборов аксиом TPTP, частичное включение не поддерживается. Эти требования совместимы со всеми заданиями в библиотеке TPTP версии 2.6.0.

Команда [Parse] возвращает перевод входного TPTP задания в язык первого порядка (вместе со включенными аксиомами). Команды [Prove with Moses] и [Prove with] запускают поиск вывода. Напоминаем, что задания, не содержащие целевых формул или дизъюнктов, должны проверяться на (не)выполнимость, поэтому САД будет выводить противоречие из входных посылок (таким образом, пустое входное задание эквивалетнто пустой секвенции).