
Given a ring in which for all x, x * x * x * x * x = x, prove that for all x and y, x * y = y * x.
cnf(a_times_b_is_c,negated_conjecture, ( multiply(a,b) = c )). cnf(prove_commutativity,negated_conjecture, ( multiply(b,a) != c )).
Copyright 2019 Inference Web group.
All Rights Reserved.