main = RunDefaultStrategyForObligation

runtimecomplexity = runtimecomplexitypreproc : TRSDumpProcessor[OutputDir="./"] : Fail

cpxreltrs = runtimecomplexity

runtimecomplexitypreproc =
  Repeat(0,*,First(CpxTrsDependencyGraph,CpxTrsNestedDefinedSymbol)) :
  Maybe(CpxRelTrsSTermination) :
  Maybe(CpxTrsRcToIrc)

# ===================================================== #
# ============= KEPT FOR TERMINATION OF S ============= #
# ===================================================== #

cls = CLSSlicing[SCCs=True]:
      CLSToITRS:
      itrs

dio = Diophantine[Range=3, Engine=PICOSAT]

otrs =
    Any(
      OTRSToCSR:
      csr,
      OTRSNonTerminationProcessor,
      Solve(
        OTRSToQTRS[Transformation=ThiemannII]:
        qtrs
      ),
      Prove(
        OTRSToQTRS[Transformation=Trivial]:
        qtrs
      ),
      Prove(
        OTRSToQTRS[Transformation=RaffelsieperZantema]:
        qtrs
      )
    )

qdp = Maybe(depgraph);
        First(
          AnyDelay(10000,
            Solve(
              Repeat(0,*,workOnDPs)
            ),
            qdpNonLoop
          ),
          Repeat(0,*,nontermOnDPs)
      )

# ===================================================== #
# ==================== QDP NONLOOP ==================== #
# ===================================================== #

beforeNonLoop = Maybe(QDPQReduction[KeepMinimality = False]):
                Maybe(QDPMNOC[Reversed = True, TestDepth = 1])

qdpNonLoop = beforeNonLoop:
             QDPNonLoop[NARROWING = 0, FULLPROOF = False, MAXITERATIONS=2500]

# ======================================================== #
# ==================== EQUATIONAL TRS ==================== #
# ======================================================== #

etes = ETESToETRS:equ

equ = Solve(
        Maybe(ETRSDirectTermination):
        Maybe(errrPolo):
        ETRSDependencyPairs:
        Maybe(EDPDependencyGraph):
        Solve(Repeat(0,*,workOnEDPs))
      )

# try polo and if it successful then reapply direct termination afterwards
errrPolo = Repeat(1,*,
             Timer(3000,
               ETRSRRRPolo[Degree = 0, Range = 3, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]
             )
           ):
           Maybe(ETRSDirectTermination)

workOnEDPs = First(
               EDPDependencyGraph,
               ESharpUsableEquations,
               EDPUsableRulesRP[Degree = 1, Range = 3, MaxSimpleDegree = 5, Engine = MINISAT],
               eqdpqdp,
               EDPRuleRemoval[Degree = 1, Range = 3, Mode = SEARCHSTRICT, MaxSimpleDegree = 5, Engine = MINISAT],
               EDPPolo[Degree = 1, Range = 3, Mode = SEARCHSTRICT, MaxSimpleDegree = 4, Engine = MINISAT, Active = True, MergeMutual = True],
               ECDPPolo[Degree = 0, Range = 1, Mode = SEARCHSTRICT, MaxSimpleDegree = 4, Engine = MINISAT],
               EDPPolo[Degree = 0, Range = 1, Mode = SEARCHSTRICT, MaxSimpleDegree = 4, Engine = MINISAT, Active = True, MergeMutual = True],
               ECDPPolo[Degree = 0, Range = 3, Mode = SEARCHSTRICT, MaxSimpleDegree = 4, Engine = MINISAT],
               EDPPolo[Degree = 0, Range = 3, Mode = SEARCHSTRICT, MaxSimpleDegree = 4, Engine = MINISAT, Active = True, MergeMutual = True],
               EDPUsableRules:
               eqdpqdp
             )

eqdpqdp = EDPToQDPProblem:
          Solve(
            Repeat(0,*,
              workOnDPs
            )
          )
# ====================================================== #
# ==================== TRS STANDARD ==================== #
# ====================================================== #

trs = TRSToQTRS:qtrs
gtrs = GTRSToQTRS:qtrs

qtrs = If[Condition = QTRSCardinality[Size = 1000], Sub1 = "bigqtrs", Sub2 = "smallqtrs"]

bigqtrs = QTRSDependencyPairs ;
          Repeat(0,*,
            First(
              QDPDependencyGraph,
              QDPSizeChange[Subterm = True],
              qdp
            )
          )

smallqtrs = First(
              Solve(
                QTRSToCSR:
                csr
              ),
              realqtrs
            )

realqtrs = Maybe(If[Condition = CeTA](QTRSUncurrying[NoEta = True, BeComplete = True, ApplicativeSignature = True])):
	   Repeat(0,*,
             Any(
               Timer(2000,
                 QTRSRRR[Order = POLO[Degree = 1, Range = 2, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]]
               ),
               Timer(4000,
                 QTRSRRR[Order = RPOS[Engine = MINISAT, Quasi = True, Afstype = MONOTONEAFS]]
               ),
               Timer(4000,
                 QTRSRRR[Order = KBO[Engine = YICES]]
               )
             )
           ):
           Maybe(QTRSAAECCNOC[Limit = 1]):
           QTRSDependencyPairs:
           qdp

workOnDPs = First(
              defaults,
              QDPATransformation[BeComplete = True, KeepMinimality = True],
              solver1,
              tosrs,
              If[Condition = CADE09[Size = 5]](solver2IndDecr, decrSolver2),
              If[Condition=CONSTNARR07](basicNI),
              If[Condition=CONSTNARR07](advancedNI),
              incr,
              Any(
                Timer(5000,
                  QDPNonMonReductionPair[Allstrict = False, PosRange = 1, NegRange = -1, Heuristic = CAND1, SatConverter = PLAIN[GTMode=DEEP, SumType=MINIMAL, PowersAsComb=False, UseIFFsInGT = True, NewTimes = True], Engine = MINISAT[Version = 2]]
                ),
                nontermSub1
              ),
              solver3,
              Any(
                QDPReductionPair[Active = True, Allstrict = False, Order = PMatroArcticInt[Collapse=True, Engine=MINISAT, Dimension=4, Max=1, Unary=True], MergeMutual = True],
                nontermSub2,
                QDPReductionPair[Active = True, Allstrict = False, Order = PMatroNat[Collapse=True, Engine=MINISAT, Dimension=4, Range=3], MergeMutual = True],
                Timer(5000, qdp_full_bounds)
              ),
              QDPRootLabelingFC2[Heuristic = LabelAll, PreserveMinimality = False]
            )

qdp_full_bounds = If[Condition = CeTA](
   QDPToSRS[Zantema = False]:full_bounds,
   QDPBoundsTAProcessor[STAS = DP_SPLIT, CRS = MYCRS2, MAX_CONFLICTS_TO_RESOLVE = 50000, MAX_TRANSITIONS_OF_A = 30000, MAX_STATES_OF_A = 50000]
)

nontermSub1 = If[Condition=RtiContains[Key=AVOID_NONTERM],
                Sub1="fail",
                Sub2="real_nontermSub1"
              ]

real_nontermSub1 = Timer(10000,
                     QDPNonTerm[TotalLimit = 3, LeftLimit = 3, RightLimit = 3]
                   )

nontermSub2 = If[Condition=RtiContains[Key=AVOID_NONTERM],
                Sub1="fail",
                Sub2="real_nontermSub2"
              ]

real_nontermSub2 = QDPNonTerm[TotalLimit = 8, LeftLimit = 8, RightLimit = 8]

defaults = First(
             depgraph,
             Timer(500, QDPMNOC[TestDepth = 2]),
             QDPUsableRules[BeComplete = True, UseApplicativeCeRules = True],
             QDPQReduction
           )

qdpmb = If[Condition = CeTA](
   QDPToSRS[Zantema = False]:QTRSRoofMatchBoundsTAProcessor[STAS = OSFEFS, CRS = KMS, MAX_STATES_OF_A = 200, MAX_TRANSITIONS_OF_A = 400],
   QDPMatchbounds[EdgeBound=700, NodeBound=300]
)

solver1 = First(
            Timer(250, QDPSizeChange[Subterm = True]),
            MRR06Heuristic[Sub1="usableRulesRP2", Sub2="ruleRemoval2", AllowATransformation=True],
            Timer(250, qdpmb)
          )

ruleRemoval2 = Any(
                 Timer(1000,
                   QDPMRR[Order = KBO[Engine = YICES]]
                 ),
                 Timer(1000,
                   QDPMRR[Order = POLO[Degree = 1, Range = 2, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]]
                 )
               )

usableRulesRP2 = Timer(900,
                   QDPUsableRulesRP[AllowATransformation = True, Degree = 1, Range = 2, MaxSimpleDegree = 5, Engine = MINISAT]
                 )

tosrs = QDPToSRS[Zantema = True]:
        QTRSDependencyPairs

decr = Repeat(1,*,
         First(
           Timer(500,QDPRewriting[Limit = 50, BeComplete = False]),
           Timer(500,QDPNarrowing[Limit = 0, BeComplete = False, Positional = True]),
           Timer(500,QDPInstantiation[Limit = 0])
         ):
         Repeat(0,*,defaults)
       )

solver2 = Any(
            First(
              Timer(5000, QDPReductionPair[Active = True, Allstrict = False, Order=NEGPOLO[Range=2, PosConstantRange=2, NegConstantRange=-2, Restriction=2, NegRangeCriterion = DAMPEN, PartialDioEval = True, Engine = MINISAT]]),
              Timer(5000, QDPReductionPair[Order = GPOLORATSIMPLE[Degree = 1, DenominatorRange = 4, NumeratorRange = 16, Heuristic = FULLRAT, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=True, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]]),
              Timer(5000, QDPReductionPair[Active = True, Allstrict = False, Order = PMatroNat[Collapse=True, Engine=MINISAT, Dimension=2, Range=1], MergeMutual = True]),
              Timer(5000, QDPReductionPair[Order = MMPOLO[StripExponents = True, Simplification = MAXIMUM, Heuristic = CAND1, SatConverter = PLAIN, Engine = MINISAT, Range = 1], ATrans = True, Active = True, MergeMutual = True, Usable = True, Allstrict = False])
            ),
            First(
              Timer(11000, QDPReductionPair[Active = True, Allstrict = False, Order = RPOS[Quasi = True, Engine=MINISAT, Afstype = FULLAFS]]),
              Timer(12000, QDPReductionPair[Active = True, Allstrict = False, Order = PMatroArcticInt[Collapse=True, Engine=MINISAT, Dimension=1, Max=5, Unary=True], MergeMutual = True])
            ),
            First(
              Timer(3000, QDPReductionPair[Order = KBO[Engine = MINISAT], MergeMutual = False]),
              Timer(20000, QDPReductionPair[Active = True, Allstrict = False, Order = POLO[Autostrict = False, Degree = 1, Range = 1, MaxSimpleDegree = 4, Engine = MINISAT], MergeMutual = True])
            )
          )

solver2IndDecr = First(
                   solver2,
                   qdpThm,
                   decr
                 )

decrSolver2 = First(
                decr,
                Any(
                  solver2,
                  Timer(2000, QDPQMonMRR[Order = POLO[Range = 2, Engine = MINISAT], DeleteROnly = False])
                )
              )



basicNI = Maybe(QDPComplexConstantRemoval):
          First(
            Timer(1700, QDPNonInfReductionPair[InductionCounter = 2, LeftChainCounter = 1, RightChainCounter = 0, Engine=MINISAT]),
            Timer(1700, QDPNonInfReductionPair[InductionCounter = 2, LeftChainCounter = 0, RightChainCounter = 1, Engine=MINISAT])
          )

advancedNI = If[Condition = BRANCHING,
               Sub1 = "tupleNI",
               Sub2 = "checkMax"
             ]

checkMax = If[Condition = SINGLERULE,
             Sub1 = "maxNIlong",
             Sub2 = "maxNIshort"
           ]

maxNIlong = Timer(12000,
              Maybe(QDPComplexConstantRemoval):
              QDPNonInfReductionPair[InductionCounter = 4, LeftChainCounter = 0, RightChainCounter = 1, Maximum=1, MaximumForSmall=2, Minimum=1, Engine=MINISAT]
            )

maxNIshort = Timer(6000,
               Maybe(QDPComplexConstantRemoval):
               QDPNonInfReductionPair[InductionCounter = 4, LeftChainCounter = 0, RightChainCounter = 1, Maximum=1, MaximumForSmall=2, Minimum=1, Engine=MINISAT]
             )

tupleNI = Timer(6000,
            Maybe(QDPComplexConstantRemoval):
            QDPNonInfReductionPair[InductionCounter =2, Maximum = 1, DegreeTuple = -2, LeftChainCounter = 2, RightChainCounter = 0, Engine=MINISAT]
          )


incr = Repeat(1,*,
         First(
           Timer(500,QDPRewriting[Limit = 50, BeComplete = False]),
           Timer(500,QDPNarrowing[Limit = 1, BeComplete = False, Positional = True]),
           Timer(500,QDPInstantiation[Limit = 2]),
           Timer(2000,QDPForwardInstantiation[Limit = 1])
         ):
         Repeat(0,*,defaults)
       )

solver3 = Any(
            Timer(15000, QDPReductionPair[Active = True, Allstrict = False, Order = PMatroNat[Collapse=True, Range = 3, Engine = MINISAT, Dimension = 2], MergeMutual = True]),
            Timer(15000, QDPReductionPair[Active = True, Allstrict = False, Order = PMatroArcticInt[Collapse=True, Max = 3, Engine = MINISAT, Dimension = 3, Unary=True], MergeMutual = True]),
            Timer(10000, QDPReductionPair[Active = True, Allstrict = False, Order = POLO[Autostrict = False, Degree = SIMPLE_MIXED, Range = 1, MaxSimpleDegree = 4, Engine = MINISAT], MergeMutual = True]),
            Timer(20000, QDPSemanticLabelling[CarrierSetSize = 2, Strategy="semlab", AllowQuasi=False, Engine=SAT4J, IncrementalEngine=INCREMENTAL]),
            Timer(1000, QDPReductionPair[Active = True, Allstrict = False, Order = POLO[Autostrict = False, Degree = 2, Range = 2, MaxSimpleDegree = 4, Engine = MINISAT], MergeMutual = True]),
            Timer(1000, QDPReductionPair[Active = True, Allstrict = False, Order = PMatroArcticInt[Collapse=True, Engine=MINISAT, Dimension=1, Max=1, Min=-1, Unary=True], MergeMutual = True])
          )

semlab = RepeatS(1,*,
           First(
             QDPDependencyGraph,
             MRR06Heuristic[AllowATransformation = False, Sub1="usableRulesRP1", Sub2="ruleRemoval1"],
             Timer(7500,QDPReductionPair[Active = True, Allstrict = False, Order = POLO[Degree = 1, Range = 1, MaxSimpleDegree = 4, Engine = MINISAT], MergeMutual = True])
           )
         )
ruleRemoval1 = Timer(500,
                 QDPMRR[Order = POLO[Degree = 1, Range = 1, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]]
               )

usableRulesRP1 = Timer(600,
                   QDPUsableRulesRP[AllowATransformation = False, Degree = 1, Range = 1, MaxSimpleDegree = 5, Engine = MINISAT]
                 )

# ============================================================ #
# ==================== QDP THEOREM PROVER ==================== #
# ============================================================ #

# Subsection for techniques based on QDPTheoremProver
qdpThm = First(
           qdpThmNoUnpack,
           qdpThmWithUnpackR3,
           qdpThmWithUnpackInstantiation
         )

qdpThmNoUnpack = QDPTheoremProver[Order = POLO[Engine = MINISAT, Range = 1, Degree = 1],
                                  RuleHeuristic = SMALL_OR_LAST_CALL,
                                  TheoremProverStrategy = "thm",
                                  TheoremProverTimeLimit = "3",
                                  UnpackConstructors = False,
                                  Runner = APROVE,
                                  RemoveDuplicates = False]:
                 Solve(RunDefaultStrategyForObligation)

qdpThmWithUnpack = QDPTheoremProver[Order = POLO[Engine = MINISAT, Range = 1, Degree = 1],
                                    RuleHeuristic = SMALL_OR_LAST_CALL,
                                    TheoremProverStrategy = "thmShort",
                                    TheoremProverTimeLimit = "3",
                                    UnpackConstructors = True,
                                    Runner = APROVE,
                                    RemoveDuplicates = True]:
                   Solve(RunDefaultStrategyForObligation)

qdpThmWithUnpackR3 = QDPTheoremProver[Order = POLO[Engine = MINISAT, Range = 3, Degree = 1],
                                      RuleHeuristic = SMALL_OR_LAST_CALL,
                                      TheoremProverStrategy = "thmShort",
                                      TheoremProverTimeLimit = "3",
                                      UnpackConstructors = True,
                                      Runner = APROVE,
                                      RemoveDuplicates = True]:
                     Solve(RunDefaultStrategyForObligation)

qdpThmWithUnpackInstantiation = QDPInstantiation[Limit=2]:
                                qdpThmWithUnpack


nontermOnDPs = If[Condition=RtiContains[Key=AVOID_NONTERM],
                 Sub1="fail",
                 Sub2="real_nontermOnDPs"
               ]

real_nontermOnDPs = First(
                      defaults,
                      QDPATransformation[BeComplete = True, KeepMinimality = False],
                      QDPNonTerm[TotalLimit = 3, LeftLimit = 3, RightLimit = 3]
                    )


# ====================================================== #
# ==================== SRS STANDARD ==================== #
# ====================================================== #
srs = TRSToQTRS:qsrs

qsrs = Any(
         Solve(SRSNonLoop),
         Solve(Timer(10000,SRSNonLoop[CompareWithOC1=0])),
         Solve(workOnSRS),
         Solve(QTRSReverse:workOnSRS)
       )


workOnSRS = Any(
              srsmb,
              Maybe(srsrrr):
               Maybe(QTRSAAECCNOC[Limit=1]):
               QTRSDependencyPairs:
              srsdp,
              srsrootlabloop
            )

full_bounds = QTRSRoofMatchBoundsTAProcessor[STAS = OSFEFS, CRS = KMS, MAX_CONFLICTS_TO_RESOLVE = 50000, MAX_STATES_OF_A = 30000, MAX_TRANSITIONS_OF_A = 50000]

srsmb = If[Condition = CeTA](
  Timer(5000, full_bounds),
  Any(
          Timer(5000, QTRSMatchbounds[NodeBound=160, EdgeBound=320]),
          QTRSStripSymbols:
          Timer(5000, QTRSMatchbounds[NodeBound=160, EdgeBound=320]),
          Timer(5000, QTRSRoofMatchBoundsTAProcessor[STAS = OSFEFS, CRS = KMS, MAX_STATES_OF_A = 200, MAX_TRANSITIONS_OF_A = 400])
     )
)

srsrootlabloop = Solve(
                   rootlab:
                   First(
                     Solve(workOnSRS2),
                     srsrootlabloop
                   )
                 )

workOnSRS2 = Maybe(srsrrr2):
             Maybe(QTRSAAECCNOC[Limit=1]):
             QTRSDependencyPairs:
             srsdp2


#srsrrr = Timer(15000, srsmanyrrr)
srsrrr = Timer(15000,
           Repeat(0, *,
             Any(QTRSRRR[Order = KBOPOLO])
           )
         )

#srsrrr2 = Timer(25000, srsmanyrrr)
srsrrr2 = Timer(15000,
            Repeat(0, *,
              Any(QTRSRRR[Order = KBOPOLO])
            )
          )

srsmanyrrr = Repeat(0, *,
               Any(
                 QTRSRRR[Order = KBO[Engine = YICES]],
                 QTRSRRR[Order = POLO[Degree = 1, Range = 3, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]],
                 QTRSRRR[Order = PMatroNat[Engine = MINISAT, Range = 1, Dimension = 3, Collapse = False]],
                 QTRSRRR[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = MONOTONEAFS]]
               )
             )

srsmanyrrr2 = Repeat(0, *,
                Any(
                  QTRSRRR[Order = KBO[Engine = YICES]],
                  QTRSRRR[Order = POLO[Degree = 1, Range = 2, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT]],
                  QTRSRRR[Order = PMatroNat[Engine = MINISAT, Range = 1, Dimension = 2, Collapse = False]]
                )
              )


srsdp = Solve(
          Repeat(0, *,
            First(
              QDPDependencyGraph,
              srseasy,
              Any(
                srsRedPair,
                Solve(
                  Repeat(0,*,srsnontermOnDPs)
                )
              ) # Any
            ) # First
          ) # Repeat
        ) # Solve

srsdp2 = Solve(
           Repeat(0, *,
             First(
               QDPDependencyGraph,
               srseasy,
               srsRedPair2
             )
           )
         )

srseasy = First(
            QDPDependencyGraph,
            Timer(500, QDPMNOC[TestDepth = 2]),
            QDPUsableRules[BeComplete = True, UseApplicativeCeRules = True],
            QDPQReduction
          )

srsnontermOnDPs = First(
                    srseasy,
                    Timer(6000, QDPNonTerm[TotalLimit = 3, LeftLimit = 3, RightLimit = 3])
                  )

srsdecr = Repeat(1,*,
            First(
              Timer(500,QDPRewriting[Limit = 50, BeComplete = False]),
              Timer(500,QDPNarrowing[Limit = 0, BeComplete = False, Positional = True]),
              Timer(500,QDPInstantiation[Limit = 0])
            ):
            Repeat(0,*,srseasy)
          )

srsRedPair = First(
               Any(
                 Timer(1000, QDPSizeChange[Subterm = True]),
                 Timer(10000, QDPMRR[Order = POLO[Degree = 1, Range = 3, Autostrict = False, MaxSimpleDegree = 10000, Engine = MINISAT]]),
                 Timer(10000, QDPReductionPair[Order = NEGPOLO[Engine = MINISAT[Version = 2], Range = 2, NegConstantRange=-2, PosConstantRange = 2, NegRangeCriterion = DAMPEN, PartialDioEval = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                 Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 1, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                 Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 5, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                 Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])),
               Any(
                 Timer(10000, QDPReductionPair[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = FULLAFS], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                 Timer(10000, QDPUsableRulesRP[AllowATransformation = False, Degree = 1, Range = 3, MaxSimpleDegree = 5, Engine = MINISAT]),
                 Timer(10000, QDPReductionPair[Order = GPOLORATSIMPLE[Degree = 1, DenominatorRange = 4, NumeratorRange = 16, Heuristic = FULLRAT, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=False, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]]),
                 Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 2, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                 Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 3, Dimension = 3, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                 Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 5, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])),
               srsdecr,
               Any(
                 QDPSemanticLabelling[CarrierSetSize = 2, Strategy="semlab", AllowQuasi=False, Engine=SAT4J, IncrementalEngine=INCREMENTAL],
                 QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 6, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False],
                 QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False],
                 QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 3, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False],
                 QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 2, Dimension = 7, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]
               )
             )


srsRedPair2 = First(
                Any(
                  Timer(5000, QDPSizeChange[Subterm = True]),
                  Timer(10000, QDPReductionPair[Order = NEGPOLO[Engine = MINISAT[Version = 2], Range = 2, NegConstantRange=-2, PosConstantRange = 2, NegRangeCriterion = DAMPEN, PartialDioEval = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                  Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 1, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                  Timer(10000, QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 5, Degree = 1, LinearMonotone = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                  Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])),
                Any(
                  Timer(10000, QDPReductionPair[Order = PPO[Engine = MINISAT[Version = 2], Quasi = True, Multiset = False, Lex = True, Prec = True, Permute = True, Xgengrc = True, Afstype = FULLAFS], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                  Timer(10000, QDPReductionPair[Order = GPOLORATSIMPLE[Degree = 1, DenominatorRange = 4, NumeratorRange = 16, Heuristic = FULLRAT, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=False, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]]),
                  Timer(10000, QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 2, Dimension = 3, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]),
                  Timer(10000, QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 3, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False])),
                Any(
                  QDPSemanticLabelling[CarrierSetSize = 2, Strategy="semlab", AllowQuasi=False, Engine=SAT4J, IncrementalEngine=INCREMENTAL],
                  QDPReductionPair[Order = POLO[Engine = MINISAT[Version = 2], Range = 2, Degree = SIMPLE_MIXED], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False],
                  QDPReductionPair[Order = MATRO[Engine = MINISAT, SatConverter=PLAIN[UseShifts=True, UseBinaryShifts=False, SumType=DUAL_COMB], Range=8, Denominator=2, Rational=True, Type=COLLAPSINGDPTUPLE[Size=2]]],
                  QDPReductionPair[Order = PMatroNat[Engine = MINISAT[Version = 2], Range = 1, Dimension = 6, Collapse = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False],
                  QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Max = 1, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False],
                  QDPReductionPair[Order = PMatroArcticInt[Engine = MINISAT[Version = 2], Min = -1, Max = 3, Dimension = 5, Collapse = True, Unary = True], Allstrict = False, Usable = True, Active = True, ATrans = False, MergeMutual = False]
                )
              )

# ================================================================= #
# ==================== ROOT LABELING TRS & SRS ==================== #
# ================================================================= #

# can be used both for TRSs and for SRSs
rootlab = Maybe(QTRSFlatCC):
          QTRSRootLabeling

relrootlab = Maybe(RelTRSFlatCC):
          RelTRSRootLabeling[Heuristic = LabelAll]


# ====================================================== #
# ==================== TRS RELATIVE ==================== #
# ====================================================== #

rtrs = Maybe(RelTRSSCleaner):
       First(
         Solve(RelTRSEmptinessCheck:RunDefaultStrategyForObligation),
         Solve(RelTRSQCCheck:qtrs),
         Solve(RelTRStoQDP:qdp),
         Any(
           relloopfinder,
           workonrel,
           relrootlabloop
         )
       )

relrootlabloop = Solve(
                   relrootlab:
                   First(
                     workonrel,
                     relrootlabloop
                   )
                 )

workonrel = Solve(
              Repeat(0, *,
                First(
                  RelTRSEmptinessCheck:
                  RunDefaultStrategyForObligation,
                  relruleremoval
                )
              )
            )

relloopfinder = First(
                  Timer(5000, RelTRSEmission),
                  Timer(10000, RelTRSLoopFinder[TotalLimit = 3, LeftLimit = 3, RightLimit = 3]),
                  RelTRSLoopFinder[TotalLimit = 8, LeftLimit = 8, RightLimit = 8]
                )

relruleremoval = First(
                   Any(
                     Timer(8000, RelRR[Order = KBO[Engine = YICES]]),
                     Timer(8000, RelRR[Order = RPOS[Engine = MINISAT, Quasi = True, Afstype = MONOTONEAFS]]),
                     Timer(8000, RelRR[Order = POLO[Engine = MINISAT, Degree = 1, Range = 1]]),
                     Timer(8000, RelRR[Order = PMatroNat[Collapse=False, Engine = MINISAT, Dimension = 2, Range = 1]])
                   ),
                   Any(
                     Timer(12000, RelTRSSemanticLabelling),
                     Timer(12000, RelRR[Order = PMatroNat[Collapse=False, Engine = MINISAT, Dimension = 2, Range = 3]]),
                     Timer(12000, RelRR[Order = POLO[Engine = MINISAT, Degree = SIMPLE_MIXED, Range = 1]]),
                     Timer(12000, RelRR[Order = POLO[Engine = MINISAT, Degree = 1, Range = 7]])
                   ),
                   Any(
                     RelRR[Order = KBOPOLO],
                     RelRR[Order = PMatroNat[Collapse=False, Engine = MINISAT, Dimension = 3, Range = 3]],
                     RelRR[Order = PMatroNat[Collapse=False, Engine = MINISAT, Dimension = 5, Range = 2]],
                     RelRR[Order = POLO[Engine = MINISAT, Degree = SIMPLE_MIXED, Range = 3]]
                   )
                 )


# ====================================================== #
# ==================== SRS RELATIVE ==================== #
# ====================================================== #

rsrs = Maybe(RelTRSSCleaner):
       First(
         Solve(
           RelTRSEmptinessCheck:
           RunDefaultStrategyForObligation
         ),
         Any(
           relloopfinder,
           workOnRelSRS,
           relSRSrootlabloop,
           RelSRSReverse:
           Any(
             relloopfinder,
             workOnRelSRS,
             relSRSrootlabloop
           )
         )
       )

relSRSrootlabloop = Solve(
                      relrootlab:
                      First(
                        workOnRelSRSrootlab,
                        relSRSrootlabloop
                      )
                    )

workOnRelSRS = Solve(
                 Repeat(0, *,
                   First(
                     RelTRSEmptinessCheck:RunDefaultStrategyForObligation,
                     relSRSruleremoval
                   )
                 )
               )

workOnRelSRSrootlab = Solve(
                        Repeat(0, *,
                          First(
                            RelTRSEmptinessCheck:RunDefaultStrategyForObligation,
                            relSRSruleremovalRootlab
                          )
                        )
                      )

relSRSruleremoval = First(
                      Any(
                        Timer(12000, RelRR[Order = KBO[Engine = YICES]]),
                        Timer(12000, RelRR[Order = POLO[Engine = MINISAT, Degree = 1, Range = 1]]),
                        Timer(12000, RelRR[Order = PMatroNat[Engine = MINISAT, Dimension = 2, Range = 2, Collapse = False]])
                      ),
                      Any(
                        RelTRSSemanticLabelling,
                        RelRR[Order = POLO[Engine = MINISAT, Degree = 1, Range = 5]],
                        RelRR[Order = RPOS[Engine = MINISAT, Quasi = True, Afstype = MONOTONEAFS]],
                        RelRR[Order = PMatroNat[Engine = MINISAT, Dimension = 3, Range = 3, Collapse = False]],
                        RelRR[Order = PMatroNat[Engine = MINISAT, Dimension = 6, Range = 1, Collapse = False]]
                      ),
                      relrootlab
                    )

relSRSruleremovalRootlab = First(
                             Any(
                               Timer(12000, RelRR[Order = KBO[Engine = YICES]]),
                               Timer(12000, RelRR[Order = POLO[Engine = MINISAT, Degree = 1, Range = 1]]),
                               Timer(12000, RelRR[Order = PMatroNat[Engine = MINISAT, Dimension = 2, Range = 2, Collapse = False]])
                             ),
                             Any(
                               Timer(20000, RelTRSSemanticLabelling),
                               Timer(20000, RelRR[Order = POLO[Engine = MINISAT, Degree = 1, Range = 5]]),
                               Timer(20000, RelRR[Order = PMatroNat[Engine = MINISAT, Dimension = 3, Range = 1, Collapse = False]])
                             )
                           )

# ================================================= #
# ==================== HASKELL ==================== #
# ================================================= #

hs = HaskellLambdaReduction:
     HaskellCaseReduction:
     HaskellIfReduction:
     HaskellIrrPatReduction:
     HaskellBindingReduction:
     HaskellCondReduction:
     HaskellNewTypeReduction:
     HaskellIrrPatReduction:
     HaskellLetReduction:
     HaskellNumReduction:
     HaskellSplit:
     HaskellNarrowing[AddTypes = False, TerminationStrategy="workOnQDPHaskell", NonTerminationStrategy="workOnQDPNonTermHaskell"]

workOnQDPHaskell = RepeatS(0,*,
                     First(
                       QDPMNOC,
                       QDPDependencyGraph,
                       decrHaskell,
                       QDPSizeChange[Subterm=True],
                       QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=0,AfsRestriction=2],
                       parallelHaskell,
                       Timer(2000, QDPReductionPair[Order=POLO[Engine=MINISAT[Version = 2], Range=3, Degree=1], Active=True]),
                       basicNonInfHaskell,
                       ptrHaskell,
                       incrHaskell
                     )
                   )

workOnQDPNonTermHaskell = RepeatS(0,*,
                            First(
                              QDPDependencyGraph,
                              QDPUsableRules,
                              nonTermParallelHaskell,
                              QDPLoopFinder[TotalLimit=4, LeftLimit=0, RightLimit=4]
                            )
                          )

nonTermParallelHaskell = First(
                           Timer(5000, Any(
                                         QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=2,AfsRestriction=2],
                                         QDPRuleRemoval[Range=2]
                                       )
                           ),
                           Timer(2000, QDPReductionPair[Order=POLO[Engine=MINISAT[Version = 2],Range=1,Degree=1],Active=True])
                         )

parallelHaskell = First(
                    Timer(5000, Any(
                                  QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=2,AfsRestriction=2],
                                  QDPRuleRemoval[Range=2]
                                )
                    ),
                    Timer(2000, QDPReductionPair[Order=POLO[Engine=MINISAT[Version = 2], Range=1, Degree=1], Active=True]),
                    Timer(5000,QDPNonTerm)
                  )

basicNonInfHaskell = QDPAddDPConstraints[InductionCounter = 2, LeftChainCounter = 0, RightChainCounter = 1]:
                     QDPNonInfReductionPair[InductionCounter = 2, LeftChainCounter = 0, RightChainCounter = 1]

ptrHaskell = QDPPairToRule

incrHaskell = Repeat(1,*, First(
                            QDPRewriting,
                            QDPNarrowing[Limit = 4]
                          ):
                          Repeat(0,*, defaults)
                    )

decrHaskell = Repeat(1,*,
                First(QDPRewriting, QDPNarrowing, QDPInstantiation):
                Repeat(0,*,defaults)
              )

# ========================================================= #
# ==================== TRS CONDITIONAL ==================== #
# ========================================================= #

ctrs = CTRSToQTRS:qtrs


# =============================================================== #
# ==================== NEW CONTEXT SENSITIVE ==================== #
# =============================================================== #

csr = Repeat(0,*,
        Any(
          Timer(500, CSRRRR[Order=POLO[Engine=MINISAT, Range = 2, Degree = 1]]),
          Timer(1000, CSRRRR[Order=PMatroNat[Collapse=True, Engine = MINISAT, Range = 1, Dimension = 2]]),
          Timer(500, CSRRRR[Order=POLO[Engine=MINISAT, Range = 1, Degree = 1]])
        )
      ):
      Any(
        Timer(10000, CSRNonTermination),
        Maybe(CSRInnermost):
        First(
          Timer(35000,
            Solve(qcsdp)
          ),
          Solve(csTransformations)
        )
      )

csrLuc = CSRToQTRS[Transformation = Lucas]
csrZan = CSRToQTRS[Transformation = Zantema]
csrFR = CSRToQTRS[Transformation = ImprovedFerreiraRibeiro]
csrGM1 = CSRToQTRS[Transformation = IncompleteGieslMiddeldorp]
csrGM2 = CSRToQTRS[Transformation = CompleteGieslMiddeldorp]
csrGM3 = CSRToQTRS[Transformation = InnermostGieslMiddeldorp]
csrTRIV = CSRToQTRS[Transformation = Trivial]

qcsdp = CSRToQCSDP:
        Repeat(0,*,qcsStrategy):
        qcsToQdp

csTransformations = CSR06Heuristic

csrTerm = Any(
            Solve(csrZan:csrqtrs),
            Solve(csrGM1:csrqtrs),
            Solve(csrFR:csrqtrs),
            Solve(csrTRIV:csrqtrs),
            Solve(csrGM2:csrqtrs)
          )

csrInn = Any(
           Solve(csrZan:csrqtrs),
           Solve(csrGM3:csrqtrs),
           Solve(csrTRIV:csrqtrs),
           Solve(csrFR:csrqtrs)
         )

qcsStrategy = First(
                QCSDependencyGraph,
                qcsSubterm,
                QCSUsableRules,
                qcsSolver,
                qcsPairTrans
              )

qcsPairTrans = First(
                 QCSDPInstantiation,
                 QCSDPForwardInstantiation,
                 QCSDPNarrowing
               )

qcsSubterm = QCSDPSubterm[Engine=SAT4J]

qcsSolver = First(
              Timer(1000, QCSDPPoloRuleRemoval[Degree = 1, Mode = SEARCHSTRICT, Range = 2, MaxSimpleDegree = 5, Engine = MINISAT]),
              Any(
                Timer(10000, QCSDPNeededSymbols[Order = NEGPOLO[Range=2, PosConstantRange=2, NegConstantRange=-1, Restriction=2, NegRangeCriterion = DAMPEN, PartialDioEval = True, Engine=MINISAT]]),
                Timer(5000, QCSDPNeededSymbols[Order = MMPOLO[StripExponents = True, Simplification = MAXIMUM, Heuristic = CSIF, SatConverter = PLAIN, Engine = MINISAT, Range = 1]]),
                Timer(10000, QCSDPNeededSymbols[Order = GPOLORATSIMPLE[\
                    Degree = 1, DenominatorRange = 4, NumeratorRange = 16, OPCSolver = MBYNTOFORMULA[FixDenominator = True, Solver = SAT[SatConverter = PLAIN[UseShifts=True, UseBinaryShifts=False, UnaryMode=CIRCUIT, NewUnaryPower=True], SatBackend = MINISAT, Simplification = MAXIMUM, SimplifyAll = True, StripExponents = False]], MaxSimpleDegree = -1, StrictMode = SEARCHSTRICT]]),
               Timer(5000, QCSDPNeededSymbols[Order = RPOS[Quasi = True, Engine=MINISAT, AfsType=FULLAFS]]),
               Timer(7000, QCSDPNeededSymbols[Order = POLO[Degree = 1, Range = 2, MaxSimpleDegree = 4, Engine = MINISAT], MergeMutual = True]),
               Timer(2000, QCSDPNeededSymbols[Order = MATRO[Engine=MINISAT,Range = 1, Type = COLLAPSINGDPTUPLE[Size = 2, Filter = NOFILTER]], MergeMutual = True] )\
               )
             )

qcsToQdp = QCSDPToQDP:qdp

csrqtrs = Repeat(0,*,
            Timer(2000, QTRSRRRPolo[Degree = 1, Range = 2, Autostrict = False, MaxSimpleDegree = 5, Engine = MINISAT])
          ):
          Maybe(QTRSAAECCNOC[Limit = 1]):
          QTRSDependencyPairs:
          Maybe(QDPDependencyGraph);
          Repeat(0,*,workOnDPs)


# =============================================== #
# ==================== ITRS  ==================== #
# =============================================== #

# if there is nothing predefined in there, just use the QDP framework
itrs = First(
         ITRStoQTRS[Apply = CONSTONLY]:RunDefaultStrategyForObligation,
         itrsToIdp:idpv2
       )

#itrsToIdpV2 = ITRSToIDPV2
itrsToIdp = ITRSToIDP:
            Maybe(IDPUsableRules):
            Maybe(IDPCapGraph):
            Maybe(idpGraphOp)


# =============================================== #
# ==================== IDPv1 ==================== #
# =============================================== #

#Only used by the JBC/LLVM people nowadays:
idpv1 = First(
             IDPtoQDP[Apply = CONSTONLY]:RunDefaultStrategyForObligation,
             First(
               Solve(
                 Timer(12000, idpFast)
               ),
               AnyDelay(5000,
                 Solve(idpSlow),
                 Solve(IDPtoQDP[Apply = ALWAYSFILTER]:RunDefaultStrategyForObligation)
               )
             )
           )

idpSlow = Repeat(0,*,
            Maybe(idpGraphOp):
            AnyDelay(7000,
              Timer(30000, idpNonInfFast),
              idpNonInfSlow
            )
          )

idpFast = Repeat(0,*,
            Maybe(idpGraphOp):
            idpNonInfIntFastFilter
          )

idpNonInfFull = Any(
                  idpNonInfFast,
                  idpNonInfSlow
                )

idpNonInfFast = Any(
                  idpNonInfNatFast,
                  idpNonInfIntFast
                )

idpNonInfSlow = AnyDelay(10000,
                  Any(
                    idpNonInfIntSlow,
                    idpNonInfIntShapedLR,
                    idpNonInfIntShapedLL
                  ),
                  First(
                    idpNonInfIntVerySlow,
                    Solve(IDPtoQDP[Apply = ALWAYSFILTER]:RunDefaultStrategyForObligation)
                  )
                )

idpGraphOp = IDPDependencyGraph:Maybe(IDPUsableRules)
idpNonInfNatFast = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = DEFAULT_SHAPE, Nat = True, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 1, MaxRightSteps = 1]]]]
idpNonInfNatSlow = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = CAND1_SHAPE, Nat = True, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 3, MaxRightSteps = 1]]]]
idpNonInfIntFast = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = DEFAULT_SHAPE, Nat = False, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 1, MaxRightSteps = 1]]]]
idpNonInfIntFastFilter = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = CAND1_SHAPE[MaxProjectionPos = False, MaxArithPos = False], Nat = False, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxDegree = 1, MaxLeftSteps = 0, MaxRightSteps = 0, MinLeftSteps = 0, MinRightSteps = 0]]]]
idpNonInfIntSlow = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = DEFAULT_SHAPE, Nat = False, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 3, MaxRightSteps = 2]]]]
idpNonInfIntVerySlow = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = DEFAULT_SHAPE, Nat = False, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 8, MaxRightSteps = 1]]]]
idpNonInfIntShapedLL = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = CAND1_SHAPE, Nat = False, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 2, MaxRightSteps = 0]]]]
idpNonInfIntShapedLR = IDPNonInf[Solver = GPOLO[PoloShapeHeuristic = CAND1_SHAPE, Nat = False, Degree = -1, OPCSolver = NATOPCSATSOLVER[Engine = MINISAT], ConstraintGenerator = NONINFCONSTRAINTS[PathGenerator = METRICPATHS[MaxLeftSteps = 2, MaxRightSteps = 1]]]]

# =============================================== #
# ==================== IDPv2 ==================== #
# =============================================== #

#Make idpv2 the default idp version:
idp = idpv2

# let the IDP framework enter first,
# the QDP framework joins after some time

idpv2 = Repeat(0,*,
        Maybe(idpGraphOp):
        AnyDelay(7000,
          Timer(30000, idpNonInfFast),
          Any(
            idpNonInfSlow,
            Delay(22000,
              Solve(
                IDPtoQDP[Apply = ALWAYS]:
                RunDefaultStrategyForObligation
              ) # Solve
            ) # Delay
          ) # Any
        ) # AnyDelay
      ) # Repeat

idp2 = idp2Preprocessing:
       idp2Loop

idp2Preprocessing = Maybe(IDP2DupplicateArgsFilter):
                    Maybe(IDP2ConstantArgsFilter):
                    Maybe(IDP2LongNamesFilter):
                    IDP2TypeInference:
                    Maybe(IDP2SCC):
                    Maybe(IDP2UsableRules):
                    Maybe(idpv2PathCollapse):
                    Maybe(idp2Bisimulation)

idp2Loop = Maybe(IDP2KnowledgeGeneration):
           Maybe(IDP2SCC):
           Maybe(idp2Bisimulation):
           Solve(
             Maybe(idp2VarPartitioning);
             IDPPolyIntInterpretationSwitch[Shapes = CONSTRUCTOR_SUM_LINEAR_SHAPE]:
             Repeat(1,*,
               Repeat(1,*,
                 Maybe(
                   IDP2SCC;
                   Maybe(idpv2AfterEdgeDeletion)
                 ):
                 Maybe(
                   First(
                     IDP2KnowledgeGeneration:
                     Maybe(idp2Bisimulation):
                     Maybe(idpv2AfterEdgeDeletion),
                     idpv2PathCollapse
                   ) # First
                 ): # Maybe
                 Any(
                   IDP2EmptyProblem,
                   AnyDelay(5000,
                     idpNonInf;
                     Maybe(idpv2AfterEdgeDeletion),
                     IDP2LoopUnroll:
                     idpNonInf;
                     Maybe(idpv2AfterEdgeDeletion),
                     Solve(idp2ToQdp)
                   ) # AnyDelay
                 ) # Any
               ) # Repeat
             ) # Repeat
           ) # Solve

delayedFail = Delay(1000000, FAIL)

idp2VarPartitioning = FAIL:
                      IDP2VariablePartitioning[Mode = SINGLE_PARTITIONS]

idp2Bisimulation = FAIL:
                   IDP2DeepFSBisimulation

idp2ToQdp = Maybe(IDP2ItpfScheduler[Strategy = PREPARE_QDP]):
            Maybe(IDP2FreeVariablesFilter):
            IDP2toQDP[Apply = CONSTONLY]:
            RunDefaultStrategyForObligation

#: QDPDumpChains[StartTerm = "47_1_MI(47_0_iL(pos(s(01())))", MaxPSteps = 5, MaxRSteps = -1]

idpv2AfterEdgeDeletion = Maybe(IDP2UsableRules):
                         idpv2PathCollapse:
                         Maybe(idp2Bisimulation)

idpv2PathCollapse = First(
                      IDP2InfPaths[MaxEdgeGain = 2]:
                      Maybe(IDP2RewritePaths[MaxEdgeGain = 2]):Maybe(IDP2UsableRules),
                      IDP2RewritePaths[MaxEdgeGain = 2]:
                      Maybe(IDP2UsableRules)
                    )

idpNonInf = IDP2NonInf[Solver = SAT_SMT_SOLVER]


# =============================================== #
# ===================== JBC ===================== #
# =============================================== #

jbc = BareJBCToJBC : RunDefaultStrategyForObligation

jbcTerm = Any(
            Solve(jbcAbstract),
            Solve(jbcEval)
          )

jbcDebugGraph = JBCToTerminationGraph[TryNontermProofs=True]:
                First(
                  JBCNonTerm,
                  Yes
                )

jbcEval =
  Timer(1000,
    JBCToTerminationGraph[
      TryNontermProofs=False,
      LoopMergeCostBase=0,
      LoopMergeCostChange=0,
      IncomingInstanceFinder=False,
      TryMerging=False,
      TrySeparateMethodAnalysis=False,
      TryParallelPathMerging=False,
      Multithreaded=False
    ]
  ) : RunDefaultStrategyForObligation

jbcTermGraph = TerminationGraphToSCC

jbcAbstract = JBCToTerminationGraph[TryNontermProofs=True];jbcGraph

jbcT2 = TerminationGraphToComplexityRuleSet:JBCGraphEdgesToIntTrs[Weighted=False]:IRSToT2SysProcessor:RunDefaultStrategyForObligation

jbcGraph = Any(
                Solve(
                  WallTimer(25000,
                    JBCNonTerm
                  )
                ),
                Solve(
                  TerminationGraphToSCC[ApplyAnalyses = "aprove.Framework.Bytecode.Processors.ToSCC.UsedFieldsAnalysis aprove.Framework.Bytecode.Processors.ToSCC.MarkerFieldAnalysis"];
                  jbcGraphSCC
                )
              )

jbcGraphSCC = jbcGraphSCCIRS

jbcGraphSCCFast = jbcGraphSCCIRS
jbcGraphSCCSlow = jbcGraphSCCIDPv1
jbcGraphSCCIDPv2 = TerminationSCCToIDPv2[CleanRules=False]:
                   jbcIDPv2

jbcGraphSCCIDPv1 = TerminationSCCToIDPv1[EncodeStaticFields=True, EncodeReferenceTypesAsTerms=True, EncodePathLength=False]:
                   jbcIDPv1


jbcGraphSCCIRS = TerminationSCCToIRS[EncodeStaticFields=True, EncodeArrayLengthSeparately=False, ApplyPathLength=False, TryQDPExport=True]:RunDefaultStrategyForObligation


jbcIDPv2 = idp
jbcIDPv1 = First(
             IDPtoQDP[Apply = CONSTONLY]:RunDefaultStrategyForObligation,
             First(
               Solve(
                 Timer(12000, idpFast)
               ),
               AnyDelay(5000,
                 Solve(idpSlow),
                 Solve(IDPtoQDP[Apply = ALWAYSFILTER]:RunDefaultStrategyForObligation)
               )
             )
           )

jbcComplexity =
  CombineParallel(
    jbcEval,
    jbcComplexityAbstract
  )

jbcComplexityAbstract =
  JBCToTerminationGraph[
    TryNontermProofs=False,
    TrySeparateMethodAnalysis=False
  ];
  jbcITS

jbcITS =
    CombineParallel(
      # Sometimes KoAT proves more precise bounds if we chain less aggressively.
      # As we just chain "straight-line code", keeping leaves of the termination graph results in less aggressive chaining.
      # Hence, we use KoAT with both, jbcEdgesForCES and jbcEdgesForITS.
      # When we chain aggressively, then we also slice, such that we generate a moderately and an aggressively simplified ITS.
      jbcEdgesForCES;
      CombineParallel(
        JBCGraphEdgesToIntTrs; jbcIntTrsChain; jbcIntTrsSimplify; WeightedIntTrsToCES,
        # also try alternative encoding of Div and Mod and filtering of Object-fields once
        JBCGraphEdgesToIntTrs[SimpleDivModEncoding=False]; jbcIntTrsChain; jbcIntTrsSimplify; WeightedIntTrsToKoAT
      ),
      jbcEdgesForITS; JBCGraphEdgesToIntTrs[FilterFieldsOfTypeObject=True, PreciseTreeEncoding=False]; jbcIntTrsChain; jbcIntTrsSlice; jbcIntTrsSimplify; WeightedIntTrsToKoAT
    )

jbcEdgesForITS =
      Maybe(SEGraphDataFlow):
      TerminationGraphToComplexityRuleSet[
        ApplyAnalyses = "aprove.Framework.Bytecode.Processors.ToSCC.UsedFieldsAnalysis",
        KeepLeaves=False
      ]

jbcEdgesForCES =
      TerminationGraphToComplexityRuleSet[
        ApplyAnalyses = "aprove.Framework.Bytecode.Processors.ToSCC.UsedFieldsAnalysis",
        KeepLeaves=True
      ]

jbcIntTrsChain = Maybe(WeightedIntTrsStraightLineCodeCompression)

jbcIntTrsSlice =
    Maybe(WeightedIntTrsUnneededArgumentFilter);
    Maybe(WeightedIntTrsDuplicateArgumentFilter)

jbcIntTrsSimplify =
    Maybe(WeightedIntTrsMoveArithmeticFromLhssToConstraints);
    Maybe(WeightedIntTrsLinearizeLhss);
    Maybe(WeightedIntTrsRemoveUnsupportedOperators);
    Maybe(WeightedIntTrsMoveArithmeticFromConstraintsToRhss);
    Maybe(WeightedIntTrsExprSimplification)

weightedIntTrs = Combine(WeightedIntTrsToKoAT, WeightedIntTrsToLoAT)

jbcMethodSummary = JBCToTerminationGraph[
    TryNontermProofs=False,
    TrySeparateMethodAnalysis=False
  ] ; StartMethodSummary
    ; TerminationGraphToComplexityRulesSetForMethodSummary[ApplyAnalyses = "aprove.Framework.Bytecode.Processors.ToSCC.UsedFieldsAnalysis"]
    ; JBCGraphEdgesToIntTrsForMethodSummary ; jbcIntTrsSimplify ; WeightedIntTrsToKoATLikeBackendForMethodSummary

# =============================================== #
# ===================== CINT ==================== #
# =============================================== #
#cint = cintCleanup : Repeat(cintRedPair : cintCleanup) # : cintDesperate : cintCleanup : Repeat(cintRedPair : cintCleanup)
cint = Combine(CpxIntTrsToLoAT[Timeout=290], CpxIntTrsToKoAT)

cintCleanup
    = Repeat(0,*,
        First(
            CpxIntTrsKnowledge,
            CpxIntTrsLeafRemoval,
            CpxIntTrsRemoveUnreachable,
            CpxIntTrsRhsSimplification,
            Repeat(1,*,CpxIntTrsChainingProcessor),
            CpxIntTrsUnsatisfiableConstraintProcessor
        )
    )

cintRedPair = First(
    CpxIntTrsRedPair[Shape = ShapeConstant],
    CpxIntTrsRedPair[Shape = ShapeConstant, UseSizeBounds = True],
	CpxIntTrsRedPair[Shape = ShapeLinear],
	CpxIntTrsRedPair[Shape = ShapeLinear, UseSizeBounds = True]
)

#cintRedPair = First(
#    CpxIntTrsRedPair[Shape = ShapeLinear],
#    CpxIntTrsRedPair[Shape = ShapeQuadraticNotMixed],
#    CpxIntTrsRedPair[Shape = ShapeQuadraticMixed],
#    CpxIntTrsRedPair[Shape = ShapeCubicNotMixed],
#    CpxIntTrsRedPair[Shape = ShapeCubicMixedQuadratic],
#    CpxIntTrsRedPair[Shape = ShapeCubicMixed]
#)

cintDesperate =
	CpxIntTrsChainingProcessor[MaximalFanOut = 2, AllowHarmful = True]

# =============================================== #
# ====================== T2 ===================== #
# =============================================== #

t2Sys = T2IntSysToIntTRS
       :Maybe(IntTRSCompressor)
       :Maybe(IntTRSUnneededArgumentFilter)
       :Maybe(Timer(15000, AddInterprocInvariants))
       :RunDefaultStrategyForObligation

# =============================================== #
# ==================== IRSwT ==================== #
# =============================================== #

#Clean, then check if this is pure IRS or QDP, go to specific substrategies then.
#Otherwise, start normal reduction loop:
irswt = IRSwTFormatTransformer:irswtMainLoop

irswtMainLoop =
     irswtCleanup;
     First(
           Solve(IRSwTRemoveTerms[NoSuccIfChanged=True]:irs),
           Solve(IRSwTRemoveInts[NoSuccIfChanged=True]:IRSwTToQDP:RunDefaultStrategyForObligation),
           Repeat(1,*,irswtOrders;irswtCleanup),
           Any(
                Solve(IRSwTChaining[Mode=SINGLE_RULE]:irswtMainLoop),
                Fail:Solve(IRSwTToIntTRS:irs)
           )
     ) # First

irswtTest = IRSwTTreeTraces

irswtCleanup = Maybe(IRSwTTerminationDigraph)
               ;Maybe(IntTRSCompressor)
               ;Maybe(IntTRSUnneededArgumentFilter)

irswtOrders =
    First(
         IRSwTTempRemoveTerms[Time=5000, Strategy="irswtIRSRuleRemoval", FilterFreeVariables=False],
         IRSwTTempRemoveInts[Time=5000, Strategy="irswtQDPRuleRemoval", FilterFreeVariables=True],
         IRSwTTrace,
         IRSwTOrder[OrderType=INTERPRETATION]
    ) # First

irswtIRSRuleRemoval = Repeat(1,*,First(irsJointSimple, irsJointComplex))
irswtQDPRuleRemoval = IRSwTToQDP:Repeat(1,*,First(solver1, solver2))

# =============================================== #
# ===================== IRS ===================== #
# =============================================== #

irs =
	irsCleanupCrew:
         Any(IntTRSNonPeriodicNonterm,
                IntTRSPeriodicNonterm,
                irsRedStrategy
            ) # Any

irsCleanupCrew = Maybe(IntTRSTerminationGraphProcessor[UseChaining=False, UseConstraintTransformation=False])
                   ;Maybe(IntTRSCompressor)
                   ;Maybe(IntTRSUnneededArgumentFilter)

irsRedStrategy =
                 Solve(
                   First(
                     Any(
                       Timer(5000, irsJointSimple),
                       Timer(7500, irsJointComplex)
                     );irs,
                     Any(
                       IntTRSTerminationGraphProcessor[UseChaining=True];irs,
                       IntTRSCaseAnalysis[Mode=DEFAULT];irs
                     ) # Any
                   ) # First
                 ) # Solve

irsJointSimple = Any(
                      RankingReductionPairProcessor[GenerateFollowingInequalities=False],
                      IntTRSPolynomialOrderProcessor[Degree=1]
                    )

irsJointComplex = Any(
                       RankingReductionPairProcessor[GenerateFollowingInequalities=True],
                       IntTRSPolynomialOrderProcessor[Degree=2, FactorBinomials=True]
                     )

irsTransitionInvariantStrategy = Maybe(IntTRSTerminationGraphProcessor[UseChaining=False]):RankingProcessor

irsUsingT2 = IRSToT2SysProcessor;T2;T2

jbcGraphSCCMCNP = TerminationSCCToIDPv1:Solve(IDPToMCS[];mcs)

# =============================================== #
# ==================== LLVM  ==================== #
# =============================================== #

llvmMemSafety = Solve(LLVMMemorySafety[Solver=HEURISTICS, Bounded=False, ProveFreeOfMemoryLeaks=False])

llvmFreeOfMemLeaks = Solve(LLVMMemorySafety[Solver=HEURISTICS, Bounded=False, ProveFreeOfMemoryLeaks=True])

llvmTermination = LLVMToSEGraph[Solver=HEURISTICS, UseOptimizations=False, Bounded=False]:
                 Any(
                     Solve(
                         LLVMSEGraphToLasso;
                         LLVMLassoToIntTRS:
                         Any(
                             Solve(irsUsingT2)
                         )
                     ),
                     Solve(
                         LLVMSEGraphToIntTRS:
                         Solve(irsUsingT2)
                     ),
                     Solve(
                         LLVMSEGraphToSCC;
                         First(
                             Solve(
                                 LLVMSCCToIntTRS:
                                 Any(
                                     Solve(irs),
                                     Solve(irsUsingT2)
                                 )
                             ),
                             Solve(
                                 LLVMSCCToIntTRS[UseInvariants=CHANGESANDINSTBOUNDS]:
                                 Any(
                                     Solve(irs),
                                     Solve(irsUsingT2)
                                 )
                             )
                         )
                     ),
                     Solve(LLVMNontermination)
                 )


llvmitrs = ITRSToIDP:RunDefaultStrategyForObligation

# ================================================ #
# ====================== C ======================= #
# ================================================ #

c = Any(
        Solve(CToLLVM:RunDefaultStrategyForObligation),
        Solve(CToIRS:RunDefaultStrategyForObligation)
    )

# ================================================ #
# ==================== PATRS  ==================== #
# ================================================ #

patrs = Maybe(PATRSUnsat):
        Maybe(PATRSReducible):
        PATRSDP:
        Repeat(0, *, PADPReducing):
        Repeat(0, *, patrsScc)

patrsScc = First(
             PADPEDG,
             PADPSubterm,
             patrsOrders,
             PADPFilter,
             PADPPairNarrowing:Maybe(PADPUnsat)
           )

patrsOrders = First(
                patrsPolo1,
                patrsPolo2,
                patrsPolo3,
                patrsPolo4,
                patrsPolo5,
                patrsPolo6
              )

patrsPolo1 = First(
               PADPPolo[Range = 1, NoIntDependence = True],
               PADPPlainPolo[Range = 1, Monotonic = False]
             )

patrsPolo2 = First(
               PADPMonotonicPolo[Range = 1, NoIntDependence = True],
               PADPPlainPolo[Range = 1, Monotonic = True]
             )

patrsPolo3 = First(
               PADPPolo[Range = 1, NoIntDependence = False],
               PADPPlainPolo[Range = 2, Monotonic = False]
             )

patrsPolo4 = First(
               PADPMonotonicPolo[Range = 1, NoIntDependence = False],
               PADPPlainPolo[Range = 2, Monotonic = True]
             )

patrsPolo5 = PADPPolo[Range = 2, NoIntDependence = True]

patrsPolo6 = PADPPolo[Range = 2, NoIntDependence = False]


# ================================================== #
# ==================== CSPATRS  ==================== #
# ================================================== #

cspatrs = Maybe(CSPATRSUnsat):
          Maybe(CSPATRSReducible):
          CSPATRSDP:
          Repeat(0, *, cspatrsScc)

cspatrsScc = First(
               CSPADPEDG,
               CSPADPSubterm,
               cspatrsOrders,
               CSPADPFilter
             )

cspatrsOrders = First(
                  cspatrsPolo1,
                  cspatrsPolo2,
                  cspatrsPolo3,
                  cspatrsPolo4,
                  cspatrsPolo5,
                  cspatrsPolo6
                )

cspatrsPolo1 = First(
                 CSPADPPolo[Range = 1, NoIntDependence = True],
                 CSPADPPlainPolo[Range = 1, Monotonic = False]
               )

cspatrsPolo2 = First(
                 CSPADPMonotonicPolo[Range = 1, NoIntDependence = True],
                 CSPADPPlainPolo[Range = 1, Monotonic = True]
               )

cspatrsPolo3 = First(
                 CSPADPPolo[Range = 1, NoIntDependence = False],
                 CSPADPPlainPolo[Range = 2, Monotonic = False]
               )

cspatrsPolo4 = First(
                 CSPADPMonotonicPolo[Range = 1, NoIntDependence = False],
                 CSPADPPlainPolo[Range = 2, Monotonic = True]
               )

cspatrsPolo5 = CSPADPPolo[Range = 2, NoIntDependence = True]

cspatrsPolo6 = CSPADPPolo[Range = 2, NoIntDependence = False]


# ================================================================ #
# ==================== INDIVIDUAL PROCESSORS  ==================== #
# ================================================================ #

depgraph = QDPDependencyGraph


# ================================================== #
# ==================== UTILITY  ==================== #
# ================================================== #

fail = Fail


# ======================================================== #
# ==================== THEOREM PROVER ==================== #
# ======================================================== #

thm = WallTimer(3000,Solve(thmprover))

thmShort = WallTimer(1200,Solve(thmprover))

thmprover = Repeat(0,*,
              First(
                Solve(
                  LemmaApplication[MinimalHeuristic = 1, Mode = OLD]:
                  thmprover
                ),
                SymbolicEvaluation,
                Solve(
                  ConditionalEvaluation:
                  thmprover
                ),
                Solve(
                  CaseAnalysis:
                  thmprover
                ),
                Solve(
                  HypothesisLifting:
                  thmprover
                ),
                Solve(
                  InverseSubstitution:
                  thmprover
                ),
                INDFMLHeuristic[Techniques = Both, UseCoverSets = True, Merging = True, SkipLAHypothesisHeuristic = False, EvaluateHypothesis = True, LooseRestrictions = False]
              )
            )


# ================================================================= #
# ==================== MONOTONICITY CONSTRAINT ==================== #
# ====================    TRANSITION SYSTEM    ==================== #
# ================================================================= #

mcs = First(MCSMCNP, MCSToITRS:itrs)


# ============================================================ #
# ============================ CIDT ========================== #
# ============================================================ #

cidt = CIdtTypeInference : Maybe(cidtKnowledgeGeneration) : Maybe(CIdtPathCollapse) : cidtCleanup : Maybe(cidtDeleteFalse) : AnyDelay(500, cidtConst, cidtLinear, cidtQuadratic)

cidtConst = Maybe(CIdtPathCollapse[CollapseSSelfLoops = 1]) : cidtDeleteFalse : cidtConst

cidtLinear = CIdtPolyInterpretationSwitch[Shapes = COMPLEXITY_CONSTRUCTORS_LINEAR_SHAPE, ReplaceExisting = TRUE]
          : cidtKnowledgeGeneration : cidtCleanup : cidtSolve

cidtQuadratic = CIdtPolyInterpretationSwitch[Shapes = COMPLEXITY_CONSTRUCTORS_QUADRATIC_SHAPE, ReplaceExisting = TRUE]
          : cidtKnowledgeGeneration : cidtCleanup : cidtSolve

cidtDeleteFalse = CIdtCNDGraph[Strategy = CND_ProveFalseStrategy, GraphStrategy = DELETE_OR_DO_NOT_CHANGE] : cidtCleanup

cidtSolve =  First(Maybe(CIdtNodeSplit) : cidtIntRedPairSolve, CIdtPathCollapse[CollapseSSelfLoops = 1] : Maybe(CIdtNodeSplit) : cidtIntRedPairSolve)

cidtCleanup =  Maybe(CIdtLeafRemoval) : Maybe(CIdtUsableRules)

cidtKnowledgePropagation = Maybe(CIdtKnowledgePropagation)

cidtKnowledgeGeneration = Maybe(CIdtCNDGraph[Strategy = CND_KNOWLEDGE_GENERATION])

cidtIntRedPairSolve = CIdtPolyIntRedPair[Solver = SAT_SOLVER, All_strict_and_bounded = FALSE, RANGE_MIN = -3, RANGE_MAX = 3] : cidtKnowledgePropagation : cidtCleanup : cidtIntRedPairSolve