%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : PRO009+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n013.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 01:59:23 PM UTC 2026
% Result : Theorem 0.23s 0.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO009+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.07 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.50 % Computer : n013.cluster.edu
% 0.18/0.50 % Model : x86_64 x86_64
% 0.18/0.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.50 % Memory : 8046.5625MB
% 0.18/0.50 % OS : Linux 6.8.0-71-generic
% 0.18/0.50 % CPULimit : 300
% 0.18/0.50 % WCLimit : 300
% 0.18/0.50 % DateTime : Mon Sep 21 03:41:22 UTC 2026
% 0.18/0.51 % CPUTime :
% 0.23/0.53 % Drodi V4.1.1
% 0.23/0.78 % Refutation found
% 0.23/0.78 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.23/0.78 % SZS output start CNFRefutation for theBenchmark
% 0.23/0.78 fof(f3,axiom,(
% 0.23/0.78 (! [X4,X5,X6] :( ( occurrence_of(X4,X5)& occurrence_of(X4,X6) )=> X5 = X6 ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f8,axiom,(
% 0.23/0.78 (! [X16,X17] :( occurrence_of(X16,X17)=> ( arboreal(X16)<=> atomic(X17) ) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f9,axiom,(
% 0.23/0.78 (! [X18] :( legal(X18)=> arboreal(X18) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f11,axiom,(
% 0.23/0.78 (! [X21,X22] :( precedes(X21,X22)<=> ( earlier(X21,X22)& legal(X22) ) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f14,axiom,(
% 0.23/0.78 (! [X31,X32,X33] :( min_precedes(X31,X32,X33)=> (? [X34] :( root(X34,X33)& min_precedes(X34,X32,X33) ) )) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f15,axiom,(
% 0.23/0.78 (! [X35,X36,X37] :( min_precedes(X35,X36,X37)=> ~ root(X36,X37) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f16,axiom,(
% 0.23/0.78 (! [X38,X39,X40] :( min_precedes(X38,X39,X40)=> precedes(X38,X39) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f23,axiom,(
% 0.23/0.78 (! [X60,X61,X62] :( next_subocc(X60,X61,X62)<=> ( min_precedes(X60,X61,X62)& ~ (? [X63] :( min_precedes(X60,X63,X62)& min_precedes(X63,X61,X62) ) )) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f29,axiom,(
% 0.23/0.78 (! [X79,X80,X81,X82] :( ( occurrence_of(X80,X79)& arboreal(X81)& arboreal(X82)& subactivity_occurrence(X81,X80)& subactivity_occurrence(X82,X80) )=> ( min_precedes(X81,X82,X79)| min_precedes(X82,X81,X79)| X81 = X82 ) ) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f34,axiom,(
% 0.23/0.78 (! [X99,X100] :( root_occ(X99,X100)<=> (? [X101] :( occurrence_of(X100,X101)& subactivity_occurrence(X99,X100)& root(X99,X101) ) )) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f35,axiom,(
% 0.23/0.78 (! [X102,X103] :( leaf_occ(X102,X103)<=> (? [X104] :( occurrence_of(X103,X104)& subactivity_occurrence(X102,X103)& leaf(X102,X104) ) )) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f36,axiom,(
% 0.23/0.78 (! [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,tptp2)| occurrence_of(X108,tptp1) )& next_subocc(X107,X108,tptp0)& leaf_occ(X108,X105) ) )) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f42,axiom,(
% 0.23/0.78 atomic(tptp3) ),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f49,conjecture,(
% 0.23/0.78 (! [X109] :( occurrence_of(X109,tptp0)=> (? [X110,X111] :( occurrence_of(X110,tptp3)& root_occ(X110,X109)& ( occurrence_of(X111,tptp2)| occurrence_of(X111,tptp1) )& min_precedes(X110,X111,tptp0)& leaf_occ(X111,X109) ) )) )),
% 0.23/0.78 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.23/0.78 fof(f50,negated_conjecture,(
% 0.23/0.78 ~((! [X109] :( occurrence_of(X109,tptp0)=> (? [X110,X111] :( occurrence_of(X110,tptp3)& root_occ(X110,X109)& ( occurrence_of(X111,tptp2)| occurrence_of(X111,tptp1) )& min_precedes(X110,X111,tptp0)& leaf_occ(X111,X109) ) )) ))),
% 0.23/0.78 inference(negated_conjecture,[status(cth)],[f49])).
% 0.23/0.78 fof(f58,plain,(
% 0.23/0.78 ![X4,X5,X6]: ((~occurrence_of(X4,X5)|~occurrence_of(X4,X6))|X5=X6)),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f3])).
% 0.23/0.78 fof(f59,plain,(
% 0.23/0.78 ![X5,X6]: ((![X4]: (~occurrence_of(X4,X5)|~occurrence_of(X4,X6)))|X5=X6)),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f58])).
% 0.23/0.78 fof(f60,plain,(
% 0.23/0.78 ![X0,X1,X2]: (~occurrence_of(X0,X1)|~occurrence_of(X0,X2)|X1=X2)),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f59])).
% 0.23/0.78 fof(f71,plain,(
% 0.23/0.78 ![X16,X17]: (~occurrence_of(X16,X17)|(arboreal(X16)<=>atomic(X17)))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f8])).
% 0.23/0.78 fof(f72,plain,(
% 0.23/0.78 ![X16,X17]: (~occurrence_of(X16,X17)|((~arboreal(X16)|atomic(X17))&(arboreal(X16)|~atomic(X17))))),
% 0.23/0.78 inference(NNF_transformation,[status(thm)],[f71])).
% 0.23/0.78 fof(f74,plain,(
% 0.23/0.78 ![X0,X1]: (~occurrence_of(X0,X1)|arboreal(X0)|~atomic(X1))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f72])).
% 0.23/0.78 fof(f75,plain,(
% 0.23/0.78 ![X18]: (~legal(X18)|arboreal(X18))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f9])).
% 0.23/0.78 fof(f76,plain,(
% 0.23/0.78 ![X0]: (~legal(X0)|arboreal(X0))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f75])).
% 0.23/0.78 fof(f80,plain,(
% 0.23/0.78 ![X21,X22]: ((~precedes(X21,X22)|(earlier(X21,X22)&legal(X22)))&(precedes(X21,X22)|(~earlier(X21,X22)|~legal(X22))))),
% 0.23/0.78 inference(NNF_transformation,[status(thm)],[f11])).
% 0.23/0.78 fof(f81,plain,(
% 0.23/0.78 (![X21,X22]: (~precedes(X21,X22)|(earlier(X21,X22)&legal(X22))))&(![X21,X22]: (precedes(X21,X22)|(~earlier(X21,X22)|~legal(X22))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f80])).
% 0.23/0.78 fof(f83,plain,(
% 0.23/0.78 ![X0,X1]: (~precedes(X0,X1)|legal(X1))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f81])).
% 0.23/0.78 fof(f96,plain,(
% 0.23/0.78 ![X31,X32,X33]: (~min_precedes(X31,X32,X33)|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f14])).
% 0.23/0.78 fof(f97,plain,(
% 0.23/0.78 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(?[X34]: (root(X34,X33)&min_precedes(X34,X32,X33))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f96])).
% 0.23/0.78 fof(f98,plain,(
% 0.23/0.78 ![X32,X33]: ((![X31]: ~min_precedes(X31,X32,X33))|(root(sK4_skl(X33,X32),X33)&min_precedes(sK4_skl(X33,X32),X32,X33)))),
% 0.23/0.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK4_skl]),skolemize(X34,sK4_skl(X33,X32))],[f97])).
% 0.23/0.78 fof(f100,plain,(
% 0.23/0.78 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|min_precedes(sK4_skl(X2,X1),X1,X2))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f98])).
% 0.23/0.78 fof(f101,plain,(
% 0.23/0.78 ![X35,X36,X37]: (~min_precedes(X35,X36,X37)|~root(X36,X37))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f15])).
% 0.23/0.78 fof(f102,plain,(
% 0.23/0.78 ![X36,X37]: ((![X35]: ~min_precedes(X35,X36,X37))|~root(X36,X37))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f101])).
% 0.23/0.78 fof(f103,plain,(
% 0.23/0.78 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|~root(X1,X2))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f102])).
% 0.23/0.78 fof(f104,plain,(
% 0.23/0.78 ![X38,X39,X40]: (~min_precedes(X38,X39,X40)|precedes(X38,X39))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f16])).
% 0.23/0.78 fof(f105,plain,(
% 0.23/0.78 ![X38,X39]: ((![X40]: ~min_precedes(X38,X39,X40))|precedes(X38,X39))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f104])).
% 0.23/0.78 fof(f106,plain,(
% 0.23/0.78 ![X0,X1,X2]: (~min_precedes(X0,X1,X2)|precedes(X0,X1))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f105])).
% 0.23/0.78 fof(f129,plain,(
% 0.23/0.78 ![X60,X61,X62]: (next_subocc(X60,X61,X62)<=>(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f23])).
% 0.23/0.78 fof(f130,plain,(
% 0.23/0.78 ![X60,X61,X62]: ((~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62)))))&(next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 0.23/0.78 inference(NNF_transformation,[status(thm)],[f129])).
% 0.23/0.78 fof(f131,plain,(
% 0.23/0.78 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(?[X63]: (min_precedes(X60,X63,X62)&min_precedes(X63,X61,X62))))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f130])).
% 0.23/0.78 fof(f132,plain,(
% 0.23/0.78 (![X60,X61,X62]: (~next_subocc(X60,X61,X62)|(min_precedes(X60,X61,X62)&(![X63]: (~min_precedes(X60,X63,X62)|~min_precedes(X63,X61,X62))))))&(![X60,X61,X62]: (next_subocc(X60,X61,X62)|(~min_precedes(X60,X61,X62)|(min_precedes(X60,sK7_skl(X62,X61,X60),X62)&min_precedes(sK7_skl(X62,X61,X60),X61,X62)))))),
% 0.23/0.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(X63,sK7_skl(X62,X61,X60))],[f131])).
% 0.23/0.78 fof(f133,plain,(
% 0.23/0.78 ![X0,X1,X2]: (~next_subocc(X0,X1,X2)|min_precedes(X0,X1,X2))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f132])).
% 0.23/0.78 fof(f160,plain,(
% 0.23/0.78 ![X79,X80,X81,X82]: (((((~occurrence_of(X80,X79)|~arboreal(X81))|~arboreal(X82))|~subactivity_occurrence(X81,X80))|~subactivity_occurrence(X82,X80))|((min_precedes(X81,X82,X79)|min_precedes(X82,X81,X79))|X81=X82))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f29])).
% 0.23/0.78 fof(f161,plain,(
% 0.23/0.78 ![X79,X81,X82]: ((![X80]: ((((~occurrence_of(X80,X79)|~arboreal(X81))|~arboreal(X82))|~subactivity_occurrence(X81,X80))|~subactivity_occurrence(X82,X80)))|((min_precedes(X81,X82,X79)|min_precedes(X82,X81,X79))|X81=X82))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f160])).
% 0.23/0.78 fof(f162,plain,(
% 0.23/0.78 ![X0,X1,X2,X3]: (~occurrence_of(X0,X1)|~arboreal(X2)|~arboreal(X3)|~subactivity_occurrence(X2,X0)|~subactivity_occurrence(X3,X0)|min_precedes(X2,X3,X1)|min_precedes(X3,X2,X1)|X2=X3)),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f161])).
% 0.23/0.78 fof(f177,plain,(
% 0.23/0.78 ![X99,X100]: ((~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101))))&(root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 0.23/0.78 inference(NNF_transformation,[status(thm)],[f34])).
% 0.23/0.78 fof(f178,plain,(
% 0.23/0.78 (![X99,X100]: (~root_occ(X99,X100)|(?[X101]: ((occurrence_of(X100,X101)&subactivity_occurrence(X99,X100))&root(X99,X101)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f177])).
% 0.23/0.78 fof(f179,plain,(
% 0.23/0.78 (![X99,X100]: (~root_occ(X99,X100)|((occurrence_of(X100,sK13_skl(X100,X99))&subactivity_occurrence(X99,X100))&root(X99,sK13_skl(X100,X99)))))&(![X99,X100]: (root_occ(X99,X100)|(![X101]: ((~occurrence_of(X100,X101)|~subactivity_occurrence(X99,X100))|~root(X99,X101)))))),
% 0.23/0.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK13_skl]),skolemize(X101,sK13_skl(X100,X99))],[f178])).
% 0.23/0.78 fof(f180,plain,(
% 0.23/0.78 ![X0,X1]: (~root_occ(X0,X1)|occurrence_of(X1,sK13_skl(X1,X0)))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f179])).
% 0.23/0.78 fof(f181,plain,(
% 0.23/0.78 ![X0,X1]: (~root_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f179])).
% 0.23/0.78 fof(f182,plain,(
% 0.23/0.78 ![X0,X1]: (~root_occ(X0,X1)|root(X0,sK13_skl(X1,X0)))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f179])).
% 0.23/0.78 fof(f183,plain,(
% 0.23/0.78 ![X0,X1,X2]: (root_occ(X0,X1)|~occurrence_of(X1,X2)|~subactivity_occurrence(X0,X1)|~root(X0,X2))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f179])).
% 0.23/0.78 fof(f184,plain,(
% 0.23/0.78 ![X102,X103]: ((~leaf_occ(X102,X103)|(?[X104]: ((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104))))&(leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 0.23/0.78 inference(NNF_transformation,[status(thm)],[f35])).
% 0.23/0.78 fof(f185,plain,(
% 0.23/0.78 (![X102,X103]: (~leaf_occ(X102,X103)|(?[X104]: ((occurrence_of(X103,X104)&subactivity_occurrence(X102,X103))&leaf(X102,X104)))))&(![X102,X103]: (leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f184])).
% 0.23/0.78 fof(f186,plain,(
% 0.23/0.78 (![X102,X103]: (~leaf_occ(X102,X103)|((occurrence_of(X103,sK14_skl(X103,X102))&subactivity_occurrence(X102,X103))&leaf(X102,sK14_skl(X103,X102)))))&(![X102,X103]: (leaf_occ(X102,X103)|(![X104]: ((~occurrence_of(X103,X104)|~subactivity_occurrence(X102,X103))|~leaf(X102,X104)))))),
% 0.23/0.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK14_skl]),skolemize(X104,sK14_skl(X103,X102))],[f185])).
% 0.23/0.78 fof(f188,plain,(
% 0.23/0.78 ![X0,X1]: (~leaf_occ(X0,X1)|subactivity_occurrence(X0,X1))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f186])).
% 0.23/0.78 fof(f191,plain,(
% 0.23/0.78 ![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,tptp2)|occurrence_of(X108,tptp1)))&next_subocc(X107,X108,tptp0))&leaf_occ(X108,X105))))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f36])).
% 0.23/0.78 fof(f192,plain,(
% 0.23/0.78 ![X105]: (~occurrence_of(X105,tptp0)|(?[X108]: ((?[X107]: (((?[X106]: (((occurrence_of(X106,tptp3)&root_occ(X106,X105))&occurrence_of(X107,tptp4))&next_subocc(X106,X107,tptp0)))&(occurrence_of(X108,tptp2)|occurrence_of(X108,tptp1)))&next_subocc(X107,X108,tptp0)))&leaf_occ(X108,X105))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f191])).
% 0.23/0.78 fof(f193,plain,(
% 0.23/0.78 ![X105]: (~occurrence_of(X105,tptp0)|((((((occurrence_of(sK17_skl(X105),tptp3)&root_occ(sK17_skl(X105),X105))&occurrence_of(sK16_skl(X105),tptp4))&next_subocc(sK17_skl(X105),sK16_skl(X105),tptp0))&(occurrence_of(sK15_skl(X105),tptp2)|occurrence_of(sK15_skl(X105),tptp1)))&next_subocc(sK16_skl(X105),sK15_skl(X105),tptp0))&leaf_occ(sK15_skl(X105),X105)))),
% 0.23/0.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK15_skl,sK16_skl,sK17_skl]),skolemize(X108,sK15_skl(X105)),skolemize(X107,sK16_skl(X105)),skolemize(X106,sK17_skl(X105))],[f192])).
% 0.23/0.78 fof(f194,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK17_skl(X0),tptp3))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f193])).
% 0.23/0.78 fof(f195,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp0)|root_occ(sK17_skl(X0),X0))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f193])).
% 0.23/0.78 fof(f198,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp0)|occurrence_of(sK15_skl(X0),tptp2)|occurrence_of(sK15_skl(X0),tptp1))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f193])).
% 0.23/0.78 fof(f199,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp0)|next_subocc(sK16_skl(X0),sK15_skl(X0),tptp0))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f193])).
% 0.23/0.78 fof(f200,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp0)|leaf_occ(sK15_skl(X0),X0))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f193])).
% 0.23/0.78 fof(f206,plain,(
% 0.23/0.78 atomic(tptp3)),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f42])).
% 0.23/0.78 fof(f213,plain,(
% 0.23/0.78 (?[X109]: (occurrence_of(X109,tptp0)&(![X110,X111]: ((((~occurrence_of(X110,tptp3)|~root_occ(X110,X109))|(~occurrence_of(X111,tptp2)&~occurrence_of(X111,tptp1)))|~min_precedes(X110,X111,tptp0))|~leaf_occ(X111,X109)))))),
% 0.23/0.78 inference(pre_NNF_transformation,[status(thm)],[f50])).
% 0.23/0.78 fof(f214,plain,(
% 0.23/0.78 ?[X109]: (occurrence_of(X109,tptp0)&(![X111]: ((![X110]: (((~occurrence_of(X110,tptp3)|~root_occ(X110,X109))|(~occurrence_of(X111,tptp2)&~occurrence_of(X111,tptp1)))|~min_precedes(X110,X111,tptp0)))|~leaf_occ(X111,X109))))),
% 0.23/0.78 inference(miniscoping,[status(thm)],[f213])).
% 0.23/0.78 fof(f215,plain,(
% 0.23/0.78 (occurrence_of(sK18_skl,tptp0)&(![X111]: ((![X110]: (((~occurrence_of(X110,tptp3)|~root_occ(X110,sK18_skl))|(~occurrence_of(X111,tptp2)&~occurrence_of(X111,tptp1)))|~min_precedes(X110,X111,tptp0)))|~leaf_occ(X111,sK18_skl))))),
% 0.23/0.78 inference(skolemize,[status(esa),new_symbols(skolem,[sK18_skl]),skolemize(X109,sK18_skl)],[f214])).
% 0.23/0.78 fof(f216,plain,(
% 0.23/0.78 occurrence_of(sK18_skl,tptp0)),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f215])).
% 0.23/0.78 fof(f217,plain,(
% 0.23/0.78 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK18_skl)|~occurrence_of(X1,tptp2)|~min_precedes(X0,X1,tptp0)|~leaf_occ(X1,sK18_skl))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f215])).
% 0.23/0.78 fof(f218,plain,(
% 0.23/0.78 ![X0,X1]: (~occurrence_of(X0,tptp3)|~root_occ(X0,sK18_skl)|~occurrence_of(X1,tptp1)|~min_precedes(X0,X1,tptp0)|~leaf_occ(X1,sK18_skl))),
% 0.23/0.78 inference(cnf_transformation,[status(thm)],[f215])).
% 0.23/0.78 fof(f219,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(sK18_skl,X0)|X0=tptp0)),
% 0.23/0.78 inference(resolution,[status(thm)],[f60,f216])).
% 0.23/0.78 fof(f232,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp0)|min_precedes(sK16_skl(X0),sK15_skl(X0),tptp0))),
% 0.23/0.78 inference(resolution,[status(thm)],[f199,f133])).
% 0.23/0.78 fof(f242,plain,(
% 0.23/0.78 min_precedes(sK16_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)),
% 0.23/0.78 inference(resolution,[status(thm)],[f232,f216])).
% 0.23/0.78 fof(f245,plain,(
% 0.23/0.78 precedes(sK16_skl(sK18_skl),sK15_skl(sK18_skl))),
% 0.23/0.78 inference(resolution,[status(thm)],[f242,f106])).
% 0.23/0.78 fof(f248,plain,(
% 0.23/0.78 legal(sK15_skl(sK18_skl))),
% 0.23/0.78 inference(resolution,[status(thm)],[f245,f83])).
% 0.23/0.78 fof(f279,plain,(
% 0.23/0.78 arboreal(sK15_skl(sK18_skl))),
% 0.23/0.78 inference(resolution,[status(thm)],[f248,f76])).
% 0.23/0.78 fof(f360,plain,(
% 0.23/0.78 min_precedes(sK4_skl(tptp0,sK15_skl(sK18_skl)),sK15_skl(sK18_skl),tptp0)),
% 0.23/0.78 inference(resolution,[status(thm)],[f242,f100])).
% 0.23/0.78 fof(f435,plain,(
% 0.23/0.78 root_occ(sK17_skl(sK18_skl),sK18_skl)),
% 0.23/0.78 inference(resolution,[status(thm)],[f195,f216])).
% 0.23/0.78 fof(f436,plain,(
% 0.23/0.78 root(sK17_skl(sK18_skl),sK13_skl(sK18_skl,sK17_skl(sK18_skl)))),
% 0.23/0.78 inference(resolution,[status(thm)],[f435,f182])).
% 0.23/0.78 fof(f437,plain,(
% 0.23/0.78 occurrence_of(sK18_skl,sK13_skl(sK18_skl,sK17_skl(sK18_skl)))),
% 0.23/0.78 inference(resolution,[status(thm)],[f435,f180])).
% 0.23/0.78 fof(f438,plain,(
% 0.23/0.78 subactivity_occurrence(sK17_skl(sK18_skl),sK18_skl)),
% 0.23/0.78 inference(resolution,[status(thm)],[f435,f181])).
% 0.23/0.78 fof(f439,plain,(
% 0.23/0.78 ![X0,X1]: (~occurrence_of(sK18_skl,X0)|~arboreal(X1)|~arboreal(sK17_skl(sK18_skl))|~subactivity_occurrence(X1,sK18_skl)|min_precedes(X1,sK17_skl(sK18_skl),X0)|min_precedes(sK17_skl(sK18_skl),X1,X0)|X1=sK17_skl(sK18_skl))),
% 0.23/0.78 inference(resolution,[status(thm)],[f438,f162])).
% 0.23/0.78 fof(f443,plain,(
% 0.23/0.78 ![X0]: (root_occ(sK17_skl(sK18_skl),sK18_skl)|~occurrence_of(sK18_skl,X0)|~root(sK17_skl(sK18_skl),X0))),
% 0.23/0.78 inference(resolution,[status(thm)],[f438,f183])).
% 0.23/0.78 fof(f444,definition,(
% 0.23/0.78 ![X0,X1]: (sQ9_spl <=> (~occurrence_of(sK18_skl,X0)|~arboreal(X1)|~subactivity_occurrence(X1,sK18_skl)|min_precedes(X1,sK17_skl(sK18_skl),X0)|min_precedes(sK17_skl(sK18_skl),X1,X0)|X1=sK17_skl(sK18_skl)))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f445,plain,(
% 0.23/0.78 ![X0,X1]: (~occurrence_of(sK18_skl,X0)|~arboreal(X1)|~subactivity_occurrence(X1,sK18_skl)|min_precedes(X1,sK17_skl(sK18_skl),X0)|min_precedes(sK17_skl(sK18_skl),X1,X0)|X1=sK17_skl(sK18_skl)|~sQ9_spl)),
% 0.23/0.78 inference(component_clause,[status(thm)],[f444])).
% 0.23/0.78 fof(f447,definition,(
% 0.23/0.78 sQ10_spl <=> (arboreal(sK17_skl(sK18_skl)))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f450,plain,(
% 0.23/0.78 sQ9_spl|~sQ10_spl),
% 0.23/0.78 inference(split_clause,[status(thm)],[f439,f444,f447])).
% 0.23/0.78 fof(f451,definition,(
% 0.23/0.78 sQ11_spl <=> (root_occ(sK17_skl(sK18_skl),sK18_skl))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f454,definition,(
% 0.23/0.78 ![X0]: (sQ12_spl <=> (~occurrence_of(sK18_skl,X0)|~root(sK17_skl(sK18_skl),X0)))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f455,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(sK18_skl,X0)|~root(sK17_skl(sK18_skl),X0)|~sQ12_spl)),
% 0.23/0.78 inference(component_clause,[status(thm)],[f454])).
% 0.23/0.78 fof(f457,plain,(
% 0.23/0.78 sQ11_spl|sQ12_spl),
% 0.23/0.78 inference(split_clause,[status(thm)],[f443,f451,f454])).
% 0.23/0.78 fof(f581,plain,(
% 0.23/0.78 sK13_skl(sK18_skl,sK17_skl(sK18_skl))=tptp0),
% 0.23/0.78 inference(resolution,[status(thm)],[f437,f219])).
% 0.23/0.78 fof(f591,plain,(
% 0.23/0.78 root(sK17_skl(sK18_skl),tptp0)),
% 0.23/0.78 inference(backward_demodulation,[status(thm)],[f581,f436])).
% 0.23/0.78 fof(f593,plain,(
% 0.23/0.78 ![X0]: (~min_precedes(X0,sK17_skl(sK18_skl),tptp0))),
% 0.23/0.78 inference(resolution,[status(thm)],[f591,f103])).
% 0.23/0.78 fof(f625,plain,(
% 0.23/0.78 leaf_occ(sK15_skl(sK18_skl),sK18_skl)),
% 0.23/0.78 inference(resolution,[status(thm)],[f200,f216])).
% 0.23/0.78 fof(f628,plain,(
% 0.23/0.78 subactivity_occurrence(sK15_skl(sK18_skl),sK18_skl)),
% 0.23/0.78 inference(resolution,[status(thm)],[f625,f188])).
% 0.23/0.78 fof(f637,definition,(
% 0.23/0.78 sQ41_spl <=> (arboreal(sK15_skl(sK18_skl)))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f639,plain,(
% 0.23/0.78 ~arboreal(sK15_skl(sK18_skl))|sQ41_spl),
% 0.23/0.78 inference(component_clause,[status(thm)],[f637])).
% 0.23/0.78 fof(f648,plain,(
% 0.23/0.78 $false|sQ41_spl),
% 0.23/0.78 inference(forward_subsumption_resolution,[status(thm)],[f639,f279])).
% 0.23/0.78 fof(f649,plain,(
% 0.23/0.78 sQ41_spl),
% 0.23/0.78 inference(contradiction_clause,[status(thm)],[f648])).
% 0.23/0.78 fof(f656,plain,(
% 0.23/0.78 occurrence_of(sK17_skl(sK18_skl),tptp3)),
% 0.23/0.78 inference(resolution,[status(thm)],[f194,f216])).
% 0.23/0.78 fof(f658,plain,(
% 0.23/0.78 ![X0]: (~root_occ(sK17_skl(sK18_skl),sK18_skl)|~occurrence_of(X0,tptp1)|~min_precedes(sK17_skl(sK18_skl),X0,tptp0)|~leaf_occ(X0,sK18_skl))),
% 0.23/0.78 inference(resolution,[status(thm)],[f656,f218])).
% 0.23/0.78 fof(f659,plain,(
% 0.23/0.78 ![X0]: (~root_occ(sK17_skl(sK18_skl),sK18_skl)|~occurrence_of(X0,tptp2)|~min_precedes(sK17_skl(sK18_skl),X0,tptp0)|~leaf_occ(X0,sK18_skl))),
% 0.23/0.78 inference(resolution,[status(thm)],[f656,f217])).
% 0.23/0.78 fof(f660,plain,(
% 0.23/0.78 arboreal(sK17_skl(sK18_skl))|~atomic(tptp3)),
% 0.23/0.78 inference(resolution,[status(thm)],[f656,f74])).
% 0.23/0.78 fof(f664,definition,(
% 0.23/0.78 ![X0]: (sQ44_spl <=> (~occurrence_of(X0,tptp1)|~min_precedes(sK17_skl(sK18_skl),X0,tptp0)|~leaf_occ(X0,sK18_skl)))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f665,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp1)|~min_precedes(sK17_skl(sK18_skl),X0,tptp0)|~leaf_occ(X0,sK18_skl)|~sQ44_spl)),
% 0.23/0.78 inference(component_clause,[status(thm)],[f664])).
% 0.23/0.78 fof(f667,plain,(
% 0.23/0.78 ~sQ11_spl|sQ44_spl),
% 0.23/0.78 inference(split_clause,[status(thm)],[f658,f451,f664])).
% 0.23/0.78 fof(f668,definition,(
% 0.23/0.78 ![X0]: (sQ45_spl <=> (~occurrence_of(X0,tptp2)|~min_precedes(sK17_skl(sK18_skl),X0,tptp0)|~leaf_occ(X0,sK18_skl)))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f669,plain,(
% 0.23/0.78 ![X0]: (~occurrence_of(X0,tptp2)|~min_precedes(sK17_skl(sK18_skl),X0,tptp0)|~leaf_occ(X0,sK18_skl)|~sQ45_spl)),
% 0.23/0.78 inference(component_clause,[status(thm)],[f668])).
% 0.23/0.78 fof(f671,plain,(
% 0.23/0.78 ~sQ11_spl|sQ45_spl),
% 0.23/0.78 inference(split_clause,[status(thm)],[f659,f451,f668])).
% 0.23/0.78 fof(f672,definition,(
% 0.23/0.78 sQ46_spl <=> (atomic(tptp3))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f674,plain,(
% 0.23/0.78 ~atomic(tptp3)|sQ46_spl),
% 0.23/0.78 inference(component_clause,[status(thm)],[f672])).
% 0.23/0.78 fof(f675,plain,(
% 0.23/0.78 sQ10_spl|~sQ46_spl),
% 0.23/0.78 inference(split_clause,[status(thm)],[f660,f447,f672])).
% 0.23/0.78 fof(f676,plain,(
% 0.23/0.78 $false|sQ46_spl),
% 0.23/0.78 inference(forward_subsumption_resolution,[status(thm)],[f674,f206])).
% 0.23/0.78 fof(f677,plain,(
% 0.23/0.78 sQ46_spl),
% 0.23/0.78 inference(contradiction_clause,[status(thm)],[f676])).
% 0.23/0.78 fof(f789,plain,(
% 0.23/0.78 ~root(sK17_skl(sK18_skl),tptp0)|~sQ12_spl),
% 0.23/0.78 inference(resolution,[status(thm)],[f455,f216])).
% 0.23/0.78 fof(f790,plain,(
% 0.23/0.78 $false|~sQ12_spl),
% 0.23/0.78 inference(forward_subsumption_resolution,[status(thm)],[f789,f591])).
% 0.23/0.78 fof(f791,plain,(
% 0.23/0.78 ~sQ12_spl),
% 0.23/0.78 inference(contradiction_clause,[status(thm)],[f790])).
% 0.23/0.78 fof(f827,plain,(
% 0.23/0.78 ![X0]: (~arboreal(X0)|~subactivity_occurrence(X0,sK18_skl)|min_precedes(X0,sK17_skl(sK18_skl),tptp0)|min_precedes(sK17_skl(sK18_skl),X0,tptp0)|X0=sK17_skl(sK18_skl)|~sQ9_spl)),
% 0.23/0.78 inference(resolution,[status(thm)],[f445,f216])).
% 0.23/0.78 fof(f828,plain,(
% 0.23/0.78 ![X0]: (~arboreal(X0)|~subactivity_occurrence(X0,sK18_skl)|min_precedes(sK17_skl(sK18_skl),X0,tptp0)|X0=sK17_skl(sK18_skl)|~sQ9_spl)),
% 0.23/0.78 inference(forward_subsumption_resolution,[status(thm)],[f827,f593])).
% 0.23/0.78 fof(f829,plain,(
% 0.23/0.78 ~arboreal(sK15_skl(sK18_skl))|min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)|sK15_skl(sK18_skl)=sK17_skl(sK18_skl)|~sQ9_spl),
% 0.23/0.78 inference(resolution,[status(thm)],[f828,f628])).
% 0.23/0.78 fof(f831,definition,(
% 0.23/0.78 sQ59_spl <=> (min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f834,definition,(
% 0.23/0.78 sQ60_spl <=> (sK15_skl(sK18_skl)=sK17_skl(sK18_skl))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f835,plain,(
% 0.23/0.78 sK15_skl(sK18_skl)=sK17_skl(sK18_skl)|~sQ60_spl),
% 0.23/0.78 inference(component_clause,[status(thm)],[f834])).
% 0.23/0.78 fof(f837,plain,(
% 0.23/0.78 ~sQ41_spl|sQ59_spl|sQ60_spl|~sQ9_spl),
% 0.23/0.78 inference(split_clause,[status(thm)],[f829,f637,f831,f834,f444])).
% 0.23/0.78 fof(f887,plain,(
% 0.23/0.78 min_precedes(sK4_skl(tptp0,sK15_skl(sK18_skl)),sK17_skl(sK18_skl),tptp0)|~sQ60_spl),
% 0.23/0.78 inference(backward_demodulation,[status(thm)],[f835,f360])).
% 0.23/0.78 fof(f918,plain,(
% 0.23/0.78 min_precedes(sK4_skl(tptp0,sK17_skl(sK18_skl)),sK17_skl(sK18_skl),tptp0)|~sQ60_spl),
% 0.23/0.78 inference(forward_demodulation,[status(thm)],[f835,f887])).
% 0.23/0.78 fof(f919,plain,(
% 0.23/0.78 $false|~sQ60_spl),
% 0.23/0.78 inference(forward_subsumption_resolution,[status(thm)],[f918,f593])).
% 0.23/0.78 fof(f920,plain,(
% 0.23/0.78 ~sQ60_spl),
% 0.23/0.78 inference(contradiction_clause,[status(thm)],[f919])).
% 0.23/0.78 fof(f1330,definition,(
% 0.23/0.78 sQ111_spl <=> (leaf_occ(sK15_skl(sK18_skl),sK18_skl))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f1332,plain,(
% 0.23/0.78 ~leaf_occ(sK15_skl(sK18_skl),sK18_skl)|sQ111_spl),
% 0.23/0.78 inference(component_clause,[status(thm)],[f1330])).
% 0.23/0.78 fof(f1344,plain,(
% 0.23/0.78 occurrence_of(sK15_skl(sK18_skl),tptp2)|occurrence_of(sK15_skl(sK18_skl),tptp1)),
% 0.23/0.78 inference(resolution,[status(thm)],[f198,f216])).
% 0.23/0.78 fof(f1345,definition,(
% 0.23/0.78 sQ115_spl <=> (occurrence_of(sK15_skl(sK18_skl),tptp2))),
% 0.23/0.78 introduced(definition,[new_symbols(definition,[sQ115_spl])],[split_symbol_definition])).
% 0.23/0.78 fof(f1346,plain,(
% 0.23/0.78 occurrence_of(sK15_skl(sK18_skl),tptp2)|~sQ115_spl),
% 0.23/0.78 inference(component_clause,[status(thm)],[f1345])).
% 0.23/0.80 fof(f1348,definition,(
% 0.23/0.80 sQ116_spl <=> (occurrence_of(sK15_skl(sK18_skl),tptp1))),
% 0.23/0.80 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.23/0.80 fof(f1349,plain,(
% 0.23/0.80 occurrence_of(sK15_skl(sK18_skl),tptp1)|~sQ116_spl),
% 0.23/0.80 inference(component_clause,[status(thm)],[f1348])).
% 0.23/0.80 fof(f1351,plain,(
% 0.23/0.80 sQ115_spl|sQ116_spl),
% 0.23/0.80 inference(split_clause,[status(thm)],[f1344,f1345,f1348])).
% 0.23/0.80 fof(f1989,plain,(
% 0.23/0.80 ~min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)|~leaf_occ(sK15_skl(sK18_skl),sK18_skl)|~sQ45_spl|~sQ115_spl),
% 0.23/0.80 inference(resolution,[status(thm)],[f669,f1346])).
% 0.23/0.80 fof(f1990,plain,(
% 0.23/0.80 ~sQ59_spl|~sQ111_spl|~sQ45_spl|~sQ115_spl),
% 0.23/0.80 inference(split_clause,[status(thm)],[f1989,f831,f1330,f668,f1345])).
% 0.23/0.80 fof(f2009,plain,(
% 0.23/0.80 ~min_precedes(sK17_skl(sK18_skl),sK15_skl(sK18_skl),tptp0)|~leaf_occ(sK15_skl(sK18_skl),sK18_skl)|~sQ116_spl|~sQ44_spl),
% 0.23/0.80 inference(resolution,[status(thm)],[f1349,f665])).
% 0.23/0.80 fof(f2020,plain,(
% 0.23/0.80 ~sQ59_spl|~sQ111_spl|~sQ116_spl|~sQ44_spl),
% 0.23/0.80 inference(split_clause,[status(thm)],[f2009,f831,f1330,f1348,f664])).
% 0.23/0.80 fof(f2029,plain,(
% 0.23/0.80 $false|sQ111_spl),
% 0.23/0.80 inference(forward_subsumption_resolution,[status(thm)],[f1332,f625])).
% 0.23/0.80 fof(f2030,plain,(
% 0.23/0.80 sQ111_spl),
% 0.23/0.80 inference(contradiction_clause,[status(thm)],[f2029])).
% 0.23/0.80 fof(f2031,plain,(
% 0.23/0.80 $false),
% 0.23/0.80 inference(sat_refutation,[status(thm)],[f450,f457,f649,f667,f671,f675,f677,f791,f837,f920,f1351,f1990,f2020,f2030])).
% 0.23/0.80 % SZS output end CNFRefutation for theBenchmark.p
% 0.23/0.83 % Elapsed time: 0.300356 seconds
% 0.23/0.83 % CPU time: 1.893332 seconds
% 0.23/0.83 % Total memory used: 106.829 MB
% 0.23/0.83 % Net memory used: 105.758 MB
%------------------------------------------------------------------------------