%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL536+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 : n007.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:56 PM UTC 2026
% Result : Theorem 0.03s 0.40s
% Output : CNFRefutation 0.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 16
% Syntax : Number of formulae : 58 ( 14 unt; 8 def)
% Number of atoms : 132 ( 5 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 125 ( 51 ~; 52 |; 8 &)
% ( 12 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 15 ( 13 usr; 13 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 31 ( 28 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f50,axiom,
( necessitation
<=> ! [X] :
( is_a_theorem(X)
=> is_a_theorem(necessarily(X)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f58,axiom,
( axiom_5
<=> ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f72,axiom,
( axiom_m10
<=> ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(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(f78,axiom,
necessitation,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f81,axiom,
axiom_5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f85,axiom,
op_strict_implies,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f88,conjecture,
axiom_m10,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f89,negated_conjecture,
~ axiom_m10,
inference(negated_conjecture,[status(cth)],[f88]) ).
fof(f228,plain,
( necessitation
<=> ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f50]) ).
fof(f229,plain,
( ( ? [X] :
( ~ is_a_theorem(necessarily(X))
& is_a_theorem(X) )
| necessitation )
& ( ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) )
| ~ necessitation ) ),
inference(NNF_transformation,[status(thm)],[f228]) ).
fof(f230,plain,
( ( ( ~ is_a_theorem(necessarily(sK55_skl))
& is_a_theorem(sK55_skl) )
| necessitation )
& ( ! [X] :
( is_a_theorem(necessarily(X))
| ~ is_a_theorem(X) )
| ~ necessitation ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(X,sK55_skl)],[f229]) ).
fof(f231,plain,
! [X0] :
( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0)
| ~ necessitation ),
inference(cnf_transformation,[status(thm)],[f230]) ).
fof(f271,plain,
( ( ? [X] : ~ is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| axiom_5 )
& ( ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(NNF_transformation,[status(thm)],[f58]) ).
fof(f272,plain,
( ( ~ is_a_theorem(implies(possibly(sK67_skl),necessarily(possibly(sK67_skl))))
| axiom_5 )
& ( ! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_5 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl]),skolemize(X,sK67_skl)],[f271]) ).
fof(f273,plain,
! [X0] :
( is_a_theorem(implies(possibly(X0),necessarily(possibly(X0))))
| ~ axiom_5 ),
inference(cnf_transformation,[status(thm)],[f272]) ).
fof(f327,plain,
( ( ? [X] : ~ is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| axiom_m10 )
& ( ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_m10 ) ),
inference(NNF_transformation,[status(thm)],[f72]) ).
fof(f328,plain,
( ( ~ is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl))))
| axiom_m10 )
& ( ! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))
| ~ axiom_m10 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK93_skl]),skolemize(X,sK93_skl)],[f327]) ).
fof(f330,plain,
( ~ is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl))))
| axiom_m10 ),
inference(cnf_transformation,[status(thm)],[f328]) ).
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(f340,plain,
necessitation,
inference(cnf_transformation,[status(thm)],[f78]) ).
fof(f343,plain,
axiom_5,
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f347,plain,
op_strict_implies,
inference(cnf_transformation,[status(thm)],[f85]) ).
fof(f350,plain,
~ axiom_m10,
inference(cnf_transformation,[status(thm)],[f89]) ).
fof(f675,definition,
( sQ88_spl
<=> necessitation ),
introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition]) ).
fof(f677,plain,
( sQ88_spl
| ~ necessitation ),
inference(component_clause,[status(thm)],[f675]) ).
fof(f678,definition,
! [X0] :
( sQ89_spl
<=> ( is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) ) ),
introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition]) ).
fof(f679,plain,
! [X0] :
( ~ sQ89_spl
| is_a_theorem(necessarily(X0))
| ~ is_a_theorem(X0) ),
inference(component_clause,[status(thm)],[f678]) ).
fof(f681,plain,
( sQ89_spl
| ~ sQ88_spl ),
inference(split_clause,[status(thm)],[f231,f675,f678]) ).
fof(f787,definition,
( sQ118_spl
<=> axiom_5 ),
introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition]) ).
fof(f789,plain,
( sQ118_spl
| ~ axiom_5 ),
inference(component_clause,[status(thm)],[f787]) ).
fof(f790,definition,
! [X0] :
( sQ119_spl
<=> is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f791,plain,
! [X0] :
( ~ sQ119_spl
| is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))) ),
inference(component_clause,[status(thm)],[f790]) ).
fof(f793,plain,
( sQ119_spl
| ~ sQ118_spl ),
inference(split_clause,[status(thm)],[f273,f787,f790]) ).
fof(f941,definition,
( sQ160_spl
<=> axiom_m10 ),
introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition]) ).
fof(f942,plain,
( ~ sQ160_spl
| axiom_m10 ),
inference(component_clause,[status(thm)],[f941]) ).
fof(f948,definition,
( sQ162_spl
<=> is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))) ),
introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition]) ).
fof(f950,plain,
( sQ162_spl
| ~ is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))) ),
inference(component_clause,[status(thm)],[f948]) ).
fof(f951,plain,
( ~ sQ162_spl
| sQ160_spl ),
inference(split_clause,[status(thm)],[f330,f941,f948]) ).
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(f984,plain,
( sQ88_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f677,f340]) ).
fof(f985,plain,
sQ88_spl,
inference(contradiction_clause,[status(thm)],[f984]) ).
fof(f988,plain,
( sQ167_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f968,f347]) ).
fof(f989,plain,
sQ167_spl,
inference(contradiction_clause,[status(thm)],[f988]) ).
fof(f1011,plain,
! [X0,X1] :
( ~ sQ168_spl
| ~ sQ89_spl
| is_a_theorem(strict_implies(X0,X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(paramodulation,[status(thm)],[f970,f679]) ).
fof(f1106,plain,
( sQ118_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f789,f343]) ).
fof(f1107,plain,
sQ118_spl,
inference(contradiction_clause,[status(thm)],[f1106]) ).
fof(f1207,plain,
( ~ sQ168_spl
| ~ sQ89_spl
| sQ162_spl
| ~ is_a_theorem(implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))) ),
inference(resolution,[status(thm)],[f950,f1011]) ).
fof(f1209,plain,
( ~ sQ168_spl
| ~ sQ89_spl
| sQ162_spl
| ~ sQ119_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1207,f791]) ).
fof(f1210,plain,
( ~ sQ168_spl
| ~ sQ89_spl
| sQ162_spl
| ~ sQ119_spl ),
inference(contradiction_clause,[status(thm)],[f1209]) ).
fof(f1211,plain,
( ~ sQ160_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f942,f350]) ).
fof(f1212,plain,
~ sQ160_spl,
inference(contradiction_clause,[status(thm)],[f1211]) ).
fof(f1213,plain,
$false,
inference(sat_refutation,[status(thm)],[f681,f793,f951,f972,f985,f989,f1107,f1210,f1212]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL536+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n007.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.03/0.36 % CPULimit : 300
% 0.03/0.36 % WCLimit : 300
% 0.03/0.36 % DateTime : Mon Sep 21 00:35:21 UTC 2026
% 0.03/0.36 % CPUTime :
% 0.03/0.38 % Drodi V4.1.1
% 0.03/0.40 % Refutation found
% 0.03/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.03/0.40 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.03/0.44 % Elapsed time: 0.066521 seconds
% 0.03/0.44 % CPU time: 0.215828 seconds
% 0.03/0.44 % Total memory used: 88.063 MB
% 0.03/0.44 % Net memory used: 87.944 MB
%------------------------------------------------------------------------------