%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : PRO011+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:29 EDT 2024
% Result : Theorem 1.07s 1.29s
% Output : Refutation 1.07s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : PRO011+2 : TPTP v8.1.2. Released v4.0.0.
% 0.07/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:24:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 1.07/1.29 % Version: 1.5
% 1.07/1.29 % SZS status Theorem
% 1.07/1.29 % SZS output start CNFRefutation
% 1.07/1.29 fof(sos_44,axiom,tptp1!=tptp2,file('/export/starexec/sandbox2/benchmark/theBenchmark.p', sos_44)).
% 1.07/1.29 cnf(c40,plain,tptp1!=tptp2,inference(split_conjunct,[status(thm)],[sos_44])).
% 1.07/1.29 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.07/1.29 fof(c154,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.07/1.29 fof(c155,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)],[c154])).
% 1.07/1.29 fof(c156,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)],[c155])).
% 1.07/1.29 fof(c158,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(c157,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)],[c156])).])).
% 1.07/1.29 fof(c159,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)],[c158])).
% 1.07/1.29 cnf(c161,plain,~leaf(X193,X191)|~min_precedes(X193,X192,X191),inference(split_conjunct,[status(thm)],[c159])).
% 1.07/1.29 fof(goals,conjecture,(![X99]:(occurrence_of(X99,tptp0)=>(?[X100]:(?[X101]:((leaf_occ(X101,X99)&(occurrence_of(X101,tptp1)=>(~(?[X102]:((occurrence_of(X102,tptp2)&subactivity_occurrence(X102,X99))&min_precedes(X100,X102,tptp0))))))&(occurrence_of(X101,tptp2)=>(~(?[X103]:((occurrence_of(X103,tptp1)&subactivity_occurrence(X103,X99))&min_precedes(X100,X103,tptp0)))))))))),file('/export/starexec/sandbox2/benchmark/theBenchmark.p', goals)).
% 1.07/1.29 fof(c17,negated_conjecture,(~(![X99]:(occurrence_of(X99,tptp0)=>(?[X100]:(?[X101]:((leaf_occ(X101,X99)&(occurrence_of(X101,tptp1)=>(~(?[X102]:((occurrence_of(X102,tptp2)&subactivity_occurrence(X102,X99))&min_precedes(X100,X102,tptp0))))))&(occurrence_of(X101,tptp2)=>(~(?[X103]:((occurrence_of(X103,tptp1)&subactivity_occurrence(X103,X99))&min_precedes(X100,X103,tptp0))))))))))),inference(assume_negation,[status(cth)],[goals])).
% 1.07/1.29 fof(c18,negated_conjecture,(?[X99]:(occurrence_of(X99,tptp0)&(![X100]:(![X101]:((~leaf_occ(X101,X99)|(occurrence_of(X101,tptp1)&(?[X102]:((occurrence_of(X102,tptp2)&subactivity_occurrence(X102,X99))&min_precedes(X100,X102,tptp0)))))|(occurrence_of(X101,tptp2)&(?[X103]:((occurrence_of(X103,tptp1)&subactivity_occurrence(X103,X99))&min_precedes(X100,X103,tptp0))))))))),inference(fof_nnf,[status(thm)],[c17])).
% 1.07/1.29 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.07/1.29 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.07/1.29 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.07/1.29 cnf(c23,negated_conjecture,occurrence_of(skolem0001,tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.07/1.29 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.07/1.29 fof(c53,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.07/1.29 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.07/1.29 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.07/1.29 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.07/1.29 cnf(c63,plain,~occurrence_of(X244,tptp0)|leaf_occ(skolem0006(X244),X244),inference(split_conjunct,[status(thm)],[c56])).
% 1.07/1.29 cnf(c281,plain,leaf_occ(skolem0006(skolem0001),skolem0001),inference(resolution,[status(thm)],[c63, c23])).
% 1.07/1.29 cnf(c27,negated_conjecture,~leaf_occ(X280,skolem0001)|occurrence_of(X280,tptp1)|min_precedes(X281,skolem0003(X281,X280),tptp0),inference(split_conjunct,[status(thm)],[c22])).
% 1.07/1.29 cnf(c315,plain,occurrence_of(skolem0006(skolem0001),tptp1)|min_precedes(X467,skolem0003(X467,skolem0006(skolem0001)),tptp0),inference(resolution,[status(thm)],[c27, c281])).
% 1.07/1.29 cnf(c781,plain,occurrence_of(skolem0006(skolem0001),tptp1)|~leaf(X468,tptp0),inference(resolution,[status(thm)],[c315, c161])).
% 1.07/1.29 cnf(reflexivity,axiom,X125=X125,theory(equality)).
% 1.07/1.29 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.07/1.29 fof(c117,plain,(![X64]:(![X65]:(![X66]:((~occurrence_of(X64,X65)|~occurrence_of(X64,X66))|X65=X66)))),inference(fof_nnf,[status(thm)],[sos_22])).
% 1.07/1.29 fof(c118,plain,(![X39]:(![X40]:(![X41]:((~occurrence_of(X39,X40)|~occurrence_of(X39,X41))|X40=X41)))),inference(variable_rename,[status(thm)],[c117])).
% 1.07/1.29 cnf(c119,plain,~occurrence_of(X285,X284)|~occurrence_of(X285,X286)|X284=X286,inference(split_conjunct,[status(thm)],[c118])).
% 1.07/1.29 cnf(c323,plain,~occurrence_of(skolem0001,X289)|X289=tptp0,inference(resolution,[status(thm)],[c119, c23])).
% 1.07/1.29 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.07/1.29 fof(c174,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.07/1.29 fof(c175,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)],[c174])).
% 1.07/1.29 fof(c176,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)],[c175])).
% 1.07/1.29 fof(c178,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(c177,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)],[c176])).])).
% 1.07/1.29 fof(c179,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)],[c178])).
% 1.07/1.29 cnf(c180,plain,~leaf_occ(X264,X263)|occurrence_of(X263,skolem0018(X264,X263)),inference(split_conjunct,[status(thm)],[c179])).
% 1.07/1.29 cnf(c292,plain,occurrence_of(skolem0001,skolem0018(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c180, c281])).
% 1.07/1.29 cnf(c363,plain,skolem0018(skolem0006(skolem0001),skolem0001)=tptp0,inference(resolution,[status(thm)],[c292, c323])).
% 1.07/1.29 cnf(c12,axiom,X241!=X240|X243!=X242|~leaf(X241,X243)|leaf(X240,X242),theory(equality)).
% 1.07/1.29 cnf(c182,plain,~leaf_occ(X267,X266)|leaf(X267,skolem0018(X267,X266)),inference(split_conjunct,[status(thm)],[c179])).
% 1.07/1.29 cnf(c294,plain,leaf(skolem0006(skolem0001),skolem0018(skolem0006(skolem0001),skolem0001)),inference(resolution,[status(thm)],[c182, c281])).
% 1.07/1.29 cnf(c574,plain,skolem0006(skolem0001)!=X636|skolem0018(skolem0006(skolem0001),skolem0001)!=X637|leaf(X636,X637),inference(resolution,[status(thm)],[c294, c12])).
% 1.07/1.29 cnf(c1629,plain,skolem0006(skolem0001)!=X638|leaf(X638,tptp0),inference(resolution,[status(thm)],[c574, c363])).
% 1.07/1.29 cnf(c1632,plain,leaf(skolem0006(skolem0001),tptp0),inference(resolution,[status(thm)],[c1629, reflexivity])).
% 1.07/1.29 cnf(c1641,plain,occurrence_of(skolem0006(skolem0001),tptp1),inference(resolution,[status(thm)],[c1632, c781])).
% 1.07/1.29 cnf(c36,negated_conjecture,~leaf_occ(X310,skolem0001)|min_precedes(X311,skolem0002(X311,X310),tptp0)|occurrence_of(X310,tptp2),inference(split_conjunct,[status(thm)],[c22])).
% 1.07/1.29 cnf(c391,plain,min_precedes(X528,skolem0002(X528,skolem0006(skolem0001)),tptp0)|occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c36, c281])).
% 1.07/1.29 cnf(c1038,plain,occurrence_of(skolem0006(skolem0001),tptp2)|~leaf(X529,tptp0),inference(resolution,[status(thm)],[c391, c161])).
% 1.07/1.29 cnf(c1640,plain,occurrence_of(skolem0006(skolem0001),tptp2),inference(resolution,[status(thm)],[c1632, c1038])).
% 1.07/1.29 cnf(c1647,plain,~occurrence_of(skolem0006(skolem0001),X639)|X639=tptp2,inference(resolution,[status(thm)],[c1640, c119])).
% 1.07/1.29 cnf(c1766,plain,tptp1=tptp2,inference(resolution,[status(thm)],[c1647, c1641])).
% 1.07/1.29 cnf(c1769,plain,$false,inference(resolution,[status(thm)],[c1766, c40])).
% 1.07/1.29 % SZS output end CNFRefutation
% 1.07/1.29
% 1.07/1.29 % Initial clauses : 119
% 1.07/1.29 % Processed clauses : 539
% 1.07/1.29 % Factors computed : 17
% 1.07/1.29 % Resolvents computed: 1512
% 1.07/1.29 % Tautologies deleted: 9
% 1.07/1.29 % Forward subsumed : 310
% 1.07/1.29 % Backward subsumed : 34
% 1.07/1.29 % -------- CPU Time ---------
% 1.07/1.29 % User time : 0.929 s
% 1.07/1.29 % System time : 0.013 s
% 1.07/1.29 % Total time : 0.942 s
%------------------------------------------------------------------------------