%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO011+4 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n019.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:37:30 EDT 2024
% Result : Theorem 0.88s 1.08s
% Output : Refutation 0.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : PRO011+4 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 03:27:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 0.88/1.08 % Version: 1.5
% 0.88/1.08 % SZS status Theorem
% 0.88/1.08 % SZS output start CNFRefutation
% 0.88/1.08 fof(sos_44,axiom,tptp1!=tptp2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_44)).
% 0.88/1.08 cnf(c40,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_44])).
% 0.88/1.08 cnf(symmetry,axiom,X132!=X133|X133=X132,theory(equality)).
% 0.88/1.08 fof(sos_08,axiom,(![X28]:(![X29]:(![X30]:((occurrence_of(X28,X29)&occurrence_of(X28,X30))=>X29=X30)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_08)).
% 0.88/1.08 fof(c200,plain,(![X28]:(![X29]:(![X30]:((~occurrence_of(X28,X29)|~occurrence_of(X28,X30))|X29=X30)))),inference(fof_nnf,[status(thm)],[sos_08])).
% 0.88/1.08 fof(c201,plain,(![X100]:(![X101]:(![X102]:((~occurrence_of(X100,X101)|~occurrence_of(X100,X102))|X101=X102)))),inference(variable_rename,[status(thm)],[c200])).
% 0.88/1.08 cnf(c202,plain,~occurrence_of(X290,X291)|~occurrence_of(X290,X289)|X291=X289,inference(split_conjunct,[status(thm)],[c201])).
% 0.88/1.08 fof(goals,conjecture,(![X105]:(occurrence_of(X105,tptp0)=>(?[X106]:(?[X107]:((leaf_occ(X107,X105)&(occurrence_of(X107,tptp1)=>(~(?[X108]:((occurrence_of(X108,tptp2)&subactivity_occurrence(X108,X105))&min_precedes(X106,X108,tptp0))))))&(occurrence_of(X107,tptp2)=>(~(?[X109]:((occurrence_of(X109,tptp1)&subactivity_occurrence(X109,X105))&min_precedes(X106,X109,tptp0)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 0.88/1.08 fof(c17,negated_conjecture,(~(![X105]:(occurrence_of(X105,tptp0)=>(?[X106]:(?[X107]:((leaf_occ(X107,X105)&(occurrence_of(X107,tptp1)=>(~(?[X108]:((occurrence_of(X108,tptp2)&subactivity_occurrence(X108,X105))&min_precedes(X106,X108,tptp0))))))&(occurrence_of(X107,tptp2)=>(~(?[X109]:((occurrence_of(X109,tptp1)&subactivity_occurrence(X109,X105))&min_precedes(X106,X109,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 0.88/1.08 fof(c18,negated_conjecture,(?[X105]:(occurrence_of(X105,tptp0)&(![X106]:(![X107]:((~leaf_occ(X107,X105)|(occurrence_of(X107,tptp1)&(?[X108]:((occurrence_of(X108,tptp2)&subactivity_occurrence(X108,X105))&min_precedes(X106,X108,tptp0)))))|(occurrence_of(X107,tptp2)&(?[X109]:((occurrence_of(X109,tptp1)&subactivity_occurrence(X109,X105))&min_precedes(X106,X109,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 0.88/1.08 fof(c19,negated_conjecture,(?[X2]:(occurrence_of(X2,tptp0)&(![X3]:(![X4]:((~leaf_occ(X4,X2)|(occurrence_of(X4,tptp1)&(?[X5]:((occurrence_of(X5,tptp2)&subactivity_occurrence(X5,X2))&min_precedes(X3,X5,tptp0)))))|(occurrence_of(X4,tptp2)&(?[X6]:((occurrence_of(X6,tptp1)&subactivity_occurrence(X6,X2))&min_precedes(X3,X6,tptp0))))))))),inference(variable_rename,[status(thm)],[c18])).
% 0.88/1.08 fof(c21,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&((~leaf_occ(X4,skolem0001)|(occurrence_of(X4,tptp1)&((occurrence_of(skolem0002(X3,X4),tptp2)&subactivity_occurrence(skolem0002(X3,X4),skolem0001))&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&((occurrence_of(skolem0003(X3,X4),tptp1)&subactivity_occurrence(skolem0003(X3,X4),skolem0001))&min_precedes(X3,skolem0003(X3,X4),tptp0))))))),inference(shift_quantors,[status(thm)],[fof(c20,negated_conjecture,(occurrence_of(skolem0001,tptp0)&(![X3]:(![X4]:((~leaf_occ(X4,skolem0001)|(occurrence_of(X4,tptp1)&((occurrence_of(skolem0002(X3,X4),tptp2)&subactivity_occurrence(skolem0002(X3,X4),skolem0001))&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&((occurrence_of(skolem0003(X3,X4),tptp1)&subactivity_occurrence(skolem0003(X3,X4),skolem0001))&min_precedes(X3,skolem0003(X3,X4),tptp0))))))),inference(skolemize,[status(esa)],[c19])).])).
% 0.88/1.08 fof(c22,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&((((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|occurrence_of(X4,tptp2))&((((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|occurrence_of(X4,tptp1))|min_precedes(X3,skolem0003(X3,X4),tptp0))))&(((((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|occurrence_of(X4,tptp2))&((((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|occurrence_of(skolem0002(X3,X4),tptp2))|min_precedes(X3,skolem0003(X3,X4),tptp0))))&(((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|occurrence_of(X4,tptp2))&((((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|subactivity_occurrence(skolem0002(X3,X4),skolem0001))|min_precedes(X3,skolem0003(X3,X4),tptp0)))))&(((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|occurrence_of(X4,tptp2))&((((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|occurrence_of(skolem0003(X3,X4),tptp1))&((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|subactivity_occurrence(skolem0003(X3,X4),skolem0001)))&((~leaf_occ(X4,skolem0001)|min_precedes(X3,skolem0002(X3,X4),tptp0))|min_precedes(X3,skolem0003(X3,X4),tptp0))))))))),inference(distribute,[status(thm)],[c21])).
% 0.88/1.08 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.88/1.08 fof(sos_32,axiom,(![X101]:(occurrence_of(X101,tptp0)=>(?[X102]:(?[X103]:(?[X104]:((((((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&next_subocc(X102,X103,tptp0))&(occurrence_of(X104,tptp1)|occurrence_of(X104,tptp2)))&next_subocc(X103,X104,tptp0))&leaf_occ(X104,X101))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_32)).
% 0.88/1.08 fof(c53,plain,(![X101]:(~occurrence_of(X101,tptp0)|(?[X102]:(?[X103]:(?[X104]:((((((occurrence_of(X102,tptp3)&root_occ(X102,X101))&occurrence_of(X103,tptp4))&next_subocc(X102,X103,tptp0))&(occurrence_of(X104,tptp1)|occurrence_of(X104,tptp2)))&next_subocc(X103,X104,tptp0))&leaf_occ(X104,X101))))))),inference(fof_nnf,[status(thm)],[sos_32])).
% 0.88/1.08 fof(c54,plain,(![X7]:(~occurrence_of(X7,tptp0)|(?[X8]:(?[X9]:(?[X10]:((((((occurrence_of(X8,tptp3)&root_occ(X8,X7))&occurrence_of(X9,tptp4))&next_subocc(X8,X9,tptp0))&(occurrence_of(X10,tptp1)|occurrence_of(X10,tptp2)))&next_subocc(X9,X10,tptp0))&leaf_occ(X10,X7))))))),inference(variable_rename,[status(thm)],[c53])).
% 0.88/1.08 fof(c55,plain,(![X7]:(~occurrence_of(X7,tptp0)|((((((occurrence_of(skolem0004(X7),tptp3)&root_occ(skolem0004(X7),X7))&occurrence_of(skolem0005(X7),tptp4))&next_subocc(skolem0004(X7),skolem0005(X7),tptp0))&(occurrence_of(skolem0006(X7),tptp1)|occurrence_of(skolem0006(X7),tptp2)))&next_subocc(skolem0005(X7),skolem0006(X7),tptp0))&leaf_occ(skolem0006(X7),X7)))),inference(skolemize,[status(esa)],[c54])).
% 0.88/1.08 fof(c56,plain,(![X7]:(((((((~occurrence_of(X7,tptp0)|occurrence_of(skolem0004(X7),tptp3))&(~occurrence_of(X7,tptp0)|root_occ(skolem0004(X7),X7)))&(~occurrence_of(X7,tptp0)|occurrence_of(skolem0005(X7),tptp4)))&(~occurrence_of(X7,tptp0)|next_subocc(skolem0004(X7),skolem0005(X7),tptp0)))&(~occurrence_of(X7,tptp0)|(occurrence_of(skolem0006(X7),tptp1)|occurrence_of(skolem0006(X7),tptp2))))&(~occurrence_of(X7,tptp0)|next_subocc(skolem0005(X7),skolem0006(X7),tptp0)))&(~occurrence_of(X7,tptp0)|leaf_occ(skolem0006(X7),X7)))),inference(distribute,[status(thm)],[c55])).
% 0.88/1.08 cnf(c63,plain,~occurrence_of(X247,tptp0)|leaf_occ(skolem0006(X247),X247),inference(split_conjunct,[status(thm)],[c56])).
% 0.88/1.08 cnf(c274,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c63, c23])).
% 0.88/1.08 fof(sos_09,axiom,(![X31]:(![X32]:(![X33]:((occurrence_of(X31,X33)&leaf_occ(X32,X31))=>(~(?[X34]:min_precedes(X32,X34,X33))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_09)).
% 0.88/1.08 fof(c196,plain,(![X31]:(![X32]:(![X33]:((~occurrence_of(X31,X33)|~leaf_occ(X32,X31))|(![X34]:~min_precedes(X32,X34,X33)))))),inference(fof_nnf,[status(thm)],[sos_09])).
% 0.88/1.08 fof(c198,plain,(![X96]:(![X97]:(![X98]:(![X99]:((~occurrence_of(X96,X98)|~leaf_occ(X97,X96))|~min_precedes(X97,X99,X98)))))),inference(shift_quantors,[status(thm)],[fof(c197,plain,(![X96]:(![X97]:(![X98]:((~occurrence_of(X96,X98)|~leaf_occ(X97,X96))|(![X99]:~min_precedes(X97,X99,X98)))))),inference(variable_rename,[status(thm)],[c196])).])).
% 0.88/1.08 cnf(c199,plain,~occurrence_of(X367,X366)|~leaf_occ(X365,X367)|~min_precedes(X365,X364,X366),inference(split_conjunct,[status(thm)],[c198])).
% 0.88/1.08 cnf(c27,negated_conjecture,~leaf_occ(X284,skolem0001)|occurrence_of(X284,tptp1)|min_precedes(X283,skolem0003(X283,X284),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 0.88/1.08 cnf(c305,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X459,skolem0003(X459,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c27, c274])).
% 0.88/1.08 cnf(c726,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~occurrence_of(X582,tptp0)|~leaf_occ(X583,X582),inference(resolution,[status(thm)],[c305, c199])).
% 0.88/1.08 cnf(c1184,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~occurrence_of(skolem0001,tptp0),inference(resolution,[status(thm)],[c726, c274])).
% 0.88/1.08 cnf(c1185,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c1184, c23])).
% 0.88/1.08 cnf(c1191,plain,~occurrence_of(skolem0006(skolem0001),X586)|X586=tptp1,inference(resolution,[status(thm)],[c1185, c202])).
% 0.88/1.08 cnf(c36,negated_conjecture,~leaf_occ(X315,skolem0001)|min_precedes(X314,skolem0002(X314,X315),tptp0)|occurrence_of(X315,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 0.88/1.08 cnf(c404,plain,min_precedes(X511,skolem0002(X511,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c36, c274])).
% 0.88/1.08 cnf(c961,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~occurrence_of(X608,tptp0)|~leaf_occ(X609,X608),inference(resolution,[status(thm)],[c404, c199])).
% 0.88/1.08 cnf(c1329,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~occurrence_of(skolem0001,tptp0),inference(resolution,[status(thm)],[c961, c274])).
% 0.88/1.08 cnf(c1330,plain,occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c1329, c23])).
% 0.88/1.08 cnf(c1333,plain,tptp2=tptp1,inference(resolution,[status(thm)],[c1330, c1191])).
% 0.88/1.08 cnf(c1356,plain,tptp1=tptp2,inference(resolution,[status(thm)],[c1333, symmetry])).
% 0.88/1.08 cnf(c1365,plain,$false,inference(resolution,[status(thm)],[c1356, c40])).
% 0.88/1.08 % SZS output end CNFRefutation
% 0.88/1.08
% 0.88/1.08 % Initial clauses : 116
% 0.88/1.08 % Processed clauses : 418
% 0.88/1.08 % Factors computed : 9
% 0.88/1.08 % Resolvents computed: 1115
% 0.88/1.08 % Tautologies deleted: 8
% 0.88/1.08 % Forward subsumed : 238
% 0.88/1.08 % Backward subsumed : 31
% 0.88/1.08 % -------- CPU Time ---------
% 0.88/1.08 % User time : 0.708 s
% 0.88/1.08 % System time : 0.017 s
% 0.88/1.08 % Total time : 0.725 s
%------------------------------------------------------------------------------