From: Ranganathan PadmanabhanTo: William McCune Cc: Ranganathan Padmanabhan Date: Wed, 29 Mar 2006 16:01:03 -0600 Subject: Prover9 input for quotient condition, please Hi Bill, I am writing an account of what we proved in Albuquerque on CS- related problems. A well-known theorem in CS says that a cancellation semigroup satisfying a non-trivial identity must satisfy the Ore's quotient condition. i.e. {CS, x*f*y = y*g*x} ==> Ore's quotient condition which is a * a0 = b * b0. c * a0 = d * b0. a * c0 = b * d0. implies c * c0 = d * d0 Some candidates of x*f*y = y*g*x for experimentation. 1. commutativity x*y = y*x. This proof must come very quickly 2. (x * y)^3 = x^3 * y^3. 3. (x * y)^3 = (y * x)^3. In our Monograph, we have proved , using Otter, the same result with x*y*z*y*x = y*x*z*x*y (the nilpotent class 2 case). (see Theorem CS-13 on page 104). Please try the above three examples and send me a Prover9 input file. Thanks. R. P.

Commutativity.

Nilpotent Class 2.prover9 -f quot-comm.in > quot-comm.out ; ### ( quot-comm.out.xml )

(xy)^3 = x^3 y^3.prover9 -f quot-np2.in > quot-np2.out ; ### ( quot-np2.out.xml )

(xy)^3 = (yx)^3.prover9 -f quot-xy3a.in > quot-xy3a.out ; ### ( quot-xy3a.out.xml )

The general caseprover9 -f quot-xy3b.in > quot-xy3b.out ; ### ( quot-xy3b.out.xml )

prover9 -f quot-general.in > quot-general.out ; ### ( quot-general.out.xml )