assign(max_seconds, 3600). assign(order, kbo). % Knuth-Bendix ordering set(lex_order_vars). assign(max_weight, 50). list(weights). % Penalize deep equations by adding the depth to the symbol count. weight(x = y) = (weight(x) + weight(y)) + depth(x = y). end_of_list. formulas(sos). f(x,x,y) = x # label(majority). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). f(f(x,w,y),w,z) = f(x,w,f(y,w,z)) # label(associativity). end_of_list. set(restrict_denials). formulas(goals). f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) # label(dist_long). f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_short). f(f(x,y,z),u,w) = f(f(x,u,w),f(y,u,w),f(z,u,w)) & f(f(x,y,z),u,w) = f(x,f(y,u,w),f(z,u,w)) # label(dist_both). end_of_list.