13.72/12.46 MAYBE 13.72/12.46 (ignored inputs)COMMENT doi:10.4230/LIPIcs.FSCD.2016.33 [36] Example 25 submitted by: Takahito Aoto and Yoshihito Toyama 13.72/12.46 Rewrite Rules: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Apply Direct Methods... 13.72/12.46 Inner CPs: 13.72/12.46 [ -(0) = 0, 13.72/12.46 -(+(-(?x_3),-(?y_3))) = +(?x_3,?y_3), 13.72/12.46 -(?x) = +(-(0),-(?x)), 13.72/12.46 -(?x_1) = +(-(?x_1),-(0)), 13.72/12.46 -(0) = +(-(1),-(-(1))), 13.72/12.46 -(0) = +(-(-(1)),-(1)), 13.72/12.46 -(+(?x_4,+(?y_4,?z_4))) = +(-(+(?x_4,?y_4)),-(?z_4)), 13.72/12.46 -(+(?y_5,?x_5)) = +(-(?x_5),-(?y_5)), 13.72/12.46 +(?x,?z_4) = +(0,+(?x,?z_4)), 13.72/12.46 +(?x_1,?z_4) = +(?x_1,+(0,?z_4)), 13.72/12.46 +(0,?z_4) = +(1,+(-(1),?z_4)), 13.72/12.46 +(0,?z_4) = +(-(1),+(1,?z_4)), 13.72/12.46 +(+(?y_5,?x_5),?z_4) = +(?x_5,+(?y_5,?z_4)), 13.72/12.46 -(?x) = -(?x), 13.72/12.46 +(+(?x,+(?y,?z)),?z_1) = +(+(?x,?y),+(?z,?z_1)) ] 13.72/12.46 Outer CPs: 13.72/12.46 [ 0 = 0, 13.72/12.46 ?x = +(?x,0), 13.72/12.46 +(?x_4,?y_4) = +(?x_4,+(?y_4,0)), 13.72/12.46 ?x_1 = +(0,?x_1), 13.72/12.46 0 = +(-(1),1), 13.72/12.46 0 = +(1,-(1)), 13.72/12.46 +(?x_4,+(?y_4,?z_4)) = +(?z_4,+(?x_4,?y_4)) ] 13.72/12.46 not Overlay, check Termination... 13.72/12.46 unknown/not Terminating 13.72/12.46 unknown Knuth & Bendix 13.72/12.46 Linear 13.72/12.46 unknown Development Closed 13.72/12.46 unknown Strongly Closed 13.72/12.46 unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow 13.72/12.46 unknown Upside-Parallel-Closed/Outside-Closed 13.72/12.46 (inner) Parallel CPs: (not computed) 13.72/12.46 unknown Toyama (Parallel CPs) 13.72/12.46 Simultaneous CPs: 13.72/12.46 [ 0 = 0, 13.72/12.46 +(?x,0) = ?x, 13.72/12.46 +(-(0),-(?x)) = -(?x), 13.72/12.46 +(0,+(?x,?z_5)) = +(?x,?z_5), 13.72/12.46 +(?x_4,+(?y_4,0)) = +(?x_4,?y_4), 13.72/12.46 +(0,?x) = ?x, 13.72/12.46 +(-(?x),-(0)) = -(?x), 13.72/12.46 +(?x,+(0,?z_5)) = +(?x,?z_5), 13.72/12.46 +(-(1),1) = 0, 13.72/12.46 +(-(1),-(-(1))) = -(0), 13.72/12.46 +(1,+(-(1),?z_4)) = +(0,?z_4), 13.72/12.46 +(1,-(1)) = 0, 13.72/12.46 +(-(-(1)),-(1)) = -(0), 13.72/12.46 +(-(1),+(1,?z_4)) = +(0,?z_4), 13.72/12.46 0 = -(0), 13.72/12.46 -(?x_1) = -(?x_1), 13.72/12.46 -(0) = 0, 13.72/12.46 -(+(-(?x_4),-(?y_4))) = +(?x_4,?y_4), 13.72/12.46 ?x_1 = -(-(?x_1)), 13.72/12.46 +(-(?x_4),-(?y_4)) = -(+(?x_4,?y_4)), 13.72/12.46 -(?y) = +(-(0),-(?y)), 13.72/12.46 -(?x) = +(-(?x),-(0)), 13.72/12.46 -(0) = +(-(1),-(-(1))), 13.72/12.46 -(0) = +(-(-(1)),-(1)), 13.72/12.46 -(+(?x_5,+(?y_5,?y))) = +(-(+(?x_5,?y_5)),-(?y)), 13.72/12.46 -(+(?y,?x)) = +(-(?x),-(?y)), 13.72/12.46 ?y = -(+(-(0),-(?y))), 13.72/12.46 ?x = -(+(-(?x),-(0))), 13.72/12.46 0 = -(+(-(1),-(-(1)))), 13.72/12.46 0 = -(+(-(-(1)),-(1))), 13.72/12.46 +(?x_5,+(?y_5,?y)) = -(+(-(+(?x_5,?y_5)),-(?y))), 13.72/12.46 +(?y,?x) = -(+(-(?x),-(?y))), 13.72/12.46 +(?x,?y) = -(+(-(?x),-(?y))), 13.72/12.46 +(?x_1,+(?y_1,?y)) = +(+(?x_1,?y_1),+(?y,0)), 13.72/12.46 ?y = +(0,+(?y,0)), 13.72/12.46 ?x = +(?x,+(0,0)), 13.72/12.46 0 = +(1,+(-(1),0)), 13.72/12.46 0 = +(-(1),+(1,0)), 13.72/12.46 +(?y,?x) = +(?x,+(?y,0)), 13.72/12.46 +(?z,+(?x_1,+(?y_1,?y))) = +(+(?x_1,?y_1),+(?y,?z)), 13.72/12.46 +(?z,?y) = +(0,+(?y,?z)), 13.72/12.46 +(?z,?x) = +(?x,+(0,?z)), 13.72/12.46 +(?z,0) = +(1,+(-(1),?z)), 13.72/12.46 +(?z,0) = +(-(1),+(1,?z)), 13.72/12.46 +(?z,+(?y,?x)) = +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) = +(?x,+(?y,0)), 13.72/12.46 +(?z,+(?x,?y)) = +(?x,+(?y,?z)), 13.72/12.46 +(+(?x_1,+(?y_1,?y)),?z) = +(+(?x_1,?y_1),+(?y,?z)), 13.72/12.46 +(?y,?z) = +(0,+(?y,?z)), 13.72/12.46 +(?x,?z) = +(?x,+(0,?z)), 13.72/12.46 +(0,?z) = +(1,+(-(1),?z)), 13.72/12.46 +(0,?z) = +(-(1),+(1,?z)), 13.72/12.46 +(+(?y,?x),?z) = +(?x,+(?y,?z)), 13.72/12.46 +(+(?x_2,+(?y_2,?y)),+(?z,?z_1)) = +(+(+(?x_2,?y_2),+(?y,?z)),?z_1), 13.72/12.46 +(?y,+(?z,?z_1)) = +(+(0,+(?y,?z)),?z_1), 13.72/12.46 +(?x,+(?z,?z_1)) = +(+(?x,+(0,?z)),?z_1), 13.72/12.46 +(0,+(?z,?z_1)) = +(+(1,+(-(1),?z)),?z_1), 13.72/12.46 +(0,+(?z,?z_1)) = +(+(-(1),+(1,?z)),?z_1), 13.72/12.46 +(+(?y,?x),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1), 13.72/12.46 +(-(+(?x_1,+(?y_1,?y))),-(?z)) = -(+(+(?x_1,?y_1),+(?y,?z))), 13.72/12.46 +(-(?y),-(?z)) = -(+(0,+(?y,?z))), 13.72/12.46 +(-(?x),-(?z)) = -(+(?x,+(0,?z))), 13.72/12.46 +(-(0),-(?z)) = -(+(1,+(-(1),?z))), 13.72/12.46 +(-(0),-(?z)) = -(+(-(1),+(1,?z))), 13.72/12.46 +(-(+(?y,?x)),-(?z)) = -(+(?x,+(?y,?z))), 13.72/12.46 +(+(?x,?y),+(?z,?z_1)) = +(+(?x,+(?y,?z)),?z_1), 13.72/12.46 +(-(+(?x,?y)),-(?z)) = -(+(?x,+(?y,?z))), 13.72/12.46 ?y = +(?y,0), 13.72/12.46 ?x = +(0,?x), 13.72/12.46 0 = +(-(1),1), 13.72/12.46 0 = +(1,-(1)), 13.72/12.46 +(?x_5,+(?y_5,?y)) = +(?y,+(?x_5,?y_5)), 13.72/12.46 +(-(?x),-(?y)) = -(+(?y,?x)), 13.72/12.46 +(?x,+(?y,?z_6)) = +(+(?y,?x),?z_6) ] 13.72/12.46 unknown Okui (Simultaneous CPs) 13.72/12.46 unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping 13.72/12.46 unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping 13.72/12.46 check Locally Decreasing Diagrams by Rule Labelling... 13.72/12.46 Critical Pair <-(0), 0> by Rules <4, 5> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[([],4)], []> 13.72/12.46 Critical Pair <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[([],6),([(+,2)],5),([(+,1)],5)], []> 13.72/12.46 joinable by a reduction of rules <[([],6),([(+,1)],5),([(+,2)],5)], []> 13.72/12.46 Critical Pair <-(?x), +(-(0),-(?x))> by Rules <0, 6> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[], [([(+,1)],4),([],0)]> 13.72/12.46 Critical Pair <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[], [([(+,2)],4),([],1)]> 13.72/12.46 Critical Pair <-(0), +(-(1),-(-(1)))> by Rules <2, 6> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[([],4)], [([(+,2)],5),([],3)]> 13.72/12.46 Critical Pair <-(0), +(-(-(1)),-(1))> by Rules <3, 6> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[([],4)], [([(+,1)],5),([],2)]> 13.72/12.46 Critical Pair <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[([],6),([(+,2)],6)], [([(+,1)],6),([],7)]> 13.72/12.46 Critical Pair <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[([],6)], [([],8)]> 13.72/12.46 Critical Pair <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7> preceded by [(+,1)] 13.72/12.46 joinable by a reduction of rules <[], [([],0)]> 13.72/12.46 Critical Pair <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7> preceded by [(+,1)] 13.72/12.46 joinable by a reduction of rules <[], [([(+,2)],0)]> 13.72/12.46 Critical Pair <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7> preceded by [(+,1)] 13.72/12.46 joinable by a reduction of rules <[([],8)], [([(+,2)],8),([],8),([],7),([(+,2)],3)]> 13.72/12.46 joinable by a reduction of rules <[([],8)], [([],8),([(+,1)],8),([],7),([(+,2)],3)]> 13.72/12.46 Critical Pair <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7> preceded by [(+,1)] 13.72/12.46 joinable by a reduction of rules <[([],8)], [([(+,2)],8),([],8),([],7),([(+,2)],2)]> 13.72/12.46 joinable by a reduction of rules <[([],8)], [([],8),([(+,1)],8),([],7),([(+,2)],2)]> 13.72/12.46 Critical Pair <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7> preceded by [(+,1)] 13.72/12.46 joinable by a reduction of rules <[([(+,1)],8),([],7)], []> 13.72/12.46 joinable by a reduction of rules <[([],7),([(+,2)],8)], [([],8),([],7)]> 13.72/12.46 Critical Pair <-(?x), -(?x)> by Rules <5, 5> preceded by [(-,1)] 13.72/12.46 joinable by a reduction of rules <[], []> 13.72/12.46 Critical Pair <+(+(?x,+(?y,?z)),?z_1), +(+(?x,?y),+(?z,?z_1))> by Rules <7, 7> preceded by [(+,1)] 13.72/12.46 joinable by a reduction of rules <[([],7),([(+,2)],7)], [([],7)]> 13.72/12.46 Critical Pair <0, 0> by Rules <1, 0> preceded by [] 13.72/12.46 joinable by a reduction of rules <[], []> 13.72/12.46 Critical Pair <+(?y_5,0), ?y_5> by Rules <8, 0> preceded by [] 13.72/12.46 joinable by a reduction of rules <[([],1)], []> 13.72/12.46 Critical Pair <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1> preceded by [] 13.72/12.46 joinable by a reduction of rules <[([(+,2)],1)], []> 13.72/12.46 Critical Pair <+(0,?x_5), ?x_5> by Rules <8, 1> preceded by [] 13.72/12.46 joinable by a reduction of rules <[([],0)], []> 13.72/12.46 Critical Pair <+(-(1),1), 0> by Rules <8, 2> preceded by [] 13.72/12.46 joinable by a reduction of rules <[([],3)], []> 13.72/12.46 Critical Pair <+(1,-(1)), 0> by Rules <8, 3> preceded by [] 13.72/12.46 joinable by a reduction of rules <[([],2)], []> 13.72/12.46 Critical Pair <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7> preceded by [] 13.72/12.46 joinable by a reduction of rules <[([],8),([],7)], []> 13.72/12.46 unknown Diagram Decreasing 13.72/12.46 check Non-Confluence... 13.72/12.46 obtain 11 rules by 3 steps unfolding 13.72/12.46 obtain 100 candidates for checking non-joinability 13.72/12.46 check by TCAP-Approximation (failure) 13.72/12.46 check by Ordering(rpo), check by Tree-Automata Approximation (failure) 13.72/12.46 check by Interpretation(mod2) (failure) 13.72/12.46 check by Descendants-Approximation, check by Ordering(poly) (failure) 13.72/12.46 unknown Non-Confluence 13.72/12.46 Check relative termination: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ] 13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Polynomial Interpretation: 13.72/12.46 +:= (2)+(1)*x1+(1)*x2 13.72/12.46 -:= (2)*x1+(2)*x1*x1 13.72/12.46 0:= 0 13.72/12.46 1:= 0 13.72/12.46 retract +(0,?x) -> ?x 13.72/12.46 retract +(?x,0) -> ?x 13.72/12.46 retract +(1,-(1)) -> 0 13.72/12.46 retract +(-(1),1) -> 0 13.72/12.46 retract -(+(?x,?y)) -> +(-(?x),-(?y)) 13.72/12.46 Polynomial Interpretation: 13.72/12.46 +:= (2)+(1)*x1+(1)*x2 13.72/12.46 -:= (1)+(2)*x1+(2)*x1*x1 13.72/12.46 0:= 0 13.72/12.46 1:= 0 13.72/12.46 relatively terminating 13.72/12.46 unknown Huet (modulo AC) 13.72/12.46 check by Reduction-Preserving Completion... 13.72/12.46 STEP: 1 (parallel) 13.72/12.46 S: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ] 13.72/12.46 P: 13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 S: terminating 13.72/12.46 CP(S,S): 13.72/12.46 <0, 0> --> <0, 0> => yes 13.72/12.46 <0, 0> --> <0, 0> => yes 13.72/12.46 <-(0), 0> --> <0, 0> => yes 13.72/12.46 <-(?x), -(?x)> --> <-(?x), -(?x)> => yes 13.72/12.46 <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> --> <+(?x_3,?y_3), +(?x_3,?y_3)> => yes 13.72/12.46 <-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes 13.72/12.46 <-(?x_1), +(-(?x_1),-(0))> --> <-(?x_1), -(?x_1)> => yes 13.72/12.46 <-(0), +(-(1),-(-(1)))> --> <0, 0> => yes 13.72/12.46 <-(0), +(-(-(1)),-(1))> --> <0, 0> => yes 13.72/12.46 PCP_in(symP,S): 13.72/12.46 <-(+(?x_3,?y_3)), +(-(?y_3),-(?x_3))> --> <+(-(?x_3),-(?y_3)), +(-(?y_3),-(?x_3))> => yes 13.72/12.46 <-(+(+(?x_2,?y_2),?z_2)), +(-(?x_2),-(+(?y_2,?z_2)))> --> <+(+(-(?x_2),-(?y_2)),-(?z_2)), +(-(?x_2),+(-(?y_2),-(?z_2)))> => yes 13.72/12.46 <-(+(?x_1,+(?y_1,?z_1))), +(-(+(?x_1,?y_1)),-(?z_1))> --> <+(-(?x_1),+(-(?y_1),-(?z_1))), +(+(-(?x_1),-(?y_1)),-(?z_1))> => yes 13.72/12.46 CP(S,symP): 13.72/12.46 <+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes 13.72/12.46 <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes 13.72/12.46 <+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes 13.72/12.46 --> => yes 13.72/12.46 <+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes 13.72/12.46 <+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes 13.72/12.46 <+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes 13.72/12.46 --> => yes 13.72/12.46 <+(0,?z), +(1,+(-(1),?z))> --> => no 13.72/12.46 <+(?x,0), +(+(?x,1),-(1))> --> => no 13.72/12.46 <0, +(-(1),1)> --> <0, 0> => yes 13.72/12.46 <+(0,?z), +(-(1),+(1,?z))> --> => no 13.72/12.46 <+(?x,0), +(+(?x,-(1)),1)> --> => no 13.72/12.46 <0, +(1,-(1))> --> <0, 0> => yes 13.72/12.46 check joinability condition: 13.72/12.46 check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable 13.72/12.46 check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable 13.72/12.46 check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable 13.72/12.46 check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable 13.72/12.46 failed 13.72/12.46 failure(Step 1) 13.72/12.46 [ ] 13.72/12.46 Added S-Rules: 13.72/12.46 [ ] 13.72/12.46 Added P-Rules: 13.72/12.46 [ ] 13.72/12.46 STEP: 2 (linear) 13.72/12.46 S: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ] 13.72/12.46 P: 13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 S: terminating 13.72/12.46 CP(S,S): 13.72/12.46 <0, 0> --> <0, 0> => yes 13.72/12.46 <0, 0> --> <0, 0> => yes 13.72/12.46 <-(0), 0> --> <0, 0> => yes 13.72/12.46 <-(?x), -(?x)> --> <-(?x), -(?x)> => yes 13.72/12.46 <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> --> <+(?x_3,?y_3), +(?x_3,?y_3)> => yes 13.72/12.46 <-(?x), +(-(0),-(?x))> --> <-(?x), -(?x)> => yes 13.72/12.46 <-(?x_1), +(-(?x_1),-(0))> --> <-(?x_1), -(?x_1)> => yes 13.72/12.46 <-(0), +(-(1),-(-(1)))> --> <0, 0> => yes 13.72/12.46 <-(0), +(-(-(1)),-(1))> --> <0, 0> => yes 13.72/12.46 CP_in(symP,S): 13.72/12.46 <-(+(?x,+(?y,?z))), +(-(+(?x,?y)),-(?z))> --> <+(-(?x),+(-(?y),-(?z))), +(+(-(?x),-(?y)),-(?z))> => yes 13.72/12.46 <-(+(+(?x,?y),?z)), +(-(?x),-(+(?y,?z)))> --> <+(+(-(?x),-(?y)),-(?z)), +(-(?x),+(-(?y),-(?z)))> => yes 13.72/12.46 <-(+(?x,?y)), +(-(?y),-(?x))> --> <+(-(?x),-(?y)), +(-(?y),-(?x))> => yes 13.72/12.46 CP(S,symP): 13.72/12.46 <+(?x,?z_1), +(0,+(?x,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes 13.72/12.46 <+(?y_1,?z_1), +(+(0,?y_1),?z_1)> --> <+(?y_1,?z_1), +(?y_1,?z_1)> => yes 13.72/12.46 <+(?x_1,?x), +(+(?x_1,0),?x)> --> <+(?x_1,?x), +(?x_1,?x)> => yes 13.72/12.46 --> => yes 13.72/12.46 <+(?x_1,?y_1), +(?x_1,+(?y_1,0))> --> <+(?x_1,?y_1), +(?x_1,?y_1)> => yes 13.72/12.46 <+(?x,?z_1), +(?x,+(0,?z_1))> --> <+(?x,?z_1), +(?x,?z_1)> => yes 13.72/12.46 <+(?x_1,?x), +(+(?x_1,?x),0)> --> <+(?x_1,?x), +(?x_1,?x)> => yes 13.72/12.46 --> => yes 13.72/12.46 <+(0,?z), +(1,+(-(1),?z))> --> => no 13.72/12.46 <+(?x,0), +(+(?x,1),-(1))> --> => no 13.72/12.46 <0, +(-(1),1)> --> <0, 0> => yes 13.72/12.46 <+(0,?z), +(-(1),+(1,?z))> --> => no 13.72/12.46 <+(?x,0), +(+(?x,-(1)),1)> --> => no 13.72/12.46 <0, +(1,-(1))> --> <0, 0> => yes 13.72/12.46 check joinability condition: 13.72/12.46 check modulo reachablity from ?z to +(1,+(-(1),?z)): maybe not reachable 13.72/12.46 check modulo reachablity from ?x to +(+(?x,1),-(1)): maybe not reachable 13.72/12.46 check modulo reachablity from ?z to +(-(1),+(1,?z)): maybe not reachable 13.72/12.46 check modulo reachablity from ?x to +(+(?x,-(1)),1): maybe not reachable 13.72/12.46 failed 13.72/12.46 failure(Step 2) 13.72/12.46 [ ] 13.72/12.46 Added S-Rules: 13.72/12.46 [ ] 13.72/12.46 Added P-Rules: 13.72/12.46 [ ] 13.72/12.46 STEP: 3 (relative) 13.72/12.46 S: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ] 13.72/12.46 P: 13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Check relative termination: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)) ] 13.72/12.46 [ +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Polynomial Interpretation: 13.72/12.46 +:= (2)+(1)*x1+(1)*x2 13.72/12.46 -:= (2)*x1+(2)*x1*x1 13.72/12.46 0:= 0 13.72/12.46 1:= 0 13.72/12.46 retract +(0,?x) -> ?x 13.72/12.46 retract +(?x,0) -> ?x 13.72/12.46 retract +(1,-(1)) -> 0 13.72/12.46 retract +(-(1),1) -> 0 13.72/12.46 retract -(+(?x,?y)) -> +(-(?x),-(?y)) 13.72/12.46 Polynomial Interpretation: 13.72/12.46 +:= (2)+(1)*x1+(1)*x2 13.72/12.46 -:= (1)+(2)*x1+(2)*x1*x1 13.72/12.46 0:= 0 13.72/12.46 1:= 0 13.72/12.46 relatively terminating 13.72/12.46 S/P: relatively terminating 13.72/12.46 check CP condition: 13.72/12.46 failed 13.72/12.46 failure(Step 3) 13.72/12.46 failure(no possibility remains) 13.72/12.46 unknown Reduction-Preserving Completion 13.72/12.46 check by Ordered Rewriting... 13.72/12.46 remove redundants rules and split 13.72/12.46 R-part: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)) ] 13.72/12.46 E-part: 13.72/12.46 [ +(?x,?y) -> +(?y,?x), 13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ] 13.72/12.46 Perform abstraction and check... 13.72/12.46 Increase tree depth and check... 13.72/12.46 Apply reduction-preserving transformation... 13.72/12.46 Rules to add: 13.72/12.46 [ +(1,+(?x_6,-(1))) -> ?x_6 ] 13.72/12.46 remove redundants rules and split 13.72/12.46 R-part: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6 ] 13.72/12.46 E-part: 13.72/12.46 [ +(?x,?y) -> +(?y,?x), 13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ] 13.72/12.46 Perform abstraction and check... 13.72/12.46 Increase tree depth and check... 13.72/12.46 Apply reduction-preserving transformation... 13.72/12.46 Rules to add: 13.72/12.46 [ +(1,+(-(1),?x_6)) -> ?x_6 ] 13.72/12.46 remove redundants rules and split 13.72/12.46 R-part: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6, 13.72/12.46 +(1,+(-(1),?x_6)) -> ?x_6 ] 13.72/12.46 E-part: 13.72/12.46 [ +(?x,?y) -> +(?y,?x), 13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ] 13.72/12.46 Perform abstraction and check... 13.72/12.46 Increase tree depth and check... 13.72/12.46 Apply reduction-preserving transformation... 13.72/12.46 Rules to add: 13.72/12.46 [ +(-(1),+(?x_8,1)) -> ?x_8 ] 13.72/12.46 remove redundants rules and split 13.72/12.46 R-part: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6, 13.72/12.46 +(1,+(-(1),?x_6)) -> ?x_6, 13.72/12.46 +(-(1),+(?x_8,1)) -> ?x_8 ] 13.72/12.46 E-part: 13.72/12.46 [ +(?x,?y) -> +(?y,?x), 13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ] 13.72/12.46 Perform abstraction and check... 13.72/12.46 Increase tree depth and check... 13.72/12.46 Apply reduction-preserving transformation... 13.72/12.46 Rules to add: 13.72/12.46 [ +(1,+(?x_9,+(?x_5,-(1)))) -> +(?x_9,?x_5) ] 13.72/12.46 remove redundants rules and split 13.72/12.46 R-part: 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(1,+(?x_6,-(1))) -> ?x_6, 13.72/12.46 +(1,+(-(1),?x_6)) -> ?x_6, 13.72/12.46 +(-(1),+(?x_8,1)) -> ?x_8, 13.72/12.46 +(1,+(?x_9,+(?x_5,-(1)))) -> +(?x_9,?x_5) ] 13.72/12.46 E-part: 13.72/12.46 [ +(?x,?y) -> +(?y,?x), 13.72/12.46 +(?x,+(?y,?z)) -> +(?y,+(?x,?z)) ] 13.72/12.46 Perform abstraction and check... 13.72/12.46 Increase tree depth and check... 13.72/12.46 unknown Confluence by Ordered Rewriting 13.72/12.46 Direct Methods: Can't judge 13.72/12.46 13.72/12.46 Try Persistent Decomposition for... 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Sort Assignment: 13.72/12.46 + : 18*18=>18 13.72/12.46 - : 18=>18 13.72/12.46 0 : =>18 13.72/12.46 1 : =>18 13.72/12.46 maximal types: {18} 13.72/12.46 Persistent Decomposition failed: Can't judge 13.72/12.46 13.72/12.46 Try Layer Preserving Decomposition for... 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Layer Preserving Decomposition failed: Can't judge 13.72/12.46 13.72/12.46 Try Commutative Decomposition for... 13.72/12.46 [ +(0,?x) -> ?x, 13.72/12.46 +(?x,0) -> ?x, 13.72/12.46 +(1,-(1)) -> 0, 13.72/12.46 +(-(1),1) -> 0, 13.72/12.46 -(0) -> 0, 13.72/12.46 -(-(?x)) -> ?x, 13.72/12.46 -(+(?x,?y)) -> +(-(?x),-(?y)), 13.72/12.46 +(+(?x,?y),?z) -> +(?x,+(?y,?z)), 13.72/12.46 +(?x,?y) -> +(?y,?x) ] 13.72/12.46 Outside Critical Pair: <0, 0> by Rules <1, 0> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{}, 0> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{}, 0> 13.72/12.46 Outside Critical Pair: <+(?y_5,0), ?y_5> by Rules <8, 0> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(0,?y_5)> 13.72/12.46 <{1}, ?y_5> 13.72/12.46 <{}, +(?y_5,0)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{}, ?y_5> 13.72/12.46 Outside Critical Pair: <+(?x_4,+(?y_4,0)), +(?x_4,?y_4)> by Rules <7, 1> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(+(0,?y_4),?x_4)> 13.72/12.46 <{1,8}, +(?y_4,?x_4)> 13.72/12.46 <{8}, +(+(?y_4,0),?x_4)> 13.72/12.46 <{8}, +(?x_4,+(0,?y_4))> 13.72/12.46 <{1}, +(?x_4,?y_4)> 13.72/12.46 <{}, +(?x_4,+(?y_4,0))> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(?y_4,?x_4)> 13.72/12.46 <{}, +(?x_4,?y_4)> 13.72/12.46 Outside Critical Pair: <+(0,?x_5), ?x_5> by Rules <8, 1> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(?x_5,0)> 13.72/12.46 <{0}, ?x_5> 13.72/12.46 <{}, +(0,?x_5)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{}, ?x_5> 13.72/12.46 Outside Critical Pair: <+(-(1),1), 0> by Rules <8, 2> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(1,-(1))> 13.72/12.46 <{3}, 0> 13.72/12.46 <{}, +(-(1),1)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{}, 0> 13.72/12.46 Outside Critical Pair: <+(1,-(1)), 0> by Rules <8, 3> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(-(1),1)> 13.72/12.46 <{2}, 0> 13.72/12.46 <{}, +(1,-(1))> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{}, 0> 13.72/12.46 Outside Critical Pair: <+(?y_5,+(?x_4,?y_4)), +(?x_4,+(?y_4,?y_5))> by Rules <8, 7> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(+(?y_4,?x_4),?y_5)> 13.72/12.46 <{8}, +(+(?x_4,?y_4),?y_5)> 13.72/12.46 <{8}, +(?y_5,+(?y_4,?x_4))> 13.72/12.46 <{}, +(?y_5,+(?x_4,?y_4))> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(+(?y_5,?y_4),?x_4)> 13.72/12.46 <{8}, +(+(?y_4,?y_5),?x_4)> 13.72/12.46 <{8}, +(?x_4,+(?y_5,?y_4))> 13.72/12.46 <{}, +(?x_4,+(?y_4,?y_5))> 13.72/12.46 Inside Critical Pair: <-(0), 0> by Rules <4, 5> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{4}, 0> 13.72/12.46 <{}, -(0)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{}, 0> 13.72/12.46 Inside Critical Pair: <-(+(-(?x_3),-(?y_3))), +(?x_3,?y_3)> by Rules <6, 5> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{6}, +(-(-(?x_3)),-(-(?y_3)))> 13.72/12.46 <{8}, -(+(-(?y_3),-(?x_3)))> 13.72/12.46 <{}, -(+(-(?x_3),-(?y_3)))> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(?y_3,?x_3)> 13.72/12.46 <{}, +(?x_3,?y_3)> 13.72/12.46 Inside Critical Pair: <-(?x), +(-(0),-(?x))> by Rules <0, 6> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{}, -(?x)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{4,8}, +(-(?x),0)> 13.72/12.46 <{8}, +(-(?x),-(0))> 13.72/12.46 <{4}, +(0,-(?x))> 13.72/12.46 <{}, +(-(0),-(?x))> 13.72/12.46 Inside Critical Pair: <-(?x_1), +(-(?x_1),-(0))> by Rules <1, 6> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{}, -(?x_1)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{4,8}, +(0,-(?x_1))> 13.72/12.46 <{8}, +(-(0),-(?x_1))> 13.72/12.46 <{4}, +(-(?x_1),0)> 13.72/12.46 <{}, +(-(?x_1),-(0))> 13.72/12.46 Inside Critical Pair: <-(0), +(-(1),-(-(1)))> by Rules <2, 6> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{4}, 0> 13.72/12.46 <{}, -(0)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{5,8}, +(1,-(1))> 13.72/12.46 <{8}, +(-(-(1)),-(1))> 13.72/12.46 <{5}, +(-(1),1)> 13.72/12.46 <{}, +(-(1),-(-(1)))> 13.72/12.46 Inside Critical Pair: <-(0), +(-(-(1)),-(1))> by Rules <3, 6> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{4}, 0> 13.72/12.46 <{}, -(0)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{5,8}, +(-(1),1)> 13.72/12.46 <{8}, +(-(1),-(-(1)))> 13.72/12.46 <{5}, +(1,-(1))> 13.72/12.46 <{}, +(-(-(1)),-(1))> 13.72/12.46 Inside Critical Pair: <-(+(?x_4,+(?y_4,?z_4))), +(-(+(?x_4,?y_4)),-(?z_4))> by Rules <7, 6> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{6,8}, +(-(?x_4),-(+(?z_4,?y_4)))> 13.72/12.46 <{6}, +(-(?x_4),-(+(?y_4,?z_4)))> 13.72/12.46 <{8}, -(+(+(?z_4,?y_4),?x_4))> 13.72/12.46 <{8}, -(+(+(?y_4,?z_4),?x_4))> 13.72/12.46 <{8}, -(+(?x_4,+(?z_4,?y_4)))> 13.72/12.46 <{}, -(+(?x_4,+(?y_4,?z_4)))> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{6,8}, +(-(?z_4),+(-(?x_4),-(?y_4)))> 13.72/12.46 <{8}, +(-(?z_4),-(+(?y_4,?x_4)))> 13.72/12.46 <{8}, +(-(?z_4),-(+(?x_4,?y_4)))> 13.72/12.46 <{6}, +(+(-(?x_4),-(?y_4)),-(?z_4))> 13.72/12.46 <{8}, +(-(+(?y_4,?x_4)),-(?z_4))> 13.72/12.46 <{}, +(-(+(?x_4,?y_4)),-(?z_4))> 13.72/12.46 Inside Critical Pair: <-(+(?y_5,?x_5)), +(-(?x_5),-(?y_5))> by Rules <8, 6> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{6}, +(-(?y_5),-(?x_5))> 13.72/12.46 <{8}, -(+(?x_5,?y_5))> 13.72/12.46 <{}, -(+(?y_5,?x_5))> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(-(?y_5),-(?x_5))> 13.72/12.46 <{}, +(-(?x_5),-(?y_5))> 13.72/12.46 Inside Critical Pair: <+(?x,?z_4), +(0,+(?x,?z_4))> by Rules <0, 7> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(?z_4,?x)> 13.72/12.46 <{}, +(?x,?z_4)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(+(?z_4,?x),0)> 13.72/12.46 <{8}, +(+(?x,?z_4),0)> 13.72/12.46 <{0,8}, +(?z_4,?x)> 13.72/12.46 <{0}, +(?x,?z_4)> 13.72/12.46 <{8}, +(0,+(?z_4,?x))> 13.72/12.46 <{}, +(0,+(?x,?z_4))> 13.72/12.46 Inside Critical Pair: <+(?x_1,?z_4), +(?x_1,+(0,?z_4))> by Rules <1, 7> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(?z_4,?x_1)> 13.72/12.46 <{}, +(?x_1,?z_4)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(+(?z_4,0),?x_1)> 13.72/12.46 <{0,8}, +(?z_4,?x_1)> 13.72/12.46 <{8}, +(+(0,?z_4),?x_1)> 13.72/12.46 <{8}, +(?x_1,+(?z_4,0))> 13.72/12.46 <{0}, +(?x_1,?z_4)> 13.72/12.46 <{}, +(?x_1,+(0,?z_4))> 13.72/12.46 Inside Critical Pair: <+(0,?z_4), +(1,+(-(1),?z_4))> by Rules <2, 7> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(?z_4,0)> 13.72/12.46 <{0}, ?z_4> 13.72/12.46 <{}, +(0,?z_4)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(+(?z_4,-(1)),1)> 13.72/12.46 <{8}, +(+(-(1),?z_4),1)> 13.72/12.46 <{8}, +(1,+(?z_4,-(1)))> 13.72/12.46 <{}, +(1,+(-(1),?z_4))> 13.72/12.46 Inside Critical Pair: <+(0,?z_4), +(-(1),+(1,?z_4))> by Rules <3, 7> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(?z_4,0)> 13.72/12.46 <{0}, ?z_4> 13.72/12.46 <{}, +(0,?z_4)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(+(?z_4,1),-(1))> 13.72/12.46 <{8}, +(+(1,?z_4),-(1))> 13.72/12.46 <{8}, +(-(1),+(?z_4,1))> 13.72/12.46 <{}, +(-(1),+(1,?z_4))> 13.72/12.46 Inside Critical Pair: <+(+(?y_5,?x_5),?z_4), +(?x_5,+(?y_5,?z_4))> by Rules <8, 7> 13.72/12.46 develop reducts from lhs term... 13.72/12.46 <{8}, +(?z_4,+(?x_5,?y_5))> 13.72/12.46 <{8}, +(?z_4,+(?y_5,?x_5))> 13.72/12.46 <{7}, +(?y_5,+(?x_5,?z_4))> 13.72/12.46 <{8}, +(+(?x_5,?y_5),?z_4)> 13.72/12.46 <{}, +(+(?y_5,?x_5),?z_4)> 13.72/12.46 develop reducts from rhs term... 13.72/12.46 <{8}, +(+(?z_4,?y_5),?x_5)> 13.72/12.46 <{8}, +(+(?y_5,?z_4),?x_5)> 13.72/12.46 <{8}, +(?x_5,+(?z_4,?y_5))> 13.72/12.46 <{}, +(?x_5,+(?y_5,?z_4))> 13.72/12.46 Commutative Decomposition failed: Can't judge 13.72/12.46 No further decomposition possible 13.72/12.46 13.72/12.46 13.72/12.46 Combined result: Can't judge 13.72/12.46 /export/starexec/sandbox/benchmark/theBenchmark.trs: Failure(unknown CR) 13.72/12.46 (5152 msec.) 13.72/12.46 EOF