Result of llprover

You are the 4-th user of this script.

System: CLL
Formula: []-->all(X,all(Y,p(X,Y))->exists(Z,p(X,Z)))
Output style: twosided, pretty

--------------------- Ax
p(X1,Y1) --> p(X1,Y1)
------------------------------ Rexists
p(X1,Y1) --> exists(Z,p(X1,Z))
------------------------------------ Lall
all(Y,p(X1,Y)) --> exists(Z,p(X1,Z))
-------------------------------------- R->
 --> all(Y,p(X1,Y))->exists(Z,p(X1,Z))
------------------------------------------- Rall
 --> all(X,all(Y,p(X,Y))->exists(Z,p(X,Z)))

CPU Time = 249 msec.

Naoyuki Tamura