Left Termination of the query pattern rem(b,f,b) w.r.t. the given Prolog program could not be shown:



PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

rem3(X, Y, R) :- notZero1(Y), sub3(X, Y, Z), rem3(Z, Y, R).
rem3(X, Y, X) :- notZero1(Y), geq2(X, Y).
sub3(s1(X), s1(Y), Z) :- sub3(X, Y, Z).
sub3(X, 00, X).
notZero1(s1(X)).
geq2(s1(X), s1(Y)) :- geq2(X, Y).
geq2(X, 00).


With regard to the inferred argument filtering the predicates were used in the following modes:
rem3: (b,f,b) (f,b,b)
sub3: (b,b,f) (f,f,f) (f,b,f)
geq2: (b,b) (f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

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

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)


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

REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)
IF_REM_3_IN_2_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_GAG3(x2, x3, x4)
SUB_3_IN_AAA3(x1, x2, x3)  =  SUB_3_IN_AAA
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
IF_REM_3_IN_5_GAG3(x1, x2, x3)  =  IF_REM_3_IN_5_GAG2(x2, x3)
IF_REM_3_IN_1_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_GAG3(x1, x3, x4)
IF_SUB_3_IN_1_AAA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AAA1(x4)
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA
IF_GEQ_2_IN_1_GG3(x1, x2, x3)  =  IF_GEQ_2_IN_1_GG1(x3)
IF_REM_3_IN_4_AGG3(x1, x2, x3)  =  IF_REM_3_IN_4_AGG3(x1, x2, x3)
IF_REM_3_IN_3_AGG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_AGG1(x5)
IF_REM_3_IN_4_GAG3(x1, x2, x3)  =  IF_REM_3_IN_4_GAG2(x1, x3)
IF_SUB_3_IN_1_AGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AGA1(x4)
SUB_3_IN_AGA3(x1, x2, x3)  =  SUB_3_IN_AGA1(x2)
GEQ_2_IN_GG2(x1, x2)  =  GEQ_2_IN_GG2(x1, x2)
REM_3_IN_GAG3(x1, x2, x3)  =  REM_3_IN_GAG2(x1, x3)
IF_GEQ_2_IN_1_AA3(x1, x2, x3)  =  IF_GEQ_2_IN_1_AA1(x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
NOTZERO_1_IN_G1(x1)  =  NOTZERO_1_IN_G1(x1)
IF_REM_3_IN_3_GAG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_GAG2(x2, x5)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)
IF_REM_3_IN_5_AGG3(x1, x2, x3)  =  IF_REM_3_IN_5_AGG1(x3)
NOTZERO_1_IN_A1(x1)  =  NOTZERO_1_IN_A
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

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

REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)
IF_REM_3_IN_2_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_GAG3(x2, x3, x4)
SUB_3_IN_AAA3(x1, x2, x3)  =  SUB_3_IN_AAA
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
IF_REM_3_IN_5_GAG3(x1, x2, x3)  =  IF_REM_3_IN_5_GAG2(x2, x3)
IF_REM_3_IN_1_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_GAG3(x1, x3, x4)
IF_SUB_3_IN_1_AAA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AAA1(x4)
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA
IF_GEQ_2_IN_1_GG3(x1, x2, x3)  =  IF_GEQ_2_IN_1_GG1(x3)
IF_REM_3_IN_4_AGG3(x1, x2, x3)  =  IF_REM_3_IN_4_AGG3(x1, x2, x3)
IF_REM_3_IN_3_AGG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_AGG1(x5)
IF_REM_3_IN_4_GAG3(x1, x2, x3)  =  IF_REM_3_IN_4_GAG2(x1, x3)
IF_SUB_3_IN_1_AGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AGA1(x4)
SUB_3_IN_AGA3(x1, x2, x3)  =  SUB_3_IN_AGA1(x2)
GEQ_2_IN_GG2(x1, x2)  =  GEQ_2_IN_GG2(x1, x2)
REM_3_IN_GAG3(x1, x2, x3)  =  REM_3_IN_GAG2(x1, x3)
IF_GEQ_2_IN_1_AA3(x1, x2, x3)  =  IF_GEQ_2_IN_1_AA1(x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
NOTZERO_1_IN_G1(x1)  =  NOTZERO_1_IN_G1(x1)
IF_REM_3_IN_3_GAG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_GAG2(x2, x5)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)
IF_REM_3_IN_5_AGG3(x1, x2, x3)  =  IF_REM_3_IN_5_AGG1(x3)
NOTZERO_1_IN_A1(x1)  =  NOTZERO_1_IN_A
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

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

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

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

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA

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
  ↳ PrologToPiTRSProof

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

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

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_1
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA

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
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

GEQ_2_IN_AA -> GEQ_2_IN_AA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {GEQ_2_IN_AA}.

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

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

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

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)
SUB_3_IN_AAA3(x1, x2, x3)  =  SUB_3_IN_AAA

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
  ↳ PrologToPiTRSProof

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

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

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

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
              ↳ PiDP
  ↳ PrologToPiTRSProof

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

SUB_3_IN_AAA -> SUB_3_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SUB_3_IN_AAA}.

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

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

REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag3(x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag2(x2, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg1(x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg1(x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag1(x2)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag2(x2, x3)
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)

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
  ↳ PrologToPiTRSProof

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

REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))

The TRS R consists of the following rules:

notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)

The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_1
0_0  =  0_0
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)

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
  ↳ PrologToPiTRSProof

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

REM_3_IN_AGG2(Y, R) -> IF_REM_3_IN_1_AGG3(Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG3(Y, R, sub_3_out_aga) -> REM_3_IN_AGG2(Y, R)
IF_REM_3_IN_1_AGG3(Y, R, notZero_1_out_g) -> IF_REM_3_IN_2_AGG3(Y, R, sub_3_in_aga1(Y))

The TRS R consists of the following rules:

notZero_1_in_g1(s_1) -> notZero_1_out_g
sub_3_in_aga1(s_1) -> if_sub_3_in_1_aga1(sub_3_in_aaa)
sub_3_in_aga1(0_0) -> sub_3_out_aga
if_sub_3_in_1_aga1(sub_3_out_aaa1(Y)) -> sub_3_out_aga
sub_3_in_aaa -> if_sub_3_in_1_aaa1(sub_3_in_aaa)
sub_3_in_aaa -> sub_3_out_aaa1(0_0)
if_sub_3_in_1_aaa1(sub_3_out_aaa1(Y)) -> sub_3_out_aaa1(s_1)

The set Q consists of the following terms:

notZero_1_in_g1(x0)
sub_3_in_aga1(x0)
if_sub_3_in_1_aga1(x0)
sub_3_in_aaa
if_sub_3_in_1_aaa1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_REM_3_IN_1_AGG3, REM_3_IN_AGG2, IF_REM_3_IN_2_AGG3}.
With regard to the inferred argument filtering the predicates were used in the following modes:
rem3: (b,f,b) (f,b,b)
sub3: (b,b,f) (f,f,f) (f,b,f)
geq2: (b,b) (f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

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

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)


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

REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)
IF_REM_3_IN_2_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_GAG4(x1, x2, x3, x4)
SUB_3_IN_AAA3(x1, x2, x3)  =  SUB_3_IN_AAA
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
IF_REM_3_IN_5_GAG3(x1, x2, x3)  =  IF_REM_3_IN_5_GAG3(x1, x2, x3)
IF_REM_3_IN_1_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_GAG3(x1, x3, x4)
IF_SUB_3_IN_1_AAA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AAA1(x4)
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA
IF_GEQ_2_IN_1_GG3(x1, x2, x3)  =  IF_GEQ_2_IN_1_GG1(x3)
IF_REM_3_IN_4_AGG3(x1, x2, x3)  =  IF_REM_3_IN_4_AGG3(x1, x2, x3)
IF_REM_3_IN_3_AGG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_AGG3(x2, x3, x5)
IF_REM_3_IN_4_GAG3(x1, x2, x3)  =  IF_REM_3_IN_4_GAG2(x1, x3)
IF_SUB_3_IN_1_AGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AGA1(x4)
SUB_3_IN_AGA3(x1, x2, x3)  =  SUB_3_IN_AGA1(x2)
GEQ_2_IN_GG2(x1, x2)  =  GEQ_2_IN_GG2(x1, x2)
REM_3_IN_GAG3(x1, x2, x3)  =  REM_3_IN_GAG2(x1, x3)
IF_GEQ_2_IN_1_AA3(x1, x2, x3)  =  IF_GEQ_2_IN_1_AA1(x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
NOTZERO_1_IN_G1(x1)  =  NOTZERO_1_IN_G1(x1)
IF_REM_3_IN_3_GAG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_GAG4(x1, x2, x3, x5)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)
IF_REM_3_IN_5_AGG3(x1, x2, x3)  =  IF_REM_3_IN_5_AGG3(x1, x2, x3)
NOTZERO_1_IN_A1(x1)  =  NOTZERO_1_IN_A
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

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

REM_3_IN_GAG3(X, Y, R) -> IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, R) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_in_gga3(X, Y, Z))
IF_REM_3_IN_1_GAG4(X, Y, R, notZero_1_out_a1(Y)) -> SUB_3_IN_GGA3(X, Y, Z)
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_GGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_GGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AAA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AAA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> IF_REM_3_IN_3_GAG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_GAG4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, R) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> SUB_3_IN_AGA3(X, Y, Z)
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> IF_SUB_3_IN_1_AGA4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
SUB_3_IN_AGA3(s_11(X), s_11(Y), Z) -> SUB_3_IN_AAA3(X, Y, Z)
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> IF_REM_3_IN_3_AGG5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
REM_3_IN_AGG3(X, Y, X) -> IF_REM_3_IN_4_AGG3(X, Y, notZero_1_in_g1(Y))
REM_3_IN_AGG3(X, Y, X) -> NOTZERO_1_IN_G1(Y)
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> IF_REM_3_IN_5_AGG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_AGG3(X, Y, notZero_1_out_g1(Y)) -> GEQ_2_IN_GG2(X, Y)
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_GG3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_GG2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> IF_GEQ_2_IN_1_AA3(X, Y, geq_2_in_aa2(X, Y))
GEQ_2_IN_AA2(s_11(X), s_11(Y)) -> GEQ_2_IN_AA2(X, Y)
REM_3_IN_GAG3(X, Y, X) -> IF_REM_3_IN_4_GAG3(X, Y, notZero_1_in_a1(Y))
REM_3_IN_GAG3(X, Y, X) -> NOTZERO_1_IN_A1(Y)
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> IF_REM_3_IN_5_GAG3(X, Y, geq_2_in_gg2(X, Y))
IF_REM_3_IN_4_GAG3(X, Y, notZero_1_out_a1(Y)) -> GEQ_2_IN_GG2(X, Y)

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)
IF_REM_3_IN_2_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_GAG4(x1, x2, x3, x4)
SUB_3_IN_AAA3(x1, x2, x3)  =  SUB_3_IN_AAA
IF_SUB_3_IN_1_GGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_GGA1(x4)
IF_REM_3_IN_5_GAG3(x1, x2, x3)  =  IF_REM_3_IN_5_GAG3(x1, x2, x3)
IF_REM_3_IN_1_GAG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_GAG3(x1, x3, x4)
IF_SUB_3_IN_1_AAA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AAA1(x4)
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA
IF_GEQ_2_IN_1_GG3(x1, x2, x3)  =  IF_GEQ_2_IN_1_GG1(x3)
IF_REM_3_IN_4_AGG3(x1, x2, x3)  =  IF_REM_3_IN_4_AGG3(x1, x2, x3)
IF_REM_3_IN_3_AGG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_AGG3(x2, x3, x5)
IF_REM_3_IN_4_GAG3(x1, x2, x3)  =  IF_REM_3_IN_4_GAG2(x1, x3)
IF_SUB_3_IN_1_AGA4(x1, x2, x3, x4)  =  IF_SUB_3_IN_1_AGA1(x4)
SUB_3_IN_AGA3(x1, x2, x3)  =  SUB_3_IN_AGA1(x2)
GEQ_2_IN_GG2(x1, x2)  =  GEQ_2_IN_GG2(x1, x2)
REM_3_IN_GAG3(x1, x2, x3)  =  REM_3_IN_GAG2(x1, x3)
IF_GEQ_2_IN_1_AA3(x1, x2, x3)  =  IF_GEQ_2_IN_1_AA1(x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
NOTZERO_1_IN_G1(x1)  =  NOTZERO_1_IN_G1(x1)
IF_REM_3_IN_3_GAG5(x1, x2, x3, x4, x5)  =  IF_REM_3_IN_3_GAG4(x1, x2, x3, x5)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)
IF_REM_3_IN_5_AGG3(x1, x2, x3)  =  IF_REM_3_IN_5_AGG3(x1, x2, x3)
NOTZERO_1_IN_A1(x1)  =  NOTZERO_1_IN_A
SUB_3_IN_GGA3(x1, x2, x3)  =  SUB_3_IN_GGA2(x1, x2)

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

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

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

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

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA

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

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

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

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

R is empty.
The argument filtering Pi contains the following mapping:
s_11(x1)  =  s_1
GEQ_2_IN_AA2(x1, x2)  =  GEQ_2_IN_AA

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

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

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

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

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)
SUB_3_IN_AAA3(x1, x2, x3)  =  SUB_3_IN_AAA

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

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

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

REM_3_IN_AGG3(X, Y, R) -> IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_in_g1(Y))
IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> REM_3_IN_AGG3(Z, Y, R)
IF_REM_3_IN_1_AGG4(X, Y, R, notZero_1_out_g1(Y)) -> IF_REM_3_IN_2_AGG4(X, Y, R, sub_3_in_aga3(X, Y, Z))

The TRS R consists of the following rules:

rem_3_in_gag3(X, Y, R) -> if_rem_3_in_1_gag4(X, Y, R, notZero_1_in_a1(Y))
notZero_1_in_a1(s_11(X)) -> notZero_1_out_a1(s_11(X))
if_rem_3_in_1_gag4(X, Y, R, notZero_1_out_a1(Y)) -> if_rem_3_in_2_gag4(X, Y, R, sub_3_in_gga3(X, Y, Z))
sub_3_in_gga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_gga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aaa4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
sub_3_in_aaa3(X, 0_0, X) -> sub_3_out_aaa3(X, 0_0, X)
if_sub_3_in_1_aaa4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aaa3(s_11(X), s_11(Y), Z)
if_sub_3_in_1_gga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_gga3(s_11(X), s_11(Y), Z)
sub_3_in_gga3(X, 0_0, X) -> sub_3_out_gga3(X, 0_0, X)
if_rem_3_in_2_gag4(X, Y, R, sub_3_out_gga3(X, Y, Z)) -> if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, R) -> if_rem_3_in_1_agg4(X, Y, R, notZero_1_in_g1(Y))
notZero_1_in_g1(s_11(X)) -> notZero_1_out_g1(s_11(X))
if_rem_3_in_1_agg4(X, Y, R, notZero_1_out_g1(Y)) -> if_rem_3_in_2_agg4(X, Y, R, sub_3_in_aga3(X, Y, Z))
sub_3_in_aga3(s_11(X), s_11(Y), Z) -> if_sub_3_in_1_aga4(X, Y, Z, sub_3_in_aaa3(X, Y, Z))
if_sub_3_in_1_aga4(X, Y, Z, sub_3_out_aaa3(X, Y, Z)) -> sub_3_out_aga3(s_11(X), s_11(Y), Z)
sub_3_in_aga3(X, 0_0, X) -> sub_3_out_aga3(X, 0_0, X)
if_rem_3_in_2_agg4(X, Y, R, sub_3_out_aga3(X, Y, Z)) -> if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_in_agg3(Z, Y, R))
rem_3_in_agg3(X, Y, X) -> if_rem_3_in_4_agg3(X, Y, notZero_1_in_g1(Y))
if_rem_3_in_4_agg3(X, Y, notZero_1_out_g1(Y)) -> if_rem_3_in_5_agg3(X, Y, geq_2_in_gg2(X, Y))
geq_2_in_gg2(s_11(X), s_11(Y)) -> if_geq_2_in_1_gg3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(s_11(X), s_11(Y)) -> if_geq_2_in_1_aa3(X, Y, geq_2_in_aa2(X, Y))
geq_2_in_aa2(X, 0_0) -> geq_2_out_aa2(X, 0_0)
if_geq_2_in_1_aa3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_aa2(s_11(X), s_11(Y))
if_geq_2_in_1_gg3(X, Y, geq_2_out_aa2(X, Y)) -> geq_2_out_gg2(s_11(X), s_11(Y))
geq_2_in_gg2(X, 0_0) -> geq_2_out_gg2(X, 0_0)
if_rem_3_in_5_agg3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_agg3(X, Y, X)
if_rem_3_in_3_agg5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_agg3(X, Y, R)
if_rem_3_in_3_gag5(X, Y, R, Z, rem_3_out_agg3(Z, Y, R)) -> rem_3_out_gag3(X, Y, R)
rem_3_in_gag3(X, Y, X) -> if_rem_3_in_4_gag3(X, Y, notZero_1_in_a1(Y))
if_rem_3_in_4_gag3(X, Y, notZero_1_out_a1(Y)) -> if_rem_3_in_5_gag3(X, Y, geq_2_in_gg2(X, Y))
if_rem_3_in_5_gag3(X, Y, geq_2_out_gg2(X, Y)) -> rem_3_out_gag3(X, Y, X)

The argument filtering Pi contains the following mapping:
rem_3_in_gag3(x1, x2, x3)  =  rem_3_in_gag2(x1, x3)
s_11(x1)  =  s_1
0_0  =  0_0
if_rem_3_in_1_gag4(x1, x2, x3, x4)  =  if_rem_3_in_1_gag3(x1, x3, x4)
notZero_1_in_a1(x1)  =  notZero_1_in_a
notZero_1_out_a1(x1)  =  notZero_1_out_a1(x1)
if_rem_3_in_2_gag4(x1, x2, x3, x4)  =  if_rem_3_in_2_gag4(x1, x2, x3, x4)
sub_3_in_gga3(x1, x2, x3)  =  sub_3_in_gga2(x1, x2)
if_sub_3_in_1_gga4(x1, x2, x3, x4)  =  if_sub_3_in_1_gga1(x4)
sub_3_in_aaa3(x1, x2, x3)  =  sub_3_in_aaa
if_sub_3_in_1_aaa4(x1, x2, x3, x4)  =  if_sub_3_in_1_aaa1(x4)
sub_3_out_aaa3(x1, x2, x3)  =  sub_3_out_aaa1(x2)
sub_3_out_gga3(x1, x2, x3)  =  sub_3_out_gga2(x1, x2)
if_rem_3_in_3_gag5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_gag4(x1, x2, x3, x5)
rem_3_in_agg3(x1, x2, x3)  =  rem_3_in_agg2(x2, x3)
if_rem_3_in_1_agg4(x1, x2, x3, x4)  =  if_rem_3_in_1_agg3(x2, x3, x4)
notZero_1_in_g1(x1)  =  notZero_1_in_g1(x1)
notZero_1_out_g1(x1)  =  notZero_1_out_g1(x1)
if_rem_3_in_2_agg4(x1, x2, x3, x4)  =  if_rem_3_in_2_agg3(x2, x3, x4)
sub_3_in_aga3(x1, x2, x3)  =  sub_3_in_aga1(x2)
if_sub_3_in_1_aga4(x1, x2, x3, x4)  =  if_sub_3_in_1_aga1(x4)
sub_3_out_aga3(x1, x2, x3)  =  sub_3_out_aga1(x2)
if_rem_3_in_3_agg5(x1, x2, x3, x4, x5)  =  if_rem_3_in_3_agg3(x2, x3, x5)
if_rem_3_in_4_agg3(x1, x2, x3)  =  if_rem_3_in_4_agg3(x1, x2, x3)
if_rem_3_in_5_agg3(x1, x2, x3)  =  if_rem_3_in_5_agg3(x1, x2, x3)
geq_2_in_gg2(x1, x2)  =  geq_2_in_gg2(x1, x2)
if_geq_2_in_1_gg3(x1, x2, x3)  =  if_geq_2_in_1_gg1(x3)
geq_2_in_aa2(x1, x2)  =  geq_2_in_aa
if_geq_2_in_1_aa3(x1, x2, x3)  =  if_geq_2_in_1_aa1(x3)
geq_2_out_aa2(x1, x2)  =  geq_2_out_aa1(x2)
geq_2_out_gg2(x1, x2)  =  geq_2_out_gg2(x1, x2)
rem_3_out_agg3(x1, x2, x3)  =  rem_3_out_agg2(x2, x3)
rem_3_out_gag3(x1, x2, x3)  =  rem_3_out_gag3(x1, x2, x3)
if_rem_3_in_4_gag3(x1, x2, x3)  =  if_rem_3_in_4_gag2(x1, x3)
if_rem_3_in_5_gag3(x1, x2, x3)  =  if_rem_3_in_5_gag3(x1, x2, x3)
REM_3_IN_AGG3(x1, x2, x3)  =  REM_3_IN_AGG2(x2, x3)
IF_REM_3_IN_2_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_2_AGG3(x2, x3, x4)
IF_REM_3_IN_1_AGG4(x1, x2, x3, x4)  =  IF_REM_3_IN_1_AGG3(x2, x3, x4)

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