Left Termination proof of ../tpdb/LP/terminweb/old-terminweb/queens.pl

YES Left Termination proof of ../tpdb/LP/terminweb/old-terminweb/queens.pl
Left Termination of the query pattern queens_in_2(g, a) w.r.t. the given Prolog program could successfully be proven:

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

Clauses:

queens(X, Y) :- ','(perm(X, Y), safe(Y)).
perm([], []).
perm(.(X, Y), .(V, Res)) :- ','(delete(V, .(X, Y), Rest), perm(Rest, Res)).
delete(X, .(X, Y), Y).
delete(X, .(F, T), .(F, R)) :- delete(X, T, R).
safe([]).
safe(.(X, Y)) :- ','(noattack(X, Y, succ(zero)), safe(Y)).
noattack(X, [], N).
noattack(X, .(F, T), N) :- ','(=\=(X, F), ','(=\=(X, +(F, N)), ','(=\=(F, +(X, N)), ','(','(isPlus(N, succ(zero), U), =(N1, U)), noattack(X, T, N1))))).
nonequal(X, Y) :- ','(=(X, Y), ','(!, fail)).
nonequal(X, Y) :- true.
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
fail :- fail(b).
fail(a).
true.
=(X, X).

Queries:

queens(g,a).

Eliminated all cuts by simply ignoring them.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

Clauses:

queens(X, Y) :- ','(perm(X, Y), safe(Y)).
perm([], []).
perm(.(X, Y), .(V, Res)) :- ','(delete(V, .(X, Y), Rest), perm(Rest, Res)).
delete(X, .(X, Y), Y).
delete(X, .(F, T), .(F, R)) :- delete(X, T, R).
safe([]).
safe(.(X, Y)) :- ','(noattack(X, Y, succ(zero)), safe(Y)).
noattack(X, [], N).
noattack(X, .(F, T), N) :- ','(=\=(X, F), ','(=\=(X, +(F, N)), ','(=\=(F, +(X, N)), ','(','(isPlus(N, succ(zero), U), =(N1, U)), noattack(X, T, N1))))).
nonequal(X, Y) :- ','(=(X, Y), fail).
nonequal(X, Y) :- true.
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
fail :- fail(b).
fail(a).
true.
=(X, X).

Queries:

queens(g,a).

Added facts for all undefined predicates.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

Clauses:

queens(X, Y) :- ','(perm(X, Y), safe(Y)).
perm([], []).
perm(.(X, Y), .(V, Res)) :- ','(delete(V, .(X, Y), Rest), perm(Rest, Res)).
delete(X, .(X, Y), Y).
delete(X, .(F, T), .(F, R)) :- delete(X, T, R).
safe([]).
safe(.(X, Y)) :- ','(noattack(X, Y, succ(zero)), safe(Y)).
noattack(X, [], N).
noattack(X, .(F, T), N) :- ','(=\=(X, F), ','(=\=(X, +(F, N)), ','(=\=(F, +(X, N)), ','(isPlus(N, succ(zero), U), ','(=(N1, U), noattack(X, T, N1)))))).
nonequal(X, Y) :- ','(=(X, Y), fail).
nonequal(X, Y) :- true.
isPlus(zero, X, X).
isPlus(succ(X), zero, succ(X)).
isPlus(succ(X), succ(Y), succ(succ(Z))) :- isPlus(X, Y, Z).
isPlus(succ(X), pred(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), zero, pred(X)).
isPlus(pred(X), succ(Y), Z) :- isPlus(X, Y, Z).
isPlus(pred(X), pred(Y), pred(pred(Z))) :- isPlus(X, Y, Z).
isMinus(X, zero, X).
isMinus(zero, succ(Y), pred(Z)) :- isMinus(zero, Y, Z).
isMinus(zero, pred(Y), succ(Z)) :- isMinus(zero, Y, Z).
isMinus(succ(X), succ(Y), Z) :- isMinus(X, Y, Z).
isMinus(succ(X), pred(Y), succ(succ(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), succ(Y), pred(pred(Z))) :- isMinus(X, Y, Z).
isMinus(pred(X), pred(Y), Z) :- isMinus(X, Y, Z).
isTimes(X, zero, zero).
isTimes(zero, succ(Y), zero).
isTimes(zero, pred(Y), zero).
isTimes(succ(X), succ(Y), Z) :- ','(isTimes(succ(X), Y, A), isPlus(A, succ(X), Z)).
isTimes(succ(X), pred(Y), Z) :- ','(isTimes(succ(X), Y, A), isMinus(A, succ(X), Z)).
isTimes(pred(X), succ(Y), Z) :- ','(isTimes(pred(X), Y, A), isPlus(A, pred(X), Z)).
isTimes(pred(X), pred(Y), Z) :- ','(isTimes(pred(X), Y, A), isMinus(A, pred(X), Z)).
isDiv(zero, succ(Y), zero).
isDiv(zero, pred(Y), zero).
isDiv(succ(X), succ(Y), zero) :- isMinus(succ(X), succ(Y), pred(Z)).
isDiv(succ(X), succ(Y), succ(Z)) :- ','(isMinus(succ(X), succ(Y), A), isDiv(A, succ(Y), Z)).
isDiv(succ(X), pred(Y), Z) :- ','(isMinus(zero, pred(Y), A), ','(isDiv(succ(X), A, B), isMinus(zero, B, Z))).
isDiv(pred(X), pred(Y), zero) :- isMinus(pred(X), pred(Y), succ(Z)).
isDiv(pred(X), pred(Y), succ(Z)) :- ','(isMinus(pred(X), pred(Y), A), isDiv(A, pred(Y), Z)).
isDiv(pred(X), succ(Y), Z) :- ','(isMinus(zero, pred(X), A), ','(isDiv(A, succ(Y), B), isMinus(zero, B, Z))).
isModulo(X, Y, Z) :- ','(isDiv(X, Y, A), ','(isTimes(A, Y, B), isMinus(X, B, Z))).
fail :- fail(b).
fail(a).
true.
=(X, X).
=\=(X0, X1).

Queries:

queens(g,a).

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

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

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

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

QUEENS_IN_GA(X, Y) → U1_GA(X, Y, perm_in_ga(X, Y))
QUEENS_IN_GA(X, Y) → PERM_IN_GA(X, Y)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
PERM_IN_GA(.(X, Y), .(V, Res)) → DELETE_IN_AGA(V, .(X, Y), Rest)
DELETE_IN_AGA(X, .(F, T), .(F, R)) → U5_AGA(X, F, T, R, delete_in_aga(X, T, R))
DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_GA(X, Y, V, Res, perm_in_ga(Rest, Res))
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
U1_GA(X, Y, perm_out_ga(X, Y)) → U2_GA(X, Y, safe_in_g(Y))
U1_GA(X, Y, perm_out_ga(X, Y)) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, succ(zero)))
SAFE_IN_G(.(X, Y)) → NOATTACK_IN_GGG(X, Y, succ(zero))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, =\=_in_gg(X, F))
NOATTACK_IN_GGG(X, .(F, T), N) → =\=_IN_GG(X, F)
U8_GGG(X, F, T, N, =\=_out_gg(X, F)) → U9_GGG(X, F, T, N, =\=_in_gg(X, +(F, N)))
U8_GGG(X, F, T, N, =\=_out_gg(X, F)) → =\=_IN_GG(X, +(F, N))
U9_GGG(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_GGG(X, F, T, N, =\=_in_gg(F, +(X, N)))
U9_GGG(X, F, T, N, =\=_out_gg(X, +(F, N))) → =\=_IN_GG(F, +(X, N))
U10_GGG(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_GGG(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
U10_GGG(X, F, T, N, =\=_out_gg(F, +(X, N))) → ISPLUS_IN_GGA(N, succ(zero), U)
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → U17_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → U18_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → U19_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → U20_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)
U11_GGG(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_GGG(X, F, T, N, =_in_ag(N1, U))
U11_GGG(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → =_IN_AG(N1, U)
U12_GGG(X, F, T, N, =_out_ag(N1, U)) → U13_GGG(X, F, T, N, noattack_in_ggg(X, T, N1))
U12_GGG(X, F, T, N, =_out_ag(N1, U)) → NOATTACK_IN_GGG(X, T, N1)
U6_G(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_G(X, Y, safe_in_g(Y))
U6_G(X, Y, noattack_out_ggg(X, Y, succ(zero))) → SAFE_IN_G(Y)

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
queens_in_ga(x1, x2) = queens_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x3)
perm_in_ga(x1, x2) = perm_in_ga(x1)
[] = []
perm_out_ga(x1, x2) = perm_out_ga(x2)
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x5)
delete_in_aga(x1, x2, x3) = delete_in_aga(x2)
delete_out_aga(x1, x2, x3) = delete_out_aga(x1, x3)
U5_aga(x1, x2, x3, x4, x5) = U5_aga(x2, x5)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x3, x5)
U2_ga(x1, x2, x3) = U2_ga(x2, x3)
safe_in_g(x1) = safe_in_g(x1)
safe_out_g(x1) = safe_out_g
U6_g(x1, x2, x3) = U6_g(x2, x3)
noattack_in_ggg(x1, x2, x3) = noattack_in_ggg(x1, x2, x3)
noattack_out_ggg(x1, x2, x3) = noattack_out_ggg
U8_ggg(x1, x2, x3, x4, x5) = U8_ggg(x1, x2, x3, x4, x5)
=\=_in_gg(x1, x2) = =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2) = =\=_out_gg
U9_ggg(x1, x2, x3, x4, x5) = U9_ggg(x1, x2, x3, x4, x5)
+(x1, x2) = +(x1, x2)
U10_ggg(x1, x2, x3, x4, x5) = U10_ggg(x1, x3, x4, x5)
U11_ggg(x1, x2, x3, x4, x5) = U11_ggg(x1, x3, x5)
isPlus_in_gga(x1, x2, x3) = isPlus_in_gga(x1, x2)
zero = zero
isPlus_out_gga(x1, x2, x3) = isPlus_out_gga(x3)
succ(x1) = succ(x1)
U17_gga(x1, x2, x3, x4) = U17_gga(x4)
pred(x1) = pred(x1)
U18_gga(x1, x2, x3, x4) = U18_gga(x4)
U19_gga(x1, x2, x3, x4) = U19_gga(x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x4)
U12_ggg(x1, x2, x3, x4, x5) = U12_ggg(x1, x3, x5)
=_in_ag(x1, x2) = =_in_ag(x2)
=_out_ag(x1, x2) = =_out_ag(x1)
U13_ggg(x1, x2, x3, x4, x5) = U13_ggg(x5)
U7_g(x1, x2, x3) = U7_g(x3)
queens_out_ga(x1, x2) = queens_out_ga(x2)
SAFE_IN_G(x1) = SAFE_IN_G(x1)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x3, x5)
U12_GGG(x1, x2, x3, x4, x5) = U12_GGG(x1, x3, x5)
U7_G(x1, x2, x3) = U7_G(x3)
U10_GGG(x1, x2, x3, x4, x5) = U10_GGG(x1, x3, x4, x5)
QUEENS_IN_GA(x1, x2) = QUEENS_IN_GA(x1)
U17_GGA(x1, x2, x3, x4) = U17_GGA(x4)
DELETE_IN_AGA(x1, x2, x3) = DELETE_IN_AGA(x2)
=_IN_AG(x1, x2) = =_IN_AG(x2)
NOATTACK_IN_GGG(x1, x2, x3) = NOATTACK_IN_GGG(x1, x2, x3)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x5)
U1_GA(x1, x2, x3) = U1_GA(x3)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x4)
U11_GGG(x1, x2, x3, x4, x5) = U11_GGG(x1, x3, x5)
U19_GGA(x1, x2, x3, x4) = U19_GGA(x4)
U6_G(x1, x2, x3) = U6_G(x2, x3)
U13_GGG(x1, x2, x3, x4, x5) = U13_GGG(x5)
U8_GGG(x1, x2, x3, x4, x5) = U8_GGG(x1, x2, x3, x4, x5)
ISPLUS_IN_GGA(x1, x2, x3) = ISPLUS_IN_GGA(x1, x2)
U5_AGA(x1, x2, x3, x4, x5) = U5_AGA(x2, x5)
U9_GGG(x1, x2, x3, x4, x5) = U9_GGG(x1, x2, x3, x4, x5)
U18_GGA(x1, x2, x3, x4) = U18_GGA(x4)
=\=_IN_GG(x1, x2) = =\=_IN_GG(x1, x2)
U2_GA(x1, x2, x3) = U2_GA(x2, x3)
PERM_IN_GA(x1, x2) = PERM_IN_GA(x1)

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

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

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

QUEENS_IN_GA(X, Y) → U1_GA(X, Y, perm_in_ga(X, Y))
QUEENS_IN_GA(X, Y) → PERM_IN_GA(X, Y)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
PERM_IN_GA(.(X, Y), .(V, Res)) → DELETE_IN_AGA(V, .(X, Y), Rest)
DELETE_IN_AGA(X, .(F, T), .(F, R)) → U5_AGA(X, F, T, R, delete_in_aga(X, T, R))
DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_GA(X, Y, V, Res, perm_in_ga(Rest, Res))
U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
U1_GA(X, Y, perm_out_ga(X, Y)) → U2_GA(X, Y, safe_in_g(Y))
U1_GA(X, Y, perm_out_ga(X, Y)) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, succ(zero)))
SAFE_IN_G(.(X, Y)) → NOATTACK_IN_GGG(X, Y, succ(zero))
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, =\=_in_gg(X, F))
NOATTACK_IN_GGG(X, .(F, T), N) → =\=_IN_GG(X, F)
U8_GGG(X, F, T, N, =\=_out_gg(X, F)) → U9_GGG(X, F, T, N, =\=_in_gg(X, +(F, N)))
U8_GGG(X, F, T, N, =\=_out_gg(X, F)) → =\=_IN_GG(X, +(F, N))
U9_GGG(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_GGG(X, F, T, N, =\=_in_gg(F, +(X, N)))
U9_GGG(X, F, T, N, =\=_out_gg(X, +(F, N))) → =\=_IN_GG(F, +(X, N))
U10_GGG(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_GGG(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
U10_GGG(X, F, T, N, =\=_out_gg(F, +(X, N))) → ISPLUS_IN_GGA(N, succ(zero), U)
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → U17_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → U18_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → U19_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → U20_GGA(X, Y, Z, isPlus_in_gga(X, Y, Z))
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)
U11_GGG(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_GGG(X, F, T, N, =_in_ag(N1, U))
U11_GGG(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → =_IN_AG(N1, U)
U12_GGG(X, F, T, N, =_out_ag(N1, U)) → U13_GGG(X, F, T, N, noattack_in_ggg(X, T, N1))
U12_GGG(X, F, T, N, =_out_ag(N1, U)) → NOATTACK_IN_GGG(X, T, N1)
U6_G(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_G(X, Y, safe_in_g(Y))
U6_G(X, Y, noattack_out_ggg(X, Y, succ(zero))) → SAFE_IN_G(Y)

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                            ↳ UsableRulesProof

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

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

ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

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

ISPLUS_IN_GGA(succ(X), succ(Y), succ(succ(Z))) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), succ(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(succ(X), pred(Y), Z) → ISPLUS_IN_GGA(X, Y, Z)
ISPLUS_IN_GGA(pred(X), pred(Y), pred(pred(Z))) → ISPLUS_IN_GGA(X, Y, Z)

R is empty.
The argument filtering Pi contains the following mapping:
succ(x1) = succ(x1)
pred(x1) = pred(x1)
ISPLUS_IN_GGA(x1, x2, x3) = ISPLUS_IN_GGA(x1, x2)

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

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

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

ISPLUS_IN_GGA(succ(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
ISPLUS_IN_GGA(pred(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)
ISPLUS_IN_GGA(pred(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
ISPLUS_IN_GGA(succ(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

ISPLUS_IN_GGA(succ(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISPLUS_IN_GGA(pred(X), succ(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISPLUS_IN_GGA(succ(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2
ISPLUS_IN_GGA(pred(X), pred(Y)) → ISPLUS_IN_GGA(X, Y)
The graph contains the following edges 1 > 1, 2 > 2

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

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

NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, =\=_in_gg(X, F))
U9_GGG(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_GGG(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_GGG(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_GGG(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
U11_GGG(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_GGG(X, F, T, N, =_in_ag(N1, U))
U12_GGG(X, F, T, N, =_out_ag(N1, U)) → NOATTACK_IN_GGG(X, T, N1)
U8_GGG(X, F, T, N, =\=_out_gg(X, F)) → U9_GGG(X, F, T, N, =\=_in_gg(X, +(F, N)))

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
queens_in_ga(x1, x2) = queens_in_ga(x1)
U1_ga(x1, x2, x3) = U1_ga(x3)
perm_in_ga(x1, x2) = perm_in_ga(x1)
[] = []
perm_out_ga(x1, x2) = perm_out_ga(x2)
.(x1, x2) = .(x1, x2)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x5)
delete_in_aga(x1, x2, x3) = delete_in_aga(x2)
delete_out_aga(x1, x2, x3) = delete_out_aga(x1, x3)
U5_aga(x1, x2, x3, x4, x5) = U5_aga(x2, x5)
U4_ga(x1, x2, x3, x4, x5) = U4_ga(x3, x5)
U2_ga(x1, x2, x3) = U2_ga(x2, x3)
safe_in_g(x1) = safe_in_g(x1)
safe_out_g(x1) = safe_out_g
U6_g(x1, x2, x3) = U6_g(x2, x3)
noattack_in_ggg(x1, x2, x3) = noattack_in_ggg(x1, x2, x3)
noattack_out_ggg(x1, x2, x3) = noattack_out_ggg
U8_ggg(x1, x2, x3, x4, x5) = U8_ggg(x1, x2, x3, x4, x5)
=\=_in_gg(x1, x2) = =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2) = =\=_out_gg
U9_ggg(x1, x2, x3, x4, x5) = U9_ggg(x1, x2, x3, x4, x5)
+(x1, x2) = +(x1, x2)
U10_ggg(x1, x2, x3, x4, x5) = U10_ggg(x1, x3, x4, x5)
U11_ggg(x1, x2, x3, x4, x5) = U11_ggg(x1, x3, x5)
isPlus_in_gga(x1, x2, x3) = isPlus_in_gga(x1, x2)
zero = zero
isPlus_out_gga(x1, x2, x3) = isPlus_out_gga(x3)
succ(x1) = succ(x1)
U17_gga(x1, x2, x3, x4) = U17_gga(x4)
pred(x1) = pred(x1)
U18_gga(x1, x2, x3, x4) = U18_gga(x4)
U19_gga(x1, x2, x3, x4) = U19_gga(x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x4)
U12_ggg(x1, x2, x3, x4, x5) = U12_ggg(x1, x3, x5)
=_in_ag(x1, x2) = =_in_ag(x2)
=_out_ag(x1, x2) = =_out_ag(x1)
U13_ggg(x1, x2, x3, x4, x5) = U13_ggg(x5)
U7_g(x1, x2, x3) = U7_g(x3)
queens_out_ga(x1, x2) = queens_out_ga(x2)
U12_GGG(x1, x2, x3, x4, x5) = U12_GGG(x1, x3, x5)
U10_GGG(x1, x2, x3, x4, x5) = U10_GGG(x1, x3, x4, x5)
NOATTACK_IN_GGG(x1, x2, x3) = NOATTACK_IN_GGG(x1, x2, x3)
U11_GGG(x1, x2, x3, x4, x5) = U11_GGG(x1, x3, x5)
U8_GGG(x1, x2, x3, x4, x5) = U8_GGG(x1, x2, x3, x4, x5)
U9_GGG(x1, x2, x3, x4, x5) = U9_GGG(x1, x2, x3, x4, x5)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting [30] we can delete all non-usable rules from R.

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

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

NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, =\=_in_gg(X, F))
U9_GGG(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_GGG(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_GGG(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_GGG(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
U11_GGG(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_GGG(X, F, T, N, =_in_ag(N1, U))
U12_GGG(X, F, T, N, =_out_ag(N1, U)) → NOATTACK_IN_GGG(X, T, N1)
U8_GGG(X, F, T, N, =\=_out_gg(X, F)) → U9_GGG(X, F, T, N, =\=_in_gg(X, +(F, N)))

The TRS R consists of the following rules:

=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
=_in_ag(X, X) → =_out_ag(X, X)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
=\=_in_gg(x1, x2) = =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2) = =\=_out_gg
+(x1, x2) = +(x1, x2)
isPlus_in_gga(x1, x2, x3) = isPlus_in_gga(x1, x2)
zero = zero
isPlus_out_gga(x1, x2, x3) = isPlus_out_gga(x3)
succ(x1) = succ(x1)
U17_gga(x1, x2, x3, x4) = U17_gga(x4)
pred(x1) = pred(x1)
U18_gga(x1, x2, x3, x4) = U18_gga(x4)
U19_gga(x1, x2, x3, x4) = U19_gga(x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x4)
=_in_ag(x1, x2) = =_in_ag(x2)
=_out_ag(x1, x2) = =_out_ag(x1)
U12_GGG(x1, x2, x3, x4, x5) = U12_GGG(x1, x3, x5)
U10_GGG(x1, x2, x3, x4, x5) = U10_GGG(x1, x3, x4, x5)
NOATTACK_IN_GGG(x1, x2, x3) = NOATTACK_IN_GGG(x1, x2, x3)
U11_GGG(x1, x2, x3, x4, x5) = U11_GGG(x1, x3, x5)
U8_GGG(x1, x2, x3, x4, x5) = U8_GGG(x1, x2, x3, x4, x5)
U9_GGG(x1, x2, x3, x4, x5) = U9_GGG(x1, x2, x3, x4, x5)

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

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

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

NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, =\=_in_gg(X, F))
U10_GGG(X, T, N, =\=_out_gg) → U11_GGG(X, T, isPlus_in_gga(N, succ(zero)))
U8_GGG(X, F, T, N, =\=_out_gg) → U9_GGG(X, F, T, N, =\=_in_gg(X, +(F, N)))
U12_GGG(X, T, =_out_ag(N1)) → NOATTACK_IN_GGG(X, T, N1)
U9_GGG(X, F, T, N, =\=_out_gg) → U10_GGG(X, T, N, =\=_in_gg(F, +(X, N)))
U11_GGG(X, T, isPlus_out_gga(U)) → U12_GGG(X, T, =_in_ag(U))

The TRS R consists of the following rules:

=\=_in_gg(X0, X1) → =\=_out_gg
isPlus_in_gga(zero, X) → isPlus_out_gga(X)
isPlus_in_gga(succ(X), succ(Y)) → U17_gga(isPlus_in_gga(X, Y))
isPlus_in_gga(pred(X), succ(Y)) → U19_gga(isPlus_in_gga(X, Y))
=_in_ag(X) → =_out_ag(X)
U17_gga(isPlus_out_gga(Z)) → isPlus_out_gga(succ(succ(Z)))
U19_gga(isPlus_out_gga(Z)) → isPlus_out_gga(Z)
isPlus_in_gga(succ(X), zero) → isPlus_out_gga(succ(X))
isPlus_in_gga(succ(X), pred(Y)) → U18_gga(isPlus_in_gga(X, Y))
isPlus_in_gga(pred(X), zero) → isPlus_out_gga(pred(X))
isPlus_in_gga(pred(X), pred(Y)) → U20_gga(isPlus_in_gga(X, Y))
U18_gga(isPlus_out_gga(Z)) → isPlus_out_gga(Z)
U20_gga(isPlus_out_gga(Z)) → isPlus_out_gga(pred(pred(Z)))

The set Q consists of the following terms:

=\=_in_gg(x0, x1)
isPlus_in_gga(x0, x1)
=_in_ag(x0)
U17_gga(x0)
U19_gga(x0)
U18_gga(x0)
U20_gga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

U8_GGG(X, F, T, N, =\=_out_gg) → U9_GGG(X, F, T, N, =\=_in_gg(X, +(F, N)))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
U12_GGG(X, T, =_out_ag(N1)) → NOATTACK_IN_GGG(X, T, N1)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
U10_GGG(X, T, N, =\=_out_gg) → U11_GGG(X, T, isPlus_in_gga(N, succ(zero)))
The graph contains the following edges 1 >= 1, 2 >= 2
U11_GGG(X, T, isPlus_out_gga(U)) → U12_GGG(X, T, =_in_ag(U))
The graph contains the following edges 1 >= 1, 2 >= 2
U9_GGG(X, F, T, N, =\=_out_gg) → U10_GGG(X, T, N, =\=_in_gg(F, +(X, N)))
The graph contains the following edges 1 >= 1, 3 >= 2, 4 >= 3
NOATTACK_IN_GGG(X, .(F, T), N) → U8_GGG(X, F, T, N, =\=_in_gg(X, F))
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 3 >= 4

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                          ↳ PiDP

                          ↳ PiDP

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

U6_G(X, Y, noattack_out_ggg(X, Y, succ(zero))) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, succ(zero)))

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                          ↳ PiDP

                          ↳ PiDP

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

U6_G(X, Y, noattack_out_ggg(X, Y, succ(zero))) → SAFE_IN_G(Y)
SAFE_IN_G(.(X, Y)) → U6_G(X, Y, noattack_in_ggg(X, Y, succ(zero)))

The TRS R consists of the following rules:

noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
=_in_ag(X, X) → =_out_ag(X, X)
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
noattack_in_ggg(x1, x2, x3) = noattack_in_ggg(x1, x2, x3)
noattack_out_ggg(x1, x2, x3) = noattack_out_ggg
U8_ggg(x1, x2, x3, x4, x5) = U8_ggg(x1, x2, x3, x4, x5)
=\=_in_gg(x1, x2) = =\=_in_gg(x1, x2)
=\=_out_gg(x1, x2) = =\=_out_gg
U9_ggg(x1, x2, x3, x4, x5) = U9_ggg(x1, x2, x3, x4, x5)
+(x1, x2) = +(x1, x2)
U10_ggg(x1, x2, x3, x4, x5) = U10_ggg(x1, x3, x4, x5)
U11_ggg(x1, x2, x3, x4, x5) = U11_ggg(x1, x3, x5)
isPlus_in_gga(x1, x2, x3) = isPlus_in_gga(x1, x2)
zero = zero
isPlus_out_gga(x1, x2, x3) = isPlus_out_gga(x3)
succ(x1) = succ(x1)
U17_gga(x1, x2, x3, x4) = U17_gga(x4)
pred(x1) = pred(x1)
U18_gga(x1, x2, x3, x4) = U18_gga(x4)
U19_gga(x1, x2, x3, x4) = U19_gga(x4)
U20_gga(x1, x2, x3, x4) = U20_gga(x4)
U12_ggg(x1, x2, x3, x4, x5) = U12_ggg(x1, x3, x5)
=_in_ag(x1, x2) = =_in_ag(x2)
=_out_ag(x1, x2) = =_out_ag(x1)
U13_ggg(x1, x2, x3, x4, x5) = U13_ggg(x5)
SAFE_IN_G(x1) = SAFE_IN_G(x1)
U6_G(x1, x2, x3) = U6_G(x2, x3)

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

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                          ↳ PiDP

                          ↳ PiDP

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

SAFE_IN_G(.(X, Y)) → U6_G(Y, noattack_in_ggg(X, Y, succ(zero)))
U6_G(Y, noattack_out_ggg) → SAFE_IN_G(Y)

The TRS R consists of the following rules:

noattack_in_ggg(X, [], N) → noattack_out_ggg
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
U8_ggg(X, F, T, N, =\=_out_gg) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
=\=_in_gg(X0, X1) → =\=_out_gg
U9_ggg(X, F, T, N, =\=_out_gg) → U10_ggg(X, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, T, N, =\=_out_gg) → U11_ggg(X, T, isPlus_in_gga(N, succ(zero)))
U11_ggg(X, T, isPlus_out_gga(U)) → U12_ggg(X, T, =_in_ag(U))
isPlus_in_gga(zero, X) → isPlus_out_gga(X)
isPlus_in_gga(succ(X), succ(Y)) → U17_gga(isPlus_in_gga(X, Y))
isPlus_in_gga(pred(X), succ(Y)) → U19_gga(isPlus_in_gga(X, Y))
U12_ggg(X, T, =_out_ag(N1)) → U13_ggg(noattack_in_ggg(X, T, N1))
U17_gga(isPlus_out_gga(Z)) → isPlus_out_gga(succ(succ(Z)))
U19_gga(isPlus_out_gga(Z)) → isPlus_out_gga(Z)
=_in_ag(X) → =_out_ag(X)
U13_ggg(noattack_out_ggg) → noattack_out_ggg
isPlus_in_gga(succ(X), zero) → isPlus_out_gga(succ(X))
isPlus_in_gga(succ(X), pred(Y)) → U18_gga(isPlus_in_gga(X, Y))
isPlus_in_gga(pred(X), zero) → isPlus_out_gga(pred(X))
isPlus_in_gga(pred(X), pred(Y)) → U20_gga(isPlus_in_gga(X, Y))
U18_gga(isPlus_out_gga(Z)) → isPlus_out_gga(Z)
U20_gga(isPlus_out_gga(Z)) → isPlus_out_gga(pred(pred(Z)))

The set Q consists of the following terms:

noattack_in_ggg(x0, x1, x2)
U8_ggg(x0, x1, x2, x3, x4)
=\=_in_gg(x0, x1)
U9_ggg(x0, x1, x2, x3, x4)
U10_ggg(x0, x1, x2, x3)
U11_ggg(x0, x1, x2)
isPlus_in_gga(x0, x1)
U12_ggg(x0, x1, x2)
U17_gga(x0)
U19_gga(x0)
=_in_ag(x0)
U13_ggg(x0)
U18_gga(x0)
U20_gga(x0)

We have to consider all (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

SAFE_IN_G(.(X, Y)) → U6_G(Y, noattack_in_ggg(X, Y, succ(zero)))
The graph contains the following edges 1 > 1
U6_G(Y, noattack_out_ggg) → SAFE_IN_G(Y)
The graph contains the following edges 1 >= 1

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                          ↳ PiDP

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

DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                          ↳ PiDP

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

DELETE_IN_AGA(X, .(F, T), .(F, R)) → DELETE_IN_AGA(X, T, R)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
DELETE_IN_AGA(x1, x2, x3) = DELETE_IN_AGA(x2)

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

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ QDPSizeChangeProof

                          ↳ PiDP

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

DELETE_IN_AGA(.(F, T)) → DELETE_IN_AGA(T)

From the DPs we obtained the following set of size-change graphs:

DELETE_IN_AGA(.(F, T)) → DELETE_IN_AGA(T)
The graph contains the following edges 1 > 1

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

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

U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))

The TRS R consists of the following rules:

queens_in_ga(X, Y) → U1_ga(X, Y, perm_in_ga(X, Y))
perm_in_ga([], []) → perm_out_ga([], [])
perm_in_ga(.(X, Y), .(V, Res)) → U3_ga(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))
delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))
U3_ga(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → U4_ga(X, Y, V, Res, perm_in_ga(Rest, Res))
U4_ga(X, Y, V, Res, perm_out_ga(Rest, Res)) → perm_out_ga(.(X, Y), .(V, Res))
U1_ga(X, Y, perm_out_ga(X, Y)) → U2_ga(X, Y, safe_in_g(Y))
safe_in_g([]) → safe_out_g([])
safe_in_g(.(X, Y)) → U6_g(X, Y, noattack_in_ggg(X, Y, succ(zero)))
noattack_in_ggg(X, [], N) → noattack_out_ggg(X, [], N)
noattack_in_ggg(X, .(F, T), N) → U8_ggg(X, F, T, N, =\=_in_gg(X, F))
=\=_in_gg(X0, X1) → =\=_out_gg(X0, X1)
U8_ggg(X, F, T, N, =\=_out_gg(X, F)) → U9_ggg(X, F, T, N, =\=_in_gg(X, +(F, N)))
U9_ggg(X, F, T, N, =\=_out_gg(X, +(F, N))) → U10_ggg(X, F, T, N, =\=_in_gg(F, +(X, N)))
U10_ggg(X, F, T, N, =\=_out_gg(F, +(X, N))) → U11_ggg(X, F, T, N, isPlus_in_gga(N, succ(zero), U))
isPlus_in_gga(zero, X, X) → isPlus_out_gga(zero, X, X)
isPlus_in_gga(succ(X), zero, succ(X)) → isPlus_out_gga(succ(X), zero, succ(X))
isPlus_in_gga(succ(X), succ(Y), succ(succ(Z))) → U17_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(succ(X), pred(Y), Z) → U18_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), zero, pred(X)) → isPlus_out_gga(pred(X), zero, pred(X))
isPlus_in_gga(pred(X), succ(Y), Z) → U19_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
isPlus_in_gga(pred(X), pred(Y), pred(pred(Z))) → U20_gga(X, Y, Z, isPlus_in_gga(X, Y, Z))
U20_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), pred(Y), pred(pred(Z)))
U19_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(pred(X), succ(Y), Z)
U18_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), pred(Y), Z)
U17_gga(X, Y, Z, isPlus_out_gga(X, Y, Z)) → isPlus_out_gga(succ(X), succ(Y), succ(succ(Z)))
U11_ggg(X, F, T, N, isPlus_out_gga(N, succ(zero), U)) → U12_ggg(X, F, T, N, =_in_ag(N1, U))
=_in_ag(X, X) → =_out_ag(X, X)
U12_ggg(X, F, T, N, =_out_ag(N1, U)) → U13_ggg(X, F, T, N, noattack_in_ggg(X, T, N1))
U13_ggg(X, F, T, N, noattack_out_ggg(X, T, N1)) → noattack_out_ggg(X, .(F, T), N)
U6_g(X, Y, noattack_out_ggg(X, Y, succ(zero))) → U7_g(X, Y, safe_in_g(Y))
U7_g(X, Y, safe_out_g(Y)) → safe_out_g(.(X, Y))
U2_ga(X, Y, safe_out_g(Y)) → queens_out_ga(X, Y)

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

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

U3_GA(X, Y, V, Res, delete_out_aga(V, .(X, Y), Rest)) → PERM_IN_GA(Rest, Res)
PERM_IN_GA(.(X, Y), .(V, Res)) → U3_GA(X, Y, V, Res, delete_in_aga(V, .(X, Y), Rest))

The TRS R consists of the following rules:

delete_in_aga(X, .(X, Y), Y) → delete_out_aga(X, .(X, Y), Y)
delete_in_aga(X, .(F, T), .(F, R)) → U5_aga(X, F, T, R, delete_in_aga(X, T, R))
U5_aga(X, F, T, R, delete_out_aga(X, T, R)) → delete_out_aga(X, .(F, T), .(F, R))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
delete_in_aga(x1, x2, x3) = delete_in_aga(x2)
delete_out_aga(x1, x2, x3) = delete_out_aga(x1, x3)
U5_aga(x1, x2, x3, x4, x5) = U5_aga(x2, x5)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x5)
PERM_IN_GA(x1, x2) = PERM_IN_GA(x1)

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

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ RuleRemovalProof

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

PERM_IN_GA(.(X, Y)) → U3_GA(delete_in_aga(.(X, Y)))
U3_GA(delete_out_aga(V, Rest)) → PERM_IN_GA(Rest)

The TRS R consists of the following rules:

delete_in_aga(.(X, Y)) → delete_out_aga(X, Y)
delete_in_aga(.(F, T)) → U5_aga(F, delete_in_aga(T))
U5_aga(F, delete_out_aga(X, R)) → delete_out_aga(X, .(F, R))

The set Q consists of the following terms:

delete_in_aga(x0)
U5_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

delete_in_aga(.(X, Y)) → delete_out_aga(X, Y)

Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(PERM_IN_GA(x₁)) = 2·x₁
POL(U3_GA(x₁)) = 2·x₁
POL(U5_aga(x₁, x₂)) = 1 + x₁ + 2·x₂
POL(delete_in_aga(x₁)) = x₁
POL(delete_out_aga(x₁, x₂)) = x₁ + x₂

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ RuleRemovalProof

                                      ↳ QDP

                                        ↳ RuleRemovalProof

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

PERM_IN_GA(.(X, Y)) → U3_GA(delete_in_aga(.(X, Y)))
U3_GA(delete_out_aga(V, Rest)) → PERM_IN_GA(Rest)

The TRS R consists of the following rules:

delete_in_aga(.(F, T)) → U5_aga(F, delete_in_aga(T))
U5_aga(F, delete_out_aga(X, R)) → delete_out_aga(X, .(F, R))

The set Q consists of the following terms:

delete_in_aga(x0)
U5_aga(x0, x1)

U3_GA(delete_out_aga(V, Rest)) → PERM_IN_GA(Rest)

Used ordering: POLO with Polynomial interpretation [25]:

POL(.(x₁, x₂)) = x₁ + x₂
POL(PERM_IN_GA(x₁)) = 2·x₁
POL(U3_GA(x₁)) = x₁
POL(U5_aga(x₁, x₂)) = 2·x₁ + x₂
POL(delete_in_aga(x₁)) = 2·x₁
POL(delete_out_aga(x₁, x₂)) = 2 + x₁ + 2·x₂

↳ Prolog

  ↳ PredefinedPredicateTransformerProof

    ↳ Prolog

      ↳ CutEliminatorProof

        ↳ Prolog

          ↳ UndefinedPredicateHandlerProof

            ↳ Prolog

              ↳ PrologToPiTRSProof

                ↳ PiTRS

                  ↳ DependencyPairsProof

                    ↳ PiDP

                      ↳ DependencyGraphProof

                        ↳ AND

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                          ↳ PiDP

                            ↳ UsableRulesProof

                              ↳ PiDP

                                ↳ PiDPToQDPProof

                                  ↳ QDP

                                    ↳ RuleRemovalProof

                                      ↳ QDP

                                        ↳ RuleRemovalProof

                                          ↳ QDP

                                            ↳ DependencyGraphProof

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

PERM_IN_GA(.(X, Y)) → U3_GA(delete_in_aga(.(X, Y)))

The TRS R consists of the following rules:

delete_in_aga(.(F, T)) → U5_aga(F, delete_in_aga(T))
U5_aga(F, delete_out_aga(X, R)) → delete_out_aga(X, .(F, R))

The set Q consists of the following terms:

delete_in_aga(x0)
U5_aga(x0, x1)

We have to consider all (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 0 SCCs with 1 less node.