Cancallative Semigroups and Ore's Quotient Condition

    From: Ranganathan Padmanabhan 
    To: 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.

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

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

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

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

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