%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP009+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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:45 PM UTC 2026
% Result : Theorem 0.19s 0.49s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : NLP009+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.44 % Computer : n004.cluster.edu
% 0.19/0.44 % Model : x86_64 x86_64
% 0.19/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.44 % Memory : 8046.5625MB
% 0.19/0.44 % OS : Linux 6.8.0-71-generic
% 0.19/0.44 % CPULimit : 300
% 0.19/0.44 % WCLimit : 300
% 0.19/0.44 % DateTime : Mon Sep 21 01:31:19 UTC 2026
% 0.19/0.44 % CPUTime :
% 0.19/0.46 % Drodi V4.1.1
% 0.19/0.49 % Refutation found
% 0.19/0.49 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.19/0.49 % SZS output start CNFRefutation for theBenchmark
% 0.19/0.49 fof(f1,conjecture,(
% 0.19/0.49 ( ( (? [U,V,W,X,Y,Z,X1,X2,X3] :( hollywood(U)& city(U)& event(V)& street(W)& way(W)& lonely(W)& chevy(X)& car(X)& white(X)& dirty(X)& old(X)& barrel(V,X)& down(V,W)& in(V,U)& seat(X1)& furniture(X1)& front(X1)& Y != Z& fellow(Y)& man(Y)& young(Y)& fellow(Z)& man(Z)& young(Z)& Y = X2& in(X2,X1)& Z = X3& in(X3,X1) ))=> (? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :( hollywood(X4)& city(X4)& event(X5)& chevy(X6)& car(X6)& white(X6)& dirty(X6)& old(X6)& street(X7)& way(X7)& lonely(X7)& barrel(X5,X6)& down(X5,X7)& in(X5,X4)& seat(X10)& furniture(X10)& front(X10)& X8 != X9& fellow(X8)& man(X8)& young(X8)& fellow(X9)& man(X9)& young(X9)& X8 = X11& in(X11,X10)& X9 = X12& in(X12,X10) ) ))& ( (? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :( hollywood(X13)& city(X13)& event(X14)& chevy(X15)& car(X15)& white(X15)& dirty(X15)& old(X15)& street(X16)& way(X16)& lonely(X16)& barrel(X14,X15)& down(X14,X16)& in(X14,X13)& seat(X19)& furniture(X19)& front(X19)& X17 != X18& fellow(X17)& man(X17)& young(X17)& fellow(X18)& man(X18)& young(X18)& X17 = X20& in(X20,X19)& X18 = X21& in(X21,X19) ))=> (? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :( hollywood(X22)& city(X22)& event(X23)& street(X24)& way(X24)& lonely(X24)& chevy(X25)& car(X25)& white(X25)& dirty(X25)& old(X25)& barrel(X23,X25)& down(X23,X24)& in(X23,X22)& seat(X28)& furniture(X28)& front(X28)& X26 != X27& fellow(X26)& man(X26)& young(X26)& fellow(X27)& man(X27)& young(X27)& X26 = X29& in(X29,X28)& X27 = X30& in(X30,X28) ) )) ) ),
% 0.19/0.49 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.19/0.49 fof(f2,negated_conjecture,(
% 0.19/0.49 ~(( ( (? [U,V,W,X,Y,Z,X1,X2,X3] :( hollywood(U)& city(U)& event(V)& street(W)& way(W)& lonely(W)& chevy(X)& car(X)& white(X)& dirty(X)& old(X)& barrel(V,X)& down(V,W)& in(V,U)& seat(X1)& furniture(X1)& front(X1)& Y != Z& fellow(Y)& man(Y)& young(Y)& fellow(Z)& man(Z)& young(Z)& Y = X2& in(X2,X1)& Z = X3& in(X3,X1) ))=> (? [X4,X5,X6,X7,X8,X9,X10,X11,X12] :( hollywood(X4)& city(X4)& event(X5)& chevy(X6)& car(X6)& white(X6)& dirty(X6)& old(X6)& street(X7)& way(X7)& lonely(X7)& barrel(X5,X6)& down(X5,X7)& in(X5,X4)& seat(X10)& furniture(X10)& front(X10)& X8 != X9& fellow(X8)& man(X8)& young(X8)& fellow(X9)& man(X9)& young(X9)& X8 = X11& in(X11,X10)& X9 = X12& in(X12,X10) ) ))& ( (? [X13,X14,X15,X16,X17,X18,X19,X20,X21] :( hollywood(X13)& city(X13)& event(X14)& chevy(X15)& car(X15)& white(X15)& dirty(X15)& old(X15)& street(X16)& way(X16)& lonely(X16)& barrel(X14,X15)& down(X14,X16)& in(X14,X13)& seat(X19)& furniture(X19)& front(X19)& X17 != X18& fellow(X17)& man(X17)& young(X17)& fellow(X18)& man(X18)& young(X18)& X17 = X20& in(X20,X19)& X18 = X21& in(X21,X19) ))=> (? [X22,X23,X24,X25,X26,X27,X28,X29,X30] :( hollywood(X22)& city(X22)& event(X23)& street(X24)& way(X24)& lonely(X24)& chevy(X25)& car(X25)& white(X25)& dirty(X25)& old(X25)& barrel(X23,X25)& down(X23,X24)& in(X23,X22)& seat(X28)& furniture(X28)& front(X28)& X26 != X27& fellow(X26)& man(X26)& young(X26)& fellow(X27)& man(X27)& young(X27)& X26 = X29& in(X29,X28)& X27 = X30& in(X30,X28) ) )) ) )),
% 0.19/0.49 inference(negated_conjecture,[status(cth)],[f1])).
% 0.19/0.49 fof(f3,plain,(
% 0.19/0.49 (((?[U,V,W,X,Y,Z,X1,X2,X3]: (((((((((((((((((((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X))&down(V,W))&in(V,U))&seat(X1))&furniture(X1))&front(X1))&~Y=Z)&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1)))&(![X4,X5,X6,X7,X8,X9,X10,X11,X12]: (((((((((((((((((((((((((((~hollywood(X4)|~city(X4))|~event(X5))|~chevy(X6))|~car(X6))|~white(X6))|~dirty(X6))|~old(X6))|~street(X7))|~way(X7))|~lonely(X7))|~barrel(X5,X6))|~down(X5,X7))|~in(X5,X4))|~seat(X10))|~furniture(X10))|~front(X10))|X8=X9)|~fellow(X8))|~man(X8))|~young(X8))|~fellow(X9))|~man(X9))|~young(X9))|~X8=X11)|~in(X11,X10))|~X9=X12)|~in(X12,X10))))|((?[X13,X14,X15,X16,X17,X18,X19,X20,X21]: (((((((((((((((((((((((((((hollywood(X13)&city(X13))&event(X14))&chevy(X15))&car(X15))&white(X15))&dirty(X15))&old(X15))&street(X16))&way(X16))&lonely(X16))&barrel(X14,X15))&down(X14,X16))&in(X14,X13))&seat(X19))&furniture(X19))&front(X19))&~X17=X18)&fellow(X17))&man(X17))&young(X17))&fellow(X18))&man(X18))&young(X18))&X17=X20)&in(X20,X19))&X18=X21)&in(X21,X19)))&(![X22,X23,X24,X25,X26,X27,X28,X29,X30]: (((((((((((((((((((((((((((~hollywood(X22)|~city(X22))|~event(X23))|~street(X24))|~way(X24))|~lonely(X24))|~chevy(X25))|~car(X25))|~white(X25))|~dirty(X25))|~old(X25))|~barrel(X23,X25))|~down(X23,X24))|~in(X23,X22))|~seat(X28))|~furniture(X28))|~front(X28))|X26=X27)|~fellow(X26))|~man(X26))|~young(X26))|~fellow(X27))|~man(X27))|~young(X27))|~X26=X29)|~in(X29,X28))|~X27=X30)|~in(X30,X28)))))),
% 0.19/0.49 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.19/0.49 fof(f4,definition,(
% 0.19/0.49 sP0_prd<=>((?[U,V,W,X,Y,Z,X1,X2,X3]: (((((((((((((((((((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X))&down(V,W))&in(V,U))&seat(X1))&furniture(X1))&front(X1))&~Y=Z)&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1)))&(![X4,X5,X6,X7,X8,X9,X10,X11,X12]: (((((((((((((((((((((((((((~hollywood(X4)|~city(X4))|~event(X5))|~chevy(X6))|~car(X6))|~white(X6))|~dirty(X6))|~old(X6))|~street(X7))|~way(X7))|~lonely(X7))|~barrel(X5,X6))|~down(X5,X7))|~in(X5,X4))|~seat(X10))|~furniture(X10))|~front(X10))|X8=X9)|~fellow(X8))|~man(X8))|~young(X8))|~fellow(X9))|~man(X9))|~young(X9))|~X8=X11)|~in(X11,X10))|~X9=X12)|~in(X12,X10))))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.19/0.49 fof(f5,plain,(
% 0.19/0.49 sP0_prd|((?[X13,X14,X15,X16,X17,X18,X19,X20,X21]: (((((((((((((((((((((((((((hollywood(X13)&city(X13))&event(X14))&chevy(X15))&car(X15))&white(X15))&dirty(X15))&old(X15))&street(X16))&way(X16))&lonely(X16))&barrel(X14,X15))&down(X14,X16))&in(X14,X13))&seat(X19))&furniture(X19))&front(X19))&~X17=X18)&fellow(X17))&man(X17))&young(X17))&fellow(X18))&man(X18))&young(X18))&X17=X20)&in(X20,X19))&X18=X21)&in(X21,X19)))&(![X22,X23,X24,X25,X26,X27,X28,X29,X30]: (((((((((((((((((((((((((((~hollywood(X22)|~city(X22))|~event(X23))|~street(X24))|~way(X24))|~lonely(X24))|~chevy(X25))|~car(X25))|~white(X25))|~dirty(X25))|~old(X25))|~barrel(X23,X25))|~down(X23,X24))|~in(X23,X22))|~seat(X28))|~furniture(X28))|~front(X28))|X26=X27)|~fellow(X26))|~man(X26))|~young(X26))|~fellow(X27))|~man(X27))|~young(X27))|~X26=X29)|~in(X29,X28))|~X27=X30)|~in(X30,X28))))),
% 0.19/0.49 inference(formula_renaming,[status(thm)],[f3,f4])).
% 0.19/0.49 fof(f6,plain,(
% 0.19/0.49 sP0_prd|((?[X19,X21]: ((?[X18]: ((?[X20]: ((?[X17]: ((((((((((((?[X13,X14]: ((?[X16]: ((?[X15]: (((((((((((hollywood(X13)&city(X13))&event(X14))&chevy(X15))&car(X15))&white(X15))&dirty(X15))&old(X15))&street(X16))&way(X16))&lonely(X16))&barrel(X14,X15)))&down(X14,X16)))&in(X14,X13)))&seat(X19))&furniture(X19))&front(X19))&~X17=X18)&fellow(X17))&man(X17))&young(X17))&fellow(X18))&man(X18))&young(X18))&X17=X20))&in(X20,X19)))&X18=X21))&in(X21,X19)))&(![X28,X30]: ((![X27]: ((![X29]: ((![X26]: ((((((((((((![X22,X23]: ((![X24]: ((![X25]: (((((((((((~hollywood(X22)|~city(X22))|~event(X23))|~street(X24))|~way(X24))|~lonely(X24))|~chevy(X25))|~car(X25))|~white(X25))|~dirty(X25))|~old(X25))|~barrel(X23,X25)))|~down(X23,X24)))|~in(X23,X22)))|~seat(X28))|~furniture(X28))|~front(X28))|X26=X27)|~fellow(X26))|~man(X26))|~young(X26))|~fellow(X27))|~man(X27))|~young(X27))|~X26=X29))|~in(X29,X28)))|~X27=X30))|~in(X30,X28))))),
% 0.19/0.49 inference(miniscoping,[status(thm)],[f5])).
% 0.19/0.49 fof(f7,plain,(
% 0.19/0.49 sP0_prd|((((((((((((((((((((((((((((hollywood(sK5_skl)&city(sK5_skl))&event(sK6_skl))&chevy(sK8_skl))&car(sK8_skl))&white(sK8_skl))&dirty(sK8_skl))&old(sK8_skl))&street(sK7_skl))&way(sK7_skl))&lonely(sK7_skl))&barrel(sK6_skl,sK8_skl))&down(sK6_skl,sK7_skl))&in(sK6_skl,sK5_skl))&seat(sK0_skl))&furniture(sK0_skl))&front(sK0_skl))&~sK4_skl=sK2_skl)&fellow(sK4_skl))&man(sK4_skl))&young(sK4_skl))&fellow(sK2_skl))&man(sK2_skl))&young(sK2_skl))&sK4_skl=sK3_skl)&in(sK3_skl,sK0_skl))&sK2_skl=sK1_skl)&in(sK1_skl,sK0_skl))&(![X28,X30]: ((![X27]: ((![X29]: ((![X26]: ((((((((((((![X22,X23]: ((![X24]: ((![X25]: (((((((((((~hollywood(X22)|~city(X22))|~event(X23))|~street(X24))|~way(X24))|~lonely(X24))|~chevy(X25))|~car(X25))|~white(X25))|~dirty(X25))|~old(X25))|~barrel(X23,X25)))|~down(X23,X24)))|~in(X23,X22)))|~seat(X28))|~furniture(X28))|~front(X28))|X26=X27)|~fellow(X26))|~man(X26))|~young(X26))|~fellow(X27))|~man(X27))|~young(X27))|~X26=X29))|~in(X29,X28)))|~X27=X30))|~in(X30,X28))))),
% 0.19/0.49 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]),skolemize(X19,sK0_skl),skolemize(X21,sK1_skl),skolemize(X18,sK2_skl),skolemize(X20,sK3_skl),skolemize(X17,sK4_skl),skolemize(X13,sK5_skl),skolemize(X14,sK6_skl),skolemize(X16,sK7_skl),skolemize(X15,sK8_skl)],[f6])).
% 0.19/0.49 fof(f8,plain,(
% 0.19/0.49 sP0_prd|hollywood(sK5_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f9,plain,(
% 0.19/0.49 sP0_prd|city(sK5_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f10,plain,(
% 0.19/0.49 sP0_prd|event(sK6_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f11,plain,(
% 0.19/0.49 sP0_prd|chevy(sK8_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f12,plain,(
% 0.19/0.49 sP0_prd|car(sK8_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f13,plain,(
% 0.19/0.49 sP0_prd|white(sK8_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f14,plain,(
% 0.19/0.49 sP0_prd|dirty(sK8_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f15,plain,(
% 0.19/0.49 sP0_prd|old(sK8_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f16,plain,(
% 0.19/0.49 sP0_prd|street(sK7_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f17,plain,(
% 0.19/0.49 sP0_prd|way(sK7_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f18,plain,(
% 0.19/0.49 sP0_prd|lonely(sK7_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f19,plain,(
% 0.19/0.49 sP0_prd|barrel(sK6_skl,sK8_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f20,plain,(
% 0.19/0.49 sP0_prd|down(sK6_skl,sK7_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f21,plain,(
% 0.19/0.49 sP0_prd|in(sK6_skl,sK5_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f22,plain,(
% 0.19/0.49 sP0_prd|seat(sK0_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f23,plain,(
% 0.19/0.49 sP0_prd|furniture(sK0_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f24,plain,(
% 0.19/0.49 sP0_prd|front(sK0_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f25,plain,(
% 0.19/0.49 sP0_prd|~sK4_skl=sK2_skl),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f26,plain,(
% 0.19/0.49 sP0_prd|fellow(sK4_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f27,plain,(
% 0.19/0.49 sP0_prd|man(sK4_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f28,plain,(
% 0.19/0.49 sP0_prd|young(sK4_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f29,plain,(
% 0.19/0.49 sP0_prd|fellow(sK2_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f30,plain,(
% 0.19/0.49 sP0_prd|man(sK2_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f31,plain,(
% 0.19/0.49 sP0_prd|young(sK2_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f32,plain,(
% 0.19/0.49 sP0_prd|sK4_skl=sK3_skl),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f33,plain,(
% 0.19/0.49 sP0_prd|in(sK3_skl,sK0_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f34,plain,(
% 0.19/0.49 sP0_prd|sK2_skl=sK1_skl),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f35,plain,(
% 0.19/0.49 sP0_prd|in(sK1_skl,sK0_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f36,plain,(
% 0.19/0.49 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (sP0_prd|~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)|~seat(X4)|~furniture(X4)|~front(X4)|X5=X6|~fellow(X5)|~man(X5)|~young(X5)|~fellow(X6)|~man(X6)|~young(X6)|~X5=X7|~in(X7,X4)|~X6=X8|~in(X8,X4))),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f7])).
% 0.19/0.49 fof(f37,plain,(
% 0.19/0.49 (~sP0_prd|((?[U,V,W,X,Y,Z,X1,X2,X3]: (((((((((((((((((((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X))&down(V,W))&in(V,U))&seat(X1))&furniture(X1))&front(X1))&~Y=Z)&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2)&in(X2,X1))&Z=X3)&in(X3,X1)))&(![X4,X5,X6,X7,X8,X9,X10,X11,X12]: (((((((((((((((((((((((((((~hollywood(X4)|~city(X4))|~event(X5))|~chevy(X6))|~car(X6))|~white(X6))|~dirty(X6))|~old(X6))|~street(X7))|~way(X7))|~lonely(X7))|~barrel(X5,X6))|~down(X5,X7))|~in(X5,X4))|~seat(X10))|~furniture(X10))|~front(X10))|X8=X9)|~fellow(X8))|~man(X8))|~young(X8))|~fellow(X9))|~man(X9))|~young(X9))|~X8=X11)|~in(X11,X10))|~X9=X12)|~in(X12,X10)))))&(sP0_prd|((![U,V,W,X,Y,Z,X1,X2,X3]: (((((((((((((((((((((((((((~hollywood(U)|~city(U))|~event(V))|~street(W))|~way(W))|~lonely(W))|~chevy(X))|~car(X))|~white(X))|~dirty(X))|~old(X))|~barrel(V,X))|~down(V,W))|~in(V,U))|~seat(X1))|~furniture(X1))|~front(X1))|Y=Z)|~fellow(Y))|~man(Y))|~young(Y))|~fellow(Z))|~man(Z))|~young(Z))|~Y=X2)|~in(X2,X1))|~Z=X3)|~in(X3,X1)))|(?[X4,X5,X6,X7,X8,X9,X10,X11,X12]: (((((((((((((((((((((((((((hollywood(X4)&city(X4))&event(X5))&chevy(X6))&car(X6))&white(X6))&dirty(X6))&old(X6))&street(X7))&way(X7))&lonely(X7))&barrel(X5,X6))&down(X5,X7))&in(X5,X4))&seat(X10))&furniture(X10))&front(X10))&~X8=X9)&fellow(X8))&man(X8))&young(X8))&fellow(X9))&man(X9))&young(X9))&X8=X11)&in(X11,X10))&X9=X12)&in(X12,X10)))))),
% 0.19/0.49 inference(NNF_transformation,[status(thm)],[f4])).
% 0.19/0.49 fof(f38,plain,(
% 0.19/0.49 (~sP0_prd|((?[X1,X3]: ((?[Z]: ((?[X2]: ((?[Y]: ((((((((((((?[U,V]: ((?[W]: ((?[X]: (((((((((((hollywood(U)&city(U))&event(V))&street(W))&way(W))&lonely(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&barrel(V,X)))&down(V,W)))&in(V,U)))&seat(X1))&furniture(X1))&front(X1))&~Y=Z)&fellow(Y))&man(Y))&young(Y))&fellow(Z))&man(Z))&young(Z))&Y=X2))&in(X2,X1)))&Z=X3))&in(X3,X1)))&(![X10,X12]: ((![X9]: ((![X11]: ((![X8]: ((((((((((((![X4,X5]: ((![X7]: ((![X6]: (((((((((((~hollywood(X4)|~city(X4))|~event(X5))|~chevy(X6))|~car(X6))|~white(X6))|~dirty(X6))|~old(X6))|~street(X7))|~way(X7))|~lonely(X7))|~barrel(X5,X6)))|~down(X5,X7)))|~in(X5,X4)))|~seat(X10))|~furniture(X10))|~front(X10))|X8=X9)|~fellow(X8))|~man(X8))|~young(X8))|~fellow(X9))|~man(X9))|~young(X9))|~X8=X11))|~in(X11,X10)))|~X9=X12))|~in(X12,X10)))))&(sP0_prd|((![X1,X3]: ((![Z]: ((![X2]: ((![Y]: ((((((((((((![U,V]: ((![W]: ((![X]: (((((((((((~hollywood(U)|~city(U))|~event(V))|~street(W))|~way(W))|~lonely(W))|~chevy(X))|~car(X))|~white(X))|~dirty(X))|~old(X))|~barrel(V,X)))|~down(V,W)))|~in(V,U)))|~seat(X1))|~furniture(X1))|~front(X1))|Y=Z)|~fellow(Y))|~man(Y))|~young(Y))|~fellow(Z))|~man(Z))|~young(Z))|~Y=X2))|~in(X2,X1)))|~Z=X3))|~in(X3,X1)))|(?[X10,X12]: ((?[X9]: ((?[X11]: ((?[X8]: ((((((((((((?[X4,X5]: ((?[X7]: ((?[X6]: (((((((((((hollywood(X4)&city(X4))&event(X5))&chevy(X6))&car(X6))&white(X6))&dirty(X6))&old(X6))&street(X7))&way(X7))&lonely(X7))&barrel(X5,X6)))&down(X5,X7)))&in(X5,X4)))&seat(X10))&furniture(X10))&front(X10))&~X8=X9)&fellow(X8))&man(X8))&young(X8))&fellow(X9))&man(X9))&young(X9))&X8=X11))&in(X11,X10)))&X9=X12))&in(X12,X10)))))),
% 0.19/0.49 inference(miniscoping,[status(thm)],[f37])).
% 0.19/0.49 fof(f39,plain,(
% 0.19/0.49 (~sP0_prd|((((((((((((((((((((((((((((hollywood(sK14_skl)&city(sK14_skl))&event(sK15_skl))&street(sK16_skl))&way(sK16_skl))&lonely(sK16_skl))&chevy(sK17_skl))&car(sK17_skl))&white(sK17_skl))&dirty(sK17_skl))&old(sK17_skl))&barrel(sK15_skl,sK17_skl))&down(sK15_skl,sK16_skl))&in(sK15_skl,sK14_skl))&seat(sK9_skl))&furniture(sK9_skl))&front(sK9_skl))&~sK13_skl=sK11_skl)&fellow(sK13_skl))&man(sK13_skl))&young(sK13_skl))&fellow(sK11_skl))&man(sK11_skl))&young(sK11_skl))&sK13_skl=sK12_skl)&in(sK12_skl,sK9_skl))&sK11_skl=sK10_skl)&in(sK10_skl,sK9_skl))&(![X10,X12]: ((![X9]: ((![X11]: ((![X8]: ((((((((((((![X4,X5]: ((![X7]: ((![X6]: (((((((((((~hollywood(X4)|~city(X4))|~event(X5))|~chevy(X6))|~car(X6))|~white(X6))|~dirty(X6))|~old(X6))|~street(X7))|~way(X7))|~lonely(X7))|~barrel(X5,X6)))|~down(X5,X7)))|~in(X5,X4)))|~seat(X10))|~furniture(X10))|~front(X10))|X8=X9)|~fellow(X8))|~man(X8))|~young(X8))|~fellow(X9))|~man(X9))|~young(X9))|~X8=X11))|~in(X11,X10)))|~X9=X12))|~in(X12,X10)))))&(sP0_prd|((![X1,X3]: ((![Z]: ((![X2]: ((![Y]: ((((((((((((![U,V]: ((![W]: ((![X]: (((((((((((~hollywood(U)|~city(U))|~event(V))|~street(W))|~way(W))|~lonely(W))|~chevy(X))|~car(X))|~white(X))|~dirty(X))|~old(X))|~barrel(V,X)))|~down(V,W)))|~in(V,U)))|~seat(X1))|~furniture(X1))|~front(X1))|Y=Z)|~fellow(Y))|~man(Y))|~young(Y))|~fellow(Z))|~man(Z))|~young(Z))|~Y=X2))|~in(X2,X1)))|~Z=X3))|~in(X3,X1)))|(((((((((((((((((((((((((((hollywood(sK23_skl)&city(sK23_skl))&event(sK24_skl))&chevy(sK26_skl))&car(sK26_skl))&white(sK26_skl))&dirty(sK26_skl))&old(sK26_skl))&street(sK25_skl))&way(sK25_skl))&lonely(sK25_skl))&barrel(sK24_skl,sK26_skl))&down(sK24_skl,sK25_skl))&in(sK24_skl,sK23_skl))&seat(sK18_skl))&furniture(sK18_skl))&front(sK18_skl))&~sK22_skl=sK20_skl)&fellow(sK22_skl))&man(sK22_skl))&young(sK22_skl))&fellow(sK20_skl))&man(sK20_skl))&young(sK20_skl))&sK22_skl=sK21_skl)&in(sK21_skl,sK18_skl))&sK20_skl=sK19_skl)&in(sK19_skl,sK18_skl))))),
% 0.19/0.49 inference(skolemize,[status(esa),new_symbols(skolem,[sK9_skl,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]),skolemize(X1,sK9_skl),skolemize(X3,sK10_skl),skolemize(Z,sK11_skl),skolemize(X2,sK12_skl),skolemize(Y,sK13_skl),skolemize(U,sK14_skl),skolemize(V,sK15_skl),skolemize(W,sK16_skl),skolemize(X,sK17_skl),skolemize(X10,sK18_skl),skolemize(X12,sK19_skl),skolemize(X9,sK20_skl),skolemize(X11,sK21_skl),skolemize(X8,sK22_skl),skolemize(X4,sK23_skl),skolemize(X5,sK24_skl),skolemize(X7,sK25_skl),skolemize(X6,sK26_skl)],[f38])).
% 0.19/0.49 fof(f40,plain,(
% 0.19/0.49 ~sP0_prd|hollywood(sK14_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f41,plain,(
% 0.19/0.49 ~sP0_prd|city(sK14_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f42,plain,(
% 0.19/0.49 ~sP0_prd|event(sK15_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f43,plain,(
% 0.19/0.49 ~sP0_prd|street(sK16_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f44,plain,(
% 0.19/0.49 ~sP0_prd|way(sK16_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f45,plain,(
% 0.19/0.49 ~sP0_prd|lonely(sK16_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f46,plain,(
% 0.19/0.49 ~sP0_prd|chevy(sK17_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f47,plain,(
% 0.19/0.49 ~sP0_prd|car(sK17_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f48,plain,(
% 0.19/0.49 ~sP0_prd|white(sK17_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f49,plain,(
% 0.19/0.49 ~sP0_prd|dirty(sK17_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f50,plain,(
% 0.19/0.49 ~sP0_prd|old(sK17_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f51,plain,(
% 0.19/0.49 ~sP0_prd|barrel(sK15_skl,sK17_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f52,plain,(
% 0.19/0.49 ~sP0_prd|down(sK15_skl,sK16_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f53,plain,(
% 0.19/0.49 ~sP0_prd|in(sK15_skl,sK14_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f54,plain,(
% 0.19/0.49 ~sP0_prd|seat(sK9_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f55,plain,(
% 0.19/0.49 ~sP0_prd|furniture(sK9_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f56,plain,(
% 0.19/0.49 ~sP0_prd|front(sK9_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f57,plain,(
% 0.19/0.49 ~sP0_prd|~sK13_skl=sK11_skl),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f58,plain,(
% 0.19/0.49 ~sP0_prd|fellow(sK13_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f59,plain,(
% 0.19/0.49 ~sP0_prd|man(sK13_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f60,plain,(
% 0.19/0.49 ~sP0_prd|young(sK13_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f61,plain,(
% 0.19/0.49 ~sP0_prd|fellow(sK11_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f62,plain,(
% 0.19/0.49 ~sP0_prd|man(sK11_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f63,plain,(
% 0.19/0.49 ~sP0_prd|young(sK11_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f64,plain,(
% 0.19/0.49 ~sP0_prd|sK13_skl=sK12_skl),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f65,plain,(
% 0.19/0.49 ~sP0_prd|in(sK12_skl,sK9_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f66,plain,(
% 0.19/0.49 ~sP0_prd|sK11_skl=sK10_skl),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f67,plain,(
% 0.19/0.49 ~sP0_prd|in(sK10_skl,sK9_skl)),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f68,plain,(
% 0.19/0.49 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~sP0_prd|~hollywood(X0)|~city(X0)|~event(X1)|~chevy(X2)|~car(X2)|~white(X2)|~dirty(X2)|~old(X2)|~street(X3)|~way(X3)|~lonely(X3)|~barrel(X1,X2)|~down(X1,X3)|~in(X1,X0)|~seat(X4)|~furniture(X4)|~front(X4)|X5=X6|~fellow(X5)|~man(X5)|~young(X5)|~fellow(X6)|~man(X6)|~young(X6)|~X5=X7|~in(X7,X4)|~X6=X8|~in(X8,X4))),
% 0.19/0.49 inference(cnf_transformation,[status(thm)],[f39])).
% 0.19/0.49 fof(f97,definition,(
% 0.19/0.49 sQ0_spl <=> (sP0_prd)),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f100,definition,(
% 0.19/0.49 sQ1_spl <=> (hollywood(sK5_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f103,plain,(
% 0.19/0.49 sQ0_spl|sQ1_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f8,f97,f100])).
% 0.19/0.49 fof(f104,definition,(
% 0.19/0.49 sQ2_spl <=> (city(sK5_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f107,plain,(
% 0.19/0.49 sQ0_spl|sQ2_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f9,f97,f104])).
% 0.19/0.49 fof(f108,definition,(
% 0.19/0.49 sQ3_spl <=> (event(sK6_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f111,plain,(
% 0.19/0.49 sQ0_spl|sQ3_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f10,f97,f108])).
% 0.19/0.49 fof(f112,definition,(
% 0.19/0.49 sQ4_spl <=> (chevy(sK8_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f115,plain,(
% 0.19/0.49 sQ0_spl|sQ4_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f11,f97,f112])).
% 0.19/0.49 fof(f116,definition,(
% 0.19/0.49 sQ5_spl <=> (car(sK8_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f119,plain,(
% 0.19/0.49 sQ0_spl|sQ5_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f12,f97,f116])).
% 0.19/0.49 fof(f120,definition,(
% 0.19/0.49 sQ6_spl <=> (white(sK8_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f123,plain,(
% 0.19/0.49 sQ0_spl|sQ6_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f13,f97,f120])).
% 0.19/0.49 fof(f124,definition,(
% 0.19/0.49 sQ7_spl <=> (dirty(sK8_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f127,plain,(
% 0.19/0.49 sQ0_spl|sQ7_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f14,f97,f124])).
% 0.19/0.49 fof(f128,definition,(
% 0.19/0.49 sQ8_spl <=> (old(sK8_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f131,plain,(
% 0.19/0.49 sQ0_spl|sQ8_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f15,f97,f128])).
% 0.19/0.49 fof(f132,definition,(
% 0.19/0.49 sQ9_spl <=> (street(sK7_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f135,plain,(
% 0.19/0.49 sQ0_spl|sQ9_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f16,f97,f132])).
% 0.19/0.49 fof(f136,definition,(
% 0.19/0.49 sQ10_spl <=> (way(sK7_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f139,plain,(
% 0.19/0.49 sQ0_spl|sQ10_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f17,f97,f136])).
% 0.19/0.49 fof(f140,definition,(
% 0.19/0.49 sQ11_spl <=> (lonely(sK7_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f143,plain,(
% 0.19/0.49 sQ0_spl|sQ11_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f18,f97,f140])).
% 0.19/0.49 fof(f144,definition,(
% 0.19/0.49 sQ12_spl <=> (barrel(sK6_skl,sK8_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f145,plain,(
% 0.19/0.49 barrel(sK6_skl,sK8_skl)|~sQ12_spl),
% 0.19/0.49 inference(component_clause,[status(thm)],[f144])).
% 0.19/0.49 fof(f147,plain,(
% 0.19/0.49 sQ0_spl|sQ12_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f19,f97,f144])).
% 0.19/0.49 fof(f148,definition,(
% 0.19/0.49 sQ13_spl <=> (down(sK6_skl,sK7_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f149,plain,(
% 0.19/0.49 down(sK6_skl,sK7_skl)|~sQ13_spl),
% 0.19/0.49 inference(component_clause,[status(thm)],[f148])).
% 0.19/0.49 fof(f151,plain,(
% 0.19/0.49 sQ0_spl|sQ13_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f20,f97,f148])).
% 0.19/0.49 fof(f152,definition,(
% 0.19/0.49 sQ14_spl <=> (in(sK6_skl,sK5_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f153,plain,(
% 0.19/0.49 in(sK6_skl,sK5_skl)|~sQ14_spl),
% 0.19/0.49 inference(component_clause,[status(thm)],[f152])).
% 0.19/0.49 fof(f155,plain,(
% 0.19/0.49 sQ0_spl|sQ14_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f21,f97,f152])).
% 0.19/0.49 fof(f156,definition,(
% 0.19/0.49 sQ15_spl <=> (seat(sK0_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f159,plain,(
% 0.19/0.49 sQ0_spl|sQ15_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f22,f97,f156])).
% 0.19/0.49 fof(f160,definition,(
% 0.19/0.49 sQ16_spl <=> (furniture(sK0_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f163,plain,(
% 0.19/0.49 sQ0_spl|sQ16_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f23,f97,f160])).
% 0.19/0.49 fof(f164,definition,(
% 0.19/0.49 sQ17_spl <=> (front(sK0_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f167,plain,(
% 0.19/0.49 sQ0_spl|sQ17_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f24,f97,f164])).
% 0.19/0.49 fof(f168,definition,(
% 0.19/0.49 sQ18_spl <=> (sK4_skl=sK2_skl)),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f171,plain,(
% 0.19/0.49 sQ0_spl|~sQ18_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f25,f97,f168])).
% 0.19/0.49 fof(f172,definition,(
% 0.19/0.49 sQ19_spl <=> (fellow(sK4_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f175,plain,(
% 0.19/0.49 sQ0_spl|sQ19_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f26,f97,f172])).
% 0.19/0.49 fof(f176,definition,(
% 0.19/0.49 sQ20_spl <=> (man(sK4_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f179,plain,(
% 0.19/0.49 sQ0_spl|sQ20_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f27,f97,f176])).
% 0.19/0.49 fof(f180,definition,(
% 0.19/0.49 sQ21_spl <=> (young(sK4_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f183,plain,(
% 0.19/0.49 sQ0_spl|sQ21_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f28,f97,f180])).
% 0.19/0.49 fof(f184,definition,(
% 0.19/0.49 sQ22_spl <=> (fellow(sK2_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f187,plain,(
% 0.19/0.49 sQ0_spl|sQ22_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f29,f97,f184])).
% 0.19/0.49 fof(f188,definition,(
% 0.19/0.49 sQ23_spl <=> (man(sK2_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f191,plain,(
% 0.19/0.49 sQ0_spl|sQ23_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f30,f97,f188])).
% 0.19/0.49 fof(f192,definition,(
% 0.19/0.49 sQ24_spl <=> (young(sK2_skl))),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f195,plain,(
% 0.19/0.49 sQ0_spl|sQ24_spl),
% 0.19/0.49 inference(split_clause,[status(thm)],[f31,f97,f192])).
% 0.19/0.49 fof(f196,definition,(
% 0.19/0.49 sQ25_spl <=> (sK4_skl=sK3_skl)),
% 0.19/0.49 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.19/0.49 fof(f197,plain,(
% 0.19/0.49 sK4_skl=sK3_skl|~sQ25_spl),
% 0.19/0.49 inference(component_clause,[status(thm)],[f196])).
% 0.19/0.50 fof(f199,plain,(
% 0.19/0.50 sQ0_spl|sQ25_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f32,f97,f196])).
% 0.19/0.50 fof(f200,definition,(
% 0.19/0.50 sQ26_spl <=> (in(sK3_skl,sK0_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f201,plain,(
% 0.19/0.50 in(sK3_skl,sK0_skl)|~sQ26_spl),
% 0.19/0.50 inference(component_clause,[status(thm)],[f200])).
% 0.19/0.50 fof(f203,plain,(
% 0.19/0.50 sQ0_spl|sQ26_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f33,f97,f200])).
% 0.19/0.50 fof(f204,definition,(
% 0.19/0.50 sQ27_spl <=> (sK2_skl=sK1_skl)),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f205,plain,(
% 0.19/0.50 sK2_skl=sK1_skl|~sQ27_spl),
% 0.19/0.50 inference(component_clause,[status(thm)],[f204])).
% 0.19/0.50 fof(f207,plain,(
% 0.19/0.50 sQ0_spl|sQ27_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f34,f97,f204])).
% 0.19/0.50 fof(f208,definition,(
% 0.19/0.50 sQ28_spl <=> (in(sK1_skl,sK0_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f209,plain,(
% 0.19/0.50 in(sK1_skl,sK0_skl)|~sQ28_spl),
% 0.19/0.50 inference(component_clause,[status(thm)],[f208])).
% 0.19/0.50 fof(f211,plain,(
% 0.19/0.50 sQ0_spl|sQ28_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f35,f97,f208])).
% 0.19/0.50 fof(f212,definition,(
% 0.19/0.50 ![X0,X1,X2,X3]: (sQ29_spl <=> (~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)))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f213,plain,(
% 0.19/0.50 ![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)|~sQ29_spl)),
% 0.19/0.50 inference(component_clause,[status(thm)],[f212])).
% 0.19/0.50 fof(f215,definition,(
% 0.19/0.50 ![X4,X5,X6,X7,X8]: (sQ30_spl <=> (~seat(X4)|~furniture(X4)|~front(X4)|X5=X6|~fellow(X5)|~man(X5)|~young(X5)|~fellow(X6)|~man(X6)|~young(X6)|~X5=X7|~in(X7,X4)|~X6=X8|~in(X8,X4)))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f216,plain,(
% 0.19/0.50 ![X0,X1,X2,X3,X4]: (~seat(X0)|~furniture(X0)|~front(X0)|X1=X2|~fellow(X1)|~man(X1)|~young(X1)|~fellow(X2)|~man(X2)|~young(X2)|~X1=X3|~in(X3,X0)|~X2=X4|~in(X4,X0)|~sQ30_spl)),
% 0.19/0.50 inference(component_clause,[status(thm)],[f215])).
% 0.19/0.50 fof(f218,plain,(
% 0.19/0.50 sQ0_spl|sQ29_spl|sQ30_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f36,f97,f212,f215])).
% 0.19/0.50 fof(f219,definition,(
% 0.19/0.50 sQ31_spl <=> (hollywood(sK14_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f222,plain,(
% 0.19/0.50 ~sQ0_spl|sQ31_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f40,f97,f219])).
% 0.19/0.50 fof(f223,definition,(
% 0.19/0.50 sQ32_spl <=> (city(sK14_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f226,plain,(
% 0.19/0.50 ~sQ0_spl|sQ32_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f41,f97,f223])).
% 0.19/0.50 fof(f227,definition,(
% 0.19/0.50 sQ33_spl <=> (event(sK15_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f230,plain,(
% 0.19/0.50 ~sQ0_spl|sQ33_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f42,f97,f227])).
% 0.19/0.50 fof(f231,definition,(
% 0.19/0.50 sQ34_spl <=> (street(sK16_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f234,plain,(
% 0.19/0.50 ~sQ0_spl|sQ34_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f43,f97,f231])).
% 0.19/0.50 fof(f235,definition,(
% 0.19/0.50 sQ35_spl <=> (way(sK16_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f238,plain,(
% 0.19/0.50 ~sQ0_spl|sQ35_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f44,f97,f235])).
% 0.19/0.50 fof(f239,definition,(
% 0.19/0.50 sQ36_spl <=> (lonely(sK16_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f242,plain,(
% 0.19/0.50 ~sQ0_spl|sQ36_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f45,f97,f239])).
% 0.19/0.50 fof(f243,definition,(
% 0.19/0.50 sQ37_spl <=> (chevy(sK17_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f246,plain,(
% 0.19/0.50 ~sQ0_spl|sQ37_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f46,f97,f243])).
% 0.19/0.50 fof(f247,definition,(
% 0.19/0.50 sQ38_spl <=> (car(sK17_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f250,plain,(
% 0.19/0.50 ~sQ0_spl|sQ38_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f47,f97,f247])).
% 0.19/0.50 fof(f251,definition,(
% 0.19/0.50 sQ39_spl <=> (white(sK17_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f254,plain,(
% 0.19/0.50 ~sQ0_spl|sQ39_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f48,f97,f251])).
% 0.19/0.50 fof(f255,definition,(
% 0.19/0.50 sQ40_spl <=> (dirty(sK17_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f258,plain,(
% 0.19/0.50 ~sQ0_spl|sQ40_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f49,f97,f255])).
% 0.19/0.50 fof(f259,definition,(
% 0.19/0.50 sQ41_spl <=> (old(sK17_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f262,plain,(
% 0.19/0.50 ~sQ0_spl|sQ41_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f50,f97,f259])).
% 0.19/0.50 fof(f263,definition,(
% 0.19/0.50 sQ42_spl <=> (barrel(sK15_skl,sK17_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f264,plain,(
% 0.19/0.50 barrel(sK15_skl,sK17_skl)|~sQ42_spl),
% 0.19/0.50 inference(component_clause,[status(thm)],[f263])).
% 0.19/0.50 fof(f266,plain,(
% 0.19/0.50 ~sQ0_spl|sQ42_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f51,f97,f263])).
% 0.19/0.50 fof(f267,definition,(
% 0.19/0.50 sQ43_spl <=> (down(sK15_skl,sK16_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f268,plain,(
% 0.19/0.50 down(sK15_skl,sK16_skl)|~sQ43_spl),
% 0.19/0.50 inference(component_clause,[status(thm)],[f267])).
% 0.19/0.50 fof(f270,plain,(
% 0.19/0.50 ~sQ0_spl|sQ43_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f52,f97,f267])).
% 0.19/0.50 fof(f271,definition,(
% 0.19/0.50 sQ44_spl <=> (in(sK15_skl,sK14_skl))),
% 0.19/0.50 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.19/0.50 fof(f272,plain,(
% 0.19/0.50 in(sK15_skl,sK14_skl)|~sQ44_spl),
% 0.19/0.50 inference(component_clause,[status(thm)],[f271])).
% 0.19/0.50 fof(f274,plain,(
% 0.19/0.50 ~sQ0_spl|sQ44_spl),
% 0.19/0.50 inference(split_clause,[status(thm)],[f53,f97,f271])).
% 0.19/0.50 fof(f275,definition,(
% 0.19/0.51 sQ45_spl <=> (seat(sK9_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f278,plain,(
% 0.19/0.51 ~sQ0_spl|sQ45_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f54,f97,f275])).
% 0.19/0.51 fof(f279,definition,(
% 0.19/0.51 sQ46_spl <=> (furniture(sK9_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f282,plain,(
% 0.19/0.51 ~sQ0_spl|sQ46_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f55,f97,f279])).
% 0.19/0.51 fof(f283,definition,(
% 0.19/0.51 sQ47_spl <=> (front(sK9_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f286,plain,(
% 0.19/0.51 ~sQ0_spl|sQ47_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f56,f97,f283])).
% 0.19/0.51 fof(f287,definition,(
% 0.19/0.51 sQ48_spl <=> (sK13_skl=sK11_skl)),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f290,plain,(
% 0.19/0.51 ~sQ0_spl|~sQ48_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f57,f97,f287])).
% 0.19/0.51 fof(f291,definition,(
% 0.19/0.51 sQ49_spl <=> (fellow(sK13_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f294,plain,(
% 0.19/0.51 ~sQ0_spl|sQ49_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f58,f97,f291])).
% 0.19/0.51 fof(f295,definition,(
% 0.19/0.51 sQ50_spl <=> (man(sK13_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f298,plain,(
% 0.19/0.51 ~sQ0_spl|sQ50_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f59,f97,f295])).
% 0.19/0.51 fof(f299,definition,(
% 0.19/0.51 sQ51_spl <=> (young(sK13_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f302,plain,(
% 0.19/0.51 ~sQ0_spl|sQ51_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f60,f97,f299])).
% 0.19/0.51 fof(f303,definition,(
% 0.19/0.51 sQ52_spl <=> (fellow(sK11_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f306,plain,(
% 0.19/0.51 ~sQ0_spl|sQ52_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f61,f97,f303])).
% 0.19/0.51 fof(f307,definition,(
% 0.19/0.51 sQ53_spl <=> (man(sK11_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f310,plain,(
% 0.19/0.51 ~sQ0_spl|sQ53_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f62,f97,f307])).
% 0.19/0.51 fof(f311,definition,(
% 0.19/0.51 sQ54_spl <=> (young(sK11_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f314,plain,(
% 0.19/0.51 ~sQ0_spl|sQ54_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f63,f97,f311])).
% 0.19/0.51 fof(f315,definition,(
% 0.19/0.51 sQ55_spl <=> (sK13_skl=sK12_skl)),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f316,plain,(
% 0.19/0.51 sK13_skl=sK12_skl|~sQ55_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f315])).
% 0.19/0.51 fof(f318,plain,(
% 0.19/0.51 ~sQ0_spl|sQ55_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f64,f97,f315])).
% 0.19/0.51 fof(f319,definition,(
% 0.19/0.51 sQ56_spl <=> (in(sK12_skl,sK9_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f320,plain,(
% 0.19/0.51 in(sK12_skl,sK9_skl)|~sQ56_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f319])).
% 0.19/0.51 fof(f322,plain,(
% 0.19/0.51 ~sQ0_spl|sQ56_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f65,f97,f319])).
% 0.19/0.51 fof(f323,definition,(
% 0.19/0.51 sQ57_spl <=> (sK11_skl=sK10_skl)),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f324,plain,(
% 0.19/0.51 sK11_skl=sK10_skl|~sQ57_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f323])).
% 0.19/0.51 fof(f326,plain,(
% 0.19/0.51 ~sQ0_spl|sQ57_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f66,f97,f323])).
% 0.19/0.51 fof(f327,definition,(
% 0.19/0.51 sQ58_spl <=> (in(sK10_skl,sK9_skl))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f328,plain,(
% 0.19/0.51 in(sK10_skl,sK9_skl)|~sQ58_spl),
% 0.19/0.51 inference(component_clause,[status(thm)],[f327])).
% 0.19/0.51 fof(f330,plain,(
% 0.19/0.51 ~sQ0_spl|sQ58_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f67,f97,f327])).
% 0.19/0.51 fof(f331,plain,(
% 0.19/0.51 ~sQ0_spl|sQ29_spl|sQ30_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f68,f97,f212,f215])).
% 0.19/0.51 fof(f444,plain,(
% 0.19/0.51 ![X0,X1,X2]: (~seat(X0)|~furniture(X0)|~front(X0)|X1=X2|~fellow(X1)|~man(X1)|~young(X1)|~fellow(X2)|~man(X2)|~young(X2)|~in(X1,X0)|~in(X2,X0)|~sQ30_spl)),
% 0.19/0.51 inference(destructive_equality_resolution,[status(thm)],[f216])).
% 0.19/0.51 fof(f445,plain,(
% 0.19/0.51 in(sK11_skl,sK9_skl)|~sQ57_spl|~sQ58_spl),
% 0.19/0.51 inference(backward_demodulation,[status(thm)],[f324,f328])).
% 0.19/0.51 fof(f446,plain,(
% 0.19/0.51 in(sK13_skl,sK9_skl)|~sQ55_spl|~sQ56_spl),
% 0.19/0.51 inference(backward_demodulation,[status(thm)],[f316,f320])).
% 0.19/0.51 fof(f447,plain,(
% 0.19/0.51 in(sK2_skl,sK0_skl)|~sQ27_spl|~sQ28_spl),
% 0.19/0.51 inference(backward_demodulation,[status(thm)],[f205,f209])).
% 0.19/0.51 fof(f448,plain,(
% 0.19/0.51 in(sK4_skl,sK0_skl)|~sQ25_spl|~sQ26_spl),
% 0.19/0.51 inference(backward_demodulation,[status(thm)],[f197,f201])).
% 0.19/0.51 fof(f472,plain,(
% 0.19/0.51 ![X0,X1]: (~hollywood(X0)|~city(X0)|~event(sK6_skl)|~street(sK7_skl)|~way(sK7_skl)|~lonely(sK7_skl)|~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK6_skl,X1)|~in(sK6_skl,X0)|~sQ29_spl|~sQ13_spl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f213,f149])).
% 0.19/0.51 fof(f473,definition,(
% 0.19/0.51 ![X0]: (sQ94_spl <=> (~hollywood(X0)|~city(X0)|~in(sK6_skl,X0)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f474,plain,(
% 0.19/0.51 ![X0]: (~hollywood(X0)|~city(X0)|~in(sK6_skl,X0)|~sQ94_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f473])).
% 0.19/0.51 fof(f476,definition,(
% 0.19/0.51 ![X1]: (sQ95_spl <=> (~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK6_skl,X1)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f477,plain,(
% 0.19/0.51 ![X0]: (~chevy(X0)|~car(X0)|~white(X0)|~dirty(X0)|~old(X0)|~barrel(sK6_skl,X0)|~sQ95_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f476])).
% 0.19/0.51 fof(f479,plain,(
% 0.19/0.51 sQ94_spl|~sQ3_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|sQ95_spl|~sQ29_spl|~sQ13_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f472,f473,f108,f132,f136,f140,f476,f212,f148])).
% 0.19/0.51 fof(f480,plain,(
% 0.19/0.51 ![X0,X1]: (~hollywood(X0)|~city(X0)|~event(sK15_skl)|~street(sK16_skl)|~way(sK16_skl)|~lonely(sK16_skl)|~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK15_skl,X1)|~in(sK15_skl,X0)|~sQ43_spl|~sQ29_spl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f268,f213])).
% 0.19/0.51 fof(f481,definition,(
% 0.19/0.51 ![X0]: (sQ96_spl <=> (~hollywood(X0)|~city(X0)|~in(sK15_skl,X0)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f482,plain,(
% 0.19/0.51 ![X0]: (~hollywood(X0)|~city(X0)|~in(sK15_skl,X0)|~sQ96_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f481])).
% 0.19/0.51 fof(f484,definition,(
% 0.19/0.51 ![X1]: (sQ97_spl <=> (~chevy(X1)|~car(X1)|~white(X1)|~dirty(X1)|~old(X1)|~barrel(sK15_skl,X1)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f485,plain,(
% 0.19/0.51 ![X0]: (~chevy(X0)|~car(X0)|~white(X0)|~dirty(X0)|~old(X0)|~barrel(sK15_skl,X0)|~sQ97_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f484])).
% 0.19/0.51 fof(f487,plain,(
% 0.19/0.51 sQ96_spl|~sQ33_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|sQ97_spl|~sQ43_spl|~sQ29_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f480,f481,f227,f231,f235,f239,f484,f267,f212])).
% 0.19/0.51 fof(f490,plain,(
% 0.19/0.51 ![X0]: (~seat(sK0_skl)|~furniture(sK0_skl)|~front(sK0_skl)|X0=sK2_skl|~fellow(X0)|~man(X0)|~young(X0)|~fellow(sK2_skl)|~man(sK2_skl)|~young(sK2_skl)|~in(X0,sK0_skl)|~sQ30_spl|~sQ27_spl|~sQ28_spl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f444,f447])).
% 0.19/0.51 fof(f491,plain,(
% 0.19/0.51 ![X0]: (~seat(sK9_skl)|~furniture(sK9_skl)|~front(sK9_skl)|X0=sK13_skl|~fellow(X0)|~man(X0)|~young(X0)|~fellow(sK13_skl)|~man(sK13_skl)|~young(sK13_skl)|~in(X0,sK9_skl)|~sQ30_spl|~sQ55_spl|~sQ56_spl)),
% 0.19/0.51 inference(resolution,[status(thm)],[f444,f446])).
% 0.19/0.51 fof(f499,definition,(
% 0.19/0.51 ![X0]: (sQ99_spl <=> (X0=sK2_skl|~fellow(X0)|~man(X0)|~young(X0)|~in(X0,sK0_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f500,plain,(
% 0.19/0.51 ![X0]: (X0=sK2_skl|~fellow(X0)|~man(X0)|~young(X0)|~in(X0,sK0_skl)|~sQ99_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f499])).
% 0.19/0.51 fof(f502,plain,(
% 0.19/0.51 ~sQ15_spl|~sQ16_spl|~sQ17_spl|sQ99_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl|~sQ30_spl|~sQ27_spl|~sQ28_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f490,f156,f160,f164,f499,f184,f188,f192,f215,f204,f208])).
% 0.19/0.51 fof(f503,definition,(
% 0.19/0.51 ![X0]: (sQ100_spl <=> (X0=sK13_skl|~fellow(X0)|~man(X0)|~young(X0)|~in(X0,sK9_skl)))),
% 0.19/0.51 introduced(definition,[new_symbols(definition,[sQ100_spl])],[split_symbol_definition])).
% 0.19/0.51 fof(f504,plain,(
% 0.19/0.51 ![X0]: (X0=sK13_skl|~fellow(X0)|~man(X0)|~young(X0)|~in(X0,sK9_skl)|~sQ100_spl)),
% 0.19/0.51 inference(component_clause,[status(thm)],[f503])).
% 0.19/0.51 fof(f506,plain,(
% 0.19/0.51 ~sQ45_spl|~sQ46_spl|~sQ47_spl|sQ100_spl|~sQ49_spl|~sQ50_spl|~sQ51_spl|~sQ30_spl|~sQ55_spl|~sQ56_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f491,f275,f279,f283,f503,f291,f295,f299,f215,f315,f319])).
% 0.19/0.51 fof(f539,plain,(
% 0.19/0.51 ~hollywood(sK14_skl)|~city(sK14_skl)|~sQ96_spl|~sQ44_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f482,f272])).
% 0.19/0.51 fof(f540,plain,(
% 0.19/0.51 ~sQ31_spl|~sQ32_spl|~sQ96_spl|~sQ44_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f539,f219,f223,f481,f271])).
% 0.19/0.51 fof(f541,plain,(
% 0.19/0.51 ~chevy(sK17_skl)|~car(sK17_skl)|~white(sK17_skl)|~dirty(sK17_skl)|~old(sK17_skl)|~sQ97_spl|~sQ42_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f485,f264])).
% 0.19/0.51 fof(f542,plain,(
% 0.19/0.51 ~sQ37_spl|~sQ38_spl|~sQ39_spl|~sQ40_spl|~sQ41_spl|~sQ97_spl|~sQ42_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f541,f243,f247,f251,f255,f259,f484,f263])).
% 0.19/0.51 fof(f549,plain,(
% 0.19/0.51 sK11_skl=sK13_skl|~fellow(sK11_skl)|~man(sK11_skl)|~young(sK11_skl)|~sQ100_spl|~sQ57_spl|~sQ58_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f504,f445])).
% 0.19/0.51 fof(f551,plain,(
% 0.19/0.51 sQ48_spl|~sQ52_spl|~sQ53_spl|~sQ54_spl|~sQ100_spl|~sQ57_spl|~sQ58_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f549,f287,f303,f307,f311,f503,f323,f327])).
% 0.19/0.51 fof(f558,plain,(
% 0.19/0.51 ~hollywood(sK5_skl)|~city(sK5_skl)|~sQ14_spl|~sQ94_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f153,f474])).
% 0.19/0.51 fof(f559,plain,(
% 0.19/0.51 ~sQ1_spl|~sQ2_spl|~sQ14_spl|~sQ94_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f558,f100,f104,f152,f473])).
% 0.19/0.51 fof(f568,plain,(
% 0.19/0.51 sK4_skl=sK2_skl|~fellow(sK4_skl)|~man(sK4_skl)|~young(sK4_skl)|~sQ99_spl|~sQ25_spl|~sQ26_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f500,f448])).
% 0.19/0.51 fof(f573,plain,(
% 0.19/0.51 sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ21_spl|~sQ99_spl|~sQ25_spl|~sQ26_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f568,f168,f172,f176,f180,f499,f196,f200])).
% 0.19/0.51 fof(f581,plain,(
% 0.19/0.51 ~chevy(sK8_skl)|~car(sK8_skl)|~white(sK8_skl)|~dirty(sK8_skl)|~old(sK8_skl)|~sQ95_spl|~sQ12_spl),
% 0.19/0.51 inference(resolution,[status(thm)],[f477,f145])).
% 0.19/0.51 fof(f582,plain,(
% 0.19/0.51 ~sQ4_spl|~sQ5_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ95_spl|~sQ12_spl),
% 0.19/0.51 inference(split_clause,[status(thm)],[f581,f112,f116,f120,f124,f128,f476,f144])).
% 0.19/0.51 fof(f583,plain,(
% 0.19/0.51 $false),
% 0.19/0.51 inference(sat_refutation,[status(thm)],[f103,f107,f111,f115,f119,f123,f127,f131,f135,f139,f143,f147,f151,f155,f159,f163,f167,f171,f175,f179,f183,f187,f191,f195,f199,f203,f207,f211,f218,f222,f226,f230,f234,f238,f242,f246,f250,f254,f258,f262,f266,f270,f274,f278,f282,f286,f290,f294,f298,f302,f306,f310,f314,f318,f322,f326,f330,f331,f479,f487,f502,f506,f540,f542,f551,f559,f573,f582])).
% 0.19/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.19/0.52 % Elapsed time: 0.064555 seconds
% 0.19/0.52 % CPU time: 0.189824 seconds
% 0.19/0.52 % Total memory used: 49.288 MB
% 0.19/0.52 % Net memory used: 49.162 MB
%------------------------------------------------------------------------------