YES
(ignored inputs)COMMENT from the collection of \cite{AT2012}
Rewrite Rules:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)),
     exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
Apply Direct Methods...
Inner CPs:
   [ not(F) = T,
     not(T) = F,
     exor(F,?y_3) = not(exor(T,?y_3)),
     exor(T,?y_3) = not(exor(F,?y_3)),
     exor(?x,?y_3) = not(exor(not(?x),?y_3)),
     exor(not(?x_1),?z_4) = exor(?x_1,exor(T,?z_4)),
     exor(?x_2,?z_4) = exor(?x_2,exor(F,?z_4)),
     exor(not(exor(?x_3,?y_3)),?z_4) = exor(not(?x_3),exor(?y_3,?z_4)),
     exor(exor(?y_5,?x_5),?z_4) = exor(?x_5,exor(?y_5,?z_4)),
     not(?x) = not(?x),
     exor(exor(?x,exor(?y,?z)),?z_1) = exor(exor(?x,?y),exor(?z,?z_1)) ]
Outer CPs:
   [ not(not(?x_3)) = not(exor(?x_3,T)),
     not(exor(?x_4,?y_4)) = exor(?x_4,exor(?y_4,T)),
     not(?x_1) = exor(T,?x_1),
     not(?x_3) = not(exor(?x_3,F)),
     exor(?x_4,?y_4) = exor(?x_4,exor(?y_4,F)),
     ?x_2 = exor(F,?x_2),
     not(exor(?x_3,?y_3)) = exor(?y_3,not(?x_3)),
     exor(?x_4,exor(?y_4,?z_4)) = exor(?z_4,exor(?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 = not(F),
     not(exor(T,?y_3)) = exor(F,?y_3),
     F = not(T),
     not(exor(F,?y_3)) = exor(T,?y_3),
     not(?x_1) = not(?x_1),
     not(F) = T,
     not(T) = F,
     ?x_1 = not(not(?x_1)),
     not(exor(?x_5,?y_4)) = exor(not(?x_5),?y_4),
     not(exor(not(?x),?y_4)) = exor(?x,?y_4),
     not(exor(?x_3,T)) = not(not(?x_3)),
     exor(?x_4,exor(?y_4,T)) = not(exor(?x_4,?y_4)),
     exor(T,?x) = not(?x),
     exor(?x,exor(T,?z_5)) = exor(not(?x),?z_5),
     not(exor(?x_3,F)) = not(?x_3),
     exor(?x_4,exor(?y_4,F)) = exor(?x_4,?y_4),
     exor(F,?x) = ?x,
     exor(?x,exor(F,?z_5)) = exor(?x,?z_5),
     not(F) = not(exor(T,T)),
     not(T) = not(exor(F,T)),
     not(?x_2) = not(exor(not(?x_2),T)),
     F = not(exor(T,F)),
     T = not(exor(F,F)),
     ?x_2 = not(exor(not(?x_2),F)),
     exor(?y,F) = not(exor(T,?y)),
     exor(?y,T) = not(exor(F,?y)),
     exor(?y,?x_2) = not(exor(not(?x_2),?y)),
     not(not(?x)) = not(exor(?x,T)),
     not(?x) = not(exor(?x,F)),
     exor(?y,not(?x)) = not(exor(?x,?y)),
     exor(F,?y) = not(exor(T,?y)),
     exor(T,?y) = not(exor(F,?y)),
     exor(?x_2,?y) = not(exor(not(?x_2),?y)),
     exor(F,exor(?y,?z_5)) = exor(not(exor(T,?y)),?z_5),
     exor(T,exor(?y,?z_5)) = exor(not(exor(F,?y)),?z_5),
     exor(?x_7,exor(?y,?z_5)) = exor(not(exor(not(?x_7),?y)),?z_5),
     exor(not(?x),exor(?y,?z_5)) = exor(not(exor(?x,?y)),?z_5),
     not(exor(?x_1,exor(?y_1,?y))) = exor(exor(?x_1,?y_1),exor(?y,T)),
     not(not(?x)) = exor(?x,exor(T,T)),
     not(?x) = exor(?x,exor(F,T)),
     not(not(exor(?x_5,?y))) = exor(not(?x_5),exor(?y,T)),
     not(exor(?y,?x)) = exor(?x,exor(?y,T)),
     exor(?x_1,exor(?y_1,?y)) = exor(exor(?x_1,?y_1),exor(?y,F)),
     not(?x) = exor(?x,exor(T,F)),
     ?x = exor(?x,exor(F,F)),
     not(exor(?x_5,?y)) = exor(not(?x_5),exor(?y,F)),
     exor(?y,?x) = exor(?x,exor(?y,F)),
     exor(?z,exor(?x_1,exor(?y_1,?y))) = exor(exor(?x_1,?y_1),exor(?y,?z)),
     exor(?z,not(?x)) = exor(?x,exor(T,?z)),
     exor(?z,?x) = exor(?x,exor(F,?z)),
     exor(?z,not(exor(?x_5,?y))) = exor(not(?x_5),exor(?y,?z)),
     exor(?z,exor(?y,?x)) = exor(?x,exor(?y,?z)),
     not(exor(?x,?y)) = exor(?x,exor(?y,T)),
     exor(?x,?y) = exor(?x,exor(?y,F)),
     exor(?z,exor(?x,?y)) = exor(?x,exor(?y,?z)),
     exor(exor(?x_1,exor(?y_1,?y)),?z) = exor(exor(?x_1,?y_1),exor(?y,?z)),
     exor(not(?x),?z) = exor(?x,exor(T,?z)),
     exor(?x,?z) = exor(?x,exor(F,?z)),
     exor(not(exor(?x_5,?y)),?z) = exor(not(?x_5),exor(?y,?z)),
     exor(exor(?y,?x),?z) = exor(?x,exor(?y,?z)),
     exor(exor(?x_2,exor(?y_2,?y)),exor(?z,?z_1)) = exor(exor(exor(?x_2,?y_2),exor(?y,?z)),?z_1),
     exor(not(?x),exor(?z,?z_1)) = exor(exor(?x,exor(T,?z)),?z_1),
     exor(?x,exor(?z,?z_1)) = exor(exor(?x,exor(F,?z)),?z_1),
     exor(not(exor(?x_6,?y)),exor(?z,?z_1)) = exor(exor(not(?x_6),exor(?y,?z)),?z_1),
     exor(exor(?y,?x),exor(?z,?z_1)) = exor(exor(?x,exor(?y,?z)),?z_1),
     exor(exor(?x,?y),exor(?z,?z_1)) = exor(exor(?x,exor(?y,?z)),?z_1),
     not(?x) = exor(T,?x),
     ?x = exor(F,?x),
     not(exor(?x_4,?y)) = exor(?y,not(?x_4)),
     exor(?x_5,exor(?y_5,?y)) = exor(?y,exor(?x_5,?y_5)),
     exor(?x,exor(?y,?z_6)) = exor(exor(?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 <not(F), T> by Rules <0, 2> preceded by [(not,1)]
 joinable by a reduction of rules <[([],1)], []>
Critical Pair <not(T), F> by Rules <1, 2> preceded by [(not,1)]
 joinable by a reduction of rules <[([],0)], []>
Critical Pair <exor(F,?y_3), not(exor(T,?y_3))> by Rules <0, 5> preceded by [(exor,1)]
 joinable by a reduction of rules <[([],7),([],4)], [([(not,1)],7),([(not,1)],3),([],2)]>
Critical Pair <exor(T,?y_3), not(exor(F,?y_3))> by Rules <1, 5> preceded by [(exor,1)]
 joinable by a reduction of rules <[([],7),([],3)], [([(not,1)],7),([(not,1)],4)]>
Critical Pair <exor(?x,?y_3), not(exor(not(?x),?y_3))> by Rules <2, 5> preceded by [(exor,1)]
 joinable by a reduction of rules <[], [([(not,1)],5),([],2)]>
Critical Pair <exor(not(?x_1),?z_4), exor(?x_1,exor(T,?z_4))> by Rules <3, 6> preceded by [(exor,1)]
 joinable by a reduction of rules <[([],5),([(not,1)],7)], [([(exor,2)],7),([(exor,2)],3),([],7),([],5)]>
 joinable by a reduction of rules <[([],5),([(not,1)],7)], [([(exor,2)],7),([],7),([(exor,1)],3),([],5)]>
 joinable by a reduction of rules <[([],5),([(not,1)],7)], [([],7),([(exor,1)],7),([(exor,1)],3),([],5)]>
 joinable by a reduction of rules <[([],5),([(not,1)],7)], [([],7),([],6),([],7),([],3)]>
Critical Pair <exor(?x_2,?z_4), exor(?x_2,exor(F,?z_4))> by Rules <4, 6> preceded by [(exor,1)]
 joinable by a reduction of rules <[], [([(exor,2)],7),([(exor,2)],4)]>
Critical Pair <exor(not(exor(?x_3,?y_3)),?z_4), exor(not(?x_3),exor(?y_3,?z_4))> by Rules <5, 6> preceded by [(exor,1)]
 joinable by a reduction of rules <[([],5),([(not,1)],6)], [([],5)]>
Critical Pair <exor(exor(?y_5,?x_5),?z_4), exor(?x_5,exor(?y_5,?z_4))> by Rules <7, 6> preceded by [(exor,1)]
 joinable by a reduction of rules <[([(exor,1)],7),([],6)], []>
 joinable by a reduction of rules <[([],6),([(exor,2)],7)], [([],7),([],6)]>
Critical Pair <not(?x), not(?x)> by Rules <2, 2> preceded by [(not,1)]
 joinable by a reduction of rules <[], []>
Critical Pair <exor(exor(?x,exor(?y,?z)),?z_1), exor(exor(?x,?y),exor(?z,?z_1))> by Rules <6, 6> preceded by [(exor,1)]
 joinable by a reduction of rules <[([],6),([(exor,2)],6)], [([],6)]>
Critical Pair <not(exor(?x_3,T)), not(not(?x_3))> by Rules <5, 3> preceded by []
 joinable by a reduction of rules <[([(not,1)],3)], []>
Critical Pair <exor(?x_4,exor(?y_4,T)), not(exor(?x_4,?y_4))> by Rules <6, 3> preceded by []
 joinable by a reduction of rules <[([(exor,2)],3),([],7),([],5)], [([(not,1)],7)]>
 joinable by a reduction of rules <[([],7),([(exor,1)],3),([],5)], [([(not,1)],7)]>
Critical Pair <exor(T,?x_5), not(?x_5)> by Rules <7, 3> preceded by []
 joinable by a reduction of rules <[([],7),([],3)], []>
Critical Pair <not(exor(?x_3,F)), not(?x_3)> by Rules <5, 4> preceded by []
 joinable by a reduction of rules <[([(not,1)],4)], []>
Critical Pair <exor(?x_4,exor(?y_4,F)), exor(?x_4,?y_4)> by Rules <6, 4> preceded by []
 joinable by a reduction of rules <[([(exor,2)],4)], []>
Critical Pair <exor(F,?x_5), ?x_5> by Rules <7, 4> preceded by []
 joinable by a reduction of rules <[([],7),([],4)], []>
Critical Pair <exor(?y_5,not(?x_3)), not(exor(?x_3,?y_5))> by Rules <7, 5> preceded by []
 joinable by a reduction of rules <[([],7),([],5)], []>
Critical Pair <exor(?y_5,exor(?x_4,?y_4)), exor(?x_4,exor(?y_4,?y_5))> by Rules <7, 6> preceded by []
 joinable by a reduction of rules <[([],7),([],6)], []>
unknown Diagram Decreasing
check Non-Confluence...
obtain 18 rules by 3 steps unfolding
strenghten not(F) and T
strenghten not(T) and F
strenghten exor(?x_8,F) and ?x_8
strenghten exor(F,?x_5) and ?x_5
strenghten exor(F,T) and T
strenghten exor(T,F) and T
strenghten exor(T,?x_5) and not(?x_5)
strenghten not(exor(?x_3,F)) and not(?x_3)
strenghten not(exor(?x_3,T)) and not(not(?x_3))
strenghten not(exor(F,?y_3)) and exor(T,?y_3)
strenghten not(exor(T,?y_3)) and exor(F,?y_3)
strenghten not(exor(?x_3,?y_5)) and exor(?y_5,not(?x_3))
strenghten not(exor(not(?x),?y_3)) and exor(?x,?y_3)
strenghten not(exor(not(F),?y_3)) and exor(F,?y_3)
strenghten not(exor(not(T),?y_3)) and exor(T,?y_3)
strenghten exor(?x_2,exor(F,?z_4)) and exor(?x_2,?z_4)
strenghten exor(?x_4,exor(?y_4,F)) and exor(?x_4,?y_4)
strenghten exor(F,exor(?x_8,?z_4)) and exor(?x_8,?z_4)
strenghten exor(F,exor(T,?z_4)) and exor(T,?z_4)
strenghten exor(T,exor(F,?z_4)) and exor(T,?z_4)
strenghten exor(?x_1,exor(T,?z_4)) and exor(not(?x_1),?z_4)
strenghten exor(?x_4,exor(?y_4,T)) and not(exor(?x_4,?y_4))
strenghten exor(?x_4,exor(?y_4,?y_5)) and exor(?y_5,exor(?x_4,?y_4))
strenghten exor(?x_5,exor(?y_5,?z_4)) and exor(exor(?y_5,?x_5),?z_4)
strenghten exor(not(?x_3),exor(?y_3,?z_4)) and exor(not(exor(?x_3,?y_3)),?z_4)
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:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)) ]
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
Polynomial Interpretation:
  F:= 0
  T:= (8)
  not:= (1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract exor(?x,T) -> not(?x)
Polynomial Interpretation:
  F:= 0
  T:= 0
  not:= (8)+(1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract not(F) -> T
retract exor(?x,T) -> not(?x)
Polynomial Interpretation:
  F:= (4)
  T:= 0
  not:= (4)+(1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract not(F) -> T
retract not(not(?x)) -> ?x
retract exor(?x,T) -> not(?x)
retract exor(?x,F) -> ?x
Polynomial Interpretation:
  F:= 0
  T:= (1)
  not:= (1)+(1)*x1
  exor:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
unknown Huet (modulo AC)
check by Reduction-Preserving Completion...
STEP: 1 (parallel)
S:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)) ]
P:
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
S: terminating
CP(S,S):
<not(F), T> --> <T, T> => yes
<not(T), F> --> <F, F> => yes
<not(?x), not(?x)> --> <not(?x), not(?x)> => yes
<not(exor(?x_3,T)), not(not(?x_3))> --> <?x_3, ?x_3> => yes
<not(exor(?x_3,F)), not(?x_3)> --> <not(?x_3), not(?x_3)> => yes
<exor(F,?y_3), not(exor(T,?y_3))> --> <exor(F,?y_3), not(exor(T,?y_3))> => no
<exor(T,?y_3), not(exor(F,?y_3))> --> <exor(T,?y_3), not(exor(F,?y_3))> => no
<exor(?x,?y_3), not(exor(not(?x),?y_3))> --> <exor(?x,?y_3), exor(?x,?y_3)> => yes
PCP_in(symP,S):
CP(S,symP):
<not(exor(?x_1,?y_1)), exor(?x_1,exor(?y_1,T))> --> <not(exor(?x_1,?y_1)), exor(?x_1,not(?y_1))> => no
<exor(not(?x),?z_1), exor(?x,exor(T,?z_1))> --> <not(exor(?x,?z_1)), exor(?x,exor(T,?z_1))> => no
<exor(?x_1,not(?x)), exor(exor(?x_1,?x),T)> --> <exor(?x_1,not(?x)), not(exor(?x_1,?x))> => no
<not(?x), exor(T,?x)> --> <not(?x), exor(T,?x)> => no
<exor(?x_1,?y_1), exor(?x_1,exor(?y_1,F))> --> <exor(?x_1,?y_1), exor(?x_1,?y_1)> => yes
<exor(?x,?z_1), exor(?x,exor(F,?z_1))> --> <exor(?x,?z_1), exor(?x,exor(F,?z_1))> => no
<exor(?x_1,?x), exor(exor(?x_1,?x),F)> --> <exor(?x_1,?x), exor(?x_1,?x)> => yes
<?x, exor(F,?x)> --> <?x, exor(F,?x)> => no
<exor(not(exor(?x,?y)),?z_1), exor(not(?x),exor(?y,?z_1))> --> <not(exor(exor(?x,?y),?z_1)), not(exor(?x,exor(?y,?z_1)))> => yes
<not(exor(?x,exor(?y_1,?z_1))), exor(exor(not(?x),?y_1),?z_1)> --> <not(exor(?x,exor(?y_1,?z_1))), not(exor(exor(?x,?y_1),?z_1))> => yes
<exor(?x_1,not(exor(?x,?y))), exor(exor(?x_1,not(?x)),?y)> --> <exor(?x_1,not(exor(?x,?y))), exor(exor(?x_1,not(?x)),?y)> => no
<not(exor(?x,?y)), exor(?y,not(?x))> --> <not(exor(?x,?y)), exor(?y,not(?x))> => no
check joinability condition:
check modulo joinability of exor(F,?y_3) and not(exor(T,?y_3)): joinable by {0}
check modulo joinability of exor(T,?y_3) and not(exor(F,?y_3)): joinable by {0}
check modulo joinability of not(exor(?x_1,?y_1)) and exor(?x_1,not(?y_1)): joinable by {0}
check modulo reachablity from not(exor(?x,?z_1)) to exor(?x,exor(T,?z_1)): maybe not reachable
check modulo joinability of exor(?x_1,not(?x)) and not(exor(?x_1,?x)): joinable by {0}
check modulo reachablity from not(?x) to exor(T,?x): maybe not reachable
check modulo reachablity from exor(?x,?z_1) to exor(?x,exor(F,?z_1)): maybe not reachable
check modulo reachablity from ?x to exor(F,?x): maybe not reachable
check modulo reachablity from exor(?x_1,not(exor(?x,?y))) to exor(exor(?x_1,not(?x)),?y): maybe not reachable
check modulo reachablity from not(exor(?x,?y)) to exor(?y,not(?x)): maybe not reachable
failed
failure(Step 1)
   [ exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
Added S-Rules:
   [ exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
Added P-Rules:
   [ ]
replace: exor(not(?x),?y) -> not(exor(?x,?y)) => exor(not(?x),?y) -> not(exor(?y,?x))
STEP: 2 (linear)
S:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)) ]
P:
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
S: terminating
CP(S,S):
<not(F), T> --> <T, T> => yes
<not(T), F> --> <F, F> => yes
<not(?x), not(?x)> --> <not(?x), not(?x)> => yes
<not(exor(?x_3,T)), not(not(?x_3))> --> <?x_3, ?x_3> => yes
<not(exor(?x_3,F)), not(?x_3)> --> <not(?x_3), not(?x_3)> => yes
<exor(F,?y_3), not(exor(T,?y_3))> --> <exor(F,?y_3), not(exor(T,?y_3))> => no
<exor(T,?y_3), not(exor(F,?y_3))> --> <exor(T,?y_3), not(exor(F,?y_3))> => no
<exor(?x,?y_3), not(exor(not(?x),?y_3))> --> <exor(?x,?y_3), exor(?x,?y_3)> => yes
CP_in(symP,S):
CP(S,symP):
<not(exor(?x_1,?y_1)), exor(?x_1,exor(?y_1,T))> --> <not(exor(?x_1,?y_1)), exor(?x_1,not(?y_1))> => no
<exor(not(?x),?z_1), exor(?x,exor(T,?z_1))> --> <not(exor(?x,?z_1)), exor(?x,exor(T,?z_1))> => no
<exor(?x_1,not(?x)), exor(exor(?x_1,?x),T)> --> <exor(?x_1,not(?x)), not(exor(?x_1,?x))> => no
<not(?x), exor(T,?x)> --> <not(?x), exor(T,?x)> => no
<exor(?x_1,?y_1), exor(?x_1,exor(?y_1,F))> --> <exor(?x_1,?y_1), exor(?x_1,?y_1)> => yes
<exor(?x,?z_1), exor(?x,exor(F,?z_1))> --> <exor(?x,?z_1), exor(?x,exor(F,?z_1))> => no
<exor(?x_1,?x), exor(exor(?x_1,?x),F)> --> <exor(?x_1,?x), exor(?x_1,?x)> => yes
<?x, exor(F,?x)> --> <?x, exor(F,?x)> => no
<exor(not(exor(?x,?y)),?z_1), exor(not(?x),exor(?y,?z_1))> --> <not(exor(exor(?x,?y),?z_1)), not(exor(?x,exor(?y,?z_1)))> => yes
<not(exor(?x,exor(?y_1,?z_1))), exor(exor(not(?x),?y_1),?z_1)> --> <not(exor(?x,exor(?y_1,?z_1))), not(exor(exor(?x,?y_1),?z_1))> => yes
<exor(?x_1,not(exor(?x,?y))), exor(exor(?x_1,not(?x)),?y)> --> <exor(?x_1,not(exor(?x,?y))), exor(exor(?x_1,not(?x)),?y)> => no
<not(exor(?x,?y)), exor(?y,not(?x))> --> <not(exor(?x,?y)), exor(?y,not(?x))> => no
check joinability condition:
check modulo joinability of exor(F,?y_3) and not(exor(T,?y_3)): maybe not joinable
check modulo joinability of exor(T,?y_3) and not(exor(F,?y_3)): maybe not joinable
check modulo joinability of not(exor(?x_1,?y_1)) and exor(?x_1,not(?y_1)): joinable by {2}
check modulo reachablity from not(exor(?x,?z_1)) to exor(?x,exor(T,?z_1)): maybe not reachable
check modulo joinability of exor(?x_1,not(?x)) and not(exor(?x_1,?x)): joinable by {2}
check modulo reachablity from not(?x) to exor(T,?x): maybe not reachable
check modulo reachablity from exor(?x,?z_1) to exor(?x,exor(F,?z_1)): maybe not reachable
check modulo reachablity from ?x to exor(F,?x): maybe not reachable
check modulo reachablity from exor(?x_1,not(exor(?x,?y))) to exor(exor(?x_1,not(?x)),?y): maybe not reachable
check modulo reachablity from not(exor(?x,?y)) to exor(?y,not(?x)): maybe not reachable
failed
failure(Step 2)
   [ exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
Added S-Rules:
   [ exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
Added P-Rules:
   [ ]
replace: exor(not(?x),?y) -> not(exor(?x,?y)) => exor(not(?x),?y) -> not(exor(?y,?x))
STEP: 3 (relative)
S:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)) ]
P:
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
Check relative termination:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)) ]
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
Polynomial Interpretation:
  F:= 0
  T:= (8)
  not:= (1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract exor(?x,T) -> not(?x)
Polynomial Interpretation:
  F:= 0
  T:= 0
  not:= (8)+(1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract not(F) -> T
retract exor(?x,T) -> not(?x)
Polynomial Interpretation:
  F:= (4)
  T:= 0
  not:= (4)+(1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract not(F) -> T
retract not(not(?x)) -> ?x
retract exor(?x,T) -> not(?x)
retract exor(?x,F) -> ?x
Polynomial Interpretation:
  F:= 0
  T:= (1)
  not:= (1)+(1)*x1
  exor:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
S/P: relatively terminating
check CP condition:
failed
failure(Step 3)
STEP: 4 (parallel)
S:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)),
     exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
P:
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
S: terminating
CP(S,S):
<not(F), T> --> <T, T> => yes
<not(T), F> --> <F, F> => yes
<not(?x), not(?x)> --> <not(?x), not(?x)> => yes
<not(exor(?x_3,T)), not(not(?x_3))> --> <?x_3, ?x_3> => yes
<not(T), not(T)> --> <F, F> => yes
<T, not(F)> --> <T, T> => yes
<not(exor(?x_3,F)), not(?x_3)> --> <not(?x_3), not(?x_3)> => yes
<not(F), T> --> <T, T> => yes
<F, F> --> <F, F> => yes
<exor(F,?y_3), not(exor(T,?y_3))> --> <?y_3, ?y_3> => yes
<exor(T,?y_3), not(exor(F,?y_3))> --> <not(?y_3), not(?y_3)> => yes
<exor(?x,?y_3), not(exor(not(?x),?y_3))> --> <exor(?x,?y_3), exor(?x,?y_3)> => yes
<not(exor(not(?x_3),?z_5)), not(exor(?x_3,exor(T,?z_5)))> --> <exor(?x_3,?z_5), exor(?z_5,?x_3)> => yes
<not(exor(?x_8,not(?x_3))), not(exor(?x_3,not(?x_8)))> --> <exor(?x_3,?x_8), exor(?x_8,?x_3)> => yes
<exor(?x_4,not(T)), not(exor(?x_4,T))> --> <?x_4, ?x_4> => yes
<exor(?x_4,T), not(exor(?x_4,F))> --> <not(?x_4), not(?x_4)> => yes
<exor(?x_2,not(exor(T,?z_1))), not(exor(?x_2,exor(T,?z_1)))> --> <exor(?x_2,?z_1), exor(?z_1,?x_2)> => yes
<not(exor(T,?z_5)), not(exor(T,?z_5))> --> <?z_5, ?z_5> => yes
<exor(?x_4,not(?x_6)), not(exor(?x_4,?x_6))> --> <not(exor(?x_6,?x_4)), not(exor(?x_4,?x_6))> => yes
<exor(T,?z_5), not(exor(F,?z_5))> --> <not(?z_5), not(?z_5)> => yes
<exor(?x_4,not(exor(?x_8,T))), not(exor(?x_4,not(?x_8)))> --> <exor(?x_4,?x_8), exor(?x_8,?x_4)> => yes
<not(exor(?x_8,T)), not(not(?x_8))> --> <?x_8, ?x_8> => yes
<not(exor(?x_8,F)), not(?x_8)> --> <not(?x_8), not(?x_8)> => yes
<exor(?y_8,F), not(exor(T,?y_8))> --> <?y_8, ?y_8> => yes
<exor(?y_8,T), not(exor(F,?y_8))> --> <not(?y_8), not(?y_8)> => yes
<exor(?y_8,?x), not(exor(not(?x),?y_8))> --> <exor(?y_8,?x), exor(?x,?y_8)> => yes
PCP_in(symP,S):
<exor(?x,exor(?x_4,T)), not(exor(?x,?x_4))> --> <not(exor(?x_4,?x)), not(exor(?x,?x_4))> => no
<exor(?x,exor(exor(T,?y_3),?z_3)), not(exor(?x,exor(?y_3,?z_3)))> --> <not(exor(exor(?y_3,?z_3),?x)), not(exor(?x,exor(?y_3,?z_3)))> => no
CP(S,symP):
<not(exor(?x_1,?y_1)), exor(?x_1,exor(?y_1,T))> --> <not(exor(?x_1,?y_1)), not(exor(?y_1,?x_1))> => yes
<exor(not(?x),?z_1), exor(?x,exor(T,?z_1))> --> <not(exor(?x,?z_1)), not(exor(?z_1,?x))> => yes
<exor(?x_1,not(?x)), exor(exor(?x_1,?x),T)> --> <not(exor(?x,?x_1)), not(exor(?x_1,?x))> => yes
<not(?x), exor(T,?x)> --> <not(?x), not(?x)> => yes
<exor(?x_1,?y_1), exor(?x_1,exor(?y_1,F))> --> <exor(?x_1,?y_1), exor(?x_1,?y_1)> => yes
<exor(?x,?z_1), exor(?x,exor(F,?z_1))> --> <exor(?x,?z_1), exor(?x,?z_1)> => yes
<exor(?x_1,?x), exor(exor(?x_1,?x),F)> --> <exor(?x_1,?x), exor(?x_1,?x)> => yes
<?x, exor(F,?x)> --> <?x, ?x> => yes
<exor(not(exor(?x,?y)),?z_1), exor(not(?x),exor(?y,?z_1))> --> <not(exor(exor(?x,?y),?z_1)), not(exor(?x,exor(?y,?z_1)))> => yes
<not(exor(?x,exor(?y_1,?z_1))), exor(exor(not(?x),?y_1),?z_1)> --> <not(exor(?x,exor(?y_1,?z_1))), not(exor(exor(?x,?y_1),?z_1))> => yes
<exor(?x_1,not(exor(?x,?y))), exor(exor(?x_1,not(?x)),?y)> --> <not(exor(exor(?x,?y),?x_1)), not(exor(exor(?x,?x_1),?y))> => no
<not(exor(?x,?y)), exor(?y,not(?x))> --> <not(exor(?x,?y)), not(exor(?x,?y))> => yes
<not(exor(exor(?x_2,?y_2),?z_1)), exor(?x_2,exor(?y_2,exor(T,?z_1)))> --> <not(exor(exor(?x_2,?y_2),?z_1)), not(exor(exor(?z_1,?y_2),?x_2))> => no
<exor(not(exor(?x,?z_1)),?z_2), exor(?x,exor(exor(T,?z_1),?z_2))> --> <not(exor(exor(?x,?z_1),?z_2)), not(exor(exor(?z_1,?z_2),?x))> => no
<not(exor(?x,?z_1)), exor(exor(?x,T),?z_1)> --> <not(exor(?x,?z_1)), not(exor(?x,?z_1))> => yes
<exor(?x_2,not(exor(?x,?z_1))), exor(exor(?x_2,?x),exor(T,?z_1))> --> <not(exor(exor(?x,?z_1),?x_2)), not(exor(?z_1,exor(?x_2,?x)))> => no
<not(exor(?x,?z_1)), exor(exor(T,?z_1),?x)> --> <not(exor(?x,?z_1)), not(exor(?z_1,?x))> => yes
<exor(not(?x),?z_1), exor(T,exor(?x,?z_1))> --> <not(exor(?x,?z_1)), not(exor(?x,?z_1))> => yes
<not(exor(?y_1,?z_1)), exor(exor(T,?y_1),?z_1)> --> <not(exor(?y_1,?z_1)), not(exor(?y_1,?z_1))> => yes
<exor(?x_1,not(?x)), exor(exor(?x_1,T),?x)> --> <not(exor(?x,?x_1)), not(exor(?x_1,?x))> => yes
<not(?x), exor(?x,T)> --> <not(?x), not(?x)> => yes
<exor(?x,?z_1), exor(F,exor(?x,?z_1))> --> <exor(?x,?z_1), exor(?x,?z_1)> => yes
<exor(?y_1,?z_1), exor(exor(F,?y_1),?z_1)> --> <exor(?y_1,?z_1), exor(?y_1,?z_1)> => yes
<exor(?x_1,?x), exor(exor(?x_1,F),?x)> --> <exor(?x_1,?x), exor(?x_1,?x)> => yes
<?x, exor(?x,F)> --> <?x, ?x> => yes
<not(exor(?x,exor(?x_1,?y_1))), exor(?x_1,exor(?y_1,not(?x)))> --> <not(exor(?x,exor(?x_1,?y_1))), not(exor(exor(?x,?y_1),?x_1))> => no
<exor(not(exor(?x,?y)),?z_1), exor(?y,exor(not(?x),?z_1))> --> <not(exor(exor(?x,?y),?z_1)), not(exor(exor(?x,?z_1),?y))> => no
<exor(?x_1,not(exor(?x,?y))), exor(exor(?x_1,?y),not(?x))> --> <not(exor(exor(?x,?y),?x_1)), not(exor(?x,exor(?x_1,?y)))> => no
<not(exor(?x,?y)), exor(not(?x),?y)> --> <not(exor(?x,?y)), not(exor(?x,?y))> => yes
check joinability condition:
check modulo joinability of not(exor(?x_4,?x)) and not(exor(?x,?x_4)): joinable by {0}
check modulo joinability of not(exor(exor(?y_3,?z_3),?x)) and not(exor(?x,exor(?y_3,?z_3))): joinable by {0}
check modulo joinability of not(exor(exor(?x,?y),?x_1)) and not(exor(exor(?x,?x_1),?y)): joinable by {2}
check modulo joinability of not(exor(exor(?x_2,?y_2),?z_1)) and not(exor(exor(?z_1,?y_2),?x_2)): joinable by {0,2}
check modulo joinability of not(exor(exor(?x,?z_1),?z_2)) and not(exor(exor(?z_1,?z_2),?x)): joinable by {0}
check modulo joinability of not(exor(exor(?x,?z_1),?x_2)) and not(exor(?z_1,exor(?x_2,?x))): joinable by {0}
check modulo joinability of not(exor(?x,exor(?x_1,?y_1))) and not(exor(exor(?x,?y_1),?x_1)): joinable by {2}
check modulo joinability of not(exor(exor(?x,?y),?z_1)) and not(exor(exor(?x,?z_1),?y)): joinable by {2}
check modulo joinability of not(exor(exor(?x,?y),?x_1)) and not(exor(?x,exor(?x_1,?y))): joinable by {2}
success
P':
   [ exor(?y,?x) -> exor(?x,?y),
     exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)) ]
Check relative termination:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)),
     exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
   [ exor(?y,?x) -> exor(?x,?y),
     exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)) ]
Polynomial Interpretation:
  F:= (2)
  T:= 0
  not:= (1)*x1
  exor:= (1)*x1+(1)*x2
retract not(F) -> T
retract exor(?x,F) -> ?x
retract exor(F,?x) -> ?x
Polynomial Interpretation:
  F:= 0
  T:= 0
  not:= (2)+(1)*x1
  exor:= (1)*x1+(1)*x2
retract not(T) -> F
retract not(F) -> T
retract not(not(?x)) -> ?x
retract exor(?x,F) -> ?x
retract exor(F,?x) -> ?x
Polynomial Interpretation:
  F:= 0
  T:= (9)
  not:= (2)+(2)*x1
  exor:= (1)+(2)*x1+(2)*x1*x2+(2)*x2
relatively terminating
S/P': relatively terminating
S:
   [ not(T) -> F,
     not(F) -> T,
     not(not(?x)) -> ?x,
     exor(?x,T) -> not(?x),
     exor(?x,F) -> ?x,
     exor(not(?x),?y) -> not(exor(?x,?y)),
     exor(?x,exor(T,?z_1)) -> not(exor(?x,?z_1)),
     exor(T,?x) -> not(?x),
     exor(F,?x) -> ?x,
     exor(?y,not(?x)) -> not(exor(?x,?y)) ]
P:
   [ exor(exor(?x,?y),?z) -> exor(?x,exor(?y,?z)),
     exor(?x,?y) -> exor(?y,?x) ]
Success
Reduction-Preserving Completion
Direct Methods: CR

Final result: CR
193.trs: Success(CR)
(3223 msec.)