%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : CSR044+1 : TPTP v8.1.2. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n012.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:18 EDT 2024
% Result : Theorem 0.61s 0.78s
% Output : Refutation 0.61s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : CSR044+1 : TPTP v8.1.2. Released v3.4.0.
% 0.04/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 01:23:37 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.61/0.78 % Version: 1.5
% 0.61/0.78 % SZS status Theorem
% 0.61/0.78 % SZS output start CNFRefutation
% 0.61/0.78 fof(query44,conjecture,(?[X]:(mtvisible(c_tptp_member3633_mt)=>(tptp_9_720(c_tptpexecutionbyfiringsquad_90,X)&tptpcol_16_29490(X)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', query44)).
% 0.61/0.78 fof(c0,negated_conjecture,(~(?[X]:(mtvisible(c_tptp_member3633_mt)=>(tptp_9_720(c_tptpexecutionbyfiringsquad_90,X)&tptpcol_16_29490(X))))),inference(assume_negation,[status(cth)],[query44])).
% 0.61/0.78 fof(c1,negated_conjecture,(![X]:(mtvisible(c_tptp_member3633_mt)&(~tptp_9_720(c_tptpexecutionbyfiringsquad_90,X)|~tptpcol_16_29490(X)))),inference(fof_nnf,[status(thm)],[c0])).
% 0.61/0.78 fof(c2,negated_conjecture,(mtvisible(c_tptp_member3633_mt)&(![X]:(~tptp_9_720(c_tptpexecutionbyfiringsquad_90,X)|~tptpcol_16_29490(X)))),inference(shift_quantors,[status(thm)],[c1])).
% 0.61/0.78 fof(c4,negated_conjecture,(![X2]:(mtvisible(c_tptp_member3633_mt)&(~tptp_9_720(c_tptpexecutionbyfiringsquad_90,X2)|~tptpcol_16_29490(X2)))),inference(shift_quantors,[status(thm)],[fof(c3,negated_conjecture,(mtvisible(c_tptp_member3633_mt)&(![X2]:(~tptp_9_720(c_tptpexecutionbyfiringsquad_90,X2)|~tptpcol_16_29490(X2)))),inference(variable_rename,[status(thm)],[c2])).])).
% 0.61/0.78 cnf(c6,negated_conjecture,~tptp_9_720(c_tptpexecutionbyfiringsquad_90,X122)|~tptpcol_16_29490(X122),inference(split_conjunct,[status(thm)],[c4])).
% 0.61/0.78 fof(just8,axiom,genlmt(c_tptp_spindleheadmt,c_cyclistsmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just8)).
% 0.61/0.78 cnf(c184,plain,genlmt(c_tptp_spindleheadmt,c_cyclistsmt),inference(split_conjunct,[status(thm)],[just8])).
% 0.61/0.78 fof(just48,axiom,(![SPECMT]:(![GENLMT]:((mtvisible(SPECMT)&genlmt(SPECMT,GENLMT))=>mtvisible(GENLMT)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just48)).
% 0.61/0.78 fof(c53,plain,(![SPECMT]:(![GENLMT]:((~mtvisible(SPECMT)|~genlmt(SPECMT,GENLMT))|mtvisible(GENLMT)))),inference(fof_nnf,[status(thm)],[just48])).
% 0.61/0.78 fof(c54,plain,(![X44]:(![X45]:((~mtvisible(X44)|~genlmt(X44,X45))|mtvisible(X45)))),inference(variable_rename,[status(thm)],[c53])).
% 0.61/0.78 cnf(c55,plain,~mtvisible(X168)|~genlmt(X168,X169)|mtvisible(X169),inference(split_conjunct,[status(thm)],[c54])).
% 0.61/0.78 cnf(c243,plain,~mtvisible(c_tptp_spindleheadmt)|mtvisible(c_cyclistsmt),inference(resolution,[status(thm)],[c55, c184])).
% 0.61/0.78 cnf(c5,negated_conjecture,mtvisible(c_tptp_member3633_mt),inference(split_conjunct,[status(thm)],[c4])).
% 0.61/0.78 fof(just9,axiom,genlmt(c_tptp_member3633_mt,c_tptp_spindleheadmt),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just9)).
% 0.61/0.78 cnf(c183,plain,genlmt(c_tptp_member3633_mt,c_tptp_spindleheadmt),inference(split_conjunct,[status(thm)],[just9])).
% 0.61/0.78 cnf(c248,plain,~mtvisible(c_tptp_member3633_mt)|mtvisible(c_tptp_spindleheadmt),inference(resolution,[status(thm)],[c55, c183])).
% 0.61/0.78 cnf(c264,plain,mtvisible(c_tptp_spindleheadmt),inference(resolution,[status(thm)],[c248, c5])).
% 0.61/0.78 cnf(c265,plain,mtvisible(c_cyclistsmt),inference(resolution,[status(thm)],[c264, c243])).
% 0.61/0.78 fof(just12,axiom,executionbyfiringsquad(c_tptpexecutionbyfiringsquad_90),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just12)).
% 0.61/0.78 cnf(c177,plain,executionbyfiringsquad(c_tptpexecutionbyfiringsquad_90),inference(split_conjunct,[status(thm)],[just12])).
% 0.61/0.78 fof(just10,axiom,(![TERM]:((mtvisible(c_cyclistsmt)&executionbyfiringsquad(TERM))=>tptp_9_720(TERM,f_relationallexistsfn(TERM,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just10)).
% 0.61/0.78 fof(c180,plain,(![TERM]:((~mtvisible(c_cyclistsmt)|~executionbyfiringsquad(TERM))|tptp_9_720(TERM,f_relationallexistsfn(TERM,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)))),inference(fof_nnf,[status(thm)],[just10])).
% 0.61/0.78 fof(c181,plain,(![X117]:((~mtvisible(c_cyclistsmt)|~executionbyfiringsquad(X117))|tptp_9_720(X117,f_relationallexistsfn(X117,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)))),inference(variable_rename,[status(thm)],[c180])).
% 0.61/0.78 cnf(c182,plain,~mtvisible(c_cyclistsmt)|~executionbyfiringsquad(X243)|tptp_9_720(X243,f_relationallexistsfn(X243,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),inference(split_conjunct,[status(thm)],[c181])).
% 0.61/0.78 cnf(c297,plain,~mtvisible(c_cyclistsmt)|tptp_9_720(c_tptpexecutionbyfiringsquad_90,f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),inference(resolution,[status(thm)],[c182, c177])).
% 0.61/0.78 cnf(c366,plain,tptp_9_720(c_tptpexecutionbyfiringsquad_90,f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),inference(resolution,[status(thm)],[c297, c265])).
% 0.61/0.78 cnf(c395,plain,~tptpcol_16_29490(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),inference(resolution,[status(thm)],[c366, c6])).
% 0.61/0.78 fof(just31,axiom,(![X]:(isa(X,c_tptpcol_16_29490)=>tptpcol_16_29490(X))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just31)).
% 0.61/0.78 fof(c112,plain,(![X]:(~isa(X,c_tptpcol_16_29490)|tptpcol_16_29490(X))),inference(fof_nnf,[status(thm)],[just31])).
% 0.61/0.78 fof(c113,plain,(![X75]:(~isa(X75,c_tptpcol_16_29490)|tptpcol_16_29490(X75))),inference(variable_rename,[status(thm)],[c112])).
% 0.61/0.78 cnf(c114,plain,~isa(X213,c_tptpcol_16_29490)|tptpcol_16_29490(X213),inference(split_conjunct,[status(thm)],[c113])).
% 0.61/0.78 fof(just34,axiom,(![X]:(executionbyfiringsquad(X)=>isa(X,c_executionbyfiringsquad))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just34)).
% 0.61/0.78 fof(c103,plain,(![X]:(~executionbyfiringsquad(X)|isa(X,c_executionbyfiringsquad))),inference(fof_nnf,[status(thm)],[just34])).
% 0.61/0.78 fof(c104,plain,(![X72]:(~executionbyfiringsquad(X72)|isa(X72,c_executionbyfiringsquad))),inference(variable_rename,[status(thm)],[c103])).
% 0.61/0.78 cnf(c105,plain,~executionbyfiringsquad(X210)|isa(X210,c_executionbyfiringsquad),inference(split_conjunct,[status(thm)],[c104])).
% 0.61/0.78 cnf(c260,plain,isa(c_tptpexecutionbyfiringsquad_90,c_executionbyfiringsquad),inference(resolution,[status(thm)],[c105, c177])).
% 0.61/0.78 fof(just11,axiom,(mtvisible(c_cyclistsmt)=>relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just11)).
% 0.61/0.78 fof(c178,plain,(~mtvisible(c_cyclistsmt)|relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),inference(fof_nnf,[status(thm)],[just11])).
% 0.61/0.78 cnf(c179,plain,~mtvisible(c_cyclistsmt)|relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),inference(split_conjunct,[status(thm)],[c178])).
% 0.61/0.78 cnf(c289,plain,relationallexists(c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),inference(resolution,[status(thm)],[c179, c265])).
% 0.61/0.78 fof(just1,axiom,(![TERM]:(![INDEPCOL]:(![PRED]:(![DEPCOL]:((isa(TERM,INDEPCOL)&relationallexists(PRED,INDEPCOL,DEPCOL))=>isa(f_relationallexistsfn(TERM,PRED,INDEPCOL,DEPCOL),DEPCOL)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', just1)).
% 0.61/0.78 fof(c191,plain,(![TERM]:(![INDEPCOL]:(![PRED]:(![DEPCOL]:((~isa(TERM,INDEPCOL)|~relationallexists(PRED,INDEPCOL,DEPCOL))|isa(f_relationallexistsfn(TERM,PRED,INDEPCOL,DEPCOL),DEPCOL)))))),inference(fof_nnf,[status(thm)],[just1])).
% 0.61/0.78 fof(c192,plain,(![X118]:(![X119]:(![X120]:(![X121]:((~isa(X118,X119)|~relationallexists(X120,X119,X121))|isa(f_relationallexistsfn(X118,X120,X119,X121),X121)))))),inference(variable_rename,[status(thm)],[c191])).
% 0.61/0.78 cnf(c193,plain,~isa(X247,X245)|~relationallexists(X246,X245,X248)|isa(f_relationallexistsfn(X247,X246,X245,X248),X248),inference(split_conjunct,[status(thm)],[c192])).
% 0.61/0.78 cnf(c298,plain,~isa(X262,c_executionbyfiringsquad)|isa(f_relationallexistsfn(X262,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),c_tptpcol_16_29490),inference(resolution,[status(thm)],[c193, c289])).
% 0.61/0.78 cnf(c367,plain,isa(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490),c_tptpcol_16_29490),inference(resolution,[status(thm)],[c298, c260])).
% 0.61/0.78 cnf(c398,plain,tptpcol_16_29490(f_relationallexistsfn(c_tptpexecutionbyfiringsquad_90,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490)),inference(resolution,[status(thm)],[c367, c114])).
% 0.61/0.78 cnf(c401,plain,$false,inference(resolution,[status(thm)],[c398, c395])).
% 0.61/0.78 % SZS output end CNFRefutation
% 0.61/0.78
% 0.61/0.78 % Initial clauses : 66
% 0.61/0.78 % Processed clauses : 135
% 0.61/0.78 % Factors computed : 3
% 0.61/0.78 % Resolvents computed: 205
% 0.61/0.78 % Tautologies deleted: 16
% 0.61/0.78 % Forward subsumed : 121
% 0.61/0.78 % Backward subsumed : 6
% 0.61/0.78 % -------- CPU Time ---------
% 0.61/0.78 % User time : 0.428 s
% 0.61/0.78 % System time : 0.015 s
% 0.61/0.78 % Total time : 0.443 s
%------------------------------------------------------------------------------