Left Termination of the query pattern queens(f) w.r.t. the given Prolog program could successfully be proven:



PROLOG
  ↳ PrologToPiTRSProof

queens1(Y) :- perm2(.2(s1(00), .2(s12 (00), .2(s13 (00), .2(s14 (00), .2(s15 (00), .2(s16 (00), .2(s17 (00), .2(s18 (00), {}0)))))))), Y), safe1(Y).
perm2({}0, {}0).
perm2(.2(X, Y), .2(V, Res)) :- delete3(V, .2(X, Y), Rest), perm2(Rest, Res).
delete3(X, .2(X, Y), Y).
delete3(X, .2(F, T), .2(F, R)) :- delete3(X, T, R).
safe1({}0).
safe1(.2(X, Y)) :- noattack3(X, Y, s1(00)), safe1(Y).
noattack3(X, {}0, N).
noattack3(X, .2(F, T), N) :- notEq2(X, F), add3(F, N, FplusN), notEq2(X, FplusN), add3(X, N, XplusN), notEq2(F, XplusN), noattack3(X, T, s1(N)).
add3(00, X, X).
add3(s1(X), Y, s1(Z)) :- add3(X, Y, Z).
notEq2(00, s1(X)).
notEq2(s1(X), 00).
notEq2(s1(X), s1(Y)) :- notEq2(X, Y).


With regard to the inferred argument filtering the predicates were used in the following modes:
queens1: (f)
perm2: (b,f)
delete3: (f,b,f)
safe1: (b)
noattack3: (b,b,b)
notEq2: (b,b)
add3: (b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

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

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)


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

QUEENS_1_IN_A1(Y) -> IF_QUEENS_1_IN_1_A2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
QUEENS_1_IN_A1(Y) -> PERM_2_IN_GA2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)
PERM_2_IN_GA2(._22(X, Y), ._22(V, Res)) -> IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
PERM_2_IN_GA2(._22(X, Y), ._22(V, Res)) -> DELETE_3_IN_AGA3(V, ._22(X, Y), Rest)
DELETE_3_IN_AGA3(X, ._22(F, T), ._22(F, R)) -> IF_DELETE_3_IN_1_AGA5(X, F, T, R, delete_3_in_aga3(X, T, R))
DELETE_3_IN_AGA3(X, ._22(F, T), ._22(F, R)) -> DELETE_3_IN_AGA3(X, T, R)
IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> IF_PERM_2_IN_2_GA6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> PERM_2_IN_GA2(Rest, Res)
IF_QUEENS_1_IN_1_A2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> IF_QUEENS_1_IN_2_A2(Y, safe_1_in_g1(Y))
IF_QUEENS_1_IN_1_A2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> SAFE_1_IN_G1(Y)
SAFE_1_IN_G1(._22(X, Y)) -> IF_SAFE_1_IN_1_G3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
SAFE_1_IN_G1(._22(X, Y)) -> NOATTACK_3_IN_GGG3(X, Y, s_11(0_0))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_in_gg2(X, F))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> NOTEQ_2_IN_GG2(X, F)
NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_NOTEQ_2_IN_1_GG3(X, Y, notEq_2_in_gg2(X, Y))
NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> NOTEQ_2_IN_GG2(X, Y)
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg2(X, F)) -> IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg2(X, F)) -> ADD_3_IN_GGA3(F, N, FplusN)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> NOTEQ_2_IN_GG2(X, FplusN)
IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> ADD_3_IN_GGA3(X, N, XplusN)
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> NOTEQ_2_IN_GG2(F, XplusN)
IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> IF_NOATTACK_3_IN_6_GGG5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> NOATTACK_3_IN_GGG3(X, T, s_11(N))
IF_SAFE_1_IN_1_G3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> IF_SAFE_1_IN_2_G3(X, Y, safe_1_in_g1(Y))
IF_SAFE_1_IN_1_G3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> SAFE_1_IN_G1(Y)

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
IF_NOATTACK_3_IN_5_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_5_GGG4(x1, x3, x4, x6)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
IF_DELETE_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_DELETE_3_IN_1_AGA2(x2, x5)
IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)
IF_NOTEQ_2_IN_1_GG3(x1, x2, x3)  =  IF_NOTEQ_2_IN_1_GG1(x3)
PERM_2_IN_GA2(x1, x2)  =  PERM_2_IN_GA1(x1)
IF_PERM_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_PERM_2_IN_1_GA1(x5)
IF_SAFE_1_IN_2_G3(x1, x2, x3)  =  IF_SAFE_1_IN_2_G1(x3)
QUEENS_1_IN_A1(x1)  =  QUEENS_1_IN_A
IF_QUEENS_1_IN_2_A2(x1, x2)  =  IF_QUEENS_1_IN_2_A2(x1, x2)
NOATTACK_3_IN_GGG3(x1, x2, x3)  =  NOATTACK_3_IN_GGG3(x1, x2, x3)
NOTEQ_2_IN_GG2(x1, x2)  =  NOTEQ_2_IN_GG2(x1, x2)
IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)
IF_NOATTACK_3_IN_6_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_6_GGG1(x5)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA1(x4)
DELETE_3_IN_AGA3(x1, x2, x3)  =  DELETE_3_IN_AGA1(x2)
IF_SAFE_1_IN_1_G3(x1, x2, x3)  =  IF_SAFE_1_IN_1_G2(x2, x3)
IF_NOATTACK_3_IN_3_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_3_GGG5(x1, x2, x3, x4, x6)
SAFE_1_IN_G1(x1)  =  SAFE_1_IN_G1(x1)
IF_QUEENS_1_IN_1_A2(x1, x2)  =  IF_QUEENS_1_IN_1_A1(x2)
IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)
IF_PERM_2_IN_2_GA6(x1, x2, x3, x4, x5, x6)  =  IF_PERM_2_IN_2_GA2(x3, x6)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

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

QUEENS_1_IN_A1(Y) -> IF_QUEENS_1_IN_1_A2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
QUEENS_1_IN_A1(Y) -> PERM_2_IN_GA2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)
PERM_2_IN_GA2(._22(X, Y), ._22(V, Res)) -> IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
PERM_2_IN_GA2(._22(X, Y), ._22(V, Res)) -> DELETE_3_IN_AGA3(V, ._22(X, Y), Rest)
DELETE_3_IN_AGA3(X, ._22(F, T), ._22(F, R)) -> IF_DELETE_3_IN_1_AGA5(X, F, T, R, delete_3_in_aga3(X, T, R))
DELETE_3_IN_AGA3(X, ._22(F, T), ._22(F, R)) -> DELETE_3_IN_AGA3(X, T, R)
IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> IF_PERM_2_IN_2_GA6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> PERM_2_IN_GA2(Rest, Res)
IF_QUEENS_1_IN_1_A2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> IF_QUEENS_1_IN_2_A2(Y, safe_1_in_g1(Y))
IF_QUEENS_1_IN_1_A2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> SAFE_1_IN_G1(Y)
SAFE_1_IN_G1(._22(X, Y)) -> IF_SAFE_1_IN_1_G3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
SAFE_1_IN_G1(._22(X, Y)) -> NOATTACK_3_IN_GGG3(X, Y, s_11(0_0))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_in_gg2(X, F))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> NOTEQ_2_IN_GG2(X, F)
NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_NOTEQ_2_IN_1_GG3(X, Y, notEq_2_in_gg2(X, Y))
NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> NOTEQ_2_IN_GG2(X, Y)
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg2(X, F)) -> IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg2(X, F)) -> ADD_3_IN_GGA3(F, N, FplusN)
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> IF_ADD_3_IN_1_GGA4(X, Y, Z, add_3_in_gga3(X, Y, Z))
ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> NOTEQ_2_IN_GG2(X, FplusN)
IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> ADD_3_IN_GGA3(X, N, XplusN)
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> NOTEQ_2_IN_GG2(F, XplusN)
IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> IF_NOATTACK_3_IN_6_GGG5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> NOATTACK_3_IN_GGG3(X, T, s_11(N))
IF_SAFE_1_IN_1_G3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> IF_SAFE_1_IN_2_G3(X, Y, safe_1_in_g1(Y))
IF_SAFE_1_IN_1_G3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> SAFE_1_IN_G1(Y)

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
IF_NOATTACK_3_IN_5_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_5_GGG4(x1, x3, x4, x6)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)
IF_DELETE_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_DELETE_3_IN_1_AGA2(x2, x5)
IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)
IF_NOTEQ_2_IN_1_GG3(x1, x2, x3)  =  IF_NOTEQ_2_IN_1_GG1(x3)
PERM_2_IN_GA2(x1, x2)  =  PERM_2_IN_GA1(x1)
IF_PERM_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_PERM_2_IN_1_GA1(x5)
IF_SAFE_1_IN_2_G3(x1, x2, x3)  =  IF_SAFE_1_IN_2_G1(x3)
QUEENS_1_IN_A1(x1)  =  QUEENS_1_IN_A
IF_QUEENS_1_IN_2_A2(x1, x2)  =  IF_QUEENS_1_IN_2_A2(x1, x2)
NOATTACK_3_IN_GGG3(x1, x2, x3)  =  NOATTACK_3_IN_GGG3(x1, x2, x3)
NOTEQ_2_IN_GG2(x1, x2)  =  NOTEQ_2_IN_GG2(x1, x2)
IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)
IF_NOATTACK_3_IN_6_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_6_GGG1(x5)
IF_ADD_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_ADD_3_IN_1_GGA1(x4)
DELETE_3_IN_AGA3(x1, x2, x3)  =  DELETE_3_IN_AGA1(x2)
IF_SAFE_1_IN_1_G3(x1, x2, x3)  =  IF_SAFE_1_IN_1_G2(x2, x3)
IF_NOATTACK_3_IN_3_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_3_GGG5(x1, x2, x3, x4, x6)
SAFE_1_IN_G1(x1)  =  SAFE_1_IN_G1(x1)
IF_QUEENS_1_IN_1_A2(x1, x2)  =  IF_QUEENS_1_IN_1_A1(x2)
IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)
IF_PERM_2_IN_2_GA6(x1, x2, x3, x4, x5, x6)  =  IF_PERM_2_IN_2_GA2(x3, x6)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 6 SCCs with 17 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
ADD_3_IN_GGA3(x1, x2, x3)  =  ADD_3_IN_GGA2(x1, x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

ADD_3_IN_GGA3(s_11(X), Y, s_11(Z)) -> ADD_3_IN_GGA3(X, Y, Z)

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

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

ADD_3_IN_GGA2(s_11(X), Y) -> ADD_3_IN_GGA2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {ADD_3_IN_GGA2}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> NOTEQ_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
NOTEQ_2_IN_GG2(x1, x2)  =  NOTEQ_2_IN_GG2(x1, x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> NOTEQ_2_IN_GG2(X, Y)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

NOTEQ_2_IN_GG2(s_11(X), s_11(Y)) -> NOTEQ_2_IN_GG2(X, Y)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {NOTEQ_2_IN_GG2}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> NOATTACK_3_IN_GGG3(X, T, s_11(N))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_in_gg2(X, F))
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg2(X, F)) -> IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
IF_NOATTACK_3_IN_5_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_5_GGG4(x1, x3, x4, x6)
IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)
NOATTACK_3_IN_GGG3(x1, x2, x3)  =  NOATTACK_3_IN_GGG3(x1, x2, x3)
IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)
IF_NOATTACK_3_IN_3_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_3_GGG5(x1, x2, x3, x4, x6)
IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> NOATTACK_3_IN_GGG3(X, T, s_11(N))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_in_gg2(X, F))
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg2(X, F)) -> IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> IF_NOATTACK_3_IN_5_GGG6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> IF_NOATTACK_3_IN_3_GGG6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))

The TRS R consists of the following rules:

add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
IF_NOATTACK_3_IN_5_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_5_GGG4(x1, x3, x4, x6)
IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_4_GGG5(x1, x2, x3, x4, x5)
NOATTACK_3_IN_GGG3(x1, x2, x3)  =  NOATTACK_3_IN_GGG3(x1, x2, x3)
IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_1_GGG5(x1, x2, x3, x4, x5)
IF_NOATTACK_3_IN_3_GGG6(x1, x2, x3, x4, x5, x6)  =  IF_NOATTACK_3_IN_3_GGG5(x1, x2, x3, x4, x6)
IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)  =  IF_NOATTACK_3_IN_2_GGG5(x1, x2, x3, x4, x5)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

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

IF_NOATTACK_3_IN_3_GGG5(X, F, T, N, notEq_2_out_gg) -> IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_in_gga2(X, N))
IF_NOATTACK_3_IN_5_GGG4(X, T, N, notEq_2_out_gg) -> NOATTACK_3_IN_GGG3(X, T, s_11(N))
NOATTACK_3_IN_GGG3(X, ._22(F, T), N) -> IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_in_gg2(X, F))
IF_NOATTACK_3_IN_1_GGG5(X, F, T, N, notEq_2_out_gg) -> IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_in_gga2(F, N))
IF_NOATTACK_3_IN_4_GGG5(X, F, T, N, add_3_out_gga1(XplusN)) -> IF_NOATTACK_3_IN_5_GGG4(X, T, N, notEq_2_in_gg2(F, XplusN))
IF_NOATTACK_3_IN_2_GGG5(X, F, T, N, add_3_out_gga1(FplusN)) -> IF_NOATTACK_3_IN_3_GGG5(X, F, T, N, notEq_2_in_gg2(X, FplusN))

The TRS R consists of the following rules:

add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg1(notEq_2_in_gg2(X, Y))
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_notEq_2_in_1_gg1(notEq_2_out_gg) -> notEq_2_out_gg

The set Q consists of the following terms:

add_3_in_gga2(x0, x1)
notEq_2_in_gg2(x0, x1)
if_add_3_in_1_gga1(x0)
if_notEq_2_in_1_gg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_NOATTACK_3_IN_4_GGG5, IF_NOATTACK_3_IN_3_GGG5, NOATTACK_3_IN_GGG3, IF_NOATTACK_3_IN_5_GGG4, IF_NOATTACK_3_IN_1_GGG5, IF_NOATTACK_3_IN_2_GGG5}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

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

SAFE_1_IN_G1(._22(X, Y)) -> IF_SAFE_1_IN_1_G3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
IF_SAFE_1_IN_1_G3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> SAFE_1_IN_G1(Y)

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
IF_SAFE_1_IN_1_G3(x1, x2, x3)  =  IF_SAFE_1_IN_1_G2(x2, x3)
SAFE_1_IN_G1(x1)  =  SAFE_1_IN_G1(x1)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

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

SAFE_1_IN_G1(._22(X, Y)) -> IF_SAFE_1_IN_1_G3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
IF_SAFE_1_IN_1_G3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> SAFE_1_IN_G1(Y)

The TRS R consists of the following rules:

noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
IF_SAFE_1_IN_1_G3(x1, x2, x3)  =  IF_SAFE_1_IN_1_G2(x2, x3)
SAFE_1_IN_G1(x1)  =  SAFE_1_IN_G1(x1)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

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

SAFE_1_IN_G1(._22(X, Y)) -> IF_SAFE_1_IN_1_G2(Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
IF_SAFE_1_IN_1_G2(Y, noattack_3_out_ggg) -> SAFE_1_IN_G1(Y)

The TRS R consists of the following rules:

noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga2(F, N))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg1(notEq_2_in_gg2(X, Y))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga1(FplusN)) -> if_noattack_3_in_3_ggg5(X, F, T, N, notEq_2_in_gg2(X, FplusN))
if_notEq_2_in_1_gg1(notEq_2_out_gg) -> notEq_2_out_gg
add_3_in_gga2(0_0, X) -> add_3_out_gga1(X)
add_3_in_gga2(s_11(X), Y) -> if_add_3_in_1_gga1(add_3_in_gga2(X, Y))
if_noattack_3_in_3_ggg5(X, F, T, N, notEq_2_out_gg) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga2(X, N))
if_add_3_in_1_gga1(add_3_out_gga1(Z)) -> add_3_out_gga1(s_11(Z))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga1(XplusN)) -> if_noattack_3_in_5_ggg4(X, T, N, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg4(X, T, N, notEq_2_out_gg) -> if_noattack_3_in_6_ggg1(noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg1(noattack_3_out_ggg) -> noattack_3_out_ggg

The set Q consists of the following terms:

noattack_3_in_ggg3(x0, x1, x2)
if_noattack_3_in_1_ggg5(x0, x1, x2, x3, x4)
notEq_2_in_gg2(x0, x1)
if_noattack_3_in_2_ggg5(x0, x1, x2, x3, x4)
if_notEq_2_in_1_gg1(x0)
add_3_in_gga2(x0, x1)
if_noattack_3_in_3_ggg5(x0, x1, x2, x3, x4)
if_add_3_in_1_gga1(x0)
if_noattack_3_in_4_ggg5(x0, x1, x2, x3, x4)
if_noattack_3_in_5_ggg4(x0, x1, x2, x3)
if_noattack_3_in_6_ggg1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_SAFE_1_IN_1_G2, SAFE_1_IN_G1}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP

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

DELETE_3_IN_AGA3(X, ._22(F, T), ._22(F, R)) -> DELETE_3_IN_AGA3(X, T, R)

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
DELETE_3_IN_AGA3(x1, x2, x3)  =  DELETE_3_IN_AGA1(x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

DELETE_3_IN_AGA3(X, ._22(F, T), ._22(F, R)) -> DELETE_3_IN_AGA3(X, T, R)

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

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

DELETE_3_IN_AGA1(._22(F, T)) -> DELETE_3_IN_AGA1(T)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DELETE_3_IN_AGA1}.
By using the subterm criterion together with the size-change analysis 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:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof

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

IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> PERM_2_IN_GA2(Rest, Res)
PERM_2_IN_GA2(._22(X, Y), ._22(V, Res)) -> IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))

The TRS R consists of the following rules:

queens_1_in_a1(Y) -> if_queens_1_in_1_a2(Y, perm_2_in_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y))
perm_2_in_ga2([]_0, []_0) -> perm_2_out_ga2([]_0, []_0)
perm_2_in_ga2(._22(X, Y), ._22(V, Res)) -> if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))
delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))
if_perm_2_in_1_ga5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_in_ga2(Rest, Res))
if_perm_2_in_2_ga6(X, Y, V, Res, Rest, perm_2_out_ga2(Rest, Res)) -> perm_2_out_ga2(._22(X, Y), ._22(V, Res))
if_queens_1_in_1_a2(Y, perm_2_out_ga2(._22(s_11(0_0), ._22(s_11(s_11(0_0)), ._22(s_11(s_11(s_11(0_0))), ._22(s_11(s_11(s_11(s_11(0_0)))), ._22(s_11(s_11(s_11(s_11(s_11(0_0))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0))))))), ._22(s_11(s_11(s_11(s_11(s_11(s_11(s_11(s_11(0_0)))))))), []_0)))))))), Y)) -> if_queens_1_in_2_a2(Y, safe_1_in_g1(Y))
safe_1_in_g1([]_0) -> safe_1_out_g1([]_0)
safe_1_in_g1(._22(X, Y)) -> if_safe_1_in_1_g3(X, Y, noattack_3_in_ggg3(X, Y, s_11(0_0)))
noattack_3_in_ggg3(X, []_0, N) -> noattack_3_out_ggg3(X, []_0, N)
noattack_3_in_ggg3(X, ._22(F, T), N) -> if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_in_gg2(X, F))
notEq_2_in_gg2(0_0, s_11(X)) -> notEq_2_out_gg2(0_0, s_11(X))
notEq_2_in_gg2(s_11(X), 0_0) -> notEq_2_out_gg2(s_11(X), 0_0)
notEq_2_in_gg2(s_11(X), s_11(Y)) -> if_notEq_2_in_1_gg3(X, Y, notEq_2_in_gg2(X, Y))
if_notEq_2_in_1_gg3(X, Y, notEq_2_out_gg2(X, Y)) -> notEq_2_out_gg2(s_11(X), s_11(Y))
if_noattack_3_in_1_ggg5(X, F, T, N, notEq_2_out_gg2(X, F)) -> if_noattack_3_in_2_ggg5(X, F, T, N, add_3_in_gga3(F, N, FplusN))
add_3_in_gga3(0_0, X, X) -> add_3_out_gga3(0_0, X, X)
add_3_in_gga3(s_11(X), Y, s_11(Z)) -> if_add_3_in_1_gga4(X, Y, Z, add_3_in_gga3(X, Y, Z))
if_add_3_in_1_gga4(X, Y, Z, add_3_out_gga3(X, Y, Z)) -> add_3_out_gga3(s_11(X), Y, s_11(Z))
if_noattack_3_in_2_ggg5(X, F, T, N, add_3_out_gga3(F, N, FplusN)) -> if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_in_gg2(X, FplusN))
if_noattack_3_in_3_ggg6(X, F, T, N, FplusN, notEq_2_out_gg2(X, FplusN)) -> if_noattack_3_in_4_ggg5(X, F, T, N, add_3_in_gga3(X, N, XplusN))
if_noattack_3_in_4_ggg5(X, F, T, N, add_3_out_gga3(X, N, XplusN)) -> if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_in_gg2(F, XplusN))
if_noattack_3_in_5_ggg6(X, F, T, N, XplusN, notEq_2_out_gg2(F, XplusN)) -> if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_in_ggg3(X, T, s_11(N)))
if_noattack_3_in_6_ggg5(X, F, T, N, noattack_3_out_ggg3(X, T, s_11(N))) -> noattack_3_out_ggg3(X, ._22(F, T), N)
if_safe_1_in_1_g3(X, Y, noattack_3_out_ggg3(X, Y, s_11(0_0))) -> if_safe_1_in_2_g3(X, Y, safe_1_in_g1(Y))
if_safe_1_in_2_g3(X, Y, safe_1_out_g1(Y)) -> safe_1_out_g1(._22(X, Y))
if_queens_1_in_2_a2(Y, safe_1_out_g1(Y)) -> queens_1_out_a1(Y)

The argument filtering Pi contains the following mapping:
queens_1_in_a1(x1)  =  queens_1_in_a
._22(x1, x2)  =  ._22(x1, x2)
s_11(x1)  =  s_11(x1)
0_0  =  0_0
[]_0  =  []_0
if_queens_1_in_1_a2(x1, x2)  =  if_queens_1_in_1_a1(x2)
perm_2_in_ga2(x1, x2)  =  perm_2_in_ga1(x1)
perm_2_out_ga2(x1, x2)  =  perm_2_out_ga1(x2)
if_perm_2_in_1_ga5(x1, x2, x3, x4, x5)  =  if_perm_2_in_1_ga1(x5)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
if_perm_2_in_2_ga6(x1, x2, x3, x4, x5, x6)  =  if_perm_2_in_2_ga2(x3, x6)
if_queens_1_in_2_a2(x1, x2)  =  if_queens_1_in_2_a2(x1, x2)
safe_1_in_g1(x1)  =  safe_1_in_g1(x1)
safe_1_out_g1(x1)  =  safe_1_out_g
if_safe_1_in_1_g3(x1, x2, x3)  =  if_safe_1_in_1_g2(x2, x3)
noattack_3_in_ggg3(x1, x2, x3)  =  noattack_3_in_ggg3(x1, x2, x3)
noattack_3_out_ggg3(x1, x2, x3)  =  noattack_3_out_ggg
if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_1_ggg5(x1, x2, x3, x4, x5)
notEq_2_in_gg2(x1, x2)  =  notEq_2_in_gg2(x1, x2)
notEq_2_out_gg2(x1, x2)  =  notEq_2_out_gg
if_notEq_2_in_1_gg3(x1, x2, x3)  =  if_notEq_2_in_1_gg1(x3)
if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_2_ggg5(x1, x2, x3, x4, x5)
add_3_in_gga3(x1, x2, x3)  =  add_3_in_gga2(x1, x2)
add_3_out_gga3(x1, x2, x3)  =  add_3_out_gga1(x3)
if_add_3_in_1_gga4(x1, x2, x3, x4)  =  if_add_3_in_1_gga1(x4)
if_noattack_3_in_3_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_3_ggg5(x1, x2, x3, x4, x6)
if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_4_ggg5(x1, x2, x3, x4, x5)
if_noattack_3_in_5_ggg6(x1, x2, x3, x4, x5, x6)  =  if_noattack_3_in_5_ggg4(x1, x3, x4, x6)
if_noattack_3_in_6_ggg5(x1, x2, x3, x4, x5)  =  if_noattack_3_in_6_ggg1(x5)
if_safe_1_in_2_g3(x1, x2, x3)  =  if_safe_1_in_2_g1(x3)
queens_1_out_a1(x1)  =  queens_1_out_a1(x1)
PERM_2_IN_GA2(x1, x2)  =  PERM_2_IN_GA1(x1)
IF_PERM_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_PERM_2_IN_1_GA1(x5)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof

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

IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_out_aga3(V, ._22(X, Y), Rest)) -> PERM_2_IN_GA2(Rest, Res)
PERM_2_IN_GA2(._22(X, Y), ._22(V, Res)) -> IF_PERM_2_IN_1_GA5(X, Y, V, Res, delete_3_in_aga3(V, ._22(X, Y), Rest))

The TRS R consists of the following rules:

delete_3_in_aga3(X, ._22(X, Y), Y) -> delete_3_out_aga3(X, ._22(X, Y), Y)
delete_3_in_aga3(X, ._22(F, T), ._22(F, R)) -> if_delete_3_in_1_aga5(X, F, T, R, delete_3_in_aga3(X, T, R))
if_delete_3_in_1_aga5(X, F, T, R, delete_3_out_aga3(X, T, R)) -> delete_3_out_aga3(X, ._22(F, T), ._22(F, R))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
delete_3_in_aga3(x1, x2, x3)  =  delete_3_in_aga1(x2)
delete_3_out_aga3(x1, x2, x3)  =  delete_3_out_aga2(x1, x3)
if_delete_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_delete_3_in_1_aga2(x2, x5)
PERM_2_IN_GA2(x1, x2)  =  PERM_2_IN_GA1(x1)
IF_PERM_2_IN_1_GA5(x1, x2, x3, x4, x5)  =  IF_PERM_2_IN_1_GA1(x5)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ RuleRemovalProof

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

IF_PERM_2_IN_1_GA1(delete_3_out_aga2(V, Rest)) -> PERM_2_IN_GA1(Rest)
PERM_2_IN_GA1(._22(X, Y)) -> IF_PERM_2_IN_1_GA1(delete_3_in_aga1(._22(X, Y)))

The TRS R consists of the following rules:

delete_3_in_aga1(._22(X, Y)) -> delete_3_out_aga2(X, Y)
delete_3_in_aga1(._22(F, T)) -> if_delete_3_in_1_aga2(F, delete_3_in_aga1(T))
if_delete_3_in_1_aga2(F, delete_3_out_aga2(X, R)) -> delete_3_out_aga2(X, ._22(F, R))

The set Q consists of the following terms:

delete_3_in_aga1(x0)
if_delete_3_in_1_aga2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {PERM_2_IN_GA1, IF_PERM_2_IN_1_GA1}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

IF_PERM_2_IN_1_GA1(delete_3_out_aga2(V, Rest)) -> PERM_2_IN_GA1(Rest)

Strictly oriented rules of the TRS R:

delete_3_in_aga1(._22(X, Y)) -> delete_3_out_aga2(X, Y)

Used ordering: POLO with Polynomial interpretation:

POL(._22(x1, x2)) = 1 + x1 + x2   
POL(if_delete_3_in_1_aga2(x1, x2)) = 2 + 2·x1 + x2   
POL(IF_PERM_2_IN_1_GA1(x1)) = x1   
POL(delete_3_in_aga1(x1)) = 2·x1   
POL(delete_3_out_aga2(x1, x2)) = 1 + x1 + 2·x2   
POL(PERM_2_IN_GA1(x1)) = 2·x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ RuleRemovalProof
QDP
                            ↳ RuleRemovalProof

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

PERM_2_IN_GA1(._22(X, Y)) -> IF_PERM_2_IN_1_GA1(delete_3_in_aga1(._22(X, Y)))

The TRS R consists of the following rules:

delete_3_in_aga1(._22(F, T)) -> if_delete_3_in_1_aga2(F, delete_3_in_aga1(T))
if_delete_3_in_1_aga2(F, delete_3_out_aga2(X, R)) -> delete_3_out_aga2(X, ._22(F, R))

The set Q consists of the following terms:

delete_3_in_aga1(x0)
if_delete_3_in_1_aga2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_PERM_2_IN_1_GA1, PERM_2_IN_GA1}.
By using a polynomial ordering, 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_3_in_aga1(._22(F, T)) -> if_delete_3_in_1_aga2(F, delete_3_in_aga1(T))

Used ordering: POLO with Polynomial interpretation:

POL(._22(x1, x2)) = 1 + x1 + x2   
POL(if_delete_3_in_1_aga2(x1, x2)) = 1 + x1 + x2   
POL(IF_PERM_2_IN_1_GA1(x1)) = x1   
POL(delete_3_in_aga1(x1)) = 1 + 2·x1   
POL(delete_3_out_aga2(x1, x2)) = x1 + x2   
POL(PERM_2_IN_GA1(x1)) = 1 + 2·x1   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ 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_2_IN_GA1(._22(X, Y)) -> IF_PERM_2_IN_1_GA1(delete_3_in_aga1(._22(X, Y)))

The TRS R consists of the following rules:

if_delete_3_in_1_aga2(F, delete_3_out_aga2(X, R)) -> delete_3_out_aga2(X, ._22(F, R))

The set Q consists of the following terms:

delete_3_in_aga1(x0)
if_delete_3_in_1_aga2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_PERM_2_IN_1_GA1, PERM_2_IN_GA1}.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.