assign(max_seconds, 30). assign(order, kbo). formulas(sos). f(x,x,y) = x # label(majority). f(f(x,w,y),z,w) = f(w,x,f(w,z,y)) # label(associativity2). end_of_list. formulas(goals). f(x,y,z) = f(z,x,y) # label(2a). f(x,y,z) = f(x,z,y) # label(2b). end_of_list.