>PhoX> Sort term.
Sort term defined
>PhoX> Cst R : term  term  prop.
R : term  term  prop
>PhoX> Cst S : term  prop.
S : term  prop
>PhoX> def F = x R x x  x,y(R x y  R y x)  x,y,z(R x y  R y z  R x z).

F = x R x x  x,y (R x y  R y x)  x,y,z (R x y  R y z  R x z)
 : prop
>PhoX> def G = x,y (S x  (R x y  S y)).
G = x,y (S x  R x y  S y) : prop
>PhoX> def H = x S x  x(S x  y (S y  R x y)).

H = x S x  x:S  y (S y  R x y) : prop
>PhoX> goal F  (G H).
Here is the goal:
goal 1/1
    F  G  H

%PhoX% intro 3.
2 goals created.

goal 2/2
H0 := F
H1 := H
    G

goal 1/2
H0 := F
H1 := G
    H

%PhoX% intro.
1 goal created.

goal 1/2
H0 := F
H1 := G
H2 := x S x
    x:S  y (S y  R x y)

%PhoX% elim H2.
1 goal created.

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    x0:S  y (S y  R x0 y)

%PhoX% intro.
1 goal created.

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    S ?1  y (S y  R ?1 y)

%PhoX% instance ?1 x.
Here are the goals:
goal 2/2
H0 := F
H1 := H
    G

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    S x  y (S y  R x y)

%PhoX% intro .
2 goals created.

goal 2/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    y (S y  R x y)

goal 1/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    S x

%PhoX% axiom H3.
0 goal created.

goal 2/2
H0 := F
H1 := H
    G

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    y (S y  R x y)

%PhoX% intro 2.
2 goals created.

goal 2/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    R x y  S y

goal 1/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    S y  R x y

%PhoX% intro.
1 goal created.

goal 1/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
H4 := S y
    R x y

%PhoX% apply -2 (y) -3 H3 H1.
1 goal created.

goal 1/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
H4 := S y
G0 := R x y  S y
    R x y

%PhoX% elim G0.
1 goal created.

goal 1/3
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
H4 := S y
G0 := R x y  S y
    S y

%PhoX% axiom H4.
0 goal created.

goal 2/2
H0 := F
H1 := H
    G

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
    R x y  S y

%PhoX% intro.
1 goal created.

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
H4 := R x y
    S y

%PhoX% apply -2 (y) -3 H3 H1.
1 goal created.

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
H4 := R x y
G0 := R x y  S y
    S y

%PhoX% elim G0.
1 goal created.

goal 1/2
H0 := F
H1 := G
H2 := x0 S x0
H3 := S x
H4 := R x y
G0 := R x y  S y
    R x y

%PhoX% axiom H4.
0 goal created.

goal 1/1
H0 := F
H1 := H
    G

%PhoX% intro 3.
1 goal created.

goal 1/1
H0 := F
H1 := H
H2 := S x
    R x y  S y

%PhoX% use x(S x  y(S y  R x y)).
2 goals created.

goal 2/2
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 1/2
H0 := F
H1 := H
H2 := S x
G0 := x0:S  y0 (S y0  R x0 y0)
    R x y  S y

%PhoX% elim G0.
1 goal created.

goal 1/2
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0  y0 (S y0  R x0 y0)
    R x y  S y

%PhoX% left H3.
1 goal created.

goal 1/2
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x y  S y

%PhoX% use R x0 x.
2 goals created.

goal 2/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 1/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
    R x y  S y

%PhoX% intro 2.
2 goals created.

goal 2/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
    R x y

goal 1/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
    S y

%PhoX% elim H4.
1 goal created.

goal 1/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
    R x0 y

%PhoX% left H0.
1 goal created.

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H6 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x0 y

%PhoX% elim H6.
1 goal created.

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H6 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x0 ?2  R ?2 y

%PhoX% instance ?2 x.
Here are the goals:
goal 4/4
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 3/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 2/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
    R x y

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H6 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x0 x  R x y

%PhoX% intro.
2 goals created.

goal 2/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H6 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x y

goal 1/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H6 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x0 x

%PhoX% axiom G1.
0 goal created.

goal 4/4
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 3/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 2/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
    R x y

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := R x y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H6 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x y

%PhoX% axiom H5.
0 goal created.

goal 3/3
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 2/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 1/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
    R x y

%PhoX% elim H4.
1 goal created.

goal 1/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S ?3  R x0 ?3
H7 := R x0 ?3  S ?3
    R x y

%PhoX% instance ?3 y.
Here are the goals:
goal 3/3
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 2/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 1/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    R x y

%PhoX% use R x0 y.
2 goals created.

goal 2/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    R x0 y

goal 1/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
    R x y

%PhoX% left H0.
1 goal created.

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H0 := x1 R x1 x1  x1,y0 (R x1 y0  R y0 x1)
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
    R x y

%PhoX% left H0.
1 goal created.

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
    R x y

%PhoX% use R x x0.
2 goals created.

goal 2/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
    R x x0

goal 1/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
G3 := R x x0
    R x y

%PhoX% elim H8.
1 goal created.

goal 1/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
G3 := R x x0
    R x ?4  R ?4 y

%PhoX% instance ?4 x0.
Here are the goals:
goal 5/5
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 4/5
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 3/5
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    R x0 y

goal 2/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
    R x x0

goal 1/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
G3 := R x x0
    R x x0  R x0 y

%PhoX% intro.
2 goals created.

goal 2/6
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
G3 := R x x0
    R x0 y

goal 1/6
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
G3 := R x x0
    R x x0

%PhoX% axiom G3.
0 goal created.

goal 5/5
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 4/5
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 3/5
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    R x0 y

goal 2/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
    R x x0

goal 1/5
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
G3 := R x x0
    R x0 y

%PhoX% axiom G2.
0 goal created.

goal 4/4
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 3/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 2/4
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    R x0 y

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
    R x x0

%PhoX% elim H9.
1 goal created.

goal 1/4
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
G2 := R x0 y
H8 := x1,y0,z (R x1 y0  R y0 z  R x1 z)
H0 := x1 R x1 x1
H9 := x1,y0 (R x1 y0  R y0 x1)
    R x0 x

%PhoX% axiom G1.
0 goal created.

goal 3/3
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 2/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

goal 1/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    R x0 y

%PhoX% elim H6.
1 goal created.

goal 1/3
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
G1 := R x0 x
H5 := S y
H6 := S y  R x0 y
H7 := R x0 y  S y
    S y

%PhoX% axiom H5.
0 goal created.

goal 2/2
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

goal 1/2
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    R x0 x

%PhoX% elim H4.
1 goal created.

goal 1/2
H0 := F
H1 := H
H2 := S x
G0 := x1:S  y0 (S y0  R x1 y0)
H3 := S x0
H4 := y0 (S y0  R x0 y0)
    S x

%PhoX% axiom H2.
0 goal created.

goal 1/1
H0 := F
H1 := H
H2 := S x
    x0:S  y0 (S y0  R x0 y0)

%PhoX% elim H1.
1 goal created.

goal 1/1
H0 := F
H1 := H
H2 := S x
    x0 S x0

%PhoX% intro.
1 goal created.

goal 1/1
H0 := F
H1 := H
H2 := S x
    S ?5

%PhoX% axiom H2.
0 goal created.

%PhoX% save th.
Building proof .... 
Typing proof .... 
Verifying proof .... 
Saving proof ....
th = F  G  H : theorem

bye