%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : CSR056+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 0.10s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR056+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n015.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Mon Sep 21 14:41:22 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f40,axiom,(
% 0.10/0.41 ( mtvisible(c_cyclistsmt)=> artsupplies(c_tptpartsupplies) ) ),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f202,axiom,(
% 0.10/0.41 (! [INS] :( ( mtvisible(c_tptp_spindleheadmt)& supplies(INS) )=> tptpofobject(INS,f_tptpquantityfn_14(n_232)) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f238,axiom,(
% 0.10/0.41 (! [OBJ] :( artsupplies(OBJ)=> supplies(OBJ) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f254,axiom,(
% 0.10/0.41 genlmt(c_tptp_spindleheadmt,c_cyclistsmt) ),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f279,axiom,(
% 0.10/0.41 genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt) ),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f1123,axiom,(
% 0.10/0.41 (! [SPECMT,GENLMT] :( ( mtvisible(SPECMT)& genlmt(SPECMT,GENLMT) )=> mtvisible(GENLMT) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f1132,conjecture,(
% 0.10/0.41 (? [QUANTITY] :( mtvisible(c_tptp_member3717_mt)=> tptpofobject(c_tptpartsupplies,QUANTITY) ) )),
% 0.10/0.41 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f1133,negated_conjecture,(
% 0.10/0.41 ~((? [QUANTITY] :( mtvisible(c_tptp_member3717_mt)=> tptpofobject(c_tptpartsupplies,QUANTITY) ) ))),
% 0.10/0.41 inference(negated_conjecture,[status(cth)],[f1132])).
% 0.10/0.41 fof(f1192,plain,(
% 0.10/0.41 ~mtvisible(c_cyclistsmt)|artsupplies(c_tptpartsupplies)),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f40])).
% 0.10/0.41 fof(f1193,plain,(
% 0.10/0.41 ~mtvisible(c_cyclistsmt)|artsupplies(c_tptpartsupplies)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f1192])).
% 0.10/0.41 fof(f1428,plain,(
% 0.10/0.41 ![INS]: ((~mtvisible(c_tptp_spindleheadmt)|~supplies(INS))|tptpofobject(INS,f_tptpquantityfn_14(n_232)))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f202])).
% 0.10/0.41 fof(f1429,plain,(
% 0.10/0.41 ![X0]: (~mtvisible(c_tptp_spindleheadmt)|~supplies(X0)|tptpofobject(X0,f_tptpquantityfn_14(n_232)))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f1428])).
% 0.10/0.41 fof(f1481,plain,(
% 0.10/0.41 ![OBJ]: (~artsupplies(OBJ)|supplies(OBJ))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f238])).
% 0.10/0.41 fof(f1482,plain,(
% 0.10/0.41 ![X0]: (~artsupplies(X0)|supplies(X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f1481])).
% 0.10/0.41 fof(f1504,plain,(
% 0.10/0.41 genlmt(c_tptp_spindleheadmt,c_cyclistsmt)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f254])).
% 0.10/0.41 fof(f1539,plain,(
% 0.10/0.41 genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f279])).
% 0.10/0.41 fof(f3181,plain,(
% 0.10/0.41 ![SPECMT,GENLMT]: ((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f1123])).
% 0.10/0.41 fof(f3182,plain,(
% 0.10/0.41 ![GENLMT]: ((![SPECMT]: (~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT)))|mtvisible(GENLMT))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f3181])).
% 0.10/0.41 fof(f3183,plain,(
% 0.10/0.41 ![X0,X1]: (~mtvisible(X0)|~genlmt(X0,X1)|mtvisible(X1))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f3182])).
% 0.10/0.41 fof(f3204,plain,(
% 0.10/0.41 (![QUANTITY]: (mtvisible(c_tptp_member3717_mt)&~tptpofobject(c_tptpartsupplies,QUANTITY)))),
% 0.10/0.41 inference(pre_NNF_transformation,[status(thm)],[f1133])).
% 0.10/0.41 fof(f3205,plain,(
% 0.10/0.41 mtvisible(c_tptp_member3717_mt)&(![QUANTITY]: ~tptpofobject(c_tptpartsupplies,QUANTITY))),
% 0.10/0.41 inference(miniscoping,[status(thm)],[f3204])).
% 0.10/0.41 fof(f3206,plain,(
% 0.10/0.41 mtvisible(c_tptp_member3717_mt)),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f3205])).
% 0.10/0.41 fof(f3207,plain,(
% 0.10/0.41 ![X0]: (~tptpofobject(c_tptpartsupplies,X0))),
% 0.10/0.41 inference(cnf_transformation,[status(thm)],[f3205])).
% 0.10/0.41 fof(f3208,plain,(
% 0.10/0.41 ~mtvisible(c_tptp_member3717_mt)|mtvisible(c_tptp_spindleheadmt)),
% 0.10/0.41 inference(resolution,[status(thm)],[f3183,f1539])).
% 0.10/0.41 fof(f3209,plain,(
% 0.10/0.41 mtvisible(c_tptp_spindleheadmt)),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f3208,f3206])).
% 0.10/0.41 fof(f3253,plain,(
% 0.10/0.41 ![X0]: (~supplies(X0)|tptpofobject(X0,f_tptpquantityfn_14(n_232)))),
% 0.10/0.41 inference(forward_subsumption_resolution,[status(thm)],[f1429,f3209])).
% 0.10/0.41 fof(f3340,plain,(
% 0.10/0.41 ~mtvisible(c_tptp_spindleheadmt)|mtvisible(c_cyclistsmt)),
% 0.10/0.41 inference(resolution,[status(thm)],[f1504,f3183])).
% 0.10/0.42 fof(f3341,plain,(
% 0.10/0.42 mtvisible(c_cyclistsmt)),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f3340,f3209])).
% 0.10/0.42 fof(f3348,plain,(
% 0.10/0.42 artsupplies(c_tptpartsupplies)),
% 0.10/0.42 inference(backward_subsumption_resolution,[status(thm)],[f1193,f3341])).
% 0.10/0.42 fof(f3350,plain,(
% 0.10/0.42 supplies(c_tptpartsupplies)),
% 0.10/0.42 inference(resolution,[status(thm)],[f3348,f1482])).
% 0.10/0.42 fof(f3355,plain,(
% 0.10/0.42 tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232))),
% 0.10/0.42 inference(resolution,[status(thm)],[f3350,f3253])).
% 0.10/0.42 fof(f3356,plain,(
% 0.10/0.42 $false),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f3355,f3207])).
% 0.10/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.45 % Elapsed time: 0.084785 seconds
% 0.10/0.45 % CPU time: 0.231620 seconds
% 0.10/0.45 % Total memory used: 98.484 MB
% 0.10/0.45 % Net memory used: 98.421 MB
%------------------------------------------------------------------------------