decisions: THEORY
 BEGIN

 u,v,w,x,y,z: VAR real
 f: [real -> real]

eq1: THEOREM x = f(x) IMPLIES f(f(f(x))) = x

 g: [real, real -> real]

eq2: THEOREM x = f(y) IMPLIES g(f(y + 2 - 2), x + 2) = g(x, f(y) + 2)

fact3: THEOREM x < 2*y AND y < 3*v IMPLIES 3*x < 18*v

flaw4: CONJECTURE x < 2*y AND y < 3*v IMPLIES 3*x < 17*v

fact5: CONJECTURE x < 0 and y < 0 IMPLIES x * y > 0

i, j, k: VAR int

fact6: THEOREM 2*i < 5 and i > 1 IMPLIES i = 2

flaw7: CONJECTURE 2*x < 5 AND x > 1 IMPLIES x = 2

fact7: CONJECTURE i > 0 and i < 3 IMPLIES i = 1 OR i = 2
 
fact8: PROPOSITION (u/(2*x) - v/(2*y))/w = (u/x - v/y)/(2*w)

fact9: PROPOSITION (x + y = i - 1)
               AND (u + v = i + 1)
           IMPLIES 1 + x + u + y + v = 2*(i + 1) - 1

END decisions