$p-WSat(d-CNF) ∈ A[1]$ (Flum–Grohe, Theorem 6.28). The reduction maps $(α, k)$ to the structure whose universe is the literal occurrences of $α$ plus a padding element $z$, with the first occurrences of the variables ($C$), the negative parts of the clauses as padded tuples ($N$), and for every clause and every branch word $b < d^k$ of the bounded search tree the pair of its negative part and the found hitting set of the positive parts of the clauses with that negative part ($Lr$); and to the $Σ_1$-sentence ∃ x̄ w ȳ (Z w ∧ ⋀ C xᵢ ∧ ⋀_{j<i} ¬ xᵢ = xⱼ ∧ ⋀_t (¬ N v_t ∨ (Lr v_t y_t ∧ ⋀_j ⋁_i y_{t,j} = xᵢ))), $t$ ranging over the maps ${0,…,d} → {x_0,…,x_{k-1},w}$. It is computed in time $O(Pk(k)³ · |x|²)$.