%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO011+1 : TPTP v8.1.2. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n013.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.31s 1.49s
% Output : Refutation 1.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : PRO011+1 : TPTP v8.1.2. Released v4.0.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n013.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 03:22:53 EDT 2024
% 0.14/0.37 % CPUTime :
% 1.31/1.49 % Version: 1.5
% 1.31/1.49 % SZS status Theorem
% 1.31/1.49 % SZS output start CNFRefutation
% 1.31/1.49 fof(sos_47,axiom,tptp1!=tptp2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_47)).
% 1.31/1.49 cnf(c40,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_47])).
% 1.31/1.49 cnf(symmetry,axiom,X136!=X137|X137=X136,theory(equality)).
% 1.31/1.49 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/sandbox2/benchmark/theBenchmark.p', sos_21)).
% 1.31/1.49 fof(c152,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.31/1.49 fof(c153,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)],[c152])).
% 1.31/1.49 fof(c154,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)],[c153])).
% 1.31/1.49 fof(c156,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(c155,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)],[c154])).])).
% 1.31/1.49 fof(c157,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)],[c156])).
% 1.31/1.49 cnf(c159,plain,~leaf(X191,X192)|~min_precedes(X191,X190,X192),inference(split_conjunct,[status(thm)],[c157])).
% 1.31/1.49 fof(goals,conjecture,(![X109]:(occurrence_of(X109,tptp0)=>(?[X110]:(?[X111]:((leaf_occ(X111,X109)&(occurrence_of(X111,tptp1)=>(~(?[X112]:((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0))))))&(occurrence_of(X111,tptp2)=>(~(?[X113]:((occurrence_of(X113,tptp1)&subactivity_occurrence(X113,X109))&min_precedes(X110,X113,tptp0)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 1.31/1.49 fof(c17,negated_conjecture,(~(![X109]:(occurrence_of(X109,tptp0)=>(?[X110]:(?[X111]:((leaf_occ(X111,X109)&(occurrence_of(X111,tptp1)=>(~(?[X112]:((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0))))))&(occurrence_of(X111,tptp2)=>(~(?[X113]:((occurrence_of(X113,tptp1)&subactivity_occurrence(X113,X109))&min_precedes(X110,X113,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 1.31/1.49 fof(c18,negated_conjecture,(?[X109]:(occurrence_of(X109,tptp0)&(![X110]:(![X111]:((~leaf_occ(X111,X109)|(occurrence_of(X111,tptp1)&(?[X112]:((occurrence_of(X112,tptp2)&subactivity_occurrence(X112,X109))&min_precedes(X110,X112,tptp0)))))|(occurrence_of(X111,tptp2)&(?[X113]:((occurrence_of(X113,tptp1)&subactivity_occurrence(X113,X109))&min_precedes(X110,X113,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 1.31/1.49 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])).
% 1.31/1.49 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])).])).
% 1.31/1.49 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])).
% 1.31/1.49 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.31/1.49 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/sandbox2/benchmark/theBenchmark.p', sos_35)).
% 1.31/1.49 fof(c53,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.31/1.49 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])).
% 1.31/1.49 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])).
% 1.31/1.49 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])).
% 1.31/1.49 cnf(c63,plain,~occurrence_of(X239,tptp0)|leaf_occ(skolem0006(X239),X239),inference(split_conjunct,[status(thm)],[c56])).
% 1.31/1.49 cnf(c287,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c63, c23])).
% 1.31/1.49 cnf(c36,negated_conjecture,~leaf_occ(X329,skolem0001)|min_precedes(X328,skolem0002(X328,X329),tptp0)|occurrence_of(X329,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 1.31/1.49 cnf(c434,plain,min_precedes(X537,skolem0002(X537,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c36, c287])).
% 1.31/1.49 cnf(c1123,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~leaf(X538,tptp0),inference(resolution,[status(thm)],[c434, c159])).
% 1.31/1.49 cnf(reflexivity,axiom,X135=X135,theory(equality)).
% 1.31/1.49 fof(sos_02,axiom,(![X4]:(![X5]:(![X6]:((occurrence_of(X4,X5)&occurrence_of(X4,X6))=>X5=X6)))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_02)).
% 1.31/1.49 fof(c241,plain,(![X4]:(![X5]:(![X6]:((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)))),inference(fof_nnf,[status(thm)],[sos_02])).
% 1.31/1.49 fof(c242,plain,(![X128]:(![X129]:(![X130]:((~occurrence_of(X128,X129)|~occurrence_of(X128,X130))|X129=X130)))),inference(variable_rename,[status(thm)],[c241])).
% 1.31/1.49 cnf(c243,plain,~occurrence_of(X295,X297)|~occurrence_of(X295,X296)|X297=X296,inference(split_conjunct,[status(thm)],[c242])).
% 1.31/1.49 cnf(c332,plain,~occurrence_of(skolem0001,X300)|X300=tptp0,inference(resolution,[status(thm)],[c243, c23])).
% 1.31/1.49 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/sandbox2/benchmark/theBenchmark.p', sos_34)).
% 1.31/1.49 fof(c64,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.31/1.49 fof(c65,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)],[c64])).
% 1.31/1.49 fof(c66,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)],[c65])).
% 1.31/1.49 fof(c68,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(c67,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)],[c66])).])).
% 1.31/1.49 fof(c69,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)],[c68])).
% 1.31/1.49 cnf(c70,plain,~leaf_occ(X245,X244)|occurrence_of(X244,skolem0007(X245,X244)),inference(split_conjunct,[status(thm)],[c69])).
% 1.31/1.49 cnf(c294,plain,occurrence_of(skolem0001,skolem0007(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c70, c287])).
% 1.31/1.49 cnf(c370,plain,skolem0007(skolem0006(skolem0001),skolem0001)=tptp0,inference(resolution,[status(thm)],[c294, c332])).
% 1.31/1.49 cnf(c12,axiom,X243!=X240|X242!=X241|~leaf(X243,X242)|leaf(X240,X241),theory(equality)).
% 1.31/1.49 cnf(c72,plain,~leaf_occ(X247,X246)|leaf(X247,skolem0007(X247,X246)),inference(split_conjunct,[status(thm)],[c69])).
% 1.31/1.49 cnf(c295,plain,leaf(skolem0006(skolem0001),skolem0007(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c72, c287])).
% 1.31/1.49 cnf(c606,plain,skolem0006(skolem0001)!=X728|skolem0007(skolem0006(skolem0001),skolem0001)!=X727|leaf(X728,X727),inference(resolution,[status(thm)],[c295, c12])).
% 1.31/1.49 cnf(c2023,plain,skolem0006(skolem0001)!=X729|leaf(X729,tptp0),inference(resolution,[status(thm)],[c606, c370])).
% 1.31/1.49 cnf(c2024,plain,leaf(skolem0006(skolem0001),tptp0),inference(resolution,[status(thm)],[c2023, reflexivity])).
% 1.31/1.49 cnf(c2034,plain,occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c2024, c1123])).
% 1.31/1.49 cnf(c27,negated_conjecture,~leaf_occ(X304,skolem0001)|occurrence_of(X304,tptp1)|min_precedes(X303,skolem0003(X303,X304),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.31/1.49 cnf(c351,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X484,skolem0003(X484,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c27, c287])).
% 1.31/1.49 cnf(c802,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~leaf(X485,tptp0),inference(resolution,[status(thm)],[c351, c159])).
% 1.31/1.49 cnf(c2033,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c2024, c802])).
% 1.31/1.49 cnf(c2041,plain,~occurrence_of(skolem0006(skolem0001),X730)|X730=tptp1,inference(resolution,[status(thm)],[c2033, c243])).
% 1.31/1.49 cnf(c2134,plain,tptp2=tptp1,inference(resolution,[status(thm)],[c2041, c2034])).
% 1.31/1.49 cnf(c2149,plain,tptp1=tptp2,inference(resolution,[status(thm)],[c2134, symmetry])).
% 1.31/1.49 cnf(c2155,plain,$false,inference(resolution,[status(thm)],[c2149, c40])).
% 1.31/1.49 % SZS output end CNFRefutation
% 1.31/1.49
% 1.31/1.49 % Initial clauses : 122
% 1.31/1.49 % Processed clauses : 611
% 1.31/1.49 % Factors computed : 24
% 1.31/1.49 % Resolvents computed: 1886
% 1.31/1.49 % Tautologies deleted: 9
% 1.31/1.49 % Forward subsumed : 382
% 1.31/1.49 % Backward subsumed : 43
% 1.31/1.49 % -------- CPU Time ---------
% 1.31/1.49 % User time : 1.110 s
% 1.31/1.49 % System time : 0.012 s
% 1.31/1.49 % Total time : 1.122 s
%------------------------------------------------------------------------------