Very Similar Problems

`AGT_PlanT`	`ALG_FTA`	`ALG_Meier`	`ALG_TPS`	`ANA_KaliszykHOL`
`ANA_Paulson`	`ARI_FloorCeiling`	`ARI_NoVars`	`ARI_Vars`	`COLGRPLCLNUNSEVSYO_FOF_ProofGold`
`COLGRPLCLNUNSEVSYO_TH0_ProofGold`	`COL_MengIsabelle`	`COL_Paulson`	`COL_StrongFixedPoint`	`COM_GreweTypeSoundness`
`COMLATRNGNUM_SAD`	`COM_QuantifierElim`	`CSR_2Trolleys`	`CSR_AdimenSUMO`	`CSR_Cyc1`
`CSR_Cyc2`	`CSR_Cyc3`	`CSR_Cyc4`	`CSR_Cyc5`	`CSR_Cyc6`
`CSR_KitchenSink`	`CSR_LogAnswer`	`CSR_SUMO1`	`CSR_SUMO2`	`CSR_SUMO3`
`CSR_SUMO4`	`CSR_SUMO5`	`CSR_SUMO6`	`DAT_DH0Lists`	`DAT_KaliszykHOL`
`DAT_WaldmannCollections`	`FLD_Draeger`	`GEO_HalesUrban`	`GEO_ILTP`	`GEO_ILTP_Affine`
`GEO_KulikCurves`	`GEO_Quaife`	`GEO_Quaresma`	`GRA_HararyHell`	`GRA_PathTriangles`
`GRA_Ramsey`	`GRP_FromHR`	`GRP_Quasi`	`GRP_StanovskyCNF`	`GRP_StanovskyFOF`
`HWV_Safelogic`	`HWV_Safelogic2`	`HWV_ZurabCNF`	`HWV_ZurabFOF`	`HWV_ZurabTFA`
`HWV_ZurabTFF`	`ITP_HOL4FOFSetBushy`	`ITP_HOL4FOFSetChainy`	`ITP_HOL4FOFSynBushy`	`ITP_HOL4FOFSynChainy`
`ITP_HOL4TF0SetBushy`	`ITP_HOL4TF0SetChainy`	`ITP_HOL4TF0SynBushy`	`ITP_HOL4TF0SynChainy`	`ITP_HOL4TF1SynBushy`
`ITP_HOL4TF1SynChainy`	`ITP_HOL4TH0SetBushy`	`ITP_HOL4TH0SetChainy`	`ITP_HOL4TH0SynBushy`	`ITP_HOL4TH0SynChainy`
`ITP_HOL4TH1SynBushy`	`ITP_HOL4TH1SynChainy`	`ITP_VBTTF0`	`ITP_VBTTF1`	`ITP_VBTTH0`
`ITP_VBTTH0M`	`ITP_VBTTH1`	`ITP_VBTTH1M`	`ITP_VBTTX0`	`ITP_VBTTX1`
`KLE_Hoefner`	`KRS_OWL`	`KRS_SZSOntology`	`LAT_McCuneSet1`	`LAT_McCuneSet2`
`LAT_McCuneSet3`	`LAT_McCuneSet4`	`LAT_Paulson`	`LCL_CondensedDetachment`	`LCL_KaminskiModal`
`LCL_LemmasFOF`	`LCL_LemmasRezus`	`LCL_Paulson`	`LCL_PCBases`	`LCL_PCModal`
`LCL_PrincipiaMathematica`	`LCL_S10Modal`	`LCL_StrongNormalization`	`LCL_TPS`	`MGT_KampsCNF`
`MGT_KampsFOF`	`NLP_DorisCNF`	`NLP_DorisFOF`	`NUM_CimattiEUF`	`NUM_Landau`
`NUM_Naproche`	`NUM_RDNArithmetic`	`NUM_RobinsonAEq`	`NUM_RobinsonAId`	`NUM_SumOfTwoSquares`
`NUM_TPS`	`PHI_Horner`	`PLA_BlocksWorld`	`PRO_Halcomb`	`PUZ_TPS`
`QBF_SeidlEPR`	`QBF_SeidlFOF`	`QML_GoedelTranslation`	`REL_HoefnerCNF`	`REL_HoefnerFOF`
`SCT_ArrowCNF`	`SCT_ArrowTF1`	`SET_ILF`	`SET_Pastre`	`SET_QuaifeCNF`
`SET_QuaifeFOF`	`SET_TPS`	`SEU_BinaryRelations`	`SEU_BushyMizar`	`SEU_ChainyMizar`
`SEU_RootMizarBushy`	`SEU_RootMizarChainyLarge`	`SEU_RootMizarChainySmall`	`SEU_RootMizarNormal`	`SEU_TPSGazing`
`SEU_ZFCGlobal`	`SEU_ZFCLocal`	`SEV_ChadSimpleDifficult`	`SEV_DH0FixedPoint`	`SEV_KaliszykHOL`
`SEV_TPSEquivalenceRelations`	`SEV_TPSGVBMB`	`SEV_TPSRelnTheorems`	`SEV_TPSSTheorems`	`SWC_Deharbe`
`SWC_OEIS`	`SWC_SWReuseCNF`	`SWC_SWReuseFOF`	`SWV_Armando`	`SWV_EPRMutex`
`SWV_FFTCNF`	`SWV_FFTTF1`	`SWV_FTATF1`	`SWV_HoareCNF`	`SWV_HoareTF1`
`SWV_HuffmanTF1`	`SWV_JinjaCNF`	`SWV_JinjaTF1`	`SWV_NASASimplified`	`SWV_NASAUnsimplified`
`SWV_NSSharedCNF`	`SWV_NSSharedTF1`	`SWV_Paulson`	`SWV_Piskac`	`SWW_Filliatre1`
`SWW_Filliatre2`	`SWW_FixPointTFA`	`SWW_FTAFOF`	`SWW_KotelnikovTX0`	`SWW_KumarCakeML`
`SWW_Li`	`SWW_PaskevichTF1`	`SWW_SeparationLogic`	`SWW_SpecSharp`	`SWX_Hansen`
`SWX_Mesnard`	`SWX_PulinaNN`	`SYN_ALCCNF`	`SYN_ALCFOF`	`SYN_Church`
`SYN_Harrison`	`SYN_KalishMontague`	`SYN_PeterAndrews`	`SYN_SchmidtPSAT`	`SYN_SchmidtQBF`
`SYO_Lampert`	`SYO_NTFBarcan`	`SYO_SiderModal`	`SYO_TPS`	`SYO_TPSBasicFOTheorems`
`SYO_TPSBasicHOEqTheorems`	`SYO_TPSBasicHOTheorems`	`SYP_CNFInstantiation`	`SYP_LWBCounterSatisfiables`	`SYP_LWBTheorems`
`SYP_TH0Instantiation`