%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO012+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n006.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 52.17s 52.35s
% Output : Refutation 52.17s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : PRO012+2 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n006.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:26:37 EDT 2024
% 0.13/0.35 % CPUTime :
% 52.17/52.35 % Version: 1.5
% 52.17/52.35 % SZS status Theorem
% 52.17/52.35 % SZS output start CNFRefutation
% 52.17/52.35 fof(goals,conjecture,(![X100]:(occurrence_of(X100,tptp0)=>(?[X101]:(?[X102]:(((occurrence_of(X101,tptp3)&root_occ(X101,X100))&(occurrence_of(X102,tptp2)|occurrence_of(X102,tptp1)))&min_precedes(X101,X102,tptp0)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 52.17/52.35 fof(c17,negated_conjecture,(~(![X100]:(occurrence_of(X100,tptp0)=>(?[X101]:(?[X102]:(((occurrence_of(X101,tptp3)&root_occ(X101,X100))&(occurrence_of(X102,tptp2)|occurrence_of(X102,tptp1)))&min_precedes(X101,X102,tptp0))))))),inference(assume_negation,[status(cth)],[goals])).
% 52.17/52.35 fof(c18,negated_conjecture,(?[X100]:(occurrence_of(X100,tptp0)&(![X101]:(![X102]:(((~occurrence_of(X101,tptp3)|~root_occ(X101,X100))|(~occurrence_of(X102,tptp2)&~occurrence_of(X102,tptp1)))|~min_precedes(X101,X102,tptp0)))))),inference(fof_nnf,[status(thm)],[c17])).
% 52.17/52.35 fof(c19,negated_conjecture,(?[X2]:(occurrence_of(X2,tptp0)&(![X3]:(![X4]:(((~occurrence_of(X3,tptp3)|~root_occ(X3,X2))|(~occurrence_of(X4,tptp2)&~occurrence_of(X4,tptp1)))|~min_precedes(X3,X4,tptp0)))))),inference(variable_rename,[status(thm)],[c18])).
% 52.17/52.35 fof(c21,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&(((~occurrence_of(X3,tptp3)|~root_occ(X3,skolem0001))|(~occurrence_of(X4,tptp2)&~occurrence_of(X4,tptp1)))|~min_precedes(X3,X4,tptp0))))),inference(shift_quantors,[status(thm)],[fof(c20,negated_conjecture,(occurrence_of(skolem0001,tptp0)&(![X3]:(![X4]:(((~occurrence_of(X3,tptp3)|~root_occ(X3,skolem0001))|(~occurrence_of(X4,tptp2)&~occurrence_of(X4,tptp1)))|~min_precedes(X3,X4,tptp0))))),inference(skolemize,[status(esa)],[c19])).])).
% 52.17/52.35 fof(c22,negated_conjecture,(![X3]:(![X4]:(occurrence_of(skolem0001,tptp0)&((((~occurrence_of(X3,tptp3)|~root_occ(X3,skolem0001))|~occurrence_of(X4,tptp2))|~min_precedes(X3,X4,tptp0))&(((~occurrence_of(X3,tptp3)|~root_occ(X3,skolem0001))|~occurrence_of(X4,tptp1))|~min_precedes(X3,X4,tptp0)))))),inference(distribute,[status(thm)],[c21])).
% 52.17/52.35 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 52.17/52.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))&min_precedes(X96,X97,tptp0))&(occurrence_of(X98,tptp2)|occurrence_of(X98,tptp1)))&min_precedes(X97,X98,tptp0))&(![X99]:(min_precedes(X96,X99,tptp0)=>(X99=X97|X99=X98))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_32)).
% 52.17/52.35 fof(c39,plain,(![X95]:(~occurrence_of(X95,tptp0)|(?[X96]:(?[X97]:(?[X98]:((((((occurrence_of(X96,tptp3)&root_occ(X96,X95))&occurrence_of(X97,tptp4))&min_precedes(X96,X97,tptp0))&(occurrence_of(X98,tptp2)|occurrence_of(X98,tptp1)))&min_precedes(X97,X98,tptp0))&(![X99]:(~min_precedes(X96,X99,tptp0)|(X99=X97|X99=X98))))))))),inference(fof_nnf,[status(thm)],[sos_32])).
% 52.17/52.35 fof(c40,plain,(![X5]:(~occurrence_of(X5,tptp0)|(?[X6]:(?[X7]:(?[X8]:((((((occurrence_of(X6,tptp3)&root_occ(X6,X5))&occurrence_of(X7,tptp4))&min_precedes(X6,X7,tptp0))&(occurrence_of(X8,tptp2)|occurrence_of(X8,tptp1)))&min_precedes(X7,X8,tptp0))&(![X9]:(~min_precedes(X6,X9,tptp0)|(X9=X7|X9=X8))))))))),inference(variable_rename,[status(thm)],[c39])).
% 52.17/52.35 fof(c42,plain,(![X5]:(![X9]:(~occurrence_of(X5,tptp0)|((((((occurrence_of(skolem0002(X5),tptp3)&root_occ(skolem0002(X5),X5))&occurrence_of(skolem0003(X5),tptp4))&min_precedes(skolem0002(X5),skolem0003(X5),tptp0))&(occurrence_of(skolem0004(X5),tptp2)|occurrence_of(skolem0004(X5),tptp1)))&min_precedes(skolem0003(X5),skolem0004(X5),tptp0))&(~min_precedes(skolem0002(X5),X9,tptp0)|(X9=skolem0003(X5)|X9=skolem0004(X5))))))),inference(shift_quantors,[status(thm)],[fof(c41,plain,(![X5]:(~occurrence_of(X5,tptp0)|((((((occurrence_of(skolem0002(X5),tptp3)&root_occ(skolem0002(X5),X5))&occurrence_of(skolem0003(X5),tptp4))&min_precedes(skolem0002(X5),skolem0003(X5),tptp0))&(occurrence_of(skolem0004(X5),tptp2)|occurrence_of(skolem0004(X5),tptp1)))&min_precedes(skolem0003(X5),skolem0004(X5),tptp0))&(![X9]:(~min_precedes(skolem0002(X5),X9,tptp0)|(X9=skolem0003(X5)|X9=skolem0004(X5))))))),inference(skolemize,[status(esa)],[c40])).])).
% 52.17/52.35 fof(c43,plain,(![X5]:(![X9]:(((((((~occurrence_of(X5,tptp0)|occurrence_of(skolem0002(X5),tptp3))&(~occurrence_of(X5,tptp0)|root_occ(skolem0002(X5),X5)))&(~occurrence_of(X5,tptp0)|occurrence_of(skolem0003(X5),tptp4)))&(~occurrence_of(X5,tptp0)|min_precedes(skolem0002(X5),skolem0003(X5),tptp0)))&(~occurrence_of(X5,tptp0)|(occurrence_of(skolem0004(X5),tptp2)|occurrence_of(skolem0004(X5),tptp1))))&(~occurrence_of(X5,tptp0)|min_precedes(skolem0003(X5),skolem0004(X5),tptp0)))&(~occurrence_of(X5,tptp0)|(~min_precedes(skolem0002(X5),X9,tptp0)|(X9=skolem0003(X5)|X9=skolem0004(X5))))))),inference(distribute,[status(thm)],[c42])).
% 52.17/52.35 cnf(c44,plain,~occurrence_of(X271,tptp0)|occurrence_of(skolem0002(X271),tptp3),inference(split_conjunct,[status(thm)],[c43])).
% 52.17/52.35 cnf(c273,plain,occurrence_of(skolem0002(skolem0001),tptp3),inference(resolution,[status(thm)],[c44, c23])).
% 52.17/52.35 cnf(c45,plain,~occurrence_of(X238,tptp0)|root_occ(skolem0002(X238),X238),inference(split_conjunct,[status(thm)],[c43])).
% 52.17/52.35 cnf(c260,plain,root_occ(skolem0002(skolem0001),skolem0001),inference(resolution,[status(thm)],[c45, c23])).
% 52.17/52.35 cnf(c25,negated_conjecture,~occurrence_of(X275,tptp3)|~root_occ(X275,skolem0001)|~occurrence_of(X274,tptp1)|~min_precedes(X275,X274,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 52.17/52.35 cnf(c47,plain,~occurrence_of(X277,tptp0)|min_precedes(skolem0002(X277),skolem0003(X277),tptp0),inference(split_conjunct,[status(thm)],[c43])).
% 52.17/52.35 cnf(c291,plain,min_precedes(skolem0002(skolem0001),skolem0003(skolem0001),tptp0),inference(resolution,[status(thm)],[c47, c23])).
% 52.17/52.35 cnf(c49,plain,~occurrence_of(X285,tptp0)|min_precedes(skolem0003(X285),skolem0004(X285),tptp0),inference(split_conjunct,[status(thm)],[c43])).
% 52.17/52.35 cnf(c310,plain,min_precedes(skolem0003(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c49, c23])).
% 52.17/52.35 fof(sos,axiom,(![X0]:(![X1]:(![X2]:(![X3]:((min_precedes(X0,X1,X3)&min_precedes(X1,X2,X3))=>min_precedes(X0,X2,X3)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos)).
% 52.17/52.35 fof(c234,plain,(![X0]:(![X1]:(![X2]:(![X3]:((~min_precedes(X0,X1,X3)|~min_precedes(X1,X2,X3))|min_precedes(X0,X2,X3)))))),inference(fof_nnf,[status(thm)],[sos])).
% 52.17/52.35 fof(c235,plain,(![X120]:(![X121]:(![X122]:(![X123]:((~min_precedes(X120,X121,X123)|~min_precedes(X121,X122,X123))|min_precedes(X120,X122,X123)))))),inference(variable_rename,[status(thm)],[c234])).
% 52.17/52.35 cnf(c236,plain,~min_precedes(X404,X407,X405)|~min_precedes(X407,X406,X405)|min_precedes(X404,X406,X405),inference(split_conjunct,[status(thm)],[c235])).
% 52.17/52.35 cnf(c561,plain,~min_precedes(X571,skolem0003(skolem0001),tptp0)|min_precedes(X571,skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c236, c310])).
% 52.17/52.35 cnf(c1578,plain,min_precedes(skolem0002(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c561, c291])).
% 52.17/52.35 cnf(c1599,plain,~occurrence_of(skolem0002(skolem0001),tptp3)|~root_occ(skolem0002(skolem0001),skolem0001)|~occurrence_of(skolem0004(skolem0001),tptp1),inference(resolution,[status(thm)],[c1578, c25])).
% 52.17/52.35 cnf(c48,plain,~occurrence_of(X278,tptp0)|occurrence_of(skolem0004(X278),tptp2)|occurrence_of(skolem0004(X278),tptp1),inference(split_conjunct,[status(thm)],[c43])).
% 52.17/52.35 cnf(c295,plain,occurrence_of(skolem0004(skolem0001),tptp2)|occurrence_of(skolem0004(skolem0001),tptp1),inference(resolution,[status(thm)],[c48, c23])).
% 52.17/52.35 fof(sos_18,axiom,(![X52]:(activity_occurrence(X52)=>(?[X53]:(activity(X53)&occurrence_of(X52,X53))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_18)).
% 52.17/52.35 fof(c120,plain,(![X52]:(~activity_occurrence(X52)|(?[X53]:(activity(X53)&occurrence_of(X52,X53))))),inference(fof_nnf,[status(thm)],[sos_18])).
% 52.17/52.35 fof(c121,plain,(![X51]:(~activity_occurrence(X51)|(?[X52]:(activity(X52)&occurrence_of(X51,X52))))),inference(variable_rename,[status(thm)],[c120])).
% 52.17/52.35 fof(c122,plain,(![X51]:(~activity_occurrence(X51)|(activity(skolem0012(X51))&occurrence_of(X51,skolem0012(X51))))),inference(skolemize,[status(esa)],[c121])).
% 52.17/52.35 fof(c123,plain,(![X51]:((~activity_occurrence(X51)|activity(skolem0012(X51)))&(~activity_occurrence(X51)|occurrence_of(X51,skolem0012(X51))))),inference(distribute,[status(thm)],[c122])).
% 52.17/52.35 cnf(c125,plain,~activity_occurrence(X186)|occurrence_of(X186,skolem0012(X186)),inference(split_conjunct,[status(thm)],[c123])).
% 52.17/52.35 fof(sos_19,axiom,(![X54]:(![X55]:(subactivity_occurrence(X54,X55)=>(activity_occurrence(X54)&activity_occurrence(X55))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_19)).
% 52.17/52.35 fof(c115,plain,(![X54]:(![X55]:(~subactivity_occurrence(X54,X55)|(activity_occurrence(X54)&activity_occurrence(X55))))),inference(fof_nnf,[status(thm)],[sos_19])).
% 52.17/52.35 fof(c116,plain,(![X49]:(![X50]:(~subactivity_occurrence(X49,X50)|(activity_occurrence(X49)&activity_occurrence(X50))))),inference(variable_rename,[status(thm)],[c115])).
% 52.17/52.35 fof(c117,plain,(![X49]:(![X50]:((~subactivity_occurrence(X49,X50)|activity_occurrence(X49))&(~subactivity_occurrence(X49,X50)|activity_occurrence(X50))))),inference(distribute,[status(thm)],[c116])).
% 52.17/52.35 cnf(c118,plain,~subactivity_occurrence(X147,X148)|activity_occurrence(X147),inference(split_conjunct,[status(thm)],[c117])).
% 52.17/52.35 fof(sos_10,axiom,(![X32]:(![X33]:(root_occ(X32,X33)<=>(?[X34]:((occurrence_of(X33,X34)&subactivity_occurrence(X32,X33))&root(X32,X34)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_10)).
% 52.17/52.35 fof(c172,plain,(![X32]:(![X33]:((~root_occ(X32,X33)|(?[X34]:((occurrence_of(X33,X34)&subactivity_occurrence(X32,X33))&root(X32,X34))))&((![X34]:((~occurrence_of(X33,X34)|~subactivity_occurrence(X32,X33))|~root(X32,X34)))|root_occ(X32,X33))))),inference(fof_nnf,[status(thm)],[sos_10])).
% 52.17/52.35 fof(c173,plain,((![X32]:(![X33]:(~root_occ(X32,X33)|(?[X34]:((occurrence_of(X33,X34)&subactivity_occurrence(X32,X33))&root(X32,X34))))))&(![X32]:(![X33]:((![X34]:((~occurrence_of(X33,X34)|~subactivity_occurrence(X32,X33))|~root(X32,X34)))|root_occ(X32,X33))))),inference(shift_quantors,[status(thm)],[c172])).
% 52.17/52.35 fof(c174,plain,((![X80]:(![X81]:(~root_occ(X80,X81)|(?[X82]:((occurrence_of(X81,X82)&subactivity_occurrence(X80,X81))&root(X80,X82))))))&(![X83]:(![X84]:((![X85]:((~occurrence_of(X84,X85)|~subactivity_occurrence(X83,X84))|~root(X83,X85)))|root_occ(X83,X84))))),inference(variable_rename,[status(thm)],[c173])).
% 52.17/52.35 fof(c176,plain,(![X80]:(![X81]:(![X83]:(![X84]:(![X85]:((~root_occ(X80,X81)|((occurrence_of(X81,skolem0017(X80,X81))&subactivity_occurrence(X80,X81))&root(X80,skolem0017(X80,X81))))&(((~occurrence_of(X84,X85)|~subactivity_occurrence(X83,X84))|~root(X83,X85))|root_occ(X83,X84)))))))),inference(shift_quantors,[status(thm)],[fof(c175,plain,((![X80]:(![X81]:(~root_occ(X80,X81)|((occurrence_of(X81,skolem0017(X80,X81))&subactivity_occurrence(X80,X81))&root(X80,skolem0017(X80,X81))))))&(![X83]:(![X84]:((![X85]:((~occurrence_of(X84,X85)|~subactivity_occurrence(X83,X84))|~root(X83,X85)))|root_occ(X83,X84))))),inference(skolemize,[status(esa)],[c174])).])).
% 52.17/52.35 fof(c177,plain,(![X80]:(![X81]:(![X83]:(![X84]:(![X85]:((((~root_occ(X80,X81)|occurrence_of(X81,skolem0017(X80,X81)))&(~root_occ(X80,X81)|subactivity_occurrence(X80,X81)))&(~root_occ(X80,X81)|root(X80,skolem0017(X80,X81))))&(((~occurrence_of(X84,X85)|~subactivity_occurrence(X83,X84))|~root(X83,X85))|root_occ(X83,X84)))))))),inference(distribute,[status(thm)],[c176])).
% 52.17/52.35 cnf(c179,plain,~root_occ(X163,X162)|subactivity_occurrence(X163,X162),inference(split_conjunct,[status(thm)],[c177])).
% 52.17/52.35 cnf(c261,plain,subactivity_occurrence(skolem0002(skolem0001),skolem0001),inference(resolution,[status(thm)],[c260, c179])).
% 52.17/52.35 cnf(c264,plain,activity_occurrence(skolem0002(skolem0001)),inference(resolution,[status(thm)],[c261, c118])).
% 52.17/52.35 cnf(c266,plain,occurrence_of(skolem0002(skolem0001),skolem0012(skolem0002(skolem0001))),inference(resolution,[status(thm)],[c264, c125])).
% 52.17/52.35 fof(sos_22,axiom,(![X64]:(![X65]:(![X66]:((occurrence_of(X64,X65)&occurrence_of(X64,X66))=>X65=X66)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_22)).
% 52.17/52.35 fof(c104,plain,(![X64]:(![X65]:(![X66]:((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)))),inference(fof_nnf,[status(thm)],[sos_22])).
% 52.17/52.35 fof(c105,plain,(![X38]:(![X39]:(![X40]:((~occurrence_of(X38,X39)|~occurrence_of(X38,X40))|X39=X40)))),inference(variable_rename,[status(thm)],[c104])).
% 52.17/52.35 cnf(c106,plain,~occurrence_of(X281,X279)|~occurrence_of(X281,X280)|X279=X280,inference(split_conjunct,[status(thm)],[c105])).
% 52.17/52.35 cnf(c299,plain,~occurrence_of(skolem0002(skolem0001),X311)|X311=tptp3,inference(resolution,[status(thm)],[c106, c273])).
% 52.17/52.35 cnf(c393,plain,skolem0012(skolem0002(skolem0001))=tptp3,inference(resolution,[status(thm)],[c299, c266])).
% 52.17/52.35 cnf(c3,axiom,X165!=X164|X166!=X167|~occurrence_of(X165,X166)|occurrence_of(X164,X167),theory(equality)).
% 52.17/52.35 cnf(c329,plain,skolem0002(skolem0001)!=X439|skolem0012(skolem0002(skolem0001))!=X438|occurrence_of(X439,X438),inference(resolution,[status(thm)],[c266, c3])).
% 52.17/52.35 cnf(c673,plain,skolem0002(skolem0001)!=X440|occurrence_of(X440,tptp3),inference(resolution,[status(thm)],[c329, c393])).
% 52.17/52.35 cnf(symmetry,axiom,X125!=X126|X126=X125,theory(equality)).
% 52.17/52.35 cnf(c178,plain,~root_occ(X266,X265)|occurrence_of(X265,skolem0017(X266,X265)),inference(split_conjunct,[status(thm)],[c177])).
% 52.17/52.35 fof(sos_34,axiom,(~atomic(tptp0)),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_34)).
% 52.17/52.35 fof(c36,plain,~atomic(tptp0),inference(fof_simplification,[status(thm)],[sos_34])).
% 52.17/52.35 cnf(c37,plain,~atomic(tptp0),inference(split_conjunct,[status(thm)],[c36])).
% 52.17/52.35 fof(sos_30,axiom,(![X91]:(![X92]:((occurrence_of(X92,X91)&(~atomic(X91)))=>(?[X93]:(root(X93,X91)&subactivity_occurrence(X93,X92)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_30)).
% 52.17/52.35 fof(c54,plain,(![X91]:(![X92]:((occurrence_of(X92,X91)&~atomic(X91))=>(?[X93]:(root(X93,X91)&subactivity_occurrence(X93,X92)))))),inference(fof_simplification,[status(thm)],[sos_30])).
% 52.17/52.35 fof(c55,plain,(![X91]:(![X92]:((~occurrence_of(X92,X91)|atomic(X91))|(?[X93]:(root(X93,X91)&subactivity_occurrence(X93,X92)))))),inference(fof_nnf,[status(thm)],[c54])).
% 52.17/52.35 fof(c56,plain,(![X11]:(![X12]:((~occurrence_of(X12,X11)|atomic(X11))|(?[X13]:(root(X13,X11)&subactivity_occurrence(X13,X12)))))),inference(variable_rename,[status(thm)],[c55])).
% 52.17/52.35 fof(c57,plain,(![X11]:(![X12]:((~occurrence_of(X12,X11)|atomic(X11))|(root(skolem0005(X11,X12),X11)&subactivity_occurrence(skolem0005(X11,X12),X12))))),inference(skolemize,[status(esa)],[c56])).
% 52.17/52.35 fof(c58,plain,(![X11]:(![X12]:(((~occurrence_of(X12,X11)|atomic(X11))|root(skolem0005(X11,X12),X11))&((~occurrence_of(X12,X11)|atomic(X11))|subactivity_occurrence(skolem0005(X11,X12),X12))))),inference(distribute,[status(thm)],[c57])).
% 52.17/52.35 cnf(c60,plain,~occurrence_of(X295,X294)|atomic(X294)|subactivity_occurrence(skolem0005(X294,X295),X295),inference(split_conjunct,[status(thm)],[c58])).
% 52.17/52.35 cnf(c334,plain,atomic(tptp0)|subactivity_occurrence(skolem0005(tptp0,skolem0001),skolem0001),inference(resolution,[status(thm)],[c60, c23])).
% 52.17/52.35 cnf(c532,plain,subactivity_occurrence(skolem0005(tptp0,skolem0001),skolem0001),inference(resolution,[status(thm)],[c334, c37])).
% 52.17/52.35 cnf(c181,plain,~occurrence_of(X375,X376)|~subactivity_occurrence(X377,X375)|~root(X377,X376)|root_occ(X377,X375),inference(split_conjunct,[status(thm)],[c177])).
% 52.17/52.35 cnf(c59,plain,~occurrence_of(X289,X288)|atomic(X288)|root(skolem0005(X288,X289),X288),inference(split_conjunct,[status(thm)],[c58])).
% 52.17/52.35 cnf(c321,plain,atomic(tptp0)|root(skolem0005(tptp0,skolem0001),tptp0),inference(resolution,[status(thm)],[c59, c23])).
% 52.17/52.35 cnf(c516,plain,root(skolem0005(tptp0,skolem0001),tptp0),inference(resolution,[status(thm)],[c321, c37])).
% 52.17/52.35 cnf(c527,plain,~occurrence_of(X545,tptp0)|~subactivity_occurrence(skolem0005(tptp0,skolem0001),X545)|root_occ(skolem0005(tptp0,skolem0001),X545),inference(resolution,[status(thm)],[c516, c181])).
% 52.17/52.35 cnf(c1359,plain,~occurrence_of(skolem0001,tptp0)|root_occ(skolem0005(tptp0,skolem0001),skolem0001),inference(resolution,[status(thm)],[c527, c532])).
% 52.17/52.35 cnf(c1675,plain,root_occ(skolem0005(tptp0,skolem0001),skolem0001),inference(resolution,[status(thm)],[c1359, c23])).
% 52.17/52.35 cnf(c1681,plain,occurrence_of(skolem0001,skolem0017(skolem0005(tptp0,skolem0001),skolem0001)),inference(resolution,[status(thm)],[c1675, c178])).
% 52.17/52.35 fof(sos_02,axiom,(![X7]:(![X8]:(![X9]:(![X10]:(((occurrence_of(X9,X10)&root_occ(X7,X9))&root_occ(X8,X9))=>X7=X8))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 52.17/52.35 fof(c226,plain,(![X7]:(![X8]:(![X9]:(![X10]:(((~occurrence_of(X9,X10)|~root_occ(X7,X9))|~root_occ(X8,X9))|X7=X8))))),inference(fof_nnf,[status(thm)],[sos_02])).
% 52.17/52.35 fof(c227,plain,(![X7]:(![X8]:((![X9]:(((![X10]:~occurrence_of(X9,X10))|~root_occ(X7,X9))|~root_occ(X8,X9)))|X7=X8))),inference(shift_quantors,[status(thm)],[c226])).
% 52.17/52.35 fof(c229,plain,(![X113]:(![X114]:(![X115]:(![X116]:(((~occurrence_of(X115,X116)|~root_occ(X113,X115))|~root_occ(X114,X115))|X113=X114))))),inference(shift_quantors,[status(thm)],[fof(c228,plain,(![X113]:(![X114]:((![X115]:(((![X116]:~occurrence_of(X115,X116))|~root_occ(X113,X115))|~root_occ(X114,X115)))|X113=X114))),inference(variable_rename,[status(thm)],[c227])).])).
% 52.17/52.35 cnf(c230,plain,~occurrence_of(X399,X398)|~root_occ(X397,X399)|~root_occ(X396,X399)|X397=X396,inference(split_conjunct,[status(thm)],[c229])).
% 52.17/52.35 cnf(c548,plain,~occurrence_of(skolem0001,X566)|~root_occ(X567,skolem0001)|X567=skolem0002(skolem0001),inference(resolution,[status(thm)],[c230, c260])).
% 52.17/52.35 cnf(c1676,plain,~occurrence_of(skolem0001,X605)|skolem0005(tptp0,skolem0001)=skolem0002(skolem0001),inference(resolution,[status(thm)],[c1675, c548])).
% 52.17/52.35 cnf(c1902,plain,skolem0005(tptp0,skolem0001)=skolem0002(skolem0001),inference(resolution,[status(thm)],[c1676, c1681])).
% 52.17/52.35 cnf(c1907,plain,skolem0002(skolem0001)=skolem0005(tptp0,skolem0001),inference(resolution,[status(thm)],[c1902, symmetry])).
% 52.17/52.35 cnf(c1926,plain,occurrence_of(skolem0005(tptp0,skolem0001),tptp3),inference(resolution,[status(thm)],[c1907, c673])).
% 52.17/52.35 cnf(c24,negated_conjecture,~occurrence_of(X273,tptp3)|~root_occ(X273,skolem0001)|~occurrence_of(X272,tptp2)|~min_precedes(X273,X272,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 52.17/52.35 cnf(reflexivity,axiom,X124=X124,theory(equality)).
% 52.17/52.35 cnf(c0,axiom,X132!=X134|X133!=X131|X135!=X136|~min_precedes(X132,X133,X135)|min_precedes(X134,X131,X136),theory(equality)).
% 52.17/52.35 cnf(c359,plain,skolem0002(skolem0001)!=X466|skolem0003(skolem0001)!=X464|tptp0!=X465|min_precedes(X466,X464,X465),inference(resolution,[status(thm)],[c291, c0])).
% 52.17/52.35 cnf(c858,plain,skolem0002(skolem0001)!=X775|tptp0!=X774|min_precedes(X775,skolem0003(skolem0001),X774),inference(resolution,[status(thm)],[c359, reflexivity])).
% 52.17/52.35 cnf(c3086,plain,tptp0!=X877|min_precedes(skolem0005(tptp0,skolem0001),skolem0003(skolem0001),X877),inference(resolution,[status(thm)],[c858, c1907])).
% 52.17/52.35 cnf(c3758,plain,min_precedes(skolem0005(tptp0,skolem0001),skolem0003(skolem0001),tptp0),inference(resolution,[status(thm)],[c3086, reflexivity])).
% 52.17/52.35 cnf(c3760,plain,min_precedes(skolem0005(tptp0,skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c3758, c561])).
% 52.17/52.35 cnf(c3798,plain,~occurrence_of(skolem0005(tptp0,skolem0001),tptp3)|~root_occ(skolem0005(tptp0,skolem0001),skolem0001)|~occurrence_of(skolem0004(skolem0001),tptp2),inference(resolution,[status(thm)],[c3760, c24])).
% 52.17/52.35 cnf(c24607,plain,~occurrence_of(skolem0005(tptp0,skolem0001),tptp3)|~occurrence_of(skolem0004(skolem0001),tptp2),inference(resolution,[status(thm)],[c3798, c1675])).
% 52.17/52.35 cnf(c24608,plain,~occurrence_of(skolem0004(skolem0001),tptp2),inference(resolution,[status(thm)],[c24607, c1926])).
% 52.17/52.35 cnf(c24615,plain,occurrence_of(skolem0004(skolem0001),tptp1),inference(resolution,[status(thm)],[c24608, c295])).
% 52.17/52.35 cnf(c24655,plain,~occurrence_of(skolem0002(skolem0001),tptp3)|~root_occ(skolem0002(skolem0001),skolem0001),inference(resolution,[status(thm)],[c24615, c1599])).
% 52.17/52.35 cnf(c24894,plain,~occurrence_of(skolem0002(skolem0001),tptp3),inference(resolution,[status(thm)],[c24655, c260])).
% 52.17/52.35 cnf(c24895,plain,$false,inference(resolution,[status(thm)],[c24894, c273])).
% 52.17/52.35 % SZS output end CNFRefutation
% 52.17/52.35
% 52.17/52.35 % Initial clauses : 105
% 52.17/52.35 % Processed clauses : 4247
% 52.17/52.35 % Factors computed : 42
% 52.17/52.35 % Resolvents computed: 24617
% 52.17/52.35 % Tautologies deleted: 25
% 52.17/52.35 % Forward subsumed : 4974
% 52.17/52.35 % Backward subsumed : 892
% 52.17/52.35 % -------- CPU Time ---------
% 52.17/52.35 % User time : 51.907 s
% 52.17/52.35 % System time : 0.093 s
% 52.17/52.35 % Total time : 52.000 s
%------------------------------------------------------------------------------