% Started on gyro.thornwood at Wed Dec 3 17:49:43 CST 2003. % Here is the mace head file head.2-3. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % set(print_models_portable). % % assign(iterate_up_to, 3). % % clauses(theory). % % % denial of group % % f(f(X,Y),Z) != f(X,f(Y,Z)) | f(f(g(X),X),Y) != Y | f(g(X),X) != f(g(Y),Y). % % end_of_list. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % g(f(g(f(f(y,z),z)),f(f(f(y,z),g(x)),x))) = z. % candidate 1 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [1]), function(g(_), [0,1,2]), function(f(_,_), [0,2,1, 2,1,0, 1,0,2]) ]). % g(f(f(f(y,z),g(z)),f(g(f(f(x,z),y)),x))) = z. % candidate 16 interpretation( 2, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0]), function(f(_,_), [1,0, 0,0]) ]). % g(f(f(g(f(y,z)),y),f(f(g(f(z,x)),z),x))) = z. % candidate 23 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0,2]), function(f(_,_), [2,0,1, 1,2,0, 0,1,2]) ]). % f(f(g(f(y,z)),y),g(f(g(f(f(x,z),z)),x))) = z. % candidate 26 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,1,2]), function(f(_,_), [1,0,2, 2,1,0, 0,2,1]) ]). % f(f(f(g(y),y),z),f(g(f(f(g(z),z),x)),x)) = z. % candidate 33 interpretation( 2, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,0]), function(f(_,_), [1,1, 1,0]) ]). % f(g(f(f(g(y),y),z)),f(f(f(z,z),g(x)),x)) = z. % candidate 37 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,1,2]), function(f(_,_), [1,2,1, 2,1,0, 1,0,1]) ]). % f(f(f(g(x),x),g(y)),f(f(f(y,z),g(x)),x)) = z. % candidate 271 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,2,1]), function(f(_,_), [1,2,0, 2,0,1, 0,1,2]) ]). % g(f(g(f(f(y,z),z)),f(f(y,f(z,g(x))),x))) = z. % candidate 318 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,1,2]), function(f(_,_), [1,2,0, 0,1,2, 2,0,1]) ]). % g(f(f(f(g(x),x),y),f(g(f(x,f(z,y))),x))) = z. % candidate 597 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0,2]), function(f(_,_), [2,1,0, 0,2,1, 1,0,2]) ]). % g(f(g(f(f(y,z),z)),f(f(y,z),f(g(x),x)))) = z. % candidate 635 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0,2]), function(f(_,_), [0,2,1, 2,1,0, 1,0,2]) ]). % f(g(f(f(y,g(z)),z)),f(f(y,z),f(g(x),x))) = z. % candidate 636 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0,2]), function(f(_,_), [2,2,0, 2,2,1, 1,0,2]) ]). % g(f(f(g(f(y,z)),z),f(g(f(x,z)),f(x,y)))) = z. % candidate 649 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,2,0]), function(f(_,_), [1,2,1, 2,2,0, 1,0,0]) ]). % f(f(g(f(y,z)),y),f(f(z,z),g(f(g(x),x)))) = z. % candidate 653 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,0,0]), function(f(_,_), [1,1,1, 0,2,1, 2,0,0]) ]). % f(f(f(g(y),y),x),g(f(g(f(x,z)),f(x,x)))) = z. % candidate 742 interpretation( 3, [ function(X, [0]), function(Y, [1]), function(Z, [0]), function(g(_), [0,1,2]), function(f(_,_), [2,1,0, 0,2,1, 0,1,2]) ]). % f(g(f(f(x,g(y)),y)),f(f(x,z),f(g(x),x))) = z. % candidate 814 interpretation( 2, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,1]), function(f(_,_), [0,1, 1,0]) ]). % f(f(f(y,z),g(z)),g(f(x,f(g(f(z,x)),y)))) = z. % candidate 957 interpretation( 2, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0]), function(f(_,_), [1,1, 0,1]) ]). % g(f(g(f(y,z)),f(f(f(x,g(f(z,x))),z),y))) = z. % candidate 3378 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [1]), function(g(_), [0,1,2]), function(f(_,_), [0,2,0, 0,2,1, 1,1,2]) ]). % g(f(f(x,x),g(f(f(f(z,f(g(y),y)),x),x)))) = z. % candidate 3542 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [1]), function(g(_), [0,1,2]), function(f(_,_), [2,0,0, 1,2,1, 0,1,2]) ]). % f(g(f(y,z)),f(f(y,f(z,z)),g(f(g(x),x)))) = z. % candidate 4811 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,2,2]), function(f(_,_), [1,0,1, 2,0,2, 2,0,2]) ]). % g(f(f(g(y),y),f(g(f(z,f(x,z))),f(z,x)))) = z. % candidate 4838 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0,2]), function(f(_,_), [2,2,1, 2,2,0, 0,1,2]) ]). % f(f(y,z),g(f(f(g(z),y),f(z,f(g(x),x))))) = z. % candidate 5410 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [1,0,2]), function(f(_,_), [1,0,1, 2,0,2, 2,0,2]) ]). % g(f(f(y,g(z)),f(f(z,x),g(f(z,f(y,x)))))) = z. % candidate 5419 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [1]), function(g(_), [0,1,2]), function(f(_,_), [2,2,0, 2,2,1, 0,1,2]) ]). % f(g(f(y,z)),f(y,f(z,f(z,g(f(g(x),x)))))) = z. % candidate 7002 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [1]), function(g(_), [1,1,2]), function(f(_,_), [0,2,0, 0,1,2, 0,2,1]) ]). % f(g(f(y,z)),f(y,f(z,g(f(x,g(f(z,x))))))) = z. % candidate 7006 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,2,0]), function(f(_,_), [1,2,1, 1,2,1, 1,2,0]) ]). % f(g(y),f(f(y,z),f(z,g(f(f(z,g(x)),x))))) = z. % candidate 15586 interpretation( 3, [ function(X, [0]), function(Y, [0]), function(Z, [0]), function(g(_), [0,0,0]), function(f(_,_), [1,2,0, 0,2,0, 0,1,0]) ]). % Checked 20568, passed 3541, new_interps 25. % Finished Wed Dec 3 18:09:56 CST 2003.