%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO010+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:29 EDT 2024
% Result : Theorem 1.15s 1.35s
% Output : Refutation 1.15s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : PRO010+2 : TPTP v8.1.2. Released v4.0.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n018.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 03:25:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 1.15/1.35 % Version: 1.5
% 1.15/1.35 % SZS status Theorem
% 1.15/1.35 % SZS output start CNFRefutation
% 1.15/1.35 fof(sos_44,axiom,tptp1!=tptp2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_44)).
% 1.15/1.35 cnf(c33,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_44])).
% 1.15/1.35 cnf(symmetry,axiom,X126!=X127|X127=X126,theory(equality)).
% 1.15/1.35 fof(sos_14,axiom,(![X42]:(![X43]:(leaf(X42,X43)<=>((root(X42,X43)|(?[X44]:min_precedes(X44,X42,X43)))&(~(?[X45]:min_precedes(X42,X45,X43))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_14)).
% 1.15/1.35 fof(c147,plain,(![X42]:(![X43]:((~leaf(X42,X43)|((root(X42,X43)|(?[X44]:min_precedes(X44,X42,X43)))&(![X45]:~min_precedes(X42,X45,X43))))&(((~root(X42,X43)&(![X44]:~min_precedes(X44,X42,X43)))|(?[X45]:min_precedes(X42,X45,X43)))|leaf(X42,X43))))),inference(fof_nnf,[status(thm)],[sos_14])).
% 1.15/1.35 fof(c148,plain,((![X42]:(![X43]:(~leaf(X42,X43)|((root(X42,X43)|(?[X44]:min_precedes(X44,X42,X43)))&(![X45]:~min_precedes(X42,X45,X43))))))&(![X42]:(![X43]:(((~root(X42,X43)&(![X44]:~min_precedes(X44,X42,X43)))|(?[X45]:min_precedes(X42,X45,X43)))|leaf(X42,X43))))),inference(shift_quantors,[status(thm)],[c147])).
% 1.15/1.35 fof(c149,plain,((![X63]:(![X64]:(~leaf(X63,X64)|((root(X63,X64)|(?[X65]:min_precedes(X65,X63,X64)))&(![X66]:~min_precedes(X63,X66,X64))))))&(![X67]:(![X68]:(((~root(X67,X68)&(![X69]:~min_precedes(X69,X67,X68)))|(?[X70]:min_precedes(X67,X70,X68)))|leaf(X67,X68))))),inference(variable_rename,[status(thm)],[c148])).
% 1.15/1.35 fof(c151,plain,(![X63]:(![X64]:(![X66]:(![X67]:(![X68]:(![X69]:((~leaf(X63,X64)|((root(X63,X64)|min_precedes(skolem0016(X63,X64),X63,X64))&~min_precedes(X63,X66,X64)))&(((~root(X67,X68)&~min_precedes(X69,X67,X68))|min_precedes(X67,skolem0017(X67,X68),X68))|leaf(X67,X68))))))))),inference(shift_quantors,[status(thm)],[fof(c150,plain,((![X63]:(![X64]:(~leaf(X63,X64)|((root(X63,X64)|min_precedes(skolem0016(X63,X64),X63,X64))&(![X66]:~min_precedes(X63,X66,X64))))))&(![X67]:(![X68]:(((~root(X67,X68)&(![X69]:~min_precedes(X69,X67,X68)))|min_precedes(X67,skolem0017(X67,X68),X68))|leaf(X67,X68))))),inference(skolemize,[status(esa)],[c149])).])).
% 1.15/1.35 fof(c152,plain,(![X63]:(![X64]:(![X66]:(![X67]:(![X68]:(![X69]:(((~leaf(X63,X64)|(root(X63,X64)|min_precedes(skolem0016(X63,X64),X63,X64)))&(~leaf(X63,X64)|~min_precedes(X63,X66,X64)))&(((~root(X67,X68)|min_precedes(X67,skolem0017(X67,X68),X68))|leaf(X67,X68))&((~min_precedes(X69,X67,X68)|min_precedes(X67,skolem0017(X67,X68),X68))|leaf(X67,X68)))))))))),inference(distribute,[status(thm)],[c151])).
% 1.15/1.35 cnf(c154,plain,~leaf(X193,X191)|~min_precedes(X193,X192,X191),inference(split_conjunct,[status(thm)],[c152])).
% 1.15/1.35 fof(goals,conjecture,(![X99]:(occurrence_of(X99,tptp0)=>(?[X100]:(?[X101]:((leaf_occ(X101,X99)&(occurrence_of(X101,tptp1)=>(~(?[X102]:(occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0))))))&(occurrence_of(X101,tptp2)=>(~(?[X103]:(occurrence_of(X103,tptp1)&min_precedes(X100,X103,tptp0)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 1.15/1.35 fof(c17,negated_conjecture,(~(![X99]:(occurrence_of(X99,tptp0)=>(?[X100]:(?[X101]:((leaf_occ(X101,X99)&(occurrence_of(X101,tptp1)=>(~(?[X102]:(occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0))))))&(occurrence_of(X101,tptp2)=>(~(?[X103]:(occurrence_of(X103,tptp1)&min_precedes(X100,X103,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 1.15/1.35 fof(c18,negated_conjecture,(?[X99]:(occurrence_of(X99,tptp0)&(![X100]:(![X101]:((~leaf_occ(X101,X99)|(occurrence_of(X101,tptp1)&(?[X102]:(occurrence_of(X102,tptp2)&min_precedes(X100,X102,tptp0)))))|(occurrence_of(X101,tptp2)&(?[X103]:(occurrence_of(X103,tptp1)&min_precedes(X100,X103,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 1.15/1.35 fof(c19,negated_conjecture,(?[X2]:(occurrence_of(X2,tptp0)&(![X3]:(![X4]:((~leaf_occ(X4,X2)|(occurrence_of(X4,tptp1)&(?[X5]:(occurrence_of(X5,tptp2)&min_precedes(X3,X5,tptp0)))))|(occurrence_of(X4,tptp2)&(?[X6]:(occurrence_of(X6,tptp1)&min_precedes(X3,X6,tptp0))))))))),inference(variable_rename,[status(thm)],[c18])).
% 1.15/1.35 fof(c21,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&((~leaf_occ(X4,skolem0001)|(occurrence_of(X4,tptp1)&(occurrence_of(skolem0002(X3,X4),tptp2)&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&(occurrence_of(skolem0003(X3,X4),tptp1)&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)&min_precedes(X3,skolem0002(X3,X4),tptp0))))|(occurrence_of(X4,tptp2)&(occurrence_of(skolem0003(X3,X4),tptp1)&min_precedes(X3,skolem0003(X3,X4),tptp0))))))),inference(skolemize,[status(esa)],[c19])).])).
% 1.15/1.35 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))|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))|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))|min_precedes(X3,skolem0003(X3,X4),tptp0))))))))),inference(distribute,[status(thm)],[c21])).
% 1.15/1.35 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.15/1.35 fof(sos_32,axiom,(![X95]:(occurrence_of(X95,tptp0)=>(?[X96]:(?[X97]:(?[X98]:((((((occurrence_of(X96,tptp3)&root_occ(X96,X95))&occurrence_of(X97,tptp4))&next_subocc(X96,X97,tptp0))&(occurrence_of(X98,tptp1)|occurrence_of(X98,tptp2)))&next_subocc(X97,X98,tptp0))&leaf_occ(X98,X95))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_32)).
% 1.15/1.35 fof(c46,plain,(![X95]:(~occurrence_of(X95,tptp0)|(?[X96]:(?[X97]:(?[X98]:((((((occurrence_of(X96,tptp3)&root_occ(X96,X95))&occurrence_of(X97,tptp4))&next_subocc(X96,X97,tptp0))&(occurrence_of(X98,tptp1)|occurrence_of(X98,tptp2)))&next_subocc(X97,X98,tptp0))&leaf_occ(X98,X95))))))),inference(fof_nnf,[status(thm)],[sos_32])).
% 1.15/1.35 fof(c47,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)],[c46])).
% 1.15/1.35 fof(c48,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)],[c47])).
% 1.15/1.35 fof(c49,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)],[c48])).
% 1.15/1.35 cnf(c56,plain,~occurrence_of(X244,tptp0)|leaf_occ(skolem0006(X244),X244),inference(split_conjunct,[status(thm)],[c49])).
% 1.15/1.35 cnf(c274,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c56, c23])).
% 1.15/1.35 cnf(c30,negated_conjecture,~leaf_occ(X293,skolem0001)|min_precedes(X292,skolem0002(X292,X293),tptp0)|occurrence_of(X293,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 1.15/1.35 cnf(c337,plain,min_precedes(X458,skolem0002(X458,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c30, c274])).
% 1.15/1.35 cnf(c862,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~leaf(X459,tptp0),inference(resolution,[status(thm)],[c337, c154])).
% 1.15/1.35 cnf(reflexivity,axiom,X125=X125,theory(equality)).
% 1.15/1.35 fof(sos_22,axiom,(![X64]:(![X65]:(![X66]:((occurrence_of(X64,X65)&occurrence_of(X64,X66))=>X65=X66)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_22)).
% 1.15/1.35 fof(c110,plain,(![X64]:(![X65]:(![X66]:((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)))),inference(fof_nnf,[status(thm)],[sos_22])).
% 1.15/1.35 fof(c111,plain,(![X39]:(![X40]:(![X41]:((~occurrence_of(X39,X40)|~occurrence_of(X39,X41))|X40=X41)))),inference(variable_rename,[status(thm)],[c110])).
% 1.15/1.35 cnf(c112,plain,~occurrence_of(X285,X286)|~occurrence_of(X285,X284)|X286=X284,inference(split_conjunct,[status(thm)],[c111])).
% 1.15/1.35 cnf(c318,plain,~occurrence_of(skolem0001,X289)|X289=tptp0,inference(resolution,[status(thm)],[c112, c23])).
% 1.15/1.35 fof(sos_11,axiom,(![X35]:(![X36]:(leaf_occ(X35,X36)<=>(?[X37]:((occurrence_of(X36,X37)&subactivity_occurrence(X35,X36))&leaf(X35,X37)))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_11)).
% 1.15/1.35 fof(c167,plain,(![X35]:(![X36]:((~leaf_occ(X35,X36)|(?[X37]:((occurrence_of(X36,X37)&subactivity_occurrence(X35,X36))&leaf(X35,X37))))&((![X37]:((~occurrence_of(X36,X37)|~subactivity_occurrence(X35,X36))|~leaf(X35,X37)))|leaf_occ(X35,X36))))),inference(fof_nnf,[status(thm)],[sos_11])).
% 1.15/1.35 fof(c168,plain,((![X35]:(![X36]:(~leaf_occ(X35,X36)|(?[X37]:((occurrence_of(X36,X37)&subactivity_occurrence(X35,X36))&leaf(X35,X37))))))&(![X35]:(![X36]:((![X37]:((~occurrence_of(X36,X37)|~subactivity_occurrence(X35,X36))|~leaf(X35,X37)))|leaf_occ(X35,X36))))),inference(shift_quantors,[status(thm)],[c167])).
% 1.15/1.35 fof(c169,plain,((![X75]:(![X76]:(~leaf_occ(X75,X76)|(?[X77]:((occurrence_of(X76,X77)&subactivity_occurrence(X75,X76))&leaf(X75,X77))))))&(![X78]:(![X79]:((![X80]:((~occurrence_of(X79,X80)|~subactivity_occurrence(X78,X79))|~leaf(X78,X80)))|leaf_occ(X78,X79))))),inference(variable_rename,[status(thm)],[c168])).
% 1.15/1.35 fof(c171,plain,(![X75]:(![X76]:(![X78]:(![X79]:(![X80]:((~leaf_occ(X75,X76)|((occurrence_of(X76,skolem0018(X75,X76))&subactivity_occurrence(X75,X76))&leaf(X75,skolem0018(X75,X76))))&(((~occurrence_of(X79,X80)|~subactivity_occurrence(X78,X79))|~leaf(X78,X80))|leaf_occ(X78,X79)))))))),inference(shift_quantors,[status(thm)],[fof(c170,plain,((![X75]:(![X76]:(~leaf_occ(X75,X76)|((occurrence_of(X76,skolem0018(X75,X76))&subactivity_occurrence(X75,X76))&leaf(X75,skolem0018(X75,X76))))))&(![X78]:(![X79]:((![X80]:((~occurrence_of(X79,X80)|~subactivity_occurrence(X78,X79))|~leaf(X78,X80)))|leaf_occ(X78,X79))))),inference(skolemize,[status(esa)],[c169])).])).
% 1.15/1.35 fof(c172,plain,(![X75]:(![X76]:(![X78]:(![X79]:(![X80]:((((~leaf_occ(X75,X76)|occurrence_of(X76,skolem0018(X75,X76)))&(~leaf_occ(X75,X76)|subactivity_occurrence(X75,X76)))&(~leaf_occ(X75,X76)|leaf(X75,skolem0018(X75,X76))))&(((~occurrence_of(X79,X80)|~subactivity_occurrence(X78,X79))|~leaf(X78,X80))|leaf_occ(X78,X79)))))))),inference(distribute,[status(thm)],[c171])).
% 1.15/1.35 cnf(c173,plain,~leaf_occ(X264,X263)|occurrence_of(X263,skolem0018(X264,X263)),inference(split_conjunct,[status(thm)],[c172])).
% 1.15/1.35 cnf(c285,plain,occurrence_of(skolem0001,skolem0018(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c173, c274])).
% 1.15/1.35 cnf(c356,plain,skolem0018(skolem0006(skolem0001),skolem0001)=tptp0,inference(resolution,[status(thm)],[c285, c318])).
% 1.15/1.35 cnf(c12,axiom,X241!=X242|X240!=X243|~leaf(X241,X240)|leaf(X242,X243),theory(equality)).
% 1.15/1.35 cnf(c175,plain,~leaf_occ(X267,X266)|leaf(X267,skolem0018(X267,X266)),inference(split_conjunct,[status(thm)],[c172])).
% 1.15/1.35 cnf(c287,plain,leaf(skolem0006(skolem0001),skolem0018(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c175, c274])).
% 1.15/1.35 cnf(c565,plain,skolem0006(skolem0001)!=X607|skolem0018(skolem0006(skolem0001),skolem0001)!=X606|leaf(X607,X606),inference(resolution,[status(thm)],[c287, c12])).
% 1.15/1.35 cnf(c1612,plain,skolem0006(skolem0001)!=X608|leaf(X608,tptp0),inference(resolution,[status(thm)],[c565, c356])).
% 1.15/1.35 cnf(c1615,plain,leaf(skolem0006(skolem0001),tptp0),inference(resolution,[status(thm)],[c1612, reflexivity])).
% 1.15/1.35 cnf(c1623,plain,occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c1615, c862])).
% 1.15/1.35 cnf(c26,negated_conjecture,~leaf_occ(X278,skolem0001)|occurrence_of(X278,tptp1)|min_precedes(X277,skolem0003(X277,X278),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.15/1.35 cnf(c300,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X448,skolem0003(X448,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c26, c274])).
% 1.15/1.35 cnf(c764,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~leaf(X450,tptp0),inference(resolution,[status(thm)],[c300, c154])).
% 1.15/1.35 cnf(c1619,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c1615, c764])).
% 1.15/1.35 cnf(c1628,plain,~occurrence_of(skolem0006(skolem0001),X612)|X612=tptp1,inference(resolution,[status(thm)],[c1619, c112])).
% 1.15/1.35 cnf(c1730,plain,tptp2=tptp1,inference(resolution,[status(thm)],[c1628, c1623])).
% 1.15/1.35 cnf(c1735,plain,tptp1=tptp2,inference(resolution,[status(thm)],[c1730, symmetry])).
% 1.15/1.35 cnf(c1751,plain,$false,inference(resolution,[status(thm)],[c1735, c33])).
% 1.15/1.35 % SZS output end CNFRefutation
% 1.15/1.35
% 1.15/1.35 % Initial clauses : 112
% 1.15/1.35 % Processed clauses : 534
% 1.15/1.35 % Factors computed : 17
% 1.15/1.35 % Resolvents computed: 1498
% 1.15/1.35 % Tautologies deleted: 9
% 1.15/1.35 % Forward subsumed : 305
% 1.15/1.35 % Backward subsumed : 33
% 1.15/1.35 % -------- CPU Time ---------
% 1.15/1.35 % User time : 0.999 s
% 1.15/1.35 % System time : 0.015 s
% 1.15/1.35 % Total time : 1.014 s
%------------------------------------------------------------------------------