(ignored inputs)COMMENT submitted by: Miguel Vitores and Salvador Lucas secret problem 2022 category: TRS
Rewrite Rules:
   [ c -> f(a,h(b)),
     f(h(f(f(a,a),h(a))),g(f(?x,g(b)))) -> c,
     c -> c,
     g(g(a)) -> f(h(g(f(c,c))),f(f(g(c),a),g(f(a,a)))),
     f(?x,?y) -> f(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ f(h(f(h(a),f(a,a))),g(f(?x,g(b)))) = c,
     f(h(f(f(a,a),h(a))),g(f(?x,g(b)))) = c,
     f(h(f(f(a,a),h(a))),g(f(g(b),?x_1))) = c ]
Outer CPs:
   [ f(a,h(b)) = c,
     c = f(g(f(?x,g(b))),h(f(f(a,a),h(a)))) ]
not Overlay, check Termination...
unknown/not Terminating
unknown Knuth & Bendix
Linear
unknown Development Closed
unknown Strongly Closed
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Upside-Parallel-Closed/Outside-Closed
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Simultaneous CPs:
   [ c = f(a,h(b)),
     f(g(f(g(b),?x)),h(f(h(a),f(a,a)))) = c,
     f(g(f(?x,g(b))),h(f(h(a),f(a,a)))) = c,
     f(g(f(g(b),?x)),h(f(f(a,a),h(a)))) = c,
     f(h(f(h(a),f(a,a))),g(f(g(b),?x))) = c,
     f(g(f(?x,g(b))),h(f(f(a,a),h(a)))) = c,
     f(h(f(h(a),f(a,a))),g(f(?x,g(b)))) = c,
     f(h(f(f(a,a),h(a))),g(f(g(b),?x))) = c,
     f(h(f(f(a,a),h(a))),g(f(?x,g(b)))) = c,
     f(a,h(b)) = c,
     c = f(g(f(?x_1,g(b))),h(f(f(a,a),h(a)))),
     c = f(h(f(h(a),f(a,a))),g(f(?x_2,g(b)))),
     c = f(h(f(f(a,a),h(a))),g(f(?x_2,g(b)))),
     c = f(h(f(f(a,a),h(a))),g(f(g(b),?x))) ]
unknown Okui (Simultaneous CPs)
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
check Locally Decreasing Diagrams by Rule Labelling...
Critical Pair <f(h(f(h(a),f(a,a))),g(f(?x,g(b)))), c> by Rules <4, 1> preceded by [(f,1),(h,1)]
 joinable by a reduction of rules <[([(f,1),(h,1)],4),([],1)], []>
Critical Pair <f(h(f(f(a,a),h(a))),g(f(?x,g(b)))), c> by Rules <4, 1> preceded by [(f,1),(h,1),(f,1)]
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <f(h(f(f(a,a),h(a))),g(f(g(b),?x_1))), c> by Rules <4, 1> preceded by [(f,2),(g,1)]
 joinable by a reduction of rules <[([(f,2),(g,1)],4),([],1)], []>
Critical Pair <c, f(a,h(b))> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <f(g(f(?x,g(b))),h(f(f(a,a),h(a)))), c> by Rules <4, 1> preceded by []
 joinable by a reduction of rules <[([],4),([],1)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 9 rules by 3 steps unfolding
obtain 52 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Ordering(rpo), check by Tree-Automata Approximation (failure)
check by Interpretation(mod2)