%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR071+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.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 12:14:59 PM UTC 2026
% Result : Theorem 0.08s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.23 % Problem : CSR071+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.24 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.56 % Computer : n013.cluster.edu
% 0.08/0.56 % Model : x86_64 x86_64
% 0.08/0.56 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.56 % Memory : 8046.5625MB
% 0.08/0.56 % OS : Linux 6.8.0-71-generic
% 0.08/0.56 % CPULimit : 300
% 0.08/0.56 % WCLimit : 300
% 0.08/0.56 % DateTime : Mon Sep 21 14:45:08 UTC 2026
% 0.08/0.56 % CPUTime :
% 0.08/0.59 % Drodi V4.1.1
% 0.08/0.61 % Refutation found
% 0.08/0.61 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.08/0.61 % SZS output start CNFRefutation for theBenchmark
% 0.08/0.61 fof(f91,axiom,(
% 0.08/0.61 ( mtvisible(c_tptp_member1672_mt)=> navypersonnel(c_tptpnavypersonnel_3) ) ),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f284,axiom,(
% 0.08/0.61 (! [OBJ] :( navypersonnel(OBJ)=> militaryperson(OBJ) ) )),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f448,axiom,(
% 0.08/0.61 genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt) ),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f453,axiom,(
% 0.08/0.61 genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt) ),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f495,axiom,(
% 0.08/0.61 (! [INS] :( ( mtvisible(c_tptp_member698_mt)& militaryperson(INS) )=> tptpofobject(INS,f_tptpquantityfn_6(n_414)) ) )),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f1123,axiom,(
% 0.08/0.61 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f1131,axiom,(
% 0.08/0.61 mtvisible(c_universalvocabularymt) ),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f1132,conjecture,(
% 0.08/0.61 ( mtvisible(c_tptp_spindlecollectormt)=> tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)) ) ),
% 0.08/0.61 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.08/0.61 fof(f1133,negated_conjecture,(
% 0.08/0.61 ~(( mtvisible(c_tptp_spindlecollectormt)=> tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)) ) )),
% 0.08/0.61 inference(negated_conjecture,[status(cth)],[f1132])).
% 0.08/0.61 fof(f1265,plain,(
% 0.08/0.61 ~mtvisible(c_tptp_member1672_mt)|navypersonnel(c_tptpnavypersonnel_3)),
% 0.08/0.61 inference(pre_NNF_transformation,[status(thm)],[f91])).
% 0.08/0.61 fof(f1266,plain,(
% 0.08/0.61 ~mtvisible(c_tptp_member1672_mt)|navypersonnel(c_tptpnavypersonnel_3)),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f1265])).
% 0.08/0.61 fof(f1546,plain,(
% 0.08/0.61 ![OBJ]: (~navypersonnel(OBJ)|militaryperson(OBJ))),
% 0.08/0.61 inference(pre_NNF_transformation,[status(thm)],[f284])).
% 0.08/0.61 fof(f1547,plain,(
% 0.08/0.61 ![X0]: (~navypersonnel(X0)|militaryperson(X0))),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f1546])).
% 0.08/0.61 fof(f1787,plain,(
% 0.08/0.61 genlmt(c_tptp_spindlecollectormt,c_tptp_member698_mt)),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f448])).
% 0.08/0.61 fof(f1795,plain,(
% 0.08/0.61 genlmt(c_tptp_spindlecollectormt,c_tptp_member1672_mt)),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f453])).
% 0.08/0.61 fof(f1858,plain,(
% 0.08/0.61 ![INS]: ((~mtvisible(c_tptp_member698_mt)|~militaryperson(INS))|tptpofobject(INS,f_tptpquantityfn_6(n_414)))),
% 0.08/0.61 inference(pre_NNF_transformation,[status(thm)],[f495])).
% 0.08/0.61 fof(f1859,plain,(
% 0.08/0.61 ![X0]: (~mtvisible(c_tptp_member698_mt)|~militaryperson(X0)|tptpofobject(X0,f_tptpquantityfn_6(n_414)))),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f1858])).
% 0.08/0.61 fof(f3181,plain,(
% 0.08/0.61 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.08/0.61 inference(pre_NNF_transformation,[status(thm)],[f1123])).
% 0.08/0.61 fof(f3182,plain,(
% 0.08/0.61 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.08/0.61 inference(miniscoping,[status(thm)],[f3181])).
% 0.08/0.61 fof(f3183,plain,(
% 0.08/0.61 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f3182])).
% 0.08/0.61 fof(f3203,plain,(
% 0.08/0.61 mtvisible(c_universalvocabularymt)),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f1131])).
% 0.08/0.61 fof(f3204,plain,(
% 0.08/0.61 (mtvisible(c_tptp_spindlecollectormt)&~tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414)))),
% 0.08/0.61 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 0.08/0.61 fof(f3205,plain,(
% 0.08/0.61 mtvisible(c_tptp_spindlecollectormt)),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f3204])).
% 0.08/0.61 fof(f3206,plain,(
% 0.08/0.61 ~tptpofobject(c_tptpnavypersonnel_3,f_tptpquantityfn_6(n_414))),
% 0.08/0.61 inference(cnf_transformation,[status(thm)],[f3204])).
% 0.08/0.61 fof(f3250,definition,(
% 0.08/0.61 sQ12_spl <=> (mtvisible(c_tptp_member1672_mt))),
% 0.08/0.61 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.08/0.61 fof(f3253,definition,(
% 0.08/0.61 sQ13_spl <=> (navypersonnel(c_tptpnavypersonnel_3))),
% 0.08/0.61 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.08/0.62 fof(f3254,plain,(
% 0.08/0.62 navypersonnel(c_tptpnavypersonnel_3)|~sQ13_spl),
% 0.08/0.62 inference(component_clause,[status(thm)],[f3253])).
% 0.08/0.62 fof(f3256,plain,(
% 0.08/0.62 ~sQ12_spl|sQ13_spl),
% 0.08/0.62 inference(split_clause,[status(thm)],[f1266,f3250,f3253])).
% 0.08/0.62 fof(f3468,definition,(
% 0.08/0.62 sQ70_spl <=> (mtvisible(c_tptp_member698_mt))),
% 0.08/0.62 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.08/0.62 fof(f3471,definition,(
% 0.08/0.62 ![X0]: (sQ71_spl <=> (~militaryperson(X0)|tptpofobject(X0,f_tptpquantityfn_6(n_414))))),
% 0.08/0.62 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 0.08/0.62 fof(f3472,plain,(
% 0.08/0.62 ![X0]: (~militaryperson(X0)|tptpofobject(X0,f_tptpquantityfn_6(n_414))|~sQ71_spl)),
% 0.08/0.62 inference(component_clause,[status(thm)],[f3471])).
% 0.08/0.62 fof(f3474,plain,(
% 0.08/0.62 ~sQ70_spl|sQ71_spl),
% 0.08/0.62 inference(split_clause,[status(thm)],[f1859,f3468,f3471])).
% 0.08/0.62 fof(f3488,definition,(
% 0.08/0.62 sQ75_spl <=> (mtvisible(c_tptp_spindlecollectormt))),
% 0.08/0.62 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.08/0.62 fof(f3490,plain,(
% 0.08/0.62 ~mtvisible(c_tptp_spindlecollectormt)|sQ75_spl),
% 0.08/0.62 inference(component_clause,[status(thm)],[f3488])).
% 0.08/0.62 fof(f3492,plain,(
% 0.08/0.62 $false|sQ75_spl),
% 0.08/0.62 inference(forward_subsumption_resolution,[status(thm)],[f3490,f3205])).
% 0.08/0.62 fof(f3493,plain,(
% 0.08/0.62 sQ75_spl),
% 0.08/0.62 inference(contradiction_clause,[status(thm)],[f3492])).
% 0.08/0.62 fof(f3564,definition,(
% 0.08/0.62 sQ91_spl <=> (mtvisible(c_universalvocabularymt))),
% 0.08/0.62 introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition])).
% 0.08/0.62 fof(f3566,plain,(
% 0.08/0.62 ~mtvisible(c_universalvocabularymt)|sQ91_spl),
% 0.08/0.62 inference(component_clause,[status(thm)],[f3564])).
% 0.08/0.62 fof(f3571,plain,(
% 0.08/0.62 $false|sQ91_spl),
% 0.08/0.62 inference(forward_subsumption_resolution,[status(thm)],[f3566,f3203])).
% 0.08/0.62 fof(f3572,plain,(
% 0.08/0.62 sQ91_spl),
% 0.08/0.62 inference(contradiction_clause,[status(thm)],[f3571])).
% 0.08/0.62 fof(f4099,plain,(
% 0.08/0.62 ~mtvisible(c_tptp_spindlecollectormt)|mtvisible(c_tptp_member698_mt)),
% 0.08/0.62 inference(resolution,[status(thm)],[f1787,f3183])).
% 0.08/0.62 fof(f4100,plain,(
% 0.08/0.62 ~sQ75_spl|sQ70_spl),
% 0.08/0.62 inference(split_clause,[status(thm)],[f4099,f3488,f3468])).
% 0.08/0.62 fof(f4103,plain,(
% 0.08/0.62 ~militaryperson(c_tptpnavypersonnel_3)|~sQ71_spl),
% 0.08/0.62 inference(resolution,[status(thm)],[f3472,f3206])).
% 0.08/0.62 fof(f4104,plain,(
% 0.08/0.62 ~navypersonnel(c_tptpnavypersonnel_3)|~sQ71_spl),
% 0.08/0.62 inference(resolution,[status(thm)],[f4103,f1547])).
% 0.08/0.62 fof(f4106,plain,(
% 0.08/0.62 ~mtvisible(c_tptp_spindlecollectormt)|mtvisible(c_tptp_member1672_mt)),
% 0.08/0.62 inference(resolution,[status(thm)],[f1795,f3183])).
% 0.08/0.62 fof(f4107,plain,(
% 0.08/0.62 ~sQ75_spl|sQ12_spl),
% 0.08/0.62 inference(split_clause,[status(thm)],[f4106,f3488,f3250])).
% 0.08/0.62 fof(f4115,plain,(
% 0.08/0.62 $false|~sQ71_spl|~sQ13_spl),
% 0.08/0.62 inference(forward_subsumption_resolution,[status(thm)],[f3254,f4104])).
% 0.08/0.62 fof(f4116,plain,(
% 0.08/0.62 ~sQ71_spl|~sQ13_spl),
% 0.08/0.62 inference(contradiction_clause,[status(thm)],[f4115])).
% 0.08/0.62 fof(f4117,plain,(
% 0.08/0.62 $false),
% 0.08/0.62 inference(sat_refutation,[status(thm)],[f3256,f3474,f3493,f3572,f4100,f4107,f4116])).
% 0.08/0.62 % SZS output end CNFRefutation for theBenchmark.p
% 1.38/1.85 % Elapsed time: 1.073390 seconds
% 1.38/1.85 % CPU time: 0.211094 seconds
% 1.38/1.85 % Total memory used: 74.362 MB
% 1.38/1.85 % Net memory used: 74.299 MB
%------------------------------------------------------------------------------