% --------------------------------------------------------------------------
% In Whitehead and Russell's 5-basis for PC, WR5 is dependent on WR1 .. WR4.
% --------------------------------------------------------------------------

op(400,infix,[v,"->"]).
op(200,prefix,[~]).

clear(auto_inference).
set(hyper_resolution).

formulas(usable).

   -P(x -> y) | -P(x) | P(y) # label("MP").

end_of_list.

formulas(sos).

   % Definition:  x -> y = ~x v y
   P((x -> y) -> (~x v y)) # label("-> Def, part a").
   P((~x v y) -> (x -> y)) # label("-> Def, part b").

   % WR axioms WR1 .. WR4
   P((x v x) -> x) # label("WR1").
   P(y -> (x v y)) # label("WR2").
   P((x v y) -> (y v x)) # label("WR3").
   P((y -> z) -> ((x v y) -> (x v z))) # label("WR4").

end_of_list.

formulas(goals).

   P((x v (y v z)) -> (y v (x v z))) # label("WR5").

end_of_list.

%
% Hints extracted from previously found proofs.
%

formulas(hints).

P((x v (y v z)) -> (y v (x v z))).
P((x v x) -> x).
P(x -> (y v x)).
P((x v y) -> (y v x)).
P((x -> y) -> ((z v x) -> (z v y))).
P((x -> y) -> (~ x v y)).
P((~ x v y) -> (x -> y)).
-P((c1 v (c2 v c3)) -> (c2 v (c1 v c3))).
P((x v (y -> z)) -> (x v ((u v y) -> (u v z)))).
P((x v (y v z)) -> (x v (z v y))).
P((x v y) -> (x v (z v y))).
P((x v (y v y)) -> (x v y)).
P(~ (x -> y) v (~ x v y)).
P((x v (y -> z)) -> (x v (~ y v z))).
P(~ (x v y) v (y v x)).
P(~ x v (y v x)).
P((x v (~ y v z)) -> (x v (y -> z))).
P((x v (y v z)) -> (x v (y v (u v z)))).
P(~ x v x).
P(x v ~ x).
P(x v (y v ~ x)).
P(~ (x v (y v z)) v (x v (z v y))).
P((x v (y v (z v u))) -> (x v (y v (u v z)))).
P(x v (~ x v y)).
P(~ x v (x v y)).
P((~ x v y) v x).
P(x -> (x v y)).
P((x v y) -> (x v (y v z))).
P((x v (y v z)) -> (x v (y v (z v u)))).
P((x v (y v (~ z v u))) -> (x v (y v (z -> u)))).
P(~ (x v ~ y) v (y -> x)).
P((x v ~ y) -> (y -> x)).
P((~ (x v y) v z) v (x v (u v y))).
P(~ (x v y) v (y v (z v x))).
P(~ (x v (y v x)) v (y v x)).
P(~ (x v y) v ((z v x) v y)).
P(~ (x v (~ y v x)) v (y -> x)).
P((x v (y v x)) -> (y v x)).
P(x v (~ (x v y) v y)).
P(x v ((x v y) -> y)).
P(x v ((y v (x v z)) -> (y v z))).
P(x v (~ (y v (x v z)) v (y v z))).
P(((x v (y v z)) -> (x v z)) v y).
P(((x v (y v z)) -> (x v z)) v (y v u)).
P(~ (x v (y v z)) v ((z v y) v x)).
P(~ (x v (y v z)) v ((u v x) v (z v y))).
P(~ (x -> (y v z)) v (~ x v (z v y))).
P(x v (~ (x v y) v (y v z))).
P((x v (~ y v x)) -> (y -> x)).
P(x v (~ (x v y) v (z v (y v u)))).
P(x v (~ (x v y) v (z -> (y v u)))).
P(((x -> (y v z)) v y) -> (x -> (y v z))).
P(((x v y) v (x v z)) -> ((x v y) v z)).
P((x v ((y v z) v (y v u))) -> (x v ((y v z) v u))).
P(~ (x v (y v z)) v ((y v x) v z)).
P((x v (y v z)) -> ((z v y) v x)).
P((x v (y v z)) v ~ (z v (y v x))).
P(~ (x v (y v z)) v ((z v x) v y)).
P(~ (x -> (y v z)) v (x -> (z v y))).
P((x v (y v z)) -> (z v (y v x))).
P((x v y) v (~ (x v (z v y)) v z)).
P((x v (y v z)) -> ((z v x) v y)).
P((x -> (y v z)) -> (x -> (z v y))).
P((x v (y v z)) -> (y v (z v x))).
P(~ (x v (y v z)) v (y v (x v z))).

end_of_list.
