문제를 주고 증명 탐색
사용자가 명세와 증명하려는 추측을 입력하면 추론을 자동으로 진행한다. 대화형 보조기에서 증명 단계를 직접 설계하는 작업과 사용 방식이 다르다. 제한 시간 안에 증명이 나오지 않았다는 사실은 추측이 거짓이라는 판정과 다르다.
전략과 자원 설정
자동 모드와 전략 스케줄을 이용해 서로 다른 탐색 방식을 적용할 수 있다. CPU 시간과 메모리 제한을 설정하는 기능도 있다. 결과를 비교하려면 문제 자체와 선택한 전략, 사용 가능한 자원을 함께 맞춰야 한다.
일차 논리와 고차 논리 구분
기본 빌드와 고차 추론을 활성화한 실행 파일은 구분된다. 고차 지원이 있다고 해서 모든 종류의 고차 논리 표현이 같은 방식으로 처리되는 것은 아니다. 입력 형식과 논리 범위를 확인하고 산출된 증명 정보를 검토한다.