15:- assert(prolog(swi)).  % Prolog dialect: eclipse, sicstus, swi
   16:- dynamic(axiom_path/1).   17
   18
   19% execute predicates specific to Prolog dialect
   20
   21:- \+ prolog(eclipse) -> true ;
   22   nodbgcomp,        % switch off debugging mode
   23   set_flag(print_depth,10000),  % set print depth
   24   set_flag(variable_names,off),
   25   ( getenv('TPTP',Path) -> Path1=Path ; Path1='' ),
   26   retract_all(axiom_path(_)), assert(axiom_path(Path1)),
   27   [leancop21].      % load leanCoP core prover
   28
   29:- \+ prolog(sicstus) -> true ;
   30   use_module(library(system)),  % load system module
   31   ( environ('TPTP',Path) -> Path1=Path ; Path1='' ),
   32   retractall(axiom_path(_)), assert(axiom_path(Path1)),
   33   [leancop21_sic].  % load leanCoP core prover
   34
   35:- prolog(Dialect), Dialect\=swi -> true ;
   36   set_prolog_flag(optimise,true),  % optimise compilation
   37   ( getenv('TPTP',Path) -> Path1=Path ; Path1='' ),
   38   retractall(axiom_path(_)), assert(axiom_path(Path1)),
   39   [leancop21_swi].  % load leanCoP core prover
   40
   41
   42% load additional leanCoP components
   43
   44:- [leancop_proof].  % load program for proof presentation
   45:- [leancop_tptp2].  % load program for TPTP input syntax
   46
   47
   48%%% call leanCoP core prover
   49
   50leancop_main(File,Settings,Result) :-
   51    axiom_path(AxPath), ( AxPath='' -> AxDir='' ;
   52    name(AxPath,AxL), append(AxL,[47],DirL), name(AxDir,DirL) ),
   53    ( leancop_tptp2(File,AxDir,[_],F,Conj) ->
   54      Problem=F ; [File], f(Problem), Conj=non_empty ),
   55    ( Conj\=[] -> Problem1=Problem ; Problem1=(~Problem) ),
   56    leancop_equal(Problem1,Problem2),
   57    make_matrix(Problem2,Matrix,Settings),
   58    ( prove2(Matrix,Settings,Proof) ->
   59      ( Conj\=[] -> Result='Theorem' ; Result='Unsatisfiable' ) ;
   60      ( Conj\=[] -> Result='Non-Theorem' ; Result='Satisfiable' )
   61    ),
   62    output_result(File,Matrix,Proof,Result,Conj).
   63
   64% print status and connection proof
   65
   66output_result(File,Matrix,Proof,Result,Conj) :-
   67    ( Conj\=[] -> Art=' is a ' ; Art=' is ' ), nl,
   68    print(File), print(Art), print(Result), nl,
   69    Proof=[] -> true ; ( Result='Theorem' -> Out=' for ' ;
   70      Result='Unsatisfiable' -> Out=' for negated ' ; true ),
   71    ( var(Out) -> true ; print('Start of proof'), print(Out),
   72      print(File), nl, leancop_proof(Matrix,Proof),
   73      print('End of proof'), print(Out), print(File), nl ).
   74
   75:- break.