%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL538+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.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:57 PM UTC 2026
% Result : Theorem 0.09s 0.41s
% Output : CNFRefutation 0.09s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 32
% Syntax : Number of formulae : 110 ( 35 unt; 17 def)
% Number of atoms : 255 ( 5 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 232 ( 87 ~; 98 |; 22 &)
% ( 22 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 31 ( 29 usr; 29 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/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
implies_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
and_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f41,axiom,
and_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
or_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
or_2,
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p') ).
fof(f55,axiom,
( axiom_M
<=> ! [X] : is_a_theorem(implies(necessarily(X),X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f75,axiom,
( op_strict_implies
=> ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f79,axiom,
axiom_K,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f80,axiom,
axiom_M,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f82,axiom,
axiom_B,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f86,axiom,
op_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f89,conjecture,
modus_ponens_strict_implies,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f90,negated_conjecture,
~ modus_ponens_strict_implies,
inference(negated_conjecture,[status(cth)],[f89]) ).
fof(f91,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(f92,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)],[f91]) ).
fof(f93,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)],[f92]) ).
fof(f94,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)],[f93]) ).
fof(f95,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f94]) ).
fof(f214,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f216,plain,
implies_1,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f219,plain,
and_1,
inference(cnf_transformation,[status(thm)],[f40]) ).
fof(f220,plain,
and_2,
inference(cnf_transformation,[status(thm)],[f41]) ).
fof(f222,plain,
or_1,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f223,plain,
or_2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f235,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(f236,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)],[f235]) ).
fof(f237,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)],[f236]) ).
fof(f238,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)],[f237]) ).
fof(f240,plain,
( is_a_theorem(sK57_skl)
| modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f241,plain,
( is_a_theorem(strict_implies(sK57_skl,sK56_skl))
| modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f242,plain,
( ~ is_a_theorem(sK56_skl)
| modus_ponens_strict_implies ),
inference(cnf_transformation,[status(thm)],[f238]) ).
fof(f260,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(f261,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)],[f260]) ).
fof(f262,plain,
! [X0] :
( is_a_theorem(implies(necessarily(X0),X0))
| ~ axiom_M ),
inference(cnf_transformation,[status(thm)],[f261]) ).
fof(f336,plain,
( ! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y))
| ~ op_strict_implies ),
inference(pre_NNF_transformation,[status(thm)],[f75]) ).
fof(f337,plain,
! [X0,X1] :
( strict_implies(X0,X1) = necessarily(implies(X0,X1))
| ~ op_strict_implies ),
inference(cnf_transformation,[status(thm)],[f336]) ).
fof(f342,plain,
axiom_K,
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f343,plain,
axiom_M,
inference(cnf_transformation,[status(thm)],[f80]) ).
fof(f345,plain,
axiom_B,
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f349,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f86]) ).
fof(f352,plain,
~ modus_ponens_strict_implies,
inference(cnf_transformation,[status(thm)],[f90]) ).
fof(f353,definition,
( sQ0_spl
<=> modus_ponens ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f355,plain,
( sQ0_spl
| ~ modus_ponens ),
inference(component_clause,[status(thm)],[f353]) ).
fof(f356,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(f357,plain,
! [X0,X1] :
( ~ sQ1_spl
| is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f356]) ).
fof(f359,plain,
( sQ1_spl
| ~ sQ0_spl ),
inference(split_clause,[status(thm)],[f95,f353,f356]) ).
fof(f398,definition,
( sQ12_spl
<=> implies_1 ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f400,plain,
( sQ12_spl
| ~ implies_1 ),
inference(component_clause,[status(thm)],[f398]) ).
fof(f431,definition,
( sQ21_spl
<=> and_1 ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f433,plain,
( sQ21_spl
| ~ and_1 ),
inference(component_clause,[status(thm)],[f431]) ).
fof(f442,definition,
( sQ24_spl
<=> and_2 ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f444,plain,
( sQ24_spl
| ~ and_2 ),
inference(component_clause,[status(thm)],[f442]) ).
fof(f464,definition,
( sQ30_spl
<=> or_1 ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f466,plain,
( sQ30_spl
| ~ or_1 ),
inference(component_clause,[status(thm)],[f464]) ).
fof(f475,definition,
( sQ33_spl
<=> or_2 ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f477,plain,
( sQ33_spl
| ~ or_2 ),
inference(component_clause,[status(thm)],[f475]) ).
fof(f692,definition,
( sQ92_spl
<=> modus_ponens_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ92_spl])],[split_symbol_definition]) ).
fof(f693,plain,
( ~ sQ92_spl
| modus_ponens_strict_implies ),
inference(component_clause,[status(thm)],[f692]) ).
fof(f699,definition,
( sQ94_spl
<=> is_a_theorem(sK57_skl) ),
introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition]) ).
fof(f702,plain,
( sQ94_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f240,f692,f699]) ).
fof(f703,definition,
( sQ95_spl
<=> is_a_theorem(strict_implies(sK57_skl,sK56_skl)) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f704,plain,
( ~ sQ95_spl
| is_a_theorem(strict_implies(sK57_skl,sK56_skl)) ),
inference(component_clause,[status(thm)],[f703]) ).
fof(f706,plain,
( sQ95_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f241,f692,f703]) ).
fof(f707,definition,
( sQ96_spl
<=> is_a_theorem(sK56_skl) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f710,plain,
( ~ sQ96_spl
| sQ92_spl ),
inference(split_clause,[status(thm)],[f242,f692,f707]) ).
fof(f745,definition,
( sQ106_spl
<=> axiom_K ),
introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition]) ).
fof(f747,plain,
( sQ106_spl
| ~ axiom_K ),
inference(component_clause,[status(thm)],[f745]) ).
fof(f756,definition,
( sQ109_spl
<=> axiom_M ),
introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition]) ).
fof(f758,plain,
( sQ109_spl
| ~ axiom_M ),
inference(component_clause,[status(thm)],[f756]) ).
fof(f759,definition,
! [X0] :
( sQ110_spl
<=> is_a_theorem(implies(necessarily(X0),X0)) ),
introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition]) ).
fof(f760,plain,
! [X0] :
( ~ sQ110_spl
| is_a_theorem(implies(necessarily(X0),X0)) ),
inference(component_clause,[status(thm)],[f759]) ).
fof(f762,plain,
( sQ110_spl
| ~ sQ109_spl ),
inference(split_clause,[status(thm)],[f262,f756,f759]) ).
fof(f778,definition,
( sQ115_spl
<=> axiom_B ),
introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition]) ).
fof(f780,plain,
( sQ115_spl
| ~ axiom_B ),
inference(component_clause,[status(thm)],[f778]) ).
fof(f968,definition,
( sQ167_spl
<=> op_strict_implies ),
introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition]) ).
fof(f970,plain,
( sQ167_spl
| ~ op_strict_implies ),
inference(component_clause,[status(thm)],[f968]) ).
fof(f971,definition,
! [X0,X1] :
( sQ168_spl
<=> strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition]) ).
fof(f972,plain,
! [X0,X1] :
( ~ sQ168_spl
| strict_implies(X0,X1) = necessarily(implies(X0,X1)) ),
inference(component_clause,[status(thm)],[f971]) ).
fof(f974,plain,
( sQ168_spl
| ~ sQ167_spl ),
inference(split_clause,[status(thm)],[f337,f968,f971]) ).
fof(f982,plain,
( ~ sQ92_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f693,f352]) ).
fof(f983,plain,
~ sQ92_spl,
inference(contradiction_clause,[status(thm)],[f982]) ).
fof(f986,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f970,f349]) ).
fof(f987,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f986]) ).
fof(f996,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f355,f214]) ).
fof(f997,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f996]) ).
fof(f1008,plain,
( sQ109_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f758,f343]) ).
fof(f1009,plain,
sQ109_spl,
inference(contradiction_clause,[status(thm)],[f1008]) ).
fof(f1031,plain,
( sQ115_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f780,f345]) ).
fof(f1032,plain,
sQ115_spl,
inference(contradiction_clause,[status(thm)],[f1031]) ).
fof(f1039,plain,
( sQ33_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f477,f223]) ).
fof(f1040,plain,
sQ33_spl,
inference(contradiction_clause,[status(thm)],[f1039]) ).
fof(f1047,plain,
( sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f433,f219]) ).
fof(f1048,plain,
sQ21_spl,
inference(contradiction_clause,[status(thm)],[f1047]) ).
fof(f1053,plain,
( sQ30_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f466,f222]) ).
fof(f1054,plain,
sQ30_spl,
inference(contradiction_clause,[status(thm)],[f1053]) ).
fof(f1057,plain,
( sQ24_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f444,f220]) ).
fof(f1058,plain,
sQ24_spl,
inference(contradiction_clause,[status(thm)],[f1057]) ).
fof(f1061,plain,
( sQ12_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f400,f216]) ).
fof(f1062,plain,
sQ12_spl,
inference(contradiction_clause,[status(thm)],[f1061]) ).
fof(f1077,plain,
! [X0] :
( ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(X0)
| ~ is_a_theorem(necessarily(X0)) ),
inference(resolution,[status(thm)],[f357,f760]) ).
fof(f1090,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)],[f972,f1077]) ).
fof(f1177,plain,
( sQ106_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f747,f342]) ).
fof(f1178,plain,
sQ106_spl,
inference(contradiction_clause,[status(thm)],[f1177]) ).
fof(f1194,plain,
( ~ sQ95_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(implies(sK57_skl,sK56_skl)) ),
inference(resolution,[status(thm)],[f1090,f704]) ).
fof(f1205,plain,
( ~ sQ95_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| is_a_theorem(sK56_skl)
| ~ is_a_theorem(sK57_skl) ),
inference(resolution,[status(thm)],[f357,f1194]) ).
fof(f1217,plain,
( ~ sQ95_spl
| ~ sQ168_spl
| ~ sQ110_spl
| ~ sQ1_spl
| sQ96_spl
| ~ sQ94_spl ),
inference(split_clause,[status(thm)],[f1205,f699,f707,f356,f759,f971,f703]) ).
fof(f1219,plain,
$false,
inference(sat_refutation,[status(thm)],[f359,f702,f706,f710,f762,f974,f983,f987,f997,f1009,f1032,f1040,f1048,f1054,f1058,f1062,f1178,f1217]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL538+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n017.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 00:32:56 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 0.09/0.41 % Refutation found
% 0.09/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.09/0.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.09/0.44 % Elapsed time: 0.056535 seconds
% 0.09/0.44 % CPU time: 0.217348 seconds
% 0.09/0.44 % Total memory used: 89.232 MB
% 0.09/0.44 % Net memory used: 89.123 MB
%------------------------------------------------------------------------------