set(hyper_res).
set(ur_res).
set(prolog_style_variables).
set(output_sequent).
clear(print_kept).
clear(print_given).
clear(print_back_sub).
assign(max_proofs,5).


%E represents equality, R the step relation, S the paths

formula_list(sos).

%reflexivity, symmetry and transitivity of E 
all X E(X,X).
all X Y (E(X,Y) -> E(Y,X)).
all X Y Z (E(X,Y) & E(Y,Z) -> E(X,Z)). %not needed!

%S includes E and R and is transitive
all X Y (E(X,Y) -> S(X,Y)).
all X Y (R(X,Y) -> S(X,Y)). %not needed!
all X Y Z (S(X,Y) & S(Y,Z) -> S(X,Z)).

%any path has either length 0 or starts with a step
all X Y (S(X,Y) -> (E(X,Y) | (exists I ( R(X,I) & S(I,Y))))).

%local confluence
all X Y Z (R(X,Y) & R(X,Z) -> (exists J (S(Y,J) & S(Z,J)))).

%IH: we have confluence any step beyond a 
all X Y Z (R(a,X) & S(X,Y) & S(X,Z) -> (exists J (S(Y,J) & S(Z,J)))). 

S(a,b).
S(a,c).
-(exists J (S(b,J) & S(c,J))).

end_of_list.