Compiling:
	make

Launching:
	./main

Commands:

	- print		{ term list }		[ signature ]
		Prints all the terms contained in the term list
		Example:
			print 		{ f(x,y) ; g(z,f(x,z),z) }		[ f(2),g(3),z(0) ]




	- match		{ (pattern = candidate) list }		[ signature ]
		Finds a substitution such that every cadidate matches its associated pattern
		Example:
			match		{ c(x,e) = c(e,x) ; c(y,y) = c(c(x,x),c(x,x)) }		[ c(2) ]




	- unify		{ equation list }	[signature]
		Return a mgu for the given equation list
		Example:
			unify	 	{ a(x) = a(a(z)) ; c (x, z) = c (x, y) }	[ a(1),c(2) ]




	- testunify	n
		Launch the exponential unify test with depth n
		Example:
			testunify	5




	- rpo		{ rule list }		[ signature ]
		Tries to find a RPO for the rule list
		Example:
			rpo		{ a(s(x)) -> s(b(x)) ; b(s(x)) -> s(a(x)) } 		[ a(1),s(1),b(1) ]




	- criticalpairs		{ rule list }		[ signature ]
		Return the criticals pairs of the rule list
		Example:
			criticalpairs 		{ f(x,g(y,z)) -> g(f(x,y),f(x,z)) ; g(g(x,y),z) -> g(x,g(y,z)) } 	[ f(2),g(2) ]




	- normal 	{ term } 	{ rule list } 		[ signature ]
		Returns the normals forms of a term given terminating system rules
		Example:
			normal         { f(x,e) }          { f(x,f(y,z)) -> f(f(x,y),z) ; f(e,x) -> x ; f(i(x), x) -> x }          [ e(0),f(2),i(1) ]




	- confluence		{ rule list }		[ signature ]
		Checks if the term rewriting system described by the rule list is confluent
		Example:
			confluence 	{ c(x,c(y,z)) -> c(c(x,y),z) ; c(x,ee) -> x ; c(ee,x) -> x } 		[ c(2), ee(0)]




	- findtrs		{ rule list }		[ signature ]
		Tries to complete the rule list to make it a terminating and confluent term TRS
		Example:
			findtrs 	{ f(f(x,y), f(y,z)) = y } 	[ f(2) ]
		WARNING: this method might not terminate
		Example:
			findtrs 	{ *(*(a,b),c) = *(a,*(b,c)) ; *(e,x) = x ; *(i(x),x) = e ; *(y,x) = *(x,y) } 		[ *(2),e(0),i(1) ]