NO (ignored inputs)COMMENT TPDB SRS_Standard/Secret_05_SRS/matchbox1 Rewrite Rules: [ r(e(?x)) -> w(r(?x)), i(t(?x)) -> e(r(?x)), e(w(?x)) -> r(i(?x)), t(e(?x)) -> r(e(?x)), w(r(?x)) -> i(t(?x)), e(r(?x)) -> e(w(?x)), r(i(t(e(r(?x))))) -> e(w(r(i(t(e(?x)))))) ] Apply Direct Methods... Inner CPs: [ r(r(i(?x_2))) = w(r(w(?x_2))), r(e(w(?x_5))) = w(r(r(?x_5))), i(r(e(?x_3))) = e(r(e(?x_3))), e(i(t(?x_4))) = r(i(r(?x_4))), t(r(i(?x_2))) = r(e(w(?x_2))), t(e(w(?x_5))) = r(e(r(?x_5))), w(w(r(?x))) = i(t(e(?x))), w(e(w(r(i(t(e(?x_6))))))) = i(t(i(t(e(r(?x_6)))))), e(w(r(?x))) = e(w(e(?x))), e(e(w(r(i(t(e(?x_6))))))) = e(w(i(t(e(r(?x_6)))))), r(i(t(e(w(r(?x)))))) = e(w(r(i(t(e(e(?x))))))), r(e(r(e(r(?x_6))))) = e(w(r(i(t(e(?x_6)))))), r(i(r(e(r(?x_6))))) = e(w(r(i(t(e(?x_6)))))), r(i(t(e(w(?x_5))))) = e(w(r(i(t(e(?x_5)))))), r(i(t(e(e(w(r(i(t(e(?x)))))))))) = e(w(r(i(t(e(i(t(e(r(?x)))))))))) ] Outer CPs: [ ] not Overlay, check Termination... unknown/not Terminating unknown Knuth & Bendix Linear unknown Development Closed unknown Strongly Closed unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow inner CP cond (upside-parallel) innter CP Cond (outside) unknown Upside-Parallel-Closed/Outside-Closed (inner) Parallel CPs: (not computed) unknown Toyama (Parallel CPs) Simultaneous CPs: [ r(r(i(?x_3))) = w(r(w(?x_3))), r(e(w(?x_6))) = w(r(r(?x_6))), i(t(r(i(?x_3)))) = w(w(r(w(?x_3)))), i(t(e(w(?x_6)))) = w(w(r(r(?x_6)))), e(w(r(i(?x_3)))) = e(w(r(w(?x_3)))), e(w(e(w(?x_6)))) = e(w(r(r(?x_6)))), e(w(r(i(t(e(r(i(?x_3)))))))) = r(i(t(e(w(r(w(?x_3))))))), e(w(r(i(t(e(e(w(?x_6)))))))) = r(i(t(e(w(r(r(?x_6))))))), i(t(e(?x))) = w(w(r(?x))), e(w(e(?x))) = e(w(r(?x))), e(w(r(i(t(e(e(?x))))))) = r(i(t(e(w(r(?x)))))), i(r(e(?x_4))) = e(r(e(?x_4))), e(w(r(i(t(e(?x_7)))))) = r(e(r(e(r(?x_7))))), e(i(t(?x_5))) = r(i(r(?x_5))), w(r(i(t(?x_5)))) = r(r(i(r(?x_5)))), r(e(i(t(?x_5)))) = t(r(i(r(?x_5)))), w(r(w(?x))) = r(r(i(?x))), r(e(w(?x))) = t(r(i(?x))), t(r(i(?x_4))) = r(e(w(?x_4))), t(e(w(?x_6))) = r(e(r(?x_6))), e(r(r(i(?x_4)))) = i(r(e(w(?x_4)))), e(r(e(w(?x_6)))) = i(r(e(r(?x_6)))), e(r(e(?x))) = i(r(e(?x))), e(w(r(i(t(e(?x_7)))))) = r(i(r(e(r(?x_7))))), w(w(r(?x_2))) = i(t(e(?x_2))), w(e(w(r(i(t(e(?x_7))))))) = i(t(i(t(e(r(?x_7)))))), r(i(w(r(?x_2)))) = e(i(t(e(?x_2)))), r(i(e(w(r(i(t(e(?x_7)))))))) = e(i(t(i(t(e(r(?x_7))))))), r(i(r(?x))) = e(i(t(?x))), e(w(r(?x_2))) = e(w(e(?x_2))), e(e(w(r(i(t(e(?x_7))))))) = e(w(i(t(e(r(?x_7)))))), w(r(w(r(?x_2)))) = r(e(w(e(?x_2)))), w(r(e(w(r(i(t(e(?x_7)))))))) = r(e(w(i(t(e(r(?x_7))))))), r(e(w(r(?x_2)))) = t(e(w(e(?x_2)))), r(e(e(w(r(i(t(e(?x_7)))))))) = t(e(w(i(t(e(r(?x_7))))))), w(r(r(?x))) = r(e(w(?x))), r(e(r(?x))) = t(e(w(?x))), e(w(r(i(t(e(?x)))))) = r(i(t(e(w(?x))))), r(e(r(e(w(?x))))) = e(w(r(i(t(e(?x)))))), r(e(r(e(e(w(r(i(t(e(?x_1)))))))))) = e(w(r(i(t(e(i(t(e(r(?x_1)))))))))), r(e(r(e(w(r(?x_2)))))) = e(w(r(i(t(e(e(?x_2))))))), r(i(r(e(e(w(r(i(t(e(?x_1)))))))))) = e(w(r(i(t(e(i(t(e(r(?x_1)))))))))), r(i(r(e(w(r(?x_2)))))) = e(w(r(i(t(e(e(?x_2))))))), r(e(r(e(r(?x))))) = e(w(r(i(t(e(?x)))))), r(i(r(e(r(?x))))) = e(w(r(i(t(e(?x)))))), r(i(t(e(w(?x))))) = e(w(r(i(t(e(?x)))))), r(i(t(e(e(w(r(i(t(e(?x_1)))))))))) = e(w(r(i(t(e(i(t(e(r(?x_1)))))))))), r(i(t(e(w(r(?x_2)))))) = e(w(r(i(t(e(e(?x_2))))))), e(w(r(i(t(e(e(r(e(w(?x)))))))))) = r(i(t(e(e(w(r(i(t(e(?x)))))))))), e(w(r(i(t(e(e(r(e(e(w(r(i(t(e(?x_1))))))))))))))) = r(i(t(e(e(w(r(i(t(e(i(t(e(r(?x_1)))))))))))))), e(w(r(i(t(e(e(r(e(w(r(?x_2))))))))))) = r(i(t(e(e(w(r(i(t(e(e(?x_2))))))))))), e(w(r(i(t(e(i(r(e(e(w(r(i(t(e(?x_1))))))))))))))) = r(i(t(e(e(w(r(i(t(e(i(t(e(r(?x_1)))))))))))))), e(w(r(i(t(e(i(r(e(w(r(?x_2))))))))))) = r(i(t(e(e(w(r(i(t(e(e(?x_2))))))))))), i(t(e(r(e(w(?x)))))) = w(e(w(r(i(t(e(?x))))))), i(t(e(r(e(e(w(r(i(t(e(?x_1))))))))))) = w(e(w(r(i(t(e(i(t(e(r(?x_1))))))))))), i(t(e(r(e(w(r(?x_2))))))) = w(e(w(r(i(t(e(e(?x_2)))))))), i(t(i(r(e(e(w(r(i(t(e(?x_1))))))))))) = w(e(w(r(i(t(e(i(t(e(r(?x_1))))))))))), i(t(i(r(e(w(r(?x_2))))))) = w(e(w(r(i(t(e(e(?x_2)))))))), e(w(e(r(e(w(?x)))))) = e(e(w(r(i(t(e(?x))))))), e(w(e(r(e(e(w(r(i(t(e(?x_1))))))))))) = e(e(w(r(i(t(e(i(t(e(r(?x_1))))))))))), e(w(e(r(e(w(r(?x_2))))))) = e(e(w(r(i(t(e(e(?x_2)))))))), e(w(i(r(e(e(w(r(i(t(e(?x_1))))))))))) = e(e(w(r(i(t(e(i(t(e(r(?x_1))))))))))), e(w(i(r(e(w(r(?x_2))))))) = e(e(w(r(i(t(e(e(?x_2)))))))), e(w(r(i(t(e(e(r(e(r(?x)))))))))) = r(i(t(e(e(w(r(i(t(e(?x)))))))))), e(w(r(i(t(e(i(r(e(r(?x)))))))))) = r(i(t(e(e(w(r(i(t(e(?x)))))))))), e(w(r(i(t(e(i(t(e(w(?x)))))))))) = r(i(t(e(e(w(r(i(t(e(?x)))))))))), e(w(r(i(t(e(i(t(e(e(w(r(i(t(e(?x_1))))))))))))))) = r(i(t(e(e(w(r(i(t(e(i(t(e(r(?x_1)))))))))))))), e(w(r(i(t(e(i(t(e(w(r(?x_2))))))))))) = r(i(t(e(e(w(r(i(t(e(e(?x_2))))))))))), i(t(e(r(e(r(?x)))))) = w(e(w(r(i(t(e(?x))))))), i(t(i(r(e(r(?x)))))) = w(e(w(r(i(t(e(?x))))))), i(t(i(t(e(w(?x)))))) = w(e(w(r(i(t(e(?x))))))), i(t(i(t(e(e(w(r(i(t(e(?x_1))))))))))) = w(e(w(r(i(t(e(i(t(e(r(?x_1))))))))))), i(t(i(t(e(w(r(?x_2))))))) = w(e(w(r(i(t(e(e(?x_2)))))))), e(w(e(r(e(r(?x)))))) = e(e(w(r(i(t(e(?x))))))), e(w(i(r(e(r(?x)))))) = e(e(w(r(i(t(e(?x))))))), e(w(i(t(e(w(?x)))))) = e(e(w(r(i(t(e(?x))))))), e(w(i(t(e(e(w(r(i(t(e(?x_1))))))))))) = e(e(w(r(i(t(e(i(t(e(r(?x_1))))))))))), e(w(i(t(e(w(r(?x_2))))))) = e(e(w(r(i(t(e(e(?x_2)))))))), e(w(r(i(t(e(i(t(e(r(?x)))))))))) = r(i(t(e(e(w(r(i(t(e(?x)))))))))), i(t(i(t(e(r(?x)))))) = w(e(w(r(i(t(e(?x))))))), e(w(i(t(e(r(?x)))))) = e(e(w(r(i(t(e(?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 by Rules <2, 0> preceded by [(r,1)] unknown Diagram Decreasing check Non-Confluence... obtain 14 rules by 3 steps unfolding obtain 100 candidates for checking non-joinability check by TCAP-Approximation (failure) check by Ordering(rpo), check by Tree-Automata Approximation (failure) check by Interpretation(mod2) (failure) check by Descendants-Approximation, check by Ordering(poly) (success) Polynomial Interpretation: e:= (2)+(1)*x1 i:= (3)+(1)*x1 r:= (1)+(1)*x1 t:= (1)*x1 w:= (2)+(1)*x1 c_1:= (2) [r(i(?x))]-[e(w(?x))] = 0 >= 0 [e(w(?x))]-[e(r(?x))] = (1) >= 0 [i(t(?x))]-[w(r(?x))] = 0 >= 0 [e(r(?x))]-[i(t(?x))] = 0 >= 0 [w(r(?x))]-[r(e(?x))] = 0 >= 0 [e(w(r(i(t(e(?x))))))]-[r(i(t(e(r(?x)))))] = (3) >= 0 [r(e(?x))]-[t(e(?x))] = (1) >= 0 [e(e(w(c_1)))]-[r(r(i(c_1)))] = (1) > 0 (success) Witness for Non-Confluence: r(r(i(c_1)))> Direct Methods: not CR Combined result: not CR 956.trs: Success(not CR) (4647 msec.)