YES
(ignored inputs)COMMENT submitted by: Kiraku Shintani secret problem 2019 category: TRS
input TRS:
   [ c(t(?x,?y,?z)) -> c(t(?y,?x,?z)),
     c(t(?x,?y,?z)) -> c(t(?x,?z,?y)),
     c(t(?x,?x,?z)) -> true ]
TRS:
   [ c(t(?x,?y,?z)) -> c(t(?y,?x,?z)),
     c(t(?x,?y,?z)) -> c(t(?x,?z,?y)),
     c(t(?x,?x,?z)) -> true ]
unknown Non-Omega-Overlapping
unknown Parallel Closed Conditional Linearization
unknown Strongly Closed Conditional Linearization
unknown Weight-Decreasing Joinable
unknown Right-Reducible
Check distinct normal forms in critical pair closure...failed
Obtained TRSs:
   [ c(t(?x,?y,?z)) -> c(t(?y,?x,?z)),
     c(t(?x,?y,?z)) -> c(t(?x,?z,?y)),
     c(t(?x,?x,?z)) -> true,
     c(t(?x_2,?z_2,?x_2)) -> true,
     c(t(?z,?x,?x)) -> true ]
unknown UNC Completion (General)
Check distinct normal forms in critical pair closure...failed
Try to prove CR of the result of UNC completion...
Rewrite Rules:
   [ c(t(?x,?y,?z)) -> c(t(?y,?x,?z)),
     c(t(?x,?y,?z)) -> c(t(?x,?z,?y)),
     c(t(?x,?x,?z)) -> true,
     c(t(?x_2,?z_2,?x_2)) -> true,
     c(t(?z,?x,?x)) -> true ]
Apply Direct Methods...
Inner CPs:
   [  ]
Outer CPs:
   [ c(t(?y,?x,?z)) = c(t(?x,?z,?y)),
     c(t(?y,?y,?z)) = true,
     c(t(?y,?z,?z)) = true,
     c(t(?z,?x,?z)) = true,
     c(t(?y_1,?z_1,?y_1)) = true,
     c(t(?z_1,?z_1,?y_1)) = true,
     c(t(?x_1,?z_1,?z_1)) = true,
     true = true,
     true = true,
     true = true ]
Overlay, check Innermost Termination...
unknown Innermost Terminating
unknown Knuth & Bendix
not Left-Linear, Right-Linear
unknown Simple-Right-Linear
unknown Weakly-Non-Overlapping & Non-Collapsing & Shallow
unknown Strongly Depth-Preserving & Root-E-Closed/Non-E-Overlapping
unknown Strongly Weight-Preserving & Root-E-Closed/Non-E-Overlapping
   [ c(t(?x,?y,?z)) -> c(t(?y,?x,?z)),
     c(t(?x_1,?y_1,?z_1)) -> c(t(?x_1,?z_1,?y_1)),
     c(t(?x_2,?x_2,?z_2)) -> true,
     c(t(?x_3,?z_3,?x_3)) -> true,
     c(t(?z_4,?x_4,?x_4)) -> true ]
Sort Assignment:
 c : 13=>20
 t : 15*15*15=>13
 true : =>20
non-linear variables: {?x_2,?x_3,?x_4}
non-linear types: {15}
types leq non-linear types: {15}
rules applicable to terms of non-linear types:
   [ ]
terms of non-linear types are innermost terminating
outer CP <p,q> = <c(t(?y:15,?x:15,?z:15)), c(t(?x:15,?z:15,?y:15))>
parallel reducts of p: {c(t(?y:15,?x:15,?z:15)),c(t(?x:15,?y:15,?z:15)),c(t(?y:15,?z:15,?x:15))}
parallel reducts of q: {c(t(?x:15,?z:15,?y:15)),c(t(?z:15,?x:15,?y:15)),c(t(?x:15,?y:15,?z:15))}
join at c(t(?x:15,?y:15,?z:15))
check subst from p
is {?x:=?y:15,?y:=?x:15,?z:=?z:15} ground inst. preserving? (yes)
check subst from q
is {?x_1:=?x:15,?y_1:=?z:15,?z_1:=?y:15} ground inst. preserving? (yes)
outer CP <p,q> = <c(t(?y:15,?y:15,?z:15)), true>
parallel reducts of p: {c(t(?y:15,?y:15,?z:15)),c(t(?y:15,?y:15,?z:15)),c(t(?y:15,?z:15,?y:15)),true}
parallel reducts of q: {true}
join at true
check subst from p
is {?x_2:=?y:15,?z_2:=?z:15} ground inst. preserving? (yes)
check subst from q
outer CP <p,q> = <c(t(?y:15,?z:15,?z:15)), true>
parallel reducts of p: {c(t(?y:15,?z:15,?z:15)),c(t(?z:15,?y:15,?z:15)),c(t(?y:15,?z:15,?z:15)),true}
parallel reducts of q: {true}
join at true
check subst from p
is {?x_4:=?z:15,?z_4:=?y:15} ground inst. preserving? (yes)
check subst from q
outer CP <p,q> = <c(t(?z:15,?x:15,?z:15)), true>
parallel reducts of p: {c(t(?z:15,?x:15,?z:15)),c(t(?x:15,?z:15,?z:15)),c(t(?z:15,?z:15,?x:15)),true}
parallel reducts of q: {true}
join at true
check subst from p
is {?x_3:=?z:15,?z_3:=?x:15} ground inst. preserving? (yes)
check subst from q
outer CP <p,q> = <c(t(?y_1:15,?z_1:15,?y_1:15)), true>
parallel reducts of p: {c(t(?y_1:15,?z_1:15,?y_1:15)),c(t(?z_1:15,?y_1:15,?y_1:15)),c(t(?y_1:15,?y_1:15,?z_1:15)),true}
parallel reducts of q: {true}
join at true
check subst from p
is {?x_3:=?y_1:15,?z_3:=?z_1:15} ground inst. preserving? (yes)
check subst from q
outer CP <p,q> = <c(t(?z_1:15,?z_1:15,?y_1:15)), true>
parallel reducts of p: {c(t(?z_1:15,?z_1:15,?y_1:15)),c(t(?z_1:15,?z_1:15,?y_1:15)),c(t(?z_1:15,?y_1:15,?z_1:15)),true}
parallel reducts of q: {true}
join at true
check subst from p
is {?x_2:=?z_1:15,?z_2:=?y_1:15} ground inst. preserving? (yes)
check subst from q
outer CP <p,q> = <c(t(?x_1:15,?z_1:15,?z_1:15)), true>
parallel reducts of p: {c(t(?x_1:15,?z_1:15,?z_1:15)),c(t(?z_1:15,?x_1:15,?z_1:15)),c(t(?x_1:15,?z_1:15,?z_1:15)),true}
parallel reducts of q: {true}
join at true
check subst from p
is {?x_4:=?z_1:15,?z_4:=?x_1:15} ground inst. preserving? (yes)
check subst from q
outer CP <p,q> = <true, true>
parallel reducts of p: {true}
parallel reducts of q: {true}
join at true
check subst from p
check subst from q
outer CP <p,q> = <true, true>
parallel reducts of p: {true}
parallel reducts of q: {true}
join at true
check subst from p
check subst from q
outer CP <p,q> = <true, true>
parallel reducts of p: {true}
parallel reducts of q: {true}
join at true
check subst from p
check subst from q
Parallel-Closed
Quasi-Left-Linear & Parallel-Closed
Direct Methods: CR

Combined result: CR
...CR proof of the result of UNC completion is successful.
problems/1133.trs: Success(UNC)
(3884 msec.)