PROCEDUREENC(
T);
CASE
OF
) THEN accept ELSE reject 0: IF extension( 1: guess nondeterministically a subset ' of conclusions of
' :=
,
IF not extension(
') or not extension(
)
T HEN reject
' T) = true THENreject ELSE IF compare( ELSE accept 2: IF
T
 CN  T HEN accept  ELSE reject otherwise: reject END
PROCEDURE applied( : 1
);
/ CN for all IF
CN and l THEN RETURN true ELSE RETURN false END
PROCEDURE compare(
' T);
let T be the ordering oT 1 T ·· T n ;
FOR i := 0 TO n DO
IF not applied( i   ) and applied( i   ') THEN RET URN false; IF applied( ;  ) and not applied( ;   ') THEN RETURN true END
RET URN true END
Figure 4: A decision procedure for ENC
- 1

T   where     is a set of defaults, is a set of T-ordering for Cn(  ),
formulae, T is a strict total order on –, and T is not a 
and
- 2 where CN.

Lemma 5.6 ENC is Turing reducible to CN in nondeterministic polynomial time.

Proof: The language ENC is accepted by a nondeterministic Turing machine given as the procedure in Figure 4. The executions of the procedure have a polynomial length.

□
Theorem 5.7  The complement of the problem of testing whether a formula belongs to all preferred - extensions of a default theory is Turing reducible to ENC in nondeterministic polynomial time.