%Selected Problems CASC18

%:-use_module(library(system)[]),system:working_directory(_,'/HG/local/provers/TPTP-v2.5.0').

% HNE
:-hgstuff:runtptpproblem('ANA003-2',_).
:-hgstuff:runtptpproblem('GEO002-4',_).
:-hgstuff:runtptpproblem('GRP048-2',_).
:-hgstuff:runtptpproblem('LCL012-1',_).
:-hgstuff:runtptpproblem('LCL024-1',_).
:-hgstuff:runtptpproblem('LCL030-1',_).
:-hgstuff:runtptpproblem('LCL048-1',_).
:-hgstuff:runtptpproblem('LCL191-1',_).
:-hgstuff:runtptpproblem('LCL223-1',_). 
:-hgstuff:runtptpproblem('LCL224-1',_). 
:-hgstuff:runtptpproblem('LCL225-1',_). 
:-hgstuff:runtptpproblem('LCL227-1',_). 
:-hgstuff:runtptpproblem('LCL249-1',_). 
:-hgstuff:runtptpproblem('LCL253-1',_). 
:-hgstuff:runtptpproblem('LCL402-1',_). 
:-hgstuff:runtptpproblem('LCL416-1',_).
:-hgstuff:runtptpproblem('LCL417-1',_). 
:-hgstuff:runtptpproblem('NUM017-1',_). 
:-hgstuff:runtptpproblem('PLA008-1',_). 
:-hgstuff:runtptpproblem('PLA010-1',_). 
:-hgstuff:runtptpproblem('PLA015-1',_). 
:-hgstuff:runtptpproblem('PLA018-1',_). 
:-hgstuff:runtptpproblem('PUZ042-1',_).
:-hgstuff:runtptpproblem('RNG001-5',_).
:-hgstuff:runtptpproblem('RNG004-3',_). 
:-hgstuff:runtptpproblem('RNG039-2',_). 
:-hgstuff:runtptpproblem('SYN556-1',_). 
:-hgstuff:runtptpproblem('SYN597-1',_). 
:-hgstuff:runtptpproblem('SYN600-1',_). 
:-hgstuff:runtptpproblem('SYN601-1',_). 
:-hgstuff:runtptpproblem('SYN602-1',_). 
:-hgstuff:runtptpproblem('SYN616-1',_).
:-hgstuff:runtptpproblem('SYN628-1',_). 
:-hgstuff:runtptpproblem('SYN631-1',_). 
:-hgstuff:runtptpproblem('SYN653-1',_).


/*

HEQ
ANA004-1 BOO008-1 BOO015-1 BOO017-1 CAT002-1 CAT011-4 CAT018-4 COL003-2
COL006-3 COL042-5 COL044-2 COL044-3 COL044-5 GRP002-1 HEN003-1 HEN003-2
HEN004-2 HEN005-4 HEN006-1 HEN006-2 HEN006-6 HEN006-7 HEN007-1 HEN010-7
HEN012-1 HWC001-1 HWC003-2 HWV002-1 LAT002-1 LAT005-5 LCL109-5 LCL152-1
LCL300-3 RNG005-1 RNG008-6




NNE
ANA002-1 ANA002-3 ANA002-4 FLD022-1 FLD036-3 FLD068-1 GRP039-6 HWV006-1
HWV006-2 HWV007-2 SET010-1 SET013-1 SET013-2 SET014-2 SYN036-1 SYN067-1
SYN353-1 SYN568-1 SYN576-1 SYN607-1 SYN633-1 SYN634-1 SYN635-1 SYN641-1
SYN642-1 SYN657-1 SYN673-1 SYN694-1 SYN698-1 SYN755-1 SYN758-1 SYN759-1
SYN784-1 SYN796-1 SYN802-1




NEQ
CAT018-3 GEO001-1 GEO002-1 GEO006-1 GEO007-1 GEO008-1 GEO009-1 GEO010-1
GEO011-1 GEO083-1 GRP026-1 GRP039-2 GRP040-3 HWV013-2 HWV016-1 HWV017-1
HWV022-1 HWV023-2 HWV027-2 HWV029-2 HWV033-1 LDA005-1 LDA006-2 LDA007-1
LDA007-2 LDA008-1 LDA010-1 LDA011-1 MGT029-1 NUM007-1 SET022-3 SET042-3
SET497-6 SWC049-1 SYN014-1




PEQ
ALG003-1 BOO020-1 BOO039-1 CAT004-2 COL076-1 COL076-2 COL077-1 COL080-1
COL081-1 GRP054-1 GRP056-1 GRP074-1 GRP086-1 GRP108-1 GRP111-1 GRP198-1
GRP210-1 GRP242-1 GRP254-1 GRP255-1 GRP263-1 GRP281-1 GRP283-1 GRP297-1
GRP305-1 GRP312-1 GRP313-1 GRP330-1 GRP332-1 GRP339-1 GRP369-1 GRP401-1
LAT015-1 LAT030-1 RNG029-3




UEQ
BOO034-1 COL003-20 COL006-1 COL006-5 COL006-6 COL006-7 COL011-1 COL036-1
COL037-1 COL042-1 COL043-1 COL043-3 COL044-1 COL044-6 COL044-7 COL044-8
COL044-9 COL065-1 COL066-1 GRP024-5 GRP164-1 GRP167-3 GRP167-4 GRP177-2
GRP178-2 GRP179-1 GRP179-2 GRP180-1 GRP180-2 GRP181-1 GRP181-2 GRP183-1
GRP183-2 GRP183-3 GRP183-4 GRP184-1 GRP184-3 GRP185-3 GRP185-4 GRP186-1
GRP187-1 LAT017-1 LAT020-1 LCL160-1 RNG019-6 RNG019-7 RNG020-6 RNG020-7
RNG021-6 RNG021-7 RNG025-4 RNG025-5 RNG025-6 RNG025-7 RNG026-6 RNG026-7
RNG027-5 RNG027-7 RNG027-8 RNG027-9 RNG028-5 RNG028-8 RNG028-9 RNG029-5
RNG029-6 RNG029-7 RNG035-7 ROB006-1 ROB006-2 ROB026-1




SNE
GRP394-2 HWV035-1 HWV036-1 HWV036-2 LCL240-1 LCL248-1 LCL415-1 NLP026-1
NLP191-1 NUM287-1 NUM288-1 PUZ045-1 PUZ046-1 SWV016-1 SYN303-1 SYN330-1
SYN351-1 SYN736-1 SYN754-1 SYN770-1 SYN776-1 SYN786-1 SYN806-1 SYN904-1
SYN907-1 SYN912-1 TOP006-1 TOP009-1 TOP010-1 TOP011-1 TOP012-1 TOP013-1
TOP014-1 TOP016-1 TOP018-1




SEQ
BOO019-1 BOO033-1 BOO037-1 BOO056-1 BOO057-1 CAT001-2 CAT020-2 COL073-1
GRP204-1 GRP395-1 GRP397-1 HEN013-3 LAT047-1 LAT048-1 LAT050-1 LAT051-1
LAT054-1 LAT056-1 LAT058-1 LAT063-1 LCL136-1 LCL142-1 LCL280-3 LCL338-3
LCL411-2 LCL412-1 NLP052-1 NLP053-1 NLP056-1 NLP186-1 RNG007-5 RNG031-6
RNG031-7 ROB015-1 ROB029-1




FNE
SWV014+1 SYN457+1 SYN460+1 SYN466+1 SYN471+1 SYN474+1 SYN482+1 SYN503+1
SYN548+1 SYN723+1




FEQ
GEO089+1 GEO093+1 GEO094+1 GEO103+1 GEO104+1 GEO113+1 GEO122+1 GEO125+1
GEO127+1 GEO146+1 MGT034+2 MGT039+2 MGT061+1 MGT064+1 SET014+4 SET017+1
SET067+1 SET076+1 SET086+1 SET096+1 SET108+1 SET143+3 SET143+4 SET171+3
SET580+3 SET601+3 SET606+3 SET607+3 SET609+3 SET611+3 SET612+3 SET614+3
SET615+3 SET624+3 SET630+3 SET640+3 SET646+3 SET647+3 SET648+3 SET649+3
SET651+3 SET657+3 SET669+3 SET671+3 SET673+3 SET680+3 SET683+3 SET684+3
SET686+3 SET716+4 SET724+4 SET747+4 SET764+4 SET770+4 SWC022+1 SWC287+1
SWC315+1 SWC330+1 SWC420+1 SYN551+2




EPT
GRP127-2.006 GRP128-2.006 GRP128-3.005 PUZ010-1 PUZ017-1 PUZ037-2 PUZ037-3
SYN440-1 SYN447-1 SYN454-1 SYN457-1 SYN462-1 SYN466-1 SYN470-1 SYN475-1
SYN483-1 SYN487-1 SYN498-1 SYN500-1 SYN501-1 SYN504-1 SYN507-1 SYN510-1
SYN813-1 SYN820-1 SYN834-1 SYN844-1 SYN845-1 SYN848-1 SYN859-1 SYN876-1
SYN883-1 SYN886-1 SYN887-1 SYN900-1




EPS
GRP123-1.005 GRP123-2.005 GRP123-6.005 GRP124-3.005 GRP124-4.005 GRP126-1.005
GRP127-1.005 GRP129-1.005 GRP130-1.005 GRP130-2.005 GRP130-4.004 GRP132-2.005
GRP135-1.005 MGT066-1 SYN307-1 SYN418-1 SYN423-1 SYN424-1 SYN429-1 SYN441-1
SYN449-1 SYN513-1 SYN518-1 SYN545-1 SYN811-1 SYN821-1 SYN827-1 SYN835-1
SYN839-1 SYN841-1 SYN842-1 SYN851-1 SYN854-1 SYN855-1 SYN863-1




*/
