Hallo! How to solve the Identity Problem for Semigroups in Z3?
like "formulas(assumptions).(xy)z=x(yz).x1x2=(((x1x1)x1)x1)x2.((((((x1x2)x1)x2)x1)x2)x1)x2=(((x1x2)x2)x2)x2.((x1x2)x3)x4=(((((x1x2)x1)x1)x1)x3)x4.end_of_list.formulas(goals).((((c1c1)c2)c2)c1)c2=((((c1c1)c2)c1)c2)*c2.end_of_list." in Prover9
Hallo! How to solve the Identity Problem for Semigroups in Z3? like "formulas(assumptions).(xy)z=x(yz).x1x2=(((x1x1)x1)x1)x2.((((((x1x2)x1)x2)x1)x2)x1)x2=(((x1x2)x2)x2)x2.((x1x2)x3)x4=(((((x1x2)x1)x1)x1)x3)x4.end_of_list.formulas(goals).((((c1c1)c2)c2)c1)c2=((((c1c1)c2)c1)c2)*c2.end_of_list." in Prover9