diff --git a/src/ltltest/Makefile.am b/src/ltltest/Makefile.am
index a1c9c0f86..24f06c177 100644
--- a/src/ltltest/Makefile.am
+++ b/src/ltltest/Makefile.am
@@ -30,15 +30,18 @@ check_SCRIPTS = defs
 # Keep this sorted alphabetically.
 check_PROGRAMS = \
   equals \
+  inf \
   ltl2dot \
   ltl2text \
   lunabbrev \
   nenoform \
+  reduc \
   tostring \
   tunabbrev \
-  tunenoform
+  tunenoform 
 
 equals_SOURCES = equals.cc
+inf_SOURCES = inf.cc
 ltl2dot_SOURCES = readltl.cc
 ltl2dot_CPPFLAGS = $(AM_CPPFLAGS) -DDOTTY
 ltl2text_SOURCES = readltl.cc
@@ -46,6 +49,7 @@ lunabbrev_SOURCES = equals.cc
 lunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DLUNABBREV
 nenoform_SOURCES = equals.cc
 nenoform_CPPFLAGS = $(AM_CPPFLAGS) -DNENOFORM
+reduc_SOURCES = reduc.cc
 tostring_SOURCES = tostring.cc
 tunabbrev_SOURCES = equals.cc
 tunabbrev_CPPFLAGS = $(AM_CPPFLAGS) -DTUNABBREV
@@ -57,6 +61,8 @@ EXTRA_DIST = $(TESTS)
 
 # Ordered by strength of the test.  Test basic features first.
 TESTS = \
+  inf.test \
+  reduc.test \
   parse.test \
   parseerr.test \
   equals.test \
diff --git a/src/ltltest/formules.ltl b/src/ltltest/formules.ltl
new file mode 100644
index 000000000..232a21793
--- /dev/null
+++ b/src/ltltest/formules.ltl
@@ -0,0 +1,2172 @@
+(a)U(F(b))
+####
+
+####
+X(X(X((X(X(!q)))U(((X(X(p)))+(X(!q)))R(!q)))))
+(((X(!q))R(!q))+(!p))U(X(X((!q)R(X(X(X(!p)))))))
+(X(p))R((X((!q)+(!q)))R(((p)R(X(!p)))+(X(!q))))
+X(X((((X(!q))*(X(!q)))R(p))*(X(X((!p)*(!q))))))
+((!p)R(q))U(((((q)U(X(p)))U(q))+(X(!p)))R(!p))
+(((!p)R(X(!q)))*(X(p)))R(((!p)R(X(!p)))+(X(!p)))
+(X(!p))+(((X((q)+(q)))R((!p)R(p)))R((!q)U(p)))
+X(X(((!p)+(!q))R(((X((!q)*(p)))R(X(p)))R(!q))))
+((X(p))R(q))R((X(q))*(((X(p))+(X(p)))R(!q)))
+((((q)R(!q))*(p))U(!q))U(((!p)*(X(!q)))+(X(q)))
+(X(!p))*(X(((q)+(X(((!q)+(X(p)))+(!q))))U(q)))
+X(X((X((!q)+(!q)))*((((p)R(!q))*(!p))+(X(!q)))))
+(((!q)*(X(!q)))+((X(q))U(q)))U(((q)U(q))U(p))
+(((q)*(!p))*(p))+((X((X(!p))*((q)R(!q))))+(!q))
+(X(p))R((X(p))R((p)*(((!p)U(q))*((p)R(p)))))
+(((((!q)U(q))U(X(!q)))+(p))+(X(q)))+((p)U(q))
+(X(p))R((((!p)U(q))*(X(!p)))R(X((q)R(X(!q)))))
+(!p)*(((p)U(!p))R((p)*((!p)U((q)*((q)+(!p))))))
+((X(p))*(q))+((p)R(((q)U(X(!p)))U((q)+(p))))
+(!q)*(X(((!p)R((q)+(p)))*((p)*((q)+(X(!q))))))
+(((((X(!q))+(q))*(p))+(q))U(X(p)))R((!q)U(!p))
+(X(q))+(((X(X(q)))U(X((p)+(q))))R((p)+(!q)))
+(p)U((((!p)R(!p))R(X(q)))+((p)*((q)R(X(q)))))
+(((!p)*(q))*(p))+(((((!q)U(!q))R(p))R(!p))R(p))
+(((X(!p))+(q))R(X(q)))R(((X(!p))R(!p))*(X(!p)))
+((X(!q))U(((p)+(p))R(X(X(!q)))))R((X(p))U(!q))
+(((!p)*(X(X(p))))*((p)R((q)+(!q))))+((!q)U(q))
+X(X(X((X(X(p)))U(X((X(q))*((X(p))R(q)))))))
+((X((!q)*((X(!p))*(X(!p)))))+(!q))U((X(p))U(p))
+(X((((X(X(X(!q))))U(!p))U(X(q)))U(X(p))))U(p)
+(((!p)R(q))R(X(!q)))U(X((!q)U((q)R((q)*(p)))))
+(q)U((((q)*(X(q)))U(!p))R(((q)R(X(!q)))+(!p)))
+(((X(!p))*(X(q)))R(X(p)))*(((X(p))+(!q))U(q))
+((X(!q))+(X(p)))U(X((X((X(p))*(X(p))))+(q)))
+((X((p)U((X(q))R(!p))))R(q))*((p)R(X(X(p))))
+X(((X(!q))*((X(q))+(q)))+(((X(!q))R(!q))R(!p)))
+X(X((((p)*((q)R(X(!p))))R(!p))*(X((!p)+(!p)))))
+((p)*(p))*(((X(!p))+(!q))+(X(X(X((!p)U(!p))))))
+(X(((!q)*((X(!p))R(q)))*(!p)))*((X(!q))U(X(q)))
+((X(!q))+(X(X(!q))))U((X((q)+(!q)))U((!q)+(!p)))
+((p)U((X(q))+(!p)))U(X(X((!q)R((X(!q))+(q)))))
+(X(((X(q))U(q))+(X(!q))))R(((p)+(X(p)))R(!p))
+(((!p)R((!p)*(q)))U(!q))U(((X(!p))*(!p))R(X(p)))
+(X(q))R(((X(X((!p)R(q))))*(X((q)+(!p))))+(!q))
+X((X((X(q))*(X(!q))))U(((q)*(!p))+((q)R(!p))))
+X((((q)R(!p))U(X(p)))+((X(X(q)))U((!p)U(!q))))
+(((X(!p))*(p))U(((q)+(!q))+(!p)))U((!q)+(X(p)))
+X((X((p)+(p)))U(((q)*(X(X((!p)U(p)))))R(!q)))
+X((X(((!p)U(X(!q)))U(X(X(!q)))))R((X(p))*(!q)))
+X((!p)+((X(!q))*(((!p)U(!p))+(((p)R(!q))R(q)))))
+(p)+(((X(p))R(!q))*(X(X(((!p)U(X(!p)))R(!q)))))
+(X(!q))+(((q)*(X(p)))R((!q)R(((p)R(p))+(p))))
+(X(((X(!q))U(!q))U(!q)))U(((q)U(q))*((q)+(q)))
+(X((X(!q))R((X((q)R(!q)))+(X(q)))))+((p)U(!q))
+((p)+(q))+(((!p)U(!q))U((X(!q))R((!p)*(X(p)))))
+X(((((q)U(q))R((!q)U(X(!q))))*((!q)U(!q)))+(p))
+(X((X(X((X(q))R((!q)*(p)))))+(!p)))R((p)R(p))
+(X((((!q)*(!p))U((!q)U(p)))+((X(!p))+(p))))R(p)
+(((X((X(!q))U(!q)))+(!p))+((X(!p))+(X(q))))U(!p)
+(X(((!q)U(!q))R(q)))U(X(X(((X(p))+(q))+(!q))))
+(X(X((q)+(!p))))+((X(!q))*(((!p)U(X(p)))+(p)))
+((((q)R(X(p)))R(X(p)))+((!p)U(q)))*(X(X(!q)))
+(((!p)+(!q))R(((!q)R(p))*(p)))+((X(p))*(X(!q)))
+((((!p)+(q))+(X(!p)))*(X((!p)R(!q))))*((q)+(p))
+X((((!p)U(p))R(X((p)+(X(!p)))))U((X(!q))*(!p)))
+((X((X(!p))U(!p)))R(X(!q)))*(X((!q)+((!p)*(!q))))
+((X((!p)+((q)R(q))))U(p))*(((q)U(!p))+(X(q)))
+X((X((((p)*(!q))R(X(p)))*((!q)R(!p))))+(X(!q)))
+(p)U(((!q)U((p)+(q)))*((X(q))R((X(!p))U(q))))
+X(X(((p)+((q)*(q)))*(((X(q))*(p))*(X(q)))))
+(X(((X(X(!p)))U(!q))*((q)+((!p)*(X(p))))))+(p)
+X((((q)+(q))+((q)*(X(p))))*((X(X(q)))R(q)))
+(((q)+(X(p)))U(X(q)))U((X(X(!q)))+(X(X(q))))
+(((q)+(!q))*((X(!p))+(X(X((X(p))U(p))))))+(p)
+(((X(!q))*(!q))R(!p))R((X(X(q)))*((q)U(X(!q))))
+((q)R((q)U(p)))*(X((X(q))R(((!p)R(!q))R(!p))))
+((X(!p))R(X(p)))R((X(!p))*(((p)+(X(q)))R(q)))
+((((p)R(p))U(!p))U(p))U(((p)+(X(!q)))U(X(q)))
+((X(!p))R(X((X(!p))*(!p))))+((q)R((!p)*(X(p))))
+(((!p)R(p))R((!p)+(!q)))R(((q)+((!q)+(p)))R(p))
+X((p)U((((p)+((X(!q))R(p)))*(X(p)))R(X(q))))
+(X(p))U((((!p)*(!p))+(X(!p)))*((!p)R((p)+(q))))
+(((!q)R(p))*((!q)+(!p)))R((X((!q)+(!q)))+(X(!q)))
+((p)R(!q))U((((p)*(p))*(q))*((q)+((!q)R(!p))))
+X(((X(q))U(q))*((q)*((!p)U((X(X(p)))*(p)))))
+(((!p)*(p))U(q))*((X(!p))*((q)+((X(!q))*(q))))
+(!p)*((((X(!q))U(!q))U((X(!q))*(p)))U((!q)U(p)))
+(!q)U((((q)+(X(q)))U((X(!q))*(!q)))R((p)R(!q)))
+(X(X(!p)))+((X(p))*((X(q))U((X(!p))U(X(!q)))))
+((X(!q))*(((X(X(q)))R(X(!p)))U(X(!q))))+(X(!q))
+((q)R((((!p)*(!p))*((p)U(!q)))U(X(X(q)))))*(!q)
+(X(X(!p)))R((X(!q))U(X(X(((!p)U(p))*(X(p))))))
+(X((X(!p))R(p)))R(((!p)+(!q))U((!q)R((!p)U(!p))))
+X(((p)+((p)+(X(q))))R((X(X(X(q))))+(X(q))))
+X(X((p)*(((X(!q))*((p)+(X(!q))))U((p)*(p)))))
+(((!q)U(X(!q)))U(((X((q)*(p)))U(p))+(!p)))+(q)
+((((!p)R((q)R(!q)))U(q))+((!q)U(!q)))+((q)R(p))
+(X(X((p)*((!q)U(q)))))U((X(!p))+(X((!q)R(!p))))
+X(X(X(X((((!q)+((!q)R(!q)))*(!q))+((p)R(!q))))))
+(X((X(!q))U(!q)))U((X(X(!q)))+(X((X(p))+(p))))
+####
+
+####
+((X(p0))U((1)+(p0)))R(X(X(p1)))
+((X(p1))R(X(p0)))*((p2)U(X(1)))
+((X(X(p1)))R(p2))U((X(p1))R(0))
+(X(0))*(X(X((X(p1))U(X(p1)))))
+((X(0))R((p2)+(X(p1))))+(X(p1))
+X(((0)R(X((p2)U(p0))))*(X(0)))
+(X(1))U((X(p2))+((p0)U(X(0))))
+(((p0)U(X((p2)+(p0))))U(p0))*(p0)
+(X(((1)+(p0))U(p0)))+((p0)U(p0))
+(p1)+(((0)U(X(p1)))*(X(X(p1))))
+(1)R((p0)*((X(0))+((p2)*(p2))))
+X(((1)*(X(0)))U((X(0))*(p0)))
+(((X(p1))+(X(p0)))R(X(1)))U(1)
+((p1)*((p1)U(p2)))*((X(1))*(p1))
+(((p1)*(p2))U(X(p1)))*((p2)R(p0))
+X((X(p1))*((X(p1))U((p0)R(p0))))
+((X(p1))+(X(p0)))U((p0)U(X(p2)))
+((X(p1))R((0)R(0)))R((p1)R(p1))
+(((p1)+(p1))*(X(p0)))U((p1)*(p2))
+X((X(p0))R((X(p2))U((p1)*(1))))
+X((((p2)+(p0))+(p0))*((0)U(1)))
+(p2)R(X(((p0)+(1))+((p0)R(p0))))
+(((X(0))R(X(X(1))))U(p0))U(p2)
+(X((X(p1))R(X(p1))))U(X(X(1)))
+((p1)+((p0)*((p0)U(X(0)))))R(p1)
+((1)+(p1))U((p1)R((p0)+(X(p0))))
+(p0)*(((X(X(p0)))U(0))U(X(0)))
+((X(X(X(0))))*((1)U(p0)))*(p1)
+((X(p2))*(1))R(((0)U(p1))U(p1))
+((X(p0))U((p1)U(X(X(p1)))))*(0)
+X(((X(X(p1)))U(p1))U(X(X(p0))))
+(X((p0)+(X((p2)+(p0)))))U(X(p1))
+X(((1)R(p2))+((0)U(X(X(p0)))))
+((1)+(p1))U(((p2)R(X(p2)))R(p0))
+(((1)*((p2)*(X(p1))))+(p2))+(0)
+(X(p2))R((p0)+((X(0))U(X(1))))
+((p2)R(X(p1)))R((p2)*(X(X(p2))))
+(((p0)+(p1))R((p2)*(p2)))U(X(p0))
+((X(p2))U(p0))U(X(X((p2)+(p0))))
+X(X(((X(p1))*(p2))U((p2)U(p1))))
+((p2)R(p1))+(X(X((X(p1))R(p2))))
+X(((X(p2))R(X(p0)))U((p2)*(p0)))
+(((X(p1))+(p1))+(X(p1)))U(X(p1))
+((X(p1))*((X(0))R(X(p2))))R(1)
+((1)U(p0))R(X(((p0)U(p2))U(p0)))
+X((p0)+((((p1)+(p0))R(p1))U(p0)))
+((X(X(X(p1))))R((p0)+(1)))U(p1)
+X(((p0)R((X(p2))R(X(p0))))U(p2))
+(p0)R((p0)R(((X(p1))U(p2))U(p2)))
+(((X(X(1)))*(0))*(1))R(X(p2))
+((X(1))U(X(0)))R(X((p2)R(1)))
+((1)U(X(p2)))*((X(p0))+(X(p0)))
+((X(X(1)))R((X(1))R(p2)))U(p0)
+(0)R(((0)*(p2))+((p0)U(X(1))))
+((X(p2))U(X(p2)))+((X(p1))U(0))
+(p2)R((X((0)+(p1)))U((p2)R(p0)))
+(p2)R(X(((1)U((p1)U(1)))R(0)))
+(((p0)+(X(p0)))U(p0))+((p2)*(p0))
+X(X(X(((p2)U(1))R((0)R(p0)))))
+(X((0)R(X(p1))))U((X(p0))*(p2))
+((p0)*(p1))+((p0)+((X(p1))*(1)))
+(((p1)+(p2))*(X(0)))U((p1)R(p0))
+((p1)U((X(1))*(1)))+(X(X(p0)))
+(0)U(X(((p0)R(1))U((p1)R(p1))))
+(p1)R((X((p1)U(X(p2))))U(X(p0)))
+(X(p2))U(X((X(1))R((p2)*(1))))
+(((X(p0))R(p1))+((p0)+(p2)))R(p1)
+((X(p2))R(p1))+(X(X((p2)U(1))))
+(1)U((p2)R((X(p0))U((0)*(p0))))
+((X(1))U(p0))U((X(p1))U(X(1)))
+(p2)+(X(((p2)*(X(1)))R(X(p2))))
+((X(p1))+(X(p1)))+((p1)+(X(p2)))
+X((((p1)R(p2))U(X(p1)))R(X(p1)))
+(X(p2))*((0)U(X((X(p2))U(p1))))
+((X(p2))R((1)U(p2)))R((p0)U(p1))
+((X(0))R(X(0)))*((p2)U(X(0)))
+(X((X(p0))+((p2)U(0))))+(X(p2))
+(p2)*(X((X(p2))U((p2)U(X(p1)))))
+(X(0))U((p0)*(((0)+(p1))U(0)))
+(((X(p2))+(p1))R(p1))R((p1)*(p2))
+(1)U((X((X(1))+(p2)))R(X(p2)))
+((X(p0))*(p2))*((X(p1))U(X(p1)))
+((X(p1))U(X(p1)))*((p0)+(X(p2)))
+X((X(1))U(((p1)R(p1))U(X(1))))
+(((p0)*(p0))*(1))U(X(X(X(p1))))
+X((X(p2))+((p0)+((X(p1))R(p1))))
+((0)R(X(p1)))+(X((0)R(X(0))))
+((X(p1))*((p2)U(X(1))))U(X(0))
+((p0)R((X(1))+(0)))+((p1)U(0))
+(X(0))U((X((p2)U(X(p0))))U(p1))
+(X(p2))+(((p1)*(X(1)))*(X(p1)))
+((p0)*(p1))R((p2)*((X(p2))U(1)))
+(((X(p0))R(p2))R((p0)+(1)))R(p0)
+(X(p0))R(((p0)U(p2))U((p1)+(0)))
+(((1)R(X(p2)))R(X(p0)))U(X(0))
+(X((((p0)R(p2))R(p2))U(0)))*(p2)
+(X((X((p1)U(p1)))U(X(p2))))U(1)
+(((p0)U((p0)U(0)))R(p0))*(X(1))
+(X((X(p0))*(p2)))+(X((0)+(p2)))
+X(X((X((X(p1))*(X(0))))U(p1)))
+(p0)R(X(X(((p2)R(X(0)))+(p2))))
+((X((p0)*(p1)))U(X(p0)))+(X(p1))
+((X(p0))*(0))R((X(1))R(X(p0)))
+X((p2)U((X(0))*((p0)R(X(p0)))))
+(X(p2))U((X(p1))U((p2)R(X(p1))))
+((p2)+(X((p2)U(p0))))U((p0)+(p2))
+(p2)*(((p1)R(X(p1)))R(X(X(0))))
+((p1)U(X(p2)))R((X(p2))*(X(p1)))
+((X(p2))*(p0))*(((p1)U(0))U(p0))
+(X(X((1)+((p1)+(p2)))))R(X(p0))
+(((p2)+(p1))*(p2))+((p0)R(X(p1)))
+(p2)R((X(X(p2)))*((1)+(X(p2))))
+((X(p0))+((p0)U((p1)*(p2))))U(p2)
+(X(((1)U(0))R((p2)U(1))))R(1)
+(((p0)+(0))U(p2))*((p2)R(X(p2)))
+(X(p0))+(((p2)+(p1))R((p1)R(p1)))
+((X(p0))U(p0))*(((1)R(p0))U(p2))
+(((p1)R(X(p1)))U(X(0)))R(X(p0))
+(p2)*(((X(X(p1)))R(p1))U(X(p1)))
+(X(p0))*(((X(p0))R(X(p0)))R(p0))
+((0)R(p1))R(((p0)U(p0))+(X(p0)))
+(X(X((X(p2))U((p0)U(1)))))R(p1)
+(((p1)*(p1))*((p1)R(p0)))*(X(p2))
+(((X(p0))+(X(p1)))U(X(0)))U(0)
+((X((p1)U(p2)))*(p1))U((0)+(0))
+(((p0)*(p2))U(X(0)))U((p1)+(p0))
+((p0)R(((0)R(0))+(X(p2))))R(p1)
+(((0)*(p2))*(X(p2)))*(X(X(p0)))
+(p2)U(((p1)R(X((p0)R(0))))*(p0))
+(X(((X(p0))+(p1))*(X(p0))))+(p2)
+((X(0))R(0))R((p0)+((0)U(p1)))
+((p0)U(X(p2)))*(((1)*(p0))*(p1))
+((p0)U((p1)+((p0)*(X(p1)))))R(p1)
+(p0)R(X((X((p2)R(p0)))R(X(p1))))
+(X((p2)R(p0)))*((p2)*((p2)R(p2)))
+((p2)U(X(X(p2))))U((0)+(X(p1)))
+(X(((X(p2))R(p1))R(p1)))R(X(1))
+(((X(p0))*(p0))R(X(p2)))*(X(0))
+(X((0)R(X(p2))))*((p2)+(X(p0)))
+(((1)+(p1))*(X(p0)))*((p1)*(p1))
+X(((1)U(X(1)))+((p2)+(X(p1))))
+((p1)*(((p0)+(X(p1)))R(p2)))+(p0)
+((X(p1))*(X(p0)))*((X(p0))+(p1))
+(p2)U(((1)R(p1))U((X(p2))+(p0)))
+(X((X((p1)R(p1)))U(p1)))U(X(p0))
+((X(p2))R((p2)R(1)))U((p1)U(p2))
+(p2)U(((p2)*((p2)U(p0)))+(X(0)))
+((X(p0))U((X(p0))*(X(p0))))*(p0)
+X((X(((1)R(p2))U(X(0))))R(p0))
+X((0)U(((p1)U(X(p1)))+(X(p2))))
+((X(X(p1)))*(p1))*((X(p1))U(p1))
+((((p0)U(p0))R(X(p1)))R(1))+(p0)
+((X(0))U(((p1)R(p0))U(p2)))+(p1)
+((X(1))*(X(p1)))U((p2)R(X(p2)))
+X((X(p1))+(((1)U(p1))*(X(p2))))
+((X(p0))R(1))+((X(p1))*(X(p0)))
+((1)R(((p1)U(p2))U(p1)))*(X(p0))
+((p1)U(X(1)))*(((p2)R(0))U(p2))
+X((((p1)U(p1))U(X(p2)))*(X(0)))
+((X(1))+(p1))*((1)R((p0)+(p1)))
+((X(p0))*((p0)R((p2)U(0))))*(p2)
+((X(p0))*(1))R((p0)*((p1)U(1)))
+(((p1)*(X(p1)))R((0)U(1)))*(p2)
+(p1)*((p1)*((X(X(p0)))*(X(1))))
+(p1)R(((p0)*(p2))*((p2)+(X(1))))
+((X(p2))*((1)R(p0)))R((0)+(p2))
+(((p2)R(p1))+(p2))+((X(p1))U(p2))
+X(X((X(1))+((X(p0))R(X(p2)))))
+((X(p2))R(0))R(X((p2)R(X(1))))
+((((p0)*(p2))R(p1))+(X(1)))U(p1)
+(1)U(((p1)U((p2)R(p2)))U(X(p1)))
+((1)U((p2)U(X(p2))))*(X(X(p0)))
+(((p1)U(X(1)))R(1))U((p0)R(1))
+(1)R((((p0)U(X(p1)))+(p1))R(p2))
+(p2)R((X((X(p2))*(p2)))R(X(p2)))
+(X(((p2)R(p0))U(X(p0))))*(X(p0))
+X((X(p2))R(((0)U(p1))R(X(1))))
+(0)+((X(p2))R(((p0)+(1))R(p2)))
+(X(p2))R(X(((p1)*(X(p2)))*(p0)))
+(((p1)*(1))R(X(p1)))+((p0)R(1))
+(X(X(1)))U((X((p0)R(p0)))U(p0))
+((p0)*((p1)U((X(0))U(p2))))+(0)
+(X((p0)*(X(p0))))R((0)R(X(p1)))
+(((p0)U(p0))*(X((p0)R(p2))))*(p0)
+(((1)*(p1))R(p1))*((p0)U(X(p1)))
+(((0)+(p0))R((p2)R(p0)))U(X(p1))
+((p0)R(p1))+(X(((p0)U(1))R(p1)))
+(((p0)R(p2))U(X(X(p0))))U(X(p1))
+((X(p2))R(X(p2)))*((p0)R(X(p2)))
+(((X(p2))+(1))+((p2)*(p0)))+(p2)
+((X((p0)U(p2)))R(p2))+((p1)R(0))
+(X(p0))+((1)R((X(p1))+(X(p0))))
+(X(X(0)))R(((1)R(p1))+(X(p0)))
+((p0)U(X(0)))U((1)U((p0)+(p0)))
+(X((0)U(p2)))+((p2)+((p1)U(p2)))
+((1)*(0))R((X(p0))*((p1)R(p1)))
+((p1)U((p2)R(p1)))*((p1)*(X(p0)))
+((p0)U(X(p2)))U(X((p0)U(X(p2))))
+((1)U(0))R((p0)*((X(1))R(p2)))
+(X(0))U(((p1)*(X(p1)))*(X(p2)))
+(X(p2))*(((X(p1))U(p2))U(X(p0)))
+(X((1)R(X((p0)U(0)))))*(X(p1))
+(((X(p1))+(1))U(p2))U((p0)R(1))
+((X(0))*((1)U((0)R(p1))))U(0)
+(p0)+(((X(p0))U(X(p1)))U(X(p0)))
+X((X(X((p1)U(X(p0)))))*(X(1)))
+((X(p0))*((p0)U(p0)))*((p1)*(p1))
+(X(p2))R(((X(1))+(p2))+(X(1)))
+(X((p0)+(1)))R(((p0)R(0))+(p1))
+X(((X(p2))*((p1)*(p1)))*(X(p2)))
+((p0)*(X(p1)))*((p1)*((p0)R(p0)))
+X(((X((p2)R(X(p0))))+(p0))+(p1))
+((p2)U(p0))*((X(p0))U((p2)+(0)))
+((0)U(p2))+((X(p1))R((1)U(p0)))
+(X(p2))+((1)R(X((p2)R(X(p2)))))
+X((X(X(p0)))*((p0)R((p0)*(p0))))
+X((p1)R(X((X(p0))R((1)U(p2)))))
+X((((0)U(p1))*(X(p0)))+(X(p1)))
+((p1)U((p0)U(X(p1))))U((p1)U(p0))
+(X(p1))U(X(((X(p1))U(p2))R(p2)))
+X(X((X(X(p0)))U((X(p0))*(p2))))
+((p0)R(p1))R(((p1)R(p2))U(X(p0)))
+((X((p1)R(p1)))U(X(p1)))*(X(p2))
+(((X(p0))U(p2))R((0)R(p0)))U(p0)
+(p2)U(((p2)U(1))U((X(1))+(1)))
+((p0)U((0)+(p0)))R((X(p1))R(p0))
+(((p0)+(X(1)))R(X(p1)))R(X(p1))
+(p1)R((X(p0))+((p0)+((p2)R(p1))))
+((p0)R(1))R((X(X(p1)))*(X(p1)))
+((X(p2))*(X(p1)))U(X((p1)*(p2)))
+(X(p0))*((X(p0))R((X(1))R(p0)))
+((p2)*(p2))R((X(X(0)))U(X(p0)))
+X(((X(p2))U(p2))*((p2)R(X(p2))))
+((p0)R((p1)+(p1)))+((X(p2))*(p0))
+((X(p0))U(p1))+((X(p2))+(X(p1)))
+(X(p1))U((p2)U((X(p2))*(X(p0))))
+((X(1))U(X(X(p2))))*((0)R(p2))
+X(((p1)U(X(p0)))+((X(p2))*(p1)))
+(1)R((((p1)U(p1))R(p1))R(X(p1)))
+X((p0)U((X(p0))U((X(p2))U(p2))))
+((1)+(p1))R(((X(p1))*(p2))U(p1))
+((p0)+(p0))U((p1)R((p2)U(X(p0))))
+(((p0)+(p1))*(p0))*(X(X(X(p1))))
+(X((0)+((p1)*(p2))))U((p0)*(p0))
+X(((0)R((p1)R(0)))U((0)U(p0)))
+(((p0)*(p0))*((p0)R(p2)))*(X(p1))
+(p1)R((((p1)R(p2))+(p0))*(X(p2)))
+((p2)R(((p2)U(p2))+(p1)))*(X(p0))
+X(((p1)R((p1)U(p0)))R((p0)R(p1)))
+(((p2)+(p2))*((X(p1))+(p2)))U(p2)
+((1)U(X(X(p1))))+((p1)+(X(p0)))
+(p2)+(((p2)+(0))+((X(p1))R(p1)))
+((X(0))*(X(X(p0))))R((p0)+(p0))
+X(X(((X(p1))R(p1))U((p2)+(p1))))
+(X(p2))+((X(X(1)))*((p2)*(0)))
+(X(1))*(X(X(X((p2)U(X(p1))))))
+X(((X(X(p2)))+(p1))*(X(X(1))))
+((((p2)U(p2))R(X(p1)))R(p0))*(p0)
+(X(p0))R(((p1)R(X(p0)))R(X(0)))
+((p2)U(1))*((X(p0))R((p2)R(0)))
+(((X(p1))R(p2))U(p1))+((0)*(p1))
+((X(p2))U((X(p1))+(p1)))U(X(1))
+(X(p0))U(X(((p1)*(X(p0)))*(p2)))
+(X(p0))*((0)+(((p0)R(p1))U(p1)))
+(((p2)R(p2))+(X(1)))R((p1)*(p0))
+X(X(((X(p2))R((0)*(p0)))+(0)))
+X(X(((X(X(p0)))*(p1))+(X(p2))))
+X((X(p2))R((p0)*(X((0)+(p1)))))
+(X(p1))*((X(p0))+((p2)R(X(p0))))
+((p2)U((X(p0))*(p1)))R((p2)*(0))
+((X(0))R((p2)+(p2)))*((p0)*(p1))
+((X((0)*(p1)))U((1)U(p1)))U(p2)
+(((p2)+(X(p2)))U((0)U(0)))R(p0)
+(p2)U(((p0)*((0)U(p2)))*(X(1)))
+(((0)U(1))R((X(p2))R(p2)))U(p1)
+X(X((((p2)U(p0))U(p1))*(X(p1))))
+((p1)R(X(p1)))R((X(X(p2)))*(p1))
+((X(X(p2)))U((X(p0))U(p2)))R(0)
+(X((p0)*(p2)))R((p1)+(X(X(p1))))
+X((((p1)R(X(1)))U(X(p2)))R(1))
+(((p0)R(p1))R(p1))R((p1)*(X(p2)))
+X(X(((1)U(1))R((p0)*(X(p1)))))
+((X(p0))R(X(1)))U((X(p0))R(0))
+(X(p0))*(((p2)U(X(0)))U(X(p2)))
+(((1)*(X(p0)))+(X(p0)))*(X(0))
+((X(p0))*(X((X(p0))+(1))))R(0)
+((X(p2))R((p2)U(X(X(p0)))))R(1)
+((p1)*(p0))R((p2)*((p0)U(X(p1))))
+((0)+((X(0))U(p1)))+((p0)U(p0))
+((X(0))U(0))U(X((p0)R(X(p2))))
+(((p2)*(X(p0)))U(p2))R((p1)R(p0))
+(X(X(((p1)*(p2))R(X(p1)))))R(p2)
+(((p2)U(p1))*(p2))+((X(p0))R(1))
+((X(p2))R(p0))R((X(p2))U(X(p2)))
+X((0)U(((p2)R(p2))*((0)+(p2))))
+(X(p2))R((((1)+(p2))R(p1))*(1))
+X((X(0))R(((p0)U(0))R(X(p1))))
+(((1)*(p1))U((p0)*(p0)))U(X(p1))
+((p2)R(X(1)))R(((p2)U(p0))+(p0))
+(X((X(p2))R(p0)))U((p1)+(X(p0)))
+(X((p0)*((p1)R((0)U(p1)))))U(p1)
+((p0)U(p2))*(X((X(X(p1)))R(0)))
+((X(p2))U(X(1)))R((p0)U(X(1)))
+((p2)+(X(p1)))R(((p2)R(p1))*(p1))
+((p0)*(X(p1)))R((1)U((p2)*(p0)))
+(X(p1))U((X(1))+((X(p0))R(p0)))
+(X(p0))R((X(p0))R((0)*(X(p0))))
+(0)+((X(0))*(((p1)U(p2))U(p0)))
+X(((p0)R(p2))*((p0)*((p1)U(p1))))
+(X(p2))R(((X(p0))+(X(p2)))*(p0))
+X((p0)R(((p2)U((p1)R(p0)))*(p2)))
+(X(1))*((((0)+(0))R(p2))+(p2))
+((X(p2))*(1))U((p2)*((p1)U(p2)))
+(p2)U(((X(X(1)))*(1))U(X(1)))
+(p2)+((X(p0))*(((p0)U(p2))*(p0)))
+((X(0))U(p1))*((1)*((1)+(p1)))
+(0)R(((p2)R((p0)*(p0)))R(X(p2)))
+(X((X(0))*(1)))R(X((1)+(p2)))
+X((0)+(X((p0)R((p1)U(X(p2))))))
+(((X(p2))U(p0))*(p2))U((0)U(p0))
+X(((X(p1))+(p1))*((p1)U(X(p1))))
+(X((p0)*(1)))*((X(p1))*(X(p0)))
+X(((X(p0))U(1))R((p1)U(X(p1))))
+(p1)*(((0)*((0)U(X(p0))))+(0))
+((X(X(p0)))R((p2)+(p2)))R(X(p1))
+((0)R(X(p2)))*(X((X(p0))*(p2)))
+((p1)R(p2))U(((p0)R(p2))*(X(p0)))
+(1)U((X(1))R((X(1))+(X(p1))))
+(X(p2))U(((X(1))+(X(p0)))R(0))
+(p2)+((X(X(p0)))+((X(0))U(p1)))
+(0)*(((X(p0))R(X(1)))U(X(p1)))
+X(((p1)+(p0))U((1)R((p1)R(p2))))
+(X(p1))U((X((p0)U(p2)))U(X(p1)))
+(p2)R((1)R((X(p0))+((p2)*(p2))))
+((X(p0))U((1)R((p0)*(p1))))R(p0)
+((X(p0))*(p2))R((p0)+((p2)*(p1)))
+((p0)R(X(p0)))R(X((X(p2))R(p1)))
+X(((X(0))U(0))R((X(p2))*(p2)))
+((X(1))*((p1)*(0)))U((p2)U(p0))
+((p1)*((p2)*(X(X(X(0))))))R(p0)
+(X(X((p1)U(p1))))*((p2)R(X(p1)))
+((p1)*((1)R(p1)))U(X((p2)R(1)))
+(X((p1)U(X(p2))))U((p2)+(X(p1)))
+((0)R(X(X(p0))))+((p0)U(X(p2)))
+((X(p2))R(p1))+((X(p2))U(X(p0)))
+((p0)U(p2))U(X((p2)R(X(X(1)))))
+(p0)R(((p0)*(p0))R((X(p2))+(p1)))
+((p1)U(p1))U((X(p1))R((0)+(p0)))
+(((p0)R(p1))U(p1))R((p0)U(X(p2)))
+((p2)*(p2))R((p1)*(X((p1)U(p0))))
+(X(p0))R((p2)*(((p1)R(1))R(p0)))
+(X(((0)R(1))R(p1)))U((p1)+(p1))
+X((X((p0)+(X(p0))))+((p2)U(p1)))
+(1)R(((p1)*(p1))*((0)U(X(p0))))
+((p0)U(X(p2)))*((X(X(p2)))*(0))
+((p1)U(X(X(0))))U((0)+(X(p2)))
+((X(p2))+((X(p1))R(p1)))R(X(0))
+((p1)R(X(1)))+((X(p1))R(X(p0)))
+(X(X((X(p0))R(0))))*((p1)R(1))
+((X(X(p1)))U(X(p2)))*((0)+(p1))
+((X(X(p2)))*(p0))+((p1)U(X(p0)))
+(((X(p0))R((p1)R(1)))*(p2))*(p1)
+(X(p2))*(((p0)U((1)R(p0)))+(1))
+X(((p0)R(p0))R((X(p2))U(X(p2))))
+(X((X(0))+(p0)))R((p1)*(X(p0)))
+(p2)R((X(1))*((0)U((p1)+(p2))))
+(p0)R(X(((p0)U((p0)U(0)))*(p1)))
+((X(p0))U(X(p2)))+((X(p2))U(1))
+(X(((0)R(X(1)))U(X(p1))))+(p2)
+((p1)+((X(p0))R(p2)))*(X(X(p0)))
+((X(p0))U((X(0))*(1)))U(X(p0))
+(X(p0))R(X(X((X(X(p2)))+(p0))))
+(X((X(p2))U((X(p1))*(p0))))U(p0)
+X(X(X(((X(p0))+(X(p2)))U(p1))))
+(X(p1))*(((p2)+(p1))U((p2)+(1)))
+((1)R(1))R((p1)U((X(p2))R(0)))
+(X((p0)R(p2)))R(((p0)+(p1))R(p2))
+X(((p2)U(X(0)))R(X((1)R(p0))))
+((1)U(p2))*(X((p2)R((p0)+(1))))
+((p1)U(X(0)))*((X(p1))+(X(p2)))
+(p2)R((p2)R(X((X(1))+(X(p2)))))
+X(X(((1)R(X(p2)))R((p0)+(p1))))
+(X(((X(p1))R(p0))U(p1)))U(X(p2))
+((X(0))R(0))R((X(p1))R(X(0)))
+X(((1)R(X(p2)))*((X(p1))+(p0)))
+(X(p2))R(X(((p2)R(p1))*(X(1))))
+((p2)*((p1)R(p0)))*((p1)R(X(p2)))
+(X(p0))U(X(((p2)*(p1))+(X(p2))))
+((p1)R((p2)R(p1)))U((p0)*(X(p1)))
+((1)R(p2))*(X((X(p1))*(X(1))))
+((p1)U(X(p0)))*(((1)R(1))R(p2))
+(X(p2))U((0)+((p0)R((p1)R(1))))
+(((1)+(X(p0)))U(p2))*(X(X(1)))
+(X(X((p0)U(X(p2)))))+((0)*(p1))
+X((((p0)U((p2)+(p2)))R(1))U(p0))
+((p0)R(p1))+((p1)U((p0)+(X(0))))
+(((p0)*(X(p1)))U(0))+((p1)U(p1))
+((((p2)R(X(p0)))+(p1))R(p0))U(p0)
+((p1)U(p2))R((X(p1))R(X(X(0))))
+((X(p2))U((0)R(X(p2))))R(X(p1))
+X((X((p1)R((X(p1))+(p2))))U(p2))
+X((X((p0)U(p0)))U(X(X(X(p0)))))
+((p2)U(X(1)))U(X((p1)+(X(p1))))
+X((X(p0))*(((p0)+(p0))R(X(1))))
+X((X(X((X(p1))*(p1))))*(X(p2)))
+((p1)U(X(1)))R((X(p2))R(X(1)))
+((1)R((X(0))R(X(p0))))U(X(p0))
+(X(p0))R((X(p1))U(X((p1)R(p2))))
+((p2)U(p0))R(((p1)U(p0))U(X(p2)))
+(X(p0))U(((0)U((p2)U(0)))R(p1))
+X((((1)R(p2))*(X(p0)))*(X(p2)))
+(p0)U((((p2)+(1))R(p2))U(X(p1)))
+X(((X(p2))R((p1)*(0)))*(X(p2)))
+((X(p1))*((0)+(X(p1))))U(X(0))
+(X((X(0))R(X(p0))))*((p0)R(p2))
+X((((p0)R(p0))R(X(p2)))R(X(p0)))
+((p0)U((X(p1))+(p1)))*((p1)R(1))
+X((X(X(p0)))R((X(p0))U(X(p2))))
+X(((p0)*(p1))+((p1)R(X(X(p1)))))
+((1)+(0))U(((X(p0))+(p2))+(1))
+((X(p2))R((X(1))U(X(p0))))R(0)
+(X(p0))+(((X(X(1)))*(p2))U(p0))
+X(((0)*(p1))+(((p0)U(p2))*(p0)))
+((p2)R((p1)R(p0)))+((p1)U(X(p2)))
+(((X(p0))+(X(p1)))R(p1))*(X(p0))
+(p2)R(((p2)+(X(p2)))*((p0)+(p1)))
+(((p0)R(p2))+(p1))+((p1)R(X(1)))
+((X(0))U(X(p0)))U((X(p1))+(0))
+((X(p0))+(X((p0)+(p0))))U(X(p1))
+(X((X(1))*((p0)R(p0))))R(X(1))
+((p2)R(p1))U(((X(p1))U(p0))R(p2))
+(X(X((X(0))+(p1))))*((1)U(p1))
+(((p2)R(p1))R((p0)R(X(p1))))U(1)
+((X(p2))U(X(p2)))+((p0)+(X(p2)))
+(X(p1))*((X(p1))*((p1)R(X(p0))))
+(((p0)U(p0))U((X(p2))U(p2)))U(p0)
+(0)R(((1)*(p1))*((0)*(X(p0))))
+(X(p1))+((0)U(((1)R(p0))*(p1)))
+(X(p1))U(((p0)*(X(p0)))*(X(p2)))
+((p2)U(p2))R((1)U((X(p2))U(p2)))
+X((1)U(X(((p0)R(1))R(X(p1)))))
+((p2)R(X(p0)))*(((0)*(p0))*(p1))
+((p1)U(X(p2)))R((0)+((p1)U(p1)))
+(p2)+((X(0))*(X((X(p2))R(p0))))
+((p2)R(p0))+(X((p0)+((p0)U(1))))
+(((1)+(X(p2)))+(p0))*((p0)R(0))
+X(((p1)R(p2))U((X(p0))R(X(1))))
+((p0)U(X(p2)))+((X(p2))R(X(1)))
+((((X(p0))R(p1))R(1))R(p0))U(p1)
+(X((p2)*((X(p2))+(p2))))R(X(p0))
+(X(X(p2)))R(((p0)+(0))U(X(p1)))
+X((X(X(X(p0))))*((p0)+(X(1))))
+(X(p0))+((X(1))+((X(p1))U(p2)))
+X(X((X(X(X(p2))))U(X(X(p0)))))
+X((X((0)U(p0)))R((p0)U(X(p0))))
+((X(p2))U(X(p1)))+((p0)*(X(1)))
+((X(p1))R(p0))U((X(1))+(X(1)))
+(X(p2))U(((X(0))*(X(p0)))R(p1))
+(((p0)*(X(p0)))U(X(p0)))U(X(p1))
+X((((1)R((p1)U(p2)))U(p0))R(p0))
+((p0)U((p0)R(p0)))+((p0)R(X(1)))
+(X(X((1)R(1))))R((0)U(X(p2)))
+(p2)R(((X(1))U(p0))+((p1)R(p2)))
+(((p2)*(X(p1)))R((p2)+(p1)))R(p2)
+X(((p0)*(p1))+((p1)+((p2)*(p0))))
+(X(1))R((X(1))U((0)+(X(1))))
+X(((0)R(X(1)))U(X((0)U(p1))))
+(p0)R(((0)U((0)+(p2)))+(X(1)))
+((X(p1))+((0)R(X(p2))))U(X(0))
+((p0)R((X(p0))*(1)))+((p1)U(p1))
+(p0)*((p2)+((X((p1)U(p2)))U(p0)))
+((p2)R(p2))U((X(0))R(X(X(p0))))
+((0)*((X(p1))R(p0)))R((1)U(p0))
+((0)U(X(0)))R((X(0))R(X(0)))
+((p0)U(X((X(p1))R(p1))))R(X(1))
+(X(p2))U(((p1)+(p2))R((1)R(1)))
+(X((p2)*(X(p0))))R((X(p2))+(p1))
+X(((X(p1))R(X(p0)))*((0)R(p2)))
+((p1)U((X(1))+(p0)))U((p0)*(0))
+(X(p1))*((p0)U(((p1)R(1))*(p0)))
+(((X(0))U(X(p1)))R(1))R(X(0))
+X(((X(0))*(p0))R((X(p0))*(p1)))
+((p2)R(((p1)*(p0))R(X(p2))))U(p1)
+((p2)U((p2)R(X(p1))))R(X(X(p2)))
+((X(p1))+((p0)U(1)))+((0)*(0))
+(X(X((p1)U((0)+(p1)))))+(X(p2))
+(((p2)R(p1))+((p2)+(p2)))R(X(p2))
+(((p0)R(X(p0)))*((p0)U(0)))+(p2)
+((X(p0))+((p2)+(0)))*(X(X(p0)))
+(0)*((((p0)*(p1))R(p0))U(X(p0)))
+(X(X((p0)+(p2))))U((X(p2))U(p1))
+(((0)U(p0))R(X(0)))U((p2)R(p0))
+((p2)R((p0)*(p0)))R((X(p0))R(0))
+X(((p1)R(X(p1)))U((X(p1))R(0)))
+(X(X(p0)))+(((X(p0))U(p2))*(p0))
+X(((p1)U((p1)+(X(p2))))U(X(p0)))
+((1)R(0))U(((p1)+(0))U(X(p2)))
+(X(p1))U(X(((p0)*(X(p1)))+(p0)))
+(p1)R(((X(p2))+(X(p2)))U(X(p1)))
+((p1)U(p0))U((X(p2))R(X(X(p1))))
+((p2)R(p0))+((X(p2))+((p1)*(1)))
+((p1)R((p2)R(p2)))+((p0)*(X(p0)))
+((p1)U((X(X(p2)))R(p2)))U(X(p2))
+((p2)U(1))*(((X(p0))*(p0))U(1))
+(((0)R(p1))+(X(p1)))U((p1)+(p0))
+X((((p2)U(p1))+(p2))+(X(X(1))))
+(p0)R(X((((p2)+(p1))*(0))*(p2)))
+(p2)U((X(p2))*((X(p0))R(X(p1))))
+(p1)R(((p1)R(0))*((0)U(X(1))))
+((X(p0))U(p1))U((p2)U((p0)+(p0)))
+X(((p1)U(X(X(p0))))R((p0)U(p2)))
+((X(1))*(p1))R((0)*((p1)R(p1)))
+((p2)U(X(X(X(p2)))))+(X(X(0)))
+X((p1)*((p0)U((X(p2))+(X(p0)))))
+X((0)+((p2)U((X(0))R(X(p0)))))
+(((0)*(X(p0)))+(0))R((p1)U(0))
+X((((p1)+(p0))+(p0))*((1)U(0)))
+(p0)R(X((X(p1))*((p2)U(X(p0)))))
+(p1)U((p2)*(((X(p2))R(p1))+(p0)))
+((1)R(X(p1)))+((X(p1))U(X(1)))
+((X(p1))R(X(1)))+((p1)R(X(1)))
+(X((p1)R((p0)U(X(X(p2))))))R(p2)
+((X(1))+(X(p1)))*((p2)U(X(p2)))
+(((p0)+(0))R(1))R(X(X(X(p0))))
+X((X(p1))*((X(p0))U((p2)U(1))))
+(p2)R(X(((1)U((p2)+(1)))+(p1)))
+((p0)R(0))U(((X(1))U(p0))R(p0))
+((X(p0))R(p2))R(((0)*(0))*(p0))
+X(((0)R(p1))R((X(p2))R(X(p2))))
+(p2)*(X((X((p1)*(p0)))+(X(p0))))
+X(X(((X(p0))U((1)R(p2)))U(p0)))
+(((X(1))R(p0))U(p0))R((1)*(p0))
+((0)+((p0)R(1)))R((p1)R(X(p1)))
+(X(p2))R((X((0)R(1)))*(X(p0)))
+(X((0)+(0)))*(((0)+(p2))+(0))
+(X(((p0)R(0))R((p2)U(p0))))U(0)
+(((p2)+(X(X(X(p2)))))U(p1))R(p2)
+(X(p2))R((p1)*((X(p2))R(X(p1))))
+((p0)R(p2))U((X(p1))U(X(X(p0))))
+(X(p1))*(X((1)*((p1)R(X(p0)))))
+((p2)*(X((p2)+(X(p1)))))*(X(p0))
+((0)U(X(p0)))U(((1)+(p0))R(p2))
+(p1)+((X(1))U((X(X(p0)))+(0)))
+(0)*((X(p2))R(((p2)*(0))*(p2)))
+((X(1))U(p0))+((X(p2))+(X(1)))
+((X(1))U(1))*((X(p2))*(X(p1)))
+((p1)R(1))+((X((1)+(p0)))R(p1))
+(p0)U((X(0))*((X(p2))R(X(p2))))
+X((X((X(p1))U(X(X(p1)))))U(0))
+((1)U(p2))U((X(p2))U((p2)U(p1)))
+X(((X(p1))U(0))+((1)+(X(p2))))
+((X(p1))*(X(X(X(1)))))R(X(p2))
+(0)U(X(((p0)U(p0))R(X(X(p2)))))
+((p1)R(((p0)*(p2))U(p0)))U(X(p0))
+(((p1)*(0))+(p2))*(X((p0)R(0)))
+((X(p0))R(p2))*(X(X(X(X(0)))))
+X(X((X(p1))U(X((X(p0))R(p0)))))
+((p1)U(p0))R(((p0)U(p2))U(X(p2)))
+(X((X(0))+(X(p0))))U((p1)U(p2))
+(0)U((((p2)*(1))*(X(p0)))*(0))
+X(((X(p0))+((X(p1))R(p2)))U(1))
+(((p2)R(X(p2)))R(p2))*((p1)+(p0))
+((p1)+(p1))U(((p1)R(p1))+(X(p2)))
+(((X(p0))R((p2)*(1)))R(p2))R(1)
+((((p0)U(p2))+(X(p2)))+(p1))*(p1)
+((X(p1))R(X(p0)))U((X(p1))+(p2))
+X(((p1)*(p2))U((X(p1))+(X(p2))))
+X(((p0)R((p0)*(p0)))U(X(X(p1))))
+(p0)R((X(p0))U((0)*((p0)R(p2))))
+X((X((X(p2))+(p2)))U((p2)+(p1)))
+((p2)*(X(p0)))U((p2)*((p1)R(p1)))
+((X(p1))R(p2))U((X(p0))+(X(p1)))
+X(((p1)R(1))*((0)R((p0)+(p1))))
+(X(p2))*((X(1))U(X(X(X(0)))))
+(((0)+(p1))*(X(0)))*((p1)R(p2))
+X(X(((p0)R(X(0)))R((p1)U(p2))))
+(p0)R(X(((X(0))U(X(p1)))U(1)))
+X((((0)R(1))U((0)R(0)))U(p1))
+((p1)*(X(1)))*((X(p0))R(X(p1)))
+(((p1)R(X(X(p2))))R(X(p2)))U(p1)
+((p2)U(p2))U(((1)U(p2))+(X(p1)))
+((p0)U(X(p0)))+((p2)R(X(X(p1))))
+(((X(p2))+(p2))+(p2))*((0)U(0))
+X(((X(X(X(p1))))*(X(0)))R(p1))
+(X(1))U(((p2)U((p2)*(1)))U(p0))
+(X(p0))R((X(X(p2)))+((0)*(p1)))
+X((((p1)U(p0))R((1)+(p0)))R(1))
+(p0)+(X(((p0)*(p2))R((0)R(1))))
+(X(p1))U((0)*((X(p0))R(X(p0))))
+(((p1)+(p0))+(X(p0)))R((1)R(p0))
+(p0)U((((1)U(p0))R(p0))U(X(0)))
+X((X(p2))+(((1)U(X(0)))*(1)))
+((X(p0))*((0)+(p1)))+(X(X(p2)))
+(X(X(1)))+((1)R((X(p1))U(p1)))
+(X((X(0))U(X(0))))*((p1)+(p1))
+(((p1)*(X(p2)))R((p0)+(p0)))U(p0)
+(X(X(p0)))+((X(X(p1)))*(X(p1)))
+(X(p1))R(X(X((X(X(p0)))R(p2))))
+(X(p0))*(X(X((X(p1))+(X(0)))))
+(p2)R(((p1)+(X(p2)))*((p0)U(1)))
+((X(0))R(X(p0)))U(X((p0)*(p0)))
+((X(p2))R((X(p0))U(X(1))))+(p0)
+(((p2)U(p2))U(X(p2)))+((p2)R(p2))
+X((p2)*(((X(p0))R(0))U(X(p2))))
+(((X(p2))*((p0)+(p2)))R(0))U(p0)
+(X((X(p0))U(p1)))U((p1)U(X(p2)))
+(((p1)U(p1))R(p0))R((X(p0))+(1))
+(X(X(X(X(p1)))))U((X(p2))R(p0))
+(((p1)R(X(p1)))*(p1))U((p0)U(p2))
+X((p2)+((p0)*((X(p0))R(X(p1)))))
+((p1)U(1))R(((0)+(X(p2)))U(p0))
+((p0)*((X(p0))*(0)))*((p0)+(p2))
+((p1)U(p1))U(((p2)*(X(1)))U(p0))
+((X(p0))R((p0)*(p0)))+((p0)*(p1))
+X(X(X(((p1)R(X(X(1))))U(p1))))
+((X(1))+(p0))R(X((0)R(X(1))))
+(X((p0)*(p2)))+(((p0)*(p0))R(p1))
+((p2)R(X(p2)))*(X((X(p2))*(1)))
+(((p1)*(p0))R(p1))R((X(0))R(p0))
+(X((1)R((p0)R(0))))U((p0)U(p1))
+(X(p0))+(X((1)U(X((p2)R(p0)))))
+(X((X(p0))R(X(0))))U((p2)*(p0))
+((X(p1))+(0))*((p2)U((p0)R(p0)))
+((X(1))R(((p2)R(p1))U(p1)))U(0)
+((1)*(X(X(p2))))R(X((p2)U(p0)))
+(X((p1)R(1)))*(X((X(0))+(p1)))
+(((0)R(p1))U(X(p0)))U((p2)+(p2))
+((0)+(X(p0)))*(((1)+(p1))+(p1))
+((X(p2))R(X(p0)))+((X(p2))U(p1))
+(X(p0))+(((X(1))*(p2))+(X(0)))
+((X(p2))*((X(p0))U(1)))+(X(p0))
+X((p1)*((p1)*((X(p2))R(X(p1)))))
+(((X(p2))R((p1)R(p0)))U(p0))*(p1)
+(X(1))+(X(((p1)U(p1))U(X(0))))
+(p1)U((X(X(p1)))R((p0)U(X(p1))))
+((X(p2))+((p1)R(1)))U((p0)+(p2))
+(((0)R(p1))R((p1)*(X(p1))))U(1)
+((1)+(X(p2)))+((p2)+(X(X(0))))
+((X(p2))U((X(p1))*(1)))*(X(p1))
+(X(p1))+(((p0)R((p2)U(p0)))U(p2))
+(1)+(X((X(p2))+((1)U(X(1)))))
+(X((p1)*(1)))R(((1)+(p1))*(p2))
+((X(1))U((p1)*(X(0))))R(X(0))
+((p1)+((p1)+(p2)))U((p0)*(X(p1)))
+((p0)R((p0)U(p1)))U((X(p2))U(p1))
+(X(X(p2)))U((0)+((p2)R(X(1))))
+(X((p0)+(((p2)U(p2))U(p1))))U(p0)
+(X(p1))R(((X(0))*(X(p0)))R(1))
+(0)U((X(p1))U((p1)U((p0)+(p1))))
+X((((p2)R(p1))+((0)U(p2)))+(1))
+((1)*((X(p1))R(X(1))))R(X(p1))
+(((p1)*(X(0)))R(X(X(0))))+(p2)
+(((X(p0))R(X(p2)))R(X(p0)))U(p2)
+(X(X(((p1)R(p2))R(1))))U(X(0))
+((X(1))R(X(p2)))R((p1)R(X(p2)))
+(X(X(X(p0))))R((X(p0))*(X(p1)))
+X(X(((p2)U((p0)+(0)))*(X(p2))))
+X((X(p1))+((X(X(p1)))R(X(p1))))
+(X(p1))U(((X(p2))U(X(p1)))R(1))
+((p1)+(1))*(((X(p2))R(1))R(0))
+(X((1)*(1)))*(((0)*(1))R(p2))
+(X(X((p0)*(0))))+((X(p2))R(p2))
+((X(p0))R(X(p1)))U((X(p0))U(p1))
+((X(1))U(1))*((X(p1))R(X(p0)))
+((X(X(p2)))*((X(p2))U(p1)))U(p2)
+((X(p0))+(X((p1)*(p1))))+(X(0))
+((X(0))R(X(p2)))U((p1)*(X(p0)))
+((p1)*(p1))R((X(0))*(X(X(p2))))
+X((((p2)U(p0))R((p2)U(p2)))*(0))
+((X(X(1)))*(X(p2)))U(X(X(p1)))
+(X(p2))R(((p1)U(X(0)))R(X(1)))
+(((p1)+(X(p0)))R(p0))*((p1)+(p1))
+(((p0)U(p1))U(X(p2)))U((p2)U(p1))
+(X((p0)R(X(p1))))*((X(0))+(0))
+(p1)U((((X(p0))U(p0))+(p0))+(1))
+(p1)+(X(((1)U(0))U((p0)R(p2))))
+((p1)R(p2))*(((p0)R(p2))R(X(p0)))
+((X(1))R(X((p0)*(X(p1)))))R(p0)
+(X((X(p2))R((0)+(X(p0)))))R(p2)
+(X(p2))U(X(((1)*(X(p1)))+(p0)))
+X(X((((p1)U(X(1)))U(p2))U(1)))
+((X(X(0)))U(1))+((p0)*(X(p0)))
+(p2)U(X((((1)R(p0))*(p0))+(p2)))
+((p1)+(p0))+(((p2)*(0))+(X(1)))
+(X(p2))R(((p0)R(1))R((p0)R(p1)))
+((p1)R(p0))R(((p2)U(p2))*(X(0)))
+X((((p2)U(p0))+((p1)U(p2)))U(p1))
+X(((X(p0))U(1))*((p1)R(X(0))))
+(((1)R((p2)U(p2)))R(p0))U(X(0))
+(((X(p0))U(X(p2)))R(p2))+(X(p0))
+X((X(p1))U(((X(p0))U(p0))U(0)))
+(X(p2))U((((p2)*(0))U(0))U(p1))
+X((X(p2))U(X((X(p1))+(X(0)))))
+((p2)R(0))U(X((p1)U((p2)R(p2))))
+(X((X(p0))+((X(0))U(p0))))+(p0)
+(((p0)U(p2))R(p2))+((X(p0))U(p0))
+X((X(p0))*((p1)U((p0)+(X(p1)))))
+X(((p1)+(X(p2)))U((X(p0))R(p1)))
+X(((p2)+(X(p1)))R((p1)U(X(p0))))
+X(((X(1))*(X(p2)))U((p0)U(p2)))
+((1)U(0))*((p0)R((X(p2))*(p2)))
+(X(p1))U(((p1)R(p1))U((p2)U(p0)))
+((p0)U(0))U(((0)R(0))*(X(p2)))
+((p1)*(p2))U((X(p2))R((p2)U(p2)))
+(0)U((((p1)U(p0))*(p0))R(X(p0)))
+X((X(((p1)+(X(p0)))U(0)))+(0))
+(X(p1))*(((X(p0))+(0))R(X(0)))
+((X(X(p2)))R(p1))U((X(p1))R(p0))
+(X((p0)U(p1)))*((X(p1))U(X(1)))
+(((X(0))U(0))R(p2))R((p2)+(p1))
+((X(p2))U(X(p1)))+((X(1))R(p1))
+((p2)U(0))R(((p1)U(p0))U(X(1)))
+(((X(0))U(X(1)))*(X(p0)))*(p2)
+((p2)R(p2))+((X(p1))R((p2)U(p1)))
+(p0)U((X(1))R((p0)+((p0)*(0))))
+(((p0)*(p2))*(p1))+((X(0))R(p1))
+(((p0)U((p2)R(p0)))U(X(0)))U(p1)
+((X((X(p1))U(0)))*(p1))R(X(p2))
+((X(p2))U(p0))U(((p1)U(1))R(p1))
+(((X(p0))+(p1))+(p1))U((1)+(1))
+((p1)*(1))+((X(p0))R((p1)+(p2)))
+(((p2)U(p2))+(X(p2)))R((p2)R(0))
+(X(X(X((p1)R(p0)))))R((p0)U(p1))
+((p2)U(X(1)))R(((p1)U(p1))U(p2))
+((X(p1))U(p0))R((X(p1))+(X(1)))
+(((X(p0))R((1)*(p2)))U(p2))*(p0)
+(((X(X(p1)))R(p2))R(X(p0)))R(1)
+(X(1))+(((p1)*(X(1)))*(X(p2)))
+X((X(p1))R((p1)U((p1)R(X(p2)))))
+((p2)*(p1))R((X(p0))*((p1)*(p1)))
+((p1)U(X(p2)))U((p2)*((p2)R(p2)))
+((p1)U((X(p1))R(p0)))+(X(X(p0)))
+X(((0)+((X(0))U(p2)))U(X(p0)))
+((0)*(p2))U((X(p2))*((0)*(p1)))
+((X(0))U(1))+(((p1)+(p2))U(1))
+((X(p0))*((X(p1))R(X(p0))))*(p1)
+((X(0))R(p2))U((X(p0))*(X(1)))
+(((X(p2))R(X(p2)))U(p2))R(X(p0))
+(X(((p2)*(p1))*(p0)))+((p0)U(p2))
+X((X(p0))U((X(p2))*((p2)R(0))))
+(((X(p0))+(1))U(p0))R((p2)R(p1))
+(((X(p0))U(1))+(X(X(1))))R(p1)
+((p0)U(X(p0)))U((X(X(p2)))+(p0))
+X((((p1)R(p1))U(p1))+((p1)*(p2)))
+((p0)R(0))*((p1)*((0)+(X(p2))))
+(((p0)U(p1))U((p0)+(p1)))*(X(p1))
+X(((p0)U(X(p2)))+((p0)R(X(p1))))
+(p1)U((X(p2))*((X(p0))U(X(p2))))
+(((X(1))R(0))U(X(p2)))R(X(p1))
+(p0)U((1)*(((X(p0))U(0))U(p0)))
+X((p1)R(((0)U(p2))+((p1)*(1))))
+((X(p1))R(p0))R(((p0)U(0))R(p2))
+((X(0))R((1)R(p0)))R((p2)R(p2))
+(p1)R(X(((p2)*(p0))U((1)U(p1))))
+(((p1)+(p1))U(p0))R((p0)*(X(p1)))
+(X((0)*((p0)R(X(p0)))))U(X(p0))
+((X(1))*(X(p2)))R((p0)U(X(p0)))
+(p2)*((X(0))+((X(p0))R(X(1))))
+((X(p2))+((X(p0))+(p1)))U(X(p1))
+X((X((p2)*((p2)R(p2))))U(X(0)))
+(p1)*(X(((p1)R(1))*((p0)U(p2))))
+(1)R((X(p0))U((X(1))+(X(p1))))
+((p1)*((X(p1))*(X(p1))))R(X(p0))
+((p1)R(p2))U(((p0)+(p2))U(X(p2)))
+((1)*(p1))U(((p0)*(p2))U(X(p1)))
+((X(p2))U(p1))R((0)*((p2)U(p0)))
+((X(p2))U((0)U((0)+(p2))))R(p0)
+((X(p0))*(X(p0)))R((X(p1))*(1))
+(((p0)U(p2))R((p2)R(1)))U(X(1))
+X(X((X(p1))+((p2)R((0)R(0)))))
+((1)U((p0)U(p0)))U((X(p2))R(0))
+((p0)*(X(p1)))U((X(p2))+(X(p1)))
+X(((p2)+(p1))*((X(p1))U(X(p1))))
+((((p0)+(X(p2)))U(p0))U(p0))U(p2)
+(X(X(X((0)U(p1)))))*((p1)*(1))
+((p1)U(1))*(X((p0)U((p1)+(p0))))
+(((p2)R(X(p1)))U(X(p0)))U(X(p2))
+(X(0))+(((p2)R(X(p2)))R(X(p0)))
+X(X(((p1)R(p2))U((X(p0))+(p2))))
+((p2)+(1))*((X(p2))+(X(X(1))))
+(0)U((p0)+(X((X(p2))R(X(p2)))))
+((X(p0))+((p0)*(X(0))))*(X(p1))
+X(((X(p1))U(X(X(p0))))U(X(p0)))
+(((p0)+(0))R((p2)U(X(p1))))*(p0)
+X((X(X((0)R(p1))))U(X(X(p0))))
+((p0)+(p1))R(((p2)+(X(p1)))*(p1))
+(p1)*(X(((p2)U(X(p2)))U(X(p1))))
+(((p2)+(p1))R((p2)U(p0)))R(X(p1))
+X(X((X(p2))+(X((1)U(X(p1))))))
+(X(p2))+(((X(1))U(p2))U(X(p2)))
+((X(p2))+(X(p0)))+((1)+(X(p2)))
+((1)*(p2))*(X((p1)U((p1)+(1))))
+(X(p2))+(X((X(X(p2)))R(X(p2))))
+((p1)R((X(0))R(X(p0))))U(X(p2))
+X(((X(p2))+(X(p0)))+((p1)U(p2)))
+X(((0)R(p0))R(((1)U(p2))R(p1)))
+((p2)*(p1))R(((p1)R(X(p0)))R(p2))
+X((((p1)R(X(X(p1))))U(p2))R(p0))
+((p1)+(X(1)))+((p2)+(X(X(0))))
+(((X(0))+(p2))R(p0))R((p2)U(p2))
+(((p2)R(X(p0)))U((p1)*(1)))+(p1)
+(p0)R(((p0)U(X(p1)))+((0)R(p0)))
+(((X(p0))*(p0))+(1))+((p1)U(p2))
+((0)U(X(p2)))*((X(1))+(X(p2)))
+(((p2)U(p2))R(X(p0)))R((1)+(p2))
+(X((X(p1))R((0)R(p1))))U(X(p0))
+((X(p1))+(X(p2)))*((X(1))*(0))
+((X(p2))+(1))*((X(1))+(X(p0)))
+((X(p2))R(X(X(p2))))+((p2)+(p0))
+((X(p2))*(X(0)))R((1)+(X(p1)))
+(X(p0))+((X(X(p0)))+(X(X(p2))))
+((X(p1))*(p2))U((X(p2))*(X(p0)))
+((1)U(X(p2)))R(((p1)U(p0))*(p1))
+(X(((p2)+(p2))*(p0)))U((1)U(p2))
+(X((X(1))+((X(p1))R(1))))*(p0)
+(X(p2))R((p2)U((X(0))+(X(1))))
+(X((p1)R(X(X(p0)))))U((p2)U(0))
+(X((1)R(p1)))R((X(p0))R(X(p1)))
+(((p2)*(X(p2)))R(1))*((p1)U(p2))
+(X((((p1)U(p0))U(p1))+(1)))U(p1)
+X((X((p0)*((p1)+(0))))U(X(p1)))
+X(((p2)R((X(p0))+(p2)))*(X(p1)))
+(p0)+(((X(1))*(p1))R((p0)*(p1)))
+((X(p2))R(X(p0)))R((X(p2))U(p0))
+X((X((p1)U(p0)))U((X(p1))U(1)))
+(X(p2))*((X(1))+((X(0))U(p0)))
+((p1)R(p1))R(((1)U(p1))+(X(p1)))
+(X((X(0))*(X(p2))))U((p2)+(p2))
+X(((X(p1))U((p1)U(p1)))U(X(p0)))
+(X(p1))+((X(1))R((X(p0))+(p2)))
+(X(p1))U(X(((p2)U(X(p0)))U(p2)))
+X(((p0)R((p2)U(1)))R((p2)*(1)))
+(((p0)U(p2))+((p2)U(1)))U(X(p1))
+((X(0))U(p2))U(X((X(p1))R(p1)))
+((1)R((1)*(X(p2))))+((p1)R(p2))
+(((X(1))R(1))U((0)R(1)))R(p0)
+((p0)R(1))U(X((X(p0))U(X(p0))))
+X(X(((X(X(p1)))U(X(1)))U(p0)))
+((X(p1))R((p1)U(p1)))*((p1)*(p1))
+((p2)+(p1))U((X(p1))R((p2)U(p2)))
+X((X(p0))R((1)R((X(0))R(p1))))
+(X(X((p0)U(X(p2)))))U(X(X(p1)))
+X((p1)+((1)+((X(p2))+(X(p2)))))
+(1)U(X((X((1)R(X(p0))))+(p1)))
+X((X(0))R((X(p2))+((1)*(p2))))
+(X(p2))R((X(p1))R(X((p2)*(p2))))
+(X(0))U(X(((p1)+(0))+(X(p2))))
+((X(p0))+((X(p1))+(p2)))U(X(p1))
+((X(p0))R(X(p0)))R((X(p0))+(p0))
+((p2)R(X(1)))R(X((X(p2))U(p1)))
+(((p1)+(X(0)))U(1))R((p1)U(p1))
+(((p0)U(1))*(X(0)))R((1)U(p2))
+((0)U(((p1)U(p0))*(p2)))R(X(p2))
+(X((p0)+(p0)))R(((p1)U(p0))R(p0))
+(((X(p0))+(1))U(X(X(1))))R(0)
+(p1)R(X((X(p0))*((p1)U(X(p2)))))
+((((p1)R(1))R(p0))U(X(p1)))R(p2)
+(1)+((p2)*(((p2)U(0))R(X(1))))
+((X(0))R(X(p0)))U((1)R(X(1)))
+(X(X((0)*(X(p0)))))+((p0)*(p1))
+((X(p2))+(X(p1)))R((X(p2))U(0))
+(X((X(p2))+(X(p0))))*((p1)R(p2))
+((p1)R(X(p1)))R(((p0)+(p1))U(p2))
+X((X(X(p1)))U((p1)U((p0)U(0))))
+(p1)U((p2)U((X(p1))R((p2)+(p1))))
+X((1)R((X((X(1))+(p0)))+(p2)))
+(X((1)*(p0)))+((X(p0))+(X(p2)))
+(((p1)*(0))U((p2)U(p1)))U(X(1))
+((X(p1))+(p2))+(X((X(p2))*(p2)))
+((p0)*(p2))R(((p2)*(p0))U(X(1)))
+X(((X((p2)R(p1)))U(X(p0)))+(p1))
+(1)+(X(((0)R(0))+(X(X(0)))))
+X(((p1)U(0))*((X(p2))R(X(1))))
+((p0)R(p2))R((X((p0)+(p0)))U(p0))
+(X(p1))R(((p2)+(0))*((p1)+(1)))
+(X(0))R(((p1)R(p1))R(X(X(p0))))
+((((X(p2))+(p2))+(1))*(p2))U(p1)
+(((p1)U(p2))R((p2)U(p2)))R(X(1))
+(X(1))+(X(((p0)+(p1))U(X(p1))))
+((X(X(p0)))*((1)U(p1)))U(X(p1))
+(X(1))R(X((X(X(1)))+(X(p1))))
+((p0)*(p2))U((X(p0))U((0)+(p1)))
+(((p0)U((X(0))*(p2)))U(p0))R(0)
+(p2)R((p2)*((p1)*((p2)+(X(p2)))))
+(X(((p0)+(0))U(X(p0))))*(X(p0))
+X((X((X(1))R(p2)))*((p2)+(1)))
+(p1)R((X((X(p2))U(X(p0))))+(p1))
+((X(X(X(p0))))R(X(p0)))*(X(0))
+((p2)U((p1)*(p2)))R((X(1))U(p2))
+((p1)U(X(p2)))R(X((p1)+(X(p1))))
+((p0)*(p2))+((0)+(X((p1)R(p1))))
+(X((1)R(X(p2))))*(X((p1)+(0)))
+((X((p1)R((p2)U(p2))))+(1))+(p2)
+(X(1))+(((p1)U(p0))R((p2)+(p1)))
+((0)*(p0))R(((p1)R(p1))+(X(p0)))
+X(((p1)R(p1))U((p0)R((p2)U(p0))))
+((X(p0))R((p2)U(p1)))R((1)*(1))
+(X(0))*(X(((X(p0))U(0))*(p0)))
+((0)U(p1))R((p1)U((0)R(X(p1))))
+(X((X((p1)R(0)))U(p2)))R(X(p1))
+X((p2)U((X(1))U((p2)*(X(0)))))
+(X(X(p0)))*((p2)U(X((p1)R(p2))))
+(X(1))U(((p2)R(p1))+((p0)R(p0)))
+((X(p2))R((0)*(p2)))R((0)R(p2))
+((p1)R((p1)+(0)))+((p2)U(X(p1)))
+(p0)U(X(X(((1)*(X(p1)))R(p1))))
+((X(p1))R((p1)*(p1)))U((p2)R(p1))
+(X(p0))+((p0)R(((p0)+(p0))U(1)))
+X((X(p1))U(((p0)+(1))*(X(p0))))
+(X((X(p1))U(p0)))U((1)*(X(p0)))
+X((((0)+(0))*(X(p1)))U(X(p2)))
+X(X(((X(p2))U(X(p2)))U(X(0))))
+((X(1))U((X(0))R(X(0))))+(p2)
+((1)R(X(X(p1))))*(X((p2)U(1)))
+(p0)+((p0)*((X((1)*(1)))U(p2)))
+(((X(p0))*(X(0)))U(p2))*(X(0))
+((p0)R(1))R(X(X(X((p2)R(1)))))
+X(((1)+(1))U((X(p2))*(X(p0))))
+((p1)U(X((p0)+(X(p0)))))U(X(p2))
+(X(0))+((X((0)R(p0)))U(X(p0)))
+((p1)R(1))U((p0)R((X(p2))R(p1)))
+((0)*(X(p2)))U(((p0)R(0))U(p2))
+X(((p1)*(p2))U(((p2)U(p2))U(p0)))
+(((p1)+(p0))U((p2)+(X(1))))R(p0)
+((p2)*((X(p1))*(X(1))))R(X(p0))
+X((((p2)*(1))*(p0))U((p1)R(p0)))
+(1)+((1)+((X(p2))U(X(X(p1)))))
+X((X(p2))R(((X(p0))R(p1))R(0)))
+(((1)U(p2))*(X(p2)))*((0)U(p1))
+(((p2)U(p2))R(p0))U((X(p2))+(0))
+((0)+((1)R(p2)))*((X(1))U(0))
+((X(p1))+(X(0)))*((X(p2))U(p1))
+X(((X(p0))R(X(p1)))U((p0)U(p0)))
+((p0)+(((1)+(p1))U(p2)))U(X(p2))
+((X(p1))*((1)U(1)))*((1)*(p0))
+((p2)R(p1))R((X(p1))R((p0)+(p2)))
+((p1)*((p2)R(p2)))*((X(0))R(p1))
+((p2)U(p0))+(X(((p0)*(p1))R(0)))
+(X(p1))+(((p1)*((p2)R(p0)))R(p2))
+(1)*(X((X(p2))*((X(p1))U(p2))))
+(((p2)R(p0))R(X(X(p1))))R(X(p1))
+(X(1))U((p2)R(X((X(p1))U(p0))))
+(X((X(X((1)R(0))))R(1)))*(p1)
+(((p0)U(X(p2)))U((1)+(p2)))U(p1)
+((p0)R(p0))U(X((X(p2))*(X(1))))
+(((p1)R(1))R(p0))R(X((p0)U(p2)))
+X((p0)R((p0)*((0)*((1)R(p2)))))
+(X(p1))+(((X(p0))R(X(p1)))R(p0))
+((1)*(X(p0)))R((X(p1))+(X(p1)))
+X((X(X(p1)))+((X(p1))+(X(0))))
+((X(X(X(p0))))+((p1)U(p0)))R(1)
+(p1)R((X(1))+(((1)U(p1))U(p1)))
+X((((X(p1))U(p2))R(p1))+(X(1)))
+((X(p1))+((p1)*(X(p1))))*(X(1))
+(X((p2)+(p2)))U((p0)*((p2)+(p0)))
+(((p2)+(p0))U(p1))R(X((p1)R(1)))
+X(((X(p1))R(X(p2)))R((p2)*(1)))
+((1)U(p1))U((X((1)+(p0)))+(0))
+((p0)*(p2))U(((p1)R(p0))U(X(p1)))
+(p2)R(((p2)R(X(p0)))*((p1)*(p1)))
+(X(p0))U(((1)+(1))*((0)U(p0)))
+(((p1)U(1))*(p0))+(X((p2)+(1)))
+(p0)U((X(p1))U((0)+((p0)+(p0))))
+(p1)U((X(X(0)))U(X((1)R(p0))))
+((X(X(p1)))U(X(X(p0))))U(X(p2))
+((1)+(1))U((p2)R((X(p0))U(p1)))
+(1)+((0)*((p2)U((X(p1))R(p0))))
+((p2)U(p2))U((X(0))U((p2)+(p1)))
+(((p1)R(p1))*(X(p1)))+(X(X(p2)))
+X(((p0)R((p1)R((p0)+(p0))))+(1))
+((0)U((p2)R(p2)))R((X(0))U(0))
+((X(p2))R((1)U(X(p0))))*(X(1))
+X((1)R(X((p2)R((X(p1))R(p0)))))
+(X(1))U(X(((p2)U(X(p1)))R(p2)))
+((((p0)*(X(p2)))R(p0))+(p2))R(p2)
+(p0)U(((p0)U(1))R((X(p2))R(p2)))
+((0)U((X(p2))R(X(p2))))+(X(p2))
+(X(p1))+(((X(p2))+(p0))U(X(p2)))
+((0)*(1))U((p1)U(X((p0)R(p1))))
+(X(p0))R(((X(p2))R(X(p2)))+(p1))
+(X((X(p1))R((p1)+(p2))))+(X(p1))
+(((p0)R(p0))*(X(p1)))R((p2)+(p1))
+X((X(0))U((X(1))U(X(X(p1)))))
+((p0)U(p0))*(((p1)R(p1))R(X(p1)))
+((p2)+(((X(0))+(p2))R(p0)))R(p2)
+(p1)*(X(((X(X(p0)))R(p2))U(0)))
+(X(p1))U((p0)+((p1)+((1)*(1))))
+X(X(X(((X(p1))R(X(0)))+(p0))))
+(X((X(p2))+(p0)))R((X(p0))*(0))
+((0)U(p1))*(((p1)+(p1))R(X(p0)))
+((X(p0))*(((p0)U(p0))R(p0)))U(p1)
+(((p2)*(p2))R(p0))R((p2)*(X(p0)))
+(p2)U(X(X((p1)R(X((p0)U(p0))))))
+(((1)U(p2))U((p1)U(X(p2))))U(p0)
+X(((p2)U(p0))R(((p1)+(p0))+(p0)))
+(X((p0)*(p0)))U(((p1)R(p1))U(1))
+((X(p1))+(0))R((X(X(p2)))U(p1))
+(X(p2))U((1)*((p1)U((0)U(p2))))
+((p1)U((X(0))*((1)R(p2))))R(p2)
+X(((X(1))+(p0))R((X(p0))R(1)))
+####
+
+####
+(X((p1)R(X(p0))))U(((p0)R(p1))R(((p2)*(p2))U(p1)))
+(1)R((X(((p1)R((p2)+(1)))U(p0)))U((X(1))*(0)))
+X(((X(p1))R((1)U(p2)))*((p1)R(((0)U(p2))R(p0))))
+X(X((X(p1))*(X((X(p0))+((p2)+((p0)+(X(p2))))))))
+X(((p2)*((p2)R(X(p1))))U((X((p1)+(p1)))*(X(p2))))
+X(((0)R(p0))U((X(p2))+(X(((1)U(1))*(X(1))))))
+(X(p1))*((((X(p0))+(X(p0)))U((p0)+(p1)))+(X(p0)))
+(((p0)+(X(p0)))U((1)R((X((p2)U(p0)))R(0))))R(p2)
+(((1)+(X(p1)))R(p2))*(((X(p1))U(p2))U((p2)R(0)))
+((X(p2))R((X(p0))R(0)))U((X(p2))*((p2)U(X(0))))
+X(((p1)+(X(1)))+((p0)*(X(((X(p1))U(p2))*(p0)))))
+((p0)+(p0))R(((p0)+((X(p0))R(X(p1))))R((p2)R(p0)))
+((p1)+((p2)U(X((X(p2))*(p1)))))+(((p0)U(p2))*(0))
+X(((((0)+((1)R(p2)))*(X(p1)))R((p0)*(1)))R(0))
+X(((p1)R((X(1))+(p0)))U(((X(1))R(X(p1)))R(p1)))
+(X(p1))+(((X(p1))R((X(0))U(0)))*(X(X(X(p2)))))
+((X((X(0))U(X(p2))))U(X(p2)))U((X(p2))R(X(p2)))
+X((X((X(p1))U(X(0))))U(X(((p1)R(p2))+(X(p2)))))
+X(X(((X(p0))R(((X(p0))U(X(1)))U(X(1))))R(0)))
+((p0)*(p2))+(((p1)+(0))*(((0)R(1))U((p1)+(p1))))
+X((X((p1)+((1)U(p0))))+((X(p1))R((X(p1))*(1))))
+((p1)R(p0))U((X(p2))*((((0)U(p2))+(p2))R(X(p0))))
+((p1)R(X(p1)))U((((p0)R(p2))+(X(p0)))*((p0)R(p0)))
+((1)R(p1))R((((p1)U(p0))R(p2))*((0)U((p2)U(1))))
+((X((X(X(0)))R(X(p0))))*(0))*(X((p1)R(X(0))))
+X(((X((p1)U((X(p1))R(1))))R(X(p0)))R(X(X(p0))))
+X((((p1)R(p0))R(X(p2)))U((X((X(p0))*(0)))R(p0)))
+(((p0)U(1))U((p2)*(X(1))))R((X(X(p0)))+(X(p0)))
+((1)R(p2))U((X(p1))U((p1)U((X(p2))*(X(X(p1))))))
+(X((X(p1))+((1)+(1))))R((p1)*((p0)+((0)R(p2))))
+((X((0)U(p0)))+(p1))U(((0)R(0))R((X(p0))U(p1)))
+((X(0))U(X(((0)U(0))*(p2))))R((p1)U((1)R(p0)))
+((p2)U((X((X(p0))U(p1)))+(X(p1))))R((X(p2))R(p0))
+((X(1))U(p2))*(((X(p1))U(p0))R(X((p2)R(X(p2)))))
+(p2)+((((p0)*((X(p0))R(X(1))))+((p2)R(p0)))*(p2))
+(X((p2)U(0)))R((X(p1))*((X(p2))R(X((p1)U(p1)))))
+((X(p0))*((X(X(p0)))U(p1)))+(X(((p2)U(p2))R(p0)))
+((((X(0))*(1))R(p2))R(p2))+(X(((p1)U(p1))*(p1)))
+(p2)+((((X(p2))R(X(p2)))U((p1)*(1)))U((1)R(p2)))
+((p0)R(X(1)))*((X(p2))*((X(p2))*((p0)+(X(p2)))))
+(X(p2))+(((1)+((((p1)U(0))*(1))*(X(0))))R(p0))
+((p0)+((p0)U(0)))U((X(X((p2)U(p2))))R((p0)+(p1)))
+X(X((X(p0))R(((p1)U(X(0)))+((0)+((p2)*(p0))))))
+(X((((p0)R(p1))U(X(p1)))R((X(p1))*(0))))U(X(p2))
+X(X(((p1)U(p1))+(((p2)*(p1))*(((p1)*(p1))*(1)))))
+((X((X(p0))R(p0)))R((p1)*(X(p2))))*(X((0)U(p1)))
+((p0)R(p1))+(X((X(p2))*(((X(p1))+(p1))+(X(p1)))))
+((((p0)R(p1))+(p0))U(p0))*(((p0)*(X(X(p1))))+(p2))
+((X(p0))U(p1))R(((p0)+(X(p2)))R(X(X((p1)U(p0)))))
+X(((p1)*(X(p2)))R(X((X(p1))U(X(X((p0)*(p2)))))))
+((X(p2))R(((p2)R((p1)R(X(p2))))+(p1)))R((p0)R(p1))
+(X((((0)*(p0))U(0))U(((0)+(X(p1)))R(p2))))U(p0)
+((X(p2))U(X(p2)))R(X(((X(p1))U(X(p1)))+(X(p1))))
+((X((p0)R((X((p1)U(p2)))*(X(1)))))U(0))U(X(1))
+((X(p0))R((p0)*(p0)))R(((1)U(p2))*((X(p2))R(p1)))
+((X((X(p2))*((p0)*(p2))))U(p2))U((X(p0))+(X(p0)))
+((X(X(1)))+(((p1)*(1))R((X(p2))R(p2))))*(X(0))
+((p1)*(((X(p0))U(X(p0)))U(0)))U((X(p1))R(X(p2)))
+(((X(p0))+(X(((0)R(p0))+(1))))U(p2))R(X(X(p2)))
+(((p1)U(0))R((X((1)R(p1)))R(p2)))+((X(p2))U(p1))
+X(((p1)R(p0))+((X(X(p1)))U((p1)+(X((0)*(p0))))))
+(X(p2))R(X(X((((p2)U((p1)*(p0)))R(p1))*(X(p1)))))
+(p2)U((X(p2))*(((X(p2))R(X(p0)))R((p1)U(X(p0)))))
+X((X(X((X((X(1))R((X(0))*(p0))))U(p0))))U(p2))
+(((1)+(p0))+((0)U(p1)))R(X((X(p2))*((p0)*(0))))
+(((X(0))U(p2))*((p1)*(0)))U((X(X(p1)))U(X(p2)))
+((0)*(X(0)))R(((p2)*((p2)R(X(p1))))U((p2)+(p1)))
+(p1)U(((p0)+(((p0)R(p0))+((X(p0))R(p1))))R(X(p0)))
+(((X(X(p0)))R(X(p0)))+((X(p0))+((p0)R(p0))))U(p2)
+(0)+((((p2)U(p0))+((p1)U(X(X(p0)))))+((p1)R(p2)))
+X(X((X(((X(p1))*(X(0)))R(X((0)+(p2)))))R(0)))
+(((X(X(p2)))R(p2))R((p2)+((X(p2))R(p0))))U(X(1))
+((X(p1))*((p1)*(X(p1))))R(((p1)*((p0)*(0)))U(0))
+(((p2)U(p0))U((p1)R(p1)))R((p2)R(((p2)R(p2))*(0)))
+(((p0)*(p2))R(X((p1)R(p0))))*((p1)+((1)R(X(p2))))
+((p0)R((X(p0))+(X((X(p1))*((p2)R(p2))))))*(X(p0))
+((((p0)+(X(p2)))+(p2))+((p1)*(p0)))U(X((p0)R(p1)))
+((X(p2))R(p2))+(X((p2)+(X((X(p1))+(X(X(1)))))))
+((p0)*((p2)U(X(X(p1)))))*((p0)+((X(p1))R(X(0))))
+(1)+((((p1)R((X(p0))R(p2)))*((1)+(p1)))+(X(p2)))
+((X(p1))R(0))U((X(p0))*((X(0))*((p0)*(X(p0)))))
+((X(p0))R((X(1))U(((0)+(p1))R(p1))))*((p2)U(p2))
+((p1)+(1))R(X((X(p1))U(((X(p1))R(X(1)))R(p2))))
+(((1)+((X(p2))U(p1)))+((0)*(1)))R((p0)*(X(p2)))
+((p2)R(p2))U(((p0)R(p0))R(((1)+(X(p1)))U(X(1))))
+X((p2)R((X(p0))+((X(p2))*(((X(p1))+(p0))+(0)))))
+((X((X(0))R((p1)U(X(p0)))))*(X(0)))*((p0)R(p1))
+(((p2)R(1))R(0))+(X(X(((p1)U(1))R((p0)R(1)))))
+((((0)*(p0))*(X(p1)))+(X(p2)))*((X(1))R(X(0)))
+X((((X(p1))R(X(0)))*(X(((0)U(1))U(p0))))R(0))
+((X(p0))R(((p1)U(((1)*(p1))*(p1)))+(p2)))R(X(1))
+((((X(0))*(p2))U(p2))*(X(p0)))R((0)+(X(X(1))))
+(0)+((((X(p0))+(X(X(p2))))R(p0))R((1)R(X(p0))))
+((1)+((p0)U(1)))U((X(X((p1)+((1)R(p0)))))*(1))
+((p0)+((1)R(p2)))U((X(X(X(p1))))R((X(p0))R(0)))
+(X((X(X((0)+(p1))))+(X(p2))))U(X((X(p1))U(p2)))
+((p0)U(1))U(X(X(((p2)+((1)+(X(0))))R(X(p0)))))
+X(X(((p1)U((X(p1))R(X(X(0)))))R((X(p2))+(p2))))
+(X((X(p1))R(p0)))U(((p1)*((0)U(X(p2))))*(X(p2)))
+(X(X((p0)U(X(p0)))))U(((p1)*((p1)R(p1)))R(X(p1)))
+(((X(X(p0)))+(X(1)))*(((p0)U(p1))R(p0)))R(X(p1))
+((p1)*(X(p1)))R(((((p1)*(p0))U(p0))R(p1))R(X(1)))
+((1)R((0)+((X(p0))+((1)U(X(p2))))))U((0)U(p0))
+X(X(((((p0)R(p2))R(X(1)))R(p2))+(X((p2)+(1)))))
+(((p1)R(1))U(((p0)*(p1))R((X(p0))U(p1))))+(X(0))
+(((p0)R(p2))U(p1))+(((X(p2))*((0)+(0)))U(X(p1)))
+(((X(p1))*(p1))+((0)*(p1)))R((X(p2))U((p1)U(p0)))
+(X(1))R((p0)U(((X(X(p0)))U(p0))*((X(p0))U(p0))))
+((p0)*(((p1)U(p1))U(X((p2)R((p0)U(p1))))))+(X(p1))
+X(((1)U(p0))U(((1)U(p0))R(X((p1)*(X(X(p1)))))))
+(X((p2)*(X((p1)U((p1)U((p2)R(p1)))))))*(X(X(0)))
+(p2)U((X(X((X(X(0)))R(X(1)))))*((p0)R(X(p0))))
+((X(p1))+(X((1)U(p2))))U((p1)R(X((p1)R(X(1)))))
+((p2)+(p0))+(X((((p2)R(1))R(X(1)))+((p0)*(p1))))
+(((p2)U(0))R(X(X(p0))))R(((p2)R(1))U((p1)U(p2)))
+((p0)U(1))U((X(X((1)R(X(p0)))))U((1)+(X(p1))))
+(X((X(p1))U((X(p1))U((p0)R((1)*(0))))))+(X(p0))
+((X(0))*((p2)U((p0)*(p1))))U(((1)*(0))*(X(0)))
+(((X(0))*(p0))U((p0)*(X(p2))))+(X((p0)+(X(p2))))
+(((p1)+(X(p0)))+(X((p1)U(X(p0)))))U((p2)R(X(p0)))
+((p2)+((p2)U(0)))U(X(((p2)R(X(1)))*((p0)R(p2))))
+(p2)U(X(((p2)+(X(p0)))*(X(X(X((p2)R(X(p2))))))))
+(((X(p2))U((X(p1))U(1)))U(((p0)U(p2))R(0)))R(p0)
+((X(X(p1)))U((p0)U(p2)))U((p2)*(((p0)+(p2))*(0)))
+((X(p2))R(X(p2)))U((X(p0))R(X((X(X(p0)))*(p1))))
+(1)R((0)R((X(p1))U(((p0)+(X(p1)))*((p2)U(p2)))))
+(((p0)U(1))R(p2))U(((1)*((p1)R(X(p0))))*(X(0)))
+(((1)U((1)U(p1)))*(0))R((p1)R((X(1))U(X(0))))
+(X(p0))U(((p0)+(X((X((p2)+(X(p1))))+(p0))))U(p0))
+((p1)U(0))U((((p0)+(X(p1)))U(X(1)))+((1)+(p2)))
+(((p1)+(1))+(p0))+(((p1)+(p0))+((p0)R((p1)+(p1))))
+((X(1))R(((X(p2))+(X(p2)))R(X(X(p2)))))*(X(1))
+(((((1)R(X(p0)))R((p2)+(p2)))R(p1))*(X(p0)))U(p0)
+((X(p0))R((p2)*(p1)))*((p2)U(X((p0)R(X(X(1))))))
+((((0)R(X(p2)))*(X(p0)))U(X(p1)))R((p1)+(X(p2)))
+X((X(((X(p1))R(0))+(X(p1))))*((X(p2))+(X(0))))
+((((p0)U(p1))R(p2))+(X(p1)))U((X(p0))U((p1)+(p0)))
+((((p0)*(p1))R(X(1)))R(X((X(p2))+(X(p2)))))U(p2)
+X((((0)R(X(0)))+(X(1)))R((p2)*((p2)*(X(p1)))))
+((X((X(1))+(X(p0))))*((p0)R(0)))U(X((p1)U(p1)))
+X((((X((X(p2))U(0)))*(p0))R(p2))+((X(1))U(p1)))
+((X((p2)U(1)))+(X(p2)))+(X((X(p2))U(X(X(p2)))))
+(X(p0))U((X((X((1)*(X(p1))))U((p2)U(p1))))*(p1))
+(((X(X(0)))R((0)U(p2)))R((1)*(p2)))U(X(X(p0)))
+(1)U(X(((0)R(p1))U((p0)+((p2)*((p1)*(X(p1)))))))
+(((p1)*(p1))*(((p0)U(p0))R((p2)R(p2))))R((p0)+(p2))
+(X(((X(p1))R(0))R((X(p2))*(X(p1)))))U(X(X(p0)))
+(((p0)U(p2))R(X(p2)))U((X((p0)*(0)))R((p1)U(p2)))
+(((X(p0))*((1)U(p2)))U(p0))U(((X(p1))+(p1))+(0))
+((X(p1))R(X(((p0)+((X(p0))R(p0)))+(p0))))U(X(p2))
+((p2)+(X((X(p0))+(X(p0)))))U(((X(p1))U(1))U(p0))
+X(((X(p2))*(((1)U(1))*(X(0))))*((X(0))R(p1)))
+((1)U(X(p1)))U(((p1)U(X(p2)))R((X(0))U(X(p0))))
+(((p1)U(p2))+((p1)+(X(p1))))R(X(((p0)R(p0))+(p2)))
+((((p1)U(0))U(X((p0)U(p2))))*(X(p1)))*((p0)U(p2))
+((p2)*((X((X(p2))R(X(p1))))*(X((1)U(1)))))R(p1)
+(((p0)*(p1))*(X(0)))U(((X(p2))+((1)U(p2)))U(p1))
+((X(1))*((X(p1))U((X(p2))U(0))))+((X(p2))*(p1))
+(1)+((p2)*((((X(p2))U((X(p2))R(p1)))*(p2))U(p0)))
+(X(X((X(0))R(((X(p1))U(0))R(X(p1))))))*(X(1))
+X((X((X((p0)U(0)))*(p2)))*(((X(p2))R(p1))+(p2)))
+(X(((p1)+(X(p1)))+(X(1))))R(((p0)U(p1))U(X(1)))
+(((0)U(p1))U(p0))U((X(p2))*(((p2)R(X(0)))U(1)))
+((p2)U(p1))*(X((((p0)*(p0))+(1))R((X(p2))U(p2))))
+(((p0)U(p0))*(((X(1))*(p2))R((p0)R(p2))))*(X(p1))
+((X(1))U(((p2)*(p2))+(p1)))R(((p1)U(0))*(X(p2)))
+((X((p1)*(X(0))))R((p1)R(X(p0))))*((1)+(X(p2)))
+((X(p1))*(((p0)+((1)U(X(p1))))U((p1)*(p0))))R(p2)
+(X((((0)R(0))+(p0))R((p0)R(p0))))R(X((0)*(p0)))
+((((p0)R(p2))*(1))R((p2)U(p1)))R(X((p1)R(X(p2))))
+((((X(p2))*(0))*((p0)U(p0)))R(p1))U((0)*(X(1)))
+((1)R(X(p2)))U((p0)R(X((X(X(p1)))+((p1)U(p0)))))
+(((X(p1))U(X(p0)))R((X(p1))*((p1)U(X(p1)))))R(p1)
+((((p0)*(p2))U(p0))R(X(p2)))U((p0)R((X(p1))*(1)))
+(X(X(p2)))+(((((X(p1))U(p2))R(X(p2)))*(p1))R(p0))
+(p1)U((X((p1)U(p0)))+(((X(1))+(p1))*((1)R(p2))))
+X((((X(p2))*(p1))U(((X(p2))U(X(0)))*(0)))R(0))
+(X((X((X(X(p0)))R(X(0))))*((p0)*(p1))))R(X(p1))
+X(((((p0)+(p2))*((X(p1))*(X(p1))))U(p1))U(X(p2)))
+((((X(p0))R(p1))*(p1))+((X(p1))R(p1)))*((1)+(p1))
+(X(p0))R(((p0)*(X(p2)))U((X((p0)R(1)))+(X(p2))))
+X((X(((p0)R((X(p1))*(0)))*(X(p1))))R((1)*(p2)))
+(X((p1)U(p1)))*((X(p2))*((X((p2)U(X(p1))))+(p2)))
+((X(p2))R(p1))+(((X(0))*(X(p0)))U((X(p1))R(p1)))
+X(((p1)+((p1)R(X(p2))))U((X(1))U((X(p2))R(p1))))
+((1)U(p1))+((p0)R(X(((p2)*(X(p1)))R(X(X(p1))))))
+(((X(((p0)U(1))+(p0)))*(p2))R(X(p0)))U((1)U(p2))
+(1)U((((p1)*(p1))R(X((X(p1))U(p1))))+((p2)*(p1)))
+(((1)U((1)+(p0)))U(((p2)R(X(1)))+(0)))*(X(0))
+(((0)R(p1))+((0)+((p1)U(1))))*(((p1)R(0))R(1))
+(X(p0))U(X(((p1)*(p0))*((p0)*((X(p1))R(X(p2))))))
+(p0)R((p2)U((((X(p1))U((p2)R(X(1))))+(p1))R(p1)))
+(X(p1))+((((0)*(X((p0)U(X(1)))))R(p2))R(X(0)))
+(X((X(p1))+(0)))*((X((p2)U((p0)U(p2))))U(X(p2)))
+X(((X(1))*(X(p1)))*((X(0))U(X((p1)R(X(p2))))))
+((X((1)*(p2)))+((X(p2))U(X(p1))))U((X(1))U(p1))
+(X(p1))+((((X(p2))U(X((p2)U(p1))))R(X(0)))*(p0))
+((X(X(X(0))))*(X(p1)))*(((p0)+(p2))*((p2)*(p1)))
+(((p1)*((p2)*(X(0))))*(p0))U((X(p0))R((p2)R(p2)))
+((p0)R(p1))R((((p2)U(p1))R(0))+(((1)+(p1))U(p0)))
+(((p0)*(p1))*((X(((p1)R(p2))*(1)))+(p0)))R(X(0))
+X(X(X(((X((X(p2))+(0)))R(X(p2)))U((p2)+(p0)))))
+(X(((1)+(1))+(X((X(p2))U(1)))))R((p1)R(X(p2)))
+((X(p2))*((p1)U((X(p0))*(0))))R(((p1)*(0))R(p1))
+X(((X(p0))*(p2))*((X(0))+(((p0)*(0))*(X(1)))))
+(((p1)+(p1))*((p0)*(0)))*(((X(X(0)))U(p2))*(p0))
+((X(X((1)U(p2))))*(p0))U((p0)R((X(p1))R(X(0))))
+X((X(p2))U(((p1)R(1))U(((p2)U(X(p0)))+(X(p2)))))
+(((p0)*(X(p2)))R((X(0))U((p1)*(p0))))U((p2)R(p0))
+(X((X(p0))R(X(p1))))U(((X(0))U(X(p2)))R(X(0)))
+X((((X(1))R(p1))U((p1)+(X(p1))))R((X(p1))U(p2)))
+((p1)U(p0))R(X((1)U(((X(p0))*(p0))R((p2)R(p2)))))
+X(((p0)*(((p0)+((p2)+(1)))*(p0)))U((p1)+(X(p1))))
+(p1)R((((p2)R(p0))R(p1))R((X((p1)*(1)))+(X(p1))))
+((X(p2))+(((p0)*(0))U(1)))U(((1)+(X(p1)))U(p2))
+(((X(X((p2)+(0))))R(X(p1)))+(X(p1)))+(X(X(0)))
+((X(p2))R((X(p1))R((X(p2))R((p2)R(X(p0))))))+(0)
+X((((X(p2))U(p1))R(p0))R(X(X(X((X(1))U(0))))))
+(X(p0))U((X(((1)*(1))U((p2)R(p2))))+((p2)+(p0)))
+(((p2)R((X(p2))U(X(1))))*(p0))*((p1)R((p2)R(p0)))
+(((X(p1))U(X(p2)))U(X((X(p1))R(p0))))U((p0)R(p1))
+X((((p1)+(p2))U((0)R(p1)))R((p1)*((X(p2))R(0))))
+(X((p0)U(0)))U(X(X((p0)R(X((p2)*((0)U(1)))))))
+(X(X((p2)U(((X(p1))U(1))*(X(0))))))R((p1)R(p1))
+((p0)R((1)R(1)))U((X(1))U((p0)+((1)R(X(p0)))))
+(X(1))+((X(((X(p1))R(p0))U(1)))*((p2)U(X(p1))))
+(((p0)+(p2))R(p0))U((X(p2))U(((p1)U(0))*(X(0))))
+((0)R(p0))+(((p2)+(p2))U((((1)R(p0))U(1))U(p1)))
+(((p1)*(X(p0)))R((X(p1))R(X((p1)U(X(p1))))))+(p0)
+((0)U(X((((p0)U(X(0)))*(p2))+(p0))))U((p1)R(p0))
+((((p0)U(p1))R((X(p1))*(1)))*(X(1)))+((p2)R(p1))
+(X(p0))U(((p1)R(X(p2)))*((p2)+(((p1)+(p2))U(0))))
+(X((p1)R((X(p0))+((X(0))*(p1)))))R((X(p0))U(p1))
+(((p1)+((p1)R(p1)))R((X(0))U(p2)))R(X((0)R(p1)))
+X(((((X(0))R(p2))R((p1)U(X(X(p2)))))R(p0))+(p0))
+X((((X(1))*(p0))U((X(0))+((1)U(1))))R(X(p1)))
+(X(((X((1)U(p2)))*(p2))*(((p0)*(p0))+(p1))))*(p2)
+(((p1)+(0))+((X(p0))+((X(1))*((p1)U(p0)))))U(0)
+(((1)*(0))U(X(p0)))R(X((X(p2))U((X(p1))+(1))))
+(((X(0))R(p0))U(p2))+(((1)R(1))+((X(p0))+(p1)))
+((X((p0)R(1)))U((p1)U(0)))*(((p2)R(p2))U(X(p0)))
+(X(p1))U((0)R(((p1)R(p0))R((X((p0)R(0)))U(p2))))
+(X(p0))U((X(X(((p2)U(X(p1)))U(X(p1)))))+(X(0)))
+(X((X(p0))*(p0)))U((X(1))+((X(p1))*(X(X(p0)))))
+((p2)U((p0)+(0)))+(((X(p2))U(X(p1)))R((p2)*(p0)))
+(((0)R((p2)U(X((1)+(X(p2))))))U(0))*(X(X(p1)))
+(p1)U(((X(1))R((p2)U(p0)))*(X((0)*(X(X(p0))))))
+(X(((X(p0))+(p0))U(0)))*((X(p1))+(X((p0)U(1))))
+(((p2)U(p2))R(X(p1)))*(((p0)+(p2))*(X(X(X(0)))))
+((p2)R((0)R(1)))R(X(((X(p1))*(p1))*((1)+(p1))))
+(((X(1))R(X(1)))+(((X(0))R(p0))R(X(p2))))R(p2)
+X((((p2)+(X((p1)U(0))))R((1)*((p0)*(1))))+(p1))
+((X(p1))+(X(p2)))+((X(X(0)))R((p1)U((1)*(1))))
+((X(p1))+(((p0)R(X(X((p1)+(p2)))))R(X(p0))))U(p2)
+((X(p2))R((p0)U(X(p0))))U((X(p0))R(X((p1)+(p1))))
+((X(p0))*(p1))U((X((1)R(p2)))R(X(X((p2)R(1)))))
+(((p1)+(p0))U(((p1)R(p0))U(1)))U((p0)*((p2)R(1)))
+(X(((X(X(p0)))+(X(p2)))U(p0)))R(((p0)*(p0))U(p2))
+(((((0)R(p1))U(p2))U((0)R(X(X(0)))))+(p2))U(p2)
+(((p0)*(0))R((0)U((p2)+(1))))+((p0)+((p0)U(0)))
+X(((p0)R((p1)+(p1)))U(((p0)*((X(p0))+(p1)))*(p0)))
+((X(X(p0)))U((p2)R(p1)))*(((X(p1))U(X(p0)))U(1))
+((p0)R(p1))R(X((p1)U((X(p0))+((X(1))U(X(1))))))
+X(((X(p1))*(X(p0)))U((1)R((p0)+((X(p0))R(p2)))))
+((p0)U((X(0))*((X(X(X(p1))))+(X(p0)))))+(X(p2))
+((p2)U(0))U(X(((X(X((p2)+(p2))))*(X(p1)))R(1)))
+((p2)R((X(p2))U(p2)))+((X((p2)*(p0)))*((p2)+(p0)))
+(X(X(X((p2)U(X(p0))))))U(((0)U(p1))+((p1)U(1)))
+(X(p0))+((1)U((p2)R(X((X(0))+((X(1))U(p1))))))
+((((p1)U(1))+(p2))R((p0)+(p0)))U((X(p2))U(X(p2)))
+(((X(p1))U(X(X(p2))))U(0))*((X(p0))U((p1)R(1)))
+(((0)R(p0))*(p1))R((0)U(((X(p1))*(X(p0)))U(0)))
+(((0)R(X(X(X(p0)))))U(X(1)))U((p0)U(X(X(p0))))
+((X((1)R(X(1))))R(X(0)))R(X((X(X(1)))+(p2)))
+((X(p1))R(((X(0))U(X(p2)))U((p0)R(p0))))+(X(p0))
+(X(p2))+((p0)U(X((X(0))*((1)U((X(p1))*(1))))))
+(((X((p1)U(p0)))R((p1)U(1)))+((1)R(p0)))*(X(p1))
+(X(((p0)+(p1))+((X(p1))*(p2))))U((p0)R((p0)U(p0)))
+((X(X((p1)*(p0))))R((X(p2))+(0)))U(X(X(X(p0))))
+((p2)+(X((p1)R(p1))))R((p1)U(X(((p2)*(0))R(p0))))
+(X(p0))U((((X(p2))R(p0))U(0))+((p1)*((1)U(p2))))
+(X((X(p1))+(X(p2))))R(((p2)U(p1))R((p0)R(X(p2))))
+(((X(p2))*(X(p1)))R((X(p0))+((0)R(1))))U(X(p1))
+((0)+(X(p1)))U(X(((p1)R(X(p1)))R((X(p0))*(p0))))
+((X(p1))U(X(p0)))U((((0)U(p2))*(X(p1)))+(X(p2)))
+(((p0)U(p1))+(X(p2)))*(X(X(((X(p1))*(1))U(p1))))
+(X(1))U((p2)U(((X(0))U(p0))U(((p1)U(1))R(p2))))
+(((1)R(1))*((1)U((p2)R(X(p0)))))+((p2)+(X(p2)))
+(X(((X(p1))*(p1))U(X(p1))))+(((X(p1))U(1))+(p0))
+((X(p0))R(((X(X(p0)))*(p1))*(p0)))R((X(p0))U(p1))
+(X(X(1)))U((((((p1)+(p2))U(p2))+(p0))R(0))+(p0))
+(X(1))*(((X(p1))R(p2))U(((p1)+(X(p0)))U(X(p0))))
+((p0)*(p0))*(((p0)R(((p2)R(p2))+(p0)))+((0)+(0)))
+(((p2)U(p2))R(p2))*(((X(p2))*(X(0)))+((1)*(p2)))
+((X((X(1))U(p1)))U(p0))*(((X(p2))R(1))U(X(0)))
+X(((X(0))*((X(p1))U((p1)R(X(p2)))))U((p2)R(p2)))
+((((X((p2)R((p2)+(p2))))U(X(0)))*(p0))+(p1))*(1)
+((p0)R((X((p0)R((p1)+(p2))))R(p0)))R((X(0))U(p2))
+(X(p1))U((X(X(X(((X(p1))*(X(0)))+(p1)))))U(p0))
+((p0)R((p0)R((p0)*(p0))))R((p1)U((X(p0))*(X(p1))))
+((X(0))+(((p1)+((p1)U(p0)))U((X(0))U(p1))))U(p0)
+((X(p2))U(X(((p0)+(p0))*(X((p1)R(0))))))R(X(p1))
+((((p1)R(p1))U(X(p0)))U(X(0)))*((p1)U((p0)R(p2)))
+(X((X(p1))U((1)U(p2))))*((p2)*((X(p2))U(X(1))))
+(X(0))R(X(X((((1)R(p1))R(p1))U((X(p2))+(1)))))
+(X(((p1)*(p0))+(p1)))U(((p1)R((p0)*(p1)))+(X(p1)))
+(p1)U(((X(p0))*(p1))R((X(p0))R((X(p2))+(X(p2)))))
+((X(X((p0)+(p2))))U((0)U(X((1)*(0)))))R(X(p1))
+((X(p0))U((1)+((p0)+((X(p1))+(X(p2))))))U(X(1))
+(X(p2))R((p0)*((p0)*((p1)R((X((p0)+(p2)))+(p1)))))
+((X(p1))U(((p0)R(p1))U(X(p0))))R((X(p1))U(X(p2)))
+((X((0)U(p0)))U(X(p2)))*((((1)+(p0))*(p0))+(p1))
+((X(p1))*((0)R(p0)))R(X(((1)*(X(0)))+(X(p1))))
+((((p2)+(p1))U(X(p2)))+((p2)*(X(p2))))+((p2)U(p0))
+((p2)*(p0))U((((1)U(p0))*(X((p0)+(X(0)))))R(p2))
+((p1)U(p2))+((X(p2))R(((0)+((0)R(p0)))+(X(p2))))
+(((X(p2))U(X(p1)))+(X(p0)))+(((p0)R(p2))*(X(p1)))
+((X(p0))R(((p2)R(p0))+((1)R(1))))*((X(p0))R(p1))
+X(X((X(X((p1)U(p1))))+(((0)U(X(p1)))R(X(0)))))
+(X(p1))U(((X(p1))+((X(p2))*(X(0))))R((p1)R(1)))
+(X((X(p0))U(((X(p2))U(p0))*(p1))))R((p0)+(X(p2)))
+(p2)*(((p2)*(X(p1)))+(((p0)U(1))+(X((p1)U(0)))))
+(((X(p2))*((0)+(0)))R((1)R(X(0))))*((p2)*(0))
+(p2)U(((X(p0))U((p0)*((p2)*(p1))))R((p2)R(X(p2))))
+(((X(p1))R(X((p0)+(X(0)))))R(X(X(p2))))R(X(p0))
+((p1)R((1)U(((p0)U(p1))R((p0)+((p0)U(1))))))+(1)
+(0)U((((p2)U(p1))+((X(p0))U((X(0))+(1))))R(p1))
+(((X(X(p1)))U(X(p2)))R(((X(p0))R(p2))U(p1)))+(p0)
+((p1)R((X(p1))+(p2)))*((X(p2))U((X(p0))U(X(1))))
+((0)R(((p2)U(p1))R((p0)U(p1))))*((X(p1))+(X(0)))
+(p0)R((((X(p0))U(p0))U((X(X(p1)))*(X(p0))))*(1))
+((X(0))R((X(X(p0)))+(0)))*((p0)U((p2)*(X(p2))))
+(X(p0))U((((p0)*((1)U(p1)))+((X(p0))U(p1)))U(p1))
+(((p0)U(p0))*((1)+(p2)))+(X((X((1)*(p2)))U(0)))
+(X(p1))R((X((0)R(p1)))U(((X(p0))R(X(p2)))*(p2)))
+((0)U((p0)*(p2)))R(((X(0))R(X(1)))+((0)+(p0)))
+((((p2)+(p2))R((p0)U(p1)))U((p2)*(p0)))R((1)+(p1))
+(X((((p2)U(p0))+(p0))+((p0)U((p1)+(p2)))))U(X(p1))
+(((1)+(p0))*(p0))U(((p1)U(X(p0)))R((X(p0))R(p0)))
+(X(p0))+(X(((1)*(X(p0)))*(((p1)+(X(1)))+(0))))
+X((((0)R(p0))U(X((X(p1))R(p2))))U((X(p0))R(p2)))
+(((p0)+((1)+(p2)))R(((p2)+(p2))R(p2)))R((0)U(p1))
+X((p1)*((X(p0))R(((p2)*(X((p1)R(p2))))*(X(1)))))
+(X((1)+(p2)))R(X(X(((0)R(X(p1)))+((p0)U(p2)))))
+(1)*((X(((p1)+(p0))U((X(p2))U((p2)+(p0)))))+(1))
+X((X(X((((X(p1))R(0))*((p1)R(p0)))+(p2))))U(p1))
+(p1)*((X(p0))U(((((0)R(p1))R(p1))*(0))*(X(p1))))
+(((p1)U((X(p0))U(X((p2)*(p0)))))*((p2)U(p2)))U(p1)
+(X(((X(p2))+(p1))R((p2)R(X(p0)))))*((X(1))R(p1))
+((p0)+(((p2)+(X(X(1))))R(p2)))U((X(1))R(X(0)))
+X((((X(p1))R(p0))+((1)+((X(p0))U(X(p0)))))+(p2))
+(p2)*((((1)U(p0))U((X(p1))U((1)R(p1))))*(X(p2)))
+((X(0))*((X(p1))R(X(((1)U(p1))+(p1)))))U(X(p0))
+((1)R(((1)R(p0))U(0)))U((X(p0))+((p2)R(X(p0))))
+X((((p1)U((p2)R(1)))U(p0))U((X(0))R((1)R(p0))))
+((((X(p2))*(p2))R(p1))U((p1)U((1)*(p2))))R(X(p1))
+X((((p2)U(p0))+(X(p1)))*((1)*(((p1)U(p1))R(p2))))
+(((X(X(1)))R(X(p1)))R(p2))U(((p0)+(X(0)))U(p0))
+((X((p1)U(p1)))R(p2))+(((0)R(X(p0)))R((1)R(1)))
+((X(1))R(X(0)))*(X(X(((p0)*(X(p2)))*(X(p1)))))
+(X(p2))+((X((p2)+(((p1)U(p1))U(X(p1)))))*(X(p1)))
+(((p1)+((X(0))U(p2)))*((p2)*(p1)))U(X((1)U(p2)))
+X(((0)U((p1)*(0)))+((X(1))U((X(1))*(X(0)))))
+(((p2)U((0)+(p0)))U(p2))+(((X(p2))*(p2))*(X(p0)))
+(X((X(X(1)))R((p0)+(X(0)))))+((p1)R((p1)R(p0)))
+((p0)+((p1)R((p0)R(p1))))R(X((p2)+((X(p2))+(p2))))
+((p0)U(X(p1)))R(((1)*(X(p1)))*((X(1))U(X(p1))))
+(X((p2)R(p1)))R(((1)R(X(p1)))U((X(p2))R(X(p1))))
+(X(p0))U(((p0)*(X(1)))+(((p0)U(X(p0)))R(X(p2))))
+X(((p1)R((X(p1))U((0)+(p1))))*((X(p0))*(X(p2))))
+X((((X(p1))+(p2))R((X((p2)R(p0)))*(p1)))R(X(0)))
+(((p1)+((0)+(p2)))+(p1))R((X(1))R((p2)*(X(p1))))
+(p2)*(((X(p1))+(X((p1)+((p2)+(p1)))))R((p0)R(0)))
+((p1)+((X(p0))U(X(X(X(X(p0)))))))+((p1)U(X(p1)))
+X(((p2)+(X(p0)))*((p0)+(((0)U(1))*(X(X(1))))))
+X((X(p2))U(X((((p1)U(X(p0)))U(X(0)))U(X(1)))))
+(X((p1)+(((X(1))+(1))*((p2)R(p2)))))U((1)U(p0))
+(p2)*(((p0)R(0))R((X((p1)R(p1)))R(X((p1)U(p1)))))
+X(X(X((((p0)R(X(p2)))*((1)+((1)+(1))))+(1))))
+(p0)R(((p0)+((X(((p2)U(0))U(p1)))*(1)))+(X(p1)))
+((X(p1))U(1))*((X(p1))*((((0)R(p1))U(p2))*(p2)))
+(X((X((p0)+(X(p1))))*(X(p2))))R((p0)+((p0)*(1)))
+(((p1)+(X(p1)))+((p1)R(X(0))))R(X((X(p0))U(p1)))
+X(((X(p1))U((1)R(p1)))R(((p2)U(p0))R((p0)R(p0))))
+X((X(p2))+((((p1)+(X(1)))+(p0))+((p2)R(X(p1)))))
+(p2)R(((p0)*((0)U((p0)R(p1))))U((X(p2))R(X(p1))))
+((p1)+(((X(p1))U(X(p1)))*(X(p2))))R((p2)R(X(0)))
+X((((p2)U(p2))*((p2)U((X(p1))U(1))))R(X(X(1))))
+(((X(p0))R((p2)U(X(0))))U(X(p2)))+(X((0)R(p0)))
+((X(p1))R((X(1))R(X(p1))))+(((1)U(X(1)))R(1))
+((X(p1))R((X((p0)U(X((p0)+(p2)))))+(1)))R(X(p1))
+((p1)U(p1))+(((0)U((p2)*((X(p2))+(X(p2)))))R(p2))
+((X(p2))U(X((X(p1))U(X((0)R((0)+(p2)))))))R(p1)
+(X((p1)U(p1)))R((X((p2)U((p2)R(p2))))*(X(X(p2))))
+((((X(p1))U(p1))U((p2)U(0)))R(p2))*((1)*(X(p0)))
+X(((1)R(p0))U(X(((X(p2))R((X(p1))R(1)))*(p2))))
+((X(1))+(((p0)*(X(p2)))U((X(0))R(p0))))+(X(1))
+(((X((X(p0))R(X(0))))R(p0))R(X(1)))*((p2)R(p0))
+X((X(0))+(X((X((p0)+((X(p0))R(0))))U(X(p2)))))
+(X(p1))R(X((X((p1)+(X(0))))U((X(X(1)))*(0))))
+((((p2)*(p2))+(p0))+((p1)R(p1)))R((X(p2))*(X(p1)))
+((1)U(X(((((1)+(p0))R(1))U(1))+(p2))))U(X(p1))
+((X(1))U(X(p1)))*(((p1)R(p2))+(((p0)U(p1))+(1)))
+X(X(X(X(((((0)*(1))R(X(1)))+(p0))R(X(p0))))))
+((X(p2))+((((p1)U(p0))R(p0))U((p1)*(p0))))+(X(p2))
+((X((X(p2))U(p2)))U(X(p2)))U((X(X(X(p0))))U(p1))
+(((p2)R(p2))U(X(((p1)U(p2))R(1))))U((X(p2))U(0))
+(((p0)U(X(X(0))))U((p1)*(0)))U((p1)R((p2)*(p0)))
+((p1)U(1))U((1)U(X((((p2)*(p1))R(p2))R(X(p0)))))
+((((p1)+(p2))U((p1)R((X(1))+(0))))R(p1))U(X(p1))
+(p2)R((p2)R((X(p1))+((X((p1)U(p1)))U((1)+(p1)))))
+((X(p0))R(X(p2)))+((0)R((((p2)+(0))*(p0))R(0)))
+(((p1)+(X(p2)))R(X((0)+((p0)+(X(0))))))+(X(0))
+((p2)R(0))+((((X(p1))R(p2))U((X(0))U(p1)))+(1))
+(((X(1))R(0))R(X(X((p2)+(X(p2))))))*((p1)R(1))
+((X(p0))U(X((p0)R(p0))))+(((p2)U(0))R((p2)*(p2)))
+((0)*((p2)+(X((p0)R(X(p0))))))*(((p1)*(p0))R(p1))
+(((p2)R(1))*(p0))*((((p0)*(p0))R(p1))U(X(X(p0))))
+(((X(p0))+((p1)R(p2)))U(p2))R((0)U((X(0))U(p0)))
+((X(p0))*(X((p1)R(X(p2)))))+((X(p2))U(X(X(0))))
+(X((((X(p2))R(p2))+(p2))U(p2)))R((0)*((p0)R(p0)))
+(((X(p1))U((X(p0))U(p1)))R(((0)U(p2))U(p2)))U(p0)
+((((X(p1))U(p1))R(0))R((X(p1))*((p2)*(p0))))R(p0)
+(p2)R((p0)R((X((X(0))U(p0)))R((X(p1))+(X(p1)))))
+((p1)*(p0))+(((p2)+(p0))U(((X(1))+(X(p0)))*(0)))
+((X(p0))+((1)*(X(p2))))*((p1)U((0)U((p2)U(p0))))
+(X(X(((p1)R(0))U(p0))))+(X(((p2)U(p2))R(X(p1))))
+((0)+(0))R((((X(0))+(p0))*(1))+((X(p1))U(0)))
+(p2)R(((X((p0)R(p1)))R(0))+((p2)U((X(1))R(p2))))
+X(((p2)U((p0)*((p1)+(p0))))*(((p0)*(p2))*(X(0))))
+(X((p0)*(p2)))+(((X(p1))R(X(p1)))R((X(p2))+(p1)))
+(X(((X(p2))U(p0))U((X(p0))U(X(p1)))))U((p0)U(p2))
+((((1)+(X(p0)))U(X(p0)))U(p0))R((p2)R((p1)+(0)))
+(((0)R((0)U(X(p0))))+(1))+((X(X(p1)))U(X(p0)))
+X(((p1)U((p2)R(p0)))+((p1)U(((X(p1))+(p0))R(0))))
+((X(p1))U(X(p1)))R(X(((1)*(p1))U((p1)R(X(p1)))))
+((X(p1))U(X(p0)))U(X((((1)+(p2))+(p1))R(X(p1))))
+(((X((p1)R(X(1))))R(X(p1)))R(X(X(p2))))U(X(1))
+((p1)R(X(p1)))+((p2)*(((X(p2))+(p2))U((p2)R(p1))))
+((X(X(((p2)R(p0))U(X(p0)))))R((1)+(X(p0))))R(p0)
+((X(p1))+((p2)*(X(0))))+((1)+(X((p2)+(X(p1)))))
+(X((X(X(p2)))*((X((p2)+(0)))R(X(X(p0))))))*(p2)
+(X(X(0)))R((((p1)+(p2))R((X(p2))R(1)))U(X(p2)))
+(p2)R((((p1)R(X((p2)+(p2))))+((p2)R(1)))U(X(p2)))
+X((0)+((((1)U(X(X(0))))R(p2))*((p0)R(X(1)))))
+X((X(p2))R(((X(X(1)))+((X(0))U(p0)))+(X(p2))))
+(X(((X(p2))R((X(p2))+(p0)))U(p1)))U((X(p1))U(1))
+(((p0)*((X((0)*(p2)))U(X((p2)+(0)))))*(1))R(p1)
+((((p0)R(p0))U((p0)+(p1)))U(X(p2)))*((p1)R(X(1)))
+(X(((p2)+(p2))*(((X(p2))U(X(1)))R(X(p0)))))U(1)
+(X(p0))U(X(((0)U(p0))R((((p0)U(1))U(p0))*(p0))))
+X(((X(p0))*((X(p1))*((p1)U(p2))))U(X((p2)U(p1))))
+(((p2)U(p0))R((p2)+(p0)))U(((p1)+(p0))U((1)R(p1)))
+((p1)+((X(p0))*(X(p2))))U((X(0))R(X((p0)U(p0))))
+X(((X(p1))U(X((X(X(X(p0))))+(p0))))U((p2)R(p2)))
+(X(p2))+((X(p1))U((X((X(X(1)))*(X(p1))))U(p1)))
+X(((X(p0))*(X((X(1))U(X(0)))))U((X(1))U(1)))
+(X(((X(0))+(X(p2)))+((0)*(p2))))R((X(p2))+(0))
+(((p2)+(0))U(p0))R((X(p2))R((X(X(X(0))))U(p2)))
+((((X(1))U(X(p0)))R(p2))U(X(p2)))U((0)*(X(1)))
+((X(p0))R((X(p0))*((p1)R(p1))))U((X(0))R(X(1)))
+(p1)U(((((p0)U(1))U((1)*(1)))R(p0))R(X(X(0))))
+(1)*(((p2)R(((X(0))U(1))*(1)))U((X(1))*(0)))
+(((((p1)U((p1)R(p2)))R(p1))R(p1))*(p1))R((p1)U(0))
+(X(p1))U((p2)*(X(X((p0)U((0)+((X(0))+(p0)))))))
+(X(p0))U(((X(p1))*((1)U(p0)))*(((p0)U(p0))U(p1)))
+(((X(p0))+(X(p0)))+(X((p0)U((p2)U(X(p0))))))R(p2)
+((X(0))R(p2))+(X(((p2)*(X(0)))U((X(0))*(p2))))
+(p1)U(((0)*(((p2)U(p2))U(p2)))U((0)U((p2)U(p0))))
+(X(((p1)*(p0))+((1)U(p1))))U(X((0)*((1)R(p2))))
+X(((p2)+(0))U(X(((X(0))*((p0)+(1)))U(X(p2)))))
+(((p2)+(p1))R((1)U(p1)))U(((X(p0))U(p2))U(X(p1)))
+(((X(p0))*(p1))U(((p2)U(p1))U(p1)))U((p0)R(X(p0)))
+(p1)+(X(X((X(p0))U((((0)R(1))+(X(1)))R(p0)))))
+((X(p1))*((X(p1))R(0)))U(((0)+(X(0)))U(X(0)))
+(p1)*((((p2)*(p1))R((X(1))+(X(X(p2)))))*(X(1)))
+((X((X(0))+((p2)+(p0))))R((p0)+(X(1))))U(X(1))
+(((p0)R(p0))+(X((0)+(X(p0)))))U(((p1)*(p1))*(p1))
+(X(p0))+(((((p1)*(p2))U(X(1)))*(p1))*((p1)U(p2)))
+((1)R(1))*(X((X((p1)*((X(p2))+(p1))))+(X(p2))))
+(((X(p1))R(p1))U(X((p2)U(X(p0)))))R((X(1))U(p0))
+X(((p2)U(p2))R((((p2)R(p1))R((p1)R(p0)))U(X(p1))))
+((0)*(((p1)U(p0))+((p0)U(X(1)))))*((p1)R(X(p2)))
+((((p0)+(1))*(p2))U((0)U((p0)R(1))))+(X(X(p2)))
+(((p1)R((p2)*(X(p2))))R(p1))*((0)R((p2)+(X(1))))
+(p2)+(X(((((1)U(p0))U(X(p2)))U((p0)+(p0)))R(p2)))
+X(X((((X(0))U(p2))R((X(1))*(X(p1))))+(X(p0))))
+(((X(p0))*((X(X(p0)))R(p1)))*(p0))R((X(p1))U(p0))
+((X(p0))U(((X(p1))R((X(p2))U(p1)))R(p1)))+(X(0))
+(((p2)U(p2))*((p1)+((X(p1))U(X(p2)))))R((1)U(p2))
+((X(p1))U(X(p2)))U((p2)R(X(X((p0)R(X(X(0)))))))
+(X(0))U((X(X(0)))U(((p1)R(p0))+((X(p0))U(p0))))
+(p2)R(X(((1)U(X((X(p2))+(p1))))*((X(0))R(p2))))
+X(((X(X(X(0))))R(1))*((0)*(((p2)*(p0))R(p0))))
+(X(X(p1)))+((((X(p1))*((p1)R(X(p2))))*(p1))+(p0))
+((X(p2))+(((p2)+(0))U(X(p1))))U(X((X(p2))+(0)))
+((1)U(X((X((1)+(X(p0))))U(X(p0)))))U((1)*(p0))
+(((p0)R(((0)R(p1))U((p2)U(p2))))+(X(X(1))))U(p2)
+(((p1)*(p0))U((0)*(p1)))U((X(p2))R((1)*(X(1))))
+((X((X(0))U(p1)))U((X(X(0)))+(p2)))*((p1)U(p2))
+X((((X(p1))+((X(p1))R(p2)))R(X(0)))R(X(X(0))))
+((0)U(p1))*(X((X((X(p2))R(X(p2))))U((0)*(p0))))
+((X(0))U((X(p1))U(((X(1))U(p0))R(p0))))+(X(p2))
+(1)+(X(((X(p0))R(X(p1)))*(((1)*(p2))R(X(p2)))))
+X(((X(p1))+(X(p1)))+((X(0))U((X(p2))+(X(p1)))))
+(X(((p2)U(p0))R(p0)))*((X(X(p2)))+(X((p2)+(p1))))
+((X((X(0))+(X(0))))U((p2)U(X(p1))))+((p2)R(p0))
+(((X(1))R(p1))R(X(1)))+(((1)+(p2))+((p2)R(p0)))
+((((X(X(p2)))+(p1))U(X(p0)))R((1)R(X(1))))U(p0)
+X((p1)R((((1)U(p2))R(X(p2)))U(X(X(X(X(p2)))))))
+(X(p0))U((((p2)R((p0)R(1)))*(p0))U((X(p2))*(p1)))
+X(((p2)R(p2))U((X(p0))+((X(p2))U((p0)U(X(p1))))))
+((p2)U((X(X(p0)))U(X(p0))))*((X(p2))+((p0)R(p2)))
+(((p2)R(p1))+(X(p2)))U((X(p1))*(((1)+(p0))+(p0)))
+X((X(X((p2)R((X(p1))*((0)R(0))))))U((p0)U(1)))
+(((p2)U(X((X(p0))U(p2))))*((p1)R(p2)))R(X(X(p1)))
+((p2)U(((X(p0))+((p1)*(p1)))R(p0)))R((p1)U(X(p1)))
+(((p0)+(0))*(X(0)))*(((p1)+(1))R((X(p0))*(p1)))
+(((1)*(p0))R(X(p1)))U(((X(0))R(p2))U((p2)U(0)))
+((p0)*(X(p0)))*(((X(0))R((0)+(p0)))U((p2)+(0)))
+X(((X(0))U((p2)U(0)))U(X(X((0)*(X(X(p2)))))))
+(X(p1))*(X((X(p2))*(((X((1)R(p0)))U(p2))R(p2))))
+(((p1)U((X(0))+((p0)R(p1))))R(X((1)R(p1))))*(p0)
+(X(p2))R(X(X(X(X(X((p1)*((X(0))U(X(p1)))))))))
+(p0)*(((p0)R(X((X(p1))R(p2))))U(((p2)*(p2))R(p2)))
+(X((X(p1))R(X(p1))))*((X(p2))U(((p1)U(p1))*(p1)))
+((((0)R(p0))R(p0))U(X(p0)))+(((p2)R(X(p2)))U(p1))
+((X(p1))*(((X(p0))+(p2))*(p1)))R(((p0)*(1))R(p0))
+((X(0))U(X(((p1)+(p2))U((p1)+(0)))))R((p1)U(1))
+X(((((X(p2))+(p1))+((1)U(p2)))R(p0))U((p2)U(1)))
+(((1)R(X(p1)))R((p2)U(X(p1))))*((1)U((p2)+(p2)))
+(X(p1))U((X((0)+((X(p2))+((1)U(p0)))))U(X(p0)))
+((p1)U((X(p1))U(p2)))R(((X(p1))R(p0))+((p2)R(p1)))
+((X(p1))R(((p1)+(p0))U((X(p2))*(p0))))R((p1)+(p2))
+((X(p1))U(((X(0))U(p1))R(X(p1))))U(X((0)+(p1)))
+X(X(X((1)R((p2)U((X(p1))+(((p1)U(p1))R(0)))))))
+((p0)*(p1))U(((p1)R(X(p1)))+((X(p2))*((1)R(p1))))
+((1)*(X(p0)))U((X(X(p0)))U((p1)R((p2)*(X(p2)))))
+X(((((p0)R(0))*(p1))U(X(0)))+((p1)*((p2)+(0))))
+(((X(1))U(X(p1)))R((X(p1))U((0)R(p2))))U(X(p1))
+(((X(p1))U((X(p2))+(p2)))*((p0)+(p1)))U((0)R(0))
+X((((X(p1))*(X(p2)))R((p1)R(p0)))*((0)+(X(1))))
+((p1)+(X(0)))R((p0)U((((X(p0))R(0))R(p2))+(p0)))
+(((X(p0))U(((1)+(p1))+(p2)))+(X((p2)U(p0))))U(p2)
+((p0)U(X(X(p2))))*((((p2)*(X(p1)))R(X(p2)))+(p1))
+(((p1)R(0))U(p2))R((X((0)U((0)*(p1))))U(X(1)))
+((p0)U(1))R(((1)U((p1)R(p1)))*((X(p2))R(X(0))))
+((((p0)+(X(p2)))U(X(p0)))R(X(p0)))U(X((p1)U(p0)))
+((1)U(((p1)R(p1))R(X(X(p0)))))+((1)R((p2)U(0)))
+(((X(p0))*((p1)U(p1)))U(p1))R(((X(p2))U(1))U(p2))
+(X(p2))U((X(p2))+((X(1))U(((p2)*(p0))+(X(p2)))))
+(((0)R(p2))*(1))*(((p1)R(X(p0)))U(X((0)U(p1))))
+(X(((p1)U(0))R(((X(p2))*(p0))U(p0))))R(X(X(0)))
+((X(p2))R(((X(p0))+(p2))+(X(p1))))+((X(p1))R(p1))
+X((X(p0))R(((p0)U((X(1))U((1)*(X(1)))))+(p2)))
+(((p1)+((X(X(p1)))*(X(p1))))+((p0)+(p1)))R(X(p0))
+((X(((X(p1))*(p2))R(p0)))U((p1)*(1)))U((p2)R(p0))
+((X(p1))+(p1))*(((0)*(p1))*(((p0)+(p0))+(X(p2))))
+(((p2)*(p1))R(0))U(X(X((X(p0))U((p0)U(X(0))))))
+((X(X(X(p0))))+((0)R(p1)))U((1)R((p0)U(X(p0))))
+((((p2)U(p0))+(((p0)R(X(p2)))U(p0)))+(1))*(X(1))
+X(X((X(p2))U((1)*(((X(p1))U(p1))+((p2)R(p0))))))
+(((p2)+(p2))R((p2)R((X(0))U(X(p1)))))+((p1)*(p0))
+((((X(p2))R(X((X(0))R(p2))))*(X(p1)))U(1))*(1)
+(X(((1)*(p1))R((p1)+(X(p2)))))R(X((p0)R(X(p0))))
+X((X((p2)+(X(0))))R(((X(1))R(p1))R((1)*(p1))))
+X((((X(((p2)R(p2))R(p0)))+(X(p0)))R(0))+(X(p1)))
+((1)R((p2)R((p0)*(X(p2)))))R(X((p1)+((1)R(p0))))
+((p2)U(0))*((X(p1))+(((p1)U(p0))U((X(p1))*(p0))))
+((X(p1))*((X(p0))U(1)))R(((p1)U(X(p0)))U(X(p2)))
+X(((X(p2))U(X(p0)))+((X(X(1)))U((p2)R(X(0)))))
+((X(1))R(X(p0)))R(((X(p1))U((X(p2))+(1)))U(p1))
+(((X(0))+((p2)+(p2)))R(p0))R((p1)R((X(p1))R(p2)))
+X(X((((p2)R(p2))U((p2)R(p0)))*(X((X(p2))*(p2)))))
+X(((X(1))R(X(p0)))+(X(((X(p1))U(1))U(X(p0)))))
+((X(1))U(X(p0)))R((((X(p1))R(p0))R(p1))+(X(1)))
+((p2)+((1)U(0)))R((p1)*((p0)U(X((p2)*(X(1))))))
+X((((X(p0))+(((p0)*(p1))*(X(p0))))+(0))U(X(p2)))
+X(((0)R(((p0)R(p2))R(1)))+((p1)U((p0)R(X(p1)))))
+((p0)+((X(p2))+(p0)))U((((p0)U(p2))R(X(0)))U(p0))
+X(((((1)R(X(p0)))R(X(0)))R((p2)*(p0)))U(X(p1)))
+X(X(((X(p2))*(X(p0)))R(X(((p2)U(1))+(X(p2))))))
+((p2)R(p1))R((p1)*(((((p0)+(p1))R(p2))U(p0))R(p1)))
+((p2)+(0))R((p1)+(X(((X(1))U(X(p0)))U(X(p1)))))
+X(((X(p2))+((p2)R(p2)))*(((X(p0))R(X(p2)))+(p2)))
+((p1)R((p0)U(X(p1))))R((((p0)U(p1))U(0))R(X(p0)))
+(((X(X(1)))U(((p1)U(p0))+(1)))U((p1)R(p2)))U(1)
+X(((p2)+((1)R(X(p0))))*(X(((X(p0))*(p0))U(0))))
+((((X(p0))R(p0))U(X(X(p2))))R(p2))+((1)R(X(p2)))
+((X((X(p0))U(X(1))))+((X(p0))+(p1)))*(X(X(p0)))
+(((X(p0))R(p1))U(X(p2)))R(((p0)U(p1))*((p1)*(p1)))
+(0)U(((p2)R(p0))R(((p1)*((p0)U((p2)*(p0))))U(p1)))
+((((X(p2))*(p1))*(p0))U(p1))R(((X(p1))U(p0))U(p0))
+(p0)*((X(X(0)))R(X((((p1)R(p1))*(X(1)))U(p1))))
+(((1)*(X(p2)))U(X(p1)))R(((1)*(p0))R((p1)U(0)))
+((1)*(X(0)))R(((p1)U((p0)U(p2)))R(X((p2)*(0))))
+(((p2)R(p2))R((1)U((X(p0))U(p0))))R((1)U(X(p1)))
+((X(p0))*((p1)R((X(p1))U(p2))))U(X((p2)U(X(p2))))
+((0)U(((1)R(p2))U(X(X(p1)))))U(((p0)U(p1))R(0))
+((p1)R(p0))U(((p1)R(p2))*((X(p1))U((p2)R(X(p0)))))
+((X(1))*(X(X((X(p1))U(X(0))))))R((p1)U(X(p2)))
+(X((X(X(p2)))U((0)+(X(0)))))U(((1)R(p1))R(p1))
+X(X(((X(0))R(X(X(1))))U((X(1))+((p1)+(p1)))))
+(X(1))+(X((((X(p2))R(p2))R(p1))R((p2)R(X(1)))))
+((0)U(X(p1)))R(X((p1)U((X(0))*((X(p1))+(p2)))))
+(p2)+((p1)U(((p2)U((1)R(p0)))U(X(X((p0)U(1))))))
+(((p2)+(X(p1)))U((X(p0))+(X(p0))))*((p2)+(X(p1)))
+(((X(p2))U(X(p1)))R(X(p0)))R((X(0))*((p0)R(p2)))
+X(((X(p1))U((1)R((1)R(p2))))*((0)+((p1)*(p1))))
+((1)R(X(0)))*((p1)R(X((X(X(p2)))U((p1)U(p1)))))
+(((1)R(X(p2)))*(X(p1)))*((((p0)+(0))R(1))*(p1))
+X((((p0)R(0))R(X(1)))U(X(((p2)U(X(p0)))U(p0))))
+X((X(X((p2)R(p1))))U(((p0)U((X(1))*(p0)))U(p1)))
+(p0)U((X((p1)R(0)))R(X(((X(p1))+(p2))R(X(p2)))))
+((p2)*(((1)*(X(p0)))+(X(p0))))+((X(p1))+(X(p1)))
+(((X(1))U(p1))+((p2)U(0)))+((p2)U(X(X(X(p2)))))
+((p2)R((0)*(0)))U((X((1)*(p1)))U(X(X(X(p1)))))
+X(((X(X((X(p2))U((0)U(1)))))U((1)*(p1)))U(p2))
+(((X(p0))U(X(p2)))*((p0)*(1)))U((p1)U((0)U(1)))
+((p2)U((p0)+(p1)))R(((p1)U(p1))R(((p0)+(p0))U(p0)))
+(p1)+(((X(p2))R((p1)R(p0)))U((X(p2))*(X(X(0)))))
+((p1)U(p1))U(X((p2)U((p0)*((X(0))U((p2)*(p2))))))
+((X(p2))U(((X(p0))U(p0))+(p1)))+((p0)U((p1)*(p2)))
+((1)U(X(((X(p0))U(X(0)))R(X(p1)))))+((0)U(p2))
+((X(1))R(X(p1)))+(((p0)*(X(p1)))U((X(0))*(p1)))
+((X(0))R((p2)R(p0)))*((X(((p0)U(p2))U(p0)))U(0))
+((p1)*((X(p1))R(X(p1))))R((X(X(p0)))R((p2)R(p1)))
+(X(X((1)U(X(p1)))))U((X((0)U(p2)))+(X(X(p0))))
+((X(p2))U((((p0)R(p0))R((X(0))+(p1)))R(0)))U(p0)
+(X(X(((X(0))+(p1))R(X(p2)))))*((p0)+(X(X(p0))))
+((((X(p1))*(1))R(X(0)))*(p1))+((p1)U((p0)R(p0)))
+((p2)+((p0)R(p1)))U((((p0)U(1))*((p2)R(p0)))*(p2))
+((X(p1))*((X(p0))*(X(p0))))U(((p2)R(p2))+(X(1)))
+((p1)U((0)R(1)))U(((p2)+(p1))*((X(0))R(X(p1))))
+((X(p0))U(p2))R((((X(0))R(p2))U((0)+(p1)))*(p2))
+X(((X(X(p1)))+(1))*((p1)U(X((p0)+((p1)*(p1))))))
+((1)R((p0)U(X(0))))*(((X(0))+(X(0)))U(X(p0)))
+X((0)*((((p0)U(0))*(((1)U(0))R(0)))+(X(1))))
+X(((p0)+(p0))R(((p0)R(X((p1)*(X(p2)))))+(X(p2))))
+((X(X(p1)))R((X(0))U(X(p2))))U((0)R((p0)R(p2)))
+((X((p0)R(p1)))*((p2)R(p0)))R(X(((p1)R(p0))*(p1)))
+(X((((p0)*(X(X(X(0)))))U(p2))+(X(p0))))*(X(p2))
+(p0)*(X((((X(0))U(p0))+(X(p2)))U((1)R(X(p1)))))
+((X((p2)U(p2)))*(p2))U(((p0)R(X(p0)))U((p1)R(p2)))
+((p1)U(X(0)))R(((X(p0))R(p0))R((p0)R((0)R(p1))))
+(X((p1)R((p0)R(X((p1)U(p1))))))U((X(p0))+(X(p2)))
+((p0)R(p1))R(((p0)U(1))*((p1)+(X((X(p2))+(p0)))))
+((p2)U(X(p2)))R((((p2)U((1)R(1)))*(X(p1)))U(1))
+X(((0)R(X((X(p1))R((p2)+(p0)))))R((X(1))U(p0)))
+((((X(X(p2)))R(X(X(1))))U(1))*(X(p0)))U(X(p1))
+(((p0)+(p1))U((p1)R((p1)R(p2))))R((X(X(1)))U(1))
+X(X(X((p0)R((X(p1))U(((X(0))+(X(p0)))R(1))))))
+((X(1))*(((p2)U((p2)R(0)))*(0)))*(X((p0)R(p2)))
+(((((p1)+(p2))*(p0))*(X(1)))+((p1)R(X(p0))))R(p0)
+((p2)*(((p0)+(p2))R((p0)R(p1))))U(X(X((p0)U(1))))
+X((X(p2))U((X(p2))U((X(p2))U((X(1))R(X(p0))))))
+(X(p0))U((0)U((((0)+(1))*(X(X(1))))+(X(0))))
+(((X(0))*((p2)*(X(p0))))+(p2))U((0)U((p1)R(p1)))
+((1)R(X((p2)+(p2))))U(X((X(0))*((X(0))R(p0))))
+((p0)R(p2))U(X(X(((X(0))+(p0))U(X((p0)+(p1))))))
+(((X(p2))U((p2)R(X(X(p2)))))U((p0)R(0)))U(X(p2))
+((p2)R((p1)U(X(X(p1)))))U(X((X((p0)*(p0)))R(p2)))
+(((p2)R(p2))+(X(0)))R(((p0)*(1))*((p1)+(X(p0))))
+(X(((X(p1))U(p2))U(X((p0)*(p1)))))U((p1)*(X(p0)))
+((X(p2))*(X(p1)))U((p1)+((X(p2))R((X(0))*(p0))))
+((X(p2))*(X(X(0))))R(((p2)U(p2))R((p1)R(X(1))))
+X(X((((p0)U(1))U(X((X(p0))*(p1))))*((0)R(p2))))
+(((p2)U((X(1))*(p0)))R(p2))U((p1)U((p2)U(X(p2))))
+(p0)R(((X(p0))U(p0))R(X(((0)R(X(X(p2))))R(p0))))
+(((1)U(p2))R((X(p2))*((p0)U(0))))*(X((1)+(p2)))
+((p0)+(p0))R((((p2)+(X(p2)))U((p1)R(X(p1))))R(p2))
+(((X(p2))U(0))+(X(p1)))U((X(X((p2)*(p1))))R(p0))
+(X(0))R(((X((1)U(((p0)R(0))U(0))))R(p1))U(p1))
+X((((X(p2))*(((0)U(p2))R(p0)))R(X(p0)))U(X(1)))
+((X(0))+((0)R(p2)))U(((p0)R((p2)*(p2)))R(X(p2)))
+X((((p2)*(p2))U((X(p1))*(p0)))*((X(0))+(X(p1))))
+(X(((p2)R((0)*(X(p2))))*((0)R(0))))R((p0)*(p0))
+(p2)R(((X(p0))U((p1)R(X(p1))))R((p0)U(X(X(p0)))))
+X(((0)U((((X(p2))R(p0))R(p0))*(p0)))U((p0)R(p0)))
+X((((p0)*(X(p0)))+(X(1)))U((X(0))*((p2)*(p0))))
+((1)R(p2))U((p2)U((((p0)*(p2))U(0))R(X(X(p0)))))
+((((X(p1))U(1))U((0)*((p0)U(1))))U(X(p1)))U(p0)
+((((X(p1))*(X(p2)))R(X(X(p2))))R(X(p1)))U(X(1))
+((X(p0))*((p2)U((1)U(p1))))R((p2)*((X(1))U(1)))
+(X((p0)*(X(X(p0)))))R(((X(p0))*(p2))*((p0)U(p2)))
+(X((p0)*(X(p2))))R((p0)+(((1)*(1))U((p0)R(p1))))
+((p0)*((p0)U((0)U(p2))))R((X(1))U((X(p0))U(p0)))
+(X((p1)R(X(((1)+(X(1)))*(X(p2))))))R((p0)*(p2))
+((p1)+((X(p0))U((p0)U(0))))+((X(p2))+((p2)R(p0)))
+X((((X(p2))+((X(p0))+(X(p2))))U(p0))R((1)R(1)))
+(X(1))R(((X(X(p2)))R(X(p1)))U((p0)R((p2)R(p2))))
+((1)R(X(p0)))*((p2)*(((p0)+(p1))U((X(p2))*(1))))
+(X((((X(1))U((p2)*((p0)R(p2))))*(p0))R(1)))U(p1)
+((((X(0))*(p2))+(p1))+((X(p0))+(p2)))U((p0)+(p1))
+((p2)R((p0)R(p0)))+(((0)U(X(p0)))*((X(p1))*(0)))
+(p2)U(((((p2)R(p2))U((X(p2))U(p2)))*(1))+(X(0)))
+((X(p0))U((X(p2))*(1)))+((p1)U((p0)*(X(X(p1)))))
+(p2)U(((X(p0))U(1))+(X(((p0)R(p2))R((1)R(1)))))
+(p1)R(((p2)R(1))R(((p1)U((1)U(p0)))R((p2)U(0))))
+X((((0)U(X(0)))R((p2)R((p0)R((1)R(p0)))))*(p0))
+(X(((X(p1))R(X(0)))R(X(p1))))R((X(p1))U(X(p2)))
+(((p1)R(p1))U(((p2)U(0))R(X((p2)+(p1)))))U(X(p1))
+(X(((p2)R(X(p1)))R(1)))R((X(p1))R((X(p2))R(p1)))
+((X(p1))+(((p2)*(X(X(X(p2)))))U(p0)))R((p1)U(p1))
+(X(((p0)U(p0))+(p1)))U(((X(p2))*(0))+((p1)*(1)))
+((X(p2))U(p1))*(((p2)R(((p2)R(1))U(p2)))U(X(p2)))
+X((((p2)+(1))+(((X(p0))U(0))U(p0)))R((p1)R(p2)))
+(p0)+(((1)R(p0))U((((0)*(p1))+(X(1)))R(X(p1))))
+(((X(p0))U(0))R(p0))R(((p0)U(0))R((1)*(X(1))))
+X(X(((0)R(1))U(X(((X(p2))R(p2))R((p2)U(p1))))))
+(((X(p0))U(X(0)))R((p0)R(1)))R((p0)+(X(X(0))))
+(((p1)R(p2))*((1)R(p2)))*(X(X((X(1))*(X(p0)))))
+(((X(p2))+(0))R(p1))R((X((1)R(X(p0))))R(X(p2)))
+((p0)R(1))R((X(X((p0)+(1))))U(X((p1)+(X(1)))))
+(((0)+(p1))*(p0))*(X((X((p0)R(X(0))))R(X(p2))))
+(X(p1))R((p1)U((X(p1))R(((0)+(p2))*((p1)+(0)))))
+(X(1))U((X(p1))U((1)R((X(p0))R((0)*(X(p1))))))
+(((X(1))R(0))+(1))R((((p0)*(p2))*(X(p1)))*(p1))
+((X(p1))R(((p1)R(p2))R(X(p1))))+((X(p2))*(X(p2)))
+((X(p2))R(X(p2)))+(((p1)*(p1))+(X(X((p2)U(p1)))))
+(X(p1))U(((X((1)*(X(p2))))*((p1)U(X(p2))))U(p1))
+(X(X(((p2)U((p2)R(1)))+((p1)R((p2)R(p1))))))R(p1)
+((X(p2))R(p1))+(X(((1)U(X(X(0))))+((p2)+(0))))
+((0)R(p2))*((p0)R(((p2)*((p1)*(0)))R((1)+(p1))))
+((p2)*((0)U(X((p1)R(p0)))))R((p0)U((X(0))*(p2)))
+X(X(X((X(X(p1)))U((X(((0)+(1))R(p1)))*(p1)))))
+X(((p2)R(X(1)))R(((p0)U(p1))U(X((X(p0))U(0)))))
+((X(p1))U(X(1)))R((X((0)U(X(p1))))R((p2)+(p0)))
+((p0)*((p2)+(X(p1))))R((X(p2))+((X(p0))*(X(p0))))
+((X(((X(p2))*(p0))R(X(1))))U((1)R(1)))*(X(0))
+((X(p0))+(((p2)+(p2))R(p2)))U((X(0))R((1)*(p2)))
+X(((((1)+(X(0)))R(p0))U((p1)R(1)))+(X(X(p2))))
+((X(p1))U((p2)U(p0)))+(((p2)R(p2))*((p2)*(X(p0))))
+((((X(p0))R(p1))U(p1))*(p2))R(X(((p1)R(p1))U(0)))
+(((p2)R(X(((0)R(0))*(X(0)))))*(X(p0)))*(X(0))
+((X(p2))+((p1)R(X(p0))))R((X((X(0))U(p0)))R(p0))
+((p1)+(X(p2)))U((((p1)*(X(p1)))R(p1))R((p0)R(1)))
+(X(X((X((p1)*(p2)))R(p1))))+((p0)*((X(p2))+(p2)))
+((p2)+((X(p0))*(X(p1))))+(((p2)U(X(X(p1))))*(p2))
+((p1)R(1))+(X(((p1)R(X(p2)))U((p2)U((p2)*(1)))))
+(((p2)U(p0))R((p2)+((X(p1))R(1))))U((p0)R(X(p2)))
+((((0)R(X(0)))+(X(p2)))R((p1)U(p0)))+((0)R(p1))
+X((X(p2))+((p0)U(((1)+(1))R(X((p2)*(X(1)))))))
+((p0)R((p2)R((p0)*(0))))U((X(0))+(X((p0)R(1))))
+(p1)*(((p0)+(X(p2)))U((p0)R(((p0)+(p0))U(X(p0)))))
+((X(1))*((X(0))R((X(p2))U(p2))))+((X(p2))U(p2))
+X((X((X((X(p0))R((p1)*(0))))R(X(1))))R(X(0)))
+((X((p2)R((1)U(0))))U(X(p2)))U(((0)U(p1))+(p2))
+((X(p2))U(p0))R((X((0)U((p0)R(p1))))U((p1)+(p2)))
+X(((X(1))*((p1)R(p1)))*((((0)U(1))+(p2))*(p1)))
+((((1)+(X(p2)))+(p0))+(p2))+((X((0)U(0)))+(p0))
+(X(p0))+(((p1)*(p0))*(X(((p0)U(X(X(1))))U(0))))
+(X((X(1))R(X(p0))))U(((X(0))U(p1))U(X(X(p2))))
+(((p2)U(1))R((p2)*(p0)))R(((X(p0))+(p2))U(X(0)))
+(((p1)*(X(p1)))U((X(p0))*((p1)U((p0)R(p1)))))R(p1)
+X((X(p0))R((((1)U(X(p2)))R(X(1)))R((p1)+(1))))
+X((((p1)U(X(p0)))R((p1)R(X(p2))))+((p0)R(X(p2))))
+X(((X(p1))R(p2))+((X(p2))R((X(p2))U((1)U(1)))))
+(X(p2))+(X(((1)R((p2)+(p2)))R((X(p0))+(X(p2)))))
+((X(p2))+(p1))R((((p0)U(p2))U((p1)R(0)))R(X(p2)))
+X((X(p2))R(((X(p2))+((p0)U(p0)))R((X(p1))U(p2))))
+(((X(p0))R((p1)U(1)))U((X(p2))U(p0)))U((0)+(p2))
+(X(p2))U(((p1)*(X(p2)))U((X(1))U((p2)+(X(p2)))))
+(X(X(X(1))))R(((p0)*(((p0)U(p2))+(p1)))R(X(1)))
+((X(X(((X(p0))*(p0))R(p1))))*((p2)U(1)))U(X(p2))
+((X(0))+(X(0)))*(((0)U((1)U(p1)))+((p2)+(p2)))
+X(X((X((X(p2))U(((p1)+(X(p2)))U(p0))))U(X(p1))))
+(0)U(X(((p2)R((p2)*(p1)))*(((p0)*(X(p2)))U(1))))
+(((p1)*(p0))*(p1))*((X(p0))R(((X(p0))+(p2))U(p1)))
+((X(X(X((p1)U(p2)))))+((p1)U(p2)))+((X(p1))R(p2))
+((p1)U(X(1)))R(((X(p1))U(p1))*((X(p2))U(X(p0))))
+((p0)R(X((1)R(p0))))*(X((X(p2))R((p1)+(X(1)))))
+((p1)U(X(p2)))*(X((X(X(p1)))R((0)U((1)R(p1)))))
+(X((X(1))*(X(p0))))+(X(((X(p0))U(p0))R(X(p1))))
+(((p1)+(X(p2)))R(X((p2)+(X(X(p0))))))R((p1)*(0))
+((p2)U(p0))+(((p0)U((p1)R(X(p0))))R((p2)*(X(p1))))
+((X(0))*(X(1)))R(X(((X(p0))U((p1)U(p0)))R(p0)))
+(1)+((X((0)+(X(X(X(1))))))R(X(X((1)*(p2)))))
+(((X(0))U(X(p2)))+(X(0)))R((p1)+((X(p1))U(p1)))
+X(((X(p1))U(X(p1)))U(((p1)U(0))U((X(p2))R(p1))))
+X(X(((1)U(p0))+(X(X(((p1)+(X(p1)))+(X(p2)))))))
+X(X((((X(p0))R(X(p0)))*((1)R(X(p0))))+(X(p1))))
+(((p0)+(X(p0)))U((0)R((p2)U(X(p0)))))U((p2)U(p1))
+((((X(p2))U(0))R(X(X(p1))))*(p2))U((X(p0))U(p1))
+(X(p2))+((((X(p1))+(p2))U(p2))*((X(X(p0)))+(1)))
+(((p0)+(p0))+(X(X(p1))))R((X(1))+((X(p1))U(p0)))
+X((p1)*(((p2)U((1)+(p0)))U(((X(p2))*(p2))U(0))))
+X((p0)U(((X((p0)*(X(p0))))+(p2))+((p0)R(X(p1)))))
+((p1)R((p1)+(p0)))*((X(1))R(X(X(X((p1)+(p0))))))
+((X(p0))+(p0))U(((p1)U(X(X(p0))))R((X(p2))U(p1)))
+((X(0))*(((X(0))*(p2))R(X(1))))*(X((p2)R(1)))
+((p1)R(p1))*(((p0)U(p2))U(((p0)+(1))R((p1)R(0))))
+(((X(1))U(X(p1)))R((p2)*(X(p0))))U((p0)U(X(0)))
+(X((p1)R((X(0))R((1)U((p0)R(p0))))))+((p0)U(p0))
+X(X((((X(0))U(X(p1)))U(0))U((X(p0))*(X(0)))))
+(((X(1))*((p1)U(X(1))))R((p1)R(p0)))U((1)U(p2))
+X((1)U((((X(p1))R((p2)R(X(p0))))U(p2))R(X(1))))
+(X((p2)+(p0)))U(((p1)*(p2))U((X(1))+((p0)U(p1))))
+((X(p2))R(((0)U((p1)*(p1)))*(X(p1))))R((p2)*(1))
+(((p2)R((p2)R(p2)))R(0))+((X((0)U(p0)))U(X(0)))
+((X((p1)U(p1)))*((1)*(p1)))+((p2)U((X(p0))U(p0)))
+((X(p2))*((p2)*(p1)))U(((p1)U((X(p1))*(p2)))R(p1))
+(X(((p1)R(p2))*((p2)+((p2)R(X(p0))))))R((1)U(p1))
+X(((p2)R(X(p1)))R(((X(0))+(X((p2)U(1))))R(p0)))
+((((0)R(p1))*((p1)*(p2)))U(p1))U(X((X(p2))R(p0)))
+((((p1)*(p1))R(X((X(p0))U(1))))+(p1))U((p2)U(p2))
+((p0)R(X(p2)))+((((1)U(X(p0)))U(p2))R((p1)*(p1)))
+((X(p1))R((X(p2))U(1)))U((p1)U(((p1)+(p1))+(1)))
+X((X(p1))+(((1)R(X((p1)U((p1)U(X(p1))))))R(p1)))
+((X((p0)R(X(p0))))*(X((0)*(X(p1)))))+((p2)*(p0))
+(((p0)R(p1))*(p0))R(((p1)+(X(X(0))))+((p2)+(1)))
+((p1)R((X(X(p0)))U(p2)))U((p2)*((p0)U((0)U(p2))))
+X(((p1)U(p1))+(X(X(((X(p2))+(p1))+((p0)+(p2))))))
+(p0)R(((X(((1)R(p2))U(X(X(p2)))))R(p2))*(X(p0)))
+((X((p0)U(X((0)R(p2)))))*((X(0))U(p2)))*(X(p0))
+(p0)+(X(X((1)+((((X(p2))U(X(p2)))U(p1))R(p0)))))
+X((X(X(p0)))+(X(X(((1)U(X(p1)))*((1)U(p2))))))
+(X(p1))U(((p0)R(X(1)))U((X(p2))*((p0)R(X(p1)))))
+(((X(X(1)))U(p0))R((X(p2))U(p1)))U(X((1)*(0)))
+X(((((1)*(X(p1)))R(p0))*(X(0)))R((X(0))U(p1)))
+((p0)R(p1))U(((p2)U((X(p1))R(X(p0))))*((1)+(1)))
+((X((p1)+(p2)))R(X(X(p2))))R((X(X(X(p1))))R(p0))
+((X(p2))*((p0)R(p1)))U((X(1))*((0)R((p2)*(p2))))
+((X((0)R((p2)R(p0))))R((p0)R((p2)*(p0))))U(X(p0))
+(((p0)*(p0))R((p0)*(0)))U(X(((X(1))R(1))+(p2)))
+X(((X(p1))R((p1)+((X(p0))U(X(p1)))))*((p1)U(p1)))
+(((1)*(p0))*(X(p1)))+((X(1))R((X(1))U(X(p1))))
+((((p0)U(p0))R(p2))U((X(p2))U(X(p0))))R((p1)*(p1))
+(((1)R(1))R((X(1))*((X(p1))U(p0))))*((0)R(p0))
+(X((1)U(0)))*(((X(p1))*((1)R(X(1))))R(X(p1)))
+(((X(p2))U((p1)*(0)))U((p0)U(p1)))R((p2)R(X(0)))
+((p2)U(0))U((X((p1)U((p2)U((X(p1))R(p1)))))+(1))
+((p2)+((p2)*(((p1)U(0))R(X(p0)))))U(X((0)U(p1)))
+((p1)U((X(p1))R((X(X(p2)))R(p1))))R((X(p2))U(p0))
+((1)U((p2)R(p1)))U(X((X((p1)R(X(p0))))*(X(p1))))
+(((X(p0))R(X(p0)))R((p0)R(1)))*((0)R((p1)R(0)))
+((0)*((X((X(p1))+(X(0))))*((0)R(p0))))+(X(p2))
+((X((p0)+(p0)))+(p0))U(((X(p0))R(X(X(1))))*(p1))
+(((p1)*(1))+(p2))U((p0)R((p1)*((X(p1))R(X(1)))))
+X((((X(X(p2)))R(p0))*(((p2)U(p1))*(p2)))R(X(p0)))
+(X((p1)U(1)))U((X(X(0)))R(((X(p1))+(p0))*(p2)))
+((p0)U(0))+(((p2)*(((1)*(p0))R(X(p1))))+(X(p0)))
+(((p2)*(p2))+(1))U(((X(X(0)))*((1)U(p2)))+(p2))
+((p0)U(X((p2)U(X(p1)))))R((((1)*(p0))+(p2))+(p0))
+((X(p2))R((X(p0))R(X(X(p1)))))U((p2)R((p0)+(p0)))
+((((p0)R(1))*((p0)R(0)))U(p0))U((X(p0))U(X(1)))
+(((p2)U((p0)R(p2)))U((X(p1))U(X(p1))))R(X(X(p0)))
+((X(1))U(p2))+(((X(p1))U(X(p0)))U((p0)+(X(p2))))
+(X((p0)R(p0)))U(X((X(p1))U((X(p1))R((1)R(0)))))
+((X(p1))R((1)U((X(p0))U(p0))))+((1)+(X(X(p2))))
+X((((p2)+(X(p2)))*(p2))U(((p0)+(X(p2)))U(X(p0))))
+((X(p1))U((p2)U((X(p2))R(X(p0)))))R(X((p1)U(p0)))
+((1)R((p2)R(X(X((p0)R(p1))))))R(X((X(p1))+(p0)))
+((((p0)R(p0))U(p0))+((p0)*(p1)))U(((p1)R(p1))+(p0))
+((p0)*(X(X(p2))))+((((p0)U(p1))U(p2))+((p0)U(p2)))
+(((1)U(p1))R((X(p0))*(X(p1))))R(((p1)*(p1))+(p0))
+((X(p2))R((X((X(p2))R(p2)))+(p2)))R(X((p2)+(1)))
+((p1)U(p0))+((X((X(X(p0)))R(X(p1))))*((p1)R(p1)))
+((p1)+(1))R((((X(p0))R(p1))U(X(1)))+((p0)R(p1)))
+((0)U(X(1)))U(((p2)R(p2))R((p1)U((X(p0))*(p0))))
+((1)*(X(p0)))R(((p1)U(p0))R(((p2)*(p1))*(X(0))))
+((((X(p2))R(p1))R(X(p0)))R(0))R((X(p1))U(X(p0)))
+(p2)*(((X(X(p1)))U((p1)R(X(0))))R((X(p0))*(p2)))
+(X((p2)U(((0)*(1))+(X((p0)U(p0))))))R((1)*(1))
+X((X(((p1)*(p0))U((p1)*((1)U((p1)*(p2))))))*(0))
+((X(p0))+(X(p0)))U(X(((X(0))*(X(p2)))R(X(p2))))
+(((1)R((1)R(p1)))U(p2))+(X((p0)U((X(p2))R(p0))))
+(X(((X((p2)*(p0)))*(p2))R(X(p0))))R((X(p1))R(p2))
+(X(p0))R((X(((p2)+(1))U(p1)))R((X(p2))+(X(p0))))
+(p1)*(((X(p0))R(p2))R((X(X(0)))*((p2)U(X(1)))))
+((X(0))R((p1)+((0)+(0))))R((X(p2))U(X(X(p2))))
+((X(p2))+(X(p0)))R(((1)+((p1)U(X(p0))))R(X(1)))
+((X(p0))+(X((p2)R(X((X(p2))U(1))))))+((p1)R(1))
+X((((X(X(0)))+(X(p0)))+((p2)R(X(0))))U(X(p2)))
+((X((X((p0)R(p1)))U(X(p2))))*((p0)+(p2)))*(X(p2))
+(X(((((p1)*(p1))+(p2))R((p0)+(0)))U(X(0))))U(0)
+(((X(0))*(X(X(0))))U((p2)*(p0)))R((p1)U(X(1)))
+(X((X(p2))R(1)))R(((1)U((X(p2))+(p2)))U(X(p0)))
+X(((1)+((0)R(p2)))U(((X(p0))U(X(p0)))U(X(0))))
+(((1)R(p1))R(X((p1)U(X(p1)))))R((p0)U((1)*(p1)))
+((p1)*((X(p1))*(0)))+((X(X(p2)))R((p1)*(X(p0))))
+(((p0)*(p0))U((0)U(X(X(X(1))))))*((1)*(X(p1)))
+(((p0)U((p0)R(((p0)R(p2))R(p2))))U(p0))U((p2)+(p0))
+((((X(X(0)))U(p2))R(X(p2)))*((X(1))R(p1)))+(1)
+((p2)U(X(p1)))R((1)R((X(X(1)))R((X(p2))U(1))))
+(((p1)*(p2))U(p2))*((X(p2))+((X(X(p1)))R(X(p1))))
+((1)+((((p0)U(p0))R(1))U(((1)*(p2))U(p2))))+(1)
+((p1)U(((X(p0))R(1))U(X(1))))+((p2)+((p1)U(p2)))
+((p1)R(1))+(((p0)U((p0)R(0)))*((p0)U(X(X(p0)))))
+(((p2)U(p2))*(X(p0)))*((p0)*((X(X(p1)))+(X(p1))))
+X(((p1)*((((X(p2))U(p2))+(p0))R(X(p0))))R(X(p0)))
+((p0)U(((1)R(p2))R((X(p0))*(X(1)))))U((1)U(p0))
+(X(p1))U((X((p1)*(((0)*(1))*(p2))))U((p2)+(p1)))
+(((p1)R(p0))U(p0))*(((X(p2))U(p0))*((1)+(X(0))))
+((X(p1))*(p2))R((0)+((X(0))*(((p1)+(p2))*(0))))
+(0)U((((X(p0))+(0))U(p2))*(((1)*(X(p0)))U(0)))
+(X(((p0)*(0))U(p1)))+(((p2)+((1)R(p2)))*(X(p0)))
+((X((p0)+(((p0)+(p2))+(X(p0)))))+(X(p1)))U(X(p0))
+X(((((X(p1))R(X(p2)))U(p1))+(X(p0)))R((p1)+(1)))
+((p2)R(((X(0))R(p2))U((X(p1))R(X(0)))))*(X(0))
+((p2)R(((1)R(p1))*(p0)))R(((p1)U(p2))R(X(X(1))))
+((X(1))U(((p0)+(X(p0)))+(X(p1))))U((X(p0))U(p0))
+((0)+(p2))R(X(((0)U(p1))+(X((p1)*((p2)R(1))))))
+X((X((X(X(p0)))R(p0)))*((X(p1))+((X(0))*(0))))
+(((p0)*(X(p2)))U(p2))U(((X(p1))*(X(p0)))R(X(1)))
+(X(0))*((((p1)R((p0)U(1)))R(p2))R((p1)*(X(p1))))
+(X(X((p2)+((p1)U(X(p0))))))R((X(1))U((0)R(p0)))
+((p1)U(p1))U((p1)*((((p2)U(X(p1)))R(1))U(X(p0))))
+X(((X((p2)U(X(0))))R(((p1)U(0))*(X(p0))))*(p0))
+((((X(p1))R(p1))U(X(p1)))+((p1)R(p0)))U((p1)U(p1))
+(p2)*(((X(0))*(0))+(((1)R(X(p2)))U((p2)R(1))))
+(((0)+(X(p1)))U(X(p1)))+((X((1)R(1)))R(X(p2)))
+((((p2)U(X(1)))*((p2)R(p0)))U(X(p2)))*((p2)R(p2))
+(X(X((p1)U((p2)*(p1)))))R((p0)*(((p0)U(p1))R(p1)))
+X(((X(0))U(1))U(((X((X(p1))+(p0)))R(p2))*(p1)))
+((X(X(p2)))U(p1))R(((X(1))+(X(p1)))R((p2)*(p0)))
+(X(((p0)U(1))U(X(0))))*(((p0)U((p2)R(p1)))*(p1))
+((X(p2))*((p0)U(0)))R((X(p1))+(X(X(X(X(1))))))
+((X(p0))R(p1))U(X(((X(p0))U((p1)*(X(p1))))*(p2)))
+(X((((p0)R(X(p2)))*(p0))R((X(1))R(p0))))U(X(0))
+((X(((p2)+(p1))U(p1)))+((X(p0))R(X(p2))))R(X(p1))
+(((p1)U(1))+(p2))*(X(((X(1))U(p0))R((p1)R(0))))
+(X(X(p1)))U(X((X((X((p0)R(X(p2))))U(p1)))U(p0)))
+(((p2)U(X(p1)))*(X(X(p0))))R((p1)R((p1)U(X(p0))))
+(X((X((X(1))+((X(p1))+(X(1)))))R(X(p1))))+(p0)
+((p0)U((p2)*((p2)*(p1))))R(((X(p2))+(p0))U(X(p2)))
+(X((p2)*(((p0)R((0)R(p0)))U(X(X(p2))))))U(X(p2))
+(((p2)R(p2))U(X(X(((X(p1))U(X(1)))*(p0)))))R(1)
+((((p2)*(0))*(p1))U((1)R(1)))U((X(1))U(X(0)))
+((p2)R(p0))R((((p0)+(X(p1)))+((p1)+(p0)))U(X(0)))
+(0)+((((p2)R(X(p2)))R(p1))R(X(((p2)U(1))R(0))))
+(X(X(p1)))*(X(((0)U(X(0)))*((X(X(p2)))U(0))))
+(X(((0)*(p0))R((p0)U(X(p1)))))U((0)*((p2)*(0)))
+X((((p0)R(p0))R((X(p0))U((p2)+(X(p1)))))+(X(p1)))
+((X(0))*((X(p0))R(p0)))*(((p0)+(p0))*(X(X(0))))
+(X(p1))U((X(p1))+((((p0)U(X(1)))*(p1))*(X(p2))))
+((X(p0))*((p1)R((p2)+(p0))))*(X((X(1))U(X(p1))))
+((((X(1))+(p2))+(X(p0)))U(p1))U(((p1)*(1))R(p2))
+((p0)+((p2)U(0)))*((X(p1))U(X(((p1)*(1))+(p2))))
+((p2)+((p2)U(p0)))R(X((((1)R(p0))*(1))+(X(p2))))
+((p2)R(X(p2)))R(X((X(p2))*(((0)+(0))+(X(0)))))
+(X(1))*((((p2)*(p2))R((p1)U(p1)))U((p1)*(X(1))))
+(X(p2))*(((((X(p1))U(p1))R(X(p0)))R(X(1)))R(p0))
+((((X(p0))*((X(p1))R(p0)))R(p2))R(X(p0)))U(X(p1))
+((p2)*(1))R(X((X(X(X(p1))))*(((p2)U(0))R(0))))
+((((1)U(((p1)*(p1))R(p1)))+(X(p2)))U(p1))R(X(p2))
+X((((X(p1))R(p0))U(p0))+(X(X(((0)+(p1))*(p1)))))
+((X((X(X(p1)))R((0)+(p2))))R(0))R((p0)R(X(p1)))
+((X(p1))+(X((X(p0))*(X(p2)))))R(((p0)+(1))U(p1))
+((X((0)*((p0)+(p2))))U((p1)R((p0)*(p0))))U(X(p0))
+(((p1)R(X(p2)))R((0)+((1)U(1))))U((X(1))R(p2))
+(X(p2))U(((p2)U(((X(p1))R(p2))R(X(X(1)))))*(0))
+(((X(p2))R(p2))U((X(0))U(X(p1))))*(X((1)*(0)))
+(((p1)R(p1))U(p2))R((X(p0))R(((1)R(X(p0)))U(p2)))
+(X((0)R((((p2)+(p1))U(p2))U((p1)R(p2)))))U(X(0))
+X((X(1))*((p2)*(X(X(((p1)R((p1)+(0)))U(p1))))))
+(((p2)R(1))*(X(p0)))U((p0)U((X((p1)R(p0)))U(1)))
+(((X(p0))+(((p1)+(p2))*(1)))R((p1)R(X(p1))))+(p0)
+((p2)U((p0)R(p2)))+(((p0)+(p0))U((p0)*(X(X(p2)))))
+(X(p1))+((((p2)R(p0))*((X(p1))R(X(p0))))*(X(0)))
+X((X(p0))*((X(((p0)+(X(X(p0))))R(X(1))))*(p2)))
+((p0)+(((p1)*((X(p1))U(p0)))+((p0)R(X(0)))))*(0)
+((1)R(X((p0)U(p0))))+(((p0)R(X(p2)))+((p0)R(p1)))
+X((((p0)R((p1)R((p2)R(X(0)))))R(p2))+((p0)U(1)))
+(p0)R((X(p0))U(((X(p0))*(p2))R(X((p0)*(X(1))))))
+(((p1)R(p1))R(X(p2)))*(((X(X(p1)))+(X(p2)))R(p1))
+((p0)R((X(0))*(p2)))R((X(p2))+(((p1)U(p1))R(p2)))
+(X((X(((X(p0))R(p0))+(X((p2)R(p1)))))R(p1)))R(p0)
+(p0)U(X((((p1)U(0))R(X(p1)))U(X((p0)*(X(1))))))
+((p2)R((p2)U((p0)R(p1))))R(((X(p1))U(p0))*(X(p0)))
+(((X(p1))R(p2))+(((1)U(p1))R(X((1)R(p0)))))R(p0)
+(p2)U((X(X(((p2)U(0))U(X(p2)))))U((X(p2))U(p1)))
+((((p0)R(p2))U(X(p0)))U(X(p1)))U((p0)U((p0)R(p1)))
+((X(p0))*(((X(p0))*((p0)*(p0)))+(p1)))U((p2)*(1))
+X(X(((X(p1))R(X(0)))U((X(p1))U(X((0)U(p1))))))
+((X(0))*((p2)R(X(p2))))U((p0)*(X(X((p0)U(p1)))))
+((p2)R(((p1)R(p0))U(p0)))R((X(p2))U((p1)*(X(p2))))
+X((p2)U(((X(X(0)))+(X(0)))R(((p1)R(p1))+(1))))
+(((X(p0))U(1))U(X(p2)))R((X(p2))R((X(p1))U(1)))
+(X((X(p0))*(X(p0))))+(((X(X(1)))R(0))R(X(1)))
+((((X(X(p2)))R(1))*(X(p2)))*((X(p1))R(p0)))*(p1)
+(X(p1))U(X(((X(p2))+((0)U((p1)R(0))))R(X(p2))))
+X((X(X(((p0)+(p1))R((1)+((p1)U(0))))))*(X(p1)))
+(((p2)R((p1)+(1)))*((1)*(p1)))*(X(X((p0)R(1))))
+X((((X(p0))U(p2))*(X(p0)))U(X((p0)+((0)U(1)))))
+((X(p2))U(X((0)U(p0))))U(((0)*(0))U((p0)U(p0)))
+(p1)R(X(((p1)U(X((p1)*(1))))R((X(p2))+(X(p2)))))
+((p1)U(X((X(p1))*((p0)U(p2)))))R((p0)+((p2)U(p0)))
+(((p1)R(X(0)))*(X((1)*(p1))))U((p0)R((0)R(p1)))
+X(((((p0)R(X(p0)))*(X(0)))U(p1))*((0)*(X(p2))))
+((p1)U(p0))*((((p2)*(p0))R(1))*((p2)+((p2)+(p0))))
+(((X(1))+(X(p1)))R((X(0))R((0)U(0))))*(X(p2))
+X(X(((X(p2))U(p2))+((X(X(p1)))R((X(0))*(p0)))))
+X(X(((X(p2))U((X(1))U(p2)))R(((p1)*(1))*(1))))
+(p0)U((((p1)+(0))*(((p0)R(p2))U(p0)))R((p2)U(p1)))
+(((X(p2))+(X(X(X(1)))))R(X(p1)))U(X((p2)*(p1)))
+X((X((0)U(((X(p0))+(0))*((X(p0))U(1)))))U(0))
+X((X((X(p2))+(X(X(0)))))+(((p2)*(p0))R(X(0))))
+(X((p2)R(0)))R((X((X(p1))*((p1)+(p0))))+(X(p0)))
+((((p2)R(0))U(X(p1)))*(X(1)))R((p1)+((p2)U(p1)))
+####
+
+####
+((p0)U(p1))U(p0)
+((X(p1))R(p1))U(!p0)
+((!p0)+(X(X(p1))))U(X(!p0))
+(X((p1)+((p1)U(X(!p0)))))R(X(p0))
+(X(X(!p0)))*((p0)+(((X(X(p1)))U(X(p1)))R(X(p1))))
+X(((X(p0))R(p0))R((!p1)*((X(!p0))U((p0)U(X(!p1))))))
+((X(!p1))*(X(p0)))*(((X(!p1))U(!p0))*((X(p1))U(!p0)))
+(!p0)U(((((p0)R(!p0))U(X(!p0)))+(!p0))R(X((!p0)+(p0))))
+X(((((p2)U(p3))R(X((p10)R(!p4))))+(p14))R((!p1)*(!p12)))
+X((((((w)*(!x))*(!y))+(((w)*(x))*(!z)))+(((x)*(!y))*(z)))+(((!x)*(y))*(!z)))
+((X(q))R(!p))U((((q)R(p))+(!q))U(X(!p)))
+(((p)R(q))+(!p))U(X(!q))
+((!p)U(!q))U((X(!p))+(!q))
+X((X(((p2)R(p1))+(X(0))))U(!p1))
+((p0)R((!p2)R(!p0)))U((p2)U(X(p0)))
+(!p2)R(X((((!p4)U(!p0))R(!p3))U((!p4)R(!p3))))
+((X(!p2))*(!p3))R(X((((!p4)U(!p0))R(!p3))U((!p4)R(!p3))))
+((X(!q))*(!r))R(X((((!s)U(!p))R(!r))U((!s)R(!r))))
+(X(p0))R((((!p0)U(p1))*(X(!p0)))R(X((p1)R(X(!p1)))))
+(X(p0))R((((!p0)U(p1))*(X(!p0)))R(X(((p1)*(X(!p1)))+(G(!p1)))))
+(p)R((p)+(q))
+((X(r))U(s))+(!(X((r)U((r)*(s)))))
+(G((p)->(F(q))))*(((X(r))U(s))+(!(X((r)U((r)*(s))))))
+(G((p)->(F(q))))*(((X(r))U(s))+(X((r)U((r)*(s)))))
+(F(p))U(G(q))
+((X(r))U(X(s)))^(X((r)U(s)))
+(!p2)*((p2)*(X(p1)))
+X((p0)R((p0)U(p0)))
+X((X(!p2))R((p0)U(X(!p3))))
+####
+
+####
+(p)U(q)
+(p)U((q)U(r))
+!((p)U((q)U(r)))
+(G(F(p)))->(G(F(q)))
+(F(p))U(G(q))
+(G(p))U(q)
+!((F(F(p)))<->(F(p)))
+!((G(F(p)))->(G(F(q))))
+(G(F(p)))^(G(F(q)))
+(p)R((p)+(q))
+((X(p))U(X(q)))+(!(X((p)U(q))))
+((X(p))U(q))+(!(X((p)U((p)*(q)))))
+(G((p)->(F(q))))*(((X(p))U(q))+(!(X((p)U((p)*(q))))))
+(G((p)->(F(q))))*(((X(p))U(X(q)))+(!(X((p)U(q)))))
+G((p)->(F(q)))
+!(G((p)->(X((q)R(r)))))
+!((G(F(p)))+(F(G(q))))
+G((F(p))*(F(q)))
+(F(p))*(F(!p))
+((X(!q))*(!r))R(X((((!s)U(!p))R(!r))U((!s)R(!r))))
+(((G((q)+(G(F(p)))))*(G((r)+(G(F(!p))))))+(G(q)))+(G(r))
+(((G((q)+(F(G(p)))))*(G((r)+(F(G(!p))))))+(G(q)))+(G(r))
+!((((G((q)+(G(F(p)))))*(G((r)+(G(F(!p))))))+(G(q)))+(G(r)))
+!((((G((q)+(F(G(p)))))*(G((r)+(F(G(!p))))))+(G(q)))+(G(r)))
+(G((q)+(X(G(p)))))*(G((r)+(X(G(!p)))))
+G((p)+((X(q))*(X(!q))))
+((p)U(q))+((q)U(p))
diff --git a/src/ltltest/inf.cc b/src/ltltest/inf.cc
new file mode 100644
index 000000000..77ab7496e
--- /dev/null
+++ b/src/ltltest/inf.cc
@@ -0,0 +1,97 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <iostream>
+#include <cassert>
+#include "ltlparse/public.hh"
+#include "ltlvisit/lunabbrev.hh"
+#include "ltlvisit/tunabbrev.hh"
+#include "ltlvisit/dump.hh"
+#include "ltlvisit/nenoform.hh"
+#include "ltlvisit/destroy.hh"
+#include "ltlvisit/tostring.hh"
+#include "ltlvisit/reducform.hh"
+#include "ltlast/allnodes.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " formula1 formula2?" << std::endl;
+  exit(2);
+}
+
+int
+main(int argc, char** argv)
+{
+  if (argc < 3)
+    syntax(argv[0]);
+
+
+  spot::ltl::parse_error_list p1;
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  spot::ltl::formula* f2 = NULL;
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
+    return 2;
+
+  spot::ltl::parse_error_list p2;
+  f2 = spot::ltl::parse(argv[2], p2);
+  
+  if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
+    return 2;
+  
+  std::string f1s = spot::ltl::to_string(f1);
+  std::string f2s = spot::ltl::to_string(f2);
+
+  int exit_return = 0;
+  
+  std::cout << "Test f1 < f2" << std::endl;
+  if (spot::ltl::inf_form(f1,f2)) {
+    std::cout << f1s << " < " << f2s << std::endl;
+    exit_return = 1;
+  }
+  
+  /*  
+  std::cout << "Test !f1 < f2" << std::endl;
+  if (spot::ltl::infneg_form(f1,f2,0)) {
+    std::cout << "!(" << f1s << ") < " << f2s << std::endl;
+    exit_return = 2;
+  }
+  
+  std::cout << "Test f1 < !f2" << std::endl;
+  if (spot::ltl::infneg_form(f1,f2,1)) {
+    std::cout << f1s << " < !(" << f2s << ")" << std::endl;
+    exit_return = 3;
+  }
+  */
+
+  spot::ltl::dump(std::cout, f1); std::cout << std::endl;
+  spot::ltl::dump(std::cout, f2); std::cout << std::endl;
+
+  spot::ltl::destroy(f1);
+  spot::ltl::destroy(f2);
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+
+  return exit_return;
+}
diff --git a/src/ltltest/inf.test b/src/ltltest/inf.test
new file mode 100755
index 000000000..852ebd151
--- /dev/null
+++ b/src/ltltest/inf.test
@@ -0,0 +1,74 @@
+#! /bin/sh
+# Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+# Check for the reduc visitor
+
+. ./defs || exit 1
+
+#
+
+run 1 ./inf '1' '1'
+run 1 ./inf '0' '0'
+
+run 1 ./inf 'a' '1'
+run 1 ./inf 'a' 'a'
+
+run 1 ./inf 'a' 'a * 1'
+
+run 1 ./inf 'a * b' 'b'
+run 1 ./inf 'a * b' 'a'
+
+run 1 ./inf 'a' 'a + b'
+run 1 ./inf 'b' 'a + b'
+
+run 1 ./inf 'a + b' '1'
+
+run 1 ./inf 'a' 'b U a'
+run 1 ./inf 'a' 'b U 1'
+run 1 ./inf 'a U b' '1'
+
+run 1 ./inf 'a' '1 R a'
+run 1 ./inf 'a' 'a R 1'
+run 1 ./inf 'a R b' 'b'
+run 1 ./inf 'a R b' '1'
+
+run 1 ./inf 'a U b' '1 U b'
+run 1 ./inf 'a R b' '1 R b' 
+
+run 1 ./inf 'b * (a U b)' 'a U b'
+run 1 ./inf 'a U b' 'c + (a U b)'
+
+exit 0
+#
+
+#run 1 ./inf '(a U b) U ((a U b) U (a U b))' 'a U b'
+#run 1 ./inf '(a U b) && (a U b)' 'a U b'
+
+'X1' '1'
+'a U 0' '0'
+'a R 1' '1'
+'Xa * Xb' 'X(a * b)'
+'F(a * GFb)' 'Fa * GFb'
+'G(a + GFb)' 'Ga + GFb'
+'X(a * GFb)' 'Xa * GFb'
+'X(a + GFb)' 'Xa + GFb'
diff --git a/src/ltltest/reduc.cc b/src/ltltest/reduc.cc
new file mode 100644
index 000000000..533de2846
--- /dev/null
+++ b/src/ltltest/reduc.cc
@@ -0,0 +1,150 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include <iostream>
+#include <cassert>
+#include "ltlparse/public.hh"
+#include "ltlvisit/lunabbrev.hh"
+#include "ltlvisit/tunabbrev.hh"
+#include "ltlvisit/dump.hh"
+#include "ltlvisit/nenoform.hh"
+#include "ltlvisit/destroy.hh"
+#include "ltlvisit/tostring.hh"
+#include "ltlvisit/reducform.hh"
+#include "ltlast/allnodes.hh"
+
+void
+syntax(char* prog)
+{
+  std::cerr << prog << " formula1 (formula2)?" << std::endl;
+  exit(2);
+}
+
+typedef spot::ltl::formula*  ptrfunct(const spot::ltl::formula*);
+
+int
+main(int argc, char** argv)
+{
+  if (argc < 2)
+    syntax(argv[0]);
+  
+  spot::ltl::parse_error_list p1;
+  spot::ltl::formula* f1 = spot::ltl::parse(argv[1], p1);
+  spot::ltl::formula* f2 = NULL;
+
+  if (spot::ltl::format_parse_errors(std::cerr, argv[1], p1))
+    return 2;
+
+  
+  if (argc == 3){
+    spot::ltl::parse_error_list p2;
+    f2 = spot::ltl::parse(argv[2], p2);
+    if (spot::ltl::format_parse_errors(std::cerr, argv[2], p2))
+      return 2;
+  }
+  
+  int exit_code = 0;
+  
+  spot::ltl::formula* ftmp1;
+  spot::ltl::formula* ftmp2;
+  
+  ftmp1 = f1;
+  f1 = unabbreviate_logic(f1);
+  ftmp2 = f1;
+  f1 = negative_normal_form(f1);
+  spot::ltl::destroy(ftmp1);
+  spot::ltl::destroy(ftmp2);
+  
+  
+  int length_f1_before = spot::ltl::form_length(f1);
+  std::string f1s_before = spot::ltl::to_string(f1);
+  
+  ftmp1 = f1;
+  f1 = spot::ltl::reduce(f1);
+  ftmp2 = f1;
+  f1 = spot::ltl::unabbreviate_logic(f1);
+  spot::ltl::destroy(ftmp1);
+  spot::ltl::destroy(ftmp2);
+  
+  int length_f1_after = spot::ltl::form_length(f1);
+  std::string f1s_after = spot::ltl::to_string(f1);
+
+  bool red = (length_f1_after < length_f1_before);
+  if (red);
+  std::string f2s = "";
+  if (f2 != NULL) {
+    ftmp1 = f2;
+    f2 = unabbreviate_logic(f2);
+    ftmp2 = f2;
+    f2 = negative_normal_form(f2);
+    spot::ltl::destroy(ftmp1);
+    spot::ltl::destroy(ftmp2);
+    ftmp1 = f2;
+    f2 = unabbreviate_logic(f2);
+    spot::ltl::destroy(ftmp1);
+    f2s = spot::ltl::to_string(f2);
+  }
+  
+  
+  if (red && (f2 == NULL)) {
+    std::cout << length_f1_before << " " << length_f1_after 
+	      << " '" << f1s_before << "' reduce to '" << f1s_after << "'" << std::endl;
+  }
+    
+  if (f2 != NULL){
+    if (f1 != f2) {
+      if (length_f1_after < length_f1_before)
+	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " KOREDUC " << std::endl;
+      else
+	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " KOIDEM " << std::endl;
+      exit_code = 1;
+    }
+    else {
+      if (f1s_before != f1s_after)
+	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " OKREDUC " << std::endl;
+      else
+	std::cout << f1s_before << " ** " << f2s << " ** " << f1s_after << " OKIDEM" << std::endl;
+      exit_code = 0;
+    }
+  }
+  else{  
+    if (length_f1_after < length_f1_before) exit_code = 0;
+  }
+  
+  /*
+  spot::ltl::dump(std::cout, f1); std::cout << std::endl;
+  if (f2 != NULL)
+    spot::ltl::dump(std::cout, f2); std::cout << std::endl;
+  */
+  
+  
+  spot::ltl::destroy(f1);
+  if (f2 != NULL)
+    spot::ltl::destroy(f2);
+  
+
+  assert(spot::ltl::atomic_prop::instance_count() == 0);
+  assert(spot::ltl::unop::instance_count() == 0);
+  assert(spot::ltl::binop::instance_count() == 0);
+  assert(spot::ltl::multop::instance_count() == 0);
+  
+  return exit_code;
+}
diff --git a/src/ltltest/reduc.test b/src/ltltest/reduc.test
new file mode 100755
index 000000000..41a0ba897
--- /dev/null
+++ b/src/ltltest/reduc.test
@@ -0,0 +1,134 @@
+#! /bin/sh
+# Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+# département Systèmes Répartis Coopératifs (SRC), Université Pierre
+# et Marie Curie.
+#
+# This file is part of Spot, a model checking library.
+#
+# Spot is free software; you can redistribute it and/or modify it
+# under the terms of the GNU General Public License as published by
+# the Free Software Foundation; either version 2 of the License, or
+# (at your option) any later version.
+#
+# Spot is distributed in the hope that it will be useful, but WITHOUT
+# ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+# or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+# License for more details.
+#
+# You should have received a copy of the GNU General Public License
+# along with Spot; see the file COPYING.  If not, write to the Free
+# Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+# 02111-1307, USA.
+
+
+# Check for the reduc visitor
+
+#. ./defs || exit 1
+if [ $1 ]; then
+    FICH=$1
+else 
+    FICH="formules.ltl"
+fi
+
+#####################################
+rm output? result_bri.test -f
+for opt in bri ##b r i br bi rb ri ib ir bri bir rbi rib ibr irb 
+  do
+  for f in `awk '{print $1}' $FICH`
+    do
+    if [ ! $f = "####" ]; then
+	#echo $f;
+	if ./reduc "$f" >> result_$opt.test; 
+	    then
+	    #echo $f >> output1
+	#    if  ../tgbatest/ltl2tgba -f "$f" >> output1; then #automate FM
+	#	echo "" >> output1
+	#    else 
+	#	echo $f;
+	#    fi
+	  #echo "'$f' is reduce ($NB)"
+	    (( NB += 1 ));
+	else
+	    (( NB = NB ));
+	    #echo "reduc failed to reduce '$f'";
+	fi
+    fi
+  done
+  #echo "$NB formula reduce"
+  (( NB = 0 ));
+done
+#####################################
+
+#ftmp=""
+#for f in `sed -e "s/\(.* reduce to \)/'1'/" result_bri.test`
+#  do
+#  if [ $ftmp = "" ]; then
+#      echo $ftmp;
+#      ftmp="";
+#  else
+#      echo $f;
+#      ftmp="$ftmp $f";
+#      echo $ftmp;
+#  fi
+#  echo $f >> output2
+#  ../tgbatest/ltl2tgba -f "$f" >> output2 #automate FM
+#  echo "" >> output2
+#done
+
+##############################################
+#exit 0
+##############################################
+
+SUM1=0
+SUM2=0
+AVG=0
+for res in `awk '{print $1}' result_bri.test`
+do
+  SUM1=$(expr $res + $SUM1)
+done
+#echo $SUM1
+
+for res in `awk '{print $2}' result_bri.test`
+do
+  SUM2=$(expr $res + $SUM2)
+done
+(( SUM2 *= 100 ))
+#echo $SUM2
+
+if [ ! $SUM1 = 0 ]; then
+    AVG=$(expr $SUM2 / $SUM1)
+fi
+
+#AVG=$(expr $AVG / $NB)
+#AVG=$(expr $AVG)
+#echo "average reduce $AVG %"
+
+exit 0;
+
+### Formule qui ne passe pas !! => Segmentation fault !!
+#'(((p2)R((X(p2))U(X(1))))*(p0))*((p1)R((p2)R(p0)))'
+#'(((p2)R((X(p2))U(X(1))))*(p0))'
+#'((p1)R((p2)R(p0)))'
+
+#'(p0 R (Gp0 U (p0 U Xp1)))'
+
+
+#'(((!p)*(X(X(p))))*((p)R((q)+(!q))))+((!q)U(q))'
+#'X(((p1)R(1))*((0)R((p0)+(p1))))'
+#'((p0)U(0))U(((0)R(0))*(X(p2)))'
+#'(((X(1))R(1))U((0)R(1)))R(p0)'
+#'((X(p0))R(X(p2)))+((0)R((((p2)+(0))*(p0))R(0)))'
+#'((X(0))+((0)R(p2)))U(((p0)R((p2)*(p2)))R(X(p2)))'
+#'(p1)R(((p2)R(1))R(((p1)U((1)U(p0)))R((p2)U(0))))'
+#'(((X(p0))R(X(p0)))R((p0)R(1)))*((0)R((p1)R(0)))'
+#'(((p1)R(X(p2)))R((0)+((1)U(1))))U((X(1))R(p2))'
+
+(((!p)*(X(X(p))))*((p)R((q)+(!q))))+((!q)U(q))
+X(((p1)R(1))*((0)R((p0)+(p1))))
+((p0)U(0))U(((0)R(0))*(X(p2)))
+(((X(1))R(1))U((0)R(1)))R(p0)
+((X(p0))R(X(p2)))+((0)R((((p2)+(0))*(p0))R(0)))
+((X(0))+((0)R(p2)))U(((p0)R((p2)*(p2)))R(X(p2)))
+(p1)R(((p2)R(1))R(((p1)U((1)U(p0)))R((p2)U(0))))
+(((X(p0))R(X(p0)))R((p0)R(1)))*((0)R((p1)R(0)))
+(((p1)R(X(p2)))R((0)+((1)U(1))))U((X(1))R(p2))
\ No newline at end of file
diff --git a/src/ltlvisit/Makefile.am b/src/ltlvisit/Makefile.am
index b06cf1990..c6f61a505 100644
--- a/src/ltlvisit/Makefile.am
+++ b/src/ltlvisit/Makefile.am
@@ -33,7 +33,8 @@ ltlvisit_HEADERS = \
   lunabbrev.hh \
   nenoform.hh \
   postfix.hh \
-  tunabbrev.hh
+  tunabbrev.hh \
+  reducform.hh
 
 noinst_LTLIBRARIES = libltlvisit.la
 libltlvisit_la_SOURCES = \
@@ -45,4 +46,8 @@ libltlvisit_la_SOURCES = \
   lunabbrev.cc \
   nenoform.cc \
   postfix.cc \
-  tunabbrev.cc
+  tunabbrev.cc \
+  reducform.cc \
+  basereduc.cc \
+  forminf.cc \
+  formlength.cc
\ No newline at end of file
diff --git a/src/ltlvisit/basereduc.cc b/src/ltlvisit/basereduc.cc
new file mode 100644
index 000000000..e7660fd9f
--- /dev/null
+++ b/src/ltlvisit/basereduc.cc
@@ -0,0 +1,578 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "reducform.hh"
+#include "ltlast/allnodes.hh"
+#include "ltlvisit/clone.hh"
+#include <cassert>
+
+#include "ltlvisit/destroy.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    class basic_reduce_form_visitor : public visitor
+    {
+    public:
+      
+      basic_reduce_form_visitor(){}
+      
+      virtual ~basic_reduce_form_visitor(){}
+
+      formula*
+      result() const
+      {
+	return result_;
+      }
+    
+      void
+      visit(atomic_prop* ap)
+      {
+	formula* f = ap->ref();
+	result_ = f;
+      }
+      
+      void
+      visit(constant* c)
+      {
+	switch (c->val())
+	  {
+	  case constant::True:
+	    result_ = constant::true_instance();
+	    return;
+	  case constant::False:
+	    result_ = constant::false_instance();
+	    return;
+	  }
+      }
+      
+      void
+      visit(unop* uo)
+      {
+	formula* f = uo->child();
+	result_ = basic_reduce_form(f);
+	switch (uo->op())
+	  {
+	  case unop::Not:
+	    result_ = unop::instance(unop::Not, result_);
+	    return;
+
+	  case unop::X:
+	    /* X(true) = true 
+	       X(false) = false */
+	    if (node_type(result_) == (node_type_form_visitor::Const))
+	      return;
+	    
+	    /* XGF(f) = GF(f) */
+	    if (is_GF(result_)) return;
+
+	    /* X(f1 & GF(f2)) = X(f1) & GF(F2) */
+	    /* X(f1 | GF(f2)) = X(f1) | GF(F2) */
+	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
+		if (spot::ltl::nb_term_multop(result_) == 2) {
+		  if (is_GF(((multop*)result_)->nth(0)) || 
+		      is_FG(((multop*)result_)->nth(0))) {
+		    multop::vec* res = new multop::vec;
+		    res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1))));
+		    res->push_back(basic_reduce_form(((multop*)result_)->nth(0)));
+		    f = result_;
+		    result_ = multop::instance(((multop*)(result_))->op(), res);
+		    spot::ltl::destroy(f);
+		    return;
+		  }
+		  if (is_GF(((multop*)result_)->nth(1)) || 
+		      is_FG(((multop*)result_)->nth(1))) {
+		    multop::vec* res = new multop::vec;
+		    res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(0))));
+		    res->push_back(basic_reduce_form(((multop*)result_)->nth(1)));
+		    f = result_;
+		    result_ = multop::instance(((multop*)(result_))->op(), res);
+		    spot::ltl::destroy(f);
+		    return;
+		  }
+		}
+	    }
+
+	    result_ = unop::instance(unop::X, result_);
+	    return;
+	    
+	  case unop::F: 
+	    
+	    /* F(true) = true 
+	       F(false) = false */
+	    if (node_type(result_) == (node_type_form_visitor::Const))
+	      return;
+	    
+	    /* FX(a) = XF(a) */
+	    if (node_type(result_) == (node_type_form_visitor::Unop))
+	      if ( ((unop*)(result_))->op() == unop::X ){
+		f = result_;
+		result_ = unop::instance(unop::X,
+					 unop::instance(unop::F,
+							basic_reduce_form(((unop*)(result_))->child()) ));
+		spot::ltl::destroy(f);
+		return;
+	      }
+	    
+	    /* F(f1 & GF(f2)) = F(f1) & GF(F2) */
+	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
+	      if ( ((multop*)(result_))->op() == multop::And ) {
+		if (spot::ltl::nb_term_multop(result_) == 2) {
+		  if (is_GF(((multop*)result_)->nth(0)) || 
+		      is_FG(((multop*)result_)->nth(0))) {
+		    multop::vec* res = new multop::vec;
+		    res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(1))));
+		    res->push_back(basic_reduce_form(((multop*)result_)->nth(0)));
+		    spot::ltl::destroy(result_);
+		    result_ = multop::instance(multop::And, res);
+		    return;
+		  }
+		  if (is_GF(((multop*)result_)->nth(1)) || 
+		      is_FG(((multop*)result_)->nth(1))) {
+		    multop::vec* res = new multop::vec;
+		    res->push_back(unop::instance(unop::F, basic_reduce_form(((multop*)result_)->nth(0))));
+		    res->push_back(basic_reduce_form(((multop*)result_)->nth(1)));
+		    spot::ltl::destroy(result_);
+		    result_ = multop::instance(multop::And, res);
+		    return;
+		  }
+		}
+	      }
+	    }
+
+	    result_ = unop::instance(unop::F, result_);
+	    return;
+
+	  case unop::G:
+	    
+	    /* G(true) = true 
+	       G(false) = false */
+	    if (node_type(result_) == (node_type_form_visitor::Const))
+	      return;
+
+	    /* G(a R b) = G(b) */
+	    if (node_type(result_) == node_type_form_visitor::Binop)
+	      if ( ((binop*)(result_))->op() == binop::R ){
+		f = result_;
+		result_ = unop::instance(unop::G, basic_reduce_form(((binop*)(result_))->second()));
+		spot::ltl::destroy(f);
+		return;
+	      }
+	    
+	    /* GX(a) = XG(a) */
+	    if (node_type(result_) == (node_type_form_visitor::Unop))
+	      if ( ((unop*)(result_))->op() == unop::X ){
+		f = result_;
+		result_ = unop::instance(unop::X,
+					 unop::instance(unop::G,
+							basic_reduce_form(((unop*)(result_))->child()) ));
+		spot::ltl::destroy(f);
+		return;
+	      }
+
+	    /* G(f1 | GF(f2)) = G(f1) | GF(F2) */
+	    if (node_type(result_) == (node_type_form_visitor::Multop)) {
+	      if ( ((multop*)(f))->op() == multop::Or ) {
+		if (spot::ltl::nb_term_multop(result_) == 2) {
+		  if (is_GF(((multop*)result_)->nth(0)) || 
+		      is_FG(((multop*)result_)->nth(0))) {
+		    multop::vec* res = new multop::vec;
+		    res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(1))));
+		    res->push_back(basic_reduce_form(((multop*)result_)->nth(0)));
+		    spot::ltl::destroy(result_);
+		    result_ = multop::instance(multop::Or, res);
+		    return;
+		  }
+		  if (is_GF(((multop*)result_)->nth(1)) || 
+		      is_FG(((multop*)result_)->nth(1))) {
+		    multop::vec* res = new multop::vec;
+		    res->push_back(unop::instance(unop::G, basic_reduce_form(((multop*)result_)->nth(0))));
+		    res->push_back(basic_reduce_form(((multop*)result_)->nth(1)));
+		    spot::ltl::destroy(result_);
+		    result_ = multop::instance(multop::Or, res);
+		    return;
+		  }
+		}
+	      }
+	    }
+
+	    result_ = unop::instance(unop::G, result_);
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(binop* bo)
+      {
+	formula* f1 = bo->first();
+	formula* f2 = bo->second();
+	formula* ftmp = NULL;
+	node_type_form_visitor v1;
+	node_type_form_visitor v2;
+	switch (bo->op())
+	  {
+	  case binop::Xor:
+	    result_ = binop::instance(binop::Xor, 
+				      basic_reduce_form(f1), 
+				      basic_reduce_form(f2));
+	    return;
+	  case binop::Equiv:
+	    result_ = binop::instance(binop::Equiv, 
+				      basic_reduce_form(f1), 
+				      basic_reduce_form(f2));
+	    return;
+	  case binop::Implies:
+	    result_ = binop::instance(binop::Implies, 
+				      basic_reduce_form(f1), 
+				      basic_reduce_form(f2));
+	    return;
+	  case binop::U:
+	    f2 = basic_reduce_form(f2);
+	    
+	    /* a U false = false 
+	       a U true = true */
+	    if (node_type(f2) == (node_type_form_visitor::Const)) {
+	      result_ = f2;
+	      return;
+	    }
+
+	    f1 = basic_reduce_form(f1);
+
+	    /* X(a) U X(b) = X(a U b) */
+	    if ( node_type(f1) == (node_type_form_visitor::Unop)
+		 && node_type(f2) == (node_type_form_visitor::Unop)) {
+	      if ( (((unop*)(f1))->op() == unop::X) 
+		   && (((unop*)(f2))->op() == unop::X) ) {
+		ftmp = binop::instance(binop::U,
+				       basic_reduce_form(((unop*)(f1))->child()),
+				       basic_reduce_form(((unop*)(f2))->child()));
+		result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
+		spot::ltl::destroy(f1);
+		spot::ltl::destroy(f2);
+		spot::ltl::destroy(ftmp);
+		return;
+	      }
+	    }
+	    result_ = binop::instance(binop::U, f1, f2);
+	    return;
+
+	  case binop::R: 
+	    f2 = basic_reduce_form(f2);
+
+	    /* a R false = false 
+	       a R true = true */
+	    if (node_type(f2) == (node_type_form_visitor::Const)) {
+	      result_ = f2;
+	      return;
+	    }
+
+	    f1 = basic_reduce_form(f1);
+	    
+	    /* X(a) R X(b) = X(a R b) */
+	    if ( node_type(f1) == (node_type_form_visitor::Unop)
+		 && node_type(f2) == (node_type_form_visitor::Unop)) {
+	      if ( (((unop*)(f1))->op() == unop::X) 
+		   && (((unop*)(f2))->op() == unop::X) ) {
+		ftmp = binop::instance(bo->op(),
+				       basic_reduce_form(((unop*)(f1))->child()),
+				       basic_reduce_form(((unop*)(f2))->child()));
+		result_ = unop::instance(unop::X, basic_reduce_form(ftmp));
+		spot::ltl::destroy(f1);
+		spot::ltl::destroy(f2);
+		spot::ltl::destroy(ftmp);
+		return;
+	      }
+	    }
+	    result_ = binop::instance(bo->op(),
+				      f1, f2);
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(multop* mo)
+      {
+	if (mo == NULL);
+	multop::type op = mo->op();
+	unsigned mos = mo->size();
+	multop::vec* res = new multop::vec;
+
+	multop::vec* tmpX = new multop::vec;
+	multop::vec* tmpU = new multop::vec;
+	multop::vec* tmpUright = NULL;
+	multop::vec* tmpR = new multop::vec;
+	multop::vec* tmpRright = NULL;
+	multop::vec* tmpFG = new multop::vec;
+	multop::vec* tmpGF = new multop::vec;
+
+	multop::vec* tmpOther = new multop::vec;
+
+	formula* ftmp = NULL;	
+	
+	for (unsigned i = 0; i < mos; ++i)
+	  res->push_back(basic_reduce_form(mo->nth(i)));
+
+	
+	switch (op)
+	  {
+	  case multop::And:
+
+	    for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
+	      if (*i == NULL) continue;
+	      switch (node_type(*i)) {
+
+	      case node_type_form_visitor::Unop: 
+
+		/* Xa & Xb = X(a & b)*/
+		if (((unop*)(*i))->op() == unop::X) {
+		  tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) );
+		  break;
+		} 
+
+		/* FG(a) & FG(b) = FG(a & b)*/
+		if (is_FG(*i)) {
+		  tmpFG->push_back( spot::ltl::basic_reduce_form( ((unop*)((unop*)(*i))->child())->child() ) );
+		  break;
+		}
+		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
+		break;
+		/* A GERER !!!!!!!!!!!!!!!!!!!!!!!
+		   case node_type_form_visitor::Const:
+		   tmpX->push_back( spot::ltl::clone((*i)) );
+		   break;
+		*/
+
+	      case node_type_form_visitor::Binop:
+
+		/* (a U b) & (c U b) = (a & c) U b */
+		if (((binop*)(*i))->op() == binop::U) {
+		  ftmp = ((binop*)(*i))->second();
+		  tmpUright = new multop::vec;
+		  for (multop::vec::iterator j = i; j != res->end(); j++) 
+		    {
+		      if (*j == NULL) continue;
+		      if (node_type(*j) == node_type_form_visitor::Binop) 
+			{
+			  if (((binop*)(*j))->op() == binop::U) 
+			    {
+			      if (ftmp == ((binop*)(*j))->second()) 
+				{
+				  tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() ));
+				  if (j != i) {
+				    spot::ltl::destroy(*j);
+				    *j = NULL;
+				  }
+				}
+			    }
+			}
+		    }
+		  tmpU->push_back(binop::instance(binop::U,
+						  multop::instance(multop::And,tmpUright),
+						  basic_reduce_form(ftmp)));
+		  break;
+		}
+		
+		/* (a R b) & (a R c) = a R (b & c) */
+		if (((binop*)(*i))->op() == binop::R) {
+		  ftmp = ((binop*)(*i))->first();
+		  tmpRright = new multop::vec;
+		  for (multop::vec::iterator j = i; j != res->end(); j++) 
+		    {
+		      if (*j == NULL) continue;
+		      if (node_type(*j) == node_type_form_visitor::Binop) 
+			{
+			  if (((binop*)(*j))->op() == binop::R) 
+			    {
+			      if (ftmp == ((binop*)(*j))->first()) 
+				{
+				  tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() ));
+				  if (j != i) {
+				    spot::ltl::destroy(*j);
+				    *j = NULL;
+				  }
+				}
+			    }
+			}
+		    }
+		  tmpR->push_back(binop::instance(binop::R,
+						  basic_reduce_form(ftmp),
+						  multop::instance(multop::And,tmpRright)));
+		  break;
+		}
+		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
+		break;
+	      default: 
+		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
+		break;
+	      }
+	      spot::ltl::destroy(*i);
+	    }
+	    
+	    delete(tmpGF);
+	    tmpGF = NULL;
+
+	    break;
+	    
+	  case multop::Or:
+	    
+	    for (multop::vec::iterator i = res->begin(); i != res->end(); i++) {
+	      if (*i == NULL) continue;
+	      switch (node_type(*i)) {
+		
+	      case node_type_form_visitor::Unop: 
+
+		/* Xa | Xb = X(a | b)*/
+		if (((unop*)(*i))->op() == unop::X) {
+		  tmpX->push_back( spot::ltl::basic_reduce_form(((unop*)(*i))->child()) );
+		  break;
+		}
+
+		/* GF(a) & GF(b) = GF(a & b)*/
+		if (is_GF(*i)) {
+		  tmpGF->push_back( spot::ltl::basic_reduce_form( ((unop*)((unop*)(*i))->child())->child() ) );
+		  break;
+		}
+		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
+		break;
+
+	      case node_type_form_visitor::Binop:
+		
+		/* (a U b) | (a U c) = a U (b | c) */
+		if (((binop*)(*i))->op() == binop::U) {
+		  ftmp = ((binop*)(*i))->first();
+		  tmpUright = new multop::vec;
+		  for (multop::vec::iterator j = i; j != res->end(); j++) 
+		    {
+		      if (*j == NULL) continue;
+		      if (node_type(*j) == node_type_form_visitor::Binop) 
+			{
+			  if (((binop*)(*j))->op() == binop::U) 
+			    {
+			      if (ftmp == ((binop*)(*j))->first()) 
+				{
+				  tmpUright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->second() ));
+				  if (j != i) {
+				    spot::ltl::destroy(*j);
+				    *j = NULL;
+				  }
+				}
+			    }
+			}
+		    }
+		  tmpU->push_back(binop::instance(binop::U,
+						  basic_reduce_form(ftmp),
+						  multop::instance(multop::Or,tmpUright)));
+		  break;
+		}
+		
+		/* (a R b) | (c R b) = (a | c) R b */
+		if (((binop*)(*i))->op() == binop::R) {
+		  ftmp = ((binop*)(*i))->second();
+		  tmpRright = new multop::vec;
+		  for (multop::vec::iterator j = i; j != res->end(); j++) 
+		    {
+		      if (*j == NULL) continue;
+		      if (node_type(*j) == node_type_form_visitor::Binop) 
+			{
+			  if (((binop*)(*j))->op() == binop::R) 
+			    {
+			      if (ftmp == ((binop*)(*j))->second()) 
+				{
+				  tmpRright->push_back(spot::ltl::basic_reduce_form(((binop*)(*j))->first() ));
+				  if (j != i) {
+				    spot::ltl::destroy(*j);
+				    *j = NULL;
+				  }
+				}
+			    }
+			}
+		    }
+		  tmpR->push_back(binop::instance(binop::R,
+						  multop::instance(multop::Or,tmpRright),
+						  basic_reduce_form(ftmp)));
+		  break;
+		}
+		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
+		break;
+	      default: 
+		tmpOther->push_back(spot::ltl::basic_reduce_form(*i));
+		break;
+	      }
+	      spot::ltl::destroy(*i);
+	    }
+	    
+	    delete(tmpFG);
+	    tmpFG = NULL;
+
+	    break;
+	  }
+	
+	
+	res->clear();
+	delete(res);
+	
+	if (tmpX->size())
+	  tmpOther->push_back(unop::instance(unop::X,multop::instance(mo->op(),tmpX)));
+	else delete(tmpX);
+	
+	if (tmpU->size())
+	  tmpOther->push_back(multop::instance(mo->op(),tmpU));
+	else delete(tmpU);
+	
+	if (tmpR->size())
+	  tmpOther->push_back(multop::instance(mo->op(),tmpR));
+	else delete(tmpR);
+	    
+	if (tmpGF != NULL)
+	  if (tmpGF->size())
+	    tmpOther->push_back(unop::instance(unop::G,
+					       unop::instance(unop::F,
+							      multop::instance(mo->op(),tmpGF))));
+	if (tmpFG != NULL)
+	  if (tmpFG->size())
+	    tmpOther->push_back(unop::instance(unop::G,
+					       unop::instance(unop::F,
+							      multop::instance(mo->op(),tmpFG))));
+	
+	result_ = multop::instance(op, tmpOther);
+
+	return;
+
+      }
+      
+    protected:
+      formula* result_;
+    };
+
+    formula* basic_reduce_form(const formula* f)
+    {
+      basic_reduce_form_visitor v;
+      const_cast<formula*>(f)->accept(v);
+      return v.result();
+    }
+
+  }
+}
diff --git a/src/ltlvisit/forminf.cc b/src/ltlvisit/forminf.cc
new file mode 100644
index 000000000..24904d862
--- /dev/null
+++ b/src/ltlvisit/forminf.cc
@@ -0,0 +1,619 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "reducform.hh"
+#include "ltlast/allnodes.hh"
+#include <cassert>
+
+#include "lunabbrev.hh"
+#include "nenoform.hh"
+#include "ltlvisit/destroy.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    bool
+    is_GF(const formula* f)
+    {
+      if ((const unop*)f != NULL)
+	if (((const unop*)f)->op() == unop::G)
+	  if ((const unop*)(((const unop*)f)->child()) != NULL)
+	    if (((const unop*)((const unop*)f)->child())->op() == unop::F)
+	      return true;
+      return false;
+    }
+    
+    bool
+    is_FG(const formula* f)
+    {
+      if ((const unop*)f != NULL)
+	if (((const unop*)f)->op() == unop::F)
+	  if ((const unop*)(((const unop*)f)->child()) != NULL)
+	    if (((const unop*)((const unop*)f)->child())->op() == unop::G)
+	      return true;
+      return false;
+    }
+
+    int
+    nb_term_multop(const formula* f)
+    {
+      if ((const multop*)f == NULL) return -1;
+      
+      unsigned mos = ((const multop*)(f))->size();
+      return mos;
+    }
+
+    
+    node_type_form_visitor::node_type_form_visitor(){}
+    
+    node_type_form_visitor::type
+    node_type_form_visitor::result() const { return result_;}
+    
+    void
+    node_type_form_visitor::visit(const atomic_prop* ap){ 
+      if (ap == NULL);
+      result_ = node_type_form_visitor::Atom;
+    }
+      
+    void
+    node_type_form_visitor::visit(const constant* c){ 
+      if (c == NULL);
+      result_ = node_type_form_visitor::Const;
+    }
+      
+    void
+    node_type_form_visitor::visit(const unop* uo){
+      if (uo == NULL); 
+      result_ = node_type_form_visitor::Unop;
+    }
+      
+    void
+    node_type_form_visitor::visit(const binop* bo){ 
+      if (bo == NULL);
+      result_ = node_type_form_visitor::Binop;
+    }
+      
+    void
+    node_type_form_visitor::visit(const multop* mo){ 
+      if (mo == NULL);
+      result_ = node_type_form_visitor::Multop;
+    }
+      
+    node_type_form_visitor::type node_type(const formula* f)
+    {
+      node_type_form_visitor v;
+      if (f == NULL) std::cout << "f == NULL !!!!!!!!" << std::endl;
+      const_cast<formula*>(f)->accept(v);
+      return v.result();
+    }
+
+    class form_eventual_universal_visitor : public const_visitor
+    {
+    public:
+      
+      form_eventual_universal_visitor()
+      {
+	eventual = false; // faux au départ
+	universal = false;
+      }
+    
+      virtual ~form_eventual_universal_visitor()
+      {
+      }
+
+      bool 
+      is_eventual() const
+      {
+	return eventual;
+      }
+    
+      bool 
+      is_universal() const
+      {
+	return universal;
+      }
+    
+      void
+      visit(const atomic_prop* ap)
+      {
+	if (ap);
+      }
+      
+      void
+      visit(const constant* c)
+      {
+	if (c->val());
+      }
+      
+      void
+      visit(const unop* uo)
+      {
+	const formula* f1 = uo->child();
+	switch (uo->op())
+	  {
+	  case unop::Not:
+	  case unop::X:
+	    eventual = recurse_ev(f1);
+	    universal = recurse_un(f1);
+	    return;
+	  case unop::F: 
+	    eventual = true;
+	    return;
+	  case unop::G:
+	    universal = true;
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(const binop* bo)
+      {
+	const formula* f1 = bo->first();
+	switch (bo->op())
+	  {
+	  case binop::Xor:
+	  case binop::Equiv:
+	  case binop::Implies:
+	    return;
+	  case binop::U:
+	    if (node_type(f1) == node_type_form_visitor::Const)
+	      if (((const constant*)f1)->val() == constant::True)
+		eventual = true;
+	    return;
+	  case binop::R:
+	    if (node_type(f1) != node_type_form_visitor::Const)
+	      if (((const constant*)f1)->val() == constant::False)
+		universal = true;
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(const multop* mo)
+      {
+	if (mo == NULL);
+	unsigned mos = mo->size();
+	
+	eventual = true;
+	universal = true;
+	for (unsigned i = 0; i < mos; ++i){
+	  if ( !(recurse_ev(mo->nth(i))) ){
+	    eventual = false;
+	    break;
+	  }
+	}
+	for (unsigned i = 0; i < mos; ++i){
+	  if ( !(recurse_un(mo->nth(i))) ){
+	    universal = false;
+	    break;
+	  }
+	}
+      }
+      
+      bool
+      recurse_ev(const formula* f)
+      {
+	form_eventual_universal_visitor v;
+	const_cast<formula*>(f)->accept(v);
+	return v.is_eventual();
+      }
+
+      bool
+      recurse_un(const formula* f)
+      {
+	form_eventual_universal_visitor v;
+	const_cast<formula*>(f)->accept(v);
+	return v.is_universal();
+      }
+
+      protected:
+      bool eventual;
+      bool universal;
+    };
+
+    
+    bool is_eventual(const formula* f)
+    {
+      form_eventual_universal_visitor v;
+      const_cast<formula*>(f)->accept(v);
+      return v.is_eventual();
+    }
+
+    bool is_universal(const formula* f)
+    {
+      form_eventual_universal_visitor v;
+      const_cast<formula*>(f)->accept(v);
+      return v.is_universal();
+    }
+    
+    /////////////////////////////////////////////////////////////////////////
+
+    class inf_form_right_recurse_visitor : public const_visitor
+    {
+    public:
+      
+      inf_form_right_recurse_visitor(const formula *f)
+      {
+	this->f = f;
+	result_ = false; // faux au départ
+      }
+    
+      virtual ~inf_form_right_recurse_visitor()
+      {
+      }
+      /*
+      bool special_case(const formula* f2,binop::operator op)
+      {
+	const binop* b = (const binop*)f;
+	const binop* b2 = (const binop*)f2;
+	if ((b != NULL) && (b2 != NULL) &&
+	    (b->op() == b2_>op() == op))
+	  if (inf_form(b2->first(),b->first())
+	      && inf_form(b2->second(),b->second()) )
+	    return true;
+	return false;
+      }
+      */
+      int 
+      result() const
+      {
+	return result_;
+      }
+    
+      void
+      visit(const atomic_prop* ap)
+      {
+	if ((const atomic_prop*)f == ap) 
+	  result_ = true;
+      }
+      
+      void
+      visit(const constant* c)
+      {
+	switch (c->val())
+	  {
+	  case constant::True:
+	    result_ = true;
+	    return;
+	  case constant::False:
+	    result_ = false;
+	    return;
+	  }
+      }
+      
+      void
+      visit(const unop* uo)
+      {
+	const formula* f1 = uo->child();
+	const formula* tmp = NULL;
+	switch (uo->op())
+	  {
+	  case unop::Not:// à gérer !!
+	    return;
+	  case unop::X:// à gérer !!
+	    return;
+	  case unop::F: 
+	    // F(a) = true U a
+	    result_ = inf_form(f,f1);
+	    return;
+	  case unop::G:
+	    // G(a) = false R a
+	    tmp = constant::false_instance();
+	    if ( inf_form(f,tmp) )
+	      result_ = true;
+	    spot::ltl::destroy(tmp);
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(const binop* bo)
+      {
+	const formula* f1 = bo->first();
+	const formula* f2 = bo->second();
+	switch (bo->op())
+	  {
+	  case binop::Xor:
+	  case binop::Equiv:
+	  case binop::Implies:
+	    return;
+	  case binop::U:
+	    if ( (inf_form(f,f2)) )
+	      result_ = true;
+	    return;
+	  case binop::R:
+	    if ( (inf_form(f,f1)) && (inf_form(f,f2)) )
+	      result_ = true;
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(const multop* mo)
+      {
+	if (mo == NULL);
+	multop::type op = mo->op();
+	unsigned mos = mo->size();
+	switch (op)
+	  {
+	  case multop::And:
+	    for (unsigned i = 0; (i < mos) ; ++i)
+	      if ( !(inf_form(f,mo->nth(i))) )
+		return;
+	    result_ = true;
+	    break;
+	  case multop::Or:
+	    for (unsigned i = 0; i < mos && !result_; ++i)
+	      if ( (inf_form(f,mo->nth(i))) )
+		result_ = true;
+	    break;
+	  }
+      }
+      
+      bool
+      recurse(const formula* f1, const formula* f2)
+      {
+	if (f1 == f2) return true;
+	inf_form_right_recurse_visitor v(f2);
+	const_cast<formula*>(f1)->accept(v);
+	return v.result();
+      }
+
+    protected:
+      bool result_; // true si f < f1, false sinon.
+      const formula* f;
+    };
+
+    /////////////////////////////////////////////////////////////////////////
+
+    class inf_form_left_recurse_visitor : public const_visitor
+    {
+    public:
+      
+      inf_form_left_recurse_visitor(const formula *f)
+      {
+	this->f = f;
+	result_ = false;
+      }
+    
+      virtual ~inf_form_left_recurse_visitor()
+      {
+      }
+
+      bool special_case(const formula* f2)
+      {
+	if ((node_type(f) == node_type_form_visitor::Binop) 
+	    && (node_type(f2) == node_type_form_visitor::Binop))
+	  if (((const binop*)f)->op() == ((const binop*)f2)->op())
+	    if (inf_form(((const binop*)f2)->first(),((const binop*)f)->first())
+		&& inf_form(((const binop*)f2)->second(),((const binop*)f)->second()) )
+	      return true;
+	return false;
+      }
+
+      int 
+      result() const
+      {
+	return result_;
+      }
+    
+      void
+      visit(const atomic_prop* ap)
+      {
+	inf_form_right_recurse_visitor v(ap);
+	const_cast<formula*>(f)->accept(v);
+	result_ = v.result();
+      }
+      
+      void
+      visit(const constant* c)
+      {
+	inf_form_right_recurse_visitor v(c);
+	switch (c->val())
+	  {
+	  case constant::True:
+	    const_cast<formula*>(f)->accept(v);
+	    result_ = v.result();
+	    return;
+	  case constant::False:
+	    result_ = true;
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(const unop* uo)
+      {
+	const formula* f1 = uo->child();
+	const formula* tmp = NULL;
+	inf_form_right_recurse_visitor v(uo);
+	switch (uo->op())
+	  {
+	  case unop::Not:
+	    if (uo == f)
+	      result_ = true;
+	    return;
+	  case unop::X:
+	    if (node_type(f) == node_type_form_visitor::Unop)
+	      if (((const unop*)f)->op() == unop::X) {
+		result_ = inf_form(f1,((const unop*)f)->child());
+	      }
+	    return;
+	  case unop::F: 
+	    // F(a) = true U a
+	    tmp = binop::instance(binop::U,constant::true_instance(),clone(f1));
+	    if (this->special_case(tmp)){
+	      result_ = true;
+	      spot::ltl::destroy(tmp);
+	      return;
+	    }
+	    if ( inf_form(tmp,f) )
+	      result_ = true;
+	    spot::ltl::destroy(tmp);
+	    return;
+	  case unop::G:
+	    // F(a) = false R a
+	    tmp = binop::instance(binop::R,constant::false_instance(),clone(f1));
+	    if (this->special_case(tmp)){
+	      result_ = true;
+	      spot::ltl::destroy(tmp);
+	      return;
+	    }
+	    if ( inf_form(f1,f) )
+	      result_ = true;
+	    spot::ltl::destroy(tmp);
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+            
+      void
+      visit(const binop* bo)
+      {
+	
+	if (this->special_case(bo))
+	  {
+	    result_ = true;
+	    return;
+	  }
+	
+	const formula* f1 = bo->first();
+	const formula* f2 = bo->second();
+	switch (bo->op())
+	  {
+	  case binop::Xor:
+	  case binop::Equiv:
+	  case binop::Implies:
+	    return;
+	  case binop::U:
+	    if ( (inf_form(f1,f)) && (inf_form(f2,f)) )
+	      result_ = true;
+	    return;
+	  case binop::R: 
+	    if ( (inf_form(f2,f)) )
+	      result_ = true;
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(const multop* mo)
+      {
+	if (mo == NULL);
+	multop::type op = mo->op();
+	unsigned mos = mo->size();
+	switch (op)
+	  {
+	  case multop::And:
+	    for (unsigned i = 0; (i < mos) && !result_ ; ++i)
+	      if ( (inf_form(mo->nth(i),f)) )
+		result_ = true;
+	    break;
+	  case multop::Or:
+	    for (unsigned i = 0; i < mos ; ++i)
+	      if ( !(inf_form(mo->nth(i),f)) )
+		return;
+	    result_ = true;
+	    break;
+	  }
+      }
+      
+    protected:
+      bool result_; // true if f1 < f, 1 otherwise.
+      const formula* f;
+    };
+
+    bool inf_form(const formula* f1, const formula* f2)
+    {
+      // f1 and f2 are unabbreviate 
+      if (f1 == f2) return true;
+      inf_form_left_recurse_visitor v1(f2);
+      inf_form_right_recurse_visitor v2(f1);
+		
+      if ( (node_type(f1) == node_type_form_visitor::Const) && 
+	   (node_type(f2) == node_type_form_visitor::Const) )
+	if ( (((const constant*)f2)->val() == constant::True) ||
+	     (((const constant*)f1)->val() == constant::False) )
+	  {
+	    return true;
+	  }
+      
+      const_cast<formula*>(f1)->accept(v1);
+      if (v1.result()) {
+	return true;
+      }
+
+      const_cast<formula*>(f2)->accept(v2);
+      if (v2.result()) {
+	return true;
+      }
+      
+      return false;
+    }
+        
+    bool infneg_form(const formula* f1, const formula* f2, int n)
+    {
+      const formula* ftmp1;
+      const formula* ftmp2;
+      const formula* ftmp3 = unop::instance(unop::Not,(n == 0)? clone(f1) : clone(f2));
+      const formula* ftmp4 = spot::ltl::negative_normal_form((n == 0)? f2 : f1);
+      const formula* ftmp5;
+      const formula* ftmp6;
+      bool retour;
+      
+      ftmp2 = spot::ltl::unabbreviate_logic(ftmp3);
+      ftmp1 = spot::ltl::negative_normal_form(ftmp2);
+      
+      ftmp5 = spot::ltl::unabbreviate_logic(ftmp4);
+      ftmp6 = spot::ltl::negative_normal_form(ftmp5);
+      
+      if (n == 0)
+	retour = inf_form(ftmp1, ftmp6);
+      else 
+	retour = inf_form(ftmp6, ftmp1);
+      
+      spot::ltl::destroy(ftmp1);
+      spot::ltl::destroy(ftmp2);
+      spot::ltl::destroy(ftmp3);
+      spot::ltl::destroy(ftmp4);
+      spot::ltl::destroy(ftmp5);
+      spot::ltl::destroy(ftmp6);
+      
+      return retour;
+    }
+
+  }
+}
diff --git a/src/ltlvisit/formlength.cc b/src/ltlvisit/formlength.cc
new file mode 100644
index 000000000..8c2f26261
--- /dev/null
+++ b/src/ltlvisit/formlength.cc
@@ -0,0 +1,103 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "reducform.hh"
+#include "ltlast/allnodes.hh"
+#include <cassert>
+
+#include "lunabbrev.hh"
+#include "nenoform.hh"
+#include "ltlvisit/destroy.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+   class length_form_visitor : public const_visitor
+    {
+    public:
+      
+      length_form_visitor()
+      {
+	result_ = 0;
+      }
+    
+      virtual ~length_form_visitor()
+      {
+      }
+
+      int 
+      result() const
+      {
+	return result_;
+      }
+
+      void
+      visit(const atomic_prop* ap)
+      { 
+	if (ap);
+	result_ = 1;
+      }
+      
+      void
+      visit(const constant* c)
+      {
+	if (c);
+	result_ = 1;
+      }
+      
+      void
+      visit(const unop* uo)
+      {
+	if (uo);
+	result_ = 1 + form_length(uo->child());
+      }
+      
+      void
+      visit(const binop* bo)
+      {
+	if (bo);
+	result_ = 1 + form_length(bo->first()) + form_length(bo->second());
+      }
+      
+      void
+      visit(const multop* mo)
+      {
+	unsigned mos = mo->size();
+	for (unsigned i = 0; i < mos; ++i)
+	  result_ += form_length(mo->nth(i));
+      }
+      
+    protected:
+      int result_; // size of the formula
+    };
+
+    int
+    form_length(const formula* f)
+    {
+      length_form_visitor v;
+      const_cast<formula*>(f)->accept(v);
+      return v.result();
+    }
+
+  }
+}
diff --git a/src/ltlvisit/lunabbrev.cc b/src/ltlvisit/lunabbrev.cc
index ea9023632..0a8afba15 100644
--- a/src/ltlvisit/lunabbrev.cc
+++ b/src/ltlvisit/lunabbrev.cc
@@ -22,12 +22,58 @@
 #include "ltlast/allnodes.hh"
 #include "ltlvisit/clone.hh"
 #include "lunabbrev.hh"
+//#include "reducform.hh"
 #include <cassert>
 
 namespace spot
 {
   namespace ltl
   {
+   
+    class node_type_form_visitor : public const_visitor
+    {
+    public:
+      enum type { Atom, Const, Unop, Binop, Multop };
+      
+      node_type_form_visitor(){}
+      
+      type
+      result() const { return result_;}
+      
+      void
+      visit(const atomic_prop* ap){ 
+	if (ap == NULL);
+	result_ = node_type_form_visitor::Atom;
+      }
+      
+      void
+      visit(const constant* c){ 
+	if (c == NULL);
+	result_ = node_type_form_visitor::Const;
+      }
+      
+      void
+      visit(const unop* uo){
+	if (uo == NULL); 
+	result_ = node_type_form_visitor::Unop;
+      }
+      
+      void
+      visit(const binop* bo){ 
+	if (bo == NULL);
+	result_ = node_type_form_visitor::Binop;
+      }
+      
+      void
+      visit(const multop* mo){ 
+	if (mo == NULL);
+	result_ = node_type_form_visitor::Multop;
+      }
+      
+    protected:
+      type result_;
+    };
+    
     unabbreviate_logic_visitor::unabbreviate_logic_visitor()
     {
     }
@@ -36,11 +82,38 @@ namespace spot
     {
     }
 
+    /*
+    void
+    unabbreviate_logic_visitor::visit(unop* uo)
+    {
+      formula* f = uo->child();
+      switch (uo->op())
+	{
+	case unop::Not:
+	case unop::X:
+	  result_ = unop::instance(uo->op(),recurse(f));
+	  return;
+	case unop::F:
+	  result_ = binop::instance(binop::U,constant::true_instance(),recurse(f));
+	  return;
+	case unop::G:
+	  result_ = binop::instance(binop::R,constant::false_instance(),recurse(f));
+	  return;
+	}
+      // Unreachable code.
+      assert(0);
+    }
+    */
+
     void
     unabbreviate_logic_visitor::visit(binop* bo)
     {
       formula* f1 = recurse(bo->first());
       formula* f2 = recurse(bo->second());
+      
+      node_type_form_visitor v;
+      const_cast<formula*>(f1)->accept(v);
+
       switch (bo->op())
 	{
 	  /* f1 ^ f2  ==  (f1 & !f2) | (f2 & !f1) */
@@ -69,10 +142,24 @@ namespace spot
 						      unop::instance(unop::Not,
 								     f2)));
 	  return;
-	  /* f1 U f2 == f1 U f2 */
-	  /* f1 R f2 == f1 R f2 */
+
+	  /* true U f2 == F(f2) */
 	case binop::U:
+	  if ( v.result() == node_type_form_visitor::Const )
+	    if ( ((constant*)f1)->val() == constant::True ) {
+	      result_ = unop::instance(unop::F,f2);
+	      return;
+	    }
+	  result_ = binop::instance(bo->op(), f1, f2);
+	  return;
+
+	  /* false R f2 == G(f2) */
 	case binop::R:
+	  if ( v.result() == node_type_form_visitor::Const )
+	    if ( ((constant*)f1)->val() == constant::False ) {
+	      result_ = unop::instance(unop::G,f2);
+	      return;
+	    }
 	  result_ = binop::instance(bo->op(), f1, f2);
 	  return;
 	}
diff --git a/src/ltlvisit/lunabbrev.hh b/src/ltlvisit/lunabbrev.hh
index 882fa6d81..e5c5b5353 100644
--- a/src/ltlvisit/lunabbrev.hh
+++ b/src/ltlvisit/lunabbrev.hh
@@ -47,6 +47,7 @@ namespace spot
       virtual ~unabbreviate_logic_visitor();
 
       using super::visit;
+      //void visit(unop* uo);
       void visit(binop* bo);
 
       virtual formula* recurse(formula* f);
diff --git a/src/ltlvisit/nenoform.hh b/src/ltlvisit/nenoform.hh
index ea960b203..9cbc215e0 100644
--- a/src/ltlvisit/nenoform.hh
+++ b/src/ltlvisit/nenoform.hh
@@ -43,6 +43,7 @@ namespace spot
     /// or spot::ltl::unabbreviate_ltl first.  (Calling these functions
     /// after spot::ltl::negative_normal_form would likely produce a
     /// formula which is not in negative normal form.)
+
     formula* negative_normal_form(const formula* f, bool negated = false);
   }
 }
diff --git a/src/ltlvisit/reducform.cc b/src/ltlvisit/reducform.cc
new file mode 100644
index 000000000..94151328f
--- /dev/null
+++ b/src/ltlvisit/reducform.cc
@@ -0,0 +1,392 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#include "reducform.hh"
+#include "ltlast/allnodes.hh"
+#include <cassert>
+
+#include "lunabbrev.hh"
+#include "nenoform.hh"
+#include "ltlvisit/destroy.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+
+    
+    //class unabbreviate_FG_visitor::unabbreviate_logic_visitor()
+    
+    class reduce_form_visitor : public visitor
+    {
+    public:
+      
+      reduce_form_visitor()
+      {
+	/*
+	  eventuality_ = false;
+	  universality_ = false;
+	*/
+      }
+    
+      virtual ~reduce_form_visitor()
+      {
+      }
+
+      formula* 
+      result() const
+      {
+	return result_;
+      }
+      
+      /*
+	bool
+	is_eventuality()
+	{
+	return eventuality_;
+	}
+	
+	bool
+	is_universality()
+	{
+	return universality_;
+	}
+      */
+    
+      void
+      visit(atomic_prop* ap)
+      { 
+	formula* f = ap->ref();
+	result_ = f;
+      }
+      
+      void
+      visit(constant* c)
+      {
+	switch (c->val())
+	  {
+	  case constant::True:
+	    result_ = constant::true_instance();
+	    return;
+	  case constant::False:
+	    result_ = constant::false_instance();
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(unop* uo)
+      {
+	result_ = recurse(uo->child());
+
+	switch (uo->op())
+	  {
+	  case unop::Not:
+	    result_ = unop::instance(unop::Not, result_);
+	    return;
+
+	  case unop::X:
+	    result_ = unop::instance(unop::X, result_);
+	    return;
+
+	  case unop::F: 
+	    /* if f is class of eventuality then F(f)=f */
+	    if (!is_eventual(result_)) {
+	      result_ = unop::instance(unop::F, result_);
+	    }
+	    return;
+
+	  case unop::G:
+	    /* if f is class of universality then G(f)=f */
+	    if (!is_universal(result_)) {
+	      result_ = unop::instance(unop::G, result_);
+	    }
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(binop* bo)
+      {
+	formula* f2 = recurse(bo->second());
+	
+	/* if b is of class eventuality then a U b = b
+	   if b is of class universality then a R b = b */
+	if ( ( is_eventual(f2) && ( (bo->op()) == binop::U )) ||
+	     ( is_universal(f2) && ( (bo->op()) == binop::R )) ) 
+	  {
+	    result_ = f2; 
+	    return;
+	  }
+	
+	/* case of implies */
+	formula* f1 = recurse(bo->first());
+	bool inf = inf_form(f1,f2);
+	bool infinv = inf_form(f2,f1);
+	//binop* ftmp = NULL;
+	bool infnegleft = infneg_form(f2,f1,0);
+	bool infnegright = infneg_form(f2,f1,1);
+	
+	switch (bo->op())
+	  {
+	  case binop::Xor:
+	  case binop::Equiv:
+	  case binop::Implies:
+	    result_ = binop::instance(bo->op(), f1, f2);
+	    return;
+
+	  case binop::U:
+	    /* a < b => a U b = b */
+	    if (inf) 
+	      { 
+		result_ = f2;
+		spot::ltl::destroy(f1);
+		return;
+	      }
+	    /* !b < a => a U b = Fb */
+	    if (infnegleft)
+	      {
+		result_ = unop::instance(unop::F, f2);
+		spot::ltl::destroy(f1);
+		return;
+	      }
+	    /* a < b => a U (b U c) = (b U c) */
+	    if (node_type(f2) == node_type_form_visitor::Binop)
+	      if (((binop*)f2)->op() == binop::U)
+		if (inf_form(f1,((binop*)f2)->first())){
+		  result_ = f2;
+		  spot::ltl::destroy(f1);
+		  return;
+		} 
+	    result_ = binop::instance(binop::U,
+				      f1, f2);
+	    return;
+
+	  case binop::R:
+	    /* b < a => a R b = b */
+	    if (infinv) 
+	      {
+		result_ = f2;
+		spot::ltl::destroy(f1);
+		return;
+	      }
+	    /* b < !a => a R b = Gb */
+	    if (infnegright)
+	      {
+		result_ = unop::instance(unop::G, f2);
+		spot::ltl::destroy(f1);
+		return;
+	      }
+	    /* b < a => a R (b R c) = b R c */
+	    if (node_type(f2) == node_type_form_visitor::Binop)
+	      if (((binop*)f2)->op() == binop::R)
+		if (inf_form(((binop*)f2)->first(),f1)){
+		  result_ = f2;
+		  spot::ltl::destroy(f1);
+		  return;
+		}  
+
+	    result_ = binop::instance(binop::R,
+				      f1, f2);
+	    return;
+	  }
+	/* Unreachable code.  */
+	assert(0);
+      }
+      
+      void
+      visit(multop* mo)
+      {
+	formula* f1 = NULL;
+	formula* f2 = NULL;
+	unsigned mos = mo->size();
+	multop::vec* res = new multop::vec;
+	multop::vec::iterator index;
+	multop::vec::iterator indextmp;
+	
+	for (unsigned i = 0; i < mos; ++i)
+	  res->push_back(recurse(mo->nth(i)));
+
+      	switch (mo->op())
+	  {
+
+	  case multop::Or:
+	    index = indextmp = res->begin();
+	    if (index != res->end()) 
+	      {
+		f1 = *index;
+		index++;
+	      }
+	    for (; index != res->end();index++)
+	      {
+		f2 = *index;
+		/* a < b => a + b = b */
+		if (inf_form(f1,f2)) // f1 < f2
+		  {
+		    f1 = f2;
+		    spot::ltl::destroy(*indextmp);
+		    res->erase(indextmp);
+		    indextmp = index;
+		    index--;
+		  }
+		else if (inf_form(f2,f1)) // f2 < f1
+		  {
+		    spot::ltl::destroy(*index);
+		    res->erase(index);
+		    index--;
+		  }
+	      }
+	    break;
+
+	  case multop::And: 
+	    index = indextmp = res->begin();
+	    if (mos)
+	      {
+		f1 = mo->nth(0);
+		index++;
+	      }
+	    for (; index != res->end(); index++)
+	      {
+		f2 = *index;
+		/* a < b => a & b = a */
+		if (inf_form(f1,f2)) // f1 < f2
+		  {
+		    spot::ltl::destroy(*index);
+		    res->erase(index);
+		    index--;
+		  }
+		else if (inf_form(f2,f1)) // f2 < f1
+		  {
+		    f1 = f2;
+		    spot::ltl::destroy(*indextmp);
+		    res->erase(indextmp);
+		    indextmp = index;
+		    index--;
+		  }
+	      }
+	    break;
+	  }
+	
+	/* f1 < !f2 => f1 & f2 = false 
+	   !f1 < f2 => f1 | f2 = true */
+	
+	for (index = res->begin(); index != res->end(); index++){
+	  for (indextmp = res->begin(); indextmp != res->end(); indextmp++){
+	    if (index != indextmp){
+	      if (infneg_form(*index,*indextmp, (mo->op() == multop::Or) ? 0 : 1)) {
+		for (multop::vec::iterator j = res->begin(); j != res->end(); j++){
+		  spot::ltl::destroy(*j);
+		}
+		if (mo->op() == multop::Or)
+		  result_ = constant::true_instance();
+		else 
+		  result_ = constant::false_instance();
+		return;
+	      }
+	
+	      /*
+	      if ((constant*)(*index) != NULL)
+		if (((((constant*)(*index))->val() == constant::True) &&
+		     (mo->op() == multop::Or)) || 
+		    (((((constant*)(*index))->val() == constant::False)) 
+		     && (mo->op() == multop::And))
+		    ) {
+		  //std::cout << "constant" << std::endl;
+		  for (multop::vec::iterator j = res->begin(); j != res->end(); j++){
+		    spot::ltl::destroy(*j);
+		  }
+		  if (mo->op() == multop::Or)
+		    result_ = constant::true_instance();
+		  else 
+		    result_ = constant::false_instance();
+		  
+		  std::cout << "2" << std::endl;
+		  spot::ltl::dump(std::cout,mo);
+		  return;
+		}
+	      */
+	
+	    }
+	  }
+	}
+	
+	if (res->size()) {
+	  result_ = multop::instance(mo->op(),res);
+	  return;
+	}
+	assert(0);
+      }
+      
+      formula*
+      recurse(formula* f)
+      {
+	return reduce_form(f);
+      }
+
+    protected:
+      formula* result_;
+      /*
+	bool eventuality_;
+	bool universality_;
+      */
+    };
+
+    formula*
+    reduce_form(const formula* f)
+    {      
+      spot::ltl::formula* ftmp1;
+      spot::ltl::formula* ftmp2;
+      reduce_form_visitor v;
+      
+      ftmp1 = spot::ltl::basic_reduce_form(f);
+      const_cast<formula*>(ftmp1)->accept(v);
+      ftmp2 = spot::ltl::basic_reduce_form(v.result());
+      
+      spot::ltl::destroy(ftmp1);
+      spot::ltl::destroy(v.result());
+      
+      return ftmp2;
+    }
+
+    formula*
+    reduce(const formula* f)
+    {
+      spot::ltl::formula* ftmp1;
+      spot::ltl::formula* ftmp2;
+      spot::ltl::formula* ftmp3;
+
+      ftmp1 = spot::ltl::unabbreviate_logic(f);
+      ftmp2 = spot::ltl::negative_normal_form(ftmp1);      
+      ftmp3 = spot::ltl::reduce_form(ftmp2);
+      
+      spot::ltl::destroy(ftmp1);
+      spot::ltl::destroy(ftmp2);
+      
+      return ftmp3;
+
+    }
+
+  }
+}
diff --git a/src/ltlvisit/reducform.hh b/src/ltlvisit/reducform.hh
new file mode 100644
index 000000000..17552e029
--- /dev/null
+++ b/src/ltlvisit/reducform.hh
@@ -0,0 +1,86 @@
+// Copyright (C) 2003  Laboratoire d'Informatique de Paris 6 (LIP6),
+// département Systèmes Répartis Coopératifs (SRC), Université Pierre
+// et Marie Curie.
+//
+// This file is part of Spot, a model checking library.
+//
+// Spot is free software; you can redistribute it and/or modify it
+// under the terms of the GNU General Public License as published by
+// the Free Software Foundation; either version 2 of the License, or
+// (at your option) any later version.
+//
+// Spot is distributed in the hope that it will be useful, but WITHOUT
+// ANY WARRANTY; without even the implied warranty of MERCHANTABILITY
+// or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General Public
+// License for more details.
+//
+// You should have received a copy of the GNU General Public License
+// along with Spot; see the file COPYING.  If not, write to the Free
+// Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
+// 02111-1307, USA.
+
+#ifndef SPOT_LTLVISIT_REDUCFORM_HH
+# define SPOT_LTLVISIT_REDUCFORM_HH
+
+#include "ltlast/formula.hh"
+#include "ltlast/visitor.hh"
+
+// For debog
+#include "ltlvisit/dump.hh"
+
+namespace spot
+{
+  namespace ltl
+  {
+    formula* reduce(const formula* f);
+
+    /* Basic rewriting */
+    formula* basic_reduce_form(const formula* f);
+    
+    /* formula rewriting using univerality, eventuality, 
+       implies and basic_reduce_form */
+    formula* reduce_form(const formula* f);
+
+    /* detect easy case of implies */
+    bool inf_form(const formula* f1, const formula* f2); 
+    /* true if f1 < f2, false otherwise */
+    bool infneg_form(const formula* f1, const formula* f2, int n); 
+    /* true if !f1 < f2, false otherwise */
+    
+    /* detect if a formula is of class eventuality or universality */
+    bool is_eventual(const formula* f);
+    bool is_universal(const formula* f);
+
+    /* detect if a formula is of form GF or FG */
+    bool is_GF(const formula* f);
+    bool is_FG(const formula* f);
+      
+    /* To know the first node of a formula */
+    
+    class node_type_form_visitor : public const_visitor
+    {
+    public:
+      enum type { Atom, Const, Unop, Binop, Multop };
+      node_type_form_visitor();
+      virtual ~node_type_form_visitor(){};
+      type result() const;
+      void visit(const atomic_prop* ap);
+      void visit(const constant* c);
+      void visit(const unop* uo);
+      void visit(const binop* bo);
+      void visit(const multop* mo);
+    protected:
+      type result_;
+    };
+    
+    node_type_form_visitor::type node_type(const formula* f);
+
+    /* Obsolete */
+    int nb_term_multop(const formula* f);
+    formula* reduce_inf_form(const formula* f); /* Obsolete */
+    int form_length(const formula* f); /* For test */
+    
+  }
+}
+
+#endif //  SPOT_LTLVISIT_REDUCFORM_HH