%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP004+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.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:31:44 PM UTC 2026
% Result : Theorem 0.12s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP004+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.35 % Computer : n007.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Mon Sep 21 01:28:36 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.39 % Refutation found
% 0.12/0.39 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.39 fof(f1,conjecture,(
% 0.12/0.39 ( ( (? [U,V,W,X,Y,Z,X1,X2,X4,X5] :( seat(U)& furniture(U)& front(U)& seat(V)& furniture(V)& front(V)& hollywood(W)& city(W)& event(X)& street(Y)& way(Y)& lonely(Y)& chevy(Z)& car(Z)& white(Z)& dirty(Z)& old(Z)& barrel(X,Z)& down(X,Y)& in(X,W)& X1 != X2& fellow(X1)& man(X1)& young(X1)& fellow(X2)& man(X2)& young(X2)& X1 = X4& in(X4,U)& X2 = X5& in(X5,V) ))=> (? [X6,X7,X8,X9,X10,X11,X12,X13,X15,X16] :( seat(X6)& furniture(X6)& front(X6)& seat(X7)& furniture(X7)& front(X7)& hollywood(X8)& city(X8)& event(X9)& chevy(X10)& car(X10)& white(X10)& dirty(X10)& old(X10)& street(X11)& way(X11)& lonely(X11)& barrel(X9,X10)& down(X9,X11)& in(X9,X8)& X12 != X13& fellow(X12)& man(X12)& young(X12)& fellow(X13)& man(X13)& young(X13)& X12 = X15& in(X15,X6)& X13 = X16& in(X16,X7) ) ))& ( (? [X17,X18,X19,X20,X21,X22,X23,X24,X26,X27] :( seat(X17)& furniture(X17)& front(X17)& seat(X18)& furniture(X18)& front(X18)& hollywood(X19)& city(X19)& event(X20)& chevy(X21)& car(X21)& white(X21)& dirty(X21)& old(X21)& street(X22)& way(X22)& lonely(X22)& barrel(X20,X21)& down(X20,X22)& in(X20,X19)& X23 != X24& fellow(X23)& man(X23)& young(X23)& fellow(X24)& man(X24)& young(X24)& X23 = X26& in(X26,X17)& X24 = X27& in(X27,X18) ))=> (? [X28,X29,X30,X31,X32,X33,X34,X35,X37,X38] :( seat(X28)& furniture(X28)& front(X28)& seat(X29)& furniture(X29)& front(X29)& hollywood(X30)& city(X30)& event(X31)& street(X32)& way(X32)& lonely(X32)& chevy(X33)& car(X33)& white(X33)& dirty(X33)& old(X33)& barrel(X31,X33)& down(X31,X32)& in(X31,X30)& X34 != X35& fellow(X34)& man(X34)& young(X34)& fellow(X35)& man(X35)& young(X35)& X34 = X37& in(X37,X28)& X35 = X38& in(X38,X29) ) )) ) ),
% 0.12/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.12/0.39 fof(f2,negated_conjecture,(
% 0.12/0.39 ~(( ( (? [U,V,W,X,Y,Z,X1,X2,X4,X5] :( seat(U)& furniture(U)& front(U)& seat(V)& furniture(V)& front(V)& hollywood(W)& city(W)& event(X)& street(Y)& way(Y)& lonely(Y)& chevy(Z)& car(Z)& white(Z)& dirty(Z)& old(Z)& barrel(X,Z)& down(X,Y)& in(X,W)& X1 != X2& fellow(X1)& man(X1)& young(X1)& fellow(X2)& man(X2)& young(X2)& X1 = X4& in(X4,U)& X2 = X5& in(X5,V) ))=> (? [X6,X7,X8,X9,X10,X11,X12,X13,X15,X16] :( seat(X6)& furniture(X6)& front(X6)& seat(X7)& furniture(X7)& front(X7)& hollywood(X8)& city(X8)& event(X9)& chevy(X10)& car(X10)& white(X10)& dirty(X10)& old(X10)& street(X11)& way(X11)& lonely(X11)& barrel(X9,X10)& down(X9,X11)& in(X9,X8)& X12 != X13& fellow(X12)& man(X12)& young(X12)& fellow(X13)& man(X13)& young(X13)& X12 = X15& in(X15,X6)& X13 = X16& in(X16,X7) ) ))& ( (? [X17,X18,X19,X20,X21,X22,X23,X24,X26,X27] :( seat(X17)& furniture(X17)& front(X17)& seat(X18)& furniture(X18)& front(X18)& hollywood(X19)& city(X19)& event(X20)& chevy(X21)& car(X21)& white(X21)& dirty(X21)& old(X21)& street(X22)& way(X22)& lonely(X22)& barrel(X20,X21)& down(X20,X22)& in(X20,X19)& X23 != X24& fellow(X23)& man(X23)& young(X23)& fellow(X24)& man(X24)& young(X24)& X23 = X26& in(X26,X17)& X24 = X27& in(X27,X18) ))=> (? [X28,X29,X30,X31,X32,X33,X34,X35,X37,X38] :( seat(X28)& furniture(X28)& front(X28)& seat(X29)& furniture(X29)& front(X29)& hollywood(X30)& city(X30)& event(X31)& street(X32)& way(X32)& lonely(X32)& chevy(X33)& car(X33)& white(X33)& dirty(X33)& old(X33)& barrel(X31,X33)& down(X31,X32)& in(X31,X30)& X34 != X35& fellow(X34)& man(X34)& young(X34)& fellow(X35)& man(X35)& young(X35)& X34 = X37& in(X37,X28)& X35 = X38& in(X38,X29) ) )) ) )),
% 0.12/0.39 inference(negated_conjecture,[status(cth)],[f1])).
% 0.12/0.39 fof(f3,plain,(
% 0.12/0.39 (((?[U,V,W,X,Y,Z,X1,X2,X4,X5]: ((((((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&seat(V))&furniture(V))&front(V))&hollywood(W))&city(W))&event(X))&street(Y))&way(Y))&lonely(Y))&chevy(Z))&car(Z))&white(Z))&dirty(Z))&old(Z))&barrel(X,Z))&down(X,Y))&in(X,W))&~X1=X2)&fellow(X1))&man(X1))&young(X1))&fellow(X2))&man(X2))&young(X2))&X1=X4)&in(X4,U))&X2=X5)&in(X5,V)))&(![X6,X7,X8,X9,X10,X11,X12,X13,X15,X16]: ((((((((((((((((((((((((((((((~seat(X6)|~furniture(X6))|~front(X6))|~seat(X7))|~furniture(X7))|~front(X7))|~hollywood(X8))|~city(X8))|~event(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~street(X11))|~way(X11))|~lonely(X11))|~barrel(X9,X10))|~down(X9,X11))|~in(X9,X8))|X12=X13)|~fellow(X12))|~man(X12))|~young(X12))|~fellow(X13))|~man(X13))|~young(X13))|~X12=X15)|~in(X15,X6))|~X13=X16)|~in(X16,X7))))|((?[X17,X18,X19,X20,X21,X22,X23,X24,X26,X27]: ((((((((((((((((((((((((((((((seat(X17)&furniture(X17))&front(X17))&seat(X18))&furniture(X18))&front(X18))&hollywood(X19))&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21))&down(X20,X22))&in(X20,X19))&~X23=X24)&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X17))&X24=X27)&in(X27,X18)))&(![X28,X29,X30,X31,X32,X33,X34,X35,X37,X38]: ((((((((((((((((((((((((((((((~seat(X28)|~furniture(X28))|~front(X28))|~seat(X29))|~furniture(X29))|~front(X29))|~hollywood(X30))|~city(X30))|~event(X31))|~street(X32))|~way(X32))|~lonely(X32))|~chevy(X33))|~car(X33))|~white(X33))|~dirty(X33))|~old(X33))|~barrel(X31,X33))|~down(X31,X32))|~in(X31,X30))|X34=X35)|~fellow(X34))|~man(X34))|~young(X34))|~fellow(X35))|~man(X35))|~young(X35))|~X34=X37)|~in(X37,X28))|~X35=X38)|~in(X38,X29)))))),
% 0.12/0.39 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.39 fof(f4,definition,(
% 0.12/0.39 sP0_prd<=>((?[U,V,W,X,Y,Z,X1,X2,X4,X5]: ((((((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&seat(V))&furniture(V))&front(V))&hollywood(W))&city(W))&event(X))&street(Y))&way(Y))&lonely(Y))&chevy(Z))&car(Z))&white(Z))&dirty(Z))&old(Z))&barrel(X,Z))&down(X,Y))&in(X,W))&~X1=X2)&fellow(X1))&man(X1))&young(X1))&fellow(X2))&man(X2))&young(X2))&X1=X4)&in(X4,U))&X2=X5)&in(X5,V)))&(![X6,X7,X8,X9,X10,X11,X12,X13,X15,X16]: ((((((((((((((((((((((((((((((~seat(X6)|~furniture(X6))|~front(X6))|~seat(X7))|~furniture(X7))|~front(X7))|~hollywood(X8))|~city(X8))|~event(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~street(X11))|~way(X11))|~lonely(X11))|~barrel(X9,X10))|~down(X9,X11))|~in(X9,X8))|X12=X13)|~fellow(X12))|~man(X12))|~young(X12))|~fellow(X13))|~man(X13))|~young(X13))|~X12=X15)|~in(X15,X6))|~X13=X16)|~in(X16,X7))))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.39 fof(f5,plain,(
% 0.12/0.39 sP0_prd|((?[X17,X18,X19,X20,X21,X22,X23,X24,X26,X27]: ((((((((((((((((((((((((((((((seat(X17)&furniture(X17))&front(X17))&seat(X18))&furniture(X18))&front(X18))&hollywood(X19))&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21))&down(X20,X22))&in(X20,X19))&~X23=X24)&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26)&in(X26,X17))&X24=X27)&in(X27,X18)))&(![X28,X29,X30,X31,X32,X33,X34,X35,X37,X38]: ((((((((((((((((((((((((((((((~seat(X28)|~furniture(X28))|~front(X28))|~seat(X29))|~furniture(X29))|~front(X29))|~hollywood(X30))|~city(X30))|~event(X31))|~street(X32))|~way(X32))|~lonely(X32))|~chevy(X33))|~car(X33))|~white(X33))|~dirty(X33))|~old(X33))|~barrel(X31,X33))|~down(X31,X32))|~in(X31,X30))|X34=X35)|~fellow(X34))|~man(X34))|~young(X34))|~fellow(X35))|~man(X35))|~young(X35))|~X34=X37)|~in(X37,X28))|~X35=X38)|~in(X38,X29))))),
% 0.12/0.39 inference(formula_renaming,[status(thm)],[f3,f4])).
% 0.12/0.39 fof(f6,plain,(
% 0.12/0.39 sP0_prd|((?[X18,X27]: ((?[X24]: ((?[X17,X26]: ((?[X23]: (((((((((?[X19,X20]: ((?[X22]: ((?[X21]: (((((((((((((((((seat(X17)&furniture(X17))&front(X17))&seat(X18))&furniture(X18))&front(X18))&hollywood(X19))&city(X19))&event(X20))&chevy(X21))&car(X21))&white(X21))&dirty(X21))&old(X21))&street(X22))&way(X22))&lonely(X22))&barrel(X20,X21)))&down(X20,X22)))&in(X20,X19)))&~X23=X24)&fellow(X23))&man(X23))&young(X23))&fellow(X24))&man(X24))&young(X24))&X23=X26))&in(X26,X17)))&X24=X27))&in(X27,X18)))&(![X29,X38]: ((![X35]: ((![X28,X37]: ((![X34]: (((((((((![X30,X31]: ((![X32]: ((![X33]: (((((((((((((((((~seat(X28)|~furniture(X28))|~front(X28))|~seat(X29))|~furniture(X29))|~front(X29))|~hollywood(X30))|~city(X30))|~event(X31))|~street(X32))|~way(X32))|~lonely(X32))|~chevy(X33))|~car(X33))|~white(X33))|~dirty(X33))|~old(X33))|~barrel(X31,X33)))|~down(X31,X32)))|~in(X31,X30)))|X34=X35)|~fellow(X34))|~man(X34))|~young(X34))|~fellow(X35))|~man(X35))|~young(X35))|~X34=X37))|~in(X37,X28)))|~X35=X38))|~in(X38,X29))))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f5])).
% 0.12/0.39 fof(f7,plain,(
% 0.12/0.39 sP0_prd|(((((((((((((((((((((((((((((((seat(sK3_skl)&furniture(sK3_skl))&front(sK3_skl))&seat(sK0_skl))&furniture(sK0_skl))&front(sK0_skl))&hollywood(sK6_skl))&city(sK6_skl))&event(sK7_skl))&chevy(sK9_skl))&car(sK9_skl))&white(sK9_skl))&dirty(sK9_skl))&old(sK9_skl))&street(sK8_skl))&way(sK8_skl))&lonely(sK8_skl))&barrel(sK7_skl,sK9_skl))&down(sK7_skl,sK8_skl))&in(sK7_skl,sK6_skl))&~sK5_skl=sK2_skl)&fellow(sK5_skl))&man(sK5_skl))&young(sK5_skl))&fellow(sK2_skl))&man(sK2_skl))&young(sK2_skl))&sK5_skl=sK4_skl)&in(sK4_skl,sK3_skl))&sK2_skl=sK1_skl)&in(sK1_skl,sK0_skl))&(![X29,X38]: ((![X35]: ((![X28,X37]: ((![X34]: (((((((((![X30,X31]: ((![X32]: ((![X33]: (((((((((((((((((~seat(X28)|~furniture(X28))|~front(X28))|~seat(X29))|~furniture(X29))|~front(X29))|~hollywood(X30))|~city(X30))|~event(X31))|~street(X32))|~way(X32))|~lonely(X32))|~chevy(X33))|~car(X33))|~white(X33))|~dirty(X33))|~old(X33))|~barrel(X31,X33)))|~down(X31,X32)))|~in(X31,X30)))|X34=X35)|~fellow(X34))|~man(X34))|~young(X34))|~fellow(X35))|~man(X35))|~young(X35))|~X34=X37))|~in(X37,X28)))|~X35=X38))|~in(X38,X29))))),
% 0.12/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl,sK2_skl,sK3_skl,sK4_skl,sK5_skl,sK6_skl,sK7_skl,sK8_skl,sK9_skl]),skolemize(X18,sK0_skl),skolemize(X27,sK1_skl),skolemize(X24,sK2_skl),skolemize(X17,sK3_skl),skolemize(X26,sK4_skl),skolemize(X23,sK5_skl),skolemize(X19,sK6_skl),skolemize(X20,sK7_skl),skolemize(X22,sK8_skl),skolemize(X21,sK9_skl)],[f6])).
% 0.12/0.39 fof(f8,plain,(
% 0.12/0.39 sP0_prd|seat(sK3_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f9,plain,(
% 0.12/0.39 sP0_prd|furniture(sK3_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f10,plain,(
% 0.12/0.39 sP0_prd|front(sK3_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f11,plain,(
% 0.12/0.39 sP0_prd|seat(sK0_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f12,plain,(
% 0.12/0.39 sP0_prd|furniture(sK0_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f13,plain,(
% 0.12/0.39 sP0_prd|front(sK0_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f14,plain,(
% 0.12/0.39 sP0_prd|hollywood(sK6_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f15,plain,(
% 0.12/0.39 sP0_prd|city(sK6_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f16,plain,(
% 0.12/0.39 sP0_prd|event(sK7_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f17,plain,(
% 0.12/0.39 sP0_prd|chevy(sK9_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f18,plain,(
% 0.12/0.39 sP0_prd|car(sK9_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f19,plain,(
% 0.12/0.39 sP0_prd|white(sK9_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f20,plain,(
% 0.12/0.39 sP0_prd|dirty(sK9_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f21,plain,(
% 0.12/0.39 sP0_prd|old(sK9_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f22,plain,(
% 0.12/0.39 sP0_prd|street(sK8_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f23,plain,(
% 0.12/0.39 sP0_prd|way(sK8_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f24,plain,(
% 0.12/0.39 sP0_prd|lonely(sK8_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f25,plain,(
% 0.12/0.39 sP0_prd|barrel(sK7_skl,sK9_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f26,plain,(
% 0.12/0.39 sP0_prd|down(sK7_skl,sK8_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f27,plain,(
% 0.12/0.39 sP0_prd|in(sK7_skl,sK6_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f28,plain,(
% 0.12/0.39 sP0_prd|~sK5_skl=sK2_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f29,plain,(
% 0.12/0.39 sP0_prd|fellow(sK5_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f30,plain,(
% 0.12/0.39 sP0_prd|man(sK5_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f31,plain,(
% 0.12/0.39 sP0_prd|young(sK5_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f32,plain,(
% 0.12/0.39 sP0_prd|fellow(sK2_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f33,plain,(
% 0.12/0.39 sP0_prd|man(sK2_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f34,plain,(
% 0.12/0.39 sP0_prd|young(sK2_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f35,plain,(
% 0.12/0.39 sP0_prd|sK5_skl=sK4_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f36,plain,(
% 0.12/0.39 sP0_prd|in(sK4_skl,sK3_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f37,plain,(
% 0.12/0.39 sP0_prd|sK2_skl=sK1_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f38,plain,(
% 0.12/0.39 sP0_prd|in(sK1_skl,sK0_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f39,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (sP0_prd|~seat(X0)|~furniture(X0)|~front(X0)|~seat(X1)|~furniture(X1)|~front(X1)|~hollywood(X2)|~city(X2)|~event(X3)|~street(X4)|~way(X4)|~lonely(X4)|~chevy(X5)|~car(X5)|~white(X5)|~dirty(X5)|~old(X5)|~barrel(X3,X5)|~down(X3,X4)|~in(X3,X2)|X6=X7|~fellow(X6)|~man(X6)|~young(X6)|~fellow(X7)|~man(X7)|~young(X7)|~X6=X8|~in(X8,X0)|~X7=X9|~in(X9,X1))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.39 fof(f40,plain,(
% 0.12/0.39 (~sP0_prd|((?[U,V,W,X,Y,Z,X1,X2,X4,X5]: ((((((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&seat(V))&furniture(V))&front(V))&hollywood(W))&city(W))&event(X))&street(Y))&way(Y))&lonely(Y))&chevy(Z))&car(Z))&white(Z))&dirty(Z))&old(Z))&barrel(X,Z))&down(X,Y))&in(X,W))&~X1=X2)&fellow(X1))&man(X1))&young(X1))&fellow(X2))&man(X2))&young(X2))&X1=X4)&in(X4,U))&X2=X5)&in(X5,V)))&(![X6,X7,X8,X9,X10,X11,X12,X13,X15,X16]: ((((((((((((((((((((((((((((((~seat(X6)|~furniture(X6))|~front(X6))|~seat(X7))|~furniture(X7))|~front(X7))|~hollywood(X8))|~city(X8))|~event(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~street(X11))|~way(X11))|~lonely(X11))|~barrel(X9,X10))|~down(X9,X11))|~in(X9,X8))|X12=X13)|~fellow(X12))|~man(X12))|~young(X12))|~fellow(X13))|~man(X13))|~young(X13))|~X12=X15)|~in(X15,X6))|~X13=X16)|~in(X16,X7)))))&(sP0_prd|((![U,V,W,X,Y,Z,X1,X2,X4,X5]: ((((((((((((((((((((((((((((((~seat(U)|~furniture(U))|~front(U))|~seat(V))|~furniture(V))|~front(V))|~hollywood(W))|~city(W))|~event(X))|~street(Y))|~way(Y))|~lonely(Y))|~chevy(Z))|~car(Z))|~white(Z))|~dirty(Z))|~old(Z))|~barrel(X,Z))|~down(X,Y))|~in(X,W))|X1=X2)|~fellow(X1))|~man(X1))|~young(X1))|~fellow(X2))|~man(X2))|~young(X2))|~X1=X4)|~in(X4,U))|~X2=X5)|~in(X5,V)))|(?[X6,X7,X8,X9,X10,X11,X12,X13,X15,X16]: ((((((((((((((((((((((((((((((seat(X6)&furniture(X6))&front(X6))&seat(X7))&furniture(X7))&front(X7))&hollywood(X8))&city(X8))&event(X9))&chevy(X10))&car(X10))&white(X10))&dirty(X10))&old(X10))&street(X11))&way(X11))&lonely(X11))&barrel(X9,X10))&down(X9,X11))&in(X9,X8))&~X12=X13)&fellow(X12))&man(X12))&young(X12))&fellow(X13))&man(X13))&young(X13))&X12=X15)&in(X15,X6))&X13=X16)&in(X16,X7)))))),
% 0.12/0.39 inference(NNF_transformation,[status(thm)],[f4])).
% 0.12/0.39 fof(f41,plain,(
% 0.12/0.39 (~sP0_prd|((?[V,X5]: ((?[X2]: ((?[U,X4]: ((?[X1]: (((((((((?[W,X]: ((?[Y]: ((?[Z]: (((((((((((((((((seat(U)&furniture(U))&front(U))&seat(V))&furniture(V))&front(V))&hollywood(W))&city(W))&event(X))&street(Y))&way(Y))&lonely(Y))&chevy(Z))&car(Z))&white(Z))&dirty(Z))&old(Z))&barrel(X,Z)))&down(X,Y)))&in(X,W)))&~X1=X2)&fellow(X1))&man(X1))&young(X1))&fellow(X2))&man(X2))&young(X2))&X1=X4))&in(X4,U)))&X2=X5))&in(X5,V)))&(![X7,X16]: ((![X13]: ((![X6,X15]: ((![X12]: (((((((((![X8,X9]: ((![X11]: ((![X10]: (((((((((((((((((~seat(X6)|~furniture(X6))|~front(X6))|~seat(X7))|~furniture(X7))|~front(X7))|~hollywood(X8))|~city(X8))|~event(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~street(X11))|~way(X11))|~lonely(X11))|~barrel(X9,X10)))|~down(X9,X11)))|~in(X9,X8)))|X12=X13)|~fellow(X12))|~man(X12))|~young(X12))|~fellow(X13))|~man(X13))|~young(X13))|~X12=X15))|~in(X15,X6)))|~X13=X16))|~in(X16,X7)))))&(sP0_prd|((![V,X5]: ((![X2]: ((![U,X4]: ((![X1]: (((((((((![W,X]: ((![Y]: ((![Z]: (((((((((((((((((~seat(U)|~furniture(U))|~front(U))|~seat(V))|~furniture(V))|~front(V))|~hollywood(W))|~city(W))|~event(X))|~street(Y))|~way(Y))|~lonely(Y))|~chevy(Z))|~car(Z))|~white(Z))|~dirty(Z))|~old(Z))|~barrel(X,Z)))|~down(X,Y)))|~in(X,W)))|X1=X2)|~fellow(X1))|~man(X1))|~young(X1))|~fellow(X2))|~man(X2))|~young(X2))|~X1=X4))|~in(X4,U)))|~X2=X5))|~in(X5,V)))|(?[X7,X16]: ((?[X13]: ((?[X6,X15]: ((?[X12]: (((((((((?[X8,X9]: ((?[X11]: ((?[X10]: (((((((((((((((((seat(X6)&furniture(X6))&front(X6))&seat(X7))&furniture(X7))&front(X7))&hollywood(X8))&city(X8))&event(X9))&chevy(X10))&car(X10))&white(X10))&dirty(X10))&old(X10))&street(X11))&way(X11))&lonely(X11))&barrel(X9,X10)))&down(X9,X11)))&in(X9,X8)))&~X12=X13)&fellow(X12))&man(X12))&young(X12))&fellow(X13))&man(X13))&young(X13))&X12=X15))&in(X15,X6)))&X13=X16))&in(X16,X7)))))),
% 0.12/0.39 inference(miniscoping,[status(thm)],[f40])).
% 0.12/0.39 fof(f42,plain,(
% 0.12/0.39 (~sP0_prd|(((((((((((((((((((((((((((((((seat(sK13_skl)&furniture(sK13_skl))&front(sK13_skl))&seat(sK10_skl))&furniture(sK10_skl))&front(sK10_skl))&hollywood(sK16_skl))&city(sK16_skl))&event(sK17_skl))&street(sK18_skl))&way(sK18_skl))&lonely(sK18_skl))&chevy(sK19_skl))&car(sK19_skl))&white(sK19_skl))&dirty(sK19_skl))&old(sK19_skl))&barrel(sK17_skl,sK19_skl))&down(sK17_skl,sK18_skl))&in(sK17_skl,sK16_skl))&~sK15_skl=sK12_skl)&fellow(sK15_skl))&man(sK15_skl))&young(sK15_skl))&fellow(sK12_skl))&man(sK12_skl))&young(sK12_skl))&sK15_skl=sK14_skl)&in(sK14_skl,sK13_skl))&sK12_skl=sK11_skl)&in(sK11_skl,sK10_skl))&(![X7,X16]: ((![X13]: ((![X6,X15]: ((![X12]: (((((((((![X8,X9]: ((![X11]: ((![X10]: (((((((((((((((((~seat(X6)|~furniture(X6))|~front(X6))|~seat(X7))|~furniture(X7))|~front(X7))|~hollywood(X8))|~city(X8))|~event(X9))|~chevy(X10))|~car(X10))|~white(X10))|~dirty(X10))|~old(X10))|~street(X11))|~way(X11))|~lonely(X11))|~barrel(X9,X10)))|~down(X9,X11)))|~in(X9,X8)))|X12=X13)|~fellow(X12))|~man(X12))|~young(X12))|~fellow(X13))|~man(X13))|~young(X13))|~X12=X15))|~in(X15,X6)))|~X13=X16))|~in(X16,X7)))))&(sP0_prd|((![V,X5]: ((![X2]: ((![U,X4]: ((![X1]: (((((((((![W,X]: ((![Y]: ((![Z]: (((((((((((((((((~seat(U)|~furniture(U))|~front(U))|~seat(V))|~furniture(V))|~front(V))|~hollywood(W))|~city(W))|~event(X))|~street(Y))|~way(Y))|~lonely(Y))|~chevy(Z))|~car(Z))|~white(Z))|~dirty(Z))|~old(Z))|~barrel(X,Z)))|~down(X,Y)))|~in(X,W)))|X1=X2)|~fellow(X1))|~man(X1))|~young(X1))|~fellow(X2))|~man(X2))|~young(X2))|~X1=X4))|~in(X4,U)))|~X2=X5))|~in(X5,V)))|((((((((((((((((((((((((((((((seat(sK23_skl)&furniture(sK23_skl))&front(sK23_skl))&seat(sK20_skl))&furniture(sK20_skl))&front(sK20_skl))&hollywood(sK26_skl))&city(sK26_skl))&event(sK27_skl))&chevy(sK29_skl))&car(sK29_skl))&white(sK29_skl))&dirty(sK29_skl))&old(sK29_skl))&street(sK28_skl))&way(sK28_skl))&lonely(sK28_skl))&barrel(sK27_skl,sK29_skl))&down(sK27_skl,sK28_skl))&in(sK27_skl,sK26_skl))&~sK25_skl=sK22_skl)&fellow(sK25_skl))&man(sK25_skl))&young(sK25_skl))&fellow(sK22_skl))&man(sK22_skl))&young(sK22_skl))&sK25_skl=sK24_skl)&in(sK24_skl,sK23_skl))&sK22_skl=sK21_skl)&in(sK21_skl,sK20_skl))))),
% 0.12/0.39 inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl,sK13_skl,sK14_skl,sK15_skl,sK16_skl,sK17_skl,sK18_skl,sK19_skl,sK20_skl,sK21_skl,sK22_skl,sK23_skl,sK24_skl,sK25_skl,sK26_skl,sK27_skl,sK28_skl,sK29_skl]),skolemize(V,sK10_skl),skolemize(X5,sK11_skl),skolemize(X2,sK12_skl),skolemize(U,sK13_skl),skolemize(X4,sK14_skl),skolemize(X1,sK15_skl),skolemize(W,sK16_skl),skolemize(X,sK17_skl),skolemize(Y,sK18_skl),skolemize(Z,sK19_skl),skolemize(X7,sK20_skl),skolemize(X16,sK21_skl),skolemize(X13,sK22_skl),skolemize(X6,sK23_skl),skolemize(X15,sK24_skl),skolemize(X12,sK25_skl),skolemize(X8,sK26_skl),skolemize(X9,sK27_skl),skolemize(X11,sK28_skl),skolemize(X10,sK29_skl)],[f41])).
% 0.12/0.39 fof(f43,plain,(
% 0.12/0.39 ~sP0_prd|seat(sK13_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f44,plain,(
% 0.12/0.39 ~sP0_prd|furniture(sK13_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f45,plain,(
% 0.12/0.39 ~sP0_prd|front(sK13_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f46,plain,(
% 0.12/0.39 ~sP0_prd|seat(sK10_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f47,plain,(
% 0.12/0.39 ~sP0_prd|furniture(sK10_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f48,plain,(
% 0.12/0.39 ~sP0_prd|front(sK10_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f49,plain,(
% 0.12/0.39 ~sP0_prd|hollywood(sK16_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f50,plain,(
% 0.12/0.39 ~sP0_prd|city(sK16_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f51,plain,(
% 0.12/0.39 ~sP0_prd|event(sK17_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f52,plain,(
% 0.12/0.39 ~sP0_prd|street(sK18_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f53,plain,(
% 0.12/0.39 ~sP0_prd|way(sK18_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f54,plain,(
% 0.12/0.39 ~sP0_prd|lonely(sK18_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f55,plain,(
% 0.12/0.39 ~sP0_prd|chevy(sK19_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f56,plain,(
% 0.12/0.39 ~sP0_prd|car(sK19_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f57,plain,(
% 0.12/0.39 ~sP0_prd|white(sK19_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f58,plain,(
% 0.12/0.39 ~sP0_prd|dirty(sK19_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f59,plain,(
% 0.12/0.39 ~sP0_prd|old(sK19_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f60,plain,(
% 0.12/0.39 ~sP0_prd|barrel(sK17_skl,sK19_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f61,plain,(
% 0.12/0.39 ~sP0_prd|down(sK17_skl,sK18_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f62,plain,(
% 0.12/0.39 ~sP0_prd|in(sK17_skl,sK16_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f63,plain,(
% 0.12/0.39 ~sP0_prd|~sK15_skl=sK12_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f64,plain,(
% 0.12/0.39 ~sP0_prd|fellow(sK15_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f65,plain,(
% 0.12/0.39 ~sP0_prd|man(sK15_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f66,plain,(
% 0.12/0.39 ~sP0_prd|young(sK15_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f67,plain,(
% 0.12/0.39 ~sP0_prd|fellow(sK12_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f68,plain,(
% 0.12/0.39 ~sP0_prd|man(sK12_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f69,plain,(
% 0.12/0.39 ~sP0_prd|young(sK12_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f70,plain,(
% 0.12/0.39 ~sP0_prd|sK15_skl=sK14_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f71,plain,(
% 0.12/0.39 ~sP0_prd|in(sK14_skl,sK13_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f72,plain,(
% 0.12/0.39 ~sP0_prd|sK12_skl=sK11_skl),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f73,plain,(
% 0.12/0.39 ~sP0_prd|in(sK11_skl,sK10_skl)),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f74,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~sP0_prd|~seat(X0)|~furniture(X0)|~front(X0)|~seat(X1)|~furniture(X1)|~front(X1)|~hollywood(X2)|~city(X2)|~event(X3)|~chevy(X4)|~car(X4)|~white(X4)|~dirty(X4)|~old(X4)|~street(X5)|~way(X5)|~lonely(X5)|~barrel(X3,X4)|~down(X3,X5)|~in(X3,X2)|X6=X7|~fellow(X6)|~man(X6)|~young(X6)|~fellow(X7)|~man(X7)|~young(X7)|~X6=X8|~in(X8,X0)|~X7=X9|~in(X9,X1))),
% 0.12/0.39 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.39 fof(f106,definition,(
% 0.12/0.39 sQ0_spl <=> (sP0_prd)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f109,definition,(
% 0.12/0.39 sQ1_spl <=> (seat(sK3_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f112,plain,(
% 0.12/0.39 sQ0_spl|sQ1_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f8,f106,f109])).
% 0.12/0.39 fof(f113,definition,(
% 0.12/0.39 sQ2_spl <=> (furniture(sK3_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f116,plain,(
% 0.12/0.39 sQ0_spl|sQ2_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f9,f106,f113])).
% 0.12/0.39 fof(f117,definition,(
% 0.12/0.39 sQ3_spl <=> (front(sK3_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f120,plain,(
% 0.12/0.39 sQ0_spl|sQ3_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f10,f106,f117])).
% 0.12/0.39 fof(f121,definition,(
% 0.12/0.39 sQ4_spl <=> (seat(sK0_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f124,plain,(
% 0.12/0.39 sQ0_spl|sQ4_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f11,f106,f121])).
% 0.12/0.39 fof(f125,definition,(
% 0.12/0.39 sQ5_spl <=> (furniture(sK0_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f128,plain,(
% 0.12/0.39 sQ0_spl|sQ5_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f12,f106,f125])).
% 0.12/0.39 fof(f129,definition,(
% 0.12/0.39 sQ6_spl <=> (front(sK0_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f132,plain,(
% 0.12/0.39 sQ0_spl|sQ6_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f13,f106,f129])).
% 0.12/0.39 fof(f133,definition,(
% 0.12/0.39 sQ7_spl <=> (hollywood(sK6_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f136,plain,(
% 0.12/0.39 sQ0_spl|sQ7_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f14,f106,f133])).
% 0.12/0.39 fof(f137,definition,(
% 0.12/0.39 sQ8_spl <=> (city(sK6_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f140,plain,(
% 0.12/0.39 sQ0_spl|sQ8_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f15,f106,f137])).
% 0.12/0.39 fof(f141,definition,(
% 0.12/0.39 sQ9_spl <=> (event(sK7_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f144,plain,(
% 0.12/0.39 sQ0_spl|sQ9_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f16,f106,f141])).
% 0.12/0.39 fof(f145,definition,(
% 0.12/0.39 sQ10_spl <=> (chevy(sK9_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f148,plain,(
% 0.12/0.39 sQ0_spl|sQ10_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f17,f106,f145])).
% 0.12/0.39 fof(f149,definition,(
% 0.12/0.39 sQ11_spl <=> (car(sK9_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f152,plain,(
% 0.12/0.39 sQ0_spl|sQ11_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f18,f106,f149])).
% 0.12/0.39 fof(f153,definition,(
% 0.12/0.39 sQ12_spl <=> (white(sK9_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f156,plain,(
% 0.12/0.39 sQ0_spl|sQ12_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f19,f106,f153])).
% 0.12/0.39 fof(f157,definition,(
% 0.12/0.39 sQ13_spl <=> (dirty(sK9_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f160,plain,(
% 0.12/0.39 sQ0_spl|sQ13_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f20,f106,f157])).
% 0.12/0.39 fof(f161,definition,(
% 0.12/0.39 sQ14_spl <=> (old(sK9_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f164,plain,(
% 0.12/0.39 sQ0_spl|sQ14_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f21,f106,f161])).
% 0.12/0.39 fof(f165,definition,(
% 0.12/0.39 sQ15_spl <=> (street(sK8_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f168,plain,(
% 0.12/0.39 sQ0_spl|sQ15_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f22,f106,f165])).
% 0.12/0.39 fof(f169,definition,(
% 0.12/0.39 sQ16_spl <=> (way(sK8_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f172,plain,(
% 0.12/0.39 sQ0_spl|sQ16_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f23,f106,f169])).
% 0.12/0.39 fof(f173,definition,(
% 0.12/0.39 sQ17_spl <=> (lonely(sK8_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f176,plain,(
% 0.12/0.39 sQ0_spl|sQ17_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f24,f106,f173])).
% 0.12/0.39 fof(f177,definition,(
% 0.12/0.39 sQ18_spl <=> (barrel(sK7_skl,sK9_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f178,plain,(
% 0.12/0.39 barrel(sK7_skl,sK9_skl)|~sQ18_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f177])).
% 0.12/0.39 fof(f180,plain,(
% 0.12/0.39 sQ0_spl|sQ18_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f25,f106,f177])).
% 0.12/0.39 fof(f181,definition,(
% 0.12/0.39 sQ19_spl <=> (down(sK7_skl,sK8_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f182,plain,(
% 0.12/0.39 down(sK7_skl,sK8_skl)|~sQ19_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f181])).
% 0.12/0.39 fof(f184,plain,(
% 0.12/0.39 sQ0_spl|sQ19_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f26,f106,f181])).
% 0.12/0.39 fof(f185,definition,(
% 0.12/0.39 sQ20_spl <=> (in(sK7_skl,sK6_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f186,plain,(
% 0.12/0.39 in(sK7_skl,sK6_skl)|~sQ20_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f185])).
% 0.12/0.39 fof(f188,plain,(
% 0.12/0.39 sQ0_spl|sQ20_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f27,f106,f185])).
% 0.12/0.39 fof(f189,definition,(
% 0.12/0.39 sQ21_spl <=> (sK5_skl=sK2_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f192,plain,(
% 0.12/0.39 sQ0_spl|~sQ21_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f28,f106,f189])).
% 0.12/0.39 fof(f193,definition,(
% 0.12/0.39 sQ22_spl <=> (fellow(sK5_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f196,plain,(
% 0.12/0.39 sQ0_spl|sQ22_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f29,f106,f193])).
% 0.12/0.39 fof(f197,definition,(
% 0.12/0.39 sQ23_spl <=> (man(sK5_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f200,plain,(
% 0.12/0.39 sQ0_spl|sQ23_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f30,f106,f197])).
% 0.12/0.39 fof(f201,definition,(
% 0.12/0.39 sQ24_spl <=> (young(sK5_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f204,plain,(
% 0.12/0.39 sQ0_spl|sQ24_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f31,f106,f201])).
% 0.12/0.39 fof(f205,definition,(
% 0.12/0.39 sQ25_spl <=> (fellow(sK2_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f208,plain,(
% 0.12/0.39 sQ0_spl|sQ25_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f32,f106,f205])).
% 0.12/0.39 fof(f209,definition,(
% 0.12/0.39 sQ26_spl <=> (man(sK2_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f212,plain,(
% 0.12/0.39 sQ0_spl|sQ26_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f33,f106,f209])).
% 0.12/0.39 fof(f213,definition,(
% 0.12/0.39 sQ27_spl <=> (young(sK2_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f216,plain,(
% 0.12/0.39 sQ0_spl|sQ27_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f34,f106,f213])).
% 0.12/0.39 fof(f217,definition,(
% 0.12/0.39 sQ28_spl <=> (sK5_skl=sK4_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f218,plain,(
% 0.12/0.39 sK5_skl=sK4_skl|~sQ28_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f217])).
% 0.12/0.39 fof(f220,plain,(
% 0.12/0.39 sQ0_spl|sQ28_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f35,f106,f217])).
% 0.12/0.39 fof(f221,definition,(
% 0.12/0.39 sQ29_spl <=> (in(sK4_skl,sK3_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f222,plain,(
% 0.12/0.39 in(sK4_skl,sK3_skl)|~sQ29_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f221])).
% 0.12/0.39 fof(f224,plain,(
% 0.12/0.39 sQ0_spl|sQ29_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f36,f106,f221])).
% 0.12/0.39 fof(f225,definition,(
% 0.12/0.39 sQ30_spl <=> (sK2_skl=sK1_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f226,plain,(
% 0.12/0.39 sK2_skl=sK1_skl|~sQ30_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f225])).
% 0.12/0.39 fof(f228,plain,(
% 0.12/0.39 sQ0_spl|sQ30_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f37,f106,f225])).
% 0.12/0.39 fof(f229,definition,(
% 0.12/0.39 sQ31_spl <=> (in(sK1_skl,sK0_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f230,plain,(
% 0.12/0.39 in(sK1_skl,sK0_skl)|~sQ31_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f229])).
% 0.12/0.39 fof(f232,plain,(
% 0.12/0.39 sQ0_spl|sQ31_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f38,f106,f229])).
% 0.12/0.39 fof(f233,definition,(
% 0.12/0.39 ![X0,X1,X6,X7,X8,X9]: (sQ32_spl <=> (~seat(X0)|~furniture(X0)|~front(X0)|~seat(X1)|~furniture(X1)|~front(X1)|X6=X7|~fellow(X6)|~man(X6)|~young(X6)|~fellow(X7)|~man(X7)|~young(X7)|~X6=X8|~in(X8,X0)|~X7=X9|~in(X9,X1)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f234,plain,(
% 0.12/0.39 ![X0,X1,X2,X3,X4,X5]: (~seat(X0)|~furniture(X0)|~front(X0)|~seat(X1)|~furniture(X1)|~front(X1)|X2=X3|~fellow(X2)|~man(X2)|~young(X2)|~fellow(X3)|~man(X3)|~young(X3)|~X2=X4|~in(X4,X0)|~X3=X5|~in(X5,X1)|~sQ32_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f233])).
% 0.12/0.39 fof(f236,definition,(
% 0.12/0.39 ![X2,X3,X4,X5]: (sQ33_spl <=> (~hollywood(X2)|~city(X2)|~event(X3)|~street(X4)|~way(X4)|~lonely(X4)|~chevy(X5)|~car(X5)|~white(X5)|~dirty(X5)|~old(X5)|~barrel(X3,X5)|~down(X3,X4)|~in(X3,X2)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f237,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~hollywood(X0)|~city(X0)|~event(X1)|~street(X2)|~way(X2)|~lonely(X2)|~chevy(X3)|~car(X3)|~white(X3)|~dirty(X3)|~old(X3)|~barrel(X1,X3)|~down(X1,X2)|~in(X1,X0)|~sQ33_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f236])).
% 0.12/0.39 fof(f239,plain,(
% 0.12/0.39 sQ0_spl|sQ32_spl|sQ33_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f39,f106,f233,f236])).
% 0.12/0.39 fof(f240,definition,(
% 0.12/0.39 sQ34_spl <=> (seat(sK13_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f243,plain,(
% 0.12/0.39 ~sQ0_spl|sQ34_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f43,f106,f240])).
% 0.12/0.39 fof(f244,definition,(
% 0.12/0.39 sQ35_spl <=> (furniture(sK13_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f247,plain,(
% 0.12/0.39 ~sQ0_spl|sQ35_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f44,f106,f244])).
% 0.12/0.39 fof(f248,definition,(
% 0.12/0.39 sQ36_spl <=> (front(sK13_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f251,plain,(
% 0.12/0.39 ~sQ0_spl|sQ36_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f45,f106,f248])).
% 0.12/0.39 fof(f252,definition,(
% 0.12/0.39 sQ37_spl <=> (seat(sK10_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f255,plain,(
% 0.12/0.39 ~sQ0_spl|sQ37_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f46,f106,f252])).
% 0.12/0.39 fof(f256,definition,(
% 0.12/0.39 sQ38_spl <=> (furniture(sK10_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f259,plain,(
% 0.12/0.39 ~sQ0_spl|sQ38_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f47,f106,f256])).
% 0.12/0.39 fof(f260,definition,(
% 0.12/0.39 sQ39_spl <=> (front(sK10_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f263,plain,(
% 0.12/0.39 ~sQ0_spl|sQ39_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f48,f106,f260])).
% 0.12/0.39 fof(f264,definition,(
% 0.12/0.39 sQ40_spl <=> (hollywood(sK16_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f267,plain,(
% 0.12/0.39 ~sQ0_spl|sQ40_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f49,f106,f264])).
% 0.12/0.39 fof(f268,definition,(
% 0.12/0.39 sQ41_spl <=> (city(sK16_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f271,plain,(
% 0.12/0.39 ~sQ0_spl|sQ41_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f50,f106,f268])).
% 0.12/0.39 fof(f272,definition,(
% 0.12/0.39 sQ42_spl <=> (event(sK17_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f275,plain,(
% 0.12/0.39 ~sQ0_spl|sQ42_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f51,f106,f272])).
% 0.12/0.39 fof(f276,definition,(
% 0.12/0.39 sQ43_spl <=> (street(sK18_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f279,plain,(
% 0.12/0.39 ~sQ0_spl|sQ43_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f52,f106,f276])).
% 0.12/0.39 fof(f280,definition,(
% 0.12/0.39 sQ44_spl <=> (way(sK18_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f283,plain,(
% 0.12/0.39 ~sQ0_spl|sQ44_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f53,f106,f280])).
% 0.12/0.39 fof(f284,definition,(
% 0.12/0.39 sQ45_spl <=> (lonely(sK18_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f287,plain,(
% 0.12/0.39 ~sQ0_spl|sQ45_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f54,f106,f284])).
% 0.12/0.39 fof(f288,definition,(
% 0.12/0.39 sQ46_spl <=> (chevy(sK19_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f291,plain,(
% 0.12/0.39 ~sQ0_spl|sQ46_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f55,f106,f288])).
% 0.12/0.39 fof(f292,definition,(
% 0.12/0.39 sQ47_spl <=> (car(sK19_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f295,plain,(
% 0.12/0.39 ~sQ0_spl|sQ47_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f56,f106,f292])).
% 0.12/0.39 fof(f296,definition,(
% 0.12/0.39 sQ48_spl <=> (white(sK19_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f299,plain,(
% 0.12/0.39 ~sQ0_spl|sQ48_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f57,f106,f296])).
% 0.12/0.39 fof(f300,definition,(
% 0.12/0.39 sQ49_spl <=> (dirty(sK19_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f303,plain,(
% 0.12/0.39 ~sQ0_spl|sQ49_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f58,f106,f300])).
% 0.12/0.39 fof(f304,definition,(
% 0.12/0.39 sQ50_spl <=> (old(sK19_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f307,plain,(
% 0.12/0.39 ~sQ0_spl|sQ50_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f59,f106,f304])).
% 0.12/0.39 fof(f308,definition,(
% 0.12/0.39 sQ51_spl <=> (barrel(sK17_skl,sK19_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f309,plain,(
% 0.12/0.39 barrel(sK17_skl,sK19_skl)|~sQ51_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f308])).
% 0.12/0.39 fof(f311,plain,(
% 0.12/0.39 ~sQ0_spl|sQ51_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f60,f106,f308])).
% 0.12/0.39 fof(f312,definition,(
% 0.12/0.39 sQ52_spl <=> (down(sK17_skl,sK18_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f313,plain,(
% 0.12/0.39 down(sK17_skl,sK18_skl)|~sQ52_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f312])).
% 0.12/0.39 fof(f315,plain,(
% 0.12/0.39 ~sQ0_spl|sQ52_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f61,f106,f312])).
% 0.12/0.39 fof(f316,definition,(
% 0.12/0.39 sQ53_spl <=> (in(sK17_skl,sK16_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f317,plain,(
% 0.12/0.39 in(sK17_skl,sK16_skl)|~sQ53_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f316])).
% 0.12/0.39 fof(f319,plain,(
% 0.12/0.39 ~sQ0_spl|sQ53_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f62,f106,f316])).
% 0.12/0.39 fof(f320,definition,(
% 0.12/0.39 sQ54_spl <=> (sK15_skl=sK12_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f323,plain,(
% 0.12/0.39 ~sQ0_spl|~sQ54_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f63,f106,f320])).
% 0.12/0.39 fof(f324,definition,(
% 0.12/0.39 sQ55_spl <=> (fellow(sK15_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f327,plain,(
% 0.12/0.39 ~sQ0_spl|sQ55_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f64,f106,f324])).
% 0.12/0.39 fof(f328,definition,(
% 0.12/0.39 sQ56_spl <=> (man(sK15_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f331,plain,(
% 0.12/0.39 ~sQ0_spl|sQ56_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f65,f106,f328])).
% 0.12/0.39 fof(f332,definition,(
% 0.12/0.39 sQ57_spl <=> (young(sK15_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f335,plain,(
% 0.12/0.39 ~sQ0_spl|sQ57_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f66,f106,f332])).
% 0.12/0.39 fof(f336,definition,(
% 0.12/0.39 sQ58_spl <=> (fellow(sK12_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f339,plain,(
% 0.12/0.39 ~sQ0_spl|sQ58_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f67,f106,f336])).
% 0.12/0.39 fof(f340,definition,(
% 0.12/0.39 sQ59_spl <=> (man(sK12_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f343,plain,(
% 0.12/0.39 ~sQ0_spl|sQ59_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f68,f106,f340])).
% 0.12/0.39 fof(f344,definition,(
% 0.12/0.39 sQ60_spl <=> (young(sK12_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f347,plain,(
% 0.12/0.39 ~sQ0_spl|sQ60_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f69,f106,f344])).
% 0.12/0.39 fof(f348,definition,(
% 0.12/0.39 sQ61_spl <=> (sK15_skl=sK14_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f349,plain,(
% 0.12/0.39 sK15_skl=sK14_skl|~sQ61_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f348])).
% 0.12/0.39 fof(f351,plain,(
% 0.12/0.39 ~sQ0_spl|sQ61_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f70,f106,f348])).
% 0.12/0.39 fof(f352,definition,(
% 0.12/0.39 sQ62_spl <=> (in(sK14_skl,sK13_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f353,plain,(
% 0.12/0.39 in(sK14_skl,sK13_skl)|~sQ62_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f352])).
% 0.12/0.39 fof(f355,plain,(
% 0.12/0.39 ~sQ0_spl|sQ62_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f71,f106,f352])).
% 0.12/0.39 fof(f356,definition,(
% 0.12/0.39 sQ63_spl <=> (sK12_skl=sK11_skl)),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f357,plain,(
% 0.12/0.39 sK12_skl=sK11_skl|~sQ63_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f356])).
% 0.12/0.39 fof(f359,plain,(
% 0.12/0.39 ~sQ0_spl|sQ63_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f72,f106,f356])).
% 0.12/0.39 fof(f360,definition,(
% 0.12/0.39 sQ64_spl <=> (in(sK11_skl,sK10_skl))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f361,plain,(
% 0.12/0.39 in(sK11_skl,sK10_skl)|~sQ64_spl),
% 0.12/0.39 inference(component_clause,[status(thm)],[f360])).
% 0.12/0.39 fof(f363,plain,(
% 0.12/0.39 ~sQ0_spl|sQ64_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f73,f106,f360])).
% 0.12/0.39 fof(f364,plain,(
% 0.12/0.39 ~sQ0_spl|sQ32_spl|sQ33_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f74,f106,f233,f236])).
% 0.12/0.39 fof(f489,plain,(
% 0.12/0.39 in(sK12_skl,sK10_skl)|~sQ63_spl|~sQ64_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f357,f361])).
% 0.12/0.39 fof(f490,plain,(
% 0.12/0.39 in(sK15_skl,sK13_skl)|~sQ61_spl|~sQ62_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f349,f353])).
% 0.12/0.39 fof(f491,plain,(
% 0.12/0.39 in(sK2_skl,sK0_skl)|~sQ30_spl|~sQ31_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f226,f230])).
% 0.12/0.39 fof(f492,plain,(
% 0.12/0.39 in(sK5_skl,sK3_skl)|~sQ28_spl|~sQ29_spl),
% 0.12/0.39 inference(backward_demodulation,[status(thm)],[f218,f222])).
% 0.12/0.39 fof(f493,plain,(
% 0.12/0.39 ![X0,X1]: (~hollywood(X0)|~city(X0)|~event(sK17_skl)|~street(sK18_skl)|~way(sK18_skl)|~lonely(sK18_skl)|~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK17_skl,X1)|~in(sK17_skl,X0)|~sQ52_spl|~sQ33_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f313,f237])).
% 0.12/0.39 fof(f494,definition,(
% 0.12/0.39 ![X0]: (sQ96_spl <=> (~hollywood(X0)|~city(X0)|~in(sK17_skl,X0)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f495,plain,(
% 0.12/0.39 ![X0]: (~hollywood(X0)|~city(X0)|~in(sK17_skl,X0)|~sQ96_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f494])).
% 0.12/0.39 fof(f497,definition,(
% 0.12/0.39 ![X1]: (sQ97_spl <=> (~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK17_skl,X1)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f498,plain,(
% 0.12/0.39 ![X0]: (~chevy(X0)|~car(X0)|~white(X0)|~dirty(X0)|~old(X0)|~barrel(sK17_skl,X0)|~sQ97_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f497])).
% 0.12/0.39 fof(f500,plain,(
% 0.12/0.39 sQ96_spl|~sQ42_spl|~sQ43_spl|~sQ44_spl|~sQ45_spl|sQ97_spl|~sQ52_spl|~sQ33_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f493,f494,f272,f276,f280,f284,f497,f312,f236])).
% 0.12/0.39 fof(f501,plain,(
% 0.12/0.39 ![X0,X1,X2,X3]: (~seat(X0)|~furniture(X0)|~front(X0)|~seat(X1)|~furniture(X1)|~front(X1)|X2=X3|~fellow(X2)|~man(X2)|~young(X2)|~fellow(X3)|~man(X3)|~young(X3)|~in(X2,X0)|~in(X3,X1)|~sQ32_spl)),
% 0.12/0.39 inference(destructive_equality_resolution,[status(thm)],[f234])).
% 0.12/0.39 fof(f503,plain,(
% 0.12/0.39 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|~seat(sK0_skl)|~furniture(sK0_skl)|~front(sK0_skl)|X1=sK2_skl|~fellow(X1)|~man(X1)|~young(X1)|~fellow(sK2_skl)|~man(sK2_skl)|~young(sK2_skl)|~in(X1,X0)|~sQ32_spl|~sQ30_spl|~sQ31_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f501,f491])).
% 0.12/0.39 fof(f504,plain,(
% 0.12/0.39 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|~seat(sK13_skl)|~furniture(sK13_skl)|~front(sK13_skl)|X1=sK15_skl|~fellow(X1)|~man(X1)|~young(X1)|~fellow(sK15_skl)|~man(sK15_skl)|~young(sK15_skl)|~in(X1,X0)|~sQ32_spl|~sQ61_spl|~sQ62_spl)),
% 0.12/0.39 inference(resolution,[status(thm)],[f501,f490])).
% 0.12/0.39 fof(f512,definition,(
% 0.12/0.39 ![X0,X1]: (sQ99_spl <=> (~seat(X0)|~furniture(X0)|~front(X0)|X1=sK2_skl|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)))),
% 0.12/0.39 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.12/0.39 fof(f513,plain,(
% 0.12/0.39 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|X1=sK2_skl|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)|~sQ99_spl)),
% 0.12/0.39 inference(component_clause,[status(thm)],[f512])).
% 0.12/0.39 fof(f515,plain,(
% 0.12/0.39 sQ99_spl|~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ25_spl|~sQ26_spl|~sQ27_spl|~sQ32_spl|~sQ30_spl|~sQ31_spl),
% 0.12/0.39 inference(split_clause,[status(thm)],[f503,f512,f121,f125,f129,f205,f209,f213,f233,f225,f229])).
% 0.12/0.39 fof(f516,definition,(
% 0.12/0.39 ![X0,X1]: (sQ100_spl <=> (~seat(X0)|~furniture(X0)|~front(X0)|X1=sK15_skl|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f517,plain,(
% 0.12/0.40 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|X1=sK15_skl|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)|~sQ100_spl)),
% 0.12/0.40 inference(component_clause,[status(thm)],[f516])).
% 0.12/0.40 fof(f519,plain,(
% 0.12/0.40 sQ100_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ55_spl|~sQ56_spl|~sQ57_spl|~sQ32_spl|~sQ61_spl|~sQ62_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f504,f516,f240,f244,f248,f324,f328,f332,f233,f348,f352])).
% 0.12/0.40 fof(f568,plain,(
% 0.12/0.40 ![X0,X1]: (~hollywood(X0)|~city(X0)|~event(sK7_skl)|~street(sK8_skl)|~way(sK8_skl)|~lonely(sK8_skl)|~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK7_skl,X1)|~in(sK7_skl,X0)|~sQ33_spl|~sQ19_spl)),
% 0.12/0.40 inference(resolution,[status(thm)],[f237,f182])).
% 0.12/0.40 fof(f569,definition,(
% 0.12/0.40 ![X0]: (sQ116_spl <=> (~hollywood(X0)|~city(X0)|~in(sK7_skl,X0)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f570,plain,(
% 0.12/0.40 ![X0]: (~hollywood(X0)|~city(X0)|~in(sK7_skl,X0)|~sQ116_spl)),
% 0.12/0.40 inference(component_clause,[status(thm)],[f569])).
% 0.12/0.40 fof(f572,definition,(
% 0.12/0.40 ![X1]: (sQ117_spl <=> (~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK7_skl,X1)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f573,plain,(
% 0.12/0.40 ![X0]: (~chevy(X0)|~car(X0)|~white(X0)|~dirty(X0)|~old(X0)|~barrel(sK7_skl,X0)|~sQ117_spl)),
% 0.12/0.40 inference(component_clause,[status(thm)],[f572])).
% 0.12/0.40 fof(f575,plain,(
% 0.12/0.40 sQ116_spl|~sQ9_spl|~sQ15_spl|~sQ16_spl|~sQ17_spl|sQ117_spl|~sQ33_spl|~sQ19_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f568,f569,f141,f165,f169,f173,f572,f236,f181])).
% 0.12/0.40 fof(f580,plain,(
% 0.12/0.40 ~hollywood(sK16_skl)|~city(sK16_skl)|~sQ96_spl|~sQ53_spl),
% 0.12/0.40 inference(resolution,[status(thm)],[f495,f317])).
% 0.12/0.40 fof(f581,plain,(
% 0.12/0.40 ~sQ40_spl|~sQ41_spl|~sQ96_spl|~sQ53_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f580,f264,f268,f494,f316])).
% 0.12/0.40 fof(f582,plain,(
% 0.12/0.40 ~chevy(sK19_skl)|~car(sK19_skl)|~white(sK19_skl)|~dirty(sK19_skl)|~old(sK19_skl)|~sQ97_spl|~sQ51_spl),
% 0.12/0.40 inference(resolution,[status(thm)],[f498,f309])).
% 0.12/0.40 fof(f583,plain,(
% 0.12/0.40 ~sQ46_spl|~sQ47_spl|~sQ48_spl|~sQ49_spl|~sQ50_spl|~sQ97_spl|~sQ51_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f582,f288,f292,f296,f300,f304,f497,f308])).
% 0.12/0.40 fof(f584,plain,(
% 0.12/0.40 ~chevy(sK9_skl)|~car(sK9_skl)|~white(sK9_skl)|~dirty(sK9_skl)|~old(sK9_skl)|~sQ18_spl|~sQ117_spl),
% 0.12/0.40 inference(resolution,[status(thm)],[f178,f573])).
% 0.12/0.40 fof(f585,plain,(
% 0.12/0.40 ~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ18_spl|~sQ117_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f584,f145,f149,f153,f157,f161,f177,f572])).
% 0.12/0.40 fof(f592,plain,(
% 0.12/0.40 ~seat(sK10_skl)|~furniture(sK10_skl)|~front(sK10_skl)|sK12_skl=sK15_skl|~fellow(sK12_skl)|~man(sK12_skl)|~young(sK12_skl)|~sQ100_spl|~sQ63_spl|~sQ64_spl),
% 0.12/0.40 inference(resolution,[status(thm)],[f517,f489])).
% 0.12/0.40 fof(f595,plain,(
% 0.12/0.40 ~sQ37_spl|~sQ38_spl|~sQ39_spl|sQ54_spl|~sQ58_spl|~sQ59_spl|~sQ60_spl|~sQ100_spl|~sQ63_spl|~sQ64_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f592,f252,f256,f260,f320,f336,f340,f344,f516,f356,f360])).
% 0.12/0.40 fof(f656,plain,(
% 0.12/0.40 ~hollywood(sK6_skl)|~city(sK6_skl)|~sQ116_spl|~sQ20_spl),
% 0.12/0.40 inference(resolution,[status(thm)],[f570,f186])).
% 0.12/0.40 fof(f657,plain,(
% 0.12/0.40 ~sQ7_spl|~sQ8_spl|~sQ116_spl|~sQ20_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f656,f133,f137,f569,f185])).
% 0.12/0.40 fof(f660,plain,(
% 0.12/0.40 ~seat(sK3_skl)|~furniture(sK3_skl)|~front(sK3_skl)|sK5_skl=sK2_skl|~fellow(sK5_skl)|~man(sK5_skl)|~young(sK5_skl)|~sQ99_spl|~sQ28_spl|~sQ29_spl),
% 0.12/0.40 inference(resolution,[status(thm)],[f513,f492])).
% 0.12/0.40 fof(f669,plain,(
% 0.12/0.40 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ21_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl|~sQ99_spl|~sQ28_spl|~sQ29_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f660,f109,f113,f117,f189,f193,f197,f201,f512,f217,f221])).
% 0.12/0.40 fof(f670,plain,(
% 0.12/0.40 $false),
% 0.12/0.40 inference(sat_refutation,[status(thm)],[f112,f116,f120,f124,f128,f132,f136,f140,f144,f148,f152,f156,f160,f164,f168,f172,f176,f180,f184,f188,f192,f196,f200,f204,f208,f212,f216,f220,f224,f228,f232,f239,f243,f247,f251,f255,f259,f263,f267,f271,f275,f279,f283,f287,f291,f295,f299,f303,f307,f311,f315,f319,f323,f327,f331,f335,f339,f343,f347,f351,f355,f359,f363,f364,f500,f515,f519,f575,f581,f583,f585,f595,f657,f669])).
% 0.12/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.42 % Elapsed time: 0.054625 seconds
% 0.12/0.42 % CPU time: 0.180183 seconds
% 0.12/0.42 % Total memory used: 88.543 MB
% 0.12/0.42 % Net memory used: 88.387 MB
%------------------------------------------------------------------------------