%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n002.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:07:55 PM UTC 2026
% Result : Theorem 0.15s 0.45s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 30
% Syntax : Number of formulae : 104 ( 32 unt; 16 def)
% Number of atoms : 246 ( 5 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 228 ( 86 ~; 96 |; 22 &)
% ( 21 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 27 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 54 ( 45 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,axiom,
implies_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
and_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
and_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
or_1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
or_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f51,axiom,
( modus_ponens_strict_implies
<=> ! [X,Y] :
( ( is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f55,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f75,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f79,axiom,
axiom_K,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f80,axiom,
axiom_M,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
op_strict_implies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,conjecture,
modus_ponens_strict_implies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
~ modus_ponens_strict_implies,
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f90,plain,
( modus_ponens
<=> ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f91,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
| modus_ponens )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens ) ),
inference(NNF_transformation,[status(thm)],[f90]) ).
fof(f92,plain,
( ( ? [Y] :
( ~ is_a_theorem(Y)
& ? [X] :
( is_a_theorem(implies(X,Y))
& is_a_theorem(X) ) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(miniscoping,[status(thm)],[f91]) ).
fof(f93,plain,
( ( ( ~ is_a_theorem(sK0_skl)
& is_a_theorem(implies(sK1_skl,sK0_skl))
& is_a_theorem(sK1_skl) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl),skolemize(X,sK1_skl)],[f92]) ).
fof(f94,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f213,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f215,plain,
implies_1,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f218,plain,
and_1,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f219,plain,
and_2,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f221,plain,
or_1,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f222,plain,
or_2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f234,plain,
( modus_ponens_strict_implies
<=> ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f51]) ).
fof(f235,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) )
| modus_ponens_strict_implies )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens_strict_implies ) ),
inference(NNF_transformation,[status(thm)],[f234]) ).
fof(f236,plain,
( ( ? [Y] :
( ~ is_a_theorem(Y)
& ? [X] :
( is_a_theorem(strict_implies(X,Y))
& is_a_theorem(X) ) )
| modus_ponens_strict_implies )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens_strict_implies ) ),
inference(miniscoping,[status(thm)],[f235]) ).
fof(f237,plain,
( ( ( ~ is_a_theorem(sK56_skl)
& is_a_theorem(strict_implies(sK57_skl,sK56_skl))
& is_a_theorem(sK57_skl) )
| modus_ponens_strict_implies )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(strict_implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens_strict_implies ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK56_skl,sK57_skl]),skolemize(Y,sK56_skl),skolemize(X,sK57_skl)],[f236]) ).
fof(f239,plain,
( is_a_theorem(sK57_skl)
| modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f240,plain,
( is_a_theorem(strict_implies(sK57_skl,sK56_skl))
| modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f241,plain,
( ~ is_a_theorem(sK56_skl)
| modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f237]) ).
fof(f259,plain,
( ( ? [X] : ~ is_a_theorem(implies(necessarily(X),X))
| axiom_M )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f260,plain,
( ( ~ is_a_theorem(implies(necessarily(sK64_skl),sK64_skl))
| axiom_M )
& ( ! [X] : is_a_theorem(implies(necessarily(X),X))
| ~ axiom_M ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK64_skl]),skolemize(X,sK64_skl)],[f259]) ).
fof(f261,plain,
! [X0] :
( is_a_theorem(implies(necessarily(X0),X0))
| ~ axiom_M ),
inference(cnf_transformation,[status(thm)],[f260]) ).
fof(f335,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f336,plain,
! [X0,X1] :
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[status(thm)],[f335]) ).
fof(f341,plain,
axiom_K,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f342,plain,
axiom_M,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f347,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f350,plain,
~ modus_ponens_strict_implies,
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f351,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f353,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f351]) ).
fof(f354,definition,
! [X0,X1] :
( sQ1_spl
<=> ( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f355,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f354]) ).
fof(f357,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f94,f351,f354]) ).
fof(f396,definition,
( sQ12_spl
<=> implies_1 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f398,plain,
( sQ12_spl
| ~ implies_1 ),
inference(component_clause,[status(thm)],[f396]) ).
fof(f429,definition,
( sQ21_spl
<=> and_1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f431,plain,
( sQ21_spl
| ~ and_1 ),
inference(component_clause,[status(thm)],[f429]) ).
fof(f440,definition,
( sQ24_spl
<=> and_2 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f442,plain,
( sQ24_spl
| ~ and_2 ),
inference(component_clause,[status(thm)],[f440]) ).
fof(f462,definition,
( sQ30_spl
<=> or_1 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f464,plain,
( sQ30_spl
| ~ or_1 ),
inference(component_clause,[status(thm)],[f462]) ).
fof(f473,definition,
( sQ33_spl
<=> or_2 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f475,plain,
( sQ33_spl
| ~ or_2 ),
inference(component_clause,[status(thm)],[f473]) ).
fof(f690,definition,
( sQ92_spl
<=> modus_ponens_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f691,plain,
( ~ sQ92_spl
| modus_ponens_strict_implies ),
inference(component_clause,[status(thm)],[f690]) ).
fof(f697,definition,
( sQ94_spl
<=> is_a_theorem(sK57_skl) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f700,plain,
( sQ94_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f239,f690,f697]) ).
fof(f701,definition,
( sQ95_spl
<=> is_a_theorem(strict_implies(sK57_skl,sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( ~ sQ95_spl
| is_a_theorem(strict_implies(sK57_skl,sK56_skl)) ),
inference(component_clause,[status(thm)],[f701]) ).
fof(f704,plain,
( sQ95_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f240,f690,f701]) ).
fof(f705,definition,
( sQ96_spl
<=> is_a_theorem(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f708,plain,
( ~ sQ96_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f241,f690,f705]) ).
fof(f743,definition,
( sQ106_spl
<=> axiom_K ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f745,plain,
( sQ106_spl
| ~ axiom_K ),
inference(component_clause,[status(thm)],[f743]) ).
fof(f754,definition,
( sQ109_spl
<=> axiom_M ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f756,plain,
( sQ109_spl
| ~ axiom_M ),
inference(component_clause,[status(thm)],[f754]) ).
fof(f757,definition,
! [X0] :
( sQ110_spl
<=> is_a_theorem(implies(necessarily(X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f758,plain,
! [X0] :
( ~ sQ110_spl
| is_a_theorem(implies(necessarily(X0),X0)) ),
inference(component_clause,[status(thm)],[f757]) ).
fof(f760,plain,
( sQ110_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f261,f754,f757]) ).
fof(f966,definition,
( sQ167_spl
<=> op_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f968,plain,
( sQ167_spl
| ~ op_strict_implies ),
inference(component_clause,[status(thm)],[f966]) ).
fof(f969,definition,
! [X0,X1] :
( sQ168_spl
<=> strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f970,plain,
! [X0,X1] :
( ~ sQ168_spl
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(component_clause,[status(thm)],[f969]) ).
fof(f972,plain,
( sQ168_spl
| ~ sQ167_spl ),
inference(split_clause,[status(thm)],[f336,f966,f969]) ).
fof(f980,plain,
( ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f691,f350]) ).
fof(f981,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f980]) ).
fof(f984,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f968,f347]) ).
fof(f985,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f984]) ).
fof(f994,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f353,f213]) ).
fof(f995,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f994]) ).
fof(f1006,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f756,f342]) ).
fof(f1007,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f1006]) ).
fof(f1035,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f475,f222]) ).
fof(f1036,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1035]) ).
fof(f1043,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f431,f218]) ).
fof(f1044,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1043]) ).
fof(f1049,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f464,f221]) ).
fof(f1050,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1049]) ).
fof(f1053,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f442,f219]) ).
fof(f1054,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1053]) ).
fof(f1057,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f398,f215]) ).
fof(f1058,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1057]) ).
fof(f1073,plain,
! [X0] :
( ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0)) ),
inference(resolution,[status(thm)],[f355,f758]) ).
fof(f1085,plain,
! [X0,X1] :
( ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(strict_implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f970,f1073]) ).
fof(f1171,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f745,f341]) ).
fof(f1172,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1171]) ).
fof(f1187,plain,
( ~ sQ95_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(implies(sK57_skl,sK56_skl)) ),
inference(resolution,[status(thm)],[f1085,f702]) ).
fof(f1193,plain,
( ~ sQ95_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(sK56_skl)
| ~ is_a_theorem(sK57_skl) ),
inference(resolution,[status(thm)],[f355,f1187]) ).
fof(f1204,plain,
( ~ sQ95_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| sQ96_spl
| ~ sQ94_spl ),
inference(split_clause,[status(thm)],[f1193,f697,f705,f354,f757,f969,f701]) ).
fof(f1206,plain,
$false,
inference(sat_refutation,[status(thm)],[f357,f700,f704,f708,f760,f972,f981,f985,f995,f1007,f1036,f1044,f1050,f1054,f1058,f1172,f1204]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL525+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 00:40:02 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.39 % Drodi V4.1.1
% 0.15/0.45 % Refutation found
% 0.15/0.45 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.15/0.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.19/0.53 % Elapsed time: 0.156065 seconds
% 0.19/0.53 % CPU time: 0.254040 seconds
% 0.19/0.53 % Total memory used: 32.622 MB
% 0.19/0.53 % Net memory used: 32.508 MB
%------------------------------------------------------------------------------