60.05/60.06	MAYBE
60.05/60.06	(ignored inputs)COMMENT doi:10.1007/978-3-540-89439-1_34 [31] Figures 3 and 4
60.05/60.06	input TRS:
60.05/60.06	   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
60.05/60.06	     .(?R,id) -> ?R,
60.05/60.06	     .(id,?R) -> ?R,
60.05/60.06	     and(id,id) -> id,
60.05/60.06	     sub(id,id) -> id,
60.05/60.06	     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
60.05/60.06	     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
60.05/60.06	     .(and(?R,?T),w1) -> .(w1,?R),
60.05/60.06	     .(and(?R,?T),w2) -> .(w2,?T),
60.05/60.06	     .(?R,c) -> .(c,and(?R,?R)),
60.05/60.06	     .(c,w1) -> id,
60.05/60.06	     .(c,w2) -> id,
60.05/60.06	     .(?R,i) -> .(i,sub(id,and(?R,id))),
60.05/60.06	     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
60.05/60.06	     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
60.05/60.06	     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
60.05/60.06	     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
60.05/60.06	     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
60.05/60.06	     .(and(i,?R),e) -> and(id,?R),
60.05/60.06	     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
60.05/60.06	     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
60.05/60.06	Try persistent and layer-preserving decomposition...
60.05/60.06	Sort Assignment:
60.05/60.07	 . : 59*59=>59
60.05/60.07	 c : =>59
60.05/60.07	 e : =>59
60.05/60.07	 i : =>59
60.05/60.07	 id : =>59
60.05/60.07	 w1 : =>59
60.05/60.07	 w2 : =>59
60.05/60.07	 and : 59*59=>59
60.05/60.07	 sub : 59*59=>59
60.05/60.07	maximal types: {59}
60.05/60.07	...decomposition failed.
60.05/60.07	TRS:
60.05/60.07	   [ .(?R,.(?T,?U)) -> .(.(?R,?T),?U),
60.05/60.07	     .(?R,id) -> ?R,
60.05/60.07	     .(id,?R) -> ?R,
60.05/60.07	     and(id,id) -> id,
60.05/60.07	     sub(id,id) -> id,
60.05/60.07	     .(and(?R,?T),and(?U,?V)) -> and(.(?R,?U),.(?T,?V)),
60.05/60.07	     .(sub(?R,?T),sub(?U,?V)) -> sub(.(?U,?R),.(?T,?V)),
60.05/60.07	     .(and(?R,?T),w1) -> .(w1,?R),
60.05/60.07	     .(and(?R,?T),w2) -> .(w2,?T),
60.05/60.07	     .(?R,c) -> .(c,and(?R,?R)),
60.05/60.07	     .(c,w1) -> id,
60.05/60.07	     .(c,w2) -> id,
60.05/60.07	     .(?R,i) -> .(i,sub(id,and(?R,id))),
60.05/60.07	     .(and(.(i,sub(id,?R)),?T),e) -> .(and(id,?T),?R),
60.05/60.07	     .(.(?W,and(?R,?T)),and(?U,?V)) -> .(?W,and(.(?R,?U),.(?T,?V))),
60.05/60.07	     .(.(?W,sub(?R,?T)),sub(?U,?V)) -> .(?W,sub(.(?U,?R),.(?T,?V))),
60.05/60.07	     .(.(?W,and(?R,?T)),w1) -> .(.(?W,w1),?R),
60.05/60.07	     .(.(?W,and(?R,?T)),w2) -> .(.(?W,w2),?T),
60.05/60.07	     .(and(i,?R),e) -> and(id,?R),
60.05/60.07	     .(.(?W,and(i,?R)),e) -> .(?W,and(id,?R)),
60.05/60.07	     .(.(?W,and(.(i,sub(id,?R)),?T)),e) -> .(.(?W,and(id,?T)),?R) ]
60.05/60.07	unknown Non-Omega-Overlapping
60.05/60.07	unknown Right-Reducible
60.05/60.07	Check distinct normal forms in critical pair closure...failed
60.05/60.07	/export/starexec/sandbox2/benchmark/theBenchmark.trs: Failure(timeout)
60.05/60.07	(111252 msec.)
60.05/60.07	EOF