| Wed, 16 May 2012 19:15:45 +0200 | kuncar | infrastructure that makes possible to prove that a relation is reflexive | changeset | files |
| Wed, 16 May 2012 18:16:51 +0200 | blanchet | temporarily disable "ext" rule helpers until Metis supports them (and until they are properly evaluated) | changeset | files |
| Wed, 16 May 2012 18:16:51 +0200 | blanchet | lower skolem penalty to ensure that some useful facts with existentials, e.g. congruence of "setsum", eventually get picked up | changeset | files |