Left Termination proof of /tmp/tmpQ8zC3p/cnfequiv.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

cnfequiv₂(X, Y) :- transform₂(X, Z), cnfequiv₂(Z, Y).
cnfequiv₂(X, X).
transform₂(n₁²(X), X).
transform₂(n₁(a₂(X, Y)), o₂(n₁(X), n₁(Y))).
transform₂(n₁(o₂(X, Y)), a₂(n₁(X), n₁(Y))).
transform₂(o₂(X, a₂(Y, Z)), a₂(o₂(X, Y), o₂(X, Z))).
transform₂(o₂(a₂(X, Y), Z), a₂(o₂(X, Z), o₂(Y, Z))).
transform₂(o₂(X1, Y), o₂(X2, Y)) :- transform₂(X1, X2).
transform₂(o₂(X, Y1), o₂(X, Y2)) :- transform₂(Y1, Y2).
transform₂(a₂(X1, Y), a₂(X2, Y)) :- transform₂(X1, X2).
transform₂(a₂(X, Y1), a₂(X, Y2)) :- transform₂(Y1, Y2).
transform₂(n₁(X1), n₁(X2)) :- transform₂(X1, X2).

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

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

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:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))
CNFEQUIV_2_IN_GA₂(X, Y) -> TRANSFORM_2_IN_GA₂(X, Z)
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_1_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_2_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_3_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_4_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> IF_TRANSFORM_2_IN_5_GA₃(X1, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> IF_CNFEQUIV_2_IN_2_GA₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

The argument filtering Pi contains the following mapping:
cnfequiv_2_in_ga₂(x1, x2) = cnfequiv_2_in_ga₁(x1)
n_1₁(x1) = n_1₁(x1)
a_2₂(x1, x2) = a_2₂(x1, x2)
o_2₂(x1, x2) = o_2₂(x1, x2)
if_cnfequiv_2_in_1_ga₃(x1, x2, x3) = if_cnfequiv_2_in_1_ga₁(x3)
transform_2_in_ga₂(x1, x2) = transform_2_in_ga₁(x1)
transform_2_out_ga₂(x1, x2) = transform_2_out_ga₁(x2)
if_transform_2_in_1_ga₄(x1, x2, x3, x4) = if_transform_2_in_1_ga₂(x2, x4)
if_transform_2_in_2_ga₄(x1, x2, x3, x4) = if_transform_2_in_2_ga₂(x1, x4)
if_transform_2_in_3_ga₄(x1, x2, x3, x4) = if_transform_2_in_3_ga₂(x2, x4)
if_transform_2_in_4_ga₄(x1, x2, x3, x4) = if_transform_2_in_4_ga₂(x1, x4)
if_transform_2_in_5_ga₃(x1, x2, x3) = if_transform_2_in_5_ga₁(x3)
if_cnfequiv_2_in_2_ga₄(x1, x2, x3, x4) = if_cnfequiv_2_in_2_ga₁(x4)
cnfequiv_2_out_ga₂(x1, x2) = cnfequiv_2_out_ga₁(x2)
IF_TRANSFORM_2_IN_5_GA₃(x1, x2, x3) = IF_TRANSFORM_2_IN_5_GA₁(x3)
IF_TRANSFORM_2_IN_4_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_4_GA₂(x1, x4)
IF_TRANSFORM_2_IN_2_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_2_GA₂(x1, x4)
CNFEQUIV_2_IN_GA₂(x1, x2) = CNFEQUIV_2_IN_GA₁(x1)
IF_CNFEQUIV_2_IN_2_GA₄(x1, x2, x3, x4) = IF_CNFEQUIV_2_IN_2_GA₁(x4)
TRANSFORM_2_IN_GA₂(x1, x2) = TRANSFORM_2_IN_GA₁(x1)
IF_TRANSFORM_2_IN_3_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_3_GA₂(x2, x4)
IF_TRANSFORM_2_IN_1_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_1_GA₂(x2, x4)
IF_CNFEQUIV_2_IN_1_GA₃(x1, x2, x3) = IF_CNFEQUIV_2_IN_1_GA₁(x3)

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:

CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))
CNFEQUIV_2_IN_GA₂(X, Y) -> TRANSFORM_2_IN_GA₂(X, Z)
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_1_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_2_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_3_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_4_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> IF_TRANSFORM_2_IN_5_GA₃(X1, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> IF_CNFEQUIV_2_IN_2_GA₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)

R is empty.
The argument filtering Pi contains the following mapping:
n_1₁(x1) = n_1₁(x1)
a_2₂(x1, x2) = a_2₂(x1, x2)
o_2₂(x1, x2) = o_2₂(x1, x2)
TRANSFORM_2_IN_GA₂(x1, x2) = TRANSFORM_2_IN_GA₁(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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

TRANSFORM_2_IN_GA₁(o_2₂(X1, Y)) -> TRANSFORM_2_IN_GA₁(X1)
TRANSFORM_2_IN_GA₁(a_2₂(X1, Y)) -> TRANSFORM_2_IN_GA₁(X1)
TRANSFORM_2_IN_GA₁(a_2₂(X, Y1)) -> TRANSFORM_2_IN_GA₁(Y1)
TRANSFORM_2_IN_GA₁(n_1₁(X1)) -> TRANSFORM_2_IN_GA₁(X1)
TRANSFORM_2_IN_GA₁(o_2₂(X, Y1)) -> TRANSFORM_2_IN_GA₁(Y1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {TRANSFORM_2_IN_GA₁}.
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:

TRANSFORM_2_IN_GA₁(o_2₂(X1, Y)) -> TRANSFORM_2_IN_GA₁(X1)
The graph contains the following edges 1 > 1
TRANSFORM_2_IN_GA₁(a_2₂(X1, Y)) -> TRANSFORM_2_IN_GA₁(X1)
The graph contains the following edges 1 > 1
TRANSFORM_2_IN_GA₁(a_2₂(X, Y1)) -> TRANSFORM_2_IN_GA₁(Y1)
The graph contains the following edges 1 > 1
TRANSFORM_2_IN_GA₁(n_1₁(X1)) -> TRANSFORM_2_IN_GA₁(X1)
The graph contains the following edges 1 > 1
TRANSFORM_2_IN_GA₁(o_2₂(X, Y1)) -> TRANSFORM_2_IN_GA₁(Y1)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)
CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)
CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))

The TRS R consists of the following rules:

transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))

The argument filtering Pi contains the following mapping:
n_1₁(x1) = n_1₁(x1)
a_2₂(x1, x2) = a_2₂(x1, x2)
o_2₂(x1, x2) = o_2₂(x1, x2)
transform_2_in_ga₂(x1, x2) = transform_2_in_ga₁(x1)
transform_2_out_ga₂(x1, x2) = transform_2_out_ga₁(x2)
if_transform_2_in_1_ga₄(x1, x2, x3, x4) = if_transform_2_in_1_ga₂(x2, x4)
if_transform_2_in_2_ga₄(x1, x2, x3, x4) = if_transform_2_in_2_ga₂(x1, x4)
if_transform_2_in_3_ga₄(x1, x2, x3, x4) = if_transform_2_in_3_ga₂(x2, x4)
if_transform_2_in_4_ga₄(x1, x2, x3, x4) = if_transform_2_in_4_ga₂(x1, x4)
if_transform_2_in_5_ga₃(x1, x2, x3) = if_transform_2_in_5_ga₁(x3)
CNFEQUIV_2_IN_GA₂(x1, x2) = CNFEQUIV_2_IN_GA₁(x1)
IF_CNFEQUIV_2_IN_1_GA₃(x1, x2, x3) = IF_CNFEQUIV_2_IN_1_GA₁(x3)

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

  ↳ PrologToPiTRSProof

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

IF_CNFEQUIV_2_IN_1_GA₁(transform_2_out_ga₁(Z)) -> CNFEQUIV_2_IN_GA₁(Z)
CNFEQUIV_2_IN_GA₁(X) -> IF_CNFEQUIV_2_IN_1_GA₁(transform_2_in_ga₁(X))

The TRS R consists of the following rules:

transform_2_in_ga₁(n_1₁(n_1₁(X))) -> transform_2_out_ga₁(X)
transform_2_in_ga₁(n_1₁(a_2₂(X, Y))) -> transform_2_out_ga₁(o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₁(n_1₁(o_2₂(X, Y))) -> transform_2_out_ga₁(a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₁(o_2₂(X, a_2₂(Y, Z))) -> transform_2_out_ga₁(a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₁(o_2₂(a_2₂(X, Y), Z)) -> transform_2_out_ga₁(a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₁(o_2₂(X1, Y)) -> if_transform_2_in_1_ga₂(Y, transform_2_in_ga₁(X1))
transform_2_in_ga₁(o_2₂(X, Y1)) -> if_transform_2_in_2_ga₂(X, transform_2_in_ga₁(Y1))
transform_2_in_ga₁(a_2₂(X1, Y)) -> if_transform_2_in_3_ga₂(Y, transform_2_in_ga₁(X1))
transform_2_in_ga₁(a_2₂(X, Y1)) -> if_transform_2_in_4_ga₂(X, transform_2_in_ga₁(Y1))
transform_2_in_ga₁(n_1₁(X1)) -> if_transform_2_in_5_ga₁(transform_2_in_ga₁(X1))
if_transform_2_in_1_ga₂(Y, transform_2_out_ga₁(X2)) -> transform_2_out_ga₁(o_2₂(X2, Y))
if_transform_2_in_2_ga₂(X, transform_2_out_ga₁(Y2)) -> transform_2_out_ga₁(o_2₂(X, Y2))
if_transform_2_in_3_ga₂(Y, transform_2_out_ga₁(X2)) -> transform_2_out_ga₁(a_2₂(X2, Y))
if_transform_2_in_4_ga₂(X, transform_2_out_ga₁(Y2)) -> transform_2_out_ga₁(a_2₂(X, Y2))
if_transform_2_in_5_ga₁(transform_2_out_ga₁(X2)) -> transform_2_out_ga₁(n_1₁(X2))

The set Q consists of the following terms:

transform_2_in_ga₁(x0)
if_transform_2_in_1_ga₂(x0, x1)
if_transform_2_in_2_ga₂(x0, x1)
if_transform_2_in_3_ga₂(x0, x1)
if_transform_2_in_4_ga₂(x0, x1)
if_transform_2_in_5_ga₁(x0)

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

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

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:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))
CNFEQUIV_2_IN_GA₂(X, Y) -> TRANSFORM_2_IN_GA₂(X, Z)
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_1_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_2_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_3_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_4_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> IF_TRANSFORM_2_IN_5_GA₃(X1, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> IF_CNFEQUIV_2_IN_2_GA₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

The argument filtering Pi contains the following mapping:
cnfequiv_2_in_ga₂(x1, x2) = cnfequiv_2_in_ga₁(x1)
n_1₁(x1) = n_1₁(x1)
a_2₂(x1, x2) = a_2₂(x1, x2)
o_2₂(x1, x2) = o_2₂(x1, x2)
if_cnfequiv_2_in_1_ga₃(x1, x2, x3) = if_cnfequiv_2_in_1_ga₂(x1, x3)
transform_2_in_ga₂(x1, x2) = transform_2_in_ga₁(x1)
transform_2_out_ga₂(x1, x2) = transform_2_out_ga₂(x1, x2)
if_transform_2_in_1_ga₄(x1, x2, x3, x4) = if_transform_2_in_1_ga₃(x1, x2, x4)
if_transform_2_in_2_ga₄(x1, x2, x3, x4) = if_transform_2_in_2_ga₃(x1, x2, x4)
if_transform_2_in_3_ga₄(x1, x2, x3, x4) = if_transform_2_in_3_ga₃(x1, x2, x4)
if_transform_2_in_4_ga₄(x1, x2, x3, x4) = if_transform_2_in_4_ga₃(x1, x2, x4)
if_transform_2_in_5_ga₃(x1, x2, x3) = if_transform_2_in_5_ga₂(x1, x3)
if_cnfequiv_2_in_2_ga₄(x1, x2, x3, x4) = if_cnfequiv_2_in_2_ga₂(x1, x4)
cnfequiv_2_out_ga₂(x1, x2) = cnfequiv_2_out_ga₂(x1, x2)
IF_TRANSFORM_2_IN_5_GA₃(x1, x2, x3) = IF_TRANSFORM_2_IN_5_GA₂(x1, x3)
IF_TRANSFORM_2_IN_4_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_4_GA₃(x1, x2, x4)
IF_TRANSFORM_2_IN_2_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_2_GA₃(x1, x2, x4)
CNFEQUIV_2_IN_GA₂(x1, x2) = CNFEQUIV_2_IN_GA₁(x1)
IF_CNFEQUIV_2_IN_2_GA₄(x1, x2, x3, x4) = IF_CNFEQUIV_2_IN_2_GA₂(x1, x4)
TRANSFORM_2_IN_GA₂(x1, x2) = TRANSFORM_2_IN_GA₁(x1)
IF_TRANSFORM_2_IN_3_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_3_GA₃(x1, x2, x4)
IF_TRANSFORM_2_IN_1_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_1_GA₃(x1, x2, x4)
IF_CNFEQUIV_2_IN_1_GA₃(x1, x2, x3) = IF_CNFEQUIV_2_IN_1_GA₂(x1, x3)

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:

CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))
CNFEQUIV_2_IN_GA₂(X, Y) -> TRANSFORM_2_IN_GA₂(X, Z)
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_1_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_2_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> IF_TRANSFORM_2_IN_3_GA₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> IF_TRANSFORM_2_IN_4_GA₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> IF_TRANSFORM_2_IN_5_GA₃(X1, X2, transform_2_in_ga₂(X1, X2))
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> IF_CNFEQUIV_2_IN_2_GA₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

The argument filtering Pi contains the following mapping:
cnfequiv_2_in_ga₂(x1, x2) = cnfequiv_2_in_ga₁(x1)
n_1₁(x1) = n_1₁(x1)
a_2₂(x1, x2) = a_2₂(x1, x2)
o_2₂(x1, x2) = o_2₂(x1, x2)
if_cnfequiv_2_in_1_ga₃(x1, x2, x3) = if_cnfequiv_2_in_1_ga₂(x1, x3)
transform_2_in_ga₂(x1, x2) = transform_2_in_ga₁(x1)
transform_2_out_ga₂(x1, x2) = transform_2_out_ga₂(x1, x2)
if_transform_2_in_1_ga₄(x1, x2, x3, x4) = if_transform_2_in_1_ga₃(x1, x2, x4)
if_transform_2_in_2_ga₄(x1, x2, x3, x4) = if_transform_2_in_2_ga₃(x1, x2, x4)
if_transform_2_in_3_ga₄(x1, x2, x3, x4) = if_transform_2_in_3_ga₃(x1, x2, x4)
if_transform_2_in_4_ga₄(x1, x2, x3, x4) = if_transform_2_in_4_ga₃(x1, x2, x4)
if_transform_2_in_5_ga₃(x1, x2, x3) = if_transform_2_in_5_ga₂(x1, x3)
if_cnfequiv_2_in_2_ga₄(x1, x2, x3, x4) = if_cnfequiv_2_in_2_ga₂(x1, x4)
cnfequiv_2_out_ga₂(x1, x2) = cnfequiv_2_out_ga₂(x1, x2)
IF_TRANSFORM_2_IN_5_GA₃(x1, x2, x3) = IF_TRANSFORM_2_IN_5_GA₂(x1, x3)
IF_TRANSFORM_2_IN_4_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_4_GA₃(x1, x2, x4)
IF_TRANSFORM_2_IN_2_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_2_GA₃(x1, x2, x4)
CNFEQUIV_2_IN_GA₂(x1, x2) = CNFEQUIV_2_IN_GA₁(x1)
IF_CNFEQUIV_2_IN_2_GA₄(x1, x2, x3, x4) = IF_CNFEQUIV_2_IN_2_GA₂(x1, x4)
TRANSFORM_2_IN_GA₂(x1, x2) = TRANSFORM_2_IN_GA₁(x1)
IF_TRANSFORM_2_IN_3_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_3_GA₃(x1, x2, x4)
IF_TRANSFORM_2_IN_1_GA₄(x1, x2, x3, x4) = IF_TRANSFORM_2_IN_1_GA₃(x1, x2, x4)
IF_CNFEQUIV_2_IN_1_GA₃(x1, x2, x3) = IF_CNFEQUIV_2_IN_1_GA₂(x1, x3)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

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

TRANSFORM_2_IN_GA₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)
TRANSFORM_2_IN_GA₂(n_1₁(X1), n_1₁(X2)) -> TRANSFORM_2_IN_GA₂(X1, X2)
TRANSFORM_2_IN_GA₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> TRANSFORM_2_IN_GA₂(Y1, Y2)

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

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

IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_out_ga₂(X, Z)) -> CNFEQUIV_2_IN_GA₂(Z, Y)
CNFEQUIV_2_IN_GA₂(X, Y) -> IF_CNFEQUIV_2_IN_1_GA₃(X, Y, transform_2_in_ga₂(X, Z))

The TRS R consists of the following rules:

cnfequiv_2_in_ga₂(X, Y) -> if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_in_ga₂(X, Z))
transform_2_in_ga₂(n_1₁(n_1₁(X)), X) -> transform_2_out_ga₂(n_1₁(n_1₁(X)), X)
transform_2_in_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(a_2₂(X, Y)), o_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y))) -> transform_2_out_ga₂(n_1₁(o_2₂(X, Y)), a_2₂(n_1₁(X), n_1₁(Y)))
transform_2_in_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z))) -> transform_2_out_ga₂(o_2₂(X, a_2₂(Y, Z)), a_2₂(o_2₂(X, Y), o_2₂(X, Z)))
transform_2_in_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z))) -> transform_2_out_ga₂(o_2₂(a_2₂(X, Y), Z), a_2₂(o_2₂(X, Z), o_2₂(Y, Z)))
transform_2_in_ga₂(o_2₂(X1, Y), o_2₂(X2, Y)) -> if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(o_2₂(X, Y1), o_2₂(X, Y2)) -> if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(a_2₂(X1, Y), a_2₂(X2, Y)) -> if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_in_ga₂(X1, X2))
transform_2_in_ga₂(a_2₂(X, Y1), a_2₂(X, Y2)) -> if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_in_ga₂(Y1, Y2))
transform_2_in_ga₂(n_1₁(X1), n_1₁(X2)) -> if_transform_2_in_5_ga₃(X1, X2, transform_2_in_ga₂(X1, X2))
if_transform_2_in_5_ga₃(X1, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(n_1₁(X1), n_1₁(X2))
if_transform_2_in_4_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(a_2₂(X, Y1), a_2₂(X, Y2))
if_transform_2_in_3_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(a_2₂(X1, Y), a_2₂(X2, Y))
if_transform_2_in_2_ga₄(X, Y1, Y2, transform_2_out_ga₂(Y1, Y2)) -> transform_2_out_ga₂(o_2₂(X, Y1), o_2₂(X, Y2))
if_transform_2_in_1_ga₄(X1, Y, X2, transform_2_out_ga₂(X1, X2)) -> transform_2_out_ga₂(o_2₂(X1, Y), o_2₂(X2, Y))
if_cnfequiv_2_in_1_ga₃(X, Y, transform_2_out_ga₂(X, Z)) -> if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_in_ga₂(Z, Y))
cnfequiv_2_in_ga₂(X, X) -> cnfequiv_2_out_ga₂(X, X)
if_cnfequiv_2_in_2_ga₄(X, Y, Z, cnfequiv_2_out_ga₂(Z, Y)) -> cnfequiv_2_out_ga₂(X, Y)