12.47/4.12	YES
12.47/4.12	
12.47/4.12	Proof:
12.47/4.12	This system is confluent.
12.47/4.12	By \cite{ALS94}, Theorem 4.1.
12.47/4.12	This system is of type 3 or smaller.
12.47/4.12	This system is strongly deterministic.
12.47/4.12	This system is quasi-decreasing.
12.47/4.12	By \cite{A14}, Theorem 11.5.9.
12.47/4.12	This system is of type 3 or smaller.
12.47/4.12	This system is deterministic.
12.47/4.12	System R transformed to V(R) + Emb.
12.47/4.12	This system is terminating.
12.47/4.12	Call external tool:
12.47/4.12	./ttt2.sh
12.47/4.12	Input:
12.47/4.12	(VAR x l y n m)
12.47/4.12	(RULES
12.47/4.12	  lte(0, n) -> true
12.47/4.12	  lte(s(m), 0) -> false
12.47/4.12	  lte(s(m), s(n)) -> lte(m, n)
12.47/4.12	  insert(nil, m) -> cons(m, nil)
12.47/4.12	  insert(cons(n, l), m) -> cons(m, cons(n, l))
12.47/4.12	  insert(cons(n, l), m) -> lte(m, n)
12.47/4.12	  insert(cons(n, l), m) -> cons(n, insert(l, m))
12.47/4.12	  ordered(nil) -> true
12.47/4.12	  ordered(cons(m, nil)) -> true
12.47/4.12	  ordered(cons(m, cons(n, l))) -> ordered(cons(n, l))
12.47/4.12	  ordered(cons(m, cons(n, l))) -> lte(m, n)
12.47/4.12	  ordered(cons(m, cons(n, l))) -> false
12.47/4.12	  s(x) -> x
12.47/4.12	  insert(x, y) -> x
12.47/4.12	  insert(x, y) -> y
12.47/4.12	  lte(x, y) -> x
12.47/4.12	  lte(x, y) -> y
12.47/4.12	  ordered(x) -> x
12.47/4.12	  cons(x, y) -> x
12.47/4.12	  cons(x, y) -> y
12.47/4.12	)
12.47/4.12	
12.47/4.12	 Matrix Interpretation Processor: dim=3
12.47/4.12	  
12.47/4.12	  interpretation:
12.47/4.12	                   [1 0 1]     [0]
12.47/4.12	   [ordered](x0) = [0 1 0]x0 + [1]
12.47/4.12	                   [0 0 1]     [1],
12.47/4.12	   
12.47/4.12	                    [1 0 0]          [1]
12.47/4.12	   [cons](x0, x1) = [0 1 0]x0 + x1 + [0]
12.47/4.12	                    [1 1 1]          [0],
12.47/4.12	   
12.47/4.12	                      [1 0 1]     [1 0 0]     [1]
12.47/4.12	   [insert](x0, x1) = [1 1 0]x0 + [0 1 0]x1 + [0]
12.47/4.12	                      [0 0 1]     [1 1 1]     [0],
12.47/4.12	   
12.47/4.12	           [0]
12.47/4.12	   [nil] = [0]
12.47/4.12	           [1],
12.47/4.12	   
12.47/4.12	             [0]
12.47/4.12	   [false] = [0]
12.47/4.12	             [0],
12.47/4.12	   
12.47/4.12	             [1 0 1]     [1]
12.47/4.12	   [s](x0) = [0 1 1]x0 + [0]
12.47/4.12	             [1 0 1]     [0],
12.47/4.12	   
12.47/4.12	            [1]
12.47/4.12	   [true] = [0]
12.47/4.12	            [0],
12.47/4.12	   
12.47/4.12	                   [1 0 0]     [1 0 1]     [1]
12.47/4.12	   [lte](x0, x1) = [0 1 0]x0 + [0 1 0]x1 + [0]
12.47/4.12	                   [0 1 1]     [0 0 1]     [0],
12.47/4.12	   
12.47/4.12	         [0]
12.47/4.12	   [0] = [0]
12.47/4.12	         [1]
12.47/4.12	  orientation:
12.47/4.12	                [1 0 1]    [1]    [1]         
12.47/4.12	   lte(0(),n) = [0 1 0]n + [0] >= [0] = true()
12.47/4.12	                [0 0 1]    [1]    [0]         
12.47/4.12	   
12.47/4.12	                   [1 0 1]    [3]    [0]          
12.47/4.12	   lte(s(m),0()) = [0 1 1]m + [0] >= [0] = false()
12.47/4.12	                   [1 1 2]    [1]    [0]          
12.47/4.12	   
12.47/4.12	                    [1 0 1]    [2 0 2]    [3]    [1 0 0]    [1 0 1]    [1]           
12.47/4.12	   lte(s(m),s(n)) = [0 1 1]m + [0 1 1]n + [0] >= [0 1 0]m + [0 1 0]n + [0] = lte(m,n)
12.47/4.12	                    [1 1 2]    [1 0 1]    [0]    [0 1 1]    [0 0 1]    [0]           
12.47/4.12	   
12.47/4.12	                     [1 0 0]    [2]    [1 0 0]    [1]                
12.47/4.12	   insert(nil(),m) = [0 1 0]m + [0] >= [0 1 0]m + [0] = cons(m,nil())
12.47/4.12	                     [1 1 1]    [1]    [1 1 1]    [1]                
12.47/4.12	   
12.47/4.12	                         [1 0 1]    [1 0 0]    [2 1 1]    [2]        [1 0 0]    [1 0 0]    [2]                    
12.47/4.12	   insert(cons(n,l),m) = [1 1 0]l + [0 1 0]m + [1 1 0]n + [1] >= l + [0 1 0]m + [0 1 0]n + [0] = cons(m,cons(n,l))
12.47/4.12	                         [0 0 1]    [1 1 1]    [1 1 1]    [0]        [1 1 1]    [1 1 1]    [0]                    
12.47/4.12	   
12.47/4.12	                         [1 0 1]    [1 0 0]    [2 1 1]    [2]    [1 0 0]    [1 0 1]    [1]           
12.47/4.12	   insert(cons(n,l),m) = [1 1 0]l + [0 1 0]m + [1 1 0]n + [1] >= [0 1 0]m + [0 1 0]n + [0] = lte(m,n)
12.47/4.12	                         [0 0 1]    [1 1 1]    [1 1 1]    [0]    [0 1 1]    [0 0 1]    [0]           
12.47/4.12	   
12.47/4.12	                         [1 0 1]    [1 0 0]    [2 1 1]    [2]    [1 0 1]    [1 0 0]    [1 0 0]    [2]                      
12.47/4.12	   insert(cons(n,l),m) = [1 1 0]l + [0 1 0]m + [1 1 0]n + [1] >= [1 1 0]l + [0 1 0]m + [0 1 0]n + [0] = cons(n,insert(l,m))
12.47/4.12	                         [0 0 1]    [1 1 1]    [1 1 1]    [0]    [0 0 1]    [1 1 1]    [1 1 1]    [0]                      
12.47/4.12	   
12.47/4.12	                    [1]    [1]         
12.47/4.12	   ordered(nil()) = [1] >= [0] = true()
12.47/4.12	                    [2]    [0]         
12.47/4.12	   
12.47/4.12	                            [2 1 1]    [2]    [1]         
12.47/4.12	   ordered(cons(m,nil())) = [0 1 0]m + [1] >= [0] = true()
12.47/4.12	                            [1 1 1]    [2]    [0]         
12.47/4.12	   
12.47/4.12	                                [1 0 1]    [2 1 1]    [2 1 1]    [2]    [1 0 1]    [2 1 1]    [1]                     
12.47/4.12	   ordered(cons(m,cons(n,l))) = [0 1 0]l + [0 1 0]m + [0 1 0]n + [1] >= [0 1 0]l + [0 1 0]n + [1] = ordered(cons(n,l))
12.47/4.12	                                [0 0 1]    [1 1 1]    [1 1 1]    [1]    [0 0 1]    [1 1 1]    [1]                     
12.47/4.12	   
12.47/4.12	                                [1 0 1]    [2 1 1]    [2 1 1]    [2]    [1 0 0]    [1 0 1]    [1]           
12.47/4.12	   ordered(cons(m,cons(n,l))) = [0 1 0]l + [0 1 0]m + [0 1 0]n + [1] >= [0 1 0]m + [0 1 0]n + [0] = lte(m,n)
12.47/4.12	                                [0 0 1]    [1 1 1]    [1 1 1]    [1]    [0 1 1]    [0 0 1]    [0]           
12.47/4.12	   
12.47/4.12	                                [1 0 1]    [2 1 1]    [2 1 1]    [2]    [0]          
12.47/4.12	   ordered(cons(m,cons(n,l))) = [0 1 0]l + [0 1 0]m + [0 1 0]n + [1] >= [0] = false()
12.47/4.12	                                [0 0 1]    [1 1 1]    [1 1 1]    [1]    [0]          
12.47/4.12	   
12.47/4.12	          [1 0 1]    [1]         
12.47/4.12	   s(x) = [0 1 1]x + [0] >= x = x
12.47/4.12	          [1 0 1]    [0]         
12.47/4.12	   
12.47/4.12	                 [1 0 1]    [1 0 0]    [1]         
12.47/4.12	   insert(x,y) = [1 1 0]x + [0 1 0]y + [0] >= x = x
12.47/4.12	                 [0 0 1]    [1 1 1]    [0]         
12.47/4.12	   
12.47/4.12	                 [1 0 1]    [1 0 0]    [1]         
12.47/4.12	   insert(x,y) = [1 1 0]x + [0 1 0]y + [0] >= y = y
12.47/4.12	                 [0 0 1]    [1 1 1]    [0]         
12.47/4.12	   
12.47/4.12	              [1 0 0]    [1 0 1]    [1]         
12.47/4.12	   lte(x,y) = [0 1 0]x + [0 1 0]y + [0] >= x = x
12.47/4.12	              [0 1 1]    [0 0 1]    [0]         
12.47/4.12	   
12.47/4.12	              [1 0 0]    [1 0 1]    [1]         
12.47/4.12	   lte(x,y) = [0 1 0]x + [0 1 0]y + [0] >= y = y
12.47/4.12	              [0 1 1]    [0 0 1]    [0]         
12.47/4.12	   
12.47/4.12	                [1 0 1]    [0]         
12.47/4.12	   ordered(x) = [0 1 0]x + [1] >= x = x
12.47/4.12	                [0 0 1]    [1]         
12.47/4.12	   
12.47/4.12	               [1 0 0]        [1]         
12.47/4.12	   cons(x,y) = [0 1 0]x + y + [0] >= x = x
12.60/4.14	               [1 1 1]        [0]         
12.60/4.14	   
12.60/4.14	               [1 0 0]        [1]         
12.60/4.14	   cons(x,y) = [0 1 0]x + y + [0] >= y = y
12.60/4.14	               [1 1 1]        [0]         
12.60/4.14	  problem:
12.60/4.14	   lte(0(),n) -> true()
12.60/4.14	   insert(cons(n,l),m) -> cons(m,cons(n,l))
12.60/4.14	   insert(cons(n,l),m) -> cons(n,insert(l,m))
12.60/4.14	   ordered(nil()) -> true()
12.60/4.14	   ordered(x) -> x
12.60/4.14	  Matrix Interpretation Processor: dim=3
12.60/4.14	   
12.60/4.14	   interpretation:
12.60/4.14	                      
12.60/4.14	    [ordered](x0) = x0
12.60/4.14	                      ,
12.60/4.14	    
12.60/4.14	                     [1 0 0]     [1 0 0]     [0]
12.60/4.14	    [cons](x0, x1) = [0 0 0]x0 + [0 1 1]x1 + [0]
12.60/4.14	                     [0 0 0]     [0 0 0]     [1],
12.60/4.14	    
12.60/4.14	                       [1 1 1]     [1 0 0]     [0]
12.60/4.14	    [insert](x0, x1) = [0 1 1]x0 + [0 0 0]x1 + [0]
12.60/4.14	                       [0 0 0]     [0 0 0]     [1],
12.60/4.14	    
12.60/4.14	            [1]
12.60/4.14	    [nil] = [0]
12.60/4.14	            [0],
12.60/4.14	    
12.64/4.14	             [0]
12.64/4.14	    [true] = [0]
12.64/4.14	             [0],
12.64/4.14	    
12.64/4.14	                    [1 0 0]     [1 0 0]     [1]
12.64/4.14	    [lte](x0, x1) = [0 0 0]x0 + [0 0 0]x1 + [0]
12.64/4.14	                    [0 0 0]     [0 0 0]     [0],
12.64/4.14	    
12.64/4.14	          [0]
12.64/4.14	    [0] = [0]
12.64/4.14	          [0]
12.64/4.14	   orientation:
12.64/4.14	                 [1 0 0]    [1]    [0]         
12.64/4.14	    lte(0(),n) = [0 0 0]n + [0] >= [0] = true()
12.64/4.14	                 [0 0 0]    [0]    [0]         
12.64/4.14	    
12.64/4.14	                          [1 1 1]    [1 0 0]    [1 0 0]    [1]    [1 0 0]    [1 0 0]    [1 0 0]    [0]                    
12.64/4.14	    insert(cons(n,l),m) = [0 1 1]l + [0 0 0]m + [0 0 0]n + [1] >= [0 1 1]l + [0 0 0]m + [0 0 0]n + [1] = cons(m,cons(n,l))
12.64/4.14	                          [0 0 0]    [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [0 0 0]    [1]                    
12.64/4.14	    
12.64/4.14	                          [1 1 1]    [1 0 0]    [1 0 0]    [1]    [1 1 1]    [1 0 0]    [1 0 0]    [0]                      
12.64/4.14	    insert(cons(n,l),m) = [0 1 1]l + [0 0 0]m + [0 0 0]n + [1] >= [0 1 1]l + [0 0 0]m + [0 0 0]n + [1] = cons(n,insert(l,m))
12.64/4.14	                          [0 0 0]    [0 0 0]    [0 0 0]    [1]    [0 0 0]    [0 0 0]    [0 0 0]    [1]                      
12.64/4.14	    
12.64/4.14	                     [1]    [0]         
12.64/4.14	    ordered(nil()) = [0] >= [0] = true()
12.64/4.14	                     [0]    [0]         
12.64/4.14	    
12.64/4.14	                           
12.64/4.14	    ordered(x) = x >= x = x
12.64/4.14	                           
12.64/4.14	   problem:
12.64/4.14	    ordered(x) -> x
12.64/4.14	   Matrix Interpretation Processor: dim=3
12.64/4.14	    
12.64/4.14	    interpretation:
12.64/4.14	                          [1]
12.64/4.14	     [ordered](x0) = x0 + [0]
12.64/4.14	                          [0]
12.64/4.14	    orientation:
12.64/4.14	                      [1]         
12.64/4.14	     ordered(x) = x + [0] >= x = x
12.64/4.14	                      [0]         
12.64/4.14	    problem:
12.64/4.14	     
12.64/4.14	    Qed
12.64/4.14	All 4 critical pairs are joinable.
12.64/4.14	Overlap: (rule1: insert(cons(z, x), y) -> cons(z, insert(x, y)) <= lte(y, z) = false, rule2: insert(cons(z', x'), y') -> cons(y', cons(z', x')) <= lte(y', z') = true, pos: ε, mgu: {(z,z'), (x,x'), (y,y')})
12.64/4.14	CP: cons(y', cons(z', x')) = cons(z', insert(x', y')) <= lte(y', z') = false, lte(y', z') = true
12.64/4.14	This critical pair is unfeasible.
12.64/4.14	Overlap: (rule1: insert(cons(z, x), y) -> cons(y, cons(z, x)) <= lte(y, z) = true, rule2: insert(cons(z', x'), y') -> cons(z', insert(x', y')) <= lte(y', z') = false, pos: ε, mgu: {(z,z'), (x,x'), (y,y')})
12.64/4.14	CP: cons(z', insert(x', y')) = cons(y', cons(z', x')) <= lte(y', z') = true, lte(y', z') = false
12.64/4.14	This critical pair is unfeasible.
12.64/4.14	Overlap: (rule1: ordered(cons(y, cons(z, x))) -> false <= lte(y, z) = false, rule2: ordered(cons(y', cons(z', x'))) -> ordered(cons(z', x')) <= lte(y', z') = true, pos: ε, mgu: {(y,y'), (z,z'), (x,x')})
12.64/4.14	CP: ordered(cons(z', x')) = false <= lte(y', z') = false, lte(y', z') = true
12.64/4.14	This critical pair is unfeasible.
12.64/4.14	Overlap: (rule1: ordered(cons(y, cons(z, x))) -> ordered(cons(z, x)) <= lte(y, z) = true, rule2: ordered(cons(y', cons(z', x'))) -> false <= lte(y', z') = false, pos: ε, mgu: {(y,y'), (z,z'), (x,x')})
12.64/4.14	CP: false = ordered(cons(z', x')) <= lte(y', z') = true, lte(y', z') = false
12.64/4.14	This critical pair is unfeasible.
12.64/4.14	
12.64/4.17	EOF