YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ or(?x,T) -> T,
     or(?x,F) -> ?x,
     or(T,?x) -> T,
     or(F,?x) -> ?x,
     or(or(?x,?y),?z) -> or(?x,or(?y,?z)),
     or(?x,?y) -> or(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ or(T,?z_4) = or(?x,or(T,?z_4)),
     or(?x_1,?z_4) = or(?x_1,or(F,?z_4)),
     or(T,?z_4) = or(T,or(?x_2,?z_4)),
     or(?x_3,?z_4) = or(F,or(?x_3,?z_4)),
     or(or(?y_5,?x_5),?z_4) = or(?x_5,or(?y_5,?z_4)),
     or(or(?x,or(?y,?z)),?z_1) = or(or(?x,?y),or(?z,?z_1)) ]
Outer CPs:
   [ T = T,
     T = T,
     T = or(?x_4,or(?y_4,T)),
     T = or(T,?x),
     T = T,
     F = F,
     or(?x_4,?y_4) = or(?x_4,or(?y_4,F)),
     ?x_1 = or(F,?x_1),
     T = or(?x_2,T),
     ?x_3 = or(?x_3,F),
     or(?x_4,or(?y_4,?z_4)) = or(?z_4,or(?x_4,?y_4)) ]
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:
   [ T = T,
     or(?x_4,or(?y_4,T)) = T,
     or(T,?x) = T,
     or(?x,or(T,?z_5)) = or(T,?z_5),
     F = F,
     or(?x_4,or(?y_4,F)) = or(?x_4,?y_4),
     or(F,?x) = ?x,
     or(?x,or(F,?z_5)) = or(?x,?z_5),
     or(?x,T) = T,
     or(T,or(?x,?z_5)) = or(T,?z_5),
     or(?x,F) = ?x,
     or(F,or(?x,?z_5)) = or(?x,?z_5),
     T = or(or(?x_1,?y_1),or(?y,T)),
     T = or(?x,or(T,T)),
     T = or(?x,or(F,T)),
     T = or(T,or(?y,T)),
     T = or(F,or(?y,T)),
     T = or(?x,or(?y,T)),
     or(?x_1,or(?y_1,?y)) = or(or(?x_1,?y_1),or(?y,F)),
     T = or(?x,or(T,F)),
     ?x = or(?x,or(F,F)),
     T = or(T,or(?y,F)),
     ?y = or(F,or(?y,F)),
     or(?y,?x) = or(?x,or(?y,F)),
     or(?z,or(?x_1,or(?y_1,?y))) = or(or(?x_1,?y_1),or(?y,?z)),
     or(?z,T) = or(?x,or(T,?z)),
     or(?z,?x) = or(?x,or(F,?z)),
     or(?z,T) = or(T,or(?y,?z)),
     or(?z,?y) = or(F,or(?y,?z)),
     or(?z,or(?y,?x)) = or(?x,or(?y,?z)),
     or(?x,?y) = or(?x,or(?y,F)),
     or(?z,or(?x,?y)) = or(?x,or(?y,?z)),
     or(or(?x_1,or(?y_1,?y)),?z) = or(or(?x_1,?y_1),or(?y,?z)),
     or(T,?z) = or(?x,or(T,?z)),
     or(?x,?z) = or(?x,or(F,?z)),
     or(T,?z) = or(T,or(?y,?z)),
     or(?y,?z) = or(F,or(?y,?z)),
     or(or(?y,?x),?z) = or(?x,or(?y,?z)),
     or(or(?x_2,or(?y_2,?y)),or(?z,?z_1)) = or(or(or(?x_2,?y_2),or(?y,?z)),?z_1),
     or(T,or(?z,?z_1)) = or(or(?x,or(T,?z)),?z_1),
     or(?x,or(?z,?z_1)) = or(or(?x,or(F,?z)),?z_1),
     or(T,or(?z,?z_1)) = or(or(T,or(?y,?z)),?z_1),
     or(?y,or(?z,?z_1)) = or(or(F,or(?y,?z)),?z_1),
     or(or(?y,?x),or(?z,?z_1)) = or(or(?x,or(?y,?z)),?z_1),
     or(or(?x,?y),or(?z,?z_1)) = or(or(?x,or(?y,?z)),?z_1),
     T = or(T,?x),
     ?x = or(F,?x),
     T = or(?y,T),
     ?y = or(?y,F),
     or(?x_5,or(?y_5,?y)) = or(?y,or(?x_5,?y_5)),
     or(?x,or(?y,?z_6)) = or(or(?y,?x),?z_6) ]
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 <or(T,?z_4), or(?x,or(T,?z_4))> by Rules <0, 4> preceded by [(or,1)]
 joinable by a reduction of rules <[([],2)], [([(or,2)],2),([],0)]>
 joinable by a reduction of rules <[([],5),([],0)], [([(or,2)],2),([],0)]>
Critical Pair <or(?x_1,?z_4), or(?x_1,or(F,?z_4))> by Rules <1, 4> preceded by [(or,1)]
 joinable by a reduction of rules <[], [([(or,2)],3)]>
Critical Pair <or(T,?z_4), or(T,or(?x_2,?z_4))> by Rules <2, 4> preceded by [(or,1)]
 joinable by a reduction of rules <[([],2)], [([],2)]>
Critical Pair <or(?x_3,?z_4), or(F,or(?x_3,?z_4))> by Rules <3, 4> preceded by [(or,1)]
 joinable by a reduction of rules <[], [([],3)]>
Critical Pair <or(or(?y_5,?x_5),?z_4), or(?x_5,or(?y_5,?z_4))> by Rules <5, 4> preceded by [(or,1)]
 joinable by a reduction of rules <[([(or,1)],5),([],4)], []>
 joinable by a reduction of rules <[([],4),([(or,2)],5)], [([],5),([],4)]>
Critical Pair <or(or(?x,or(?y,?z)),?z_1), or(or(?x,?y),or(?z,?z_1))> by Rules <4, 4> preceded by [(or,1)]
 joinable by a reduction of rules <[([],4),([(or,2)],4)], [([],4)]>
Critical Pair <T, T> by Rules <2, 0> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <T, T> by Rules <3, 0> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <or(?x_4,or(?y_4,T)), T> by Rules <4, 0> preceded by []
 joinable by a reduction of rules <[([(or,2)],0),([],0)], []>
Critical Pair <or(T,?x_5), T> by Rules <5, 0> preceded by []
 joinable by a reduction of rules <[([],2)], []>
Critical Pair <T, T> by Rules <2, 1> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <F, F> by Rules <3, 1> preceded by []
 joinable by a reduction of rules <[], []>
Critical Pair <or(?x_4,or(?y_4,F)), or(?x_4,?y_4)> by Rules <4, 1> preceded by []
 joinable by a reduction of rules <[([(or,2)],1)], []>
Critical Pair <or(F,?x_5), ?x_5> by Rules <5, 1> preceded by []
 joinable by a reduction of rules <[([],3)], []>
Critical Pair <or(?y_5,T), T> by Rules <5, 2> preceded by []
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <or(?y_5,F), ?y_5> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <or(?y_5,or(?x_4,?y_4)), or(?x_4,or(?y_4,?y_5))> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([],5),([],4)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 16 rules by 3 steps unfolding
strenghten or(?x_10,F) and ?x_10
strenghten or(?x_12,T) and T
strenghten or(F,?x_5) and ?x_5
strenghten or(T,?x_5) and T
strenghten or(?x_15,?y_15) and or(?y_15,?x_15)
strenghten or(?x_4,or(?y_4,T)) and T
strenghten or(?x,or(T,?z_4)) and or(T,?z_4)
strenghten or(?x_1,or(F,?z_4)) and or(?x_1,?z_4)
strenghten or(?x_4,or(?y_4,F)) and or(?x_4,?y_4)
strenghten or(F,or(?x_3,?z_4)) and or(?x_3,?z_4)
strenghten or(T,or(?x_2,?z_4)) and or(T,?z_4)
strenghten or(?x_4,or(?y_4,?y_5)) and or(?y_5,or(?x_4,?y_4))
strenghten or(?x_4,or(?y_4,?y_14)) and or(or(?x_4,?y_4),?y_14)
strenghten or(?x_5,or(?y_5,?z_4)) and or(or(?y_5,?x_5),?z_4)
strenghten or(or(?x,?y),or(?z,?z_1)) and or(or(?x,or(?y,?z)),?z_1)
obtain 100 candidates for checking non-joinability
check by TCAP-Approximation (failure)
check by Root-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) (failure)
unknown Non-Confluence
Check relative termination:
   [ or(?x,T) -> T,
     or(?x,F) -> ?x,
     or(T,?x) -> T,
     or(F,?x) -> ?x ]
   [ or(or(?x,?y),?z) -> or(?x,or(?y,?z)),
     or(?x,?y) -> or(?y,?x) ]
Polynomial Interpretation:
  F:= (8)
  T:= 0
  or:= (1)*x1+(1)*x2
retract or(?x,F) -> ?x
retract or(F,?x) -> ?x
Polynomial Interpretation:
  F:= 0
  T:= 0
  or:= (2)+(2)*x1+(1)*x1*x2+(2)*x2
relatively terminating
Huet (modulo AC)
Direct Methods: CR

Final result: CR
201.trs: Success(CR)
(2420 msec.)