Left Termination of the query pattern p_in_4(g, g, g, a) w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 PiDP
↳9 UsableRulesProof (⇔)
↳10 PiDP
↳11 PiDPToQDPProof (⇐)
↳12 QDP
↳13 QDPSizeChangeProof (⇔)
↳14 YES

(0) Obligation:

Clauses:

p(M, N, s(R), RES) :- p(M, R, N, RES).
p(M, s(N), R, RES) :- p(R, N, M, RES).
p(M, X1, X2, M).

Queries:

p(g,g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

p1(T30, s(T32), s(T31), T34) :- p1(T30, T32, T31, T34).
p1(T55, T57, s(s(T56)), T59) :- p1(T57, T56, T55, T59).
p1(T76, T78, s(T77), T76).
p1(T95, s(T96), s(T97), T99) :- p1(s(T97), T96, T95, T99).
p1(T110, T111, s(T112), T110).
p1(s(T140), s(T139), T138, T142) :- p1(T138, T140, T139, T142).
p1(T165, s(s(T164)), T163, T167) :- p1(T165, T164, T163, T167).
p1(T186, s(T185), T184, T184).
p1(T193, s(T194), T195, T193).
p1(T199, T200, T201, T199).

Queries:

p1(g,g,g,a).

(3) PrologToPiTRSProof (SOUND transformation)

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

p1_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
p1_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
p1_in_ggga(T76, T78, s(T77), T76) → p1_out_ggga(T76, T78, s(T77), T76)
p1_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
p1_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
p1_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
p1_in_ggga(T186, s(T185), T184, T184) → p1_out_ggga(T186, s(T185), T184, T184)
p1_in_ggga(T193, s(T194), T195, T193) → p1_out_ggga(T193, s(T194), T195, T193)
p1_in_ggga(T199, T200, T201, T199) → p1_out_ggga(T199, T200, T201, T199)
U5_ggga(T165, T164, T163, T167, p1_out_ggga(T165, T164, T163, T167)) → p1_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, p1_out_ggga(T138, T140, T139, T142)) → p1_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, p1_out_ggga(s(T97), T96, T95, T99)) → p1_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, p1_out_ggga(T57, T56, T55, T59)) → p1_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, p1_out_ggga(T30, T32, T31, T34)) → p1_out_ggga(T30, s(T32), s(T31), T34)

The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4)  =  p1_in_ggga(x1, x2, x3)
s(x1)  =  s(x1)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
p1_out_ggga(x1, x2, x3, x4)  =  p1_out_ggga(x4)
U3_ggga(x1, x2, x3, x4, x5)  =  U3_ggga(x5)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_ggga(x5)
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

p1_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
p1_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
p1_in_ggga(T76, T78, s(T77), T76) → p1_out_ggga(T76, T78, s(T77), T76)
p1_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
p1_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
p1_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
p1_in_ggga(T186, s(T185), T184, T184) → p1_out_ggga(T186, s(T185), T184, T184)
p1_in_ggga(T193, s(T194), T195, T193) → p1_out_ggga(T193, s(T194), T195, T193)
p1_in_ggga(T199, T200, T201, T199) → p1_out_ggga(T199, T200, T201, T199)
U5_ggga(T165, T164, T163, T167, p1_out_ggga(T165, T164, T163, T167)) → p1_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, p1_out_ggga(T138, T140, T139, T142)) → p1_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, p1_out_ggga(s(T97), T96, T95, T99)) → p1_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, p1_out_ggga(T57, T56, T55, T59)) → p1_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, p1_out_ggga(T30, T32, T31, T34)) → p1_out_ggga(T30, s(T32), s(T31), T34)

The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4)  =  p1_in_ggga(x1, x2, x3)
s(x1)  =  s(x1)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
p1_out_ggga(x1, x2, x3, x4)  =  p1_out_ggga(x4)
U3_ggga(x1, x2, x3, x4, x5)  =  U3_ggga(x5)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_ggga(x5)
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x5)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

P1_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)

The TRS R consists of the following rules:

p1_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
p1_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
p1_in_ggga(T76, T78, s(T77), T76) → p1_out_ggga(T76, T78, s(T77), T76)
p1_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
p1_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
p1_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
p1_in_ggga(T186, s(T185), T184, T184) → p1_out_ggga(T186, s(T185), T184, T184)
p1_in_ggga(T193, s(T194), T195, T193) → p1_out_ggga(T193, s(T194), T195, T193)
p1_in_ggga(T199, T200, T201, T199) → p1_out_ggga(T199, T200, T201, T199)
U5_ggga(T165, T164, T163, T167, p1_out_ggga(T165, T164, T163, T167)) → p1_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, p1_out_ggga(T138, T140, T139, T142)) → p1_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, p1_out_ggga(s(T97), T96, T95, T99)) → p1_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, p1_out_ggga(T57, T56, T55, T59)) → p1_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, p1_out_ggga(T30, T32, T31, T34)) → p1_out_ggga(T30, s(T32), s(T31), T34)

The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4)  =  p1_in_ggga(x1, x2, x3)
s(x1)  =  s(x1)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
p1_out_ggga(x1, x2, x3, x4)  =  p1_out_ggga(x4)
U3_ggga(x1, x2, x3, x4, x5)  =  U3_ggga(x5)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_ggga(x5)
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x5)
P1_IN_GGGA(x1, x2, x3, x4)  =  P1_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5)  =  U1_GGGA(x5)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x5)
U3_GGGA(x1, x2, x3, x4, x5)  =  U3_GGGA(x5)
U4_GGGA(x1, x2, x3, x4, x5)  =  U4_GGGA(x5)
U5_GGGA(x1, x2, x3, x4, x5)  =  U5_GGGA(x5)

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

(6) Obligation:

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

P1_IN_GGGA(T30, s(T32), s(T31), T34) → U1_GGGA(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → U2_GGGA(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → U3_GGGA(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → U4_GGGA(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → U5_GGGA(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)

The TRS R consists of the following rules:

p1_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
p1_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
p1_in_ggga(T76, T78, s(T77), T76) → p1_out_ggga(T76, T78, s(T77), T76)
p1_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
p1_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
p1_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
p1_in_ggga(T186, s(T185), T184, T184) → p1_out_ggga(T186, s(T185), T184, T184)
p1_in_ggga(T193, s(T194), T195, T193) → p1_out_ggga(T193, s(T194), T195, T193)
p1_in_ggga(T199, T200, T201, T199) → p1_out_ggga(T199, T200, T201, T199)
U5_ggga(T165, T164, T163, T167, p1_out_ggga(T165, T164, T163, T167)) → p1_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, p1_out_ggga(T138, T140, T139, T142)) → p1_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, p1_out_ggga(s(T97), T96, T95, T99)) → p1_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, p1_out_ggga(T57, T56, T55, T59)) → p1_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, p1_out_ggga(T30, T32, T31, T34)) → p1_out_ggga(T30, s(T32), s(T31), T34)

The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4)  =  p1_in_ggga(x1, x2, x3)
s(x1)  =  s(x1)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
p1_out_ggga(x1, x2, x3, x4)  =  p1_out_ggga(x4)
U3_ggga(x1, x2, x3, x4, x5)  =  U3_ggga(x5)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_ggga(x5)
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x5)
P1_IN_GGGA(x1, x2, x3, x4)  =  P1_IN_GGGA(x1, x2, x3)
U1_GGGA(x1, x2, x3, x4, x5)  =  U1_GGGA(x5)
U2_GGGA(x1, x2, x3, x4, x5)  =  U2_GGGA(x5)
U3_GGGA(x1, x2, x3, x4, x5)  =  U3_GGGA(x5)
U4_GGGA(x1, x2, x3, x4, x5)  =  U4_GGGA(x5)
U5_GGGA(x1, x2, x3, x4, x5)  =  U5_GGGA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 5 less nodes.

(8) Obligation:

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

P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)

The TRS R consists of the following rules:

p1_in_ggga(T30, s(T32), s(T31), T34) → U1_ggga(T30, T32, T31, T34, p1_in_ggga(T30, T32, T31, T34))
p1_in_ggga(T55, T57, s(s(T56)), T59) → U2_ggga(T55, T57, T56, T59, p1_in_ggga(T57, T56, T55, T59))
p1_in_ggga(T76, T78, s(T77), T76) → p1_out_ggga(T76, T78, s(T77), T76)
p1_in_ggga(T95, s(T96), s(T97), T99) → U3_ggga(T95, T96, T97, T99, p1_in_ggga(s(T97), T96, T95, T99))
p1_in_ggga(s(T140), s(T139), T138, T142) → U4_ggga(T140, T139, T138, T142, p1_in_ggga(T138, T140, T139, T142))
p1_in_ggga(T165, s(s(T164)), T163, T167) → U5_ggga(T165, T164, T163, T167, p1_in_ggga(T165, T164, T163, T167))
p1_in_ggga(T186, s(T185), T184, T184) → p1_out_ggga(T186, s(T185), T184, T184)
p1_in_ggga(T193, s(T194), T195, T193) → p1_out_ggga(T193, s(T194), T195, T193)
p1_in_ggga(T199, T200, T201, T199) → p1_out_ggga(T199, T200, T201, T199)
U5_ggga(T165, T164, T163, T167, p1_out_ggga(T165, T164, T163, T167)) → p1_out_ggga(T165, s(s(T164)), T163, T167)
U4_ggga(T140, T139, T138, T142, p1_out_ggga(T138, T140, T139, T142)) → p1_out_ggga(s(T140), s(T139), T138, T142)
U3_ggga(T95, T96, T97, T99, p1_out_ggga(s(T97), T96, T95, T99)) → p1_out_ggga(T95, s(T96), s(T97), T99)
U2_ggga(T55, T57, T56, T59, p1_out_ggga(T57, T56, T55, T59)) → p1_out_ggga(T55, T57, s(s(T56)), T59)
U1_ggga(T30, T32, T31, T34, p1_out_ggga(T30, T32, T31, T34)) → p1_out_ggga(T30, s(T32), s(T31), T34)

The argument filtering Pi contains the following mapping:
p1_in_ggga(x1, x2, x3, x4)  =  p1_in_ggga(x1, x2, x3)
s(x1)  =  s(x1)
U1_ggga(x1, x2, x3, x4, x5)  =  U1_ggga(x5)
U2_ggga(x1, x2, x3, x4, x5)  =  U2_ggga(x5)
p1_out_ggga(x1, x2, x3, x4)  =  p1_out_ggga(x4)
U3_ggga(x1, x2, x3, x4, x5)  =  U3_ggga(x5)
U4_ggga(x1, x2, x3, x4, x5)  =  U4_ggga(x5)
U5_ggga(x1, x2, x3, x4, x5)  =  U5_ggga(x5)
P1_IN_GGGA(x1, x2, x3, x4)  =  P1_IN_GGGA(x1, x2, x3)

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

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

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

P1_IN_GGGA(T55, T57, s(s(T56)), T59) → P1_IN_GGGA(T57, T56, T55, T59)
P1_IN_GGGA(T30, s(T32), s(T31), T34) → P1_IN_GGGA(T30, T32, T31, T34)
P1_IN_GGGA(T95, s(T96), s(T97), T99) → P1_IN_GGGA(s(T97), T96, T95, T99)
P1_IN_GGGA(s(T140), s(T139), T138, T142) → P1_IN_GGGA(T138, T140, T139, T142)
P1_IN_GGGA(T165, s(s(T164)), T163, T167) → P1_IN_GGGA(T165, T164, T163, T167)

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

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

(11) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(12) Obligation:

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

P1_IN_GGGA(T55, T57, s(s(T56))) → P1_IN_GGGA(T57, T56, T55)
P1_IN_GGGA(T30, s(T32), s(T31)) → P1_IN_GGGA(T30, T32, T31)
P1_IN_GGGA(T95, s(T96), s(T97)) → P1_IN_GGGA(s(T97), T96, T95)
P1_IN_GGGA(s(T140), s(T139), T138) → P1_IN_GGGA(T138, T140, T139)
P1_IN_GGGA(T165, s(s(T164)), T163) → P1_IN_GGGA(T165, T164, T163)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • P1_IN_GGGA(T55, T57, s(s(T56))) → P1_IN_GGGA(T57, T56, T55)
    The graph contains the following edges 2 >= 1, 3 > 2, 1 >= 3

  • P1_IN_GGGA(T30, s(T32), s(T31)) → P1_IN_GGGA(T30, T32, T31)
    The graph contains the following edges 1 >= 1, 2 > 2, 3 > 3

  • P1_IN_GGGA(T95, s(T96), s(T97)) → P1_IN_GGGA(s(T97), T96, T95)
    The graph contains the following edges 3 >= 1, 2 > 2, 1 >= 3

  • P1_IN_GGGA(s(T140), s(T139), T138) → P1_IN_GGGA(T138, T140, T139)
    The graph contains the following edges 3 >= 1, 1 > 2, 2 > 3

  • P1_IN_GGGA(T165, s(s(T164)), T163) → P1_IN_GGGA(T165, T164, T163)
    The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3

(14) YES