%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR056+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:18:26 EDT 2024
% Result : Theorem 0.49s 0.73s
% Output : Refutation 0.49s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : CSR056+1 : TPTP v8.1.2. Released v3.4.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n010.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 01:15:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.49/0.73 % Version: 1.5
% 0.49/0.73 % SZS status Theorem
% 0.49/0.73 % SZS output start CNFRefutation
% 0.49/0.73 fof(query56,conjecture,(?[QUANTITY]:(mtvisible(c_tptp_member3717_mt)=>tptpofobject(c_tptpartsupplies,QUANTITY))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', query56)).
% 0.49/0.73 fof(c0,negated_conjecture,(~(?[QUANTITY]:(mtvisible(c_tptp_member3717_mt)=>tptpofobject(c_tptpartsupplies,QUANTITY)))),inference(assume_negation,[status(cth)],[query56])).
% 0.49/0.73 fof(c1,negated_conjecture,(![QUANTITY]:(mtvisible(c_tptp_member3717_mt)&~tptpofobject(c_tptpartsupplies,QUANTITY))),inference(fof_nnf,[status(thm)],[c0])).
% 0.49/0.73 fof(c2,negated_conjecture,(mtvisible(c_tptp_member3717_mt)&(![QUANTITY]:~tptpofobject(c_tptpartsupplies,QUANTITY))),inference(shift_quantors,[status(thm)],[c1])).
% 0.49/0.73 fof(c4,negated_conjecture,(![X2]:(mtvisible(c_tptp_member3717_mt)&~tptpofobject(c_tptpartsupplies,X2))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(mtvisible(c_tptp_member3717_mt)&(![X2]:~tptpofobject(c_tptpartsupplies,X2))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.49/0.73 cnf(c6,negated_conjecture,~tptpofobject(c_tptpartsupplies,X113),inference(split_conjunct,[status(thm)],[c4])).
% 0.49/0.73 cnf(c5,negated_conjecture,mtvisible(c_tptp_member3717_mt),inference(split_conjunct,[status(thm)],[c4])).
% 0.49/0.73 fof(just9,axiom,genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just9)).
% 0.49/0.73 cnf(c201,plain,genlmt(c_tptp_member3717_mt,c_tptp_spindleheadmt),inference(split_conjunct,[status(thm)],[just9])).
% 0.49/0.73 fof(just47,axiom,(![SPECMT]:(![GENLMT]:((mtvisible(SPECMT)&genlmt(SPECMT,GENLMT))=>mtvisible(GENLMT)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just47)).
% 0.49/0.73 fof(c76,plain,(![SPECMT]:(![GENLMT]:((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT)))),inference(fof_nnf,[status(thm)],[just47])).
% 0.49/0.73 fof(c77,plain,(![X39]:(![X40]:((~mtvisible(X39)|~genlmt(X39,X40))|mtvisible(X40)))),inference(variable_rename,[status(thm)],[c76])).
% 0.49/0.73 cnf(c78,plain,~mtvisible(X152)|~genlmt(X152,X153)|mtvisible(X153),inference(split_conjunct,[status(thm)],[c77])).
% 0.49/0.73 cnf(c270,plain,~mtvisible(c_tptp_member3717_mt)|mtvisible(c_tptp_spindleheadmt),inference(resolution,[status(thm)],[c78, c201])).
% 0.49/0.73 cnf(c304,plain,mtvisible(c_tptp_spindleheadmt),inference(resolution,[status(thm)],[c270, c5])).
% 0.49/0.73 fof(just2,axiom,(![OBJ]:(artsupplies(OBJ)=>supplies(OBJ))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just2)).
% 0.49/0.73 fof(c208,plain,(![OBJ]:(~artsupplies(OBJ)|supplies(OBJ))),inference(fof_nnf,[status(thm)],[just2])).
% 0.49/0.73 fof(c209,plain,(![X112]:(~artsupplies(X112)|supplies(X112))),inference(variable_rename,[status(thm)],[c208])).
% 0.49/0.73 cnf(c210,plain,~artsupplies(X121)|supplies(X121),inference(split_conjunct,[status(thm)],[c209])).
% 0.49/0.73 fof(just12,axiom,(mtvisible(c_cyclistsmt)=>artsupplies(c_tptpartsupplies)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just12)).
% 0.49/0.73 fof(c194,plain,(~mtvisible(c_cyclistsmt)|artsupplies(c_tptpartsupplies)),inference(fof_nnf,[status(thm)],[just12])).
% 0.49/0.73 cnf(c195,plain,~mtvisible(c_cyclistsmt)|artsupplies(c_tptpartsupplies),inference(split_conjunct,[status(thm)],[c194])).
% 0.49/0.73 fof(just8,axiom,genlmt(c_tptp_spindleheadmt,c_cyclistsmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just8)).
% 0.49/0.73 cnf(c202,plain,genlmt(c_tptp_spindleheadmt,c_cyclistsmt),inference(split_conjunct,[status(thm)],[just8])).
% 0.49/0.73 cnf(c277,plain,~mtvisible(c_tptp_spindleheadmt)|mtvisible(c_cyclistsmt),inference(resolution,[status(thm)],[c78, c202])).
% 0.49/0.73 cnf(c305,plain,mtvisible(c_cyclistsmt),inference(resolution,[status(thm)],[c277, c304])).
% 0.49/0.73 cnf(c306,plain,artsupplies(c_tptpartsupplies),inference(resolution,[status(thm)],[c305, c195])).
% 0.49/0.73 cnf(c308,plain,supplies(c_tptpartsupplies),inference(resolution,[status(thm)],[c306, c210])).
% 0.49/0.73 fof(just10,axiom,(![INS]:((mtvisible(c_tptp_spindleheadmt)&supplies(INS))=>tptpofobject(INS,f_tptpquantityfn_14(n_232)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just10)).
% 0.49/0.73 fof(c198,plain,(![INS]:((~mtvisible(c_tptp_spindleheadmt)|~supplies(INS))|tptpofobject(INS,f_tptpquantityfn_14(n_232)))),inference(fof_nnf,[status(thm)],[just10])).
% 0.49/0.73 fof(c199,plain,(![X111]:((~mtvisible(c_tptp_spindleheadmt)|~supplies(X111))|tptpofobject(X111,f_tptpquantityfn_14(n_232)))),inference(variable_rename,[status(thm)],[c198])).
% 0.49/0.73 cnf(c200,plain,~mtvisible(c_tptp_spindleheadmt)|~supplies(X233)|tptpofobject(X233,f_tptpquantityfn_14(n_232)),inference(split_conjunct,[status(thm)],[c199])).
% 0.49/0.73 cnf(c323,plain,~mtvisible(c_tptp_spindleheadmt)|tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)),inference(resolution,[status(thm)],[c200, c308])).
% 0.49/0.73 cnf(c411,plain,tptpofobject(c_tptpartsupplies,f_tptpquantityfn_14(n_232)),inference(resolution,[status(thm)],[c323, c304])).
% 0.49/0.73 cnf(c413,plain,$false,inference(resolution,[status(thm)],[c411, c6])).
% 0.49/0.73 % SZS output end CNFRefutation
% 0.49/0.73
% 0.49/0.73 % Initial clauses : 70
% 0.49/0.73 % Processed clauses : 124
% 0.49/0.73 % Factors computed : 4
% 0.49/0.73 % Resolvents computed: 199
% 0.49/0.73 % Tautologies deleted: 29
% 0.49/0.73 % Forward subsumed : 103
% 0.49/0.73 % Backward subsumed : 7
% 0.49/0.73 % -------- CPU Time ---------
% 0.49/0.73 % User time : 0.370 s
% 0.49/0.73 % System time : 0.014 s
% 0.49/0.73 % Total time : 0.384 s
%------------------------------------------------------------------------------