Left Termination proof of ../tpdb/LP/talp/apt/dc

MAYBE Left Termination proof of ../tpdb/LP/talp/apt/dc_schema.pl
Left Termination of the query pattern dcsolve_in_2(g, a) w.r.t. the given Prolog program could not be shown:

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

Clauses:

dcsolve(X, Y) :- ','(base(X), conquer(X, Y)).
dcsolve(X, Y) :- ','(divide(X, X0, X1, X2), ','(dcsolve(X1, Y1), ','(dcsolve(X2, Y2), merge(X0, Y1, Y2, Y)))).

Queries:

dcsolve(g,a).

Added facts for all undefined predicates.

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

Clauses:

dcsolve(X, Y) :- ','(base(X), conquer(X, Y)).
dcsolve(X, Y) :- ','(divide(X, X0, X1, X2), ','(dcsolve(X1, Y1), ','(dcsolve(X2, Y2), merge(X0, Y1, Y2, Y)))).
base(X0).
conquer(X0, X1).
divide(X0, X1, X2, X3).
merge(X0, X1, X2, X3).

Queries:

dcsolve(g,a).

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
dcsolve_in: (b,f) (f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

      ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

DCSOLVE_IN_GA(X, Y) → U1_GA(X, Y, base_in_g(X))
DCSOLVE_IN_GA(X, Y) → BASE_IN_G(X)
U1_GA(X, Y, base_out_g(X)) → U2_GA(X, Y, conquer_in_ga(X, Y))
U1_GA(X, Y, base_out_g(X)) → CONQUER_IN_GA(X, Y)
DCSOLVE_IN_GA(X, Y) → U3_GA(X, Y, divide_in_gaaa(X, X0, X1, X2))
DCSOLVE_IN_GA(X, Y) → DIVIDE_IN_GAAA(X, X0, X1, X2)
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_GA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
DCSOLVE_IN_AA(X, Y) → U1_AA(X, Y, base_in_a(X))
DCSOLVE_IN_AA(X, Y) → BASE_IN_A(X)
U1_AA(X, Y, base_out_a(X)) → U2_AA(X, Y, conquer_in_aa(X, Y))
U1_AA(X, Y, base_out_a(X)) → CONQUER_IN_AA(X, Y)
DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
DCSOLVE_IN_AA(X, Y) → DIVIDE_IN_AAAA(X, X0, X1, X2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_AA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_AA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_GA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_GA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)

The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
dcsolve_in_ga(x1, x2) = dcsolve_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
base_in_g(x1) = base_in_g(x1)
base_out_g(x1) = base_out_g
U2_ga(x1, x2, x3) = U2_ga(x3)
conquer_in_ga(x1, x2) = conquer_in_ga(x1)
conquer_out_ga(x1, x2) = conquer_out_ga
dcsolve_out_ga(x1, x2) = dcsolve_out_ga
U3_ga(x1, x2, x3) = U3_ga(x3)
divide_in_gaaa(x1, x2, x3, x4) = divide_in_gaaa(x1)
divide_out_gaaa(x1, x2, x3, x4) = divide_out_gaaa
U4_ga(x1, x2, x3, x4, x5, x6) = U4_ga(x6)
dcsolve_in_aa(x1, x2) = dcsolve_in_aa
U1_aa(x1, x2, x3) = U1_aa(x3)
base_in_a(x1) = base_in_a
base_out_a(x1) = base_out_a
U2_aa(x1, x2, x3) = U2_aa(x3)
conquer_in_aa(x1, x2) = conquer_in_aa
conquer_out_aa(x1, x2) = conquer_out_aa
dcsolve_out_aa(x1, x2) = dcsolve_out_aa
U3_aa(x1, x2, x3) = U3_aa(x3)
divide_in_aaaa(x1, x2, x3, x4) = divide_in_aaaa
divide_out_aaaa(x1, x2, x3, x4) = divide_out_aaaa
U4_aa(x1, x2, x3, x4, x5, x6) = U4_aa(x6)
U5_aa(x1, x2, x3, x4, x5) = U5_aa(x5)
U6_aa(x1, x2, x3) = U6_aa(x3)
merge_in_aaaa(x1, x2, x3, x4) = merge_in_aaaa
merge_out_aaaa(x1, x2, x3, x4) = merge_out_aaaa
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x5)
U6_ga(x1, x2, x3) = U6_ga(x3)
BASE_IN_G(x1) = BASE_IN_G(x1)
DIVIDE_IN_AAAA(x1, x2, x3, x4) = DIVIDE_IN_AAAA
U3_AA(x1, x2, x3) = U3_AA(x3)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x5)
U1_AA(x1, x2, x3) = U1_AA(x3)
U4_AA(x1, x2, x3, x4, x5, x6) = U4_AA(x6)
CONQUER_IN_AA(x1, x2) = CONQUER_IN_AA
BASE_IN_A(x1) = BASE_IN_A
MERGE_IN_AAAA(x1, x2, x3, x4) = MERGE_IN_AAAA
U6_GA(x1, x2, x3) = U6_GA(x3)
DIVIDE_IN_GAAA(x1, x2, x3, x4) = DIVIDE_IN_GAAA(x1)
U6_AA(x1, x2, x3) = U6_AA(x3)
U5_AA(x1, x2, x3, x4, x5) = U5_AA(x5)
DCSOLVE_IN_GA(x1, x2) = DCSOLVE_IN_GA(x1)
CONQUER_IN_GA(x1, x2) = CONQUER_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x3)
U2_AA(x1, x2, x3) = U2_AA(x3)
U4_GA(x1, x2, x3, x4, x5, x6) = U4_GA(x6)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U2_GA(x1, x2, x3) = U2_GA(x3)
DCSOLVE_IN_AA(x1, x2) = DCSOLVE_IN_AA

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

      ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_GA(X, Y) → U1_GA(X, Y, base_in_g(X))
DCSOLVE_IN_GA(X, Y) → BASE_IN_G(X)
U1_GA(X, Y, base_out_g(X)) → U2_GA(X, Y, conquer_in_ga(X, Y))
U1_GA(X, Y, base_out_g(X)) → CONQUER_IN_GA(X, Y)
DCSOLVE_IN_GA(X, Y) → U3_GA(X, Y, divide_in_gaaa(X, X0, X1, X2))
DCSOLVE_IN_GA(X, Y) → DIVIDE_IN_GAAA(X, X0, X1, X2)
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_GA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
DCSOLVE_IN_AA(X, Y) → U1_AA(X, Y, base_in_a(X))
DCSOLVE_IN_AA(X, Y) → BASE_IN_A(X)
U1_AA(X, Y, base_out_a(X)) → U2_AA(X, Y, conquer_in_aa(X, Y))
U1_AA(X, Y, base_out_a(X)) → CONQUER_IN_AA(X, Y)
DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
DCSOLVE_IN_AA(X, Y) → DIVIDE_IN_AAAA(X, X0, X1, X2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_AA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_AA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_GA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_GA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)

The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

      ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))

The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

      ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))

The TRS R consists of the following rules:

divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
base_in_a(X0) → base_out_a(X0)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)

The argument filtering Pi contains the following mapping:
dcsolve_in_aa(x1, x2) = dcsolve_in_aa
U1_aa(x1, x2, x3) = U1_aa(x3)
base_in_a(x1) = base_in_a
base_out_a(x1) = base_out_a
U2_aa(x1, x2, x3) = U2_aa(x3)
conquer_in_aa(x1, x2) = conquer_in_aa
conquer_out_aa(x1, x2) = conquer_out_aa
dcsolve_out_aa(x1, x2) = dcsolve_out_aa
U3_aa(x1, x2, x3) = U3_aa(x3)
divide_in_aaaa(x1, x2, x3, x4) = divide_in_aaaa
divide_out_aaaa(x1, x2, x3, x4) = divide_out_aaaa
U4_aa(x1, x2, x3, x4, x5, x6) = U4_aa(x6)
U5_aa(x1, x2, x3, x4, x5) = U5_aa(x5)
U6_aa(x1, x2, x3) = U6_aa(x3)
merge_in_aaaa(x1, x2, x3, x4) = merge_in_aaaa
merge_out_aaaa(x1, x2, x3, x4) = merge_out_aaaa
U3_AA(x1, x2, x3) = U3_AA(x3)
U4_AA(x1, x2, x3, x4, x5, x6) = U4_AA(x6)
DCSOLVE_IN_AA(x1, x2) = DCSOLVE_IN_AA

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem [30] into ordinary QDP problem [15] by application of Pi.

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA → U3_AA(divide_in_aaaa)
U3_AA(divide_out_aaaa) → U4_AA(dcsolve_in_aa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule DCSOLVE_IN_AA → U3_AA(divide_in_aaaa) at position [0] we obtained the following new rules:

DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U3_AA(divide_out_aaaa) → U4_AA(dcsolve_in_aa)
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U3_AA(divide_out_aaaa) → U4_AA(dcsolve_in_aa) at position [0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_in_a))
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_in_a))
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa))
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_in_a)) at position [0,0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa))
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa)) at position [0,0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a))
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a)) at position [0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_in_aa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_in_aa))
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_in_aa)) at position [0,0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_out_aa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_out_aa))
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_out_aa)) at position [0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(dcsolve_out_aa)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ NonTerminationProof

      ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(dcsolve_out_aa)
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(dcsolve_out_aa)
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

s = U3_AA(divide_out_aaaa) evaluates to t =U3_AA(divide_out_aaaa)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]

Rewriting sequence

U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
with rule U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA at position [] and matcher [ ]

DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
with rule DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.

We use the technique of [30]. With regard to the inferred argument filtering the predicates were used in the following modes:
dcsolve_in: (b,f) (f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

DCSOLVE_IN_GA(X, Y) → U1_GA(X, Y, base_in_g(X))
DCSOLVE_IN_GA(X, Y) → BASE_IN_G(X)
U1_GA(X, Y, base_out_g(X)) → U2_GA(X, Y, conquer_in_ga(X, Y))
U1_GA(X, Y, base_out_g(X)) → CONQUER_IN_GA(X, Y)
DCSOLVE_IN_GA(X, Y) → U3_GA(X, Y, divide_in_gaaa(X, X0, X1, X2))
DCSOLVE_IN_GA(X, Y) → DIVIDE_IN_GAAA(X, X0, X1, X2)
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_GA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
DCSOLVE_IN_AA(X, Y) → U1_AA(X, Y, base_in_a(X))
DCSOLVE_IN_AA(X, Y) → BASE_IN_A(X)
U1_AA(X, Y, base_out_a(X)) → U2_AA(X, Y, conquer_in_aa(X, Y))
U1_AA(X, Y, base_out_a(X)) → CONQUER_IN_AA(X, Y)
DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
DCSOLVE_IN_AA(X, Y) → DIVIDE_IN_AAAA(X, X0, X1, X2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_AA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_AA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_GA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_GA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)

The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
dcsolve_in_ga(x1, x2) = dcsolve_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
base_in_g(x1) = base_in_g(x1)
base_out_g(x1) = base_out_g(x1)
U2_ga(x1, x2, x3) = U2_ga(x1, x3)
conquer_in_ga(x1, x2) = conquer_in_ga(x1)
conquer_out_ga(x1, x2) = conquer_out_ga(x1)
dcsolve_out_ga(x1, x2) = dcsolve_out_ga(x1)
U3_ga(x1, x2, x3) = U3_ga(x1, x3)
divide_in_gaaa(x1, x2, x3, x4) = divide_in_gaaa(x1)
divide_out_gaaa(x1, x2, x3, x4) = divide_out_gaaa(x1)
U4_ga(x1, x2, x3, x4, x5, x6) = U4_ga(x1, x6)
dcsolve_in_aa(x1, x2) = dcsolve_in_aa
U1_aa(x1, x2, x3) = U1_aa(x3)
base_in_a(x1) = base_in_a
base_out_a(x1) = base_out_a
U2_aa(x1, x2, x3) = U2_aa(x3)
conquer_in_aa(x1, x2) = conquer_in_aa
conquer_out_aa(x1, x2) = conquer_out_aa
dcsolve_out_aa(x1, x2) = dcsolve_out_aa
U3_aa(x1, x2, x3) = U3_aa(x3)
divide_in_aaaa(x1, x2, x3, x4) = divide_in_aaaa
divide_out_aaaa(x1, x2, x3, x4) = divide_out_aaaa
U4_aa(x1, x2, x3, x4, x5, x6) = U4_aa(x6)
U5_aa(x1, x2, x3, x4, x5) = U5_aa(x5)
U6_aa(x1, x2, x3) = U6_aa(x3)
merge_in_aaaa(x1, x2, x3, x4) = merge_in_aaaa
merge_out_aaaa(x1, x2, x3, x4) = merge_out_aaaa
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x5)
U6_ga(x1, x2, x3) = U6_ga(x1, x3)
BASE_IN_G(x1) = BASE_IN_G(x1)
DIVIDE_IN_AAAA(x1, x2, x3, x4) = DIVIDE_IN_AAAA
U3_AA(x1, x2, x3) = U3_AA(x3)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x1, x5)
U1_AA(x1, x2, x3) = U1_AA(x3)
U4_AA(x1, x2, x3, x4, x5, x6) = U4_AA(x6)
CONQUER_IN_AA(x1, x2) = CONQUER_IN_AA
BASE_IN_A(x1) = BASE_IN_A
MERGE_IN_AAAA(x1, x2, x3, x4) = MERGE_IN_AAAA
U6_GA(x1, x2, x3) = U6_GA(x1, x3)
DIVIDE_IN_GAAA(x1, x2, x3, x4) = DIVIDE_IN_GAAA(x1)
U6_AA(x1, x2, x3) = U6_AA(x3)
U5_AA(x1, x2, x3, x4, x5) = U5_AA(x5)
DCSOLVE_IN_GA(x1, x2) = DCSOLVE_IN_GA(x1)
CONQUER_IN_GA(x1, x2) = CONQUER_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U2_AA(x1, x2, x3) = U2_AA(x3)
U4_GA(x1, x2, x3, x4, x5, x6) = U4_GA(x1, x6)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
DCSOLVE_IN_AA(x1, x2) = DCSOLVE_IN_AA

We have to consider all (P,R,Pi)-chains

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_GA(X, Y) → U1_GA(X, Y, base_in_g(X))
DCSOLVE_IN_GA(X, Y) → BASE_IN_G(X)
U1_GA(X, Y, base_out_g(X)) → U2_GA(X, Y, conquer_in_ga(X, Y))
U1_GA(X, Y, base_out_g(X)) → CONQUER_IN_GA(X, Y)
DCSOLVE_IN_GA(X, Y) → U3_GA(X, Y, divide_in_gaaa(X, X0, X1, X2))
DCSOLVE_IN_GA(X, Y) → DIVIDE_IN_GAAA(X, X0, X1, X2)
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_GA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_GA(X, Y, divide_out_gaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
DCSOLVE_IN_AA(X, Y) → U1_AA(X, Y, base_in_a(X))
DCSOLVE_IN_AA(X, Y) → BASE_IN_A(X)
U1_AA(X, Y, base_out_a(X)) → U2_AA(X, Y, conquer_in_aa(X, Y))
U1_AA(X, Y, base_out_a(X)) → CONQUER_IN_AA(X, Y)
DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
DCSOLVE_IN_AA(X, Y) → DIVIDE_IN_AAAA(X, X0, X1, X2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_AA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_AA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_AA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_GA(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U4_GA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_GA(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U5_GA(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → MERGE_IN_AAAA(X0, Y1, Y2, Y)

The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
dcsolve_in_ga(x1, x2) = dcsolve_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
base_in_g(x1) = base_in_g(x1)
base_out_g(x1) = base_out_g(x1)
U2_ga(x1, x2, x3) = U2_ga(x1, x3)
conquer_in_ga(x1, x2) = conquer_in_ga(x1)
conquer_out_ga(x1, x2) = conquer_out_ga(x1)
dcsolve_out_ga(x1, x2) = dcsolve_out_ga(x1)
U3_ga(x1, x2, x3) = U3_ga(x1, x3)
divide_in_gaaa(x1, x2, x3, x4) = divide_in_gaaa(x1)
divide_out_gaaa(x1, x2, x3, x4) = divide_out_gaaa(x1)
U4_ga(x1, x2, x3, x4, x5, x6) = U4_ga(x1, x6)
dcsolve_in_aa(x1, x2) = dcsolve_in_aa
U1_aa(x1, x2, x3) = U1_aa(x3)
base_in_a(x1) = base_in_a
base_out_a(x1) = base_out_a
U2_aa(x1, x2, x3) = U2_aa(x3)
conquer_in_aa(x1, x2) = conquer_in_aa
conquer_out_aa(x1, x2) = conquer_out_aa
dcsolve_out_aa(x1, x2) = dcsolve_out_aa
U3_aa(x1, x2, x3) = U3_aa(x3)
divide_in_aaaa(x1, x2, x3, x4) = divide_in_aaaa
divide_out_aaaa(x1, x2, x3, x4) = divide_out_aaaa
U4_aa(x1, x2, x3, x4, x5, x6) = U4_aa(x6)
U5_aa(x1, x2, x3, x4, x5) = U5_aa(x5)
U6_aa(x1, x2, x3) = U6_aa(x3)
merge_in_aaaa(x1, x2, x3, x4) = merge_in_aaaa
merge_out_aaaa(x1, x2, x3, x4) = merge_out_aaaa
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x5)
U6_ga(x1, x2, x3) = U6_ga(x1, x3)
BASE_IN_G(x1) = BASE_IN_G(x1)
DIVIDE_IN_AAAA(x1, x2, x3, x4) = DIVIDE_IN_AAAA
U3_AA(x1, x2, x3) = U3_AA(x3)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x1, x5)
U1_AA(x1, x2, x3) = U1_AA(x3)
U4_AA(x1, x2, x3, x4, x5, x6) = U4_AA(x6)
CONQUER_IN_AA(x1, x2) = CONQUER_IN_AA
BASE_IN_A(x1) = BASE_IN_A
MERGE_IN_AAAA(x1, x2, x3, x4) = MERGE_IN_AAAA
U6_GA(x1, x2, x3) = U6_GA(x1, x3)
DIVIDE_IN_GAAA(x1, x2, x3, x4) = DIVIDE_IN_GAAA(x1)
U6_AA(x1, x2, x3) = U6_AA(x3)
U5_AA(x1, x2, x3, x4, x5) = U5_AA(x5)
DCSOLVE_IN_GA(x1, x2) = DCSOLVE_IN_GA(x1)
CONQUER_IN_GA(x1, x2) = CONQUER_IN_GA(x1)
U3_GA(x1, x2, x3) = U3_GA(x1, x3)
U2_AA(x1, x2, x3) = U2_AA(x3)
U4_GA(x1, x2, x3, x4, x5, x6) = U4_GA(x1, x6)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
U2_GA(x1, x2, x3) = U2_GA(x1, x3)
DCSOLVE_IN_AA(x1, x2) = DCSOLVE_IN_AA

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 1 SCC with 20 less nodes.

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))

The TRS R consists of the following rules:

dcsolve_in_ga(X, Y) → U1_ga(X, Y, base_in_g(X))
base_in_g(X0) → base_out_g(X0)
U1_ga(X, Y, base_out_g(X)) → U2_ga(X, Y, conquer_in_ga(X, Y))
conquer_in_ga(X0, X1) → conquer_out_ga(X0, X1)
U2_ga(X, Y, conquer_out_ga(X, Y)) → dcsolve_out_ga(X, Y)
dcsolve_in_ga(X, Y) → U3_ga(X, Y, divide_in_gaaa(X, X0, X1, X2))
divide_in_gaaa(X0, X1, X2, X3) → divide_out_gaaa(X0, X1, X2, X3)
U3_ga(X, Y, divide_out_gaaa(X, X0, X1, X2)) → U4_ga(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
base_in_a(X0) → base_out_a(X0)
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
U4_ga(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_ga(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
U5_ga(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_ga(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_ga(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_ga(X, Y)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA(X, Y) → U3_AA(X, Y, divide_in_aaaa(X, X0, X1, X2))
U4_AA(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → DCSOLVE_IN_AA(X2, Y2)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → DCSOLVE_IN_AA(X1, Y1)
U3_AA(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_AA(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))

The TRS R consists of the following rules:

divide_in_aaaa(X0, X1, X2, X3) → divide_out_aaaa(X0, X1, X2, X3)
dcsolve_in_aa(X, Y) → U1_aa(X, Y, base_in_a(X))
dcsolve_in_aa(X, Y) → U3_aa(X, Y, divide_in_aaaa(X, X0, X1, X2))
U1_aa(X, Y, base_out_a(X)) → U2_aa(X, Y, conquer_in_aa(X, Y))
U3_aa(X, Y, divide_out_aaaa(X, X0, X1, X2)) → U4_aa(X, Y, X0, X1, X2, dcsolve_in_aa(X1, Y1))
base_in_a(X0) → base_out_a(X0)
U2_aa(X, Y, conquer_out_aa(X, Y)) → dcsolve_out_aa(X, Y)
U4_aa(X, Y, X0, X1, X2, dcsolve_out_aa(X1, Y1)) → U5_aa(X, Y, X0, Y1, dcsolve_in_aa(X2, Y2))
conquer_in_aa(X0, X1) → conquer_out_aa(X0, X1)
U5_aa(X, Y, X0, Y1, dcsolve_out_aa(X2, Y2)) → U6_aa(X, Y, merge_in_aaaa(X0, Y1, Y2, Y))
U6_aa(X, Y, merge_out_aaaa(X0, Y1, Y2, Y)) → dcsolve_out_aa(X, Y)
merge_in_aaaa(X0, X1, X2, X3) → merge_out_aaaa(X0, X1, X2, X3)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA → U3_AA(divide_in_aaaa)
U3_AA(divide_out_aaaa) → U4_AA(dcsolve_in_aa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule DCSOLVE_IN_AA → U3_AA(divide_in_aaaa) at position [0] we obtained the following new rules:

DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

Q DP problem:
The TRS P consists of the following rules:

DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U3_AA(divide_out_aaaa) → U4_AA(dcsolve_in_aa)
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By narrowing [15] the rule U3_AA(divide_out_aaaa) → U4_AA(dcsolve_in_aa) at position [0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_in_a))
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_in_a))
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa))
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_in_a)) at position [0,0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa))
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_in_aaaa)) at position [0,0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a))
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U1_aa(base_out_a)) at position [0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_in_aa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_in_aa))
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_in_aa)) at position [0,0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_out_aa))

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_out_aa))
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

We have to consider all (P,Q,R)-chains.
By rewriting [15] the rule U3_AA(divide_out_aaaa) → U4_AA(U2_aa(conquer_out_aa)) at position [0] we obtained the following new rules:

U3_AA(divide_out_aaaa) → U4_AA(dcsolve_out_aa)

↳ Prolog

  ↳ UndefinedPredicateHandlerProof

    ↳ Prolog

      ↳ PrologToPiTRSProof

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ Rewriting

                            ↳ QDP

                              ↳ Narrowing

                                ↳ QDP

                                  ↳ Rewriting

                                    ↳ QDP

                                      ↳ Rewriting

                                        ↳ QDP

                                          ↳ Rewriting

                                            ↳ QDP

                                              ↳ Rewriting

                                                ↳ QDP

                                                  ↳ Rewriting

                                                    ↳ QDP

                                                      ↳ NonTerminationProof

Q DP problem:
The TRS P consists of the following rules:

U3_AA(divide_out_aaaa) → U4_AA(dcsolve_out_aa)
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

The set Q consists of the following terms:

divide_in_aaaa
dcsolve_in_aa
U1_aa(x0)
U3_aa(x0)
base_in_a
U2_aa(x0)
U4_aa(x0)
conquer_in_aa
U5_aa(x0)
U6_aa(x0)
merge_in_aaaa

U3_AA(divide_out_aaaa) → U4_AA(dcsolve_out_aa)
U3_AA(divide_out_aaaa) → U4_AA(U3_aa(divide_out_aaaa))
DCSOLVE_IN_AA → U3_AA(divide_out_aaaa)
U3_AA(divide_out_aaaa) → DCSOLVE_IN_AA
U4_AA(dcsolve_out_aa) → DCSOLVE_IN_AA

The TRS R consists of the following rules:

divide_in_aaaa → divide_out_aaaa
dcsolve_in_aa → U1_aa(base_in_a)
dcsolve_in_aa → U3_aa(divide_in_aaaa)
U1_aa(base_out_a) → U2_aa(conquer_in_aa)
U3_aa(divide_out_aaaa) → U4_aa(dcsolve_in_aa)
base_in_a → base_out_a
U2_aa(conquer_out_aa) → dcsolve_out_aa
U4_aa(dcsolve_out_aa) → U5_aa(dcsolve_in_aa)
conquer_in_aa → conquer_out_aa
U5_aa(dcsolve_out_aa) → U6_aa(merge_in_aaaa)
U6_aa(merge_out_aaaa) → dcsolve_out_aa
merge_in_aaaa → merge_out_aaaa

s = U3_AA(divide_out_aaaa) evaluates to t =U3_AA(divide_out_aaaa)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [ ]