Needing help with call_with_depth_limit/3

Help! Predicate
78

LEM is not even derivable from RAA in intuitionistic logic.
Proof via provers.

  1. RAA is the classical double negation elimination rule that allows the derivation of the conditional in the following proof given by Michel Levy’s Prover :
1    assume --A.
2      A.                                                  Raa 1
3    therefore --A => A.                                   =>I 1,2
  1. It is provable via fCube that LEM is not derivable from RAA:
true
Input Formula:
F ((~~a => a) => (~a | a))
Sign Permanence tried,input formula equivalent to: 
F ((~~a => a) => (~a | a));
F->,Main SWFF: F ((~~a => a) => (a | ~a))
T (~~a => a);
F (a | ~a);

Main SWFF: F (a | ~a)
F a;
F ~a;
T (~~a => a);

F non,Main SWFF: F ~a
T a;

Found a backtacking point:

F ~a;
T (~~a => a);
F a;
 
Right branch of T->not,Main SWFF: T (~~a => a)
T a;
F 1;

Left branch of T->not,Main SWFF: T (~~a => a)
FC a;

1 search result = unprovable (fCube-4.1)
*** The Counter Model (see also the prolog term ) ***
-- root --
-- end world -- 
F a;
-- end world -- 
T a;
-- end world -- 
FC a;
-- end world --
*** Prolog term of the countermodel ***
[[swff(F,a),[swff(T,a)],[swff(FC,a)]]]
631.0 msec.