Jans

pkif :-

        [ implies,

          [ isa(F, tPred),
            isa(A, ftInt),
            poss(KB, POS([arity(F, A)])),
            poss(KB, arity(F, A))
          ],
          =>,

          [ all[F],

            [ implies,
              [isa(F, tPred), ex[A], isa(A, ftInt), poss(KB, arity(F, A))],
              =>,
              [ex[A], [isa(A, ftInt), arity(F, A)]]
            ]
          ]
        ].




Okefs

rok_portray_clause((
|    pkif :-
|
|            [ implies,
|
|              [ isa(F, tPred),
|                isa(A, ftInt),
|                poss(KB, POS([arity(F, A)])),
|                poss(KB, arity(F, A))
|              ],
|              =>,
|
|              [ all[F],
|
|                [ implies,
|                  [isa(F, tPred), ex[A], isa(A, ftInt), poss(KB, arity(F, A))],
|                  =>,
|                  [ex[A], [isa(A, ftInt), arity(F, A)]]
|                ]
|              ]
|            ])).
pkif :-
        [implies,[isa(_G3891,tPred),isa(_G3897,ftInt),poss(_G3911,POS([arity(_G3891,_G3897)])),poss(_G3911,arity(_G3891,_G3897))],(=>),[all[_G3891],[implies,[isa(_G3891,tPred),ex[_G3897],isa(_G3897,ftInt),poss(_G3911,arity(_G3891,_G3897))],(=>),[ex[_G3897],[isa(_G3897,ftInt),arity(_G3891,_G3897)]]]]].