%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR056+3 : 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 : n004.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:52 PM UTC 2026
% Result : Theorem 2.56s 0.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR056+3 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n004.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 14:38:20 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.45 % Drodi V4.1.1
% 2.56/0.84 % Refutation found
% 2.56/0.84 % SZS status Theorem for theBenchmark: Theorem is valid
% 2.56/0.84 % SZS output start CNFRefutation for theBenchmark
% 2.56/0.84 fof(f842,axiom,(
% 2.56/0.84 (! [INS] :( ( mtvisible(c_tptp_member3717_mt)& supplies(INS) )=> tptpofobject(INS,f_tptpquantityfn_17(n_385)) ) )),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f856,axiom,(
% 2.56/0.84 genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt) ),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f1480,axiom,(
% 2.56/0.84 (! [OBJ] :( artsupplies(OBJ)=> supplies(OBJ) ) )),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f1986,axiom,(
% 2.56/0.84 ( mtvisible(c_cyclistsmt)=> artsupplies(c_tptpartsupplies) ) ),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f4288,axiom,(
% 2.56/0.84 genlmt(c_tptp_spindleheadmt,c_cyclistsmt) ),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f7997,axiom,(
% 2.56/0.84 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f8006,conjecture,(
% 2.56/0.84 (? [QUANTITY] :( mtvisible(c_tptp_member3717_mt)=> tptpofobject(c_tptpartsupplies,QUANTITY) ) )),
% 2.56/0.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 2.56/0.84 fof(f8007,negated_conjecture,(
% 2.56/0.84 ~((? [QUANTITY] :( mtvisible(c_tptp_member3717_mt)=> tptpofobject(c_tptpartsupplies,QUANTITY) ) ))),
% 2.56/0.84 inference(negated_conjecture,[status(cth)],[f8006])).
% 2.56/0.84 fof(f9172,plain,(
% 2.56/0.84 ![INS]: ((~mtvisible(c_tptp_member3717_mt)|~supplies(INS))|tptpofobject(INS,f_tptpquantityfn_17(n_385)))),
% 2.56/0.84 inference(pre_NNF_transformation,[status(thm)],[f842])).
% 2.56/0.84 fof(f9173,plain,(
% 2.56/0.84 ![X0]: (~mtvisible(c_tptp_member3717_mt)|~supplies(X0)|tptpofobject(X0,f_tptpquantityfn_17(n_385)))),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f9172])).
% 2.56/0.84 fof(f9196,plain,(
% 2.56/0.84 genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f856])).
% 2.56/0.84 fof(f10081,plain,(
% 2.56/0.84 ![OBJ]: (~artsupplies(OBJ)|supplies(OBJ))),
% 2.56/0.84 inference(pre_NNF_transformation,[status(thm)],[f1480])).
% 2.56/0.84 fof(f10082,plain,(
% 2.56/0.84 ![X0]: (~artsupplies(X0)|supplies(X0))),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f10081])).
% 2.56/0.84 fof(f10792,plain,(
% 2.56/0.84 ~mtvisible(c_cyclistsmt)|artsupplies(c_tptpartsupplies)),
% 2.56/0.84 inference(pre_NNF_transformation,[status(thm)],[f1986])).
% 2.56/0.84 fof(f10793,plain,(
% 2.56/0.84 ~mtvisible(c_cyclistsmt)|artsupplies(c_tptpartsupplies)),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f10792])).
% 2.56/0.84 fof(f14003,plain,(
% 2.56/0.84 genlmt(c_tptp_spindleheadmt,c_cyclistsmt)),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f4288])).
% 2.56/0.84 fof(f21368,plain,(
% 2.56/0.84 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 2.56/0.84 inference(pre_NNF_transformation,[status(thm)],[f7997])).
% 2.56/0.84 fof(f21369,plain,(
% 2.56/0.84 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 2.56/0.84 inference(miniscoping,[status(thm)],[f21368])).
% 2.56/0.84 fof(f21370,plain,(
% 2.56/0.84 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f21369])).
% 2.56/0.84 fof(f21391,plain,(
% 2.56/0.84 (![QUANTITY]: (mtvisible(c_tptp_member3717_mt)&~tptpofobject(c_tptpartsupplies,QUANTITY)))),
% 2.56/0.84 inference(pre_NNF_transformation,[status(thm)],[f8007])).
% 2.56/0.84 fof(f21392,plain,(
% 2.56/0.84 mtvisible(c_tptp_member3717_mt)&(![QUANTITY]: ~tptpofobject(c_tptpartsupplies,QUANTITY))),
% 2.56/0.84 inference(miniscoping,[status(thm)],[f21391])).
% 2.56/0.84 fof(f21393,plain,(
% 2.56/0.84 mtvisible(c_tptp_member3717_mt)),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f21392])).
% 2.56/0.84 fof(f21394,plain,(
% 2.56/0.84 ![X0]: (~tptpofobject(c_tptpartsupplies,X0))),
% 2.56/0.84 inference(cnf_transformation,[status(thm)],[f21392])).
% 2.56/0.84 fof(f21395,plain,(
% 2.56/0.84 ![X0]: (~genlmt(c_tptp_member3717_mt,X0)|mtvisible(X0))),
% 2.56/0.84 inference(resolution,[status(thm)],[f21370,f21393])).
% 2.56/0.84 fof(f21397,plain,(
% 2.56/0.84 mtvisible(c_tptp_spindleheadmt)),
% 2.56/0.84 inference(resolution,[status(thm)],[f21395,f9196])).
% 2.56/0.84 fof(f21399,plain,(
% 2.56/0.84 ![X0]: (~genlmt(c_tptp_spindleheadmt,X0)|mtvisible(X0))),
% 2.56/0.84 inference(resolution,[status(thm)],[f21397,f21370])).
% 2.56/0.84 fof(f21663,plain,(
% 2.56/0.84 ![X0]: (~supplies(X0)|tptpofobject(X0,f_tptpquantityfn_17(n_385)))),
% 2.56/0.84 inference(forward_subsumption_resolution,[status(thm)],[f9173,f21393])).
% 1.38/0.91 fof(f21712,plain,(
% 1.38/0.91 supplies(c_tptpartsupplies)|~mtvisible(c_cyclistsmt)),
% 1.38/0.91 inference(resolution,[status(thm)],[f10082,f10793])).
% 1.38/0.91 fof(f22311,plain,(
% 1.38/0.91 mtvisible(c_cyclistsmt)),
% 1.38/0.91 inference(resolution,[status(thm)],[f14003,f21399])).
% 1.38/0.91 fof(f22347,plain,(
% 1.38/0.91 supplies(c_tptpartsupplies)),
% 1.38/0.91 inference(backward_subsumption_resolution,[status(thm)],[f21712,f22311])).
% 1.38/0.91 fof(f22357,plain,(
% 1.38/0.91 tptpofobject(c_tptpartsupplies,f_tptpquantityfn_17(n_385))),
% 1.38/0.91 inference(resolution,[status(thm)],[f22347,f21663])).
% 1.38/0.91 fof(f22359,plain,(
% 1.38/0.91 $false),
% 1.38/0.91 inference(forward_subsumption_resolution,[status(thm)],[f22357,f21394])).
% 1.38/0.91 % SZS output end CNFRefutation for theBenchmark.p
% 2.08/2.09 % Elapsed time: 1.480949 seconds
% 2.08/2.09 % CPU time: 3.051966 seconds
% 2.08/2.09 % Total memory used: 422.730 MB
% 2.08/2.09 % Net memory used: 421.904 MB
%------------------------------------------------------------------------------