Prior work has revealed the weaknesses of LLMs in logical reasoning (Han et al., 2022; Saparov and He, 2022; Saparov et al., 2023; Wan et al., 2024; Xu et al., 2023), especially when the proof is long and requires the knowledge of multiple deduction theorems. To isolate the effect of premise orders, we focus on a confined problem space adapted from SimpleLogic (Zhang et al., 2022), which only includes propositional logic problems with definite clauses. Specifically, each problem includes: (1) a set of facts \(A_{1}\),\(\ldots\), \(A_{n}\) that hold true; (2) a set of rules of the form "If \(X\), then \(Y\)", "If \(X_{0}\) and \(X_{1}\), then \(Y\)", or "If \(X_{0}\) and \(X_{1}\) and \(X_{2}\), then \(Y\)"; and (3) a conclusion "\(C\) is True" to be proved. As opposed to SimpleLogic -- which formulates the problem as a binary classification task (i.e., indicate whether the conclusion is True or False) -- in our benchmark, every problem has a ground-truth label of True, and we consider the prediction to be correct only when the generated proof is completely valid. With these strict criteria, the LLM is required to produce the step-by-step deduction that leads to the conclusion, and any hallucination of non-existent facts and rules is considered erroneous.