% STANDARD.IN                 2003 May 27
% This template contains the best versions of all include files.

% set(binary_res).
set(ur_res).
set(factor).
set(unit_deletion).
set(para_from).
set(para_into).
set(dynamic_demod_all).
set(back_demod).
set(sos_queue).

set(lex_order_vars).
set(lrpo).
lex([0,id(x),Id,V,omega,OMEGA,FULL,FINITE,DEDEKIND,
     REGULAR,RUSSELL,UNOPS,Q,BIJ,FUNS,pair(x,x),
     $c1,$c2,               % Skolem constants
     swap(x),first(x),second(x),transposition(x,x),
     singleton(x),DESCENDING,pairset(x,x),succ(x),union(x,x),
     cart(x,x),Di,U(x),tc(x),P(x),
     BIGCUP,POWER,SINGLETON,SUCC,PAIRSET,RANK,CARD,
     VERTSECT(x),HC,TC,CROSS,IMAGE(x),RC(x),
     UCLOSURE,ACLOSURE,CUP,CART,CAP,SYMDIF,ZN,
     cross(x,x),PSM(x),funpart(x),H(x),map(x,x),
     intersection(x,x),cantor(x),compreln(x),complement(x),
     fix(x),D(x),R(x),rank(x),card(x),apply(x,x),
     Uclosure(x),Aclosure(x),image(x,x),
     IMG,RIGHT(x),LEFT(x),ADJOIN(x),A(x),invar(x),subvar(x),
     composite(x,x),restrict(x,x,x),
     LEAST(x),GREATEST(x),GLB(x),LUB(x),LB(x),UPPERBOUND,
     K,PS,S,UB(x),DISJOINT,subcommutant(x),inverse(x),
     RIF,COMPOSE,BIGCAP,FIX,IDP,SUPERPOWER,ES,LOWERBOUND,
     E,ROT,DUP,TWIST,FIRST,ASSOC,SECOND,
     REVERSE,SWAP,flip(x),rotate(x),sv3(x),sv1(x),sv2(x),bij(x,x),
     com(x,x,x,x),ind(x),dom(x,x,x),ran(x,x,x),notsub(x,x),
     ONEONE(x),UNOP(x),FUNCTION(x),thin(x),WELLORDER(x),
     TOTALORDER(x),PARTIALORDER(x),REFLEXIVE(x),SYMMETRIC(x),
     TRANSITIVE(x),EQUIVALENCE(x),PARTITION(x),INDUCTIVE(x),
     Uclosed(x),Aclosed(x),full(x),subcommute(x,x),equal(x,x),
     member(x,x),subclass(x,x),disjoint(x,x)]).

assign(stats_level,1).
% assign(pick_given_ratio,3).
assign(max_seconds,20).
assign(max_weight,20).
% assign(max_literals,2).
assign(max_distinct_vars,0).

%                                     % date of last update
% Axioms
include("u:\ax-a\ax-a-8.use").        % 1997 july 22
include("u:\ax-b\ax-b-16.use").       % 1998 january 3
include("u:\ax-c\axc.use").           % 2002 august 14
include("u:\ax-de\ax-reg.use").       % 1997 april 22
include("u:\ax-de\ax-ch-jb.use").     % 1997 august 13
% Definitions
include("u:\df-id\df-oo-1.use").      % 1998 january 3: replaces df-id-5 
% Theorems
include("u:\po\po-1.use").            % 1996 september 28
include("u:\eq\eq-2.use").            % 1996 september 28
include("u:\sp\sp1.use").             % 1998 january 10
include("u:\la\la1.use").             % 1998 march 24
include("u:\i\i1.use").               % 1997 may 10
include("u:\c\c1.use").               % 2000 august 18
include("u:\u\u1.use").               % 2000 december 25
include("u:\su\su1-a.use").           % 1998 january 21
include("u:\la\la2.use").             % 1997 may 10
include("u:\su\su2.use").             % 2000 april 7
include("u:\d\d.use").                % 2000 august 19
% include("u:\relcomp\rlc.use").        % 2001 september 3   (usually omit)
include("u:\dj\dj.use").              % 2000 august 19
include("u:\up\up1.use").             % 1998 january 3
include("u:\up\up2.use").             % 1997 august 29
include("u:\ss\ss1.use").             % 2000 april 1
include("u:\ss\ss2.use").             % 1997 september 3
include("u:\ss\ss3.use").             % 1998 may 10
include("u:\ss\ss4.use").             % 1998 january 3
include("u:\op\op1.use").             % 2000 august 13
include("u:\op\op2.use").             % 1998 february 10
include("u:\op\op3.use").             % 1999 august 9
include("u:\op\op4.use").             % 1998 february 10
include("u:\cp\cp1.use").             % 1998 july 4
include("u:\cp\cp2.use").             % 1997 july 25
include("u:\cp\cp3.use").             % 1997 may 8
include("u:\cp\cp-ss.use").           % 2000 december 2
include("u:\cp\cp-c.use").            % 1997 december 21
include("u:\rs\rs.use").              % 1998 june 5
include("u:\do\do1.use").             % 1997 december 17
include("u:\do\do2-a.use").           % 2002 august 1
include("u:\do\do3.use").             % 1997 december 18
include("u:\in\in1.use").             % 1998 december 8
include("u:\in\in2.use").             % 1999 august 10
include("u:\ra\ra1.use").             % 1997 november 4
include("u:\ra\ra2.use").             % 1997 december 19
include("u:\ra\ra3.use").             % 1997 december 17
include("u:\im\im1.use").             % 2001 august 26
include("u:\im\im2.use").             % 2000 october 8
include("u:\im\im3.use").             % 1998 october 6
include("u:\sc\sc1.use").             % 1999 april 11
include("u:\sc\sc2.use").             % 2000 march 10
include("u:\a\a1.use").               % 1999 january 4
include("u:\a\a2.use").               % 2000 august 13
include("u:\pc\pc0-a.use").           % 1998 april 27
include("u:\pc\pc1.use").             % 1999 december 30
include("u:\pc\pc2.use").             % 1998 october 22
include("u:\rl\rl.use").              % 1999 august 6
include("u:\cr\cr.use").              % 2000 july 19
include("u:\fl\fl1.use").             % 2000 february 11
include("u:\fl\fl2.use").             % 1997 july 24
include("u:\ro\ro1.use").             % 1997 july 25
include("u:\ro\ro2.use").             % 2000 august 18
include("u:\ro\ro3.use").             % 1997 july 25
include("u:\co\co1-b.use").           % 1998 december 8
include("u:\co\co2-a.use").           % 1998 november 29
include("u:\co\co3-c.use").           % 2001 january 3
include("u:\co\co4-b.use").           % 2001 july 13
include("u:\co\co5.use").             % 2000 may 19
include("u:\e\e1-a.use").             % 1999 january 19
include("u:\e\e2-a.use").             % 2002 august 14
include("u:\sr\sr1.use").             % 2000 january 25
include("u:\sr\sr2.use").             % 1999 march 18
include("u:\sr\sr3.use").             % 2000 february 12
include("u:\id\id1-a.use").           % 1998 january 19
include("u:\id\id-co.use").           % 1999 september 23
include("u:\id\id2.use").             % 1999 september 9
include("u:\fp\fp1-b.use").           % 2002 august 14
include("u:\id\id3-a.use").           % 2000 november 28
include("u:\id\id4.use").             % 1998 january 19
% include("u:\id\id-ro.use").
include("u:\ub\ub1.use").             % 2000 december 26
include("u:\lb\lb1.use").             % 2000 november 26
include("u:\di\di.use").              % 2000 march 28
include("u:\fp\fp2-b.use").           % 2002 august 14
include("u:\fp\fp3.use").             % 2002 august 14
include("u:\fp\fp4.use").             % 2002 august 14
include("u:\djt\djt-d.use").          % 2000 july 28
include("u:\sv\sv-ref.use").          % 2000 august 11
include("u:\fu\fu1-ref.use").         % 2000 december 22
include("u:\fu\fu2-a.use").           % 2001 april 26
include("u:\oo\oo.use").              % 2000 april 28
include("u:\idx\idx1.use").           % 2000 november 12
include("u:\idx\idx2-a.use").         % 2003 may 27
include("u:\fp\fp5.use").             % 2002 august 15
include("u:\fp\fp6.use").             % 2002 august 15
include("u:\fp\fp-sr.use").           % 2002 august 15
include("u:\fp\fp-dj.use").           % 2002 august 15
include("u:\fp\fp-im.use").           % 2002 august 15
include("u:\fp\fp-ub.use").           % 2002 august 15
include("u:\idx\idx3-a.use").         % 2000 december 28
include("u:\st\st1.use").             % 2001 july 10
include("u:\fu\fu3-ref.use").         % 2000 september 2
include("u:\sg\sg1-a.use").           % 2000 december 20
include("u:\sg\sg2-ref.use").         % 2000 july 21
include("u:\fp\fp-fu.use").           % 2002 august 18
include("u:\rp\rp1.use").             % 2001 july 8
include("u:\rp\rp2-ref.use").         % 1999 september 2 (reformulated)
include("u:\greatest\gt.use").        % 2000 december 28
include("u:\least\lt.use").           % 2000 december 28
include("u:\glb\glb.use").            % 2000 november 26
include("u:\lub\lub.use").            % 2000 november 25
include("u:\rfx\rfx.use").            % 2000 december 3
include("u:\sym\sym.use").            % 1998 january 2
include("u:\trv\trv.use").            % 2000 november 12
include("u:\poset\por.use").          % 2002 august 14
include("u:\totalord\to.use").        % 2000 december 26
include("u:\eqv\eqv1.use").           % 2002 july 31
include("u:\eqv\eqv2.use").           % 2002 july 31
include("u:\eqv\eqv3.use").           % 2002 july 31
include("u:\rus\rus1.use").           % 1999 march 27
include("u:\rus\rus2.use").           % 1999 march 27
include("u:\reg\reg1.use").           % 1999 march 19
include("u:\reg\reg2.use").           % 2001 august 10
include("u:\sp\sp2.use").             % 1998 november 11
include("u:\sp\sp3.use").             % 1999 april 13
include("u:\sp\sp4.use").             % 2001 june 8
include("u:\ps\ps1-a.use").           % 2000 may 15
include("u:\k\k.use").                % 2000 october 8
include("u:\psm\psm-a.use").          % 2000 may 17
include("u:\e\e-c.use").              % 1999 march 26
include("u:\sr\sr-c4.use").           % 2000 may 24
include("u:\ap\ap1-ref.use").         % 2000 may 10
include("u:\ap\ap2-ref.use").         % 2000 august 14
include("u:\ap\ap3-ref.use").         % 2001 september 27
include("u:\ap\ap4.use").             % 1997 november 5
include("u:\wo\wo.use").              % 2000 december 29
include("u:\pn\pn.use").              % 2000 february 13
include("u:\bigcup\ub.use").          % 1998 july 20
include("u:\bigcup\bc.use").          % 1999 july 16
include("u:\ucl\ucl1.use").           % 2001 september 24
include("u:\ucl\ucl2.use").           % 2001 september 23
include("u:\bigcap\lb.use").          % 1998 december 8
include("u:\bigcap\ba1-ref.use").     % 2000 june 7
include("u:\bigcap\ba2-ref.use").     % 1999 december 30
include("u:\acl\acl1.use").           % 2002 july 26
include("u:\acl\acl2.use").           % 2001 september 29
include("u:\pow\pow1.use").           % 1997 december 6
include("u:\pow\pow2.use").           % 2000 march 23
include("u:\pow\pow3-a.use").         % 1999 march 4
include("u:\pow\pow4-b.use").         % 1999 march 9
include("u:\pow\pow5-a.use").         % 2000 june 4
include("u:\vs\vs1-ref.use").         % 2001 july 6
include("u:\vs\vs2.use").             % 2002 august 5
include("u:\thin\th1.use").           % 2000 december 1
include("u:\zer\zer.use").            % 1999 march 11
include("u:\ca\ca-ref.use").          % 1999 september 9  (reformulated)
include("u:\sw\sw1.use").             % 1998 july 15
include("u:\sw\sw2.use").             % 1998 november 2
include("u:\sw\sw3-a.use").           % 2000 july 31
include("u:\1st\1st.use").            % 2001 may 27
include("u:\2nd\2nd.use").            % 2001 may 27
include("u:\dup\dup.use").            % 2000 august 31
include("u:\x\x1-c.use").             % 2001 january 15
include("u:\x\x2-b.use").             % 2000 september 3
include("u:\x\x3-ref.use").           % 2001 january 14
include("u:\st\st2.use").             % 2001 july 10
include("u:\assoc\ass.use").          % 2000 september 2
include("u:\rot\rot.use").            % 2001 january 16
include("u:\compose\rif.use").        % 2001 january 16
include("u:\reverse\rev.use").        % 2000 august 5
include("u:\twist\tw.use").           % 2000 august 8
include("u:\right\rt.use").           % 2000 july 23
% LEFT - not yet done
include("u:\cup\cup.use").            % 2001 september 4
include("u:\rc\rc.use").              % 2001 september 6
include("u:\pairset\prs.use").        % 2000 august 15
include("u:\cart\cart.use").          % 2000 september 30
% BO
% BH
include("u:\fs\fs.use").              % 2001 april 26
include("u:\ff\ff.use").              % 1998 december 24
include("u:\img\img1-c.use").         % 2000 august 26
include("u:\img\img2-b.use").         % 2002 august 18
include("u:\map\map1.use").           % 2001 april 27
include("u:\compose\cps.use").        % 2001 january 23
include("u:\img\img3.use").           % 2001 september 27
include("u:\img\img4-b.use").         % 2001 september 27
include("u:\ucl\ucl3.use").           % 2001 september 29
include("u:\acl\acl3.use").           % 2002 july 26
include("u:\img\img-x.use").          % 1999 april 14
include("u:\cross\crs.use").          % 2000 august 7
include("u:\cut\cut1.use").           % 2000 march 25
include("u:\cut\cut2-ref.use").       % 1999 august 29     (reformulated)
include("u:\adjoin\adj-2.use").       % 2000 july 24
include("u:\idp\idp.use").            % 2001 june 9
include("u:\fix\fix1.use").           % 2000 july 29
include("u:\fix\fix2.use").           % 1998 december 20
include("u:\cap\cap.use").            % 2000 august 19
include("u:\symdif\sdf.use").         % 2000 august 18
include("u:\her\her.use").            % added 1998 february 2
include("u:\mg\mg.use").              % 2000 august 27
% include("u:\domain\dom.use").    planned - not yet ready
include("u:\inverse\inv1.use").       % 2000 may 1
include("u:\inverse\inv2.use").       % 1997 november 29
include("u:\bij\bij.use").            % 2000 october 31
include("u:\q\q-1.use").              % 2002 august 1
include("u:\q\q-2.use").              % 2002 august 7
include("u:\q\q-3.use").              % 2002 august 2
include("u:\q\q-4.use").              % 2002 august 1
include("u:\q\q-5.use").              % 2002 august 2
include("u:\q\q-6.use").              % 2002 august 2
include("u:\q\q-7.use").              % 2002 august 1
include("u:\q\q-8.use").              % 2002 august 2
include("u:\choice\ac.use").          % 2001 may 7
include("u:\suc\suc-fun1.use").       % 2000 march 12
include("u:\es\es-b.use").            % 1998 september 19 
include("u:\suc\suc-rel2.use").       % 1999 october 3
include("u:\ful\ful1-a.use").         % 1998 march 14
include("u:\ful\ful2-b.use").         % 2001 august 15
include("u:\ful\ful3-a.use").         % 2000 february 18
include("u:\om\om1.use").             % 2000 february 21
include("u:\om\om2.use").             % 2000 march 12
include("u:\om\om3-b.use").           % 2000 june 11
include("u:\om\om4.use").             % 2000 june 11
include("u:\ind\ind1.use").           % 2000 february 6
include("u:\ind\ind2-a.use").         % 2002 august 14
include("u:\on\on1.use").             % 1999 march 2
include("u:\on\on2.use").             % 1998 march 5
include("u:\on\on3.use").             % 2000 december 12
include("u:\on\on4.use").             % 2002 august 3
include("u:\on\on5.use").             % 2001 august 25
include("u:\on\on6-a.use").           % 2000 march 14
include("u:\on\on7.use").             % 2000 november 1
include("u:\card\card1.use").         % 2002 august 8
include("u:\card\card2.use").         % 2002 august 9
include("u:\card\card3.use").         % 2002 august 9
include("u:\invar\ivr.use").          % 2000 november 30
include("u:\subvar\sbv1.use").        % 2000 december 5
include("u:\subvar\sbv2.use").        % 2001 september 15
include("u:\subvar\sbv3.use").        % 2000 march 10
include("u:\subvar\sbv4.use").        % 2000 march 10
include("u:\subvar\sbv5.use").        % 2000 march 10
include("u:\subvar\sbv6.use").        % 2000 october 15
include("u:\tc\tc1.use").             % 2000 october 23
include("u:\tc\tc2.use").             % 2001 august 28
include("u:\tc\tc3.use").             % 2001 march 15
include("u:\tc\tc4.use").             % 2001 august 15
include("u:\zn\zn1.use").             % 2001 july 11
include("u:\zn\zn2.use").             % 2001 july 11
include("u:\zn\zn3.use").             % 2001 july 19
include("u:\zn\zn4.use").             % 2001 august 3
include("u:\zn\zn5.use").             % 2001 july 17
include("u:\zn\zn6.use").             % 2001 august 2
include("u:\rank\rk1.use").           % 2001 august 11
include("u:\rank\rk2.use").           % 2001 august 10
include("u:\rank\rk3.use").           % 2001 august 11
include("u:\rank\rk4.use").           % 2001 august 10
include("u:\rank\rk5.use").           % 2001 august 13
include("u:\rank\rk6.use").           % 2001 august 11
include("u:\rank\rk7.use").           % 2001 august 12
include("u:\h\h.use").                % 2001 april 19
include("u:\hc\hc.use").              % 2001 april 20  
include("u:\finite\fin.use").         % 2001 august 28
include("u:\hf\hf1.use").             % 2001 august 26
include("u:\hf\hf2.use").             % 2001 august 26
include("u:\hf\hf3.use").             % 2001 august 28
include("u:\dedekind\dk.use").        % 2000 june 12
include("u:\card\card-om.use").       % 2002 august 8
include("u:\uo\uo.use").              % 2000 february 25
% MAP
% NOTSUB
% TOP
include("u:\re\re1.use").             % 1999 february 13
include("u:\re\re2.use").             % 1999 february 25
include("u:\re\re3-a.use").           % 2002 august 14
include("u:\re\re4.use").             % 2001 march 25

formula_list(sos).
% negation of Theorem
% -(all x y (subclass(composite(Id,x),y) ->
%            subclass(composite(Id,complement(y)),complement(x)))).
end_of_list.

% Axioms and Definitions.

include("m:\ax-a\ax-a.dem").          % 1997 july 22 (contains df-ss alone)
include("m:\ax-b\ax-b1.dem").         % 1998 july 12
include("m:\ax-c\axc.dem").           % 2002 august 14
% Definitions
% there is no demodulator file corresponding to DF-OO
% Theorems
include("m:\i\i1.dem").               % 1997 may 10

list(demodulators).
% LRPO-dependent demodulator
% equal(intersection(x,y),intersection(y,x)).                      % I-2
end_of_list.

include("m:\c\c1.dem").               % 2000 august 18
include("m:\u\u1.dem").               % 1997 may 10

list(demodulators).
% LRPO-dependent demodulator
% equal(union(x,y),union(y,x)).                                    % U-2
end_of_list.

include("m:\d\d.dem").                % 1999 april 10
% include("m:\relcomp\rlc.dem").        % 2001 september 3   (usually omit)
% There are no demodulators for the DJ group.
% There are no demodulators for the UP1 group
include("m:\up\up2.dem").             % 1997 august 29
% There are no demodulators for any of the SS groups.
% There are no demodulators for any of the OP groups.
include("m:\cp\cp1.dem").             % 1997 may 8
include("m:\cp\cp2.dem").             % 1997 december 21
include("m:\cp\cp3.dem").             % 1997 may 8
% there is no demodulator file for the CP-SS group
include("m:\cp\cp-c.dem").            % 1997 december 21
include("m:\rs\rs-a.dem").            % 1998 july 25          
include("m:\do\do1.dem").             % 1997 december 17
include("m:\do\do2.dem").             % 2002 august 1
include("m:\do\do3.dem").             % 1997 december 18
include("m:\in\in1.dem").             % 1998 september 24
include("m:\in\in2-b.dem").           % 1998 july 25
include("m:\ra\ra1.dem").             % 1997 december 17
include("m:\ra\ra2.dem").             % 1997 december 17
include("m:\ra\ra3.dem").             % 1997 december 17
include("m:\im\im1.dem").             % 2001 august 26
include("m:\im\im2.dem").             % 2000 march 30
include("m:\im\im3-a.dem").           % 1998 august 14
include("m:\sc\sc1.dem").             % 1999 april 11
include("m:\sc\sc2.dem").             % 1997 august 30
include("m:\a\a1.dem").               % 1998 december 10
include("m:\a\a2.dem").               % 1998 july 17
include("m:\pc\pc0-a.dem").           % 1998 january 5
include("m:\pc\pc1.dem").             % 1998 january 27
include("m:\pc\pc2.dem").             % 1998 april 19
include("m:\rl\rl.dem").              % 1998 march 26
% include("m:\cr\cr.dem").            % usually omit
include("m:\fl\fl1.dem").             % 1997 july 24
include("m:\fl\fl2.dem").             % 1997 july 24
include("m:\ro\ro1.dem").             % 1997 july 25
include("m:\ro\ro2.dem").             % 1997 july 25
include("m:\ro\ro3.dem").             % 1997 july 26
include("m:\co\co1-b.dem").           % 1998 september 24
include("m:\co\co2-a.dem").           % 1998 april 21
include("m:\co\co3-c.dem").           % 2000 august 31
include("m:\co\co4.dem").             % 1997 july 28
include("m:\co\co5.dem").             % 1998 july 1
include("m:\e\e1-a.dem").             % 1999 january 19
include("m:\e\e2.dem").               % 1998 november 21
include("m:\sr\sr1.dem").             % 1998 october 18
include("m:\sr\sr2.dem").             % 1999 march 18
include("m:\sr\sr3.dem").             % 1998 october 27
include("m:\id\id1.dem").             % 1998 march 23
include("m:\id\id-co.dem").           % 1998 november 28
include("m:\id\id2.dem").             % 1999 september 9
include("m:\fp\fp1-a.dem").           % 2002 august 14
include("m:\id\id3.dem").             % 1998 june 2
% there are no demodulators for ID\4
% there are no demodulators for ID\RO
include("m:\ub\ub1.dem").             % 2000 december 26
include("m:\lb\lb1.dem").             % 2000 november 24
include("m:\di\di.dem").              % 1998 december 21
include("m:\fp\fp2-b.dem").           % 2002 august 14
include("m:\fp\fp3.dem").             % 2002 august 14
include("m:\fp\fp4.dem").             % 2002 august 14
include("m:\djt\djt-d.dem").          % 1999 march 25
include("m:\sv\sv.dem").              % 1999 august 26  (unchanged)
include("m:\fu\fu1.dem").             % 2000 december 22
include("m:\fu\fu2.dem").             % 1997 august 29
include("m:\idx\idx1.dem").           % 2000 november 12
include("m:\idx\idx2-b.dem").         % 2003 may 27
include("m:\fp\fp5.dem").             % 2002 august 15
% there are no demodulators for the FP\6 group
include("m:\fp\fp-sr.dem").           % 2002 august 15
include("m:\fp\fp-dj.dem").           % 2002 august 15
include("m:\fp\fp-im.dem").           % 2002 august 15
% there are no demodulators for the FP\UB group
include("m:\idx\idx3-a.dem").         % 1998 september 19
% there are no demodulators for the ST\1 group
include("m:\fu\fu3.dem").             % 2000 february 5
include("m:\sg\sg1-a.dem").           % 1999 february 5
include("m:\sg\sg2.dem").             % 1998 september 2
include("m:\fp\fp-fu.dem").           % 2002 august 15
include("m:\rp\rp1.dem").             % 1998 october 22
include("m:\rp\rp2.dem").             % 1999 march 13
include("m:\greatest\gt.dem").        % 2000 december 28
include("m:\least\lt.dem").           % 2000 december 28
include("m:\glb\glb.dem").            % 2000 november 26
include("m:\lub\lub.dem").            % 2000 november 25
% there is no demodulator file for the RFX group
% there is no demodulator file for the SYM group
% there is no demodulator file for the TRV group
% there is no demodulator file for the POSET group
% there is no demodulator file for the TOTALORD group
% there is no demodulator file for the EQV\1 group
% there is no demodulator file for the EQV\2 group
include("m:\rus\rus1.dem").           % 1999 march 27
include("m:\rus\rus2.dem").           % 1998 january 25
include("m:\reg\reg1.dem").           % 1999 march 19
include("m:\reg\reg2.dem").           % 1999 april 27
include("m:\sp\sp2.dem").             % 1998 november 11
include("m:\sp\sp3.dem").             % 1999 april 13
include("m:\sp\sp4.dem").             % 1999 march 25
include("m:\ps\ps1.dem").             % 1998 december 21
include("m:\k\k.dem").                % 2000 october 8
include("m:\psm\psm-c.dem").          % 2000 may 17
include("m:\e\e-c.dem").              % 1999 march 26
include("m:\sr\sr-c4.dem").           % 2000 may 24
include("m:\ap\ap1.dem").             % 1998 february 5
include("m:\ap\ap2-ref.dem").         % 1999 september 5  (reformulated)
include("m:\ap\ap3.dem").             % 1999 september 5
% there is no demodulator file for the AP4 group
% there is no demodulator file for the WO group
% there is no demodulator file for the PN group
include("m:\bigcup\ub.dem").          % created 1998 july 20
include("m:\bigcup\bc.dem").          % 1999 july 16
include("m:\ucl\ucl1.dem").           % 2001 september 23
% there is no demodulator file for the UCL\2 group
include("m:\bigcap\lb.dem").          % 1998 december 8
include("m:\bigcap\ba1-ref.dem").     % 2000 june 7
include("m:\bigcap\ba2-ref.dem").     % 1999 december 30
include("m:\acl\acl1.dem").           % 2002 july 26
% there are no demodulators for the ACL\2 group
include("m:\pow\pow1.dem").           % 1997 december 6
include("m:\pow\pow2.dem").           % 1999 january 26
include("m:\pow\pow3-b.dem").         % 1999 july 20
include("m:\pow\pow4-a.dem").         % 1998 december 20
include("m:\pow\pow5.dem").           % 1999 march 4
include("m:\vs\vs1.dem").             % 2001 july 6
include("m:\vs\vs2.dem").             % 2000 february 27
% Theres is no demodulator file for the group THIN\1
include("m:\ca\ca.dem").              % 1997 august 28
include("m:\sw\sw1.dem").             % 1997 july 31
include("m:\sw\sw2-a.dem").           % 1998 november 2
include("m:\sw\sw3-b.dem").           % 1998 january 5
include("m:\1st\1st.dem").            % 2001 may 27
include("m:\2nd\2nd.dem").            % 2001 may 27
include("m:\dup\dup.dem").            % 2000 august 31
include("m:\x\x1-c.dem").             % 1999 august 9
include("m:\x\x2-c.dem").             % 2000 september 3
include("m:\x\x3.dem").               % 2000 august 1
include("m:\st\st2.dem").             % 2001 july 10
include("m:\assoc\ass.dem").          % 2000 september 2
include("m:\rot\rot.dem").            % 2001 january 14
include("m:\compose\rif.dem").        % 2002 august 7
include("m:\reverse\rev.dem").        % 2000 august 5
include("m:\twist\tw.dem").           % 2000 august 8
include("m:\right\rt.dem").           % 2000 july 21
% LEFT - not yet done
include("m:\cup\cup.dem").            % 2001 september 4
include("m:\rc\rc.dem").              % 2001 september 6
include("m:\pairset\prs.dem").        % 2000 august 15
include("m:\cart\cart.dem").          % 2000 july 18
% BO
% BH
include("m:\fs\fs.dem").              % 2000 march 2
% there is no FF.DEM file
include("m:\img\img1.dem").           % 2000 july 19
include("m:\img\img2-a.dem").         % 2002 july 25
include("m:\map\map1.dem").           % 2001 april 27
include("m:\compose\cps.dem").        % 2001 january 23
include("m:\img\img3.dem").           % 2001 july 18
include("m:\img\img4-b.dem").         % 2000 august 26
include("m:\ucl\ucl3.dem").           % 2001 september 28
include("m:\acl\acl3.dem").           % 2002 august 14
include("m:\cross\crs.dem").          % 2000 august 7
include("m:\cut\cut1.dem").           % 2000 march 25
include("m:\cut\cut2.dem").           % 1998 december 25
include("m:\adjoin\adj-2.dem").       % 2000 july 24
include("m:\idp\idp.dem").            % 2001 june 9
include("m:\fix\fix1.dem").           % 2000 july 29
include("m:\fix\fix2.dem").           % 1998 december 20
include("m:\cap\cap.dem").            % 2000 august 19
include("m:\symdif\sdf.dem").         % 2000 august 18
include("m:\her\her-a.dem").          % 1998 july 12
include("m:\mg\mg.dem").              % 2000 august 27
% include("m:\domain\dom.dem").       % planned - not done yet
include("m:\inverse\inv1a.dem").      % 1998 july 12
include("m:\inverse\inv2a.dem").      % 1998 july 12
include("m:\bij\bij.dem").            % 2000 april 27
include("m:\q\q-1.dem").              % 2002 august 1
include("m:\q\q-2.dem").              % 2002 august 1
include("m:\q\q-3.dem").              % 2002 august 1
% there is no demodulator file for the group Q\4
include("m:\q\q-5.dem").              % 2002 august 2
include("m:\q\q-6.dem").              % 2002 august 2
include("m:\q\q-7.dem").              % 2002 august 1
include("m:\q\q-8.dem").              % 2002 august 1
% there is no demodulator file for the CHOICE group
include("m:\suc\suc-fun.dem").        % 1998 may 10
include("m:\es\es-a.dem").            % 2002 august 14
include("m:\suc\suc-rel3.dem").       % 1999 october 3
include("m:\ful\ful2-a.dem").         % 1999 march 27
include("m:\ful\ful3.dem").           % 2000 february 18
include("m:\om\om1.dem").             % 1998 january 27
include("m:\om\om2.dem").             % 1997 august 22
include("m:\om\om3-c.dem").           % 1998 july 28
include("m:\om\om4.dem").             % 1998 september 17
include("m:\ind\ind1.dem").           % 1997 august 25
include("m:\ind\ind2.dem").           % 1997 august 25
include("m:\on\on1.dem").             % 1999 march 2
include("m:\on\on2.dem").             % 1997 august 27
% there is no demodulator file for the ON\3 group.
include("m:\on\on4.dem").             % 2002 august 3
include("m:\on\on5.dem").             % 1999 december 30
include("m:\on\on6-a.dem").           % 2000 march 14
include("m:\on\on7.dem").             % 1997 october 30
include("m:\card\card1.dem").         % 2002 august 4
include("m:\card\card2.dem").         % 2002 august 9
include("m:\card\card3.dem").         % 2002 august 9
include("m:\invar\ivr.dem").          % 2002 august 14
include("m:\subvar\sbv1.dem").        % 2000 december 5
include("m:\subvar\sbv2.dem").        % 2001 september 13
include("m:\subvar\sbv3.dem").        % 2000 march 10
include("m:\subvar\sbv4.dem").        % 2000 march 10
include("m:\subvar\sbv5.dem").        % 2000 march 10
include("m:\subvar\sbv6.dem").        % 2000 october 15
include("m:\tc\tc1.dem").             % 2000 october 23
include("m:\tc\tc2.dem").             % 2001 august 28
include("m:\tc\tc3.dem").             % 2001 march 15
% There is no demodulator file for the TC\4 group
% There is no demodulator file for the ZN\1 group
include("m:\zn\zn2.dem").             % 2001 july 11
include("m:\zn\zn3.dem").             % 2001 july 13
include("m:\zn\zn4.dem").             % 2001 july 19
include("m:\zn\zn5.dem").             % 2001 july 17
include("m:\zn\zn6.dem").             % 2001 july 17
include("m:\rank\rk1.dem").           % 2001 august 11
include("m:\rank\rk2.dem").           % 2001 august 10
include("m:\rank\rk3.dem").           % 2001 august 10
include("m:\rank\rk4.dem").           % 2001 august 10
include("m:\rank\rk5.dem").           % 2001 august 13
include("m:\rank\rk6.dem").           % 2001 august 11
include("m:\rank\rk7.dem").           % 2001 august 12
include("m:\h\h.dem").                % 2001 april 6
include("m:\hc\hc.dem").              % 2001 april 19
include("m:\finite\fin.dem").         % 2000 october 9
include("m:\hf\hf1.dem").             % 2001 august 26
include("m:\hf\hf2.dem").             % 2001 august 26
include("m:\hf\hf3.dem").             % 2001 august 28
include("m:\dedekind\dk.dem").        % 2000 june 12
include("m:\card\card-om.dem").       % 2002 august 8
include("m:\uo\uo.dem").              % 2000 february 24
% MAP
% NOTSUB
% TOP
% There are no demodulators for the RE groups

weight_list(pick_and_purge).
weight(member($(1),V),1).
weight(member($(1),cart(V,V)),1).
weight(0,100).
weight(A($(1)),100).
weight(Aclosed($(1)),100).
weight(Aclosure($(1)),100).
weight(ACLOSURE,100).
weight(ADJOIN($(1)),100).
weight(apply($(1),$(1)),100).
weight(ASSOC,100).
weight(AxCh,100).                            % blocks use of Ax of Choice
weight(AxReg,100).                           % blocks use of Ax of Reg
weight(BIGCAP,100).
weight(BIGCUP,100).
weight(bij($(1),$(1)),100).
weight(BIJ,100).
weight(cantor($(1)),100).
weight(CAP,100).
weight(card($(1)),100).
weight(CARD,100).
weight(CART,100).
weight(cart($(1),$(1)),100).
% weight(cart(cart($(1),$(1)),$(1)),100).
% weight(cart($(1),cart($(1),$(1))),100).
weight(CHOICE,100).
weight(com($(1),$(1),$(1),$(1)),100).
weight(complement($(1)),100).
weight(COMPOSE,100).
weight(composite($(1),$(1)),100).
% weight(composite($(1),composite($(1),$(1))),100).
weight(compreln($(1)),100).
weight(CROSS,100).
weight(cross($(1),$(1)),100).
weight(CUP,100).
weight(D($(1)),100).
weight(DEDEKIND,100).
weight(DESCENDING,100).
weight(Di,100).
weight(DISJOINT,100).
weight(disjoint($(1),$(1)),100).
weight(dom($(1),$(1),$(1)),100).
weight(DUP,100).
weight(E,100).
weight(equal($(1),$(1)),100).
weight(EQUIVALENCE($(1)),100).
weight(ES,100).
weight(FINITE,100).
weight(first($(1)),100).
weight(FIRST,100).
weight(fix($(1)),100).
weight(FIX,100).
weight(flip($(1)),100).
weight(full($(1)),100).
weight(FULL,100).
weight(FUNCTION($(1)),100).
weight(FUNCTIONFAMILY($(1)),100).
weight(funpart($(1)),100).
weight(FUNS,100).
weight(GLB($(1)),100).
weight(GREATEST($(1)),100).
weight(H($(1)),100).
weight(HC,100).
weight(Id,100).
weight(id($(1)),100).
weight(IDP,100).
weight(image($(1),$(1)),100).
weight(IMAGE($(1)),100).
weight(IMG,100).
weight(ind($(1)),100).
weight(INDUCTIVE($(1)),100).
weight(intersection($(1),$(1)),100).
% weight(intersection($(1),intersection($(1),$(1))),100).
weight(invar($(1)),100).
weight(inverse($(1)),100).
weight(IRREG,100).
weight(K,100).
weight(LB($(1)),100).
weight(LEAST($(1)),100).
weight(LEFT($(1)),100).
weight(LOWERBOUND,100).
weight(LUB($(1)),100).
weight(map($(1),$(1)),100).
weight(memb($(1)),100).
weight(member($(1),$(1)),100).
weight(notsub($(1),$(1)),100).
weight(omega,100).
weight(OMEGA,100).
weight(ONEONE($(1)),100).
weight(P($(1)),100).
weight(pair($(1),$(1)),100).
% weight(pair(pair($(1),$(1)),$(1)),100).
% weight(pair($(1),pair($(1),$(1))),100).
weight(PAIRSET,100).
weight(pairset($(1),$(1)),100).
weight(PARTIALORDER($(1)),100).
weight(PARTITION($(1)),100).
weight(POWER,100).
weight(PS,100).
weight(PSM($(1)),100).
weight(Q,100).
weight(R($(1)),100).
weight(ran($(1),$(1),$(1)),100).
weight(rank($(1)),100).
weight(RANK,100).
weight(RC($(1)),100).
weight(REFLEXIVE($(1)),100).
weight(REGULAR,100).
weight(regular($(1)),1).
weight(restrict($(1),$(1),$(1)),100).
weight(REVERSE,100).
weight(RIF,100).
weight(RIGHT($(1)),100).
weight(ROT,100).
weight(rotate($(1)),100).
weight(RUSSELL,100).
weight(S,100).
weight(second($(1)),100).
weight(SECOND,100).
weight(singleton($(1)),100).
weight(SINGLETON,100).
weight(subclass($(1),$(1)),100).
weight(subcommutant($(1)),100).
weight(subcommute($(1),$(1)),100).
weight(subvar($(1)),100).
weight(succ($(1)),100).
weight(SUCC,100).
weight(SUPERPOWER,100).
weight(sv1($(1)),100).
weight(sv2($(1)),100).
weight(sv3($(1)),100).
weight(swap($(1)),100).
weight(SWAP,100).
weight(SYMDIF,100).
weight(SYMMETRIC($(1)),100).
weight(tc($(1)),100).
weight(TC,100).
weight(thin($(1)),100).
weight(TOTALORDER($(1)),100).
weight(TRANSITIVE($(1)),100).
weight(transposition($(1),$(1)),100).
weight(TWIST,100).
weight(U($(1)),100).
weight(UB($(1)),100).
weight(Uclosed($(1)),100).
weight(Uclosure($(1)),100).
weight(UCLOSURE,100).
weight(union($(1),$(1)),100).
% weight(union($(1),union($(1),$(1))),100).
weight(UNOP($(1)),100).
weight(UNOPS,100).
weight(UPPERBOUND,100).
weight(V,100).
weight(VERTSECT($(1)),100).
weight(WELLORDER($(1)),100).
weight(ZN,100).
end_of_list.