if(Prover9). assign(order, kbo). end_if. formulas(assumptions). % IP loop axioms 1 * x = x. x * 1 = x. x' * (x * y) = y. x'' = x. (x * y) * y' = x. 1' = 1. % alt, flex x * (x * y) = (x * x) * y. (x * y) * y = x * (y * y). x * (y * x) = (x * y) * x. % semiuniversal flexibility (x * (y * z)) * (y * x) = x * (y * (z * (y * x))). (((x * y) * z) * y) * x = (x * y) * ((z * y) * x). end_of_list. formulas(goals). % Moufang? x * (y * (x * z)) = ((x * y) * x) * z # answer(M1). ((z * x) * y) * x = z * (x * (y * x)) # answer(M2). x * ((y * z) * x) = (x * y) * (z * x) # answer(N1). end_of_list. %BEGIN % additional assumptions, possibly useful for sketches x * (y * (y * z)) = ((x * y) * y) * z # label(C). x * ((y * (z * z)) * x) = (x * y) * ((z * z) * x) # label(SM). (x * y) * (x * (y * z)) = x * (y * ((x * y) * z)) # label(S1). ((z * y) * x) * (y * x) = ((z * (y * x)) * y) * x # label(S2). (x * y) * (z * (x * y)) = ((x * (y * z)) * x) * y # label(RIF1). ((y * x) * z) * (y * x) = y * (x * ((z * y) * x)) # label(RIF2). x * ((y * (x * y)) * z) = (x * (y * x)) * (y * z) # label(ARIF1). (z * ((y * x) * y)) * x = (z * y) * ((x * y) * x) # label(ARIF2). x * ((x' * (y * y)) * (x * z)) = (y * (y * x)) * z # label(H1). ((z * x) * ((y * y) * x')) * x = z * ((x * y) * y) # label(H2). x * ((y * z) * (x * y)) = ((x * y) * (z * x)) * y # label(TSI1). ((y * x) * (z * y)) * x = y * ((x * z) * (y * x)) # label(TSI2). (x * y) * (y * ((z * y) * (y * x))) = (((x * y) * (y * z)) * y) * (y * x) # answer(MSUF). END%