$$$unsound.pvs
unsound  % [ parameters ]
		: THEORY

  BEGIN

  % ASSUMING
   % assuming declarations
  % ENDASSUMING
 
% U:TYPE+   % Nonempty type
 U:TYPE    % Possibly empty universe
 z:VAR U   % x and y are variables ranging over U
 P: PRED[U]   % P is a unary predicate

 A0:THEOREM (forall z: P(z)) => (exists z: P(z))

 A1:THEOREM (exists z: TRUE)

 A2:THEOREM (exists (x:{y:nat| y>2 AND y<1}):TRUE)

 A3:THEOREM NOT (exists (x:{y:nat| y>2 AND y<1}):TRUE)

 A4:THEOREM NOT (exists (x:{y:nat| y>2 AND y<1}):TRUE)
	AND (exists (x:{y:nat| y>2 AND y<1}):TRUE)

 A5:THEOREM NOT (exists (x:{y:nat| y>2 AND y<1}):TRUE)
	AND (exists (x:{y:nat| y>2 AND y<1}):TRUE) => 1=2

 A6: THEOREM 1=2  

  END unsound

$$$unsound.prf
(|unsound|
 (A0 "" (FLATTEN)
  (("" (INST 1 "epsilon(TRUE)") (("" (INST -1 "epsilon(TRUE)") NIL NIL)) NIL))
  NIL)
 (A1 "" (INST 1 "epsilon(TRUE)") NIL NIL)
 (A2 "" (INST 1 "epsilon(TRUE)") NIL NIL) (A3 "" (GRIND) NIL NIL)
 (A4 "" (LEMMA "A2") (("" (LEMMA "A3") (("" (PROPAX) NIL NIL)) NIL)) NIL)
 (A5 "" (LEMMA "A4") (("" (BDDSIMP) NIL NIL)) NIL)
 (A6 "" (LEMMA "A4") (("" (LEMMA "A5") (("" (BDDSIMP) NIL NIL)) NIL)) NIL))