0.00/0.04	MAYBE
0.00/0.04	
0.00/0.04	-- Is this system SN? ...MAYBE.
0.00/0.04	
0.00/0.04	We split firstr-order part and higher-order part, and do modular checking by a general modularity.
0.00/0.04	
0.00/0.04	******** FO SN check ********
0.00/0.04	Check SN using NaTT (Nagoya Termination Tool)
0.00/0.04	Input TRS:
0.00/0.04	    1: f(X,X) -> a()
0.00/0.04	    2: f(X,s(X)) -> b()
0.00/0.04	    3: _(X1,X2) -> X1
0.00/0.04	    4: _(X1,X2) -> X2
0.00/0.04	Number of strict rules: 4
0.00/0.04	Direct POLO(bPol) ... removes: 4 1 3 2
0.00/0.04	      a 	w: 0
0.00/0.04	      s 	w: x1 + 1
0.00/0.04	      b 	w: 2
0.00/0.04	      _ 	w: 2 * x1 + 2 * x2 + 1
0.00/0.04	      f 	w: x1 + 2 * x2 + 1
0.00/0.04	Number of strict rules: 0
0.00/0.04	
0.00/0.04	...
0.00/0.04	Input TRS:
0.00/0.04	    1: f(X,X) -> a()
0.00/0.04	    2: f(X,s(X)) -> b()
0.00/0.04	    3: _(X1,X2) -> X1
0.00/0.04	    4: _(X1,X2) -> X2
0.00/0.04	Number of strict rules: 4
0.00/0.04	Direct POLO(bPol) ... removes: 4 1 3 2
0.00/0.04	      a 	w: 0
0.00/0.04	      s 	w: x1 + 1
0.00/0.04	      b 	w: 2
0.00/0.04	      _ 	w: 2 * x1 + 2 * x2 + 1
0.00/0.04	      f 	w: x1 + 2 * x2 + 1
0.00/0.04	Number of strict rules: 0
0.00/0.04	>>YES
0.00/0.04	
0.00/0.04	******** Signature ********
0.00/0.04	 mu : (o -> o) -> o
0.00/0.04	******** Computation rules ********
0.00/0.04	 (3)  mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	
0.00/0.04	
0.00/0.04	******** General Schema criterion ********
0.00/0.04	Checking function dependency >>OK
0.00/0.04	Checking type dependency >>OK
0.00/0.04	Checking  (1) f(X,X) => a
0.00/0.04	 (fun f>a) >>True
0.00/0.04	Checking  (2) f(X,s(X)) => b
0.00/0.04	 (fun f>b) >>True
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. LR LR >>False
0.00/0.04	
0.00/0.04	Try again using status RL
0.00/0.04	Checking  (1) f(X,X) => a
0.00/0.04	 (fun f>a) >>True
0.00/0.04	Checking  (2) f(X,s(X)) => b
0.00/0.04	 (fun f>b) >>True
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. RL RL >>False
0.00/0.04	
0.00/0.04	Try again using status Mul
0.00/0.04	Checking  (1) f(X,X) => a
0.00/0.04	 (fun f>a) >>True
0.00/0.04	Checking  (2) f(X,s(X)) => b
0.00/0.04	 (fun f>b) >>True
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. Mul Mul >>False
0.00/0.04	Checking function dependency >>OK
0.00/0.04	Checking type dependency >>OK
0.00/0.04	Checking  (1) f(X,X) => a
0.00/0.04	 (fun f>a) >>True
0.00/0.04	Checking  (2) f(X,s(X)) => b
0.00/0.04	 (fun f>b) >>True
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. LR LR >>False
0.00/0.04	
0.00/0.04	Try again using status RL
0.00/0.04	Checking  (1) f(X,X) => a
0.00/0.04	 (fun f>a) >>True
0.00/0.04	Checking  (2) f(X,s(X)) => b
0.00/0.04	 (fun f>b) >>True
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. RL RL >>False
0.00/0.04	
0.00/0.04	Try again using status Mul
0.00/0.04	Checking  (1) f(X,X) => a
0.00/0.04	 (fun f>a) >>True
0.00/0.04	Checking  (2) f(X,s(X)) => b
0.00/0.04	 (fun f>b) >>True
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. Mul Mul >>False
0.00/0.04	Checking function dependency >>OK
0.00/0.04	Checking type dependency >>OK
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. LR LR >>False
0.00/0.04	
0.00/0.04	Try again using status RL
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. RL RL >>False
0.00/0.04	
0.00/0.04	Try again using status Mul
0.00/0.04	Checking  (3) mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	 (meta Z)[is acc in x.Z[x]] [is acc in Z[x]] 
0.00/0.04	 (fun mu=mu) subterm comparison of args w. Mul Mul >>False
0.00/0.04	#No idea..
0.00/0.04	******** Critical pairs ********
0.00/0.04	#All are joinable, but  CR is not sure (Total 0 CPs)
0.00/0.04	
0.00/0.04	******** Signature ********
0.00/0.04	f : o -> o -> o
0.00/0.04	s : o -> o
0.00/0.04	a : o
0.00/0.04	b : o
0.00/0.04	mu : (o -> o) -> o
0.00/0.04	
0.00/0.04	******** Computation rules ********
0.00/0.04	 (1)  f(X,X) => a
0.00/0.04	 (2)  f(X,s(X)) => b
0.00/0.04	 (3)  mu(x.Z[x]) => Z[mu(x.Z[x])]
0.00/0.04	
0.00/0.04	MAYBE
0.00/0.04	EOF