Online Otter-λ
-->
Examples
% distributivity of union over intersection in set theory
set(lambda).
set(binary_res).
set(demod_inf).
set(para_into).
set(para_from).
set(para_from_units_only).
set(process_input).
assign(max_distinct_vars,3).
assign(max_weight,24).
assign(pick_given_ratio,4).
assign(bsub_hint_wt,1).
weight_list(pick_and_purge).
weight(junk,50).
weight(g($(0)),1). %every g-term counts like a constant
end_of_list.
%set(very_verbose).
list(usable).
u!=v|v=u.
Set(p).
Set(q).
Set(r).
-Set(x) | Prop(Ap(x,y)).
Set(x) | -Prop(Ap(x,c(x))).
end_of_list.
list(demodulators).
in(x,y) = Ap(y,x).
not($T) = $F.
j = lambda(u,lambda(v,lambda(x,and(in(x,u),in(x,v))))). % j is intersection
i = lambda(u,lambda(v,lambda(x,or(in(x,u),in(x,v))))). % i is union
% q union r is Ap(Ap(i,q),r)
or(x,and(y,z)) = and(or(x,y),or(x,z)). % classical logic on the propositions
end_of_list.
list(sos).
x = x.
Ap(Ap(i,p), Ap( Ap(j,q),r)) != Ap( Ap(j, Ap(Ap(i,p),q)), Ap(Ap(i,p),r)). % the negation of the distributivity law we're trying to prove
end_of_list.