%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO014+2 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n020.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 175.59s 175.86s
% Output : Refutation 175.59s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.14 % Problem : PRO014+2 : TPTP v8.1.2. Released v4.0.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n020.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 03:22:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 175.59/175.86 % Version: 1.5
% 175.59/175.86 % SZS status Theorem
% 175.59/175.86 % SZS output start CNFRefutation
% 175.59/175.86 fof(goals,conjecture,(![X100]:(![X101]:((((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&(~leaf_occ(X100,X101)))=>(?[X102]:(?[X103]:((((occurrence_of(X102,tptp3)&next_subocc(X100,X102,tptp0))&(occurrence_of(X103,tptp2)|occurrence_of(X103,tptp1)))&min_precedes(X102,X103,tptp0))&leaf(X103,tptp0))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 175.59/175.86 fof(c17,negated_conjecture,(~(![X100]:(![X101]:((((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&(~leaf_occ(X100,X101)))=>(?[X102]:(?[X103]:((((occurrence_of(X102,tptp3)&next_subocc(X100,X102,tptp0))&(occurrence_of(X103,tptp2)|occurrence_of(X103,tptp1)))&min_precedes(X102,X103,tptp0))&leaf(X103,tptp0)))))))),inference(assume_negation,[status(cth)],[goals])).
% 175.59/175.86 fof(c18,negated_conjecture,(~(![X100]:(![X101]:((((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&~leaf_occ(X100,X101))=>(?[X102]:(?[X103]:((((occurrence_of(X102,tptp3)&next_subocc(X100,X102,tptp0))&(occurrence_of(X103,tptp2)|occurrence_of(X103,tptp1)))&min_precedes(X102,X103,tptp0))&leaf(X103,tptp0)))))))),inference(fof_simplification,[status(thm)],[c17])).
% 175.59/175.86 fof(c19,negated_conjecture,(?[X100]:(?[X101]:((((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&~leaf_occ(X100,X101))&(![X102]:(![X103]:((((~occurrence_of(X102,tptp3)|~next_subocc(X100,X102,tptp0))|(~occurrence_of(X103,tptp2)&~occurrence_of(X103,tptp1)))|~min_precedes(X102,X103,tptp0))|~leaf(X103,tptp0))))))),inference(fof_nnf,[status(thm)],[c18])).
% 175.59/175.86 fof(c20,negated_conjecture,(?[X100]:((?[X101]:(((occurrence_of(X101,tptp0)&subactivity_occurrence(X100,X101))&arboreal(X100))&~leaf_occ(X100,X101)))&(![X102]:(![X103]:((((~occurrence_of(X102,tptp3)|~next_subocc(X100,X102,tptp0))|(~occurrence_of(X103,tptp2)&~occurrence_of(X103,tptp1)))|~min_precedes(X102,X103,tptp0))|~leaf(X103,tptp0)))))),inference(shift_quantors,[status(thm)],[c19])).
% 175.59/175.86 fof(c21,negated_conjecture,(?[X2]:((?[X3]:(((occurrence_of(X3,tptp0)&subactivity_occurrence(X2,X3))&arboreal(X2))&~leaf_occ(X2,X3)))&(![X4]:(![X5]:((((~occurrence_of(X4,tptp3)|~next_subocc(X2,X4,tptp0))|(~occurrence_of(X5,tptp2)&~occurrence_of(X5,tptp1)))|~min_precedes(X4,X5,tptp0))|~leaf(X5,tptp0)))))),inference(variable_rename,[status(thm)],[c20])).
% 175.59/175.86 fof(c23,negated_conjecture,(![X4]:(![X5]:((((occurrence_of(skolem0002,tptp0)&subactivity_occurrence(skolem0001,skolem0002))&arboreal(skolem0001))&~leaf_occ(skolem0001,skolem0002))&((((~occurrence_of(X4,tptp3)|~next_subocc(skolem0001,X4,tptp0))|(~occurrence_of(X5,tptp2)&~occurrence_of(X5,tptp1)))|~min_precedes(X4,X5,tptp0))|~leaf(X5,tptp0))))),inference(shift_quantors,[status(thm)],[fof(c22,negated_conjecture,((((occurrence_of(skolem0002,tptp0)&subactivity_occurrence(skolem0001,skolem0002))&arboreal(skolem0001))&~leaf_occ(skolem0001,skolem0002))&(![X4]:(![X5]:((((~occurrence_of(X4,tptp3)|~next_subocc(skolem0001,X4,tptp0))|(~occurrence_of(X5,tptp2)&~occurrence_of(X5,tptp1)))|~min_precedes(X4,X5,tptp0))|~leaf(X5,tptp0))))),inference(skolemize,[status(esa)],[c21])).])).
% 175.59/175.86 fof(c24,negated_conjecture,(![X4]:(![X5]:((((occurrence_of(skolem0002,tptp0)&subactivity_occurrence(skolem0001,skolem0002))&arboreal(skolem0001))&~leaf_occ(skolem0001,skolem0002))&(((((~occurrence_of(X4,tptp3)|~next_subocc(skolem0001,X4,tptp0))|~occurrence_of(X5,tptp2))|~min_precedes(X4,X5,tptp0))|~leaf(X5,tptp0))&((((~occurrence_of(X4,tptp3)|~next_subocc(skolem0001,X4,tptp0))|~occurrence_of(X5,tptp1))|~min_precedes(X4,X5,tptp0))|~leaf(X5,tptp0)))))),inference(distribute,[status(thm)],[c23])).
% 175.59/175.86 cnf(c28,negated_conjecture,~leaf_occ(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c24])).
% 175.59/175.86 cnf(c27,negated_conjecture,arboreal(skolem0001),inference(split_conjunct,[status(thm)],[c24])).
% 175.59/175.86 cnf(c25,negated_conjecture,occurrence_of(skolem0002,tptp0),inference(split_conjunct,[status(thm)],[c24])).
% 175.59/175.86 cnf(c26,negated_conjecture,subactivity_occurrence(skolem0001,skolem0002),inference(split_conjunct,[status(thm)],[c24])).
% 175.59/175.86 fof(sos_32,axiom,(![X95]:(![X96]:((((occurrence_of(X96,tptp0)&subactivity_occurrence(X95,X96))&arboreal(X95))&(~leaf_occ(X95,X96)))=>(?[X97]:(?[X98]:(?[X99]:((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&next_subocc(X98,X99,tptp0))&leaf(X99,tptp0)))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_32)).
% 175.59/175.86 fof(c44,plain,(![X95]:(![X96]:((((occurrence_of(X96,tptp0)&subactivity_occurrence(X95,X96))&arboreal(X95))&~leaf_occ(X95,X96))=>(?[X97]:(?[X98]:(?[X99]:((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&next_subocc(X98,X99,tptp0))&leaf(X99,tptp0)))))))),inference(fof_simplification,[status(thm)],[sos_32])).
% 175.59/175.86 fof(c45,plain,(![X95]:(![X96]:((((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96))|(?[X97]:(?[X98]:(?[X99]:((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&next_subocc(X98,X99,tptp0))&leaf(X99,tptp0)))))))),inference(fof_nnf,[status(thm)],[c44])).
% 175.59/175.86 fof(c46,plain,(![X95]:((![X96]:(((~occurrence_of(X96,tptp0)|~subactivity_occurrence(X95,X96))|~arboreal(X95))|leaf_occ(X95,X96)))|(?[X97]:(?[X98]:(?[X99]:((((((occurrence_of(X97,tptp3)&next_subocc(X95,X97,tptp0))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0))&(occurrence_of(X99,tptp2)|occurrence_of(X99,tptp1)))&next_subocc(X98,X99,tptp0))&leaf(X99,tptp0))))))),inference(shift_quantors,[status(thm)],[c45])).
% 175.59/175.86 fof(c47,plain,(![X6]:((![X7]:(((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7)))|(?[X8]:(?[X9]:(?[X10]:((((((occurrence_of(X8,tptp3)&next_subocc(X6,X8,tptp0))&occurrence_of(X9,tptp4))&next_subocc(X8,X9,tptp0))&(occurrence_of(X10,tptp2)|occurrence_of(X10,tptp1)))&next_subocc(X9,X10,tptp0))&leaf(X10,tptp0))))))),inference(variable_rename,[status(thm)],[c46])).
% 175.59/175.86 fof(c49,plain,(![X6]:(![X7]:((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|((((((occurrence_of(skolem0003(X6),tptp3)&next_subocc(X6,skolem0003(X6),tptp0))&occurrence_of(skolem0004(X6),tptp4))&next_subocc(skolem0003(X6),skolem0004(X6),tptp0))&(occurrence_of(skolem0005(X6),tptp2)|occurrence_of(skolem0005(X6),tptp1)))&next_subocc(skolem0004(X6),skolem0005(X6),tptp0))&leaf(skolem0005(X6),tptp0))))),inference(shift_quantors,[status(thm)],[fof(c48,plain,(![X6]:((![X7]:(((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7)))|((((((occurrence_of(skolem0003(X6),tptp3)&next_subocc(X6,skolem0003(X6),tptp0))&occurrence_of(skolem0004(X6),tptp4))&next_subocc(skolem0003(X6),skolem0004(X6),tptp0))&(occurrence_of(skolem0005(X6),tptp2)|occurrence_of(skolem0005(X6),tptp1)))&next_subocc(skolem0004(X6),skolem0005(X6),tptp0))&leaf(skolem0005(X6),tptp0)))),inference(skolemize,[status(esa)],[c47])).])).
% 175.59/175.86 fof(c50,plain,(![X6]:(![X7]:((((((((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|occurrence_of(skolem0003(X6),tptp3))&((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|next_subocc(X6,skolem0003(X6),tptp0)))&((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|occurrence_of(skolem0004(X6),tptp4)))&((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|next_subocc(skolem0003(X6),skolem0004(X6),tptp0)))&((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|(occurrence_of(skolem0005(X6),tptp2)|occurrence_of(skolem0005(X6),tptp1))))&((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|next_subocc(skolem0004(X6),skolem0005(X6),tptp0)))&((((~occurrence_of(X7,tptp0)|~subactivity_occurrence(X6,X7))|~arboreal(X6))|leaf_occ(X6,X7))|leaf(skolem0005(X6),tptp0))))),inference(distribute,[status(thm)],[c49])).
% 175.59/175.86 cnf(c51,plain,~occurrence_of(X282,tptp0)|~subactivity_occurrence(X281,X282)|~arboreal(X281)|leaf_occ(X281,X282)|occurrence_of(skolem0003(X281),tptp3),inference(split_conjunct,[status(thm)],[c50])).
% 175.59/175.86 cnf(c301,plain,~occurrence_of(skolem0002,tptp0)|~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|occurrence_of(skolem0003(skolem0001),tptp3),inference(resolution,[status(thm)],[c51, c26])).
% 175.59/175.86 cnf(c410,plain,~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|occurrence_of(skolem0003(skolem0001),tptp3),inference(resolution,[status(thm)],[c301, c25])).
% 175.59/175.86 cnf(c655,plain,leaf_occ(skolem0001,skolem0002)|occurrence_of(skolem0003(skolem0001),tptp3),inference(resolution,[status(thm)],[c410, c27])).
% 175.59/175.86 cnf(c660,plain,occurrence_of(skolem0003(skolem0001),tptp3),inference(resolution,[status(thm)],[c655, c28])).
% 175.59/175.86 cnf(c55,plain,~occurrence_of(X301,tptp0)|~subactivity_occurrence(X300,X301)|~arboreal(X300)|leaf_occ(X300,X301)|occurrence_of(skolem0005(X300),tptp2)|occurrence_of(skolem0005(X300),tptp1),inference(split_conjunct,[status(thm)],[c50])).
% 175.59/175.86 cnf(c313,plain,~occurrence_of(skolem0002,tptp0)|~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|occurrence_of(skolem0005(skolem0001),tptp2)|occurrence_of(skolem0005(skolem0001),tptp1),inference(resolution,[status(thm)],[c55, c26])).
% 175.59/175.86 cnf(c474,plain,~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|occurrence_of(skolem0005(skolem0001),tptp2)|occurrence_of(skolem0005(skolem0001),tptp1),inference(resolution,[status(thm)],[c313, c25])).
% 175.59/175.86 cnf(c1234,plain,leaf_occ(skolem0001,skolem0002)|occurrence_of(skolem0005(skolem0001),tptp2)|occurrence_of(skolem0005(skolem0001),tptp1),inference(resolution,[status(thm)],[c474, c27])).
% 175.59/175.86 cnf(c4541,plain,occurrence_of(skolem0005(skolem0001),tptp2)|occurrence_of(skolem0005(skolem0001),tptp1),inference(resolution,[status(thm)],[c1234, c28])).
% 175.59/175.86 cnf(c57,plain,~occurrence_of(X335,tptp0)|~subactivity_occurrence(X334,X335)|~arboreal(X334)|leaf_occ(X334,X335)|leaf(skolem0005(X334),tptp0),inference(split_conjunct,[status(thm)],[c50])).
% 175.59/175.86 cnf(c321,plain,~occurrence_of(skolem0002,tptp0)|~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c57, c26])).
% 175.59/175.86 cnf(c504,plain,~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c321, c25])).
% 175.59/175.86 cnf(c1285,plain,leaf_occ(skolem0001,skolem0002)|leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c504, c27])).
% 175.59/175.86 cnf(c1291,plain,leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c1285, c28])).
% 175.59/175.86 cnf(c52,plain,~occurrence_of(X284,tptp0)|~subactivity_occurrence(X283,X284)|~arboreal(X283)|leaf_occ(X283,X284)|next_subocc(X283,skolem0003(X283),tptp0),inference(split_conjunct,[status(thm)],[c50])).
% 175.59/175.86 cnf(c302,plain,~occurrence_of(skolem0002,tptp0)|~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0001,skolem0003(skolem0001),tptp0),inference(resolution,[status(thm)],[c52, c26])).
% 175.59/175.86 cnf(c414,plain,~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0001,skolem0003(skolem0001),tptp0),inference(resolution,[status(thm)],[c302, c25])).
% 175.59/175.86 cnf(c810,plain,leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0001,skolem0003(skolem0001),tptp0),inference(resolution,[status(thm)],[c414, c27])).
% 175.59/175.86 cnf(c877,plain,next_subocc(skolem0001,skolem0003(skolem0001),tptp0),inference(resolution,[status(thm)],[c810, c28])).
% 175.59/175.86 cnf(c30,negated_conjecture,~occurrence_of(X279,tptp3)|~next_subocc(skolem0001,X279,tptp0)|~occurrence_of(X280,tptp1)|~min_precedes(X279,X280,tptp0)|~leaf(X280,tptp0),inference(split_conjunct,[status(thm)],[c24])).
% 175.59/175.86 fof(sos_04,axiom,(![X15]:(![X16]:(![X17]:(next_subocc(X15,X16,X17)<=>(min_precedes(X15,X16,X17)&(~(?[X18]:(min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_04)).
% 175.59/175.86 fof(c216,plain,(![X15]:(![X16]:(![X17]:((~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]:(~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17)))))&((~min_precedes(X15,X16,X17)|(?[X18]:(min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))|next_subocc(X15,X16,X17)))))),inference(fof_nnf,[status(thm)],[sos_04])).
% 175.59/175.86 fof(c217,plain,((![X15]:(![X16]:(![X17]:(~next_subocc(X15,X16,X17)|(min_precedes(X15,X16,X17)&(![X18]:(~min_precedes(X15,X18,X17)|~min_precedes(X18,X16,X17))))))))&(![X15]:(![X16]:(![X17]:((~min_precedes(X15,X16,X17)|(?[X18]:(min_precedes(X15,X18,X17)&min_precedes(X18,X16,X17))))|next_subocc(X15,X16,X17)))))),inference(shift_quantors,[status(thm)],[c216])).
% 175.59/175.86 fof(c218,plain,((![X102]:(![X103]:(![X104]:(~next_subocc(X102,X103,X104)|(min_precedes(X102,X103,X104)&(![X105]:(~min_precedes(X102,X105,X104)|~min_precedes(X105,X103,X104))))))))&(![X106]:(![X107]:(![X108]:((~min_precedes(X106,X107,X108)|(?[X109]:(min_precedes(X106,X109,X108)&min_precedes(X109,X107,X108))))|next_subocc(X106,X107,X108)))))),inference(variable_rename,[status(thm)],[c217])).
% 175.59/175.86 fof(c220,plain,(![X102]:(![X103]:(![X104]:(![X105]:(![X106]:(![X107]:(![X108]:((~next_subocc(X102,X103,X104)|(min_precedes(X102,X103,X104)&(~min_precedes(X102,X105,X104)|~min_precedes(X105,X103,X104))))&((~min_precedes(X106,X107,X108)|(min_precedes(X106,skolem0019(X106,X107,X108),X108)&min_precedes(skolem0019(X106,X107,X108),X107,X108)))|next_subocc(X106,X107,X108)))))))))),inference(shift_quantors,[status(thm)],[fof(c219,plain,((![X102]:(![X103]:(![X104]:(~next_subocc(X102,X103,X104)|(min_precedes(X102,X103,X104)&(![X105]:(~min_precedes(X102,X105,X104)|~min_precedes(X105,X103,X104))))))))&(![X106]:(![X107]:(![X108]:((~min_precedes(X106,X107,X108)|(min_precedes(X106,skolem0019(X106,X107,X108),X108)&min_precedes(skolem0019(X106,X107,X108),X107,X108)))|next_subocc(X106,X107,X108)))))),inference(skolemize,[status(esa)],[c218])).])).
% 175.59/175.86 fof(c221,plain,(![X102]:(![X103]:(![X104]:(![X105]:(![X106]:(![X107]:(![X108]:(((~next_subocc(X102,X103,X104)|min_precedes(X102,X103,X104))&(~next_subocc(X102,X103,X104)|(~min_precedes(X102,X105,X104)|~min_precedes(X105,X103,X104))))&(((~min_precedes(X106,X107,X108)|min_precedes(X106,skolem0019(X106,X107,X108),X108))|next_subocc(X106,X107,X108))&((~min_precedes(X106,X107,X108)|min_precedes(skolem0019(X106,X107,X108),X107,X108))|next_subocc(X106,X107,X108))))))))))),inference(distribute,[status(thm)],[c220])).
% 175.59/175.86 cnf(c222,plain,~next_subocc(X236,X238,X237)|min_precedes(X236,X238,X237),inference(split_conjunct,[status(thm)],[c221])).
% 175.59/175.86 cnf(c54,plain,~occurrence_of(X295,tptp0)|~subactivity_occurrence(X294,X295)|~arboreal(X294)|leaf_occ(X294,X295)|next_subocc(skolem0003(X294),skolem0004(X294),tptp0),inference(split_conjunct,[status(thm)],[c50])).
% 175.59/175.86 cnf(c310,plain,~occurrence_of(skolem0002,tptp0)|~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0003(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c54, c26])).
% 175.59/175.86 cnf(c455,plain,~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0003(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c310, c25])).
% 175.59/175.86 cnf(c1109,plain,leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0003(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c455, c27])).
% 175.59/175.86 cnf(c1656,plain,next_subocc(skolem0003(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c1109, c28])).
% 175.59/175.86 cnf(c1665,plain,min_precedes(skolem0003(skolem0001),skolem0004(skolem0001),tptp0),inference(resolution,[status(thm)],[c1656, c222])).
% 175.59/175.86 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/sandbox2/benchmark/theBenchmark.p', sos)).
% 175.59/175.86 fof(c240,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])).
% 175.59/175.86 fof(c241,plain,(![X121]:(![X122]:(![X123]:(![X124]:((~min_precedes(X121,X122,X124)|~min_precedes(X122,X123,X124))|min_precedes(X121,X123,X124)))))),inference(variable_rename,[status(thm)],[c240])).
% 175.59/175.86 cnf(c242,plain,~min_precedes(X385,X386,X384)|~min_precedes(X386,X383,X384)|min_precedes(X385,X383,X384),inference(split_conjunct,[status(thm)],[c241])).
% 175.59/175.86 cnf(c56,plain,~occurrence_of(X318,tptp0)|~subactivity_occurrence(X317,X318)|~arboreal(X317)|leaf_occ(X317,X318)|next_subocc(skolem0004(X317),skolem0005(X317),tptp0),inference(split_conjunct,[status(thm)],[c50])).
% 175.59/175.86 cnf(c314,plain,~occurrence_of(skolem0002,tptp0)|~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0004(skolem0001),skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c56, c26])).
% 175.59/175.86 cnf(c486,plain,~arboreal(skolem0001)|leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0004(skolem0001),skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c314, c25])).
% 175.59/175.86 cnf(c1361,plain,leaf_occ(skolem0001,skolem0002)|next_subocc(skolem0004(skolem0001),skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c486, c27])).
% 175.59/175.86 cnf(c2139,plain,next_subocc(skolem0004(skolem0001),skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c1361, c28])).
% 175.59/175.86 cnf(c2148,plain,min_precedes(skolem0004(skolem0001),skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2139, c222])).
% 175.59/175.86 cnf(c2166,plain,~min_precedes(X677,skolem0004(skolem0001),tptp0)|min_precedes(X677,skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2148, c242])).
% 175.59/175.86 cnf(c2627,plain,min_precedes(skolem0003(skolem0001),skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2166, c1665])).
% 175.59/175.86 cnf(c2648,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|~next_subocc(skolem0001,skolem0003(skolem0001),tptp0)|~occurrence_of(skolem0005(skolem0001),tptp1)|~leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2627, c30])).
% 175.59/175.86 cnf(c22864,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|~occurrence_of(skolem0005(skolem0001),tptp1)|~leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2648, c877])).
% 175.59/175.86 cnf(c51076,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|~occurrence_of(skolem0005(skolem0001),tptp1),inference(resolution,[status(thm)],[c22864, c1291])).
% 175.59/175.86 cnf(c51079,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|occurrence_of(skolem0005(skolem0001),tptp2),inference(resolution,[status(thm)],[c51076, c4541])).
% 175.59/175.86 cnf(c51235,plain,occurrence_of(skolem0005(skolem0001),tptp2),inference(resolution,[status(thm)],[c51079, c660])).
% 175.59/175.86 cnf(c29,negated_conjecture,~occurrence_of(X274,tptp3)|~next_subocc(skolem0001,X274,tptp0)|~occurrence_of(X275,tptp2)|~min_precedes(X274,X275,tptp0)|~leaf(X275,tptp0),inference(split_conjunct,[status(thm)],[c24])).
% 175.59/175.86 cnf(c2662,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|~next_subocc(skolem0001,skolem0003(skolem0001),tptp0)|~occurrence_of(skolem0005(skolem0001),tptp2)|~leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2627, c29])).
% 175.59/175.86 cnf(c22937,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|~occurrence_of(skolem0005(skolem0001),tptp2)|~leaf(skolem0005(skolem0001),tptp0),inference(resolution,[status(thm)],[c2662, c877])).
% 175.59/175.86 cnf(c53797,plain,~occurrence_of(skolem0003(skolem0001),tptp3)|~occurrence_of(skolem0005(skolem0001),tptp2),inference(resolution,[status(thm)],[c22937, c1291])).
% 175.59/175.86 cnf(c53798,plain,~occurrence_of(skolem0003(skolem0001),tptp3),inference(resolution,[status(thm)],[c53797, c51235])).
% 175.59/175.86 cnf(c53799,plain,$false,inference(resolution,[status(thm)],[c53798, c660])).
% 175.59/175.86 % SZS output end CNFRefutation
% 175.59/175.86
% 175.59/175.86 % Initial clauses : 108
% 175.59/175.86 % Processed clauses : 6596
% 175.59/175.86 % Factors computed : 60
% 175.59/175.86 % Resolvents computed: 53497
% 175.59/175.86 % Tautologies deleted: 51
% 175.59/175.86 % Forward subsumed : 8651
% 175.59/175.86 % Backward subsumed : 1839
% 175.59/175.86 % -------- CPU Time ---------
% 175.59/175.86 % User time : 175.238 s
% 175.59/175.86 % System time : 0.184 s
% 175.59/175.86 % Total time : 175.422 s
%------------------------------------------------------------------------------