YES

Problem 1: 


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::


Problem 1: 

Problem 1: 
Not CS-TRS Procedure:
R is not a CS-TRS

Problem 1: 
Termination Procedure:
Terminating?
YES

Problem 1: 

(VAR vu95NonEmpty vNonEmpty x)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)

Problem 1: 

Dependency Pairs Processor:
-> Pairs:
 PSharp(x) -> QSharp(Q(p(x)))
 PSharp(x) -> QSharp(p(x))
 PSharp(x) -> pSharp(x)
 QSharp(p(q(x))) -> QSharp(x)
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

SCC Processor:
-> Pairs:
 PSharp(x) -> QSharp(Q(p(x)))
 PSharp(x) -> QSharp(p(x))
 PSharp(x) -> pSharp(x)
 QSharp(p(q(x))) -> QSharp(x)
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> QSharp(x)
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> QSharp(x)
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = 2.X + 2
[p](X) = 2.X + 2
[q](X) = 2.X + 2
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X + 1
[pSharp](X) = 2.X + 1
[qSharp](X) = 2.X + 1

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> pSharp(Q(x))
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = X
[Q](X) = 2.X + 1
[p](X) = 2.X + 1
[q](X) = 2.X + 1
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = X + 2
[pSharp](X) = X + 2
[qSharp](X) = X + 2

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> QSharp(p(x))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = 2.X + 2
[p](X) = 2.X + 2
[q](X) = 2.X + 2
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X
[pSharp](X) = 2.X
[qSharp](X) = 2.X

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(Q(Q(x))) -> pSharp(x)
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = 2.X + 2
[p](X) = 2.X + 2
[q](X) = 2.X + 2
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X + 2
[pSharp](X) = 2.X + 2
[qSharp](X) = 2.X + 2

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(p(x)) -> qSharp(q(x))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = X + 2
[p](X) = X + 2
[q](X) = X + 1
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X + 2
[pSharp](X) = 2.X + 2
[qSharp](X) = 2.X

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 pSharp(p(x)) -> qSharp(x)
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = 2.X + 1
[p](X) = 2.X + 1
[q](X) = 2.X + 1
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = X + 2
[pSharp](X) = X + 2
[qSharp](X) = X + 2

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(q(x))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = 2.X + 2
[p](X) = 2.X + 2
[q](X) = 2.X + 2
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X + 2
[pSharp](X) = 2.X + 2
[qSharp](X) = 2.X + 2

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(x)
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
 qSharp(q(p(x))) -> qSharp(x)
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 Natural Numbers
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = 2.X
[Q](X) = 2.X + 2
[p](X) = 2.X + 2
[q](X) = 2.X + 2
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X + 2
[pSharp](X) = 2.X + 2
[qSharp](X) = 2.X + 2

Problem 1: 

SCC Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
->->Cycle:
->->-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
->->-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))

Problem 1: 

Reduction Pair Processor:
-> Pairs:
 QSharp(p(q(x))) -> qSharp(p(Q(x)))
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Usable rules:
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Interpretation type:
 Linear
->Coefficients:
 All rationals
->Dimension:
 1
->Bound:
 2
->Interpretation:
 
[P](X) = X
[Q](X) = 2.X + 2
[p](X) = X
[q](X) = 1/2.X
[fSNonEmpty] = 0
[PSharp](X) = 0
[QSharp](X) = 2.X + 2
[pSharp](X) = X
[qSharp](X) = 1/2.X + 1/2

Problem 1: 

SCC Processor:
-> Pairs:
 pSharp(Q(Q(x))) -> QSharp(Q(p(x)))
 qSharp(q(p(x))) -> pSharp(q(q(x)))
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
->Strongly Connected Components:
 There is no strongly connected component

The problem is finite.


Problem 1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR vNonEmpty x)
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Levy NW Procedure:
-> Rules:
 P(p(x)) -> x
 P(x) -> Q(Q(p(x)))
 Q(p(q(x))) -> q(p(Q(x)))
 Q(q(x)) -> x
 p(P(x)) -> x
 p(Q(Q(x))) -> Q(Q(p(x)))
 p(p(x)) -> q(q(x))
 q(Q(x)) -> x
 q(q(p(x))) -> p(q(q(x)))
-> Vars:
 x, x, x, x, x, x, x, x, x

-> Rlps:
 (rule: P(p(x)) -> x, id: 1, possubterms: P(p(x))->[], p(x)->[1])
 (rule: P(x) -> Q(Q(p(x))), id: 2, possubterms: P(x)->[])
 (rule: Q(p(q(x))) -> q(p(Q(x))), id: 3, possubterms: Q(p(q(x)))->[], p(q(x))->[1], q(x)->[1, 1])
 (rule: Q(q(x)) -> x, id: 4, possubterms: Q(q(x))->[], q(x)->[1])
 (rule: p(P(x)) -> x, id: 5, possubterms: p(P(x))->[], P(x)->[1])
 (rule: p(Q(Q(x))) -> Q(Q(p(x))), id: 6, possubterms: p(Q(Q(x)))->[], Q(Q(x))->[1], Q(x)->[1, 1])
 (rule: p(p(x)) -> q(q(x)), id: 7, possubterms: p(p(x))->[], p(x)->[1])
 (rule: q(Q(x)) -> x, id: 8, possubterms: q(Q(x))->[], Q(x)->[1])
 (rule: q(q(p(x))) -> p(q(q(x))), id: 9, possubterms: q(q(p(x)))->[], q(p(x))->[1], p(x)->[1, 1])

-> Unifications:
(R1 unifies with R5 at p: [1], l: P(p(x)), lp: p(x), sig: {x -> P(x')}, l': p(P(x')), r: x, r': x')
(R1 unifies with R6 at p: [1], l: P(p(x)), lp: p(x), sig: {x -> Q(Q(x'))}, l': p(Q(Q(x'))), r: x, r': Q(Q(p(x'))))
(R1 unifies with R7 at p: [1], l: P(p(x)), lp: p(x), sig: {x -> p(x')}, l': p(p(x')), r: x, r': q(q(x')))
(R2 unifies with R1 at p: [], l: P(x), lp: P(x), sig: {x -> p(x')}, l': P(p(x')), r: Q(Q(p(x))), r': x')
(R3 unifies with R8 at p: [1,1], l: Q(p(q(x))), lp: q(x), sig: {x -> Q(x')}, l': q(Q(x')), r: q(p(Q(x))), r': x')
(R3 unifies with R9 at p: [1,1], l: Q(p(q(x))), lp: q(x), sig: {x -> q(p(x'))}, l': q(q(p(x'))), r: q(p(Q(x))), r': p(q(q(x'))))
(R4 unifies with R8 at p: [1], l: Q(q(x)), lp: q(x), sig: {x -> Q(x')}, l': q(Q(x')), r: x, r': x')
(R4 unifies with R9 at p: [1], l: Q(q(x)), lp: q(x), sig: {x -> q(p(x'))}, l': q(q(p(x'))), r: x, r': p(q(q(x'))))
(R5 unifies with R1 at p: [1], l: p(P(x)), lp: P(x), sig: {x -> p(x')}, l': P(p(x')), r: x, r': x')
(R5 unifies with R2 at p: [1], l: p(P(x)), lp: P(x), sig: {x -> x'}, l': P(x'), r: x, r': Q(Q(p(x'))))
(R6 unifies with R3 at p: [1,1], l: p(Q(Q(x))), lp: Q(x), sig: {x -> p(q(x'))}, l': Q(p(q(x'))), r: Q(Q(p(x))), r': q(p(Q(x'))))
(R6 unifies with R4 at p: [1,1], l: p(Q(Q(x))), lp: Q(x), sig: {x -> q(x')}, l': Q(q(x')), r: Q(Q(p(x))), r': x')
(R7 unifies with R5 at p: [1], l: p(p(x)), lp: p(x), sig: {x -> P(x')}, l': p(P(x')), r: q(q(x)), r': x')
(R7 unifies with R6 at p: [1], l: p(p(x)), lp: p(x), sig: {x -> Q(Q(x'))}, l': p(Q(Q(x'))), r: q(q(x)), r': Q(Q(p(x'))))
(R7 unifies with R7 at p: [1], l: p(p(x)), lp: p(x), sig: {x -> p(x')}, l': p(p(x')), r: q(q(x)), r': q(q(x')))
(R8 unifies with R3 at p: [1], l: q(Q(x)), lp: Q(x), sig: {x -> p(q(x'))}, l': Q(p(q(x'))), r: x, r': q(p(Q(x'))))
(R8 unifies with R4 at p: [1], l: q(Q(x)), lp: Q(x), sig: {x -> q(x')}, l': Q(q(x')), r: x, r': x')
(R9 unifies with R5 at p: [1,1], l: q(q(p(x))), lp: p(x), sig: {x -> P(x')}, l': p(P(x')), r: p(q(q(x))), r': x')
(R9 unifies with R6 at p: [1,1], l: q(q(p(x))), lp: p(x), sig: {x -> Q(Q(x'))}, l': p(Q(Q(x'))), r: p(q(q(x))), r': Q(Q(p(x'))))
(R9 unifies with R7 at p: [1,1], l: q(q(p(x))), lp: p(x), sig: {x -> p(x')}, l': p(p(x')), r: p(q(q(x))), r': q(q(x')))

-> Critical pairs info:
<x',Q(Q(p(p(x'))))>   =>  Not trivial, Overlay, Proper, NW1, N1
<p(Q(Q(p(x')))),x'>   =>  Not trivial, Not overlay, Proper, NW1, N2
<p(Q(x')),Q(Q(p(q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N3
<Q(x'),Q(x')>   =>  Trivial, Not overlay, Proper, NW0, N4
<p(Q(q(p(Q(x'))))),Q(Q(p(p(q(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N5
<Q(p(p(q(q(x'))))),q(p(Q(q(p(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N6
<P(x'),P(x')>   =>  Trivial, Not overlay, Proper, NW0, N7
<q(q(q(q(x')))),p(q(q(p(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N8
<q(q(Q(Q(p(x'))))),p(q(q(Q(Q(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N9
<q(q(x')),p(q(q(P(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N10
<q(x'),q(x')>   =>  Trivial, Not overlay, Proper, NW0, N11
<q(q(p(Q(x')))),p(q(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N12
<p(q(q(x'))),q(q(p(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N13
<Q(p(q(q(x')))),q(p(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N14
<P(Q(Q(p(x')))),Q(Q(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N15
<p(x'),q(q(P(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N16
<p(x'),p(x')>   =>  Trivial, Not overlay, Proper, NW0, N17
<p(Q(Q(p(x')))),q(q(Q(Q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N18
<Q(p(x')),q(p(Q(Q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N19
<P(q(q(x'))),p(x')>   =>  Not trivial, Not overlay, Proper, NW0, N20

-> Problem conclusions:
 Left linear, Right linear, Linear
 Not weakly orthogonal, Not almost orthogonal, Not orthogonal
 Not Huet-Levy confluent, Not Newman confluent
 R is a TRS 



The problem is decomposed in 16 subproblems.

Problem 1.1: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<x',Q(Q(p(p(x'))))>   =>  Not trivial, Overlay, Proper, NW1, N1
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: x'
Nodes: [0]
Edges: []
ID: 0 => ('x'', D0)
t: Q(Q(p(p(x'))))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(2,3)]
ID: 0 => ('Q(Q(p(p(x'))))', D0)
ID: 1 => ('Q(Q(q(q(x'))))', D1, R7, P[1, 1], S{x10 -> x'}), NR: 'q(q(x'))'
ID: 2 => ('Q(q(x'))', D2, R4, P[1], S{x7 -> q(x')}), NR: 'q(x')'
ID: 3 => ('x'', D3, R4, P[], S{x7 -> x'}), NR: 'x''
SNodesPath: x'
TNodesPath: Q(Q(p(p(x')))) -> Q(Q(q(q(x')))) -> Q(q(x')) -> x'
x' ->* x' *<- Q(Q(p(p(x'))))
"Joinable"

The problem is confluent.

Problem 1.2: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<p(Q(Q(p(x')))),x'>   =>  Not trivial, Not overlay, Proper, NW1, N2
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: p(Q(Q(p(x'))))
Nodes: [0,1,2,3,4]
Edges: [(0,1),(1,2),(2,3),(3,4)]
ID: 0 => ('p(Q(Q(p(x'))))', D0)
ID: 1 => ('Q(Q(p(p(x'))))', D1, R6, P[], S{x9 -> p(x')}), NR: 'Q(Q(p(p(x'))))'
ID: 2 => ('Q(Q(q(q(x'))))', D2, R7, P[1, 1], S{x10 -> x'}), NR: 'q(q(x'))'
ID: 3 => ('Q(q(x'))', D3, R4, P[1], S{x7 -> q(x')}), NR: 'q(x')'
ID: 4 => ('x'', D4, R4, P[], S{x7 -> x'}), NR: 'x''
t: x'
Nodes: [0]
Edges: []
ID: 0 => ('x'', D0)
SNodesPath: p(Q(Q(p(x')))) -> Q(Q(p(p(x')))) -> Q(Q(q(q(x')))) -> Q(q(x')) -> x'
TNodesPath: x'
p(Q(Q(p(x')))) ->* x' *<- x'
"Joinable"

The problem is confluent.

Problem 1.3: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<p(Q(x')),Q(Q(p(q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N3
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: p(Q(x'))
Nodes: [0]
Edges: []
ID: 0 => ('p(Q(x'))', D0)
t: Q(Q(p(q(x'))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('Q(Q(p(q(x'))))', D0)
ID: 1 => ('Q(q(p(Q(x'))))', D1, R3, P[1], S{x6 -> x'}), NR: 'q(p(Q(x')))'
ID: 2 => ('p(Q(x'))', D2, R4, P[], S{x7 -> p(Q(x'))}), NR: 'p(Q(x'))'
SNodesPath: p(Q(x'))
TNodesPath: Q(Q(p(q(x')))) -> Q(q(p(Q(x')))) -> p(Q(x'))
p(Q(x')) ->* p(Q(x')) *<- Q(Q(p(q(x'))))
"Joinable"

The problem is confluent.

Problem 1.4: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<p(Q(q(p(Q(x'))))),Q(Q(p(p(q(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N5
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: p(Q(q(p(Q(x')))))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(2,3)]
ID: 0 => ('p(Q(q(p(Q(x')))))', D0)
ID: 1 => ('p(p(Q(x')))', D1, R4, P[1], S{x7 -> p(Q(x'))}), NR: 'p(Q(x'))'
ID: 2 => ('q(q(Q(x')))', D2, R7, P[], S{x10 -> Q(x')}), NR: 'q(q(Q(x')))'
ID: 3 => ('q(x')', D3, R8, P[1], S{x11 -> x'}), NR: 'x''
t: Q(Q(p(p(q(x')))))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(2,3)]
ID: 0 => ('Q(Q(p(p(q(x')))))', D0)
ID: 1 => ('Q(Q(q(q(q(x')))))', D1, R7, P[1, 1], S{x10 -> q(x')}), NR: 'q(q(q(x')))'
ID: 2 => ('Q(q(q(x')))', D2, R4, P[1], S{x7 -> q(q(x'))}), NR: 'q(q(x'))'
ID: 3 => ('q(x')', D3, R4, P[], S{x7 -> q(x')}), NR: 'q(x')'
SNodesPath: p(Q(q(p(Q(x'))))) -> p(p(Q(x'))) -> q(q(Q(x'))) -> q(x')
TNodesPath: Q(Q(p(p(q(x'))))) -> Q(Q(q(q(q(x'))))) -> Q(q(q(x'))) -> q(x')
p(Q(q(p(Q(x'))))) ->* q(x') *<- Q(Q(p(p(q(x')))))
"Joinable"

The problem is confluent.

Problem 1.5: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<Q(p(p(q(q(x'))))),q(p(Q(q(p(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N6
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: Q(p(p(q(q(x')))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('Q(p(p(q(q(x')))))', D0)
ID: 1 => ('Q(q(q(q(q(x')))))', D1, R7, P[1], S{x10 -> q(q(x'))}), NR: 'q(q(q(q(x'))))'
ID: 2 => ('q(q(q(x')))', D2, R4, P[], S{x7 -> q(q(q(x')))}), NR: 'q(q(q(x')))'
t: q(p(Q(q(p(x')))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('q(p(Q(q(p(x')))))', D0)
ID: 1 => ('q(p(p(x')))', D1, R4, P[1, 1], S{x7 -> p(x')}), NR: 'p(x')'
ID: 2 => ('q(q(q(x')))', D2, R7, P[1], S{x10 -> x'}), NR: 'q(q(x'))'
SNodesPath: Q(p(p(q(q(x'))))) -> Q(q(q(q(q(x'))))) -> q(q(q(x')))
TNodesPath: q(p(Q(q(p(x'))))) -> q(p(p(x'))) -> q(q(q(x')))
Q(p(p(q(q(x'))))) ->* q(q(q(x'))) *<- q(p(Q(q(p(x')))))
"Joinable"

The problem is confluent.

Problem 1.6: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<q(q(q(q(x')))),p(q(q(p(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N8
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: q(q(q(q(x'))))
Nodes: [0]
Edges: []
ID: 0 => ('q(q(q(q(x'))))', D0)
t: p(q(q(p(x'))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('p(q(q(p(x'))))', D0)
ID: 1 => ('p(p(q(q(x'))))', D1, R9, P[1], S{x12 -> x'}), NR: 'p(q(q(x')))'
ID: 2 => ('q(q(q(q(x'))))', D2, R7, P[], S{x10 -> q(q(x'))}), NR: 'q(q(q(q(x'))))'
SNodesPath: q(q(q(q(x'))))
TNodesPath: p(q(q(p(x')))) -> p(p(q(q(x')))) -> q(q(q(q(x'))))
q(q(q(q(x')))) ->* q(q(q(q(x')))) *<- p(q(q(p(x'))))
"Joinable"

The problem is confluent.

Problem 1.7: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<q(q(Q(Q(p(x'))))),p(q(q(Q(Q(x')))))>   =>  Not trivial, Not overlay, Proper, NW0, N9
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: q(q(Q(Q(p(x')))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('q(q(Q(Q(p(x')))))', D0)
ID: 1 => ('q(Q(p(x')))', D1, R8, P[1], S{x11 -> Q(p(x'))}), NR: 'Q(p(x'))'
ID: 2 => ('p(x')', D2, R8, P[], S{x11 -> p(x')}), NR: 'p(x')'
t: p(q(q(Q(Q(x')))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('p(q(q(Q(Q(x')))))', D0)
ID: 1 => ('p(q(Q(x')))', D1, R8, P[1, 1], S{x11 -> Q(x')}), NR: 'Q(x')'
ID: 2 => ('p(x')', D2, R8, P[1], S{x11 -> x'}), NR: 'x''
SNodesPath: q(q(Q(Q(p(x'))))) -> q(Q(p(x'))) -> p(x')
TNodesPath: p(q(q(Q(Q(x'))))) -> p(q(Q(x'))) -> p(x')
q(q(Q(Q(p(x'))))) ->* p(x') *<- p(q(q(Q(Q(x')))))
"Joinable"

The problem is confluent.

Problem 1.8: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<q(q(x')),p(q(q(P(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N10
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: q(q(x'))
Nodes: [0]
Edges: []
ID: 0 => ('q(q(x'))', D0)
t: p(q(q(P(x'))))
Nodes: [0,1,2,3,4]
Edges: [(0,1),(1,2),(2,3),(3,4)]
ID: 0 => ('p(q(q(P(x'))))', D0)
ID: 1 => ('p(q(q(Q(Q(p(x'))))))', D1, R2, P[1, 1, 1], S{x5 -> x'}), NR: 'Q(Q(p(x')))'
ID: 2 => ('p(q(Q(p(x'))))', D2, R8, P[1, 1], S{x11 -> Q(p(x'))}), NR: 'Q(p(x'))'
ID: 3 => ('p(p(x'))', D3, R8, P[1], S{x11 -> p(x')}), NR: 'p(x')'
ID: 4 => ('q(q(x'))', D4, R7, P[], S{x10 -> x'}), NR: 'q(q(x'))'
SNodesPath: q(q(x'))
TNodesPath: p(q(q(P(x')))) -> p(q(q(Q(Q(p(x')))))) -> p(q(Q(p(x')))) -> p(p(x')) -> q(q(x'))
q(q(x')) ->* q(q(x')) *<- p(q(q(P(x'))))
"Joinable"

The problem is confluent.

Problem 1.9: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<q(q(p(Q(x')))),p(q(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N12
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: q(q(p(Q(x'))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('q(q(p(Q(x'))))', D0)
ID: 1 => ('p(q(q(Q(x'))))', D1, R9, P[], S{x12 -> Q(x')}), NR: 'p(q(q(Q(x'))))'
ID: 2 => ('p(q(x'))', D2, R8, P[1, 1], S{x11 -> x'}), NR: 'x''
t: p(q(x'))
Nodes: [0]
Edges: []
ID: 0 => ('p(q(x'))', D0)
SNodesPath: q(q(p(Q(x')))) -> p(q(q(Q(x')))) -> p(q(x'))
TNodesPath: p(q(x'))
q(q(p(Q(x')))) ->* p(q(x')) *<- p(q(x'))
"Joinable"

The problem is confluent.

Problem 1.10: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<p(q(q(x'))),q(q(p(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N13
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: p(q(q(x')))
Nodes: [0]
Edges: []
ID: 0 => ('p(q(q(x')))', D0)
t: q(q(p(x')))
Nodes: [0,1]
Edges: [(0,1)]
ID: 0 => ('q(q(p(x')))', D0)
ID: 1 => ('p(q(q(x')))', D1, R9, P[], S{x12 -> x'}), NR: 'p(q(q(x')))'
SNodesPath: p(q(q(x')))
TNodesPath: q(q(p(x'))) -> p(q(q(x')))
p(q(q(x'))) ->* p(q(q(x'))) *<- q(q(p(x')))
"Joinable"

The problem is confluent.

Problem 1.11: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<Q(p(q(q(x')))),q(p(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N14
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: Q(p(q(q(x'))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('Q(p(q(q(x'))))', D0)
ID: 1 => ('q(p(Q(q(x'))))', D1, R3, P[], S{x6 -> q(x')}), NR: 'q(p(Q(q(x'))))'
ID: 2 => ('q(p(x'))', D2, R4, P[1, 1], S{x7 -> x'}), NR: 'x''
t: q(p(x'))
Nodes: [0]
Edges: []
ID: 0 => ('q(p(x'))', D0)
SNodesPath: Q(p(q(q(x')))) -> q(p(Q(q(x')))) -> q(p(x'))
TNodesPath: q(p(x'))
Q(p(q(q(x')))) ->* q(p(x')) *<- q(p(x'))
"Joinable"

The problem is confluent.

Problem 1.12: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<P(Q(Q(p(x')))),Q(Q(x'))>   =>  Not trivial, Not overlay, Proper, NW0, N15
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: P(Q(Q(p(x'))))
Nodes: [0,1,2,3,4,5]
Edges: [(0,1),(1,2),(2,3),(3,4),(4,5)]
ID: 0 => ('P(Q(Q(p(x'))))', D0)
ID: 1 => ('Q(Q(p(Q(Q(p(x'))))))', D1, R2, P[], S{x5 -> Q(Q(p(x')))}), NR: 'Q(Q(p(Q(Q(p(x'))))))'
ID: 2 => ('Q(Q(Q(Q(p(p(x'))))))', D2, R6, P[1, 1], S{x9 -> p(x')}), NR: 'Q(Q(p(p(x'))))'
ID: 3 => ('Q(Q(Q(Q(q(q(x'))))))', D3, R7, P[1, 1, 1, 1], S{x10 -> x'}), NR: 'q(q(x'))'
ID: 4 => ('Q(Q(Q(q(x'))))', D4, R4, P[1, 1, 1], S{x7 -> q(x')}), NR: 'q(x')'
ID: 5 => ('Q(Q(x'))', D5, R4, P[1, 1], S{x7 -> x'}), NR: 'x''
t: Q(Q(x'))
Nodes: [0]
Edges: []
ID: 0 => ('Q(Q(x'))', D0)
SNodesPath: P(Q(Q(p(x')))) -> Q(Q(p(Q(Q(p(x')))))) -> Q(Q(Q(Q(p(p(x')))))) -> Q(Q(Q(Q(q(q(x')))))) -> Q(Q(Q(q(x')))) -> Q(Q(x'))
TNodesPath: Q(Q(x'))
P(Q(Q(p(x')))) ->* Q(Q(x')) *<- Q(Q(x'))
"Joinable"

The problem is confluent.

Problem 1.13: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<p(x'),q(q(P(x')))>   =>  Not trivial, Not overlay, Proper, NW0, N16
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: p(x')
Nodes: [0]
Edges: []
ID: 0 => ('p(x')', D0)
t: q(q(P(x')))
Nodes: [0,1,2,3]
Edges: [(0,1),(1,2),(2,3)]
ID: 0 => ('q(q(P(x')))', D0)
ID: 1 => ('q(q(Q(Q(p(x')))))', D1, R2, P[1, 1], S{x5 -> x'}), NR: 'Q(Q(p(x')))'
ID: 2 => ('q(Q(p(x')))', D2, R8, P[1], S{x11 -> Q(p(x'))}), NR: 'Q(p(x'))'
ID: 3 => ('p(x')', D3, R8, P[], S{x11 -> p(x')}), NR: 'p(x')'
SNodesPath: p(x')
TNodesPath: q(q(P(x'))) -> q(q(Q(Q(p(x'))))) -> q(Q(p(x'))) -> p(x')
p(x') ->* p(x') *<- q(q(P(x')))
"Joinable"

The problem is confluent.

Problem 1.14: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<p(Q(Q(p(x')))),q(q(Q(Q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N18
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: p(Q(Q(p(x'))))
Nodes: [0,1,2,3,4]
Edges: [(0,1),(1,2),(2,3),(3,4)]
ID: 0 => ('p(Q(Q(p(x'))))', D0)
ID: 1 => ('Q(Q(p(p(x'))))', D1, R6, P[], S{x9 -> p(x')}), NR: 'Q(Q(p(p(x'))))'
ID: 2 => ('Q(Q(q(q(x'))))', D2, R7, P[1, 1], S{x10 -> x'}), NR: 'q(q(x'))'
ID: 3 => ('Q(q(x'))', D3, R4, P[1], S{x7 -> q(x')}), NR: 'q(x')'
ID: 4 => ('x'', D4, R4, P[], S{x7 -> x'}), NR: 'x''
t: q(q(Q(Q(x'))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('q(q(Q(Q(x'))))', D0)
ID: 1 => ('q(Q(x'))', D1, R8, P[1], S{x11 -> Q(x')}), NR: 'Q(x')'
ID: 2 => ('x'', D2, R8, P[], S{x11 -> x'}), NR: 'x''
SNodesPath: p(Q(Q(p(x')))) -> Q(Q(p(p(x')))) -> Q(Q(q(q(x')))) -> Q(q(x')) -> x'
TNodesPath: q(q(Q(Q(x')))) -> q(Q(x')) -> x'
p(Q(Q(p(x')))) ->* x' *<- q(q(Q(Q(x'))))
"Joinable"

The problem is confluent.

Problem 1.15: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<Q(p(x')),q(p(Q(Q(x'))))>   =>  Not trivial, Not overlay, Proper, NW0, N19
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: Q(p(x'))
Nodes: [0]
Edges: []
ID: 0 => ('Q(p(x'))', D0)
t: q(p(Q(Q(x'))))
Nodes: [0,1,2]
Edges: [(0,1),(1,2)]
ID: 0 => ('q(p(Q(Q(x'))))', D0)
ID: 1 => ('q(Q(Q(p(x'))))', D1, R6, P[1], S{x9 -> x'}), NR: 'Q(Q(p(x')))'
ID: 2 => ('Q(p(x'))', D2, R8, P[], S{x11 -> Q(p(x'))}), NR: 'Q(p(x'))'
SNodesPath: Q(p(x'))
TNodesPath: q(p(Q(Q(x')))) -> q(Q(Q(p(x')))) -> Q(p(x'))
Q(p(x')) ->* Q(p(x')) *<- q(p(Q(Q(x'))))
"Joinable"

The problem is confluent.

Problem 1.16: 
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
Confluence Problem:
(VAR x x')
(REPLACEMENT-MAP
(P 1)
(Q 1)
(p 1)
(q 1)
(fSNonEmpty)
)
(RULES
P(p(x)) -> x
P(x) -> Q(Q(p(x)))
Q(p(q(x))) -> q(p(Q(x)))
Q(q(x)) -> x
p(P(x)) -> x
p(Q(Q(x))) -> Q(Q(p(x)))
p(p(x)) -> q(q(x))
q(Q(x)) -> x
q(q(p(x))) -> p(q(q(x)))
)
Critical Pairs:
<P(q(q(x'))),p(x')>   =>  Not trivial, Not overlay, Proper, NW0, N20
Terminating:"YES"
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

Huet Brute Force Joinability Procedure:
-> Rewritings:
s: P(q(q(x')))
Nodes: [0,1,2,3,4,5]
Edges: [(0,1),(1,2),(2,3),(2,4),(3,5),(4,5)]
ID: 0 => ('P(q(q(x')))', D0)
ID: 1 => ('Q(Q(p(q(q(x')))))', D1, R2, P[], S{x5 -> q(q(x'))}), NR: 'Q(Q(p(q(q(x')))))'
ID: 2 => ('Q(q(p(Q(q(x')))))', D2, R3, P[1], S{x6 -> q(x')}), NR: 'q(p(Q(q(x'))))'
ID: 3 => ('p(Q(q(x')))', D3, R4, P[], S{x7 -> p(Q(q(x')))}), NR: 'p(Q(q(x')))'
ID: 4 => ('Q(q(p(x')))', D3, R4, P[1, 1, 1], S{x7 -> x'}), NR: 'x''
ID: 5 => ('p(x')', D4, R4, P[1], S{x7 -> x'}), NR: 'x''
t: p(x')
Nodes: [0]
Edges: []
ID: 0 => ('p(x')', D0)
SNodesPath: P(q(q(x'))) -> Q(Q(p(q(q(x'))))) -> Q(q(p(Q(q(x'))))) -> p(Q(q(x'))) -> p(x')
TNodesPath: p(x')
P(q(q(x'))) ->* p(x') *<- p(x')
"Joinable"

The problem is confluent.