%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LCL536+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:10:14 PM UTC 2026
% Result : Theorem 0.13s 0.42s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL536+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n017.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 00:32:43 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.13/0.42 % Refutation found
% 0.13/0.42 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.42 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.42 fof(f50,axiom,(
% 0.13/0.42 ( necessitation<=> (! [X] :( is_a_theorem(X)=> is_a_theorem(necessarily(X)) ) )) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f58,axiom,(
% 0.13/0.42 ( axiom_5<=> (! [X] : is_a_theorem(implies(possibly(X),necessarily(possibly(X)))) )) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f72,axiom,(
% 0.13/0.42 ( axiom_m10<=> (! [X] : is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X)))) )) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f75,axiom,(
% 0.13/0.42 ( op_strict_implies=> (! [X,Y] : strict_implies(X,Y) = necessarily(implies(X,Y)) )) ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f78,axiom,(
% 0.13/0.42 necessitation ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f81,axiom,(
% 0.13/0.42 axiom_5 ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f85,axiom,(
% 0.13/0.42 op_strict_implies ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f88,conjecture,(
% 0.13/0.42 axiom_m10 ),
% 0.13/0.42 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.13/0.42 fof(f89,negated_conjecture,(
% 0.13/0.42 ~(axiom_m10 )),
% 0.13/0.42 inference(negated_conjecture,[status(cth)],[f88])).
% 0.13/0.42 fof(f228,plain,(
% 0.13/0.42 necessitation<=>(![X]: (~is_a_theorem(X)|is_a_theorem(necessarily(X))))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.13/0.42 fof(f229,plain,(
% 0.13/0.42 (~necessitation|(![X]: (~is_a_theorem(X)|is_a_theorem(necessarily(X)))))&(necessitation|(?[X]: (is_a_theorem(X)&~is_a_theorem(necessarily(X)))))),
% 0.13/0.42 inference(NNF_transformation,[status(thm)],[f228])).
% 0.13/0.42 fof(f230,plain,(
% 0.13/0.42 (~necessitation|(![X]: (~is_a_theorem(X)|is_a_theorem(necessarily(X)))))&(necessitation|(is_a_theorem(sK55_skl)&~is_a_theorem(necessarily(sK55_skl))))),
% 0.13/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK55_skl]),skolemize(X,sK55_skl)],[f229])).
% 0.13/0.42 fof(f231,plain,(
% 0.13/0.42 ![X0]: (~necessitation|~is_a_theorem(X0)|is_a_theorem(necessarily(X0)))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f230])).
% 0.13/0.42 fof(f271,plain,(
% 0.13/0.42 (~axiom_5|(![X]: is_a_theorem(implies(possibly(X),necessarily(possibly(X))))))&(axiom_5|(?[X]: ~is_a_theorem(implies(possibly(X),necessarily(possibly(X))))))),
% 0.13/0.42 inference(NNF_transformation,[status(thm)],[f58])).
% 0.13/0.42 fof(f272,plain,(
% 0.13/0.42 (~axiom_5|(![X]: is_a_theorem(implies(possibly(X),necessarily(possibly(X))))))&(axiom_5|~is_a_theorem(implies(possibly(sK67_skl),necessarily(possibly(sK67_skl)))))),
% 0.13/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK67_skl]),skolemize(X,sK67_skl)],[f271])).
% 0.13/0.42 fof(f273,plain,(
% 0.13/0.42 ![X0]: (~axiom_5|is_a_theorem(implies(possibly(X0),necessarily(possibly(X0)))))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f272])).
% 0.13/0.42 fof(f327,plain,(
% 0.13/0.42 (~axiom_m10|(![X]: is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))))&(axiom_m10|(?[X]: ~is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))))),
% 0.13/0.42 inference(NNF_transformation,[status(thm)],[f72])).
% 0.13/0.42 fof(f328,plain,(
% 0.13/0.42 (~axiom_m10|(![X]: is_a_theorem(strict_implies(possibly(X),necessarily(possibly(X))))))&(axiom_m10|~is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))))),
% 0.13/0.42 inference(skolemize,[status(esa),new_symbols(skolem,[sK93_skl]),skolemize(X,sK93_skl)],[f327])).
% 0.13/0.42 fof(f330,plain,(
% 0.13/0.42 axiom_m10|~is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl))))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f328])).
% 0.13/0.42 fof(f335,plain,(
% 0.13/0.42 ~op_strict_implies|(![X,Y]: strict_implies(X,Y)=necessarily(implies(X,Y)))),
% 0.13/0.42 inference(pre_NNF_transformation,[status(thm)],[f75])).
% 0.13/0.42 fof(f336,plain,(
% 0.13/0.42 ![X0,X1]: (~op_strict_implies|strict_implies(X0,X1)=necessarily(implies(X0,X1)))),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f335])).
% 0.13/0.42 fof(f340,plain,(
% 0.13/0.42 necessitation),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f78])).
% 0.13/0.42 fof(f343,plain,(
% 0.13/0.42 axiom_5),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f81])).
% 0.13/0.42 fof(f347,plain,(
% 0.13/0.42 op_strict_implies),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f85])).
% 0.13/0.42 fof(f350,plain,(
% 0.13/0.42 ~axiom_m10),
% 0.13/0.42 inference(cnf_transformation,[status(thm)],[f89])).
% 0.13/0.42 fof(f675,definition,(
% 0.13/0.42 sQ88_spl <=> (necessitation)),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ88_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f677,plain,(
% 0.13/0.42 ~necessitation|sQ88_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f675])).
% 0.13/0.42 fof(f678,definition,(
% 0.13/0.42 ![X0]: (sQ89_spl <=> (~is_a_theorem(X0)|is_a_theorem(necessarily(X0))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f679,plain,(
% 0.13/0.42 ![X0]: (~is_a_theorem(X0)|is_a_theorem(necessarily(X0))|~sQ89_spl)),
% 0.13/0.42 inference(component_clause,[status(thm)],[f678])).
% 0.13/0.42 fof(f681,plain,(
% 0.13/0.42 ~sQ88_spl|sQ89_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f231,f675,f678])).
% 0.13/0.42 fof(f787,definition,(
% 0.13/0.42 sQ118_spl <=> (axiom_5)),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ118_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f789,plain,(
% 0.13/0.42 ~axiom_5|sQ118_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f787])).
% 0.13/0.42 fof(f790,definition,(
% 0.13/0.42 ![X0]: (sQ119_spl <=> (is_a_theorem(implies(possibly(X0),necessarily(possibly(X0))))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f791,plain,(
% 0.13/0.42 ![X0]: (is_a_theorem(implies(possibly(X0),necessarily(possibly(X0))))|~sQ119_spl)),
% 0.13/0.42 inference(component_clause,[status(thm)],[f790])).
% 0.13/0.42 fof(f793,plain,(
% 0.13/0.42 ~sQ118_spl|sQ119_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f273,f787,f790])).
% 0.13/0.42 fof(f941,definition,(
% 0.13/0.42 sQ160_spl <=> (axiom_m10)),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ160_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f942,plain,(
% 0.13/0.42 axiom_m10|~sQ160_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f941])).
% 0.13/0.42 fof(f948,definition,(
% 0.13/0.42 sQ162_spl <=> (is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl)))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ162_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f950,plain,(
% 0.13/0.42 ~is_a_theorem(strict_implies(possibly(sK93_skl),necessarily(possibly(sK93_skl))))|sQ162_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f948])).
% 0.13/0.42 fof(f951,plain,(
% 0.13/0.42 sQ160_spl|~sQ162_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f330,f941,f948])).
% 0.13/0.42 fof(f966,definition,(
% 0.13/0.42 sQ167_spl <=> (op_strict_implies)),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f968,plain,(
% 0.13/0.42 ~op_strict_implies|sQ167_spl),
% 0.13/0.42 inference(component_clause,[status(thm)],[f966])).
% 0.13/0.42 fof(f969,definition,(
% 0.13/0.42 ![X0,X1]: (sQ168_spl <=> (strict_implies(X0,X1)=necessarily(implies(X0,X1))))),
% 0.13/0.42 introduced(definition,[new_symbols(definition,[sQ168_spl])],[split_symbol_definition])).
% 0.13/0.42 fof(f970,plain,(
% 0.13/0.42 ![X0,X1]: (strict_implies(X0,X1)=necessarily(implies(X0,X1))|~sQ168_spl)),
% 0.13/0.42 inference(component_clause,[status(thm)],[f969])).
% 0.13/0.42 fof(f972,plain,(
% 0.13/0.42 ~sQ167_spl|sQ168_spl),
% 0.13/0.42 inference(split_clause,[status(thm)],[f336,f966,f969])).
% 0.13/0.42 fof(f982,plain,(
% 0.13/0.42 $false|sQ167_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f968,f347])).
% 0.13/0.42 fof(f983,plain,(
% 0.13/0.42 sQ167_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f982])).
% 0.13/0.42 fof(f1037,plain,(
% 0.13/0.42 $false|sQ88_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f677,f340])).
% 0.13/0.42 fof(f1038,plain,(
% 0.13/0.42 sQ88_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f1037])).
% 0.13/0.42 fof(f1091,plain,(
% 0.13/0.42 $false|sQ118_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f789,f343])).
% 0.13/0.42 fof(f1092,plain,(
% 0.13/0.42 sQ118_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f1091])).
% 0.13/0.42 fof(f1154,plain,(
% 0.13/0.42 ![X0]: (is_a_theorem(necessarily(implies(possibly(X0),necessarily(possibly(X0)))))|~sQ119_spl|~sQ89_spl)),
% 0.13/0.42 inference(resolution,[status(thm)],[f791,f679])).
% 0.13/0.42 fof(f1155,plain,(
% 0.13/0.42 $false|~sQ168_spl|~sQ119_spl|~sQ89_spl|sQ162_spl),
% 0.13/0.42 inference(backward_subsumption_resolution,[status(thm)],[f950,f1156])).
% 0.13/0.42 fof(f1156,plain,(
% 0.13/0.42 ![X0]: (is_a_theorem(strict_implies(possibly(X0),necessarily(possibly(X0))))|~sQ168_spl|~sQ119_spl|~sQ89_spl)),
% 0.13/0.42 inference(forward_demodulation,[status(thm)],[f970,f1154])).
% 0.13/0.42 fof(f1157,plain,(
% 0.13/0.42 ~sQ168_spl|~sQ119_spl|~sQ89_spl|sQ162_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f1155])).
% 0.13/0.42 fof(f1158,plain,(
% 0.13/0.42 $false|~sQ160_spl),
% 0.13/0.42 inference(forward_subsumption_resolution,[status(thm)],[f942,f350])).
% 0.13/0.42 fof(f1159,plain,(
% 0.13/0.42 ~sQ160_spl),
% 0.13/0.42 inference(contradiction_clause,[status(thm)],[f1158])).
% 0.13/0.42 fof(f1160,plain,(
% 0.13/0.42 $false),
% 0.13/0.42 inference(sat_refutation,[status(thm)],[f681,f793,f951,f972,f983,f1038,f1092,f1157,f1159])).
% 0.13/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.46 % Elapsed time: 0.084574 seconds
% 0.13/0.46 % CPU time: 0.249289 seconds
% 0.13/0.46 % Total memory used: 87.844 MB
% 0.13/0.46 % Net memory used: 87.724 MB
%------------------------------------------------------------------------------