%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO010+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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.28s 1.47s
% Output : Refutation 1.28s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PRO010+1 : TPTP v8.1.2. Released v4.0.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n009.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 03:28:23 EDT 2024
% 0.12/0.34 % CPUTime :
% 1.28/1.47 % Version: 1.5
% 1.28/1.47 % SZS status Theorem
% 1.28/1.47 % SZS output start CNFRefutation
% 1.28/1.47 fof(sos_47,axiom,tptp1!=tptp2,file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_47)).
% 1.28/1.47 cnf(c33,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_47])).
% 1.28/1.47 cnf(symmetry,axiom,X137!=X136|X136=X137,theory(equality)).
% 1.28/1.47 fof(sos_21,axiom,(![X56]:(![X57]:(leaf(X56,X57)<=>((root(X56,X57)|(?[X58]:min_precedes(X58,X56,X57)))&(~(?[X59]:min_precedes(X56,X59,X57))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_21)).
% 1.28/1.47 fof(c145,plain,(![X56]:(![X57]:((~leaf(X56,X57)|((root(X56,X57)|(?[X58]:min_precedes(X58,X56,X57)))&(![X59]:~min_precedes(X56,X59,X57))))&(((~root(X56,X57)&(![X58]:~min_precedes(X58,X56,X57)))|(?[X59]:min_precedes(X56,X59,X57)))|leaf(X56,X57))))),inference(fof_nnf,[status(thm)],[sos_21])).
% 1.28/1.47 fof(c146,plain,((![X56]:(![X57]:(~leaf(X56,X57)|((root(X56,X57)|(?[X58]:min_precedes(X58,X56,X57)))&(![X59]:~min_precedes(X56,X59,X57))))))&(![X56]:(![X57]:(((~root(X56,X57)&(![X58]:~min_precedes(X58,X56,X57)))|(?[X59]:min_precedes(X56,X59,X57)))|leaf(X56,X57))))),inference(shift_quantors,[status(thm)],[c145])).
% 1.28/1.47 fof(c147,plain,((![X69]:(![X70]:(~leaf(X69,X70)|((root(X69,X70)|(?[X71]:min_precedes(X71,X69,X70)))&(![X72]:~min_precedes(X69,X72,X70))))))&(![X73]:(![X74]:(((~root(X73,X74)&(![X75]:~min_precedes(X75,X73,X74)))|(?[X76]:min_precedes(X73,X76,X74)))|leaf(X73,X74))))),inference(variable_rename,[status(thm)],[c146])).
% 1.28/1.47 fof(c149,plain,(![X69]:(![X70]:(![X72]:(![X73]:(![X74]:(![X75]:((~leaf(X69,X70)|((root(X69,X70)|min_precedes(skolem0015(X69,X70),X69,X70))&~min_precedes(X69,X72,X70)))&(((~root(X73,X74)&~min_precedes(X75,X73,X74))|min_precedes(X73,skolem0016(X73,X74),X74))|leaf(X73,X74))))))))),inference(shift_quantors,[status(thm)],[fof(c148,plain,((![X69]:(![X70]:(~leaf(X69,X70)|((root(X69,X70)|min_precedes(skolem0015(X69,X70),X69,X70))&(![X72]:~min_precedes(X69,X72,X70))))))&(![X73]:(![X74]:(((~root(X73,X74)&(![X75]:~min_precedes(X75,X73,X74)))|min_precedes(X73,skolem0016(X73,X74),X74))|leaf(X73,X74))))),inference(skolemize,[status(esa)],[c147])).])).
% 1.28/1.47 fof(c150,plain,(![X69]:(![X70]:(![X72]:(![X73]:(![X74]:(![X75]:(((~leaf(X69,X70)|(root(X69,X70)|min_precedes(skolem0015(X69,X70),X69,X70)))&(~leaf(X69,X70)|~min_precedes(X69,X72,X70)))&(((~root(X73,X74)|min_precedes(X73,skolem0016(X73,X74),X74))|leaf(X73,X74))&((~min_precedes(X75,X73,X74)|min_precedes(X73,skolem0016(X73,X74),X74))|leaf(X73,X74)))))))))),inference(distribute,[status(thm)],[c149])).
% 1.28/1.47 cnf(c152,plain,~leaf(X192,X191)|~min_precedes(X192,X190,X191),inference(split_conjunct,[status(thm)],[c150])).
% 1.28/1.47 fof(goals,conjecture,(![X109]:(occurrence_of(X109,tptp0)=>(?[X110]:(?[X111]:((leaf_occ(X111,X109)&(occurrence_of(X111,tptp1)=>(~(?[X112]:(occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0))))))&(occurrence_of(X111,tptp2)=>(~(?[X113]:(occurrence_of(X113,tptp1)&min_precedes(X110,X113,tptp0)))))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 1.28/1.47 fof(c17,negated_conjecture,(~(![X109]:(occurrence_of(X109,tptp0)=>(?[X110]:(?[X111]:((leaf_occ(X111,X109)&(occurrence_of(X111,tptp1)=>(~(?[X112]:(occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0))))))&(occurrence_of(X111,tptp2)=>(~(?[X113]:(occurrence_of(X113,tptp1)&min_precedes(X110,X113,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 1.28/1.47 fof(c18,negated_conjecture,(?[X109]:(occurrence_of(X109,tptp0)&(![X110]:(![X111]:((~leaf_occ(X111,X109)|(occurrence_of(X111,tptp1)&(?[X112]:(occurrence_of(X112,tptp2)&min_precedes(X110,X112,tptp0)))))|(occurrence_of(X111,tptp2)&(?[X113]:(occurrence_of(X113,tptp1)&min_precedes(X110,X113,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 1.28/1.47 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.28/1.47 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.28/1.47 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.28/1.47 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.28/1.47 fof(sos_35,axiom,(![X105]:(occurrence_of(X105,tptp0)=>(?[X106]:(?[X107]:(?[X108]:((((((occurrence_of(X106,tptp3)&root_occ(X106,X105))&occurrence_of(X107,tptp4))&next_subocc(X106,X107,tptp0))&(occurrence_of(X108,tptp1)|occurrence_of(X108,tptp2)))&next_subocc(X107,X108,tptp0))&leaf_occ(X108,X105))))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_35)).
% 1.28/1.47 fof(c46,plain,(![X105]:(~occurrence_of(X105,tptp0)|(?[X106]:(?[X107]:(?[X108]:((((((occurrence_of(X106,tptp3)&root_occ(X106,X105))&occurrence_of(X107,tptp4))&next_subocc(X106,X107,tptp0))&(occurrence_of(X108,tptp1)|occurrence_of(X108,tptp2)))&next_subocc(X107,X108,tptp0))&leaf_occ(X108,X105))))))),inference(fof_nnf,[status(thm)],[sos_35])).
% 1.28/1.47 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.28/1.47 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.28/1.47 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.28/1.47 cnf(c56,plain,~occurrence_of(X239,tptp0)|leaf_occ(skolem0006(X239),X239),inference(split_conjunct,[status(thm)],[c49])).
% 1.28/1.47 cnf(c280,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c56, c23])).
% 1.28/1.47 cnf(c30,negated_conjecture,~leaf_occ(X309,skolem0001)|min_precedes(X310,skolem0002(X310,X309),tptp0)|occurrence_of(X309,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 1.28/1.47 cnf(c359,plain,min_precedes(X481,skolem0002(X481,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c30, c280])).
% 1.28/1.47 cnf(c908,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~leaf(X482,tptp0),inference(resolution,[status(thm)],[c359, c152])).
% 1.28/1.47 cnf(reflexivity,axiom,X135=X135,theory(equality)).
% 1.28/1.47 fof(sos_02,axiom,(![X4]:(![X5]:(![X6]:((occurrence_of(X4,X5)&occurrence_of(X4,X6))=>X5=X6)))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 1.28/1.47 fof(c234,plain,(![X4]:(![X5]:(![X6]:((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)))),inference(fof_nnf,[status(thm)],[sos_02])).
% 1.28/1.47 fof(c235,plain,(![X128]:(![X129]:(![X130]:((~occurrence_of(X128,X129)|~occurrence_of(X128,X130))|X129=X130)))),inference(variable_rename,[status(thm)],[c234])).
% 1.28/1.47 cnf(c236,plain,~occurrence_of(X297,X296)|~occurrence_of(X297,X295)|X296=X295,inference(split_conjunct,[status(thm)],[c235])).
% 1.28/1.47 cnf(c323,plain,~occurrence_of(skolem0001,X300)|X300=tptp0,inference(resolution,[status(thm)],[c236, c23])).
% 1.28/1.47 fof(sos_34,axiom,(![X102]:(![X103]:(leaf_occ(X102,X103)<=>(?[X104]:((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104)))))),file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_34)).
% 1.28/1.47 fof(c57,plain,(![X102]:(![X103]:((~leaf_occ(X102,X103)|(?[X104]:((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104))))&((![X104]:((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))|leaf_occ(X102,X103))))),inference(fof_nnf,[status(thm)],[sos_34])).
% 1.28/1.47 fof(c58,plain,((![X102]:(![X103]:(~leaf_occ(X102,X103)|(?[X104]:((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104))))))&(![X102]:(![X103]:((![X104]:((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))|leaf_occ(X102,X103))))),inference(shift_quantors,[status(thm)],[c57])).
% 1.28/1.47 fof(c59,plain,((![X11]:(![X12]:(~leaf_occ(X11,X12)|(?[X13]:((occurrence_of(X12,X13)&subactivity_occurrence(X11,X12))&leaf(X11,X13))))))&(![X14]:(![X15]:((![X16]:((~occurrence_of(X15,X16)|~subactivity_occurrence(X14,X15))|~leaf(X14,X16)))|leaf_occ(X14,X15))))),inference(variable_rename,[status(thm)],[c58])).
% 1.28/1.47 fof(c61,plain,(![X11]:(![X12]:(![X14]:(![X15]:(![X16]:((~leaf_occ(X11,X12)|((occurrence_of(X12,skolem0007(X11,X12))&subactivity_occurrence(X11,X12))&leaf(X11,skolem0007(X11,X12))))&(((~occurrence_of(X15,X16)|~subactivity_occurrence(X14,X15))|~leaf(X14,X16))|leaf_occ(X14,X15)))))))),inference(shift_quantors,[status(thm)],[fof(c60,plain,((![X11]:(![X12]:(~leaf_occ(X11,X12)|((occurrence_of(X12,skolem0007(X11,X12))&subactivity_occurrence(X11,X12))&leaf(X11,skolem0007(X11,X12))))))&(![X14]:(![X15]:((![X16]:((~occurrence_of(X15,X16)|~subactivity_occurrence(X14,X15))|~leaf(X14,X16)))|leaf_occ(X14,X15))))),inference(skolemize,[status(esa)],[c59])).])).
% 1.28/1.47 fof(c62,plain,(![X11]:(![X12]:(![X14]:(![X15]:(![X16]:((((~leaf_occ(X11,X12)|occurrence_of(X12,skolem0007(X11,X12)))&(~leaf_occ(X11,X12)|subactivity_occurrence(X11,X12)))&(~leaf_occ(X11,X12)|leaf(X11,skolem0007(X11,X12))))&(((~occurrence_of(X15,X16)|~subactivity_occurrence(X14,X15))|~leaf(X14,X16))|leaf_occ(X14,X15)))))))),inference(distribute,[status(thm)],[c61])).
% 1.28/1.47 cnf(c63,plain,~leaf_occ(X245,X244)|occurrence_of(X244,skolem0007(X245,X244)),inference(split_conjunct,[status(thm)],[c62])).
% 1.28/1.47 cnf(c287,plain,occurrence_of(skolem0001,skolem0007(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c63, c280])).
% 1.28/1.47 cnf(c363,plain,skolem0007(skolem0006(skolem0001),skolem0001)=tptp0,inference(resolution,[status(thm)],[c287, c323])).
% 1.28/1.47 cnf(c12,axiom,X243!=X242|X240!=X241|~leaf(X243,X240)|leaf(X242,X241),theory(equality)).
% 1.28/1.47 cnf(c65,plain,~leaf_occ(X247,X246)|leaf(X247,skolem0007(X247,X246)),inference(split_conjunct,[status(thm)],[c62])).
% 1.28/1.47 cnf(c288,plain,leaf(skolem0006(skolem0001),skolem0007(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c65, c280])).
% 1.28/1.47 cnf(c591,plain,skolem0006(skolem0001)!=X674|skolem0007(skolem0006(skolem0001),skolem0001)!=X675|leaf(X674,X675),inference(resolution,[status(thm)],[c288, c12])).
% 1.28/1.47 cnf(c1799,plain,skolem0006(skolem0001)!=X676|leaf(X676,tptp0),inference(resolution,[status(thm)],[c591, c363])).
% 1.28/1.47 cnf(c1801,plain,leaf(skolem0006(skolem0001),tptp0),inference(resolution,[status(thm)],[c1799, reflexivity])).
% 1.28/1.47 cnf(c1808,plain,occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c1801, c908])).
% 1.28/1.47 cnf(c26,negated_conjecture,~leaf_occ(X301,skolem0001)|occurrence_of(X301,tptp1)|min_precedes(X302,skolem0003(X302,X301),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.28/1.47 cnf(c329,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X469,skolem0003(X469,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c26, c280])).
% 1.28/1.47 cnf(c765,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~leaf(X471,tptp0),inference(resolution,[status(thm)],[c329, c152])).
% 1.28/1.47 cnf(c1807,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c1801, c765])).
% 1.28/1.47 cnf(c1813,plain,~occurrence_of(skolem0006(skolem0001),X680)|X680=tptp1,inference(resolution,[status(thm)],[c1807, c236])).
% 1.28/1.47 cnf(c1926,plain,tptp2=tptp1,inference(resolution,[status(thm)],[c1813, c1808])).
% 1.28/1.47 cnf(c1930,plain,tptp1=tptp2,inference(resolution,[status(thm)],[c1926, symmetry])).
% 1.28/1.47 cnf(c1971,plain,$false,inference(resolution,[status(thm)],[c1930, c33])).
% 1.28/1.47 % SZS output end CNFRefutation
% 1.28/1.47
% 1.28/1.47 % Initial clauses : 115
% 1.28/1.47 % Processed clauses : 582
% 1.28/1.47 % Factors computed : 24
% 1.28/1.47 % Resolvents computed: 1702
% 1.28/1.47 % Tautologies deleted: 9
% 1.28/1.47 % Forward subsumed : 346
% 1.28/1.47 % Backward subsumed : 35
% 1.28/1.47 % -------- CPU Time ---------
% 1.28/1.47 % User time : 1.111 s
% 1.28/1.47 % System time : 0.016 s
% 1.28/1.47 % Total time : 1.127 s
%------------------------------------------------------------------------------