Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-02-14 22:22:36 -0800 (Sat, 14 Feb 2004)
Revision: 5378
Log message:

      Added an artificial example "testn" to check usefulness of my yesterday commit.
      I generate 10 "random" terms (of depth 3) and 10 inequalities over them.
      After yesterday commit it takes 5 secs to find a contradiction among those inequalities,
      a day before it would take 108 secs(!)
      So I think we should keep yesterday commit despite a small slowing down.
      It is slow on simple terms because contradictory inequalities are normalized twice but
      as terms become more complex and number of "unutilized" inequlaities grows
      we save more and more time.
      

Changes	Path
+53 -1	metaprl/theories/itt/itt_int_arith.ml
+22 -5	metaprl/theories/itt/itt_int_arith.mli
+11337 -8346	metaprl/theories/itt/itt_int_arith.prla