% This input file directs Otter to find a specific proof.

op(400, xfx, ^).
op(400, xfx, v).

set(para_from).
set(para_into).
set(order_eq).
set(hyper_res).
set(ancestor_subsume).
set(back_sub).

assign(max_weight,61).
assign(change_limit_after,100).
assign(new_max_weight,31).
assign(bsub_hint_wt,1).
set(keep_hint_subsumers).

clear(print_kept).
clear(print_back_sub).
clear(print_new_demod).
clear(print_back_demod).
clear(detailed_history).
set(order_history).

% assign(max_proofs,-1).
  
weight_list(pick_and_purge).
%  Following are, first 4, less common basis, second 6, more standard basis; to cause immediate focus to get respective conjunctions proved quickly.
weight(y v (x^ (y^z))=y,0).
weight(y^ (x v (y v z))=y,0).
weight(((x^y) v (y^z)) v y=y,0).
weight(((x v y)^ (y v z))^y=y,0).
weight(y ^ x = x ^ y,0).
weight((x ^ y) ^ z = x ^ (y ^ z),0).
weight(x ^ (x v y) = x,0).
weight(y v x = x v y,0).
weight((x v y) v z = x v (y v z),0).
weight(x v (x ^ y) = x,0).
weight(junk,1000).
end_of_list.

list(sos).  % Here is the single axiom.
(((y v x)^x) v (((z^ (x v x)) v (u^x))^v))^ (w v ((v6 v x)^ (x v v7)))=x.
end_of_list.
  
list(usable).
x = x.

% Denial of the McKenzie 4-basis.

B v (A^ (B^C))!=B |
    B^ (A v (B v C))!=B |
    ((A^B) v (B^C)) v B!=B |
    ((A v B)^ (B v C))^B!=B.

% Denial of the standard 6-basis.
%
% B ^ A != A ^ B |
%     (A ^ B) ^ C != A ^ (B ^ C) |
%     A ^ (A v B) != A |
%     B v A != A v B |
%     (A v B) v C != A v (B v C) |
%     A v (A ^ B) != A.

end_of_list.

list(demodulators).  % Block a particular step.
EQ((x v (((y^ (x v x)) v (z^ (x v x)))^u))^ (v v (x v x))=x v x, junk).
end_of_list.

% The following list of hints leads Otter directly to a specific proof.

list(hints).
(((x v y)^y) v (y v y))^ (z v ((u v y)^ (y v v)))=y.
(((x v (y v y))^ (y v y)) v ((y v y) v (y v y)))^ (z v y)=y v y.
(((x v y)^y) v (((y v y) v (z^y))^u))^ (v v ((w v y)^ (y v v6)))=y.
(((x v (((y v y) v (z^y))^u))^ (((y v y) v (z^y))^u)) v ((((y v y) v (z^y))^u) v (((y v y) v (z^y))^u)))^ (v v y)= ((y v y) v (z^y))^u.
(((x v y)^y) v (((((y v y) v (z^y))^u) v (v^y))^w))^ (v6 v ((v7 v y)^ (y v v8)))=y.
(((x v y)^y) v (z^y))^ (u v ((v v y)^ (y v w)))=y.
(((x v (y^z))^ (y^z)) v (u^ (y^z)))^ (v v z)=y^z.
(((x v y)^y) v (((z^y) v (u^y))^v))^ (w v ((v6 v y)^ (y v v7)))=y.
(((x v y)^y) v y)^ (z v ((u v y)^ (y v v)))=y.
(((x v y)^y) v (((z^y) v (u^y))^v))^ (w v y)=y.
(((x v y)^y) v (z^y))^ (u v y)=y.
(((x v y)^y) v (y v y))^ (z v y)=y.
(x v (((y^ (x v x)) v (z^ (x v x)))^u))^ (v v (x v x))=x v x.
(x v (y^ (x v x)))^ (z v ((u v (x v x))^ ((x v x) v v)))=x v x.
(((x v y)^y) v ((z^y) v (z^y)))^ (u v y)=y.
(x v x)^ (y v ((z v (x v x))^ ((x v x) v u)))=x v x.
((x^y) v (x^y))^ (z v y)= (x^y) v (x^y).
((x v y)^y) v ((x v y)^y)=y.
(x^y)^ (z v y)=x^y.
x^ (y v ((z v x)^ (x v u)))=x.
(((x v y)^y) v ((z^y) v (u^y)))^ (v v y)=y.
((x^y) v (z^y))^ (u v y)= (x^y) v (z^y).
((x v y)^y) v (z^y)=y.
x^ (x v y)=x.
((x v y)^y) v ((z^y) v (u^y))=y.
((x v y)^y) v y=y.
x^ (y v (x v z))=x^ (x v z).
x^ (y v (x v z))=x.
(x^x) v x=x.
x^ ((y v x)^ (x v z))=x.
x^ (y v (x^ (x v z)))=x.
x^x=x.
x v x=x.
(x v y)^y=y.
x^ (y^x)=y^x.
(x v (((y^x) v (z^x))^u))^ (v v x)=x.
((x v y)^ (y v z))^y=y^ ((x v y)^ (y v z)).
(x v (x^y))^ (z v x)=x.
x v (((y^x) v (z^x))^u)=x.
((x v y)^ (y v z))^y=y.
(((x^y) v (z^y)) v (((x^y) v (z^y))^u))^y= (x^y) v (z^y).
(x^y)^x=x^y.
x v (((y^x) v x)^z)=x.
x v ((y^x)^z)=x.
((x^y) v y)^y= (x^y) v y.
x v (y^ (z^x))=x.
x v (y^ (x^z))=x.
(x^y) v y=y.
((x^y) v (z^y)) v y=y.
((x^y) v (y^z)) v y=y.
end_of_list.

