% Examples of complicated substitutions in condensed detachment.
% These occur in Larry Wos's proofs that XCB is a single axiom for EC.

set(hyper_res).
assign(max_given, 1).

list(usable).

% Condensed detachment, but we'll also show the instance of the minor premise.

-major(e(x,y)) | -minor(x) | P(y) | minor_instance(x).  % condensed detachment

major(e(e(e(e(e(x,e(y,e(e(e(e(e(z,e(e(e(z,u),e(v,u)),v)),e(e(w,e(e(e(w,
      v6),e(v7,v6)),v7)),y)),v8),e(v9,v8)),v9))),x),v10),e(v11,v10)),v11)).

end_of_list.

list(sos).

minor(e(e(e(e(e(e(x,e(e(y,e(e(e(y,z),e(u,z)),u)),x)),e(v,e(e(e(v,w),
      e(v6,w)),v6))),v7),v8),e(v7,v8)),e(v9,e(e(e(v9,v10),e(v11,v10)),v11)))).

end_of_list.

% The preceding example has a minor instance with almost 3,000 symbols;
% the conclusion is P(e(e(e(x,e(y,e(e(e(y,z),e(u,z)),u))),v),e(x,v))).
%
% The following example has a minor instance with almost 10,000 symbols.
%
% major(e(e(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(e(w,e(e(v6,
%    e(e(e(v6,v7),e(v8,v7)),v8)),e(e(v9,e(e(e(v9,v10),e(v11,v10 )),v11)),
%    w))),e(v12,e(e(e(v12,v13),e(v14,v13)),v14)))),v15),e(v16,v15)),v16))
% 
% minor(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),e(w,
%     e(e(e(e(e(e(e(e(e(e(e(v6,e(e(e(v6,v7),e(v8,v7)),v8)),v9),v10),e(v9,
%     v10)),v11),e(v12,v11)),v12),w),v13),e(v14,v13)),v14)))).
%
% The conclusion is P(e(e(e(e(e(e(x,e(e(e(x,y),e(z,y)),z)),u),v),e(u,v)),
%                      e(e(e(w,v6),e(v7,v6)),v7)),w)).