%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : NLP007+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 : n015.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.12s 0.40s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP007+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.36 % Computer : n015.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Mon Sep 21 01:34:20 UTC 2026
% 0.11/0.36 % CPUTime :
% 0.12/0.37 % Drodi V4.1.1
% 0.12/0.40 % Refutation found
% 0.12/0.40 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.12/0.40 % SZS output start CNFRefutation for theBenchmark
% 0.12/0.40 fof(f1,conjecture,(
% 0.12/0.40 ( ( (? [U,V,W,X,Y,Z,X1,X2,X3,X4] :( seat(U)& furniture(U)& front(U)& hollywood(V)& city(V)& event(W)& chevy(X)& car(X)& white(X)& dirty(X)& old(X)& street(Y)& way(Y)& lonely(Y)& barrel(W,X)& down(W,Y)& in(W,V)& seat(X2)& furniture(X2)& front(X2)& Z != X1& fellow(Z)& man(Z)& young(Z)& fellow(X1)& man(X1)& young(X1)& Z = X3& in(X3,X2)& X1 = X4& in(X4,U) ))=> (? [X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :( seat(X5)& furniture(X5)& front(X5)& hollywood(X6)& city(X6)& event(X7)& chevy(X8)& car(X8)& white(X8)& dirty(X8)& old(X8)& street(X9)& way(X9)& lonely(X9)& barrel(X7,X8)& down(X7,X9)& in(X7,X6)& seat(X12)& furniture(X12)& front(X12)& X10 != X11& fellow(X10)& man(X10)& young(X10)& fellow(X11)& man(X11)& young(X11)& X10 = X13& in(X13,X5)& X11 = X14& in(X14,X12) ) ))& ( (? [X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :( seat(X15)& furniture(X15)& front(X15)& hollywood(X16)& city(X16)& event(X17)& chevy(X18)& car(X18)& white(X18)& dirty(X18)& old(X18)& street(X19)& way(X19)& lonely(X19)& barrel(X17,X18)& down(X17,X19)& in(X17,X16)& seat(X22)& furniture(X22)& front(X22)& X20 != X21& fellow(X20)& man(X20)& young(X20)& fellow(X21)& man(X21)& young(X21)& X20 = X23& in(X23,X15)& X21 = X24& in(X24,X22) ))=> (? [X25,X26,X27,X28,X29,X30,X31,X32,X33,X34] :( seat(X25)& furniture(X25)& front(X25)& hollywood(X26)& city(X26)& event(X27)& chevy(X28)& car(X28)& white(X28)& dirty(X28)& old(X28)& street(X29)& way(X29)& lonely(X29)& barrel(X27,X28)& down(X27,X29)& in(X27,X26)& seat(X32)& furniture(X32)& front(X32)& X30 != X31& fellow(X30)& man(X30)& young(X30)& fellow(X31)& man(X31)& young(X31)& X30 = X33& in(X33,X32)& X31 = X34& in(X34,X25) ) )) ) ),
% 0.12/0.40 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.12/0.40 fof(f2,negated_conjecture,(
% 0.12/0.40 ~(( ( (? [U,V,W,X,Y,Z,X1,X2,X3,X4] :( seat(U)& furniture(U)& front(U)& hollywood(V)& city(V)& event(W)& chevy(X)& car(X)& white(X)& dirty(X)& old(X)& street(Y)& way(Y)& lonely(Y)& barrel(W,X)& down(W,Y)& in(W,V)& seat(X2)& furniture(X2)& front(X2)& Z != X1& fellow(Z)& man(Z)& young(Z)& fellow(X1)& man(X1)& young(X1)& Z = X3& in(X3,X2)& X1 = X4& in(X4,U) ))=> (? [X5,X6,X7,X8,X9,X10,X11,X12,X13,X14] :( seat(X5)& furniture(X5)& front(X5)& hollywood(X6)& city(X6)& event(X7)& chevy(X8)& car(X8)& white(X8)& dirty(X8)& old(X8)& street(X9)& way(X9)& lonely(X9)& barrel(X7,X8)& down(X7,X9)& in(X7,X6)& seat(X12)& furniture(X12)& front(X12)& X10 != X11& fellow(X10)& man(X10)& young(X10)& fellow(X11)& man(X11)& young(X11)& X10 = X13& in(X13,X5)& X11 = X14& in(X14,X12) ) ))& ( (? [X15,X16,X17,X18,X19,X20,X21,X22,X23,X24] :( seat(X15)& furniture(X15)& front(X15)& hollywood(X16)& city(X16)& event(X17)& chevy(X18)& car(X18)& white(X18)& dirty(X18)& old(X18)& street(X19)& way(X19)& lonely(X19)& barrel(X17,X18)& down(X17,X19)& in(X17,X16)& seat(X22)& furniture(X22)& front(X22)& X20 != X21& fellow(X20)& man(X20)& young(X20)& fellow(X21)& man(X21)& young(X21)& X20 = X23& in(X23,X15)& X21 = X24& in(X24,X22) ))=> (? [X25,X26,X27,X28,X29,X30,X31,X32,X33,X34] :( seat(X25)& furniture(X25)& front(X25)& hollywood(X26)& city(X26)& event(X27)& chevy(X28)& car(X28)& white(X28)& dirty(X28)& old(X28)& street(X29)& way(X29)& lonely(X29)& barrel(X27,X28)& down(X27,X29)& in(X27,X26)& seat(X32)& furniture(X32)& front(X32)& X30 != X31& fellow(X30)& man(X30)& young(X30)& fellow(X31)& man(X31)& young(X31)& X30 = X33& in(X33,X32)& X31 = X34& in(X34,X25) ) )) ) )),
% 0.12/0.40 inference(negated_conjecture,[status(cth)],[f1])).
% 0.12/0.40 fof(f3,plain,(
% 0.12/0.40 (((?[U,V,W,X,Y,Z,X1,X2,X3,X4]: ((((((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&street(Y))&way(Y))&lonely(Y))&barrel(W,X))&down(W,Y))&in(W,V))&seat(X2))&furniture(X2))&front(X2))&~Z=X1)&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,X2))&X1=X4)&in(X4,U)))&(![X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: ((((((((((((((((((((((((((((((~seat(X5)|~furniture(X5))|~front(X5))|~hollywood(X6))|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|~seat(X12))|~furniture(X12))|~front(X12))|X10=X11)|~fellow(X10))|~man(X10))|~young(X10))|~fellow(X11))|~man(X11))|~young(X11))|~X10=X13)|~in(X13,X5))|~X11=X14)|~in(X14,X12))))|((?[X15,X16,X17,X18,X19,X20,X21,X22,X23,X24]: ((((((((((((((((((((((((((((((seat(X15)&furniture(X15))&front(X15))&hollywood(X16))&city(X16))&event(X17))&chevy(X18))&car(X18))&white(X18))&dirty(X18))&old(X18))&street(X19))&way(X19))&lonely(X19))&barrel(X17,X18))&down(X17,X19))&in(X17,X16))&seat(X22))&furniture(X22))&front(X22))&~X20=X21)&fellow(X20))&man(X20))&young(X20))&fellow(X21))&man(X21))&young(X21))&X20=X23)&in(X23,X15))&X21=X24)&in(X24,X22)))&(![X25,X26,X27,X28,X29,X30,X31,X32,X33,X34]: ((((((((((((((((((((((((((((((~seat(X25)|~furniture(X25))|~front(X25))|~hollywood(X26))|~city(X26))|~event(X27))|~chevy(X28))|~car(X28))|~white(X28))|~dirty(X28))|~old(X28))|~street(X29))|~way(X29))|~lonely(X29))|~barrel(X27,X28))|~down(X27,X29))|~in(X27,X26))|~seat(X32))|~furniture(X32))|~front(X32))|X30=X31)|~fellow(X30))|~man(X30))|~young(X30))|~fellow(X31))|~man(X31))|~young(X31))|~X30=X33)|~in(X33,X32))|~X31=X34)|~in(X34,X25)))))),
% 0.12/0.40 inference(pre_NNF_transformation,[status(thm)],[f2])).
% 0.12/0.40 fof(f4,definition,(
% 0.12/0.40 sP0_prd<=>((?[U,V,W,X,Y,Z,X1,X2,X3,X4]: ((((((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&street(Y))&way(Y))&lonely(Y))&barrel(W,X))&down(W,Y))&in(W,V))&seat(X2))&furniture(X2))&front(X2))&~Z=X1)&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,X2))&X1=X4)&in(X4,U)))&(![X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: ((((((((((((((((((((((((((((((~seat(X5)|~furniture(X5))|~front(X5))|~hollywood(X6))|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|~seat(X12))|~furniture(X12))|~front(X12))|X10=X11)|~fellow(X10))|~man(X10))|~young(X10))|~fellow(X11))|~man(X11))|~young(X11))|~X10=X13)|~in(X13,X5))|~X11=X14)|~in(X14,X12))))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sP0_prd])],[])).
% 0.12/0.40 fof(f5,plain,(
% 0.12/0.40 sP0_prd|((?[X15,X16,X17,X18,X19,X20,X21,X22,X23,X24]: ((((((((((((((((((((((((((((((seat(X15)&furniture(X15))&front(X15))&hollywood(X16))&city(X16))&event(X17))&chevy(X18))&car(X18))&white(X18))&dirty(X18))&old(X18))&street(X19))&way(X19))&lonely(X19))&barrel(X17,X18))&down(X17,X19))&in(X17,X16))&seat(X22))&furniture(X22))&front(X22))&~X20=X21)&fellow(X20))&man(X20))&young(X20))&fellow(X21))&man(X21))&young(X21))&X20=X23)&in(X23,X15))&X21=X24)&in(X24,X22)))&(![X25,X26,X27,X28,X29,X30,X31,X32,X33,X34]: ((((((((((((((((((((((((((((((~seat(X25)|~furniture(X25))|~front(X25))|~hollywood(X26))|~city(X26))|~event(X27))|~chevy(X28))|~car(X28))|~white(X28))|~dirty(X28))|~old(X28))|~street(X29))|~way(X29))|~lonely(X29))|~barrel(X27,X28))|~down(X27,X29))|~in(X27,X26))|~seat(X32))|~furniture(X32))|~front(X32))|X30=X31)|~fellow(X30))|~man(X30))|~young(X30))|~fellow(X31))|~man(X31))|~young(X31))|~X30=X33)|~in(X33,X32))|~X31=X34)|~in(X34,X25))))),
% 0.12/0.40 inference(formula_renaming,[status(thm)],[f3,f4])).
% 0.12/0.40 fof(f6,plain,(
% 0.12/0.40 sP0_prd|((?[X22,X24]: ((?[X21]: ((?[X15,X23]: ((?[X20]: ((((((((((((?[X16,X17]: ((?[X19]: ((?[X18]: ((((((((((((((seat(X15)&furniture(X15))&front(X15))&hollywood(X16))&city(X16))&event(X17))&chevy(X18))&car(X18))&white(X18))&dirty(X18))&old(X18))&street(X19))&way(X19))&lonely(X19))&barrel(X17,X18)))&down(X17,X19)))&in(X17,X16)))&seat(X22))&furniture(X22))&front(X22))&~X20=X21)&fellow(X20))&man(X20))&young(X20))&fellow(X21))&man(X21))&young(X21))&X20=X23))&in(X23,X15)))&X21=X24))&in(X24,X22)))&(![X25,X34]: ((![X31]: ((![X32,X33]: ((![X30]: ((((((((((((![X26,X27]: ((![X29]: ((![X28]: ((((((((((((((~seat(X25)|~furniture(X25))|~front(X25))|~hollywood(X26))|~city(X26))|~event(X27))|~chevy(X28))|~car(X28))|~white(X28))|~dirty(X28))|~old(X28))|~street(X29))|~way(X29))|~lonely(X29))|~barrel(X27,X28)))|~down(X27,X29)))|~in(X27,X26)))|~seat(X32))|~furniture(X32))|~front(X32))|X30=X31)|~fellow(X30))|~man(X30))|~young(X30))|~fellow(X31))|~man(X31))|~young(X31))|~X30=X33))|~in(X33,X32)))|~X31=X34))|~in(X34,X25))))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f5])).
% 0.12/0.40 fof(f7,plain,(
% 0.12/0.40 sP0_prd|(((((((((((((((((((((((((((((((seat(sK3_skl)&furniture(sK3_skl))&front(sK3_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))&seat(sK0_skl))&furniture(sK0_skl))&front(sK0_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))&(![X25,X34]: ((![X31]: ((![X32,X33]: ((![X30]: ((((((((((((![X26,X27]: ((![X29]: ((![X28]: ((((((((((((((~seat(X25)|~furniture(X25))|~front(X25))|~hollywood(X26))|~city(X26))|~event(X27))|~chevy(X28))|~car(X28))|~white(X28))|~dirty(X28))|~old(X28))|~street(X29))|~way(X29))|~lonely(X29))|~barrel(X27,X28)))|~down(X27,X29)))|~in(X27,X26)))|~seat(X32))|~furniture(X32))|~front(X32))|X30=X31)|~fellow(X30))|~man(X30))|~young(X30))|~fellow(X31))|~man(X31))|~young(X31))|~X30=X33))|~in(X33,X32)))|~X31=X34))|~in(X34,X25))))),
% 0.12/0.40 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(X22,sK0_skl),skolemize(X24,sK1_skl),skolemize(X21,sK2_skl),skolemize(X15,sK3_skl),skolemize(X23,sK4_skl),skolemize(X20,sK5_skl),skolemize(X16,sK6_skl),skolemize(X17,sK7_skl),skolemize(X19,sK8_skl),skolemize(X18,sK9_skl)],[f6])).
% 0.12/0.40 fof(f8,plain,(
% 0.12/0.40 sP0_prd|seat(sK3_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f9,plain,(
% 0.12/0.40 sP0_prd|furniture(sK3_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f10,plain,(
% 0.12/0.40 sP0_prd|front(sK3_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f11,plain,(
% 0.12/0.40 sP0_prd|hollywood(sK6_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f12,plain,(
% 0.12/0.40 sP0_prd|city(sK6_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f13,plain,(
% 0.12/0.40 sP0_prd|event(sK7_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f14,plain,(
% 0.12/0.40 sP0_prd|chevy(sK9_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f15,plain,(
% 0.12/0.40 sP0_prd|car(sK9_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f16,plain,(
% 0.12/0.40 sP0_prd|white(sK9_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f17,plain,(
% 0.12/0.40 sP0_prd|dirty(sK9_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f18,plain,(
% 0.12/0.40 sP0_prd|old(sK9_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f19,plain,(
% 0.12/0.40 sP0_prd|street(sK8_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f20,plain,(
% 0.12/0.40 sP0_prd|way(sK8_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f21,plain,(
% 0.12/0.40 sP0_prd|lonely(sK8_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f22,plain,(
% 0.12/0.40 sP0_prd|barrel(sK7_skl,sK9_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f23,plain,(
% 0.12/0.40 sP0_prd|down(sK7_skl,sK8_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f24,plain,(
% 0.12/0.40 sP0_prd|in(sK7_skl,sK6_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f25,plain,(
% 0.12/0.40 sP0_prd|seat(sK0_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f26,plain,(
% 0.12/0.40 sP0_prd|furniture(sK0_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f27,plain,(
% 0.12/0.40 sP0_prd|front(sK0_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f28,plain,(
% 0.12/0.40 sP0_prd|~sK5_skl=sK2_skl),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f29,plain,(
% 0.12/0.40 sP0_prd|fellow(sK5_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f30,plain,(
% 0.12/0.40 sP0_prd|man(sK5_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f31,plain,(
% 0.12/0.40 sP0_prd|young(sK5_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f32,plain,(
% 0.12/0.40 sP0_prd|fellow(sK2_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f33,plain,(
% 0.12/0.40 sP0_prd|man(sK2_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f34,plain,(
% 0.12/0.40 sP0_prd|young(sK2_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f35,plain,(
% 0.12/0.40 sP0_prd|sK5_skl=sK4_skl),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f36,plain,(
% 0.12/0.40 sP0_prd|in(sK4_skl,sK3_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f37,plain,(
% 0.12/0.40 sP0_prd|sK2_skl=sK1_skl),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f38,plain,(
% 0.12/0.40 sP0_prd|in(sK1_skl,sK0_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f39,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (sP0_prd|~seat(X0)|~furniture(X0)|~front(X0)|~hollywood(X1)|~city(X1)|~event(X2)|~chevy(X3)|~car(X3)|~white(X3)|~dirty(X3)|~old(X3)|~street(X4)|~way(X4)|~lonely(X4)|~barrel(X2,X3)|~down(X2,X4)|~in(X2,X1)|~seat(X5)|~furniture(X5)|~front(X5)|X6=X7|~fellow(X6)|~man(X6)|~young(X6)|~fellow(X7)|~man(X7)|~young(X7)|~X6=X8|~in(X8,X5)|~X7=X9|~in(X9,X0))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f7])).
% 0.12/0.40 fof(f40,plain,(
% 0.12/0.40 (~sP0_prd|((?[U,V,W,X,Y,Z,X1,X2,X3,X4]: ((((((((((((((((((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&street(Y))&way(Y))&lonely(Y))&barrel(W,X))&down(W,Y))&in(W,V))&seat(X2))&furniture(X2))&front(X2))&~Z=X1)&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3)&in(X3,X2))&X1=X4)&in(X4,U)))&(![X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: ((((((((((((((((((((((((((((((~seat(X5)|~furniture(X5))|~front(X5))|~hollywood(X6))|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8))|~down(X7,X9))|~in(X7,X6))|~seat(X12))|~furniture(X12))|~front(X12))|X10=X11)|~fellow(X10))|~man(X10))|~young(X10))|~fellow(X11))|~man(X11))|~young(X11))|~X10=X13)|~in(X13,X5))|~X11=X14)|~in(X14,X12)))))&(sP0_prd|((![U,V,W,X,Y,Z,X1,X2,X3,X4]: ((((((((((((((((((((((((((((((~seat(U)|~furniture(U))|~front(U))|~hollywood(V))|~city(V))|~event(W))|~chevy(X))|~car(X))|~white(X))|~dirty(X))|~old(X))|~street(Y))|~way(Y))|~lonely(Y))|~barrel(W,X))|~down(W,Y))|~in(W,V))|~seat(X2))|~furniture(X2))|~front(X2))|Z=X1)|~fellow(Z))|~man(Z))|~young(Z))|~fellow(X1))|~man(X1))|~young(X1))|~Z=X3)|~in(X3,X2))|~X1=X4)|~in(X4,U)))|(?[X5,X6,X7,X8,X9,X10,X11,X12,X13,X14]: ((((((((((((((((((((((((((((((seat(X5)&furniture(X5))&front(X5))&hollywood(X6))&city(X6))&event(X7))&chevy(X8))&car(X8))&white(X8))&dirty(X8))&old(X8))&street(X9))&way(X9))&lonely(X9))&barrel(X7,X8))&down(X7,X9))&in(X7,X6))&seat(X12))&furniture(X12))&front(X12))&~X10=X11)&fellow(X10))&man(X10))&young(X10))&fellow(X11))&man(X11))&young(X11))&X10=X13)&in(X13,X5))&X11=X14)&in(X14,X12)))))),
% 0.12/0.40 inference(NNF_transformation,[status(thm)],[f4])).
% 0.12/0.40 fof(f41,plain,(
% 0.12/0.40 (~sP0_prd|((?[U,X4]: ((?[X1]: ((?[X2,X3]: ((?[Z]: ((((((((((((?[V,W]: ((?[Y]: ((?[X]: ((((((((((((((seat(U)&furniture(U))&front(U))&hollywood(V))&city(V))&event(W))&chevy(X))&car(X))&white(X))&dirty(X))&old(X))&street(Y))&way(Y))&lonely(Y))&barrel(W,X)))&down(W,Y)))&in(W,V)))&seat(X2))&furniture(X2))&front(X2))&~Z=X1)&fellow(Z))&man(Z))&young(Z))&fellow(X1))&man(X1))&young(X1))&Z=X3))&in(X3,X2)))&X1=X4))&in(X4,U)))&(![X12,X14]: ((![X11]: ((![X5,X13]: ((![X10]: ((((((((((((![X6,X7]: ((![X9]: ((![X8]: ((((((((((((((~seat(X5)|~furniture(X5))|~front(X5))|~hollywood(X6))|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8)))|~down(X7,X9)))|~in(X7,X6)))|~seat(X12))|~furniture(X12))|~front(X12))|X10=X11)|~fellow(X10))|~man(X10))|~young(X10))|~fellow(X11))|~man(X11))|~young(X11))|~X10=X13))|~in(X13,X5)))|~X11=X14))|~in(X14,X12)))))&(sP0_prd|((![U,X4]: ((![X1]: ((![X2,X3]: ((![Z]: ((((((((((((![V,W]: ((![Y]: ((![X]: ((((((((((((((~seat(U)|~furniture(U))|~front(U))|~hollywood(V))|~city(V))|~event(W))|~chevy(X))|~car(X))|~white(X))|~dirty(X))|~old(X))|~street(Y))|~way(Y))|~lonely(Y))|~barrel(W,X)))|~down(W,Y)))|~in(W,V)))|~seat(X2))|~furniture(X2))|~front(X2))|Z=X1)|~fellow(Z))|~man(Z))|~young(Z))|~fellow(X1))|~man(X1))|~young(X1))|~Z=X3))|~in(X3,X2)))|~X1=X4))|~in(X4,U)))|(?[X12,X14]: ((?[X11]: ((?[X5,X13]: ((?[X10]: ((((((((((((?[X6,X7]: ((?[X9]: ((?[X8]: ((((((((((((((seat(X5)&furniture(X5))&front(X5))&hollywood(X6))&city(X6))&event(X7))&chevy(X8))&car(X8))&white(X8))&dirty(X8))&old(X8))&street(X9))&way(X9))&lonely(X9))&barrel(X7,X8)))&down(X7,X9)))&in(X7,X6)))&seat(X12))&furniture(X12))&front(X12))&~X10=X11)&fellow(X10))&man(X10))&young(X10))&fellow(X11))&man(X11))&young(X11))&X10=X13))&in(X13,X5)))&X11=X14))&in(X14,X12)))))),
% 0.12/0.40 inference(miniscoping,[status(thm)],[f40])).
% 0.12/0.40 fof(f42,plain,(
% 0.12/0.40 (~sP0_prd|(((((((((((((((((((((((((((((((seat(sK10_skl)&furniture(sK10_skl))&front(sK10_skl))&hollywood(sK16_skl))&city(sK16_skl))&event(sK17_skl))&chevy(sK19_skl))&car(sK19_skl))&white(sK19_skl))&dirty(sK19_skl))&old(sK19_skl))&street(sK18_skl))&way(sK18_skl))&lonely(sK18_skl))&barrel(sK17_skl,sK19_skl))&down(sK17_skl,sK18_skl))&in(sK17_skl,sK16_skl))&seat(sK13_skl))&furniture(sK13_skl))&front(sK13_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))&(![X12,X14]: ((![X11]: ((![X5,X13]: ((![X10]: ((((((((((((![X6,X7]: ((![X9]: ((![X8]: ((((((((((((((~seat(X5)|~furniture(X5))|~front(X5))|~hollywood(X6))|~city(X6))|~event(X7))|~chevy(X8))|~car(X8))|~white(X8))|~dirty(X8))|~old(X8))|~street(X9))|~way(X9))|~lonely(X9))|~barrel(X7,X8)))|~down(X7,X9)))|~in(X7,X6)))|~seat(X12))|~furniture(X12))|~front(X12))|X10=X11)|~fellow(X10))|~man(X10))|~young(X10))|~fellow(X11))|~man(X11))|~young(X11))|~X10=X13))|~in(X13,X5)))|~X11=X14))|~in(X14,X12)))))&(sP0_prd|((![U,X4]: ((![X1]: ((![X2,X3]: ((![Z]: ((((((((((((![V,W]: ((![Y]: ((![X]: ((((((((((((((~seat(U)|~furniture(U))|~front(U))|~hollywood(V))|~city(V))|~event(W))|~chevy(X))|~car(X))|~white(X))|~dirty(X))|~old(X))|~street(Y))|~way(Y))|~lonely(Y))|~barrel(W,X)))|~down(W,Y)))|~in(W,V)))|~seat(X2))|~furniture(X2))|~front(X2))|Z=X1)|~fellow(Z))|~man(Z))|~young(Z))|~fellow(X1))|~man(X1))|~young(X1))|~Z=X3))|~in(X3,X2)))|~X1=X4))|~in(X4,U)))|((((((((((((((((((((((((((((((seat(sK23_skl)&furniture(sK23_skl))&front(sK23_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))&seat(sK20_skl))&furniture(sK20_skl))&front(sK20_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.40 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(U,sK10_skl),skolemize(X4,sK11_skl),skolemize(X1,sK12_skl),skolemize(X2,sK13_skl),skolemize(X3,sK14_skl),skolemize(Z,sK15_skl),skolemize(V,sK16_skl),skolemize(W,sK17_skl),skolemize(Y,sK18_skl),skolemize(X,sK19_skl),skolemize(X12,sK20_skl),skolemize(X14,sK21_skl),skolemize(X11,sK22_skl),skolemize(X5,sK23_skl),skolemize(X13,sK24_skl),skolemize(X10,sK25_skl),skolemize(X6,sK26_skl),skolemize(X7,sK27_skl),skolemize(X9,sK28_skl),skolemize(X8,sK29_skl)],[f41])).
% 0.12/0.40 fof(f43,plain,(
% 0.12/0.40 ~sP0_prd|seat(sK10_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f44,plain,(
% 0.12/0.40 ~sP0_prd|furniture(sK10_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f45,plain,(
% 0.12/0.40 ~sP0_prd|front(sK10_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f46,plain,(
% 0.12/0.40 ~sP0_prd|hollywood(sK16_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f47,plain,(
% 0.12/0.40 ~sP0_prd|city(sK16_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f48,plain,(
% 0.12/0.40 ~sP0_prd|event(sK17_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f49,plain,(
% 0.12/0.40 ~sP0_prd|chevy(sK19_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f50,plain,(
% 0.12/0.40 ~sP0_prd|car(sK19_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f51,plain,(
% 0.12/0.40 ~sP0_prd|white(sK19_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f52,plain,(
% 0.12/0.40 ~sP0_prd|dirty(sK19_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f53,plain,(
% 0.12/0.40 ~sP0_prd|old(sK19_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f54,plain,(
% 0.12/0.40 ~sP0_prd|street(sK18_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f55,plain,(
% 0.12/0.40 ~sP0_prd|way(sK18_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f56,plain,(
% 0.12/0.40 ~sP0_prd|lonely(sK18_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f57,plain,(
% 0.12/0.40 ~sP0_prd|barrel(sK17_skl,sK19_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f58,plain,(
% 0.12/0.40 ~sP0_prd|down(sK17_skl,sK18_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f59,plain,(
% 0.12/0.40 ~sP0_prd|in(sK17_skl,sK16_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f60,plain,(
% 0.12/0.40 ~sP0_prd|seat(sK13_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f61,plain,(
% 0.12/0.40 ~sP0_prd|furniture(sK13_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f62,plain,(
% 0.12/0.40 ~sP0_prd|front(sK13_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f63,plain,(
% 0.12/0.40 ~sP0_prd|~sK15_skl=sK12_skl),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f64,plain,(
% 0.12/0.40 ~sP0_prd|fellow(sK15_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f65,plain,(
% 0.12/0.40 ~sP0_prd|man(sK15_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f66,plain,(
% 0.12/0.40 ~sP0_prd|young(sK15_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f67,plain,(
% 0.12/0.40 ~sP0_prd|fellow(sK12_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f68,plain,(
% 0.12/0.40 ~sP0_prd|man(sK12_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f69,plain,(
% 0.12/0.40 ~sP0_prd|young(sK12_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f70,plain,(
% 0.12/0.40 ~sP0_prd|sK15_skl=sK14_skl),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f71,plain,(
% 0.12/0.40 ~sP0_prd|in(sK14_skl,sK13_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f72,plain,(
% 0.12/0.40 ~sP0_prd|sK12_skl=sK11_skl),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f73,plain,(
% 0.12/0.40 ~sP0_prd|in(sK11_skl,sK10_skl)),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f74,plain,(
% 0.12/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~sP0_prd|~seat(X0)|~furniture(X0)|~front(X0)|~hollywood(X1)|~city(X1)|~event(X2)|~chevy(X3)|~car(X3)|~white(X3)|~dirty(X3)|~old(X3)|~street(X4)|~way(X4)|~lonely(X4)|~barrel(X2,X3)|~down(X2,X4)|~in(X2,X1)|~seat(X5)|~furniture(X5)|~front(X5)|X6=X7|~fellow(X6)|~man(X6)|~young(X6)|~fellow(X7)|~man(X7)|~young(X7)|~X6=X8|~in(X8,X0)|~X7=X9|~in(X9,X5))),
% 0.12/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.12/0.40 fof(f106,definition,(
% 0.12/0.40 sQ0_spl <=> (sP0_prd)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f109,definition,(
% 0.12/0.40 sQ1_spl <=> (seat(sK3_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f112,plain,(
% 0.12/0.40 sQ0_spl|sQ1_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f8,f106,f109])).
% 0.12/0.40 fof(f113,definition,(
% 0.12/0.40 sQ2_spl <=> (furniture(sK3_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f116,plain,(
% 0.12/0.40 sQ0_spl|sQ2_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f9,f106,f113])).
% 0.12/0.40 fof(f117,definition,(
% 0.12/0.40 sQ3_spl <=> (front(sK3_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f120,plain,(
% 0.12/0.40 sQ0_spl|sQ3_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f10,f106,f117])).
% 0.12/0.40 fof(f121,definition,(
% 0.12/0.40 sQ4_spl <=> (hollywood(sK6_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f124,plain,(
% 0.12/0.40 sQ0_spl|sQ4_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f11,f106,f121])).
% 0.12/0.40 fof(f125,definition,(
% 0.12/0.40 sQ5_spl <=> (city(sK6_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f128,plain,(
% 0.12/0.40 sQ0_spl|sQ5_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f12,f106,f125])).
% 0.12/0.40 fof(f129,definition,(
% 0.12/0.40 sQ6_spl <=> (event(sK7_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f132,plain,(
% 0.12/0.40 sQ0_spl|sQ6_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f13,f106,f129])).
% 0.12/0.40 fof(f133,definition,(
% 0.12/0.40 sQ7_spl <=> (chevy(sK9_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f136,plain,(
% 0.12/0.40 sQ0_spl|sQ7_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f14,f106,f133])).
% 0.12/0.40 fof(f137,definition,(
% 0.12/0.40 sQ8_spl <=> (car(sK9_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f140,plain,(
% 0.12/0.40 sQ0_spl|sQ8_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f15,f106,f137])).
% 0.12/0.40 fof(f141,definition,(
% 0.12/0.40 sQ9_spl <=> (white(sK9_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f144,plain,(
% 0.12/0.40 sQ0_spl|sQ9_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f16,f106,f141])).
% 0.12/0.40 fof(f145,definition,(
% 0.12/0.40 sQ10_spl <=> (dirty(sK9_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f148,plain,(
% 0.12/0.40 sQ0_spl|sQ10_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f17,f106,f145])).
% 0.12/0.40 fof(f149,definition,(
% 0.12/0.40 sQ11_spl <=> (old(sK9_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f152,plain,(
% 0.12/0.40 sQ0_spl|sQ11_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f18,f106,f149])).
% 0.12/0.40 fof(f153,definition,(
% 0.12/0.40 sQ12_spl <=> (street(sK8_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f156,plain,(
% 0.12/0.40 sQ0_spl|sQ12_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f19,f106,f153])).
% 0.12/0.40 fof(f157,definition,(
% 0.12/0.40 sQ13_spl <=> (way(sK8_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f160,plain,(
% 0.12/0.40 sQ0_spl|sQ13_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f20,f106,f157])).
% 0.12/0.40 fof(f161,definition,(
% 0.12/0.40 sQ14_spl <=> (lonely(sK8_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f164,plain,(
% 0.12/0.40 sQ0_spl|sQ14_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f21,f106,f161])).
% 0.12/0.40 fof(f165,definition,(
% 0.12/0.40 sQ15_spl <=> (barrel(sK7_skl,sK9_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f166,plain,(
% 0.12/0.40 barrel(sK7_skl,sK9_skl)|~sQ15_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f165])).
% 0.12/0.40 fof(f168,plain,(
% 0.12/0.40 sQ0_spl|sQ15_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f22,f106,f165])).
% 0.12/0.40 fof(f169,definition,(
% 0.12/0.40 sQ16_spl <=> (down(sK7_skl,sK8_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f170,plain,(
% 0.12/0.40 down(sK7_skl,sK8_skl)|~sQ16_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f169])).
% 0.12/0.40 fof(f172,plain,(
% 0.12/0.40 sQ0_spl|sQ16_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f23,f106,f169])).
% 0.12/0.40 fof(f173,definition,(
% 0.12/0.40 sQ17_spl <=> (in(sK7_skl,sK6_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f174,plain,(
% 0.12/0.40 in(sK7_skl,sK6_skl)|~sQ17_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f173])).
% 0.12/0.40 fof(f176,plain,(
% 0.12/0.40 sQ0_spl|sQ17_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f24,f106,f173])).
% 0.12/0.40 fof(f177,definition,(
% 0.12/0.40 sQ18_spl <=> (seat(sK0_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f180,plain,(
% 0.12/0.40 sQ0_spl|sQ18_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f25,f106,f177])).
% 0.12/0.40 fof(f181,definition,(
% 0.12/0.40 sQ19_spl <=> (furniture(sK0_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f184,plain,(
% 0.12/0.40 sQ0_spl|sQ19_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f26,f106,f181])).
% 0.12/0.40 fof(f185,definition,(
% 0.12/0.40 sQ20_spl <=> (front(sK0_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f188,plain,(
% 0.12/0.40 sQ0_spl|sQ20_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f27,f106,f185])).
% 0.12/0.40 fof(f189,definition,(
% 0.12/0.40 sQ21_spl <=> (sK5_skl=sK2_skl)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f191,plain,(
% 0.12/0.40 ~sK5_skl=sK2_skl|sQ21_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f189])).
% 0.12/0.40 fof(f192,plain,(
% 0.12/0.40 sQ0_spl|~sQ21_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f28,f106,f189])).
% 0.12/0.40 fof(f193,definition,(
% 0.12/0.40 sQ22_spl <=> (fellow(sK5_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f194,plain,(
% 0.12/0.40 fellow(sK5_skl)|~sQ22_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f193])).
% 0.12/0.40 fof(f196,plain,(
% 0.12/0.40 sQ0_spl|sQ22_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f29,f106,f193])).
% 0.12/0.40 fof(f197,definition,(
% 0.12/0.40 sQ23_spl <=> (man(sK5_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f198,plain,(
% 0.12/0.40 man(sK5_skl)|~sQ23_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f197])).
% 0.12/0.40 fof(f200,plain,(
% 0.12/0.40 sQ0_spl|sQ23_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f30,f106,f197])).
% 0.12/0.40 fof(f201,definition,(
% 0.12/0.40 sQ24_spl <=> (young(sK5_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f202,plain,(
% 0.12/0.40 young(sK5_skl)|~sQ24_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f201])).
% 0.12/0.40 fof(f204,plain,(
% 0.12/0.40 sQ0_spl|sQ24_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f31,f106,f201])).
% 0.12/0.40 fof(f205,definition,(
% 0.12/0.40 sQ25_spl <=> (fellow(sK2_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f206,plain,(
% 0.12/0.40 fellow(sK2_skl)|~sQ25_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f205])).
% 0.12/0.40 fof(f208,plain,(
% 0.12/0.40 sQ0_spl|sQ25_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f32,f106,f205])).
% 0.12/0.40 fof(f209,definition,(
% 0.12/0.40 sQ26_spl <=> (man(sK2_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f210,plain,(
% 0.12/0.40 man(sK2_skl)|~sQ26_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f209])).
% 0.12/0.40 fof(f212,plain,(
% 0.12/0.40 sQ0_spl|sQ26_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f33,f106,f209])).
% 0.12/0.40 fof(f213,definition,(
% 0.12/0.40 sQ27_spl <=> (young(sK2_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f214,plain,(
% 0.12/0.40 young(sK2_skl)|~sQ27_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f213])).
% 0.12/0.40 fof(f216,plain,(
% 0.12/0.40 sQ0_spl|sQ27_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f34,f106,f213])).
% 0.12/0.40 fof(f217,definition,(
% 0.12/0.40 sQ28_spl <=> (sK5_skl=sK4_skl)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f218,plain,(
% 0.12/0.40 sK5_skl=sK4_skl|~sQ28_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f217])).
% 0.12/0.40 fof(f220,plain,(
% 0.12/0.40 sQ0_spl|sQ28_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f35,f106,f217])).
% 0.12/0.40 fof(f221,definition,(
% 0.12/0.40 sQ29_spl <=> (in(sK4_skl,sK3_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f222,plain,(
% 0.12/0.40 in(sK4_skl,sK3_skl)|~sQ29_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f221])).
% 0.12/0.40 fof(f224,plain,(
% 0.12/0.40 sQ0_spl|sQ29_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f36,f106,f221])).
% 0.12/0.40 fof(f225,definition,(
% 0.12/0.40 sQ30_spl <=> (sK2_skl=sK1_skl)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f226,plain,(
% 0.12/0.40 sK2_skl=sK1_skl|~sQ30_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f225])).
% 0.12/0.40 fof(f228,plain,(
% 0.12/0.40 sQ0_spl|sQ30_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f37,f106,f225])).
% 0.12/0.40 fof(f229,definition,(
% 0.12/0.40 sQ31_spl <=> (in(sK1_skl,sK0_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f230,plain,(
% 0.12/0.40 in(sK1_skl,sK0_skl)|~sQ31_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f229])).
% 0.12/0.40 fof(f232,plain,(
% 0.12/0.40 sQ0_spl|sQ31_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f38,f106,f229])).
% 0.12/0.40 fof(f233,definition,(
% 0.12/0.40 ![X0,X5,X6,X7,X8,X9]: (sQ32_spl <=> (~seat(X0)|~furniture(X0)|~front(X0)|~seat(X5)|~furniture(X5)|~front(X5)|X6=X7|~fellow(X6)|~man(X6)|~young(X6)|~fellow(X7)|~man(X7)|~young(X7)|~X6=X8|~in(X8,X5)|~X7=X9|~in(X9,X0)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f234,plain,(
% 0.12/0.40 ![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,X1)|~X3=X5|~in(X5,X0)|~sQ32_spl)),
% 0.12/0.40 inference(component_clause,[status(thm)],[f233])).
% 0.12/0.40 fof(f236,definition,(
% 0.12/0.40 ![X1,X2,X3,X4]: (sQ33_spl <=> (~hollywood(X1)|~city(X1)|~event(X2)|~chevy(X3)|~car(X3)|~white(X3)|~dirty(X3)|~old(X3)|~street(X4)|~way(X4)|~lonely(X4)|~barrel(X2,X3)|~down(X2,X4)|~in(X2,X1)))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f237,plain,(
% 0.12/0.40 ![X0,X1,X2,X3]: (~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)|~sQ33_spl)),
% 0.12/0.40 inference(component_clause,[status(thm)],[f236])).
% 0.12/0.40 fof(f239,plain,(
% 0.12/0.40 sQ0_spl|sQ32_spl|sQ33_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f39,f106,f233,f236])).
% 0.12/0.40 fof(f240,definition,(
% 0.12/0.40 sQ34_spl <=> (seat(sK10_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f243,plain,(
% 0.12/0.40 ~sQ0_spl|sQ34_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f43,f106,f240])).
% 0.12/0.40 fof(f244,definition,(
% 0.12/0.40 sQ35_spl <=> (furniture(sK10_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f247,plain,(
% 0.12/0.40 ~sQ0_spl|sQ35_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f44,f106,f244])).
% 0.12/0.40 fof(f248,definition,(
% 0.12/0.40 sQ36_spl <=> (front(sK10_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f251,plain,(
% 0.12/0.40 ~sQ0_spl|sQ36_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f45,f106,f248])).
% 0.12/0.40 fof(f252,definition,(
% 0.12/0.40 sQ37_spl <=> (hollywood(sK16_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f255,plain,(
% 0.12/0.40 ~sQ0_spl|sQ37_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f46,f106,f252])).
% 0.12/0.40 fof(f256,definition,(
% 0.12/0.40 sQ38_spl <=> (city(sK16_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f259,plain,(
% 0.12/0.40 ~sQ0_spl|sQ38_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f47,f106,f256])).
% 0.12/0.40 fof(f260,definition,(
% 0.12/0.40 sQ39_spl <=> (event(sK17_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f263,plain,(
% 0.12/0.40 ~sQ0_spl|sQ39_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f48,f106,f260])).
% 0.12/0.40 fof(f264,definition,(
% 0.12/0.40 sQ40_spl <=> (chevy(sK19_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f267,plain,(
% 0.12/0.40 ~sQ0_spl|sQ40_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f49,f106,f264])).
% 0.12/0.40 fof(f268,definition,(
% 0.12/0.40 sQ41_spl <=> (car(sK19_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f271,plain,(
% 0.12/0.40 ~sQ0_spl|sQ41_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f50,f106,f268])).
% 0.12/0.40 fof(f272,definition,(
% 0.12/0.40 sQ42_spl <=> (white(sK19_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f275,plain,(
% 0.12/0.40 ~sQ0_spl|sQ42_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f51,f106,f272])).
% 0.12/0.40 fof(f276,definition,(
% 0.12/0.40 sQ43_spl <=> (dirty(sK19_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f279,plain,(
% 0.12/0.40 ~sQ0_spl|sQ43_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f52,f106,f276])).
% 0.12/0.40 fof(f280,definition,(
% 0.12/0.40 sQ44_spl <=> (old(sK19_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f283,plain,(
% 0.12/0.40 ~sQ0_spl|sQ44_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f53,f106,f280])).
% 0.12/0.40 fof(f284,definition,(
% 0.12/0.40 sQ45_spl <=> (street(sK18_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f287,plain,(
% 0.12/0.40 ~sQ0_spl|sQ45_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f54,f106,f284])).
% 0.12/0.40 fof(f288,definition,(
% 0.12/0.40 sQ46_spl <=> (way(sK18_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f291,plain,(
% 0.12/0.40 ~sQ0_spl|sQ46_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f55,f106,f288])).
% 0.12/0.40 fof(f292,definition,(
% 0.12/0.40 sQ47_spl <=> (lonely(sK18_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f295,plain,(
% 0.12/0.40 ~sQ0_spl|sQ47_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f56,f106,f292])).
% 0.12/0.40 fof(f296,definition,(
% 0.12/0.40 sQ48_spl <=> (barrel(sK17_skl,sK19_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f297,plain,(
% 0.12/0.40 barrel(sK17_skl,sK19_skl)|~sQ48_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f296])).
% 0.12/0.40 fof(f299,plain,(
% 0.12/0.40 ~sQ0_spl|sQ48_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f57,f106,f296])).
% 0.12/0.40 fof(f300,definition,(
% 0.12/0.40 sQ49_spl <=> (down(sK17_skl,sK18_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f301,plain,(
% 0.12/0.40 down(sK17_skl,sK18_skl)|~sQ49_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f300])).
% 0.12/0.40 fof(f303,plain,(
% 0.12/0.40 ~sQ0_spl|sQ49_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f58,f106,f300])).
% 0.12/0.40 fof(f304,definition,(
% 0.12/0.40 sQ50_spl <=> (in(sK17_skl,sK16_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f305,plain,(
% 0.12/0.40 in(sK17_skl,sK16_skl)|~sQ50_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f304])).
% 0.12/0.40 fof(f307,plain,(
% 0.12/0.40 ~sQ0_spl|sQ50_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f59,f106,f304])).
% 0.12/0.40 fof(f308,definition,(
% 0.12/0.40 sQ51_spl <=> (seat(sK13_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f311,plain,(
% 0.12/0.40 ~sQ0_spl|sQ51_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f60,f106,f308])).
% 0.12/0.40 fof(f312,definition,(
% 0.12/0.40 sQ52_spl <=> (furniture(sK13_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f315,plain,(
% 0.12/0.40 ~sQ0_spl|sQ52_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f61,f106,f312])).
% 0.12/0.40 fof(f316,definition,(
% 0.12/0.40 sQ53_spl <=> (front(sK13_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f319,plain,(
% 0.12/0.40 ~sQ0_spl|sQ53_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f62,f106,f316])).
% 0.12/0.40 fof(f320,definition,(
% 0.12/0.40 sQ54_spl <=> (sK15_skl=sK12_skl)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f322,plain,(
% 0.12/0.40 ~sK15_skl=sK12_skl|sQ54_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f320])).
% 0.12/0.40 fof(f323,plain,(
% 0.12/0.40 ~sQ0_spl|~sQ54_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f63,f106,f320])).
% 0.12/0.40 fof(f324,definition,(
% 0.12/0.40 sQ55_spl <=> (fellow(sK15_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f325,plain,(
% 0.12/0.40 fellow(sK15_skl)|~sQ55_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f324])).
% 0.12/0.40 fof(f327,plain,(
% 0.12/0.40 ~sQ0_spl|sQ55_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f64,f106,f324])).
% 0.12/0.40 fof(f328,definition,(
% 0.12/0.40 sQ56_spl <=> (man(sK15_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f329,plain,(
% 0.12/0.40 man(sK15_skl)|~sQ56_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f328])).
% 0.12/0.40 fof(f331,plain,(
% 0.12/0.40 ~sQ0_spl|sQ56_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f65,f106,f328])).
% 0.12/0.40 fof(f332,definition,(
% 0.12/0.40 sQ57_spl <=> (young(sK15_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f333,plain,(
% 0.12/0.40 young(sK15_skl)|~sQ57_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f332])).
% 0.12/0.40 fof(f335,plain,(
% 0.12/0.40 ~sQ0_spl|sQ57_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f66,f106,f332])).
% 0.12/0.40 fof(f336,definition,(
% 0.12/0.40 sQ58_spl <=> (fellow(sK12_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f337,plain,(
% 0.12/0.40 fellow(sK12_skl)|~sQ58_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f336])).
% 0.12/0.40 fof(f339,plain,(
% 0.12/0.40 ~sQ0_spl|sQ58_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f67,f106,f336])).
% 0.12/0.40 fof(f340,definition,(
% 0.12/0.40 sQ59_spl <=> (man(sK12_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f341,plain,(
% 0.12/0.40 man(sK12_skl)|~sQ59_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f340])).
% 0.12/0.40 fof(f343,plain,(
% 0.12/0.40 ~sQ0_spl|sQ59_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f68,f106,f340])).
% 0.12/0.40 fof(f344,definition,(
% 0.12/0.40 sQ60_spl <=> (young(sK12_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f345,plain,(
% 0.12/0.40 young(sK12_skl)|~sQ60_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f344])).
% 0.12/0.40 fof(f347,plain,(
% 0.12/0.40 ~sQ0_spl|sQ60_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f69,f106,f344])).
% 0.12/0.40 fof(f348,definition,(
% 0.12/0.40 sQ61_spl <=> (sK15_skl=sK14_skl)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f349,plain,(
% 0.12/0.40 sK15_skl=sK14_skl|~sQ61_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f348])).
% 0.12/0.40 fof(f351,plain,(
% 0.12/0.40 ~sQ0_spl|sQ61_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f70,f106,f348])).
% 0.12/0.40 fof(f352,definition,(
% 0.12/0.40 sQ62_spl <=> (in(sK14_skl,sK13_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f353,plain,(
% 0.12/0.40 in(sK14_skl,sK13_skl)|~sQ62_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f352])).
% 0.12/0.40 fof(f355,plain,(
% 0.12/0.40 ~sQ0_spl|sQ62_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f71,f106,f352])).
% 0.12/0.40 fof(f356,definition,(
% 0.12/0.40 sQ63_spl <=> (sK12_skl=sK11_skl)),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f357,plain,(
% 0.12/0.40 sK12_skl=sK11_skl|~sQ63_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f356])).
% 0.12/0.40 fof(f359,plain,(
% 0.12/0.40 ~sQ0_spl|sQ63_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f72,f106,f356])).
% 0.12/0.40 fof(f360,definition,(
% 0.12/0.40 sQ64_spl <=> (in(sK11_skl,sK10_skl))),
% 0.12/0.40 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.12/0.40 fof(f361,plain,(
% 0.12/0.40 in(sK11_skl,sK10_skl)|~sQ64_spl),
% 0.12/0.40 inference(component_clause,[status(thm)],[f360])).
% 0.12/0.40 fof(f363,plain,(
% 0.12/0.40 ~sQ0_spl|sQ64_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f73,f106,f360])).
% 0.12/0.40 fof(f364,plain,(
% 0.12/0.40 ~sQ0_spl|sQ32_spl|sQ33_spl),
% 0.12/0.40 inference(split_clause,[status(thm)],[f74,f106,f233,f236])).
% 0.12/0.40 fof(f489,plain,(
% 0.12/0.40 young(sK11_skl)|~sQ63_spl|~sQ60_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f357,f345])).
% 0.12/0.40 fof(f490,plain,(
% 0.12/0.40 man(sK11_skl)|~sQ63_spl|~sQ59_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f357,f341])).
% 0.12/0.40 fof(f491,plain,(
% 0.12/0.40 fellow(sK11_skl)|~sQ63_spl|~sQ58_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f357,f337])).
% 0.12/0.40 fof(f492,plain,(
% 0.12/0.40 young(sK14_skl)|~sQ61_spl|~sQ57_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f349,f333])).
% 0.12/0.40 fof(f493,plain,(
% 0.12/0.40 man(sK14_skl)|~sQ61_spl|~sQ56_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f349,f329])).
% 0.12/0.40 fof(f494,plain,(
% 0.12/0.40 fellow(sK14_skl)|~sQ61_spl|~sQ55_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f349,f325])).
% 0.12/0.40 fof(f495,plain,(
% 0.12/0.40 ~sK14_skl=sK12_skl|~sQ61_spl|sQ54_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f349,f322])).
% 0.12/0.40 fof(f496,plain,(
% 0.12/0.40 ~sK14_skl=sK11_skl|~sQ63_spl|~sQ61_spl|sQ54_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f357,f495])).
% 0.12/0.40 fof(f497,plain,(
% 0.12/0.40 young(sK1_skl)|~sQ30_spl|~sQ27_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f226,f214])).
% 0.12/0.40 fof(f498,plain,(
% 0.12/0.40 man(sK1_skl)|~sQ30_spl|~sQ26_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f226,f210])).
% 0.12/0.40 fof(f499,plain,(
% 0.12/0.40 fellow(sK1_skl)|~sQ30_spl|~sQ25_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f226,f206])).
% 0.12/0.40 fof(f500,plain,(
% 0.12/0.40 young(sK4_skl)|~sQ28_spl|~sQ24_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f218,f202])).
% 0.12/0.40 fof(f501,plain,(
% 0.12/0.40 man(sK4_skl)|~sQ28_spl|~sQ23_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f218,f198])).
% 0.12/0.40 fof(f502,plain,(
% 0.12/0.40 fellow(sK4_skl)|~sQ28_spl|~sQ22_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f218,f194])).
% 0.12/0.40 fof(f503,plain,(
% 0.12/0.40 ~sK4_skl=sK2_skl|~sQ28_spl|sQ21_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f218,f191])).
% 0.12/0.40 fof(f504,plain,(
% 0.12/0.40 ~sK4_skl=sK1_skl|~sQ30_spl|~sQ28_spl|sQ21_spl),
% 0.12/0.40 inference(forward_demodulation,[status(thm)],[f226,f503])).
% 0.12/0.40 fof(f505,plain,(
% 0.12/0.40 ![X0,X1]: (~hollywood(X0)|~city(X0)|~event(sK17_skl)|~chevy(sK19_skl)|~car(sK19_skl)|~white(sK19_skl)|~dirty(sK19_skl)|~old(sK19_skl)|~street(X1)|~way(X1)|~lonely(X1)|~down(sK17_skl,X1)|~in(sK17_skl,X0)|~sQ48_spl|~sQ33_spl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f297,f237])).
% 0.12/0.41 fof(f506,definition,(
% 0.12/0.41 ![X0]: (sQ96_spl <=> (~hollywood(X0)|~city(X0)|~in(sK17_skl,X0)))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f507,plain,(
% 0.12/0.41 ![X0]: (~hollywood(X0)|~city(X0)|~in(sK17_skl,X0)|~sQ96_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f506])).
% 0.12/0.41 fof(f509,definition,(
% 0.12/0.41 ![X1]: (sQ97_spl <=> (~street(X1)|~way(X1)|~lonely(X1)|~down(sK17_skl,X1)))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f510,plain,(
% 0.12/0.41 ![X0]: (~street(X0)|~way(X0)|~lonely(X0)|~down(sK17_skl,X0)|~sQ97_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f509])).
% 0.12/0.41 fof(f512,plain,(
% 0.12/0.41 sQ96_spl|~sQ39_spl|~sQ40_spl|~sQ41_spl|~sQ42_spl|~sQ43_spl|~sQ44_spl|sQ97_spl|~sQ48_spl|~sQ33_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f505,f506,f260,f264,f268,f272,f276,f280,f509,f296,f236])).
% 0.12/0.41 fof(f513,plain,(
% 0.12/0.41 ![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,X1)|~in(X3,X0)|~sQ32_spl)),
% 0.12/0.41 inference(destructive_equality_resolution,[status(thm)],[f234])).
% 0.12/0.41 fof(f516,plain,(
% 0.12/0.41 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|~seat(sK0_skl)|~furniture(sK0_skl)|~front(sK0_skl)|sK1_skl=X1|~fellow(sK1_skl)|~man(sK1_skl)|~young(sK1_skl)|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)|~sQ32_spl|~sQ31_spl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f513,f230])).
% 0.12/0.41 fof(f519,plain,(
% 0.12/0.41 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|~seat(sK10_skl)|~furniture(sK10_skl)|~front(sK10_skl)|sK11_skl=X1|~fellow(sK11_skl)|~man(sK11_skl)|~young(sK11_skl)|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)|~sQ32_spl|~sQ64_spl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f513,f361])).
% 0.12/0.41 fof(f545,definition,(
% 0.12/0.41 sQ106_spl <=> (fellow(sK4_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ106_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f547,plain,(
% 0.12/0.41 ~fellow(sK4_skl)|sQ106_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f545])).
% 0.12/0.41 fof(f548,definition,(
% 0.12/0.41 sQ107_spl <=> (man(sK4_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f550,plain,(
% 0.12/0.41 ~man(sK4_skl)|sQ107_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f548])).
% 0.12/0.41 fof(f551,definition,(
% 0.12/0.41 sQ108_spl <=> (young(sK4_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ108_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f553,plain,(
% 0.12/0.41 ~young(sK4_skl)|sQ108_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f551])).
% 0.12/0.41 fof(f555,definition,(
% 0.12/0.41 ![X0,X1]: (sQ109_spl <=> (~seat(X0)|~furniture(X0)|~front(X0)|sK1_skl=X1|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ109_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f556,plain,(
% 0.12/0.41 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|sK1_skl=X1|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)|~sQ109_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f555])).
% 0.12/0.41 fof(f558,definition,(
% 0.12/0.41 sQ110_spl <=> (fellow(sK1_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ110_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f560,plain,(
% 0.12/0.41 ~fellow(sK1_skl)|sQ110_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f558])).
% 0.12/0.41 fof(f561,definition,(
% 0.12/0.41 sQ111_spl <=> (man(sK1_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f563,plain,(
% 0.12/0.41 ~man(sK1_skl)|sQ111_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f561])).
% 0.12/0.41 fof(f564,definition,(
% 0.12/0.41 sQ112_spl <=> (young(sK1_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ112_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f566,plain,(
% 0.12/0.41 ~young(sK1_skl)|sQ112_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f564])).
% 0.12/0.41 fof(f567,plain,(
% 0.12/0.41 sQ109_spl|~sQ18_spl|~sQ19_spl|~sQ20_spl|~sQ110_spl|~sQ111_spl|~sQ112_spl|~sQ32_spl|~sQ31_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f516,f555,f177,f181,f185,f558,f561,f564,f233,f229])).
% 0.12/0.41 fof(f593,definition,(
% 0.12/0.41 sQ121_spl <=> (fellow(sK14_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f595,plain,(
% 0.12/0.41 ~fellow(sK14_skl)|sQ121_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f593])).
% 0.12/0.41 fof(f596,definition,(
% 0.12/0.41 sQ122_spl <=> (man(sK14_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ122_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f598,plain,(
% 0.12/0.41 ~man(sK14_skl)|sQ122_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f596])).
% 0.12/0.41 fof(f599,definition,(
% 0.12/0.41 sQ123_spl <=> (young(sK14_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ123_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f601,plain,(
% 0.12/0.41 ~young(sK14_skl)|sQ123_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f599])).
% 0.12/0.41 fof(f603,definition,(
% 0.12/0.41 ![X0,X1]: (sQ124_spl <=> (~seat(X0)|~furniture(X0)|~front(X0)|sK11_skl=X1|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ124_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f604,plain,(
% 0.12/0.41 ![X0,X1]: (~seat(X0)|~furniture(X0)|~front(X0)|sK11_skl=X1|~fellow(X1)|~man(X1)|~young(X1)|~in(X1,X0)|~sQ124_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f603])).
% 0.12/0.41 fof(f606,definition,(
% 0.12/0.41 sQ125_spl <=> (fellow(sK11_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ125_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f608,plain,(
% 0.12/0.41 ~fellow(sK11_skl)|sQ125_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f606])).
% 0.12/0.41 fof(f609,definition,(
% 0.12/0.41 sQ126_spl <=> (man(sK11_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ126_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f611,plain,(
% 0.12/0.41 ~man(sK11_skl)|sQ126_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f609])).
% 0.12/0.41 fof(f612,definition,(
% 0.12/0.41 sQ127_spl <=> (young(sK11_skl))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ127_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f614,plain,(
% 0.12/0.41 ~young(sK11_skl)|sQ127_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f612])).
% 0.12/0.41 fof(f615,plain,(
% 0.12/0.41 sQ124_spl|~sQ34_spl|~sQ35_spl|~sQ36_spl|~sQ125_spl|~sQ126_spl|~sQ127_spl|~sQ32_spl|~sQ64_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f519,f603,f240,f244,f248,f606,f609,f612,f233,f360])).
% 0.12/0.41 fof(f616,plain,(
% 0.12/0.41 $false|~sQ63_spl|~sQ60_spl|sQ127_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f614,f489])).
% 0.12/0.41 fof(f617,plain,(
% 0.12/0.41 ~sQ63_spl|~sQ60_spl|sQ127_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f616])).
% 0.12/0.41 fof(f618,plain,(
% 0.12/0.41 $false|~sQ63_spl|~sQ59_spl|sQ126_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f611,f490])).
% 0.12/0.41 fof(f619,plain,(
% 0.12/0.41 ~sQ63_spl|~sQ59_spl|sQ126_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f618])).
% 0.12/0.41 fof(f620,plain,(
% 0.12/0.41 $false|~sQ63_spl|~sQ58_spl|sQ125_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f608,f491])).
% 0.12/0.41 fof(f621,plain,(
% 0.12/0.41 ~sQ63_spl|~sQ58_spl|sQ125_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f620])).
% 0.12/0.41 fof(f624,plain,(
% 0.12/0.41 ~hollywood(sK16_skl)|~city(sK16_skl)|~sQ96_spl|~sQ50_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f507,f305])).
% 0.12/0.41 fof(f625,plain,(
% 0.12/0.41 ~sQ37_spl|~sQ38_spl|~sQ96_spl|~sQ50_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f624,f252,f256,f506,f304])).
% 0.12/0.41 fof(f626,plain,(
% 0.12/0.41 ~street(sK18_skl)|~way(sK18_skl)|~lonely(sK18_skl)|~sQ97_spl|~sQ49_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f510,f301])).
% 0.12/0.41 fof(f627,plain,(
% 0.12/0.41 ~sQ45_spl|~sQ46_spl|~sQ47_spl|~sQ97_spl|~sQ49_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f626,f284,f288,f292,f509,f300])).
% 0.12/0.41 fof(f636,plain,(
% 0.12/0.41 $false|~sQ61_spl|~sQ57_spl|sQ123_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f601,f492])).
% 0.12/0.41 fof(f637,plain,(
% 0.12/0.41 ~sQ61_spl|~sQ57_spl|sQ123_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f636])).
% 0.12/0.41 fof(f638,plain,(
% 0.12/0.41 $false|~sQ61_spl|~sQ56_spl|sQ122_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f598,f493])).
% 0.12/0.41 fof(f639,plain,(
% 0.12/0.41 ~sQ61_spl|~sQ56_spl|sQ122_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f638])).
% 0.12/0.41 fof(f640,plain,(
% 0.12/0.41 $false|~sQ61_spl|~sQ55_spl|sQ121_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f595,f494])).
% 0.12/0.41 fof(f641,plain,(
% 0.12/0.41 ~sQ61_spl|~sQ55_spl|sQ121_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f640])).
% 0.12/0.41 fof(f642,plain,(
% 0.12/0.41 $false|~sQ30_spl|~sQ27_spl|sQ112_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f566,f497])).
% 0.12/0.41 fof(f643,plain,(
% 0.12/0.41 ~sQ30_spl|~sQ27_spl|sQ112_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f642])).
% 0.12/0.41 fof(f644,plain,(
% 0.12/0.41 $false|~sQ28_spl|~sQ24_spl|sQ108_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f553,f500])).
% 0.12/0.41 fof(f645,plain,(
% 0.12/0.41 ~sQ28_spl|~sQ24_spl|sQ108_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f644])).
% 0.12/0.41 fof(f646,plain,(
% 0.12/0.41 $false|~sQ28_spl|~sQ23_spl|sQ107_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f550,f501])).
% 0.12/0.41 fof(f647,plain,(
% 0.12/0.41 ~sQ28_spl|~sQ23_spl|sQ107_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f646])).
% 0.12/0.41 fof(f655,plain,(
% 0.12/0.41 ~seat(sK13_skl)|~furniture(sK13_skl)|~front(sK13_skl)|sK11_skl=sK14_skl|~fellow(sK14_skl)|~man(sK14_skl)|~young(sK14_skl)|~sQ124_spl|~sQ62_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f604,f353])).
% 0.12/0.41 fof(f661,definition,(
% 0.12/0.41 sQ129_spl <=> (sK11_skl=sK14_skl)),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f662,plain,(
% 0.12/0.41 sK11_skl=sK14_skl|~sQ129_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f661])).
% 0.12/0.41 fof(f664,plain,(
% 0.12/0.41 ~sQ51_spl|~sQ52_spl|~sQ53_spl|sQ129_spl|~sQ121_spl|~sQ122_spl|~sQ123_spl|~sQ124_spl|~sQ62_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f655,f308,f312,f316,f661,f593,f596,f599,f603,f352])).
% 0.12/0.41 fof(f669,plain,(
% 0.12/0.41 $false|~sQ63_spl|~sQ61_spl|sQ54_spl|~sQ129_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f662,f496])).
% 0.12/0.41 fof(f670,plain,(
% 0.12/0.41 ~sQ63_spl|~sQ61_spl|sQ54_spl|~sQ129_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f669])).
% 0.12/0.41 fof(f677,plain,(
% 0.12/0.41 $false|sQ106_spl|~sQ28_spl|~sQ22_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f502,f547])).
% 0.12/0.41 fof(f678,plain,(
% 0.12/0.41 sQ106_spl|~sQ28_spl|~sQ22_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f677])).
% 0.12/0.41 fof(f683,plain,(
% 0.12/0.41 $false|sQ110_spl|~sQ30_spl|~sQ25_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f499,f560])).
% 0.12/0.41 fof(f684,plain,(
% 0.12/0.41 sQ110_spl|~sQ30_spl|~sQ25_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f683])).
% 0.12/0.41 fof(f685,plain,(
% 0.12/0.41 $false|sQ111_spl|~sQ30_spl|~sQ26_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f498,f563])).
% 0.12/0.41 fof(f686,plain,(
% 0.12/0.41 sQ111_spl|~sQ30_spl|~sQ26_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f685])).
% 0.12/0.41 fof(f694,plain,(
% 0.12/0.41 ![X0,X1]: (~hollywood(X0)|~city(X0)|~event(sK7_skl)|~chevy(sK9_skl)|~car(sK9_skl)|~white(sK9_skl)|~dirty(sK9_skl)|~old(sK9_skl)|~street(X1)|~way(X1)|~lonely(X1)|~down(sK7_skl,X1)|~in(sK7_skl,X0)|~sQ33_spl|~sQ15_spl)),
% 0.12/0.41 inference(resolution,[status(thm)],[f237,f166])).
% 0.12/0.41 fof(f695,definition,(
% 0.12/0.41 ![X0]: (sQ131_spl <=> (~hollywood(X0)|~city(X0)|~in(sK7_skl,X0)))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ131_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f696,plain,(
% 0.12/0.41 ![X0]: (~hollywood(X0)|~city(X0)|~in(sK7_skl,X0)|~sQ131_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f695])).
% 0.12/0.41 fof(f698,definition,(
% 0.12/0.41 ![X1]: (sQ132_spl <=> (~street(X1)|~way(X1)|~lonely(X1)|~down(sK7_skl,X1)))),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ132_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f699,plain,(
% 0.12/0.41 ![X0]: (~street(X0)|~way(X0)|~lonely(X0)|~down(sK7_skl,X0)|~sQ132_spl)),
% 0.12/0.41 inference(component_clause,[status(thm)],[f698])).
% 0.12/0.41 fof(f701,plain,(
% 0.12/0.41 sQ131_spl|~sQ6_spl|~sQ7_spl|~sQ8_spl|~sQ9_spl|~sQ10_spl|~sQ11_spl|sQ132_spl|~sQ33_spl|~sQ15_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f694,f695,f129,f133,f137,f141,f145,f149,f698,f236,f165])).
% 0.12/0.41 fof(f702,plain,(
% 0.12/0.41 ~hollywood(sK6_skl)|~city(sK6_skl)|~sQ131_spl|~sQ17_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f696,f174])).
% 0.12/0.41 fof(f703,plain,(
% 0.12/0.41 ~sQ4_spl|~sQ5_spl|~sQ131_spl|~sQ17_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f702,f121,f125,f695,f173])).
% 0.12/0.41 fof(f704,plain,(
% 0.12/0.41 ~street(sK8_skl)|~way(sK8_skl)|~lonely(sK8_skl)|~sQ132_spl|~sQ16_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f699,f170])).
% 0.12/0.41 fof(f705,plain,(
% 0.12/0.41 ~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ132_spl|~sQ16_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f704,f153,f157,f161,f698,f169])).
% 0.12/0.41 fof(f749,plain,(
% 0.12/0.41 ~seat(sK3_skl)|~furniture(sK3_skl)|~front(sK3_skl)|sK1_skl=sK4_skl|~fellow(sK4_skl)|~man(sK4_skl)|~young(sK4_skl)|~sQ109_spl|~sQ29_spl),
% 0.12/0.41 inference(resolution,[status(thm)],[f556,f222])).
% 0.12/0.41 fof(f758,definition,(
% 0.12/0.41 sQ138_spl <=> (sK1_skl=sK4_skl)),
% 0.12/0.41 introduced(definition,[new_symbols(definition,[sQ138_spl])],[split_symbol_definition])).
% 0.12/0.41 fof(f759,plain,(
% 0.12/0.41 sK1_skl=sK4_skl|~sQ138_spl),
% 0.12/0.41 inference(component_clause,[status(thm)],[f758])).
% 0.12/0.41 fof(f761,plain,(
% 0.12/0.41 ~sQ1_spl|~sQ2_spl|~sQ3_spl|sQ138_spl|~sQ106_spl|~sQ107_spl|~sQ108_spl|~sQ109_spl|~sQ29_spl),
% 0.12/0.41 inference(split_clause,[status(thm)],[f749,f109,f113,f117,f758,f545,f548,f551,f555,f221])).
% 0.12/0.41 fof(f762,plain,(
% 0.12/0.41 $false|~sQ30_spl|~sQ28_spl|sQ21_spl|~sQ138_spl),
% 0.12/0.41 inference(forward_subsumption_resolution,[status(thm)],[f759,f504])).
% 0.12/0.41 fof(f763,plain,(
% 0.12/0.41 ~sQ30_spl|~sQ28_spl|sQ21_spl|~sQ138_spl),
% 0.12/0.41 inference(contradiction_clause,[status(thm)],[f762])).
% 0.12/0.41 fof(f764,plain,(
% 0.12/0.41 $false),
% 0.12/0.41 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,f512,f567,f615,f617,f619,f621,f625,f627,f637,f639,f641,f643,f645,f647,f664,f670,f678,f684,f686,f701,f703,f705,f761,f763])).
% 0.12/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.12/0.42 % Elapsed time: 0.056384 seconds
% 0.12/0.42 % CPU time: 0.197407 seconds
% 0.12/0.42 % Total memory used: 88.828 MB
% 0.12/0.42 % Net memory used: 88.607 MB
%------------------------------------------------------------------------------