MAYBE
(ignored inputs)COMMENT full experiments for [35] submitted by: Takahito Aoto and Yoshihito Toyama
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)) ]
Linear
(inner) Parallel CPs: (not computed)
unknown Toyama (Parallel CPs)
Direct Methods: Can't judge

Combined result: Can't judge
193.trs: Failure(unknown CR)
(0 msec.)