%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PRO010+2 : TPTP v9.2.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n012.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 : Tue May 5 05:01:53 PM UTC 2026
% Result : Theorem 0.15s 1.52s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : PRO010+2 : TPTP v9.2.1. Released v4.0.0.
% 0.00/0.06 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.06/0.25 % Computer : n012.cluster.edu
% 0.06/0.25 % Model : x86_64 x86_64
% 0.06/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.25 % Memory : 8042.1875MB
% 0.06/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.25 % CPULimit : 300
% 0.06/0.25 % WCLimit : 300
% 0.06/0.25 % DateTime : Tue May 5 01:30:31 EDT 2026
% 0.06/0.25 % CPUTime :
% 0.06/0.26 % start to proof: theBenchmark
% 0.15/1.52 % Version : CSE_E---1.7
% 0.15/1.52 % Problem : theBenchmark.p
% 0.15/1.52 % SZS status Theorem for theBenchmark.p
% 0.15/1.52 % SZS output start CNFRefutation
% 0.15/1.52 fof(goals, conjecture, ![X100]:(occurrence_of(X100,tptp0)=>?[X101, X102]:((leaf_occ(X102,X100)&(occurrence_of(X102,tptp1)=>~(?[X103]:(occurrence_of(X103,tptp2)&min_precedes(X101,X103,tptp0)))))&(occurrence_of(X102,tptp2)=>~(?[X104]:(occurrence_of(X104,tptp1)&min_precedes(X101,X104,tptp0)))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', goals)).
% 0.15/1.52 fof(sos_07, axiom, ![X26, X27, X28]:(min_precedes(X26,X27,X28)=>~(root(X27,X28))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_07)).
% 0.15/1.52 fof(sos_03, axiom, ![X12, X13, X14, X15]:((((occurrence_of(X14,X15)&~(atomic(X15)))&leaf_occ(X12,X14))&leaf_occ(X13,X14))=>X12=X13), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_03)).
% 0.15/1.52 fof(sos_30, axiom, ![X92, X93]:((occurrence_of(X93,X92)&~(atomic(X92)))=>?[X94]:(root(X94,X92)&subactivity_occurrence(X94,X93))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_30)).
% 0.15/1.52 fof(sos_25, axiom, ![X75, X76]:((leaf(X75,X76)&~(atomic(X76)))=>?[X77]:(occurrence_of(X77,X76)&leaf_occ(X75,X77))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_25)).
% 0.15/1.52 fof(sos_23, axiom, ![X68, X69]:((leaf(X68,X69)&~(atomic(X69)))=>?[X70]:(occurrence_of(X70,X69)&leaf_occ(X68,X70))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_23)).
% 0.15/1.52 fof(sos_09, axiom, ![X31, X32]:(earlier(X31,X32)=>~(earlier(X32,X31))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_09)).
% 0.15/1.52 fof(sos_04, axiom, ![X16, X17, X18]:(next_subocc(X16,X17,X18)<=>(min_precedes(X16,X17,X18)&~(?[X19]:(min_precedes(X16,X19,X18)&min_precedes(X19,X17,X18))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_04)).
% 0.15/1.52 fof(sos, axiom, ![X1, X2, X3, X4]:((min_precedes(X1,X2,X4)&min_precedes(X2,X3,X4))=>min_precedes(X1,X3,X4)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos)).
% 0.15/1.52 fof(sos_26, axiom, ![X78, X79, X80]:(min_precedes(X79,X80,X78)=>?[X81, X82]:(((subactivity(X81,X78)&subactivity(X82,X78))&atocc(X79,X81))&atocc(X80,X82))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_26)).
% 0.15/1.52 fof(sos_24, axiom, ![X71, X72, X73]:(min_precedes(X72,X73,X71)=>?[X74]:((occurrence_of(X74,X71)&subactivity_occurrence(X72,X74))&subactivity_occurrence(X73,X74))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_24)).
% 0.15/1.52 fof(sos_28, axiom, ![X86, X87, X88, X89]:(((((occurrence_of(X87,X86)&arboreal(X88))&arboreal(X89))&subactivity_occurrence(X88,X87))&subactivity_occurrence(X89,X87))=>(min_precedes(X88,X89,X86)|min_precedes(X89,X88,X86)|X88=X89)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_28)).
% 0.15/1.52 fof(sos_14, axiom, ![X43, X44]:(leaf(X43,X44)<=>((root(X43,X44)|?[X45]:min_precedes(X45,X43,X44))&~(?[X46]:min_precedes(X43,X46,X44)))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_14)).
% 0.15/1.52 fof(sos_21, axiom, ![X61, X62, X63]:((occurrence_of(X61,X63)&leaf_occ(X62,X61))=>~(?[X64]:min_precedes(X62,X64,X63))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_21)).
% 0.15/1.52 fof(sos_20, axiom, ![X57, X58, X59]:((occurrence_of(X57,X59)&root_occ(X58,X57))=>~(?[X60]:min_precedes(X60,X58,X59))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_20)).
% 0.15/1.52 fof(sos_06, axiom, ![X23, X24, X25]:(min_precedes(X23,X24,X25)=>precedes(X23,X24)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_06)).
% 0.15/1.52 fof(sos_05, axiom, ![X20, X21, X22]:(next_subocc(X20,X21,X22)=>(arboreal(X20)&arboreal(X21))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_05)).
% 0.15/1.52 fof(sos_32, axiom, ![X96]:(occurrence_of(X96,tptp0)=>?[X97, X98, X99]:((((((occurrence_of(X97,tptp3)&root_occ(X97,X96))&occurrence_of(X98,tptp4))&next_subocc(X97,X98,tptp0))&(occurrence_of(X99,tptp1)|occurrence_of(X99,tptp2)))&next_subocc(X98,X99,tptp0))&leaf_occ(X99,X96))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_32)).
% 0.15/1.52 fof(sos_11, axiom, ![X36, X37]:(leaf_occ(X36,X37)<=>?[X38]:((occurrence_of(X37,X38)&subactivity_occurrence(X36,X37))&leaf(X36,X38))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_11)).
% 0.15/1.52 fof(sos_10, axiom, ![X33, X34]:(root_occ(X33,X34)<=>?[X35]:((occurrence_of(X34,X35)&subactivity_occurrence(X33,X34))&root(X33,X35))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_10)).
% 0.15/1.52 fof(sos_02, axiom, ![X8, X9, X10, X11]:(((occurrence_of(X10,X11)&root_occ(X8,X10))&root_occ(X9,X10))=>X8=X9), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_02)).
% 0.15/1.52 fof(sos_15, axiom, ![X47, X48]:(atocc(X47,X48)<=>?[X49]:((subactivity(X48,X49)&atomic(X49))&occurrence_of(X47,X49))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_15)).
% 0.15/1.52 fof(sos_27, axiom, ![X83, X84]:(root(X84,X83)=>?[X85]:(subactivity(X85,X83)&atocc(X84,X85))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_27)).
% 0.15/1.52 fof(sos_01, axiom, ![X5, X6, X7]:((earlier(X5,X6)&earlier(X6,X7))=>earlier(X5,X7)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_01)).
% 0.15/1.52 fof(sos_22, axiom, ![X65, X66, X67]:((occurrence_of(X65,X66)&occurrence_of(X65,X67))=>X66=X67), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_22)).
% 0.15/1.52 fof(sos_16, axiom, ![X50, X51]:((atocc(X50,X51)&legal(X50))=>root(X50,X51)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_16)).
% 0.15/1.52 fof(sos_08, axiom, ![X29, X30]:(precedes(X29,X30)<=>(earlier(X29,X30)&legal(X30))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_08)).
% 0.15/1.52 fof(sos_13, axiom, ![X41, X42]:(occurrence_of(X41,X42)=>(arboreal(X41)<=>atomic(X42))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_13)).
% 0.15/1.52 fof(sos_18, axiom, ![X53]:(activity_occurrence(X53)=>?[X54]:(activity(X54)&occurrence_of(X53,X54))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_18)).
% 0.15/1.52 fof(sos_29, axiom, ![X90, X91]:(occurrence_of(X91,X90)=>(activity(X90)&activity_occurrence(X91))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_29)).
% 0.15/1.52 fof(sos_19, axiom, ![X55, X56]:(subactivity_occurrence(X55,X56)=>(activity_occurrence(X55)&activity_occurrence(X56))), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_19)).
% 0.15/1.52 fof(sos_12, axiom, ![X39, X40]:(root(X39,X40)=>legal(X39)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_12)).
% 0.15/1.52 fof(sos_31, axiom, ![X95]:(activity(X95)=>subactivity(X95,X95)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_31)).
% 0.15/1.52 fof(sos_17, axiom, ![X52]:(legal(X52)=>arboreal(X52)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_17)).
% 0.15/1.52 fof(sos_34, axiom, ~(atomic(tptp0)), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_34)).
% 0.15/1.52 fof(sos_33, axiom, activity(tptp0), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_33)).
% 0.15/1.52 fof(sos_37, axiom, atomic(tptp2), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_37)).
% 0.15/1.52 fof(sos_36, axiom, atomic(tptp1), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_36)).
% 0.15/1.52 fof(sos_35, axiom, atomic(tptp4), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_35)).
% 0.15/1.52 fof(sos_38, axiom, atomic(tptp3), file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_38)).
% 0.15/1.52 fof(sos_44, axiom, tptp1!=tptp2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_44)).
% 0.15/1.52 fof(sos_41, axiom, tptp4!=tptp2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_41)).
% 0.15/1.52 fof(sos_43, axiom, tptp3!=tptp2, file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_43)).
% 0.15/1.52 fof(sos_40, axiom, tptp4!=tptp1, file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_40)).
% 0.15/1.52 fof(sos_42, axiom, tptp3!=tptp1, file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_42)).
% 0.15/1.52 fof(sos_39, axiom, tptp4!=tptp3, file('/export/starexec/sandbox/benchmark/theBenchmark.p', sos_39)).
% 0.15/1.52 fof(i_0_46, negated_conjecture, ~(![X100]:(occurrence_of(X100,tptp0)=>?[X101, X102]:((leaf_occ(X102,X100)&(occurrence_of(X102,tptp1)=>~(?[X103]:(occurrence_of(X103,tptp2)&min_precedes(X101,X103,tptp0)))))&(occurrence_of(X102,tptp2)=>~(?[X104]:(occurrence_of(X104,tptp1)&min_precedes(X101,X104,tptp0))))))), inference(assume_negation,[status(cth)],[goals])).
% 0.15/1.52 fof(i_0_47, plain, ![X26, X27, X28]:(min_precedes(X26,X27,X28)=>~root(X27,X28)), inference(fof_simplification,[status(thm)],[sos_07])).
% 0.15/1.52 fof(i_0_48, plain, ![X12, X13, X14, X15]:((((occurrence_of(X14,X15)&~atomic(X15))&leaf_occ(X12,X14))&leaf_occ(X13,X14))=>X12=X13), inference(fof_simplification,[status(thm)],[sos_03])).
% 0.15/1.52 fof(i_0_49, plain, ![X92, X93]:((occurrence_of(X93,X92)&~atomic(X92))=>?[X94]:(root(X94,X92)&subactivity_occurrence(X94,X93))), inference(fof_simplification,[status(thm)],[sos_30])).
% 0.15/1.52 fof(i_0_50, plain, ![X75, X76]:((leaf(X75,X76)&~atomic(X76))=>?[X77]:(occurrence_of(X77,X76)&leaf_occ(X75,X77))), inference(fof_simplification,[status(thm)],[sos_25])).
% 0.15/1.52 fof(i_0_51, plain, ![X68, X69]:((leaf(X68,X69)&~atomic(X69))=>?[X70]:(occurrence_of(X70,X69)&leaf_occ(X68,X70))), inference(fof_simplification,[status(thm)],[sos_23])).
% 0.15/1.52 fof(i_0_52, plain, ![X31, X32]:(earlier(X31,X32)=>~earlier(X32,X31)), inference(fof_simplification,[status(thm)],[sos_09])).
% 0.15/1.52 fof(i_0_53, plain, ![X224, X225, X226, X227, X228, X229, X230]:(((min_precedes(X224,X225,X226)|~next_subocc(X224,X225,X226))&(~min_precedes(X224,X227,X226)|~min_precedes(X227,X225,X226)|~next_subocc(X224,X225,X226)))&((min_precedes(X228,esk1_3(X228,X229,X230),X230)|~min_precedes(X228,X229,X230)|next_subocc(X228,X229,X230))&(min_precedes(esk1_3(X228,X229,X230),X229,X230)|~min_precedes(X228,X229,X230)|next_subocc(X228,X229,X230)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_04])])])])])])).
% 0.15/1.52 fof(i_0_54, plain, ![X209, X210, X211, X212]:(~min_precedes(X209,X210,X212)|~min_precedes(X210,X211,X212)|min_precedes(X209,X211,X212)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos])])).
% 0.15/1.52 fof(i_0_55, plain, ![X303, X304, X305]:((((subactivity(esk11_3(X303,X304,X305),X303)|~min_precedes(X304,X305,X303))&(subactivity(esk12_3(X303,X304,X305),X303)|~min_precedes(X304,X305,X303)))&(atocc(X304,esk11_3(X303,X304,X305))|~min_precedes(X304,X305,X303)))&(atocc(X305,esk12_3(X303,X304,X305))|~min_precedes(X304,X305,X303))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_26])])])])).
% 0.15/1.52 fof(i_0_56, plain, ![X296, X297, X298]:(((occurrence_of(esk9_3(X296,X297,X298),X296)|~min_precedes(X297,X298,X296))&(subactivity_occurrence(X297,esk9_3(X296,X297,X298))|~min_precedes(X297,X298,X296)))&(subactivity_occurrence(X298,esk9_3(X296,X297,X298))|~min_precedes(X297,X298,X296))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_24])])])])).
% 0.15/1.52 fof(i_0_57, plain, ![X311, X312, X313, X314]:(~occurrence_of(X312,X311)|~arboreal(X313)|~arboreal(X314)|~subactivity_occurrence(X313,X312)|~subactivity_occurrence(X314,X312)|(min_precedes(X313,X314,X311)|min_precedes(X314,X313,X311)|X313=X314)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_28])])).
% 0.15/1.52 fof(i_0_58, plain, ![X261, X262, X264, X265, X266, X267]:(((root(X261,X262)|min_precedes(esk4_2(X261,X262),X261,X262)|~leaf(X261,X262))&(~min_precedes(X261,X264,X262)|~leaf(X261,X262)))&((~root(X265,X266)|min_precedes(X265,esk5_2(X265,X266),X266)|leaf(X265,X266))&(~min_precedes(X267,X265,X266)|min_precedes(X265,esk5_2(X265,X266),X266)|leaf(X265,X266)))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_14])])])])])])).
% 0.15/1.52 fof(i_0_59, negated_conjecture, ![X326, X327]:(occurrence_of(esk18_0,tptp0)&(((occurrence_of(X327,tptp2)|(occurrence_of(X327,tptp1)|~leaf_occ(X327,esk18_0)))&((occurrence_of(esk20_2(X326,X327),tptp1)|(occurrence_of(X327,tptp1)|~leaf_occ(X327,esk18_0)))&(min_precedes(X326,esk20_2(X326,X327),tptp0)|(occurrence_of(X327,tptp1)|~leaf_occ(X327,esk18_0)))))&(((occurrence_of(X327,tptp2)|(occurrence_of(esk19_2(X326,X327),tptp2)|~leaf_occ(X327,esk18_0)))&((occurrence_of(esk20_2(X326,X327),tptp1)|(occurrence_of(esk19_2(X326,X327),tptp2)|~leaf_occ(X327,esk18_0)))&(min_precedes(X326,esk20_2(X326,X327),tptp0)|(occurrence_of(esk19_2(X326,X327),tptp2)|~leaf_occ(X327,esk18_0)))))&((occurrence_of(X327,tptp2)|(min_precedes(X326,esk19_2(X326,X327),tptp0)|~leaf_occ(X327,esk18_0)))&((occurrence_of(esk20_2(X326,X327),tptp1)|(min_precedes(X326,esk19_2(X326,X327),tptp0)|~leaf_occ(X327,esk18_0)))&(min_precedes(X326,esk20_2(X326,X327),tptp0)|(min_precedes(X326,esk19_2(X326,X327),tptp0)|~leaf_occ(X327,esk18_0)))))))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_46])])])])])).
% 0.15/1.52 fof(i_0_60, plain, ![X286, X287, X288, X289]:(~occurrence_of(X286,X288)|~leaf_occ(X287,X286)|~min_precedes(X287,X289,X288)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_21])])])).
% 0.15/1.52 fof(i_0_61, plain, ![X282, X283, X284, X285]:(~occurrence_of(X282,X284)|~root_occ(X283,X282)|~min_precedes(X285,X283,X284)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_20])])])).
% 0.15/1.52 fof(i_0_62, plain, ![X238, X239, X240]:(~min_precedes(X238,X239,X240)|~root(X239,X240)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_47])])).
% 0.15/1.52 fof(i_0_63, plain, ![X235, X236, X237]:(~min_precedes(X235,X236,X237)|precedes(X235,X236)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_06])])).
% 0.15/1.52 fof(i_0_64, plain, ![X232, X233, X234]:((arboreal(X232)|~next_subocc(X232,X233,X234))&(arboreal(X233)|~next_subocc(X232,X233,X234))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_05])])])).
% 0.15/1.52 fof(i_0_65, plain, ![X321]:(((((((occurrence_of(esk15_1(X321),tptp3)|~occurrence_of(X321,tptp0))&(root_occ(esk15_1(X321),X321)|~occurrence_of(X321,tptp0)))&(occurrence_of(esk16_1(X321),tptp4)|~occurrence_of(X321,tptp0)))&(next_subocc(esk15_1(X321),esk16_1(X321),tptp0)|~occurrence_of(X321,tptp0)))&(occurrence_of(esk17_1(X321),tptp1)|occurrence_of(esk17_1(X321),tptp2)|~occurrence_of(X321,tptp0)))&(next_subocc(esk16_1(X321),esk17_1(X321),tptp0)|~occurrence_of(X321,tptp0)))&(leaf_occ(esk17_1(X321),X321)|~occurrence_of(X321,tptp0))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_32])])])])).
% 0.15/1.52 fof(i_0_66, plain, ![X251, X252, X254, X255, X256]:((((occurrence_of(X252,esk3_2(X251,X252))|~leaf_occ(X251,X252))&(subactivity_occurrence(X251,X252)|~leaf_occ(X251,X252)))&(leaf(X251,esk3_2(X251,X252))|~leaf_occ(X251,X252)))&(~occurrence_of(X255,X256)|~subactivity_occurrence(X254,X255)|~leaf(X254,X256)|leaf_occ(X254,X255))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_11])])])])])])).
% 0.15/1.52 fof(i_0_67, plain, ![X245, X246, X248, X249, X250]:((((occurrence_of(X246,esk2_2(X245,X246))|~root_occ(X245,X246))&(subactivity_occurrence(X245,X246)|~root_occ(X245,X246)))&(root(X245,esk2_2(X245,X246))|~root_occ(X245,X246)))&(~occurrence_of(X249,X250)|~subactivity_occurrence(X248,X249)|~root(X248,X250)|root_occ(X248,X249))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_10])])])])])])).
% 0.15/1.52 fof(i_0_68, plain, ![X220, X221, X222, X223]:(~occurrence_of(X222,X223)|atomic(X223)|~leaf_occ(X220,X222)|~leaf_occ(X221,X222)|X220=X221), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_48])])).
% 0.15/1.52 fof(i_0_69, plain, ![X216, X217, X218, X219]:(~occurrence_of(X218,X219)|~root_occ(X216,X218)|~root_occ(X217,X218)|X216=X217), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_02])])).
% 0.15/1.52 fof(i_0_70, plain, ![X317, X318]:((root(esk14_2(X317,X318),X317)|(~occurrence_of(X318,X317)|atomic(X317)))&(subactivity_occurrence(esk14_2(X317,X318),X318)|(~occurrence_of(X318,X317)|atomic(X317)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_49])])])])).
% 0.15/1.52 fof(i_0_71, plain, ![X300, X301]:((occurrence_of(esk10_2(X300,X301),X301)|(~leaf(X300,X301)|atomic(X301)))&(leaf_occ(X300,esk10_2(X300,X301))|(~leaf(X300,X301)|atomic(X301)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_50])])])])).
% 0.15/1.52 fof(i_0_72, plain, ![X293, X294]:((occurrence_of(esk8_2(X293,X294),X294)|(~leaf(X293,X294)|atomic(X294)))&(leaf_occ(X293,esk8_2(X293,X294))|(~leaf(X293,X294)|atomic(X294)))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_51])])])])).
% 0.15/1.52 fof(i_0_73, plain, ![X269, X270, X272, X273, X274]:((((subactivity(X270,esk6_2(X269,X270))|~atocc(X269,X270))&(atomic(esk6_2(X269,X270))|~atocc(X269,X270)))&(occurrence_of(X269,esk6_2(X269,X270))|~atocc(X269,X270)))&(~subactivity(X273,X274)|~atomic(X274)|~occurrence_of(X272,X274)|atocc(X272,X273))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_15])])])])])])).
% 0.15/1.52 fof(i_0_74, plain, ![X308, X309]:((subactivity(esk13_2(X308,X309),X308)|~root(X309,X308))&(atocc(X309,esk13_2(X308,X309))|~root(X309,X308))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_27])])])])).
% 0.15/1.52 fof(i_0_75, plain, ![X213, X214, X215]:(~earlier(X213,X214)|~earlier(X214,X215)|earlier(X213,X215)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_01])])).
% 0.15/1.52 fof(i_0_76, plain, ![X290, X291, X292]:(~occurrence_of(X290,X291)|~occurrence_of(X290,X292)|X291=X292), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_22])])).
% 0.15/1.52 fof(i_0_77, plain, ![X243, X244]:(~earlier(X243,X244)|~earlier(X244,X243)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_52])])).
% 0.15/1.52 fof(i_0_78, plain, ![X275, X276]:(~atocc(X275,X276)|~legal(X275)|root(X275,X276)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_16])])).
% 0.15/1.52 fof(i_0_79, plain, ![X241, X242]:(((earlier(X241,X242)|~precedes(X241,X242))&(legal(X242)|~precedes(X241,X242)))&(~earlier(X241,X242)|~legal(X242)|precedes(X241,X242))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_08])])])).
% 0.15/1.52 fof(i_0_80, plain, ![X259, X260]:((~arboreal(X259)|atomic(X260)|~occurrence_of(X259,X260))&(~atomic(X260)|arboreal(X259)|~occurrence_of(X259,X260))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_13])])])).
% 0.15/1.52 fof(i_0_81, plain, ![X278]:((activity(esk7_1(X278))|~activity_occurrence(X278))&(occurrence_of(X278,esk7_1(X278))|~activity_occurrence(X278))), inference(distribute,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_18])])])])).
% 0.15/1.52 fof(i_0_82, plain, ![X315, X316]:((activity(X315)|~occurrence_of(X316,X315))&(activity_occurrence(X316)|~occurrence_of(X316,X315))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_29])])])).
% 0.15/1.52 fof(i_0_83, plain, ![X280, X281]:((activity_occurrence(X280)|~subactivity_occurrence(X280,X281))&(activity_occurrence(X281)|~subactivity_occurrence(X280,X281))), inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_19])])])).
% 0.15/1.52 fof(i_0_84, plain, ![X257, X258]:(~root(X257,X258)|legal(X257)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_12])])).
% 0.15/1.52 fof(i_0_85, plain, ![X320]:(~activity(X320)|subactivity(X320,X320)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_31])])).
% 0.15/1.52 fof(i_0_86, plain, ![X277]:(~legal(X277)|arboreal(X277)), inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[sos_17])])).
% 0.15/1.52 fof(i_0_87, plain, ~atomic(tptp0), inference(fof_simplification,[status(thm)],[sos_34])).
% 0.15/1.52 cnf(i_0_88, plain, (min_precedes(esk1_3(X1,X2,X3),X2,X3)|next_subocc(X1,X2,X3)|~min_precedes(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.15/1.52 cnf(i_0_89, plain, (min_precedes(X1,esk1_3(X1,X2,X3),X3)|next_subocc(X1,X2,X3)|~min_precedes(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.15/1.52 cnf(i_0_90, plain, (~min_precedes(X1,X2,X3)|~min_precedes(X2,X4,X3)|~next_subocc(X1,X4,X3)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.15/1.52 cnf(i_0_91, plain, (min_precedes(X1,X4,X3)|~min_precedes(X1,X2,X3)|~min_precedes(X2,X4,X3)), inference(split_conjunct,[status(thm)],[i_0_54]), ['final']).
% 0.15/1.52 cnf(i_0_92, plain, (subactivity(esk12_3(X1,X2,X3),X1)|~min_precedes(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.15/1.52 cnf(i_0_93, plain, (subactivity(esk11_3(X1,X2,X3),X1)|~min_precedes(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.15/1.52 cnf(i_0_94, plain, (occurrence_of(esk9_3(X1,X2,X3),X1)|~min_precedes(X2,X3,X1)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.15/1.52 cnf(i_0_95, plain, (atocc(X1,esk12_3(X2,X3,X1))|~min_precedes(X3,X1,X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.15/1.52 cnf(i_0_96, plain, (atocc(X1,esk11_3(X2,X1,X3))|~min_precedes(X1,X3,X2)), inference(split_conjunct,[status(thm)],[i_0_55]), ['final']).
% 0.15/1.52 cnf(i_0_97, plain, (subactivity_occurrence(X1,esk9_3(X2,X1,X3))|~min_precedes(X1,X3,X2)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.15/1.52 cnf(i_0_98, plain, (subactivity_occurrence(X1,esk9_3(X2,X3,X1))|~min_precedes(X3,X1,X2)), inference(split_conjunct,[status(thm)],[i_0_56]), ['final']).
% 0.15/1.52 cnf(i_0_99, plain, (min_precedes(X3,X4,X2)|min_precedes(X4,X3,X2)|X3=X4|~occurrence_of(X1,X2)|~arboreal(X3)|~arboreal(X4)|~subactivity_occurrence(X3,X1)|~subactivity_occurrence(X4,X1)), inference(split_conjunct,[status(thm)],[i_0_57]), ['final']).
% 0.15/1.52 cnf(i_0_100, plain, (min_precedes(X2,esk5_2(X2,X3),X3)|leaf(X2,X3)|~min_precedes(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.15/1.52 cnf(i_0_101, negated_conjecture, (min_precedes(X1,esk20_2(X1,X2),tptp0)|min_precedes(X1,esk19_2(X1,X2),tptp0)|~leaf_occ(X2,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_102, plain, (min_precedes(X1,X2,X3)|~next_subocc(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_53]), ['final']).
% 0.15/1.52 cnf(i_0_103, negated_conjecture, (occurrence_of(esk20_2(X1,X2),tptp1)|min_precedes(X1,esk19_2(X1,X2),tptp0)|~leaf_occ(X2,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_104, negated_conjecture, (min_precedes(X1,esk20_2(X1,X2),tptp0)|occurrence_of(esk19_2(X1,X2),tptp2)|~leaf_occ(X2,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_105, plain, (~occurrence_of(X1,X2)|~leaf_occ(X3,X1)|~min_precedes(X3,X4,X2)), inference(split_conjunct,[status(thm)],[i_0_60]), ['final']).
% 0.15/1.52 cnf(i_0_106, plain, (~occurrence_of(X1,X2)|~root_occ(X3,X1)|~min_precedes(X4,X3,X2)), inference(split_conjunct,[status(thm)],[i_0_61]), ['final']).
% 0.15/1.52 cnf(i_0_107, plain, (root(X1,X2)|min_precedes(esk4_2(X1,X2),X1,X2)|~leaf(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.15/1.52 cnf(i_0_108, plain, (min_precedes(X1,esk5_2(X1,X2),X2)|leaf(X1,X2)|~root(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.15/1.52 cnf(i_0_109, negated_conjecture, (occurrence_of(X1,tptp2)|min_precedes(X2,esk19_2(X2,X1),tptp0)|~leaf_occ(X1,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_110, negated_conjecture, (min_precedes(X1,esk20_2(X1,X2),tptp0)|occurrence_of(X2,tptp1)|~leaf_occ(X2,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_111, plain, (~min_precedes(X1,X2,X3)|~leaf(X1,X3)), inference(split_conjunct,[status(thm)],[i_0_58]), ['final']).
% 0.15/1.52 cnf(i_0_112, plain, (~min_precedes(X1,X2,X3)|~root(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_62]), ['final']).
% 0.15/1.52 cnf(i_0_113, plain, (precedes(X1,X2)|~min_precedes(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_63]), ['final']).
% 0.15/1.52 cnf(i_0_114, negated_conjecture, (occurrence_of(esk20_2(X1,X2),tptp1)|occurrence_of(esk19_2(X1,X2),tptp2)|~leaf_occ(X2,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_115, plain, (arboreal(X1)|~next_subocc(X1,X2,X3)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.15/1.52 cnf(i_0_116, plain, (arboreal(X1)|~next_subocc(X2,X1,X3)), inference(split_conjunct,[status(thm)],[i_0_64]), ['final']).
% 0.15/1.52 cnf(i_0_117, plain, (next_subocc(esk16_1(X1),esk17_1(X1),tptp0)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_118, plain, (next_subocc(esk15_1(X1),esk16_1(X1),tptp0)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_119, plain, (leaf_occ(X3,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X3,X1)|~leaf(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.15/1.52 cnf(i_0_120, plain, (root_occ(X3,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X3,X1)|~root(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.15/1.52 cnf(i_0_121, plain, (atomic(X2)|X3=X4|~occurrence_of(X1,X2)|~leaf_occ(X3,X1)|~leaf_occ(X4,X1)), inference(split_conjunct,[status(thm)],[i_0_68]), ['final']).
% 0.15/1.52 cnf(i_0_122, negated_conjecture, (occurrence_of(X1,tptp2)|occurrence_of(esk19_2(X2,X1),tptp2)|~leaf_occ(X1,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_123, negated_conjecture, (occurrence_of(esk20_2(X1,X2),tptp1)|occurrence_of(X2,tptp1)|~leaf_occ(X2,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_124, plain, (X3=X4|~occurrence_of(X1,X2)|~root_occ(X3,X1)|~root_occ(X4,X1)), inference(split_conjunct,[status(thm)],[i_0_69]), ['final']).
% 0.15/1.52 cnf(i_0_125, plain, (subactivity_occurrence(esk14_2(X1,X2),X2)|atomic(X1)|~occurrence_of(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.15/1.52 cnf(i_0_126, plain, (root(esk14_2(X1,X2),X1)|atomic(X1)|~occurrence_of(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_70]), ['final']).
% 0.15/1.52 cnf(i_0_127, plain, (occurrence_of(esk10_2(X1,X2),X2)|atomic(X2)|~leaf(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.15/1.52 cnf(i_0_128, plain, (occurrence_of(esk8_2(X1,X2),X2)|atomic(X2)|~leaf(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.15/1.52 cnf(i_0_129, plain, (leaf_occ(X1,esk10_2(X1,X2))|atomic(X2)|~leaf(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_71]), ['final']).
% 0.15/1.52 cnf(i_0_130, plain, (leaf_occ(X1,esk8_2(X1,X2))|atomic(X2)|~leaf(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_72]), ['final']).
% 0.15/1.52 cnf(i_0_131, plain, (atocc(X3,X1)|~subactivity(X1,X2)|~atomic(X2)|~occurrence_of(X3,X2)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.15/1.52 cnf(i_0_132, plain, (subactivity(esk13_2(X1,X2),X1)|~root(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.15/1.52 cnf(i_0_133, plain, (subactivity(X1,esk6_2(X2,X1))|~atocc(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.15/1.52 cnf(i_0_134, plain, (atocc(X1,esk13_2(X2,X1))|~root(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_74]), ['final']).
% 0.15/1.52 cnf(i_0_135, plain, (leaf(X1,esk3_2(X1,X2))|~leaf_occ(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.15/1.52 cnf(i_0_136, plain, (root(X1,esk2_2(X1,X2))|~root_occ(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.15/1.52 cnf(i_0_137, plain, (occurrence_of(X1,esk6_2(X1,X2))|~atocc(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.15/1.52 cnf(i_0_138, plain, (occurrence_of(X1,esk3_2(X2,X1))|~leaf_occ(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.15/1.52 cnf(i_0_139, plain, (occurrence_of(X1,esk2_2(X2,X1))|~root_occ(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.15/1.52 cnf(i_0_140, plain, (earlier(X1,X3)|~earlier(X1,X2)|~earlier(X2,X3)), inference(split_conjunct,[status(thm)],[i_0_75]), ['final']).
% 0.15/1.52 cnf(i_0_141, plain, (occurrence_of(esk17_1(X1),tptp1)|occurrence_of(esk17_1(X1),tptp2)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_142, plain, (atomic(esk6_2(X1,X2))|~atocc(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_73]), ['final']).
% 0.15/1.52 cnf(i_0_143, plain, (X2=X3|~occurrence_of(X1,X2)|~occurrence_of(X1,X3)), inference(split_conjunct,[status(thm)],[i_0_76]), ['final']).
% 0.15/1.52 cnf(i_0_144, negated_conjecture, (occurrence_of(X1,tptp2)|occurrence_of(X1,tptp1)|~leaf_occ(X1,esk18_0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_145, plain, (~earlier(X1,X2)|~earlier(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_77]), ['final']).
% 0.15/1.52 cnf(i_0_146, plain, (root(X1,X2)|~atocc(X1,X2)|~legal(X1)), inference(split_conjunct,[status(thm)],[i_0_78]), ['final']).
% 0.15/1.52 cnf(i_0_147, plain, (precedes(X1,X2)|~earlier(X1,X2)|~legal(X2)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.15/1.52 cnf(i_0_148, plain, (leaf_occ(esk17_1(X1),X1)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_149, plain, (root_occ(esk15_1(X1),X1)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_150, plain, (occurrence_of(esk16_1(X1),tptp4)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_151, plain, (occurrence_of(esk15_1(X1),tptp3)|~occurrence_of(X1,tptp0)), inference(split_conjunct,[status(thm)],[i_0_65]), ['final']).
% 0.15/1.52 cnf(i_0_152, plain, (subactivity_occurrence(X1,X2)|~leaf_occ(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_66]), ['final']).
% 0.15/1.52 cnf(i_0_153, plain, (subactivity_occurrence(X1,X2)|~root_occ(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_67]), ['final']).
% 0.15/1.52 cnf(i_0_154, plain, (earlier(X1,X2)|~precedes(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.15/1.52 cnf(i_0_155, plain, (arboreal(X2)|~atomic(X1)|~occurrence_of(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_80]), ['final']).
% 0.15/1.52 cnf(i_0_156, plain, (atomic(X2)|~arboreal(X1)|~occurrence_of(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_80]), ['final']).
% 0.15/1.52 cnf(i_0_157, plain, (occurrence_of(X1,esk7_1(X1))|~activity_occurrence(X1)), inference(split_conjunct,[status(thm)],[i_0_81]), ['final']).
% 0.15/1.52 cnf(i_0_158, plain, (activity(X1)|~occurrence_of(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 0.15/1.52 cnf(i_0_159, plain, (activity_occurrence(X1)|~subactivity_occurrence(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_83]), ['final']).
% 0.15/1.52 cnf(i_0_160, plain, (activity_occurrence(X1)|~subactivity_occurrence(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_83]), ['final']).
% 0.15/1.52 cnf(i_0_161, plain, (activity_occurrence(X1)|~occurrence_of(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_82]), ['final']).
% 0.15/1.52 cnf(i_0_162, plain, (legal(X1)|~root(X1,X2)), inference(split_conjunct,[status(thm)],[i_0_84]), ['final']).
% 0.15/1.52 cnf(i_0_163, plain, (legal(X1)|~precedes(X2,X1)), inference(split_conjunct,[status(thm)],[i_0_79]), ['final']).
% 0.15/1.52 cnf(i_0_164, plain, (subactivity(X1,X1)|~activity(X1)), inference(split_conjunct,[status(thm)],[i_0_85]), ['final']).
% 0.15/1.52 cnf(i_0_165, plain, (activity(esk7_1(X1))|~activity_occurrence(X1)), inference(split_conjunct,[status(thm)],[i_0_81]), ['final']).
% 0.15/1.52 cnf(i_0_166, plain, (arboreal(X1)|~legal(X1)), inference(split_conjunct,[status(thm)],[i_0_86]), ['final']).
% 0.15/1.52 cnf(i_0_167, negated_conjecture, (occurrence_of(esk18_0,tptp0)), inference(split_conjunct,[status(thm)],[i_0_59]), ['final']).
% 0.15/1.52 cnf(i_0_168, plain, (~atomic(tptp0)), inference(split_conjunct,[status(thm)],[i_0_87]), ['final']).
% 0.15/1.52 cnf(i_0_169, plain, (activity(tptp0)), inference(split_conjunct,[status(thm)],[sos_33]), ['final']).
% 0.15/1.52 cnf(i_0_170, plain, (atomic(tptp2)), inference(split_conjunct,[status(thm)],[sos_37]), ['final']).
% 0.15/1.52 cnf(i_0_171, plain, (atomic(tptp1)), inference(split_conjunct,[status(thm)],[sos_36]), ['final']).
% 0.15/1.52 cnf(i_0_172, plain, (atomic(tptp4)), inference(split_conjunct,[status(thm)],[sos_35]), ['final']).
% 0.15/1.52 cnf(i_0_173, plain, (atomic(tptp3)), inference(split_conjunct,[status(thm)],[sos_38]), ['final']).
% 0.15/1.52 cnf(i_0_174, plain, (tptp1!=tptp2), inference(split_conjunct,[status(thm)],[sos_44]), ['final']).
% 0.15/1.52 cnf(i_0_175, plain, (tptp4!=tptp2), inference(split_conjunct,[status(thm)],[sos_41]), ['final']).
% 0.15/1.52 cnf(i_0_176, plain, (tptp3!=tptp2), inference(split_conjunct,[status(thm)],[sos_43]), ['final']).
% 0.15/1.52 cnf(i_0_177, plain, (tptp4!=tptp1), inference(split_conjunct,[status(thm)],[sos_40]), ['final']).
% 0.15/1.52 cnf(i_0_178, plain, (tptp3!=tptp1), inference(split_conjunct,[status(thm)],[sos_42]), ['final']).
% 0.15/1.52 cnf(i_0_179, plain, (tptp4!=tptp3), inference(split_conjunct,[status(thm)],[sos_39]), ['final']).
% 0.15/1.52 cnf(i_0_180, axiom, (X1=X1)).
% 0.15/1.52 cnf(i_0_181, axiom, (X1=X2|X2!=X1)).
% 0.15/1.52 cnf(i_0_182, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.15/1.52 cnf(i_0_183, axiom, (X1!=X2|~min_precedes(X1,X3,X4)|min_precedes(X2,X3,X4))).
% 0.15/1.52 cnf(i_0_184, axiom, (X1!=X2|~min_precedes(X3,X1,X4)|min_precedes(X3,X2,X4))).
% 0.15/1.52 cnf(i_0_185, axiom, (X1!=X2|~min_precedes(X3,X4,X1)|min_precedes(X3,X4,X2))).
% 0.15/1.52 cnf(i_0_186, axiom, (X1!=X2|~root_occ(X1,X3)|root_occ(X2,X3))).
% 0.15/1.52 cnf(i_0_187, axiom, (X1!=X2|~root_occ(X3,X1)|root_occ(X3,X2))).
% 0.15/1.52 cnf(i_0_188, axiom, (X1!=X2|~root(X1,X3)|root(X2,X3))).
% 0.15/1.52 cnf(i_0_189, axiom, (X1!=X2|~root(X3,X1)|root(X3,X2))).
% 0.15/1.52 cnf(i_0_190, axiom, (X1!=X2|~precedes(X1,X3)|precedes(X2,X3))).
% 0.15/1.52 cnf(i_0_191, axiom, (X1!=X2|~precedes(X3,X1)|precedes(X3,X2))).
% 0.15/1.52 cnf(i_0_192, axiom, (X1!=X2|~atomic(X1)|atomic(X2))).
% 0.15/1.52 cnf(i_0_193, axiom, (X1!=X2|~earlier(X1,X3)|earlier(X2,X3))).
% 0.15/1.52 cnf(i_0_194, axiom, (X1!=X2|~earlier(X3,X1)|earlier(X3,X2))).
% 0.15/1.52 cnf(i_0_195, axiom, (X1!=X2|~legal(X1)|legal(X2))).
% 0.15/1.52 cnf(i_0_196, axiom, (X1!=X2|~activity_occurrence(X1)|activity_occurrence(X2))).
% 0.15/1.52 cnf(i_0_197, axiom, (X1!=X2|~activity(X1)|activity(X2))).
% 0.15/1.52 cnf(i_0_198, axiom, (X1!=X2|~next_subocc(X1,X3,X4)|next_subocc(X2,X3,X4))).
% 0.15/1.52 cnf(i_0_199, axiom, (X1!=X2|~next_subocc(X3,X1,X4)|next_subocc(X3,X2,X4))).
% 0.15/1.52 cnf(i_0_200, axiom, (X1!=X2|~next_subocc(X3,X4,X1)|next_subocc(X3,X4,X2))).
% 0.15/1.52 cnf(i_0_201, axiom, (X1!=X2|~subactivity(X1,X3)|subactivity(X2,X3))).
% 0.15/1.52 cnf(i_0_202, axiom, (X1!=X2|~subactivity(X3,X1)|subactivity(X3,X2))).
% 0.15/1.52 cnf(i_0_203, axiom, (X1!=X2|~occurrence_of(X1,X3)|occurrence_of(X2,X3))).
% 0.15/1.52 cnf(i_0_204, axiom, (X1!=X2|~occurrence_of(X3,X1)|occurrence_of(X3,X2))).
% 0.15/1.52 cnf(i_0_205, axiom, (X1!=X2|~atocc(X1,X3)|atocc(X2,X3))).
% 0.15/1.52 cnf(i_0_206, axiom, (X1!=X2|~atocc(X3,X1)|atocc(X3,X2))).
% 0.15/1.52 cnf(i_0_207, axiom, (X1!=X2|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X2,X3))).
% 0.15/1.52 cnf(i_0_208, axiom, (X1!=X2|~subactivity_occurrence(X3,X1)|subactivity_occurrence(X3,X2))).
% 0.15/1.52 cnf(i_0_209, axiom, (X1!=X2|~arboreal(X1)|arboreal(X2))).
% 0.15/1.52 cnf(i_0_210, axiom, (X1!=X2|~leaf(X1,X3)|leaf(X2,X3))).
% 0.15/1.52 cnf(i_0_211, axiom, (X1!=X2|~leaf(X3,X1)|leaf(X3,X2))).
% 0.15/1.52 cnf(i_0_212, axiom, (X1!=X2|~leaf_occ(X1,X3)|leaf_occ(X2,X3))).
% 0.15/1.52 cnf(i_0_213, axiom, (X1!=X2|~leaf_occ(X3,X1)|leaf_occ(X3,X2))).
% 0.24/1.61 cnf(i_0_180, axiom, (X1=X1)).
% 0.24/1.61 cnf(i_0_181, axiom, (X1=X2|X2!=X1)).
% 0.24/1.61 cnf(i_0_182, axiom, (X1=X2|X1!=X3|X3!=X2)).
% 0.24/1.61 cnf(i_0_183, axiom, (X1!=X2|~min_precedes(X1,X3,X4)|min_precedes(X2,X3,X4))).
% 0.24/1.61 cnf(i_0_184, axiom, (X1!=X2|~min_precedes(X3,X1,X4)|min_precedes(X3,X2,X4))).
% 0.24/1.61 cnf(i_0_185, axiom, (X1!=X2|~min_precedes(X3,X4,X1)|min_precedes(X3,X4,X2))).
% 0.24/1.61 cnf(i_0_186, axiom, (X1!=X2|~root_occ(X1,X3)|root_occ(X2,X3))).
% 0.24/1.61 cnf(i_0_187, axiom, (X1!=X2|~root_occ(X3,X1)|root_occ(X3,X2))).
% 0.24/1.61 cnf(i_0_188, axiom, (X1!=X2|~root(X1,X3)|root(X2,X3))).
% 0.24/1.61 cnf(i_0_189, axiom, (X1!=X2|~root(X3,X1)|root(X3,X2))).
% 0.24/1.61 cnf(i_0_190, axiom, (X1!=X2|~precedes(X1,X3)|precedes(X2,X3))).
% 0.24/1.61 cnf(i_0_191, axiom, (X1!=X2|~precedes(X3,X1)|precedes(X3,X2))).
% 0.24/1.61 cnf(i_0_192, axiom, (X1!=X2|~atomic(X1)|atomic(X2))).
% 0.24/1.61 cnf(i_0_193, axiom, (X1!=X2|~earlier(X1,X3)|earlier(X2,X3))).
% 0.24/1.61 cnf(i_0_194, axiom, (X1!=X2|~earlier(X3,X1)|earlier(X3,X2))).
% 0.24/1.61 cnf(i_0_195, axiom, (X1!=X2|~legal(X1)|legal(X2))).
% 0.24/1.61 cnf(i_0_196, axiom, (X1!=X2|~activity_occurrence(X1)|activity_occurrence(X2))).
% 0.24/1.61 cnf(i_0_197, axiom, (X1!=X2|~activity(X1)|activity(X2))).
% 0.24/1.61 cnf(i_0_198, axiom, (X1!=X2|~next_subocc(X1,X3,X4)|next_subocc(X2,X3,X4))).
% 0.24/1.61 cnf(i_0_199, axiom, (X1!=X2|~next_subocc(X3,X1,X4)|next_subocc(X3,X2,X4))).
% 0.24/1.61 cnf(i_0_200, axiom, (X1!=X2|~next_subocc(X3,X4,X1)|next_subocc(X3,X4,X2))).
% 0.24/1.61 cnf(i_0_201, axiom, (X1!=X2|~subactivity(X1,X3)|subactivity(X2,X3))).
% 0.24/1.61 cnf(i_0_202, axiom, (X1!=X2|~subactivity(X3,X1)|subactivity(X3,X2))).
% 0.24/1.61 cnf(i_0_203, axiom, (X1!=X2|~occurrence_of(X1,X3)|occurrence_of(X2,X3))).
% 0.24/1.61 cnf(i_0_204, axiom, (X1!=X2|~occurrence_of(X3,X1)|occurrence_of(X3,X2))).
% 0.24/1.61 cnf(i_0_205, axiom, (X1!=X2|~atocc(X1,X3)|atocc(X2,X3))).
% 0.24/1.61 cnf(i_0_206, axiom, (X1!=X2|~atocc(X3,X1)|atocc(X3,X2))).
% 0.24/1.61 cnf(i_0_207, axiom, (X1!=X2|~subactivity_occurrence(X1,X3)|subactivity_occurrence(X2,X3))).
% 0.24/1.61 cnf(i_0_208, axiom, (X1!=X2|~subactivity_occurrence(X3,X1)|subactivity_occurrence(X3,X2))).
% 0.24/1.61 cnf(i_0_209, axiom, (X1!=X2|~arboreal(X1)|arboreal(X2))).
% 0.24/1.61 cnf(i_0_210, axiom, (X1!=X2|~leaf(X1,X3)|leaf(X2,X3))).
% 0.24/1.61 cnf(i_0_211, axiom, (X1!=X2|~leaf(X3,X1)|leaf(X3,X2))).
% 0.24/1.61 cnf(i_0_212, axiom, (X1!=X2|~leaf_occ(X1,X3)|leaf_occ(X2,X3))).
% 0.24/1.61 cnf(i_0_213, axiom, (X1!=X2|~leaf_occ(X3,X1)|leaf_occ(X3,X2))).
% 0.24/1.61 cnf(i_0_214, plain, (leaf_occ(esk17_1(esk18_0),esk18_0)), inference(scs_inference,[],[i_0_167,i_0_148])).
% 0.24/1.61 cnf(i_0_215, plain, (~occurrence_of(X1,tptp0)|leaf_occ(esk17_1(X1),X1)), inference(rename_variables,[],[i_0_148])).
% 0.24/1.61 cnf(i_0_216, plain, (root_occ(esk15_1(esk18_0),esk18_0)), inference(scs_inference,[],[i_0_167,i_0_148,i_0_149])).
% 0.24/1.61 cnf(i_0_217, plain, (~occurrence_of(X1,tptp0)|root_occ(esk15_1(X1),X1)), inference(rename_variables,[],[i_0_149])).
% 0.24/1.61 cnf(i_0_218, plain, (subactivity_occurrence(esk17_1(esk18_0),esk18_0)), inference(scs_inference,[],[i_0_167,i_0_148,i_0_149,i_0_152])).
% 0.24/1.61 cnf(i_0_219, plain, (~leaf_occ(X1,X2)|subactivity_occurrence(X1,X2)), inference(rename_variables,[],[i_0_152])).
% 0.24/1.61 cnf(i_0_220, plain, (subactivity_occurrence(esk15_1(esk18_0),esk18_0)), inference(scs_inference,[],[i_0_167,i_0_148,i_0_149,i_0_152,i_0_153])).
% 0.24/1.61 cnf(i_0_221, plain, (~root_occ(X1,X2)|subactivity_occurrence(X1,X2)), inference(rename_variables,[],[i_0_153])).
% 0.24/1.61 cnf(i_0_222, plain, (subactivity(tptp0,tptp0)), inference(scs_inference,[],[i_0_167,i_0_169,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164])).
% 0.24/1.61 cnf(i_0_223, plain, (~activity(X1)|subactivity(X1,X1)), inference(rename_variables,[],[i_0_164])).
% 0.24/1.61 cnf(i_0_224, plain, (~min_precedes(esk17_1(esk18_0),X1,tptp0)), inference(scs_inference,[],[i_0_167,i_0_169,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105])).
% 0.24/1.61 cnf(i_0_225, plain, (~occurrence_of(X1,X2)|~min_precedes(X3,X4,X2)|~leaf_occ(X3,X1)), inference(rename_variables,[],[i_0_105])).
% 0.24/1.61 cnf(i_0_226, plain, (~min_precedes(X1,esk15_1(esk18_0),tptp0)), inference(scs_inference,[],[i_0_167,i_0_169,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106])).
% 0.24/1.61 cnf(i_0_227, plain, (~occurrence_of(X1,X2)|~min_precedes(X3,X4,X2)|~root_occ(X4,X1)), inference(rename_variables,[],[i_0_106])).
% 0.24/1.61 cnf(i_0_228, plain, (~arboreal(esk18_0)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156])).
% 0.24/1.61 cnf(i_0_229, plain, (~occurrence_of(X1,X2)|atomic(X2)|~arboreal(X1)), inference(rename_variables,[],[i_0_156])).
% 0.24/1.61 cnf(i_0_230, plain, (tptp2!=tptp0), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192])).
% 0.24/1.61 cnf(i_0_231, plain, (~next_subocc(esk18_0,X1,X2)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115])).
% 0.24/1.61 cnf(i_0_232, plain, (arboreal(X1)|~next_subocc(X1,X2,X3)), inference(rename_variables,[],[i_0_115])).
% 0.24/1.61 cnf(i_0_233, plain, (~next_subocc(X1,esk18_0,X2)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116])).
% 0.24/1.61 cnf(i_0_234, plain, (arboreal(X1)|~next_subocc(X2,X1,X3)), inference(rename_variables,[],[i_0_116])).
% 0.24/1.61 cnf(i_0_235, plain, (min_precedes(esk17_1(esk18_0),esk20_2(esk17_1(esk18_0),esk17_1(esk18_0)),tptp0)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101])).
% 0.24/1.61 cnf(i_0_236, plain, (min_precedes(X1,esk19_2(X1,X2),tptp0)|min_precedes(X1,esk20_2(X1,X2),tptp0)|~leaf_occ(X2,esk18_0)), inference(rename_variables,[],[i_0_101])).
% 0.24/1.61 cnf(i_0_237, plain, (occurrence_of(esk17_1(esk18_0),tptp2)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109])).
% 0.24/1.61 cnf(i_0_238, plain, (min_precedes(X1,esk19_2(X1,X2),tptp0)|~leaf_occ(X2,esk18_0)|occurrence_of(X2,tptp2)), inference(rename_variables,[],[i_0_109])).
% 0.24/1.61 cnf(i_0_239, plain, (min_precedes(X1,esk20_2(esk17_1(esk18_0),esk17_1(esk18_0)),tptp0)|~min_precedes(X1,esk17_1(esk18_0),tptp0)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91])).
% 0.24/1.61 cnf(i_0_240, plain, (~min_precedes(X1,X2,X3)|min_precedes(X4,X2,X3)|~min_precedes(X4,X1,X3)), inference(rename_variables,[],[i_0_91])).
% 0.24/1.61 cnf(i_0_241, plain, (~occurrence_of(esk18_0,tptp2)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143])).
% 0.24/1.61 cnf(i_0_242, plain, (~occurrence_of(X1,X2)|X3=X2|~occurrence_of(X1,X3)), inference(rename_variables,[],[i_0_143])).
% 0.24/1.61 cnf(i_0_243, plain, (arboreal(esk17_1(esk18_0))), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155])).
% 0.24/1.61 cnf(i_0_244, plain, (~occurrence_of(X1,X2)|arboreal(X1)|~atomic(X2)), inference(rename_variables,[],[i_0_155])).
% 0.24/1.61 cnf(i_0_245, plain, (esk20_2(esk17_1(esk18_0),esk17_1(esk18_0))!=esk15_1(esk18_0)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155,i_0_184])).
% 0.24/1.61 cnf(i_0_246, plain, (esk17_1(esk18_0)!=esk18_0), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155,i_0_184,i_0_203])).
% 0.24/1.61 cnf(i_0_247, plain, (tptp0!=tptp2), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155,i_0_184,i_0_203,i_0_204])).
% 0.24/1.61 cnf(i_0_248, plain, (~root_occ(esk20_2(esk17_1(esk18_0),esk17_1(esk18_0)),esk18_0)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155,i_0_184,i_0_203,i_0_204,i_0_227])).
% 0.24/1.61 cnf(i_0_249, plain, (~occurrence_of(X1,X2)|~min_precedes(X3,X4,X2)|~root_occ(X4,X1)), inference(rename_variables,[],[i_0_106])).
% 0.24/1.61 cnf(i_0_250, plain, (X1!=esk17_1(esk18_0)|~min_precedes(X1,esk19_2(esk17_1(esk18_0),esk17_1(esk18_0)),tptp0)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155,i_0_184,i_0_203,i_0_204,i_0_227,i_0_183])).
% 0.24/1.61 cnf(i_0_251, plain, (X1!=tptp0|~min_precedes(esk17_1(esk18_0),esk19_2(esk17_1(esk18_0),esk17_1(esk18_0)),X1)), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_91,i_0_225,i_0_143,i_0_155,i_0_184,i_0_203,i_0_204,i_0_227,i_0_183,i_0_185])).
% 0.24/1.61 cnf(i_0_252, plain, (min_precedes(esk4_2(X1,X2),X1,X2)|~leaf(X1,X2)|root(X1,X2)), inference(rename_variables,[],[i_0_107])).
% 0.24/1.61 cnf(i_0_253, plain, (activity(X1)|esk4_2(esk19_2(esk17_1(esk18_0),esk17_1(esk18_0)),tptp0)!=esk17_1(esk18_0)|tptp0!=X1), inference(scs_inference,[],[i_0_167,i_0_168,i_0_169,i_0_170,i_0_148,i_0_149,i_0_152,i_0_153,i_0_164,i_0_105,i_0_106,i_0_156,i_0_192,i_0_115,i_0_116,i_0_101,i_0_109,i_0_225,i_0_143,i_0_155,i_0_184,i_0_203,i_0_204,i_0_227,i_0_183,i_0_197])).
% 0.24/1.61 cnf(i_0_254, plain, (~min_precedes(esk17_1(esk18_0),esk19_2(esk17_1(esk18_0),esk17_1(esk18_0)),tptp0)), inference(equality_inference,[],[250])).
% 0.24/1.61 cnf(i_0_255, plain, (~min_precedes(esk17_1(esk18_0),esk19_2(esk17_1(esk18_0),esk17_1(esk18_0)),tptp0)), inference(equality_inference,[],[251])).
% 0.24/1.61 cnf(i_0_256,plain, ($false), inference(scs_inference,[],[i_0+235, i_0_224]), ['proof']).
% 0.24/1.61 % SZS output end CNFRefutation
% 0.24/1.61 % Total time : 1.261s
%------------------------------------------------------------------------------