assign(max_seconds, 30). assign(new_constants, 1). formulas(sos). f(x,f(f(y,z),f(y,z))) = f(y,f(f(x,z),f(x,z))). % A_SS f(f(x,x),f(x,y)) = x. % B_SS f(x,f(x,x)) = f(y,f(y,y)). % ONE_SS f(x,f(y,f(x,f(z,z)))) = f(x,f(z,f(x,f(y,y)))). % MOD_SS x v y = f(f(x,x),f(y,y)) # label(definition_join). x ^ y = f(f(x,y),f(x,y)) # label(definition_meet). x' = f(x,x) # label(definition_complementation). end_of_list. formulas(goals). x v (y v z) = y v (x v z) # answer(AJ). x v (x ^ y) = x # answer(B1). x ^ y = (x' v y')' # answer(DM). x'' = x # answer(CC). x v x' = y v y' # answer(ONE). x v (y ^ (x v z)) = x v (z ^ (x v y)) # answer(MOD). f(x,y) = x' v y' # answer(DEF_SS). end_of_list.