The paraphrases listed here were automatically induced from the Nuprl Multiparallel Verbalization Corpus via multiple-sequence alignment (applied pairwise), as described and evaluated in Barzilay and Lee EMNLP 2002. Each line represents a paraphrase pair (underscores join a sequence of words making up one element of the pair). Since some Nuprl symbols are non-ascii, we have substituted them with ascii symbols for presentation purposes. The original file can be downloaded from this link (view it with "cat -v" on unix).

assume let
a\216b it
& ,
by expanding
and such
arbitrary in
, and
. and
should want_to
inner middle
conclude know
a any
natural \202
= is
on to
this which
-- ndiff
int_entire the
= are_equal_to
0 zero
positive_integer \202
integer z
as be
-- monus
applying by
n natural
integers \205
if suppose
arbitrary z
integers z
case if
case otherwise
expanding unfolding
by unfolding
is_not ¨
: either
prove show
analysis split
contracts contradicts
z …
: that
.aŽ­ Ž­
(a+-b+-c;0) (a+-b+-c;imax(0+-c;0)
: be
assumptions supposition
follow follows
n \202
assume suppose
. then
integers n
need_to should
assumption fact
else otherwise
0Ž.aŽŞa 0ŽŽŞa
our the
if otherwise
simplify y
are be
integers numbers
cases choices
arbitrary integers
need_to want_to
, .
let suppose
and or
‚ĥ …·¸ ·¸ \202 positive_integer 
monus ndiff
use using
by from
given let
conclusion result