----- MACE4 2003-C, Nov 2003 ----- Built with library LADR 2003-C (working), Nov 2003. The process was started by mccune on gyro.thornwood, Fri Nov 21 14:43:27 2003 The command was "mace4". The process ID is 23163. op(450,infix_right,+). op(400,infix_right,*). op(350,prefix,-). set(print_models_portable). assign(iterate_up_to,19). set(integer_ring). lex([H,K,A,B,C]). clauses(theory). f(x,y) = H * x + K * y. f(f(f(f(x,y),z),z),f(y,f(x,z))) = y. f(A,B) != f(B,A) | f(f(A,B),f(A,f(B,C))) != A. end_of_list. % There are no domain elements in the input. ====== Starting search for domain size 2. ====== Clearing flag lnh, because the least number heuristic is not compatible with flag integer_ring. ====== Starting search for domain size 3. ====== ====== Starting search for domain size 4. ====== ====== Starting search for domain size 5. ====== ====== Starting search for domain size 6. ====== ====== Starting search for domain size 7. ====== ====== Starting search for domain size 8. ====== ====== Starting search for domain size 9. ====== ====== Starting search for domain size 10. ====== ====== Starting search for domain size 11. ====== -------- Model 1 at 0.05 seconds -------- interpretation( 11, [ function(H, [8]), function(K, [4]), function(A, [0]), function(B, [0]), function(C, [1]), function(+(_,_), [0,1,2,3,4,5,6,7,8,9,10, 1,2,3,4,5,6,7,8,9,10,0, 2,3,4,5,6,7,8,9,10,0,1, 3,4,5,6,7,8,9,10,0,1,2, 4,5,6,7,8,9,10,0,1,2,3, 5,6,7,8,9,10,0,1,2,3,4, 6,7,8,9,10,0,1,2,3,4,5, 7,8,9,10,0,1,2,3,4,5,6, 8,9,10,0,1,2,3,4,5,6,7, 9,10,0,1,2,3,4,5,6,7,8, 10,0,1,2,3,4,5,6,7,8,9]), function(*(_,_), [0,0,0,0,0,0,0,0,0,0,0, 0,1,2,3,4,5,6,7,8,9,10, 0,2,4,6,8,10,1,3,5,7,9, 0,3,6,9,1,4,7,10,2,5,8, 0,4,8,1,5,9,2,6,10,3,7, 0,5,10,4,9,3,8,2,7,1,6, 0,6,1,7,2,8,3,9,4,10,5, 0,7,3,10,6,2,9,5,1,8,4, 0,8,5,2,10,7,4,1,9,6,3, 0,9,7,5,3,1,10,8,6,4,2, 0,10,9,8,7,6,5,4,3,2,1]), function(f(_,_), [0,4,8,1,5,9,2,6,10,3,7, 8,1,5,9,2,6,10,3,7,0,4, 5,9,2,6,10,3,7,0,4,8,1, 2,6,10,3,7,0,4,8,1,5,9, 10,3,7,0,4,8,1,5,9,2,6, 7,0,4,8,1,5,9,2,6,10,3, 4,8,1,5,9,2,6,10,3,7,0, 1,5,9,2,6,10,3,7,0,4,8, 9,2,6,10,3,7,0,4,8,1,5, 6,10,3,7,0,4,8,1,5,9,2, 3,7,0,4,8,1,5,9,2,6,10]) ]). -------- end of model -------- ----- MAX_MODELS EXIT (1 model) ----- CPU time: 0.05 seconds. The process finished Fri Nov 21 14:43:27 2003