set(print_models_portable). assign(domain_size, 16). clauses(theory). % All of these are consequences of C1 below. f(x,y) != f(x,z) | y = z. f(y,x) != f(z,x) | y = z. f(0,x) = x. f(x,0) = x. f(g(x),x) = 0. f(x,g(x)) = 0. g(g(x)) = x. g(0) = 0. g(f(x,y)) = f(g(y),g(x)). f(x,f(g(x),y)) = y. f(g(x),f(x,y)) = y. f(f(x,x),y) = f(x,f(x,y)). f(f(x,y),x) = f(x,f(y,x)). f(f(y,x),x) = f(y,f(x,x)). % Some of the following are redundant. f(f(x,f(y,y)),y)=f(f(x,y),f(y,y)). f(f(x,y),f(x,x))=f(x,f(y,f(x,x))). f(f(x,y),f(x,y))=f(x,f(y,f(x,y))). f(f(x,f(y,x)),y)=f(x,f(y,f(x,y))). f(f(x,f(x,y)),y)=f(x,f(x,f(y,y))). f(x,f(f(y,x),z))=f(f(x,y),f(x,z)). f(f(x,y),f(x,z))=f(x,f(f(y,x),z)). f(f(x,y),f(y,x))=f(x,f(y,f(y,x))). f(f(f(x,y),z),y)=f(x,f(y,f(z,y))). f(f(f(x,y),z),x)=f(x,f(y,f(z,x))). f(f(x,y),f(y,y))=f(x,f(y,f(y,y))). f(f(x,f(y,y)),y)=f(x,f(y,f(y,y))). f(f(x,f(y,x)),z)=f(x,f(y,f(x,z))). f(f(x,f(y,y)),z)=f(x,f(y,f(y,z))). f(f(x,f(x,y)),z)=f(x,f(x,f(y,z))). f(f(x,y),f(z,z))=f(x,f(y,f(z,z))). f(f(x,f(y,z)),y)=f(f(x,y),f(z,y)). f(f(x,y),f(z,x))=f(x,f(f(y,z),x)). f(x,f(f(y,z),x))=f(f(x,y),f(z,x)). f(f(g(f(y,x)),x),g(f(g(f(y,f(x,z))),x))) = z. % C1 f(f(A,B),C) != f(A,f(B,C)). end_of_list.