% STANDARD.IN                 2002 August 18
% 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").         % 2002 August 11
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").         % 2000 May 5
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.