assign(max_seconds, 30). assign(order, kbo). % It works with the default (lpo) but it takes longer. formulas(assumptions). % combinators B and W a(a(a(B,x),y),z) = a(x,a(y,z)) # label(B). a(a(W,x),y) = a(a(x,y),y) # label(W). end_of_list. formulas(goals). % existence of a fixed point combinator (exists Q all x (a(Q,x) = a(x,a(Q,x)))) # label(fixed_point_combinator). end_of_list. % Here is a different way of specifying the goal, which tells us % what the fixed point combinator is. We use an answer attribute. % Unfortunately, answer attributes are not allowed on non-clausal % (e.g., goal) formulas, so we deny the goal and state it as an assumption. % Note that this introduces the Skolem function f. % % formulas(assumptions). % a(x,f(x)) != a(f(x),a(x,f(x))) # answer(x). % end_of_list.