%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.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 : Fri Sep 25 02:14:24 PM UTC 2026
% Result : Theorem 22.19s 3.41s
% Output : Proof 22.19s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP001+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n003.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 01:37:21 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.19/3.41 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.19/3.41 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.19/3.41 fof(sdef30, definition, (spl30 <=> (~city(sk0))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 22.19/3.41 cnf(p256, plain, (~city(sk0) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 22.19/3.41 fof(sdef16, definition, (spl16 <=> (city(sk0))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 22.19/3.41 cnf(p32, plain, (city(sk0) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 22.19/3.41 cnf(p265, plain, ($false | ~spl16 | ~spl30), inference(resolution, [status(thm)], [p256, p32])).
% 22.19/3.41 cnf(sct0, plain, (~spl16 | ~spl30), inference(avatar_contradiction_clause, [status(thm)], [p265])).
% 22.19/3.41 fof(sdef32, definition, (spl32 <=> (~city(sk4))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 22.19/3.41 cnf(p259, plain, (~city(sk4) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 22.19/3.41 fof(sdef2, definition, (spl2 <=> (city(sk4))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 22.19/3.41 cnf(p4, plain, (city(sk4) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 22.19/3.41 cnf(p266, plain, ($false | ~spl2 | ~spl32), inference(resolution, [status(thm)], [p259, p4])).
% 22.19/3.41 cnf(sct1, plain, (~spl2 | ~spl32), inference(avatar_contradiction_clause, [status(thm)], [p266])).
% 22.19/3.41 fof(sdef41, definition, (spl41 <=> (~in(sk1,sk0))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 22.19/3.41 cnf(p274, plain, (~in(sk1,sk0) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 22.19/3.41 fof(sdef28, definition, (spl28 <=> (in(sk1,sk0))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 22.19/3.41 cnf(p224, plain, (in(sk1,sk0) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 22.19/3.41 cnf(p279, plain, ($false | ~spl28 | ~spl41), inference(resolution, [status(thm)], [p274, p224])).
% 22.19/3.41 cnf(sct2, plain, (~spl28 | ~spl41), inference(avatar_contradiction_clause, [status(thm)], [p279])).
% 22.19/3.41 fof(sdef42, definition, (spl42 <=> (~in(sk5,sk4))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 22.19/3.41 cnf(p276, plain, (~in(sk5,sk4) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 22.19/3.41 fof(sdef14, definition, (spl14 <=> (in(sk5,sk4))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 22.19/3.41 cnf(p28, plain, (in(sk5,sk4) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 22.19/3.41 cnf(p280, plain, ($false | ~spl14 | ~spl42), inference(resolution, [status(thm)], [p276, p28])).
% 22.19/3.41 cnf(sct3, plain, (~spl14 | ~spl42), inference(avatar_contradiction_clause, [status(thm)], [p280])).
% 22.19/3.41 fof(sdef44, definition, (spl44 <=> (~way(sk7))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 22.19/3.41 cnf(p282, plain, (~way(sk7) | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 22.19/3.41 fof(sdef10, definition, (spl10 <=> (way(sk7))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 22.19/3.41 cnf(p20, plain, (way(sk7) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 22.19/3.41 cnf(p290, plain, ($false | ~spl10 | ~spl44), inference(resolution, [status(thm)], [p282, p20])).
% 22.19/3.41 cnf(sct4, plain, (~spl10 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p290])).
% 22.19/3.41 fof(sdef45, definition, (spl45 <=> (~lonely(sk7))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 22.19/3.41 cnf(p283, plain, (~lonely(sk7) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 22.19/3.41 fof(sdef11, definition, (spl11 <=> (lonely(sk7))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 22.19/3.41 cnf(p22, plain, (lonely(sk7) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 22.19/3.41 cnf(p291, plain, ($false | ~spl11 | ~spl45), inference(resolution, [status(thm)], [p283, p22])).
% 22.19/3.41 cnf(sct5, plain, (~spl11 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p291])).
% 22.19/3.41 fof(sdef47, definition, (spl47 <=> (~way(sk2))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 22.19/3.41 cnf(p286, plain, (~way(sk2) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 22.19/3.41 fof(sdef19, definition, (spl19 <=> (way(sk2))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 22.19/3.41 cnf(p80, plain, (way(sk2) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 22.19/3.41 cnf(p292, plain, ($false | ~spl19 | ~spl47), inference(resolution, [status(thm)], [p286, p80])).
% 22.19/3.41 cnf(sct6, plain, (~spl19 | ~spl47), inference(avatar_contradiction_clause, [status(thm)], [p292])).
% 22.19/3.41 fof(sdef48, definition, (spl48 <=> (~lonely(sk2))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 22.19/3.41 cnf(p287, plain, (~lonely(sk2) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 22.19/3.41 fof(sdef20, definition, (spl20 <=> (lonely(sk2))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 22.19/3.41 cnf(p96, plain, (lonely(sk2) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 22.19/3.41 cnf(p293, plain, ($false | ~spl20 | ~spl48), inference(resolution, [status(thm)], [p287, p96])).
% 22.19/3.41 cnf(sct7, plain, (~spl20 | ~spl48), inference(avatar_contradiction_clause, [status(thm)], [p293])).
% 22.19/3.41 fof(sdef46, definition, (spl46 <=> (~down(sk5,sk7))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 22.19/3.41 cnf(p284, plain, (~down(sk5,sk7) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 22.19/3.41 fof(sdef13, definition, (spl13 <=> (down(sk5,sk7))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 22.19/3.41 cnf(p26, plain, (down(sk5,sk7) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 22.19/3.41 cnf(p295, plain, ($false | ~spl13 | ~spl46), inference(resolution, [status(thm)], [p284, p26])).
% 22.19/3.41 cnf(sct8, plain, (~spl13 | ~spl46), inference(avatar_contradiction_clause, [status(thm)], [p295])).
% 22.19/3.41 fof(sdef52, definition, (spl52 <=> (~car(sk6))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 22.19/3.41 cnf(p301, plain, (~car(sk6) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 22.19/3.41 fof(sdef5, definition, (spl5 <=> (car(sk6))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 22.19/3.41 cnf(p10, plain, (car(sk6) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 22.19/3.41 cnf(p312, plain, ($false | ~spl5 | ~spl52), inference(resolution, [status(thm)], [p301, p10])).
% 22.19/3.41 cnf(sct9, plain, (~spl5 | ~spl52), inference(avatar_contradiction_clause, [status(thm)], [p312])).
% 22.19/3.41 fof(sdef53, definition, (spl53 <=> (~white(sk6))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 22.19/3.41 cnf(p302, plain, (~white(sk6) | ~spl53), inference(avatar_component_clause, [status(thm)], [sdef53])).
% 22.19/3.41 fof(sdef6, definition, (spl6 <=> (white(sk6))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 22.19/3.41 cnf(p12, plain, (white(sk6) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 22.19/3.41 cnf(p313, plain, ($false | ~spl6 | ~spl53), inference(resolution, [status(thm)], [p302, p12])).
% 22.19/3.41 cnf(sct10, plain, (~spl6 | ~spl53), inference(avatar_contradiction_clause, [status(thm)], [p313])).
% 22.19/3.41 fof(sdef54, definition, (spl54 <=> (~dirty(sk6))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 22.19/3.41 cnf(p303, plain, (~dirty(sk6) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 22.19/3.41 fof(sdef7, definition, (spl7 <=> (dirty(sk6))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 22.19/3.41 cnf(p14, plain, (dirty(sk6) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 22.19/3.41 cnf(p314, plain, ($false | ~spl7 | ~spl54), inference(resolution, [status(thm)], [p303, p14])).
% 22.19/3.41 cnf(sct11, plain, (~spl7 | ~spl54), inference(avatar_contradiction_clause, [status(thm)], [p314])).
% 22.19/3.41 fof(sdef55, definition, (spl55 <=> (~old(sk6))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 22.19/3.41 cnf(p304, plain, (~old(sk6) | ~spl55), inference(avatar_component_clause, [status(thm)], [sdef55])).
% 22.19/3.41 fof(sdef8, definition, (spl8 <=> (old(sk6))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 22.19/3.41 cnf(p16, plain, (old(sk6) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 22.19/3.41 cnf(p315, plain, ($false | ~spl8 | ~spl55), inference(resolution, [status(thm)], [p304, p16])).
% 22.19/3.41 cnf(sct12, plain, (~spl8 | ~spl55), inference(avatar_contradiction_clause, [status(thm)], [p315])).
% 22.19/3.41 fof(sdef57, definition, (spl57 <=> (~car(sk3))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 22.19/3.41 cnf(p307, plain, (~car(sk3) | ~spl57), inference(avatar_component_clause, [status(thm)], [sdef57])).
% 22.19/3.41 fof(sdef22, definition, (spl22 <=> (car(sk3))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 22.19/3.41 cnf(p128, plain, (car(sk3) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 22.19/3.41 cnf(p318, plain, ($false | ~spl22 | ~spl57), inference(resolution, [status(thm)], [p307, p128])).
% 22.19/3.41 cnf(sct13, plain, (~spl22 | ~spl57), inference(avatar_contradiction_clause, [status(thm)], [p318])).
% 22.19/3.41 fof(sdef58, definition, (spl58 <=> (~white(sk3))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 22.19/3.41 cnf(p308, plain, (~white(sk3) | ~spl58), inference(avatar_component_clause, [status(thm)], [sdef58])).
% 22.19/3.41 fof(sdef23, definition, (spl23 <=> (white(sk3))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 22.19/3.41 cnf(p144, plain, (white(sk3) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 22.19/3.41 cnf(p319, plain, ($false | ~spl23 | ~spl58), inference(resolution, [status(thm)], [p308, p144])).
% 22.19/3.41 cnf(sct14, plain, (~spl23 | ~spl58), inference(avatar_contradiction_clause, [status(thm)], [p319])).
% 22.19/3.41 fof(sdef59, definition, (spl59 <=> (~dirty(sk3))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 22.19/3.41 cnf(p309, plain, (~dirty(sk3) | ~spl59), inference(avatar_component_clause, [status(thm)], [sdef59])).
% 22.19/3.41 fof(sdef24, definition, (spl24 <=> (dirty(sk3))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 22.19/3.41 cnf(p160, plain, (dirty(sk3) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 22.19/3.41 cnf(p320, plain, ($false | ~spl24 | ~spl59), inference(resolution, [status(thm)], [p309, p160])).
% 22.19/3.41 cnf(sct15, plain, (~spl24 | ~spl59), inference(avatar_contradiction_clause, [status(thm)], [p320])).
% 22.19/3.41 fof(sdef60, definition, (spl60 <=> (~old(sk3))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 22.19/3.41 cnf(p310, plain, (~old(sk3) | ~spl60), inference(avatar_component_clause, [status(thm)], [sdef60])).
% 22.19/3.41 fof(sdef25, definition, (spl25 <=> (old(sk3))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 22.19/3.41 cnf(p176, plain, (old(sk3) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 22.19/3.41 cnf(p321, plain, ($false | ~spl25 | ~spl60), inference(resolution, [status(thm)], [p310, p176])).
% 22.19/3.41 cnf(sct16, plain, (~spl25 | ~spl60), inference(avatar_contradiction_clause, [status(thm)], [p321])).
% 22.19/3.41 fof(sdef51, definition, (spl51 <=> (~down(sk1,sk2))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 22.19/3.41 cnf(p299, plain, (~down(sk1,sk2) | ~spl51), inference(avatar_component_clause, [status(thm)], [sdef51])).
% 22.19/3.41 fof(sdef27, definition, (spl27 <=> (down(sk1,sk2))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 22.19/3.41 cnf(p208, plain, (down(sk1,sk2) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 22.19/3.41 cnf(p322, plain, ($false | ~spl27 | ~spl51), inference(resolution, [status(thm)], [p299, p208])).
% 22.19/3.41 cnf(sct17, plain, (~spl27 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p322])).
% 22.19/3.41 fof(sdef56, definition, (spl56 <=> (~barrel(sk5,sk6))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 22.19/3.41 cnf(p305, plain, (~barrel(sk5,sk6) | ~spl56), inference(avatar_component_clause, [status(thm)], [sdef56])).
% 22.19/3.41 fof(sdef12, definition, (spl12 <=> (barrel(sk5,sk6))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 22.19/3.41 cnf(p24, plain, (barrel(sk5,sk6) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 22.19/3.41 cnf(p323, plain, ($false | ~spl12 | ~spl56), inference(resolution, [status(thm)], [p305, p24])).
% 22.19/3.41 cnf(sct18, plain, (~spl12 | ~spl56), inference(avatar_contradiction_clause, [status(thm)], [p323])).
% 22.19/3.41 fof(sdef63, definition, (spl63 <=> (~barrel(sk1,sk3))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 22.19/3.41 cnf(p327, plain, (~barrel(sk1,sk3) | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 22.19/3.41 fof(sdef26, definition, (spl26 <=> (barrel(sk1,sk3))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 22.19/3.41 cnf(p192, plain, (barrel(sk1,sk3) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 22.19/3.41 cnf(p328, plain, ($false | ~spl26 | ~spl63), inference(resolution, [status(thm)], [p327, p192])).
% 22.19/3.41 cnf(sct19, plain, (~spl26 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p328])).
% 22.19/3.41 fof(f0, conjecture, ( ( ? [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) ) => ? [Y,Z,X1,X2] : ( hollywood(Y) & city(Y) & event(Z) & chevy(X1) & car(X1) & white(X1) & dirty(X1) & old(X1) & street(X2) & way(X2) & lonely(X2) & barrel(Z,X1) & down(Z,X2) & in(Z,Y) ) ) & ( ? [X3,X4,X5,X6] : ( hollywood(X3) & city(X3) & event(X4) & chevy(X5) & car(X5) & white(X5) & dirty(X5) & old(X5) & street(X6) & way(X6) & lonely(X6) & barrel(X4,X5) & down(X4,X6) & in(X4,X3) ) => ? [X7,X8,X9,X10] : ( hollywood(X7) & city(X7) & event(X8) & street(X9) & way(X9) & lonely(X9) & chevy(X10) & car(X10) & white(X10) & dirty(X10) & old(X10) & barrel(X8,X10) & down(X8,X9) & in(X8,X7) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 22.19/3.41 fof(f0_neg, negated_conjecture, ~(( ( ? [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) ) => ? [Y,Z,X1,X2] : ( hollywood(Y) & city(Y) & event(Z) & chevy(X1) & car(X1) & white(X1) & dirty(X1) & old(X1) & street(X2) & way(X2) & lonely(X2) & barrel(Z,X1) & down(Z,X2) & in(Z,Y) ) ) & ( ? [X3,X4,X5,X6] : ( hollywood(X3) & city(X3) & event(X4) & chevy(X5) & car(X5) & white(X5) & dirty(X5) & old(X5) & street(X6) & way(X6) & lonely(X6) & barrel(X4,X5) & down(X4,X6) & in(X4,X3) ) => ? [X7,X8,X9,X10] : ( hollywood(X7) & city(X7) & event(X8) & street(X9) & way(X9) & lonely(X9) & chevy(X10) & car(X10) & white(X10) & dirty(X10) & old(X10) & barrel(X8,X10) & down(X8,X9) & in(X8,X7) ) ) )), inference(negated_conjecture, [status(cth)], [f0])).
% 22.19/3.41 fof(f0_nnf, plain, ((? [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))) & ! [Y,Z,X1,X2] : ((((((((((((((~(hollywood(Y)) | ~(city(Y))) | ~(event(Z))) | ~(chevy(X1))) | ~(car(X1))) | ~(white(X1))) | ~(dirty(X1))) | ~(old(X1))) | ~(street(X2))) | ~(way(X2))) | ~(lonely(X2))) | ~(barrel(Z,X1))) | ~(down(Z,X2))) | ~(in(Z,Y))))) | (? [X3,X4,X5,X6] : ((((((((((((((hollywood(X3) & city(X3)) & event(X4)) & chevy(X5)) & car(X5)) & white(X5)) & dirty(X5)) & old(X5)) & street(X6)) & way(X6)) & lonely(X6)) & barrel(X4,X5)) & down(X4,X6)) & in(X4,X3))) & ! [X7,X8,X9,X10] : ((((((((((((((~(hollywood(X7)) | ~(city(X7))) | ~(event(X8))) | ~(street(X9))) | ~(way(X9))) | ~(lonely(X9))) | ~(chevy(X10))) | ~(car(X10))) | ~(white(X10))) | ~(dirty(X10))) | ~(old(X10))) | ~(barrel(X8,X10))) | ~(down(X8,X9))) | ~(in(X8,X7)))))), inference(nnf_transformation, [status(thm)], [f0_neg])).
% 22.19/3.41 fof(f0_sk, plain, ! [Y,Z,X1,X2,X7,X8,X9,X10] : ((((((((((((((((hollywood(sk0) & city(sk0)) & event(sk1)) & street(sk2)) & way(sk2)) & lonely(sk2)) & chevy(sk3)) & car(sk3)) & white(sk3)) & dirty(sk3)) & old(sk3)) & barrel(sk1,sk3)) & down(sk1,sk2)) & in(sk1,sk0)) & (((((((((((((~(hollywood(Y)) | ~(city(Y))) | ~(event(Z))) | ~(chevy(X1))) | ~(car(X1))) | ~(white(X1))) | ~(dirty(X1))) | ~(old(X1))) | ~(street(X2))) | ~(way(X2))) | ~(lonely(X2))) | ~(barrel(Z,X1))) | ~(down(Z,X2))) | ~(in(Z,Y)))) | ((((((((((((((hollywood(sk4) & city(sk4)) & event(sk5)) & chevy(sk6)) & car(sk6)) & white(sk6)) & dirty(sk6)) & old(sk6)) & street(sk7)) & way(sk7)) & lonely(sk7)) & barrel(sk5,sk6)) & down(sk5,sk7)) & in(sk5,sk4)) & (((((((((((((~(hollywood(X7)) | ~(city(X7))) | ~(event(X8))) | ~(street(X9))) | ~(way(X9))) | ~(lonely(X9))) | ~(chevy(X10))) | ~(car(X10))) | ~(white(X10))) | ~(dirty(X10))) | ~(old(X10))) | ~(barrel(X8,X10))) | ~(down(X8,X9))) | ~(in(X8,X7)))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7])], [f0_nnf])).
% 22.19/3.41 cnf(c0, plain, hollywood(sk0) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef0, definition, (spl0 <=> (hollywood(sk0))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 22.19/3.41 fof(sdef1, definition, (spl1 <=> (hollywood(sk4))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 22.19/3.41 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c0, sdef0, sdef1])).
% 22.19/3.41 cnf(c1, plain, hollywood(sk0) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp1, plain, (spl0 | spl2), inference(avatar_split_clause, [status(thm)], [c1, sdef0, sdef2])).
% 22.19/3.41 cnf(c2, plain, hollywood(sk0) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef3, definition, (spl3 <=> (event(sk5))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 22.19/3.41 cnf(ssp2, plain, (spl0 | spl3), inference(avatar_split_clause, [status(thm)], [c2, sdef0, sdef3])).
% 22.19/3.41 cnf(c3, plain, hollywood(sk0) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef4, definition, (spl4 <=> (chevy(sk6))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 22.19/3.41 cnf(ssp3, plain, (spl0 | spl4), inference(avatar_split_clause, [status(thm)], [c3, sdef0, sdef4])).
% 22.19/3.41 cnf(c4, plain, hollywood(sk0) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp4, plain, (spl0 | spl5), inference(avatar_split_clause, [status(thm)], [c4, sdef0, sdef5])).
% 22.19/3.41 cnf(c5, plain, hollywood(sk0) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp5, plain, (spl0 | spl6), inference(avatar_split_clause, [status(thm)], [c5, sdef0, sdef6])).
% 22.19/3.41 cnf(c6, plain, hollywood(sk0) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp6, plain, (spl0 | spl7), inference(avatar_split_clause, [status(thm)], [c6, sdef0, sdef7])).
% 22.19/3.41 cnf(c7, plain, hollywood(sk0) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp7, plain, (spl0 | spl8), inference(avatar_split_clause, [status(thm)], [c7, sdef0, sdef8])).
% 22.19/3.41 cnf(c8, plain, hollywood(sk0) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef9, definition, (spl9 <=> (street(sk7))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 22.19/3.41 cnf(ssp8, plain, (spl0 | spl9), inference(avatar_split_clause, [status(thm)], [c8, sdef0, sdef9])).
% 22.19/3.41 cnf(c9, plain, hollywood(sk0) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp9, plain, (spl0 | spl10), inference(avatar_split_clause, [status(thm)], [c9, sdef0, sdef10])).
% 22.19/3.41 cnf(c10, plain, hollywood(sk0) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp10, plain, (spl0 | spl11), inference(avatar_split_clause, [status(thm)], [c10, sdef0, sdef11])).
% 22.19/3.41 cnf(c11, plain, hollywood(sk0) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp11, plain, (spl0 | spl12), inference(avatar_split_clause, [status(thm)], [c11, sdef0, sdef12])).
% 22.19/3.41 cnf(c12, plain, hollywood(sk0) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp12, plain, (spl0 | spl13), inference(avatar_split_clause, [status(thm)], [c12, sdef0, sdef13])).
% 22.19/3.41 cnf(c13, plain, hollywood(sk0) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp13, plain, (spl0 | spl14), inference(avatar_split_clause, [status(thm)], [c13, sdef0, sdef14])).
% 22.19/3.41 cnf(c14, plain, hollywood(sk0) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef15, definition, (spl15 <=> (~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))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 22.19/3.41 cnf(ssp14, plain, (spl0 | spl15), inference(avatar_split_clause, [status(thm)], [c14, sdef0, sdef15])).
% 22.19/3.41 cnf(c15, plain, city(sk0) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp15, plain, (spl1 | spl16), inference(avatar_split_clause, [status(thm)], [c15, sdef1, sdef16])).
% 22.19/3.41 cnf(c16, plain, city(sk0) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp16, plain, (spl2 | spl16), inference(avatar_split_clause, [status(thm)], [c16, sdef2, sdef16])).
% 22.19/3.41 cnf(c17, plain, city(sk0) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp17, plain, (spl3 | spl16), inference(avatar_split_clause, [status(thm)], [c17, sdef3, sdef16])).
% 22.19/3.41 cnf(c18, plain, city(sk0) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp18, plain, (spl4 | spl16), inference(avatar_split_clause, [status(thm)], [c18, sdef4, sdef16])).
% 22.19/3.41 cnf(c19, plain, city(sk0) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp19, plain, (spl5 | spl16), inference(avatar_split_clause, [status(thm)], [c19, sdef5, sdef16])).
% 22.19/3.41 cnf(c20, plain, city(sk0) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp20, plain, (spl6 | spl16), inference(avatar_split_clause, [status(thm)], [c20, sdef6, sdef16])).
% 22.19/3.41 cnf(c21, plain, city(sk0) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp21, plain, (spl7 | spl16), inference(avatar_split_clause, [status(thm)], [c21, sdef7, sdef16])).
% 22.19/3.41 cnf(c22, plain, city(sk0) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp22, plain, (spl8 | spl16), inference(avatar_split_clause, [status(thm)], [c22, sdef8, sdef16])).
% 22.19/3.41 cnf(c23, plain, city(sk0) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp23, plain, (spl9 | spl16), inference(avatar_split_clause, [status(thm)], [c23, sdef9, sdef16])).
% 22.19/3.41 cnf(c24, plain, city(sk0) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp24, plain, (spl10 | spl16), inference(avatar_split_clause, [status(thm)], [c24, sdef10, sdef16])).
% 22.19/3.41 cnf(c25, plain, city(sk0) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp25, plain, (spl11 | spl16), inference(avatar_split_clause, [status(thm)], [c25, sdef11, sdef16])).
% 22.19/3.41 cnf(c26, plain, city(sk0) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp26, plain, (spl12 | spl16), inference(avatar_split_clause, [status(thm)], [c26, sdef12, sdef16])).
% 22.19/3.41 cnf(c27, plain, city(sk0) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp27, plain, (spl13 | spl16), inference(avatar_split_clause, [status(thm)], [c27, sdef13, sdef16])).
% 22.19/3.41 cnf(c28, plain, city(sk0) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp28, plain, (spl14 | spl16), inference(avatar_split_clause, [status(thm)], [c28, sdef14, sdef16])).
% 22.19/3.41 cnf(c29, plain, city(sk0) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp29, plain, (spl15 | spl16), inference(avatar_split_clause, [status(thm)], [c29, sdef15, sdef16])).
% 22.19/3.41 cnf(c30, plain, event(sk1) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef17, definition, (spl17 <=> (event(sk1))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 22.19/3.41 cnf(ssp30, plain, (spl1 | spl17), inference(avatar_split_clause, [status(thm)], [c30, sdef1, sdef17])).
% 22.19/3.41 cnf(c31, plain, event(sk1) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp31, plain, (spl2 | spl17), inference(avatar_split_clause, [status(thm)], [c31, sdef2, sdef17])).
% 22.19/3.41 cnf(c32, plain, event(sk1) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp32, plain, (spl3 | spl17), inference(avatar_split_clause, [status(thm)], [c32, sdef3, sdef17])).
% 22.19/3.41 cnf(c33, plain, event(sk1) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp33, plain, (spl4 | spl17), inference(avatar_split_clause, [status(thm)], [c33, sdef4, sdef17])).
% 22.19/3.41 cnf(c34, plain, event(sk1) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp34, plain, (spl5 | spl17), inference(avatar_split_clause, [status(thm)], [c34, sdef5, sdef17])).
% 22.19/3.41 cnf(c35, plain, event(sk1) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp35, plain, (spl6 | spl17), inference(avatar_split_clause, [status(thm)], [c35, sdef6, sdef17])).
% 22.19/3.41 cnf(c36, plain, event(sk1) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp36, plain, (spl7 | spl17), inference(avatar_split_clause, [status(thm)], [c36, sdef7, sdef17])).
% 22.19/3.41 cnf(c37, plain, event(sk1) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp37, plain, (spl8 | spl17), inference(avatar_split_clause, [status(thm)], [c37, sdef8, sdef17])).
% 22.19/3.41 cnf(c38, plain, event(sk1) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp38, plain, (spl9 | spl17), inference(avatar_split_clause, [status(thm)], [c38, sdef9, sdef17])).
% 22.19/3.41 cnf(c39, plain, event(sk1) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp39, plain, (spl10 | spl17), inference(avatar_split_clause, [status(thm)], [c39, sdef10, sdef17])).
% 22.19/3.41 cnf(c40, plain, event(sk1) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp40, plain, (spl11 | spl17), inference(avatar_split_clause, [status(thm)], [c40, sdef11, sdef17])).
% 22.19/3.41 cnf(c41, plain, event(sk1) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp41, plain, (spl12 | spl17), inference(avatar_split_clause, [status(thm)], [c41, sdef12, sdef17])).
% 22.19/3.41 cnf(c42, plain, event(sk1) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp42, plain, (spl13 | spl17), inference(avatar_split_clause, [status(thm)], [c42, sdef13, sdef17])).
% 22.19/3.41 cnf(c43, plain, event(sk1) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp43, plain, (spl14 | spl17), inference(avatar_split_clause, [status(thm)], [c43, sdef14, sdef17])).
% 22.19/3.41 cnf(c44, plain, event(sk1) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp44, plain, (spl15 | spl17), inference(avatar_split_clause, [status(thm)], [c44, sdef15, sdef17])).
% 22.19/3.41 cnf(c45, plain, street(sk2) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef18, definition, (spl18 <=> (street(sk2))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 22.19/3.41 cnf(ssp45, plain, (spl1 | spl18), inference(avatar_split_clause, [status(thm)], [c45, sdef1, sdef18])).
% 22.19/3.41 cnf(c46, plain, street(sk2) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp46, plain, (spl2 | spl18), inference(avatar_split_clause, [status(thm)], [c46, sdef2, sdef18])).
% 22.19/3.41 cnf(c47, plain, street(sk2) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp47, plain, (spl3 | spl18), inference(avatar_split_clause, [status(thm)], [c47, sdef3, sdef18])).
% 22.19/3.41 cnf(c48, plain, street(sk2) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp48, plain, (spl4 | spl18), inference(avatar_split_clause, [status(thm)], [c48, sdef4, sdef18])).
% 22.19/3.41 cnf(c49, plain, street(sk2) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp49, plain, (spl5 | spl18), inference(avatar_split_clause, [status(thm)], [c49, sdef5, sdef18])).
% 22.19/3.41 cnf(c50, plain, street(sk2) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp50, plain, (spl6 | spl18), inference(avatar_split_clause, [status(thm)], [c50, sdef6, sdef18])).
% 22.19/3.41 cnf(c51, plain, street(sk2) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp51, plain, (spl7 | spl18), inference(avatar_split_clause, [status(thm)], [c51, sdef7, sdef18])).
% 22.19/3.41 cnf(c52, plain, street(sk2) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp52, plain, (spl8 | spl18), inference(avatar_split_clause, [status(thm)], [c52, sdef8, sdef18])).
% 22.19/3.41 cnf(c53, plain, street(sk2) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp53, plain, (spl9 | spl18), inference(avatar_split_clause, [status(thm)], [c53, sdef9, sdef18])).
% 22.19/3.41 cnf(c54, plain, street(sk2) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp54, plain, (spl10 | spl18), inference(avatar_split_clause, [status(thm)], [c54, sdef10, sdef18])).
% 22.19/3.41 cnf(c55, plain, street(sk2) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp55, plain, (spl11 | spl18), inference(avatar_split_clause, [status(thm)], [c55, sdef11, sdef18])).
% 22.19/3.41 cnf(c56, plain, street(sk2) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp56, plain, (spl12 | spl18), inference(avatar_split_clause, [status(thm)], [c56, sdef12, sdef18])).
% 22.19/3.41 cnf(c57, plain, street(sk2) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp57, plain, (spl13 | spl18), inference(avatar_split_clause, [status(thm)], [c57, sdef13, sdef18])).
% 22.19/3.41 cnf(c58, plain, street(sk2) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp58, plain, (spl14 | spl18), inference(avatar_split_clause, [status(thm)], [c58, sdef14, sdef18])).
% 22.19/3.41 cnf(c59, plain, street(sk2) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp59, plain, (spl15 | spl18), inference(avatar_split_clause, [status(thm)], [c59, sdef15, sdef18])).
% 22.19/3.41 cnf(c60, plain, way(sk2) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp60, plain, (spl1 | spl19), inference(avatar_split_clause, [status(thm)], [c60, sdef1, sdef19])).
% 22.19/3.41 cnf(c61, plain, way(sk2) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp61, plain, (spl2 | spl19), inference(avatar_split_clause, [status(thm)], [c61, sdef2, sdef19])).
% 22.19/3.41 cnf(c62, plain, way(sk2) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp62, plain, (spl3 | spl19), inference(avatar_split_clause, [status(thm)], [c62, sdef3, sdef19])).
% 22.19/3.41 cnf(c63, plain, way(sk2) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp63, plain, (spl4 | spl19), inference(avatar_split_clause, [status(thm)], [c63, sdef4, sdef19])).
% 22.19/3.41 cnf(c64, plain, way(sk2) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp64, plain, (spl5 | spl19), inference(avatar_split_clause, [status(thm)], [c64, sdef5, sdef19])).
% 22.19/3.41 cnf(c65, plain, way(sk2) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp65, plain, (spl6 | spl19), inference(avatar_split_clause, [status(thm)], [c65, sdef6, sdef19])).
% 22.19/3.41 cnf(c66, plain, way(sk2) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp66, plain, (spl7 | spl19), inference(avatar_split_clause, [status(thm)], [c66, sdef7, sdef19])).
% 22.19/3.41 cnf(c67, plain, way(sk2) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp67, plain, (spl8 | spl19), inference(avatar_split_clause, [status(thm)], [c67, sdef8, sdef19])).
% 22.19/3.41 cnf(c68, plain, way(sk2) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp68, plain, (spl9 | spl19), inference(avatar_split_clause, [status(thm)], [c68, sdef9, sdef19])).
% 22.19/3.41 cnf(c69, plain, way(sk2) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp69, plain, (spl10 | spl19), inference(avatar_split_clause, [status(thm)], [c69, sdef10, sdef19])).
% 22.19/3.41 cnf(c70, plain, way(sk2) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp70, plain, (spl11 | spl19), inference(avatar_split_clause, [status(thm)], [c70, sdef11, sdef19])).
% 22.19/3.41 cnf(c71, plain, way(sk2) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp71, plain, (spl12 | spl19), inference(avatar_split_clause, [status(thm)], [c71, sdef12, sdef19])).
% 22.19/3.41 cnf(c72, plain, way(sk2) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp72, plain, (spl13 | spl19), inference(avatar_split_clause, [status(thm)], [c72, sdef13, sdef19])).
% 22.19/3.41 cnf(c73, plain, way(sk2) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp73, plain, (spl14 | spl19), inference(avatar_split_clause, [status(thm)], [c73, sdef14, sdef19])).
% 22.19/3.41 cnf(c74, plain, way(sk2) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp74, plain, (spl15 | spl19), inference(avatar_split_clause, [status(thm)], [c74, sdef15, sdef19])).
% 22.19/3.41 cnf(c75, plain, lonely(sk2) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp75, plain, (spl1 | spl20), inference(avatar_split_clause, [status(thm)], [c75, sdef1, sdef20])).
% 22.19/3.41 cnf(c76, plain, lonely(sk2) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp76, plain, (spl2 | spl20), inference(avatar_split_clause, [status(thm)], [c76, sdef2, sdef20])).
% 22.19/3.41 cnf(c77, plain, lonely(sk2) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp77, plain, (spl3 | spl20), inference(avatar_split_clause, [status(thm)], [c77, sdef3, sdef20])).
% 22.19/3.41 cnf(c78, plain, lonely(sk2) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp78, plain, (spl4 | spl20), inference(avatar_split_clause, [status(thm)], [c78, sdef4, sdef20])).
% 22.19/3.41 cnf(c79, plain, lonely(sk2) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp79, plain, (spl5 | spl20), inference(avatar_split_clause, [status(thm)], [c79, sdef5, sdef20])).
% 22.19/3.41 cnf(c80, plain, lonely(sk2) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp80, plain, (spl6 | spl20), inference(avatar_split_clause, [status(thm)], [c80, sdef6, sdef20])).
% 22.19/3.41 cnf(c81, plain, lonely(sk2) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp81, plain, (spl7 | spl20), inference(avatar_split_clause, [status(thm)], [c81, sdef7, sdef20])).
% 22.19/3.41 cnf(c82, plain, lonely(sk2) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp82, plain, (spl8 | spl20), inference(avatar_split_clause, [status(thm)], [c82, sdef8, sdef20])).
% 22.19/3.41 cnf(c83, plain, lonely(sk2) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp83, plain, (spl9 | spl20), inference(avatar_split_clause, [status(thm)], [c83, sdef9, sdef20])).
% 22.19/3.41 cnf(c84, plain, lonely(sk2) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp84, plain, (spl10 | spl20), inference(avatar_split_clause, [status(thm)], [c84, sdef10, sdef20])).
% 22.19/3.41 cnf(c85, plain, lonely(sk2) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp85, plain, (spl11 | spl20), inference(avatar_split_clause, [status(thm)], [c85, sdef11, sdef20])).
% 22.19/3.41 cnf(c86, plain, lonely(sk2) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp86, plain, (spl12 | spl20), inference(avatar_split_clause, [status(thm)], [c86, sdef12, sdef20])).
% 22.19/3.41 cnf(c87, plain, lonely(sk2) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp87, plain, (spl13 | spl20), inference(avatar_split_clause, [status(thm)], [c87, sdef13, sdef20])).
% 22.19/3.41 cnf(c88, plain, lonely(sk2) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp88, plain, (spl14 | spl20), inference(avatar_split_clause, [status(thm)], [c88, sdef14, sdef20])).
% 22.19/3.41 cnf(c89, plain, lonely(sk2) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp89, plain, (spl15 | spl20), inference(avatar_split_clause, [status(thm)], [c89, sdef15, sdef20])).
% 22.19/3.41 cnf(c90, plain, chevy(sk3) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 fof(sdef21, definition, (spl21 <=> (chevy(sk3))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 22.19/3.41 cnf(ssp90, plain, (spl1 | spl21), inference(avatar_split_clause, [status(thm)], [c90, sdef1, sdef21])).
% 22.19/3.41 cnf(c91, plain, chevy(sk3) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp91, plain, (spl2 | spl21), inference(avatar_split_clause, [status(thm)], [c91, sdef2, sdef21])).
% 22.19/3.41 cnf(c92, plain, chevy(sk3) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp92, plain, (spl3 | spl21), inference(avatar_split_clause, [status(thm)], [c92, sdef3, sdef21])).
% 22.19/3.41 cnf(c93, plain, chevy(sk3) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp93, plain, (spl4 | spl21), inference(avatar_split_clause, [status(thm)], [c93, sdef4, sdef21])).
% 22.19/3.41 cnf(c94, plain, chevy(sk3) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp94, plain, (spl5 | spl21), inference(avatar_split_clause, [status(thm)], [c94, sdef5, sdef21])).
% 22.19/3.41 cnf(c95, plain, chevy(sk3) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp95, plain, (spl6 | spl21), inference(avatar_split_clause, [status(thm)], [c95, sdef6, sdef21])).
% 22.19/3.41 cnf(c96, plain, chevy(sk3) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp96, plain, (spl7 | spl21), inference(avatar_split_clause, [status(thm)], [c96, sdef7, sdef21])).
% 22.19/3.41 cnf(c97, plain, chevy(sk3) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp97, plain, (spl8 | spl21), inference(avatar_split_clause, [status(thm)], [c97, sdef8, sdef21])).
% 22.19/3.41 cnf(c98, plain, chevy(sk3) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp98, plain, (spl9 | spl21), inference(avatar_split_clause, [status(thm)], [c98, sdef9, sdef21])).
% 22.19/3.41 cnf(c99, plain, chevy(sk3) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp99, plain, (spl10 | spl21), inference(avatar_split_clause, [status(thm)], [c99, sdef10, sdef21])).
% 22.19/3.41 cnf(c100, plain, chevy(sk3) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp100, plain, (spl11 | spl21), inference(avatar_split_clause, [status(thm)], [c100, sdef11, sdef21])).
% 22.19/3.41 cnf(c101, plain, chevy(sk3) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp101, plain, (spl12 | spl21), inference(avatar_split_clause, [status(thm)], [c101, sdef12, sdef21])).
% 22.19/3.41 cnf(c102, plain, chevy(sk3) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp102, plain, (spl13 | spl21), inference(avatar_split_clause, [status(thm)], [c102, sdef13, sdef21])).
% 22.19/3.41 cnf(c103, plain, chevy(sk3) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp103, plain, (spl14 | spl21), inference(avatar_split_clause, [status(thm)], [c103, sdef14, sdef21])).
% 22.19/3.41 cnf(c104, plain, chevy(sk3) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp104, plain, (spl15 | spl21), inference(avatar_split_clause, [status(thm)], [c104, sdef15, sdef21])).
% 22.19/3.41 cnf(c105, plain, car(sk3) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp105, plain, (spl1 | spl22), inference(avatar_split_clause, [status(thm)], [c105, sdef1, sdef22])).
% 22.19/3.41 cnf(c106, plain, car(sk3) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp106, plain, (spl2 | spl22), inference(avatar_split_clause, [status(thm)], [c106, sdef2, sdef22])).
% 22.19/3.41 cnf(c107, plain, car(sk3) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp107, plain, (spl3 | spl22), inference(avatar_split_clause, [status(thm)], [c107, sdef3, sdef22])).
% 22.19/3.41 cnf(c108, plain, car(sk3) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp108, plain, (spl4 | spl22), inference(avatar_split_clause, [status(thm)], [c108, sdef4, sdef22])).
% 22.19/3.41 cnf(c109, plain, car(sk3) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp109, plain, (spl5 | spl22), inference(avatar_split_clause, [status(thm)], [c109, sdef5, sdef22])).
% 22.19/3.41 cnf(c110, plain, car(sk3) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp110, plain, (spl6 | spl22), inference(avatar_split_clause, [status(thm)], [c110, sdef6, sdef22])).
% 22.19/3.41 cnf(c111, plain, car(sk3) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp111, plain, (spl7 | spl22), inference(avatar_split_clause, [status(thm)], [c111, sdef7, sdef22])).
% 22.19/3.41 cnf(c112, plain, car(sk3) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp112, plain, (spl8 | spl22), inference(avatar_split_clause, [status(thm)], [c112, sdef8, sdef22])).
% 22.19/3.41 cnf(c113, plain, car(sk3) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp113, plain, (spl9 | spl22), inference(avatar_split_clause, [status(thm)], [c113, sdef9, sdef22])).
% 22.19/3.41 cnf(c114, plain, car(sk3) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp114, plain, (spl10 | spl22), inference(avatar_split_clause, [status(thm)], [c114, sdef10, sdef22])).
% 22.19/3.41 cnf(c115, plain, car(sk3) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp115, plain, (spl11 | spl22), inference(avatar_split_clause, [status(thm)], [c115, sdef11, sdef22])).
% 22.19/3.41 cnf(c116, plain, car(sk3) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp116, plain, (spl12 | spl22), inference(avatar_split_clause, [status(thm)], [c116, sdef12, sdef22])).
% 22.19/3.41 cnf(c117, plain, car(sk3) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp117, plain, (spl13 | spl22), inference(avatar_split_clause, [status(thm)], [c117, sdef13, sdef22])).
% 22.19/3.41 cnf(c118, plain, car(sk3) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp118, plain, (spl14 | spl22), inference(avatar_split_clause, [status(thm)], [c118, sdef14, sdef22])).
% 22.19/3.41 cnf(c119, plain, car(sk3) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp119, plain, (spl15 | spl22), inference(avatar_split_clause, [status(thm)], [c119, sdef15, sdef22])).
% 22.19/3.41 cnf(c120, plain, white(sk3) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp120, plain, (spl1 | spl23), inference(avatar_split_clause, [status(thm)], [c120, sdef1, sdef23])).
% 22.19/3.41 cnf(c121, plain, white(sk3) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp121, plain, (spl2 | spl23), inference(avatar_split_clause, [status(thm)], [c121, sdef2, sdef23])).
% 22.19/3.41 cnf(c122, plain, white(sk3) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp122, plain, (spl3 | spl23), inference(avatar_split_clause, [status(thm)], [c122, sdef3, sdef23])).
% 22.19/3.41 cnf(c123, plain, white(sk3) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp123, plain, (spl4 | spl23), inference(avatar_split_clause, [status(thm)], [c123, sdef4, sdef23])).
% 22.19/3.41 cnf(c124, plain, white(sk3) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp124, plain, (spl5 | spl23), inference(avatar_split_clause, [status(thm)], [c124, sdef5, sdef23])).
% 22.19/3.41 cnf(c125, plain, white(sk3) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp125, plain, (spl6 | spl23), inference(avatar_split_clause, [status(thm)], [c125, sdef6, sdef23])).
% 22.19/3.41 cnf(c126, plain, white(sk3) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp126, plain, (spl7 | spl23), inference(avatar_split_clause, [status(thm)], [c126, sdef7, sdef23])).
% 22.19/3.41 cnf(c127, plain, white(sk3) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp127, plain, (spl8 | spl23), inference(avatar_split_clause, [status(thm)], [c127, sdef8, sdef23])).
% 22.19/3.41 cnf(c128, plain, white(sk3) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp128, plain, (spl9 | spl23), inference(avatar_split_clause, [status(thm)], [c128, sdef9, sdef23])).
% 22.19/3.41 cnf(c129, plain, white(sk3) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp129, plain, (spl10 | spl23), inference(avatar_split_clause, [status(thm)], [c129, sdef10, sdef23])).
% 22.19/3.41 cnf(c130, plain, white(sk3) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp130, plain, (spl11 | spl23), inference(avatar_split_clause, [status(thm)], [c130, sdef11, sdef23])).
% 22.19/3.41 cnf(c131, plain, white(sk3) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp131, plain, (spl12 | spl23), inference(avatar_split_clause, [status(thm)], [c131, sdef12, sdef23])).
% 22.19/3.41 cnf(c132, plain, white(sk3) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp132, plain, (spl13 | spl23), inference(avatar_split_clause, [status(thm)], [c132, sdef13, sdef23])).
% 22.19/3.41 cnf(c133, plain, white(sk3) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp133, plain, (spl14 | spl23), inference(avatar_split_clause, [status(thm)], [c133, sdef14, sdef23])).
% 22.19/3.41 cnf(c134, plain, white(sk3) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp134, plain, (spl15 | spl23), inference(avatar_split_clause, [status(thm)], [c134, sdef15, sdef23])).
% 22.19/3.41 cnf(c135, plain, dirty(sk3) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp135, plain, (spl1 | spl24), inference(avatar_split_clause, [status(thm)], [c135, sdef1, sdef24])).
% 22.19/3.41 cnf(c136, plain, dirty(sk3) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp136, plain, (spl2 | spl24), inference(avatar_split_clause, [status(thm)], [c136, sdef2, sdef24])).
% 22.19/3.41 cnf(c137, plain, dirty(sk3) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp137, plain, (spl3 | spl24), inference(avatar_split_clause, [status(thm)], [c137, sdef3, sdef24])).
% 22.19/3.41 cnf(c138, plain, dirty(sk3) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp138, plain, (spl4 | spl24), inference(avatar_split_clause, [status(thm)], [c138, sdef4, sdef24])).
% 22.19/3.41 cnf(c139, plain, dirty(sk3) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp139, plain, (spl5 | spl24), inference(avatar_split_clause, [status(thm)], [c139, sdef5, sdef24])).
% 22.19/3.41 cnf(c140, plain, dirty(sk3) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp140, plain, (spl6 | spl24), inference(avatar_split_clause, [status(thm)], [c140, sdef6, sdef24])).
% 22.19/3.41 cnf(c141, plain, dirty(sk3) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp141, plain, (spl7 | spl24), inference(avatar_split_clause, [status(thm)], [c141, sdef7, sdef24])).
% 22.19/3.41 cnf(c142, plain, dirty(sk3) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp142, plain, (spl8 | spl24), inference(avatar_split_clause, [status(thm)], [c142, sdef8, sdef24])).
% 22.19/3.41 cnf(c143, plain, dirty(sk3) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp143, plain, (spl9 | spl24), inference(avatar_split_clause, [status(thm)], [c143, sdef9, sdef24])).
% 22.19/3.41 cnf(c144, plain, dirty(sk3) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp144, plain, (spl10 | spl24), inference(avatar_split_clause, [status(thm)], [c144, sdef10, sdef24])).
% 22.19/3.41 cnf(c145, plain, dirty(sk3) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp145, plain, (spl11 | spl24), inference(avatar_split_clause, [status(thm)], [c145, sdef11, sdef24])).
% 22.19/3.41 cnf(c146, plain, dirty(sk3) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp146, plain, (spl12 | spl24), inference(avatar_split_clause, [status(thm)], [c146, sdef12, sdef24])).
% 22.19/3.41 cnf(c147, plain, dirty(sk3) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp147, plain, (spl13 | spl24), inference(avatar_split_clause, [status(thm)], [c147, sdef13, sdef24])).
% 22.19/3.41 cnf(c148, plain, dirty(sk3) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp148, plain, (spl14 | spl24), inference(avatar_split_clause, [status(thm)], [c148, sdef14, sdef24])).
% 22.19/3.41 cnf(c149, plain, dirty(sk3) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp149, plain, (spl15 | spl24), inference(avatar_split_clause, [status(thm)], [c149, sdef15, sdef24])).
% 22.19/3.41 cnf(c150, plain, old(sk3) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp150, plain, (spl1 | spl25), inference(avatar_split_clause, [status(thm)], [c150, sdef1, sdef25])).
% 22.19/3.41 cnf(c151, plain, old(sk3) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp151, plain, (spl2 | spl25), inference(avatar_split_clause, [status(thm)], [c151, sdef2, sdef25])).
% 22.19/3.41 cnf(c152, plain, old(sk3) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp152, plain, (spl3 | spl25), inference(avatar_split_clause, [status(thm)], [c152, sdef3, sdef25])).
% 22.19/3.41 cnf(c153, plain, old(sk3) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp153, plain, (spl4 | spl25), inference(avatar_split_clause, [status(thm)], [c153, sdef4, sdef25])).
% 22.19/3.41 cnf(c154, plain, old(sk3) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp154, plain, (spl5 | spl25), inference(avatar_split_clause, [status(thm)], [c154, sdef5, sdef25])).
% 22.19/3.41 cnf(c155, plain, old(sk3) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp155, plain, (spl6 | spl25), inference(avatar_split_clause, [status(thm)], [c155, sdef6, sdef25])).
% 22.19/3.41 cnf(c156, plain, old(sk3) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp156, plain, (spl7 | spl25), inference(avatar_split_clause, [status(thm)], [c156, sdef7, sdef25])).
% 22.19/3.41 cnf(c157, plain, old(sk3) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp157, plain, (spl8 | spl25), inference(avatar_split_clause, [status(thm)], [c157, sdef8, sdef25])).
% 22.19/3.41 cnf(c158, plain, old(sk3) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp158, plain, (spl9 | spl25), inference(avatar_split_clause, [status(thm)], [c158, sdef9, sdef25])).
% 22.19/3.41 cnf(c159, plain, old(sk3) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp159, plain, (spl10 | spl25), inference(avatar_split_clause, [status(thm)], [c159, sdef10, sdef25])).
% 22.19/3.41 cnf(c160, plain, old(sk3) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp160, plain, (spl11 | spl25), inference(avatar_split_clause, [status(thm)], [c160, sdef11, sdef25])).
% 22.19/3.41 cnf(c161, plain, old(sk3) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp161, plain, (spl12 | spl25), inference(avatar_split_clause, [status(thm)], [c161, sdef12, sdef25])).
% 22.19/3.41 cnf(c162, plain, old(sk3) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp162, plain, (spl13 | spl25), inference(avatar_split_clause, [status(thm)], [c162, sdef13, sdef25])).
% 22.19/3.41 cnf(c163, plain, old(sk3) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp163, plain, (spl14 | spl25), inference(avatar_split_clause, [status(thm)], [c163, sdef14, sdef25])).
% 22.19/3.41 cnf(c164, plain, old(sk3) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp164, plain, (spl15 | spl25), inference(avatar_split_clause, [status(thm)], [c164, sdef15, sdef25])).
% 22.19/3.41 cnf(c165, plain, barrel(sk1,sk3) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp165, plain, (spl1 | spl26), inference(avatar_split_clause, [status(thm)], [c165, sdef1, sdef26])).
% 22.19/3.41 cnf(c166, plain, barrel(sk1,sk3) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp166, plain, (spl2 | spl26), inference(avatar_split_clause, [status(thm)], [c166, sdef2, sdef26])).
% 22.19/3.41 cnf(c167, plain, barrel(sk1,sk3) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp167, plain, (spl3 | spl26), inference(avatar_split_clause, [status(thm)], [c167, sdef3, sdef26])).
% 22.19/3.41 cnf(c168, plain, barrel(sk1,sk3) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp168, plain, (spl4 | spl26), inference(avatar_split_clause, [status(thm)], [c168, sdef4, sdef26])).
% 22.19/3.41 cnf(c169, plain, barrel(sk1,sk3) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp169, plain, (spl5 | spl26), inference(avatar_split_clause, [status(thm)], [c169, sdef5, sdef26])).
% 22.19/3.41 cnf(c170, plain, barrel(sk1,sk3) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp170, plain, (spl6 | spl26), inference(avatar_split_clause, [status(thm)], [c170, sdef6, sdef26])).
% 22.19/3.41 cnf(c171, plain, barrel(sk1,sk3) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp171, plain, (spl7 | spl26), inference(avatar_split_clause, [status(thm)], [c171, sdef7, sdef26])).
% 22.19/3.41 cnf(c172, plain, barrel(sk1,sk3) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp172, plain, (spl8 | spl26), inference(avatar_split_clause, [status(thm)], [c172, sdef8, sdef26])).
% 22.19/3.41 cnf(c173, plain, barrel(sk1,sk3) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp173, plain, (spl9 | spl26), inference(avatar_split_clause, [status(thm)], [c173, sdef9, sdef26])).
% 22.19/3.41 cnf(c174, plain, barrel(sk1,sk3) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp174, plain, (spl10 | spl26), inference(avatar_split_clause, [status(thm)], [c174, sdef10, sdef26])).
% 22.19/3.41 cnf(c175, plain, barrel(sk1,sk3) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp175, plain, (spl11 | spl26), inference(avatar_split_clause, [status(thm)], [c175, sdef11, sdef26])).
% 22.19/3.41 cnf(c176, plain, barrel(sk1,sk3) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp176, plain, (spl12 | spl26), inference(avatar_split_clause, [status(thm)], [c176, sdef12, sdef26])).
% 22.19/3.41 cnf(c177, plain, barrel(sk1,sk3) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp177, plain, (spl13 | spl26), inference(avatar_split_clause, [status(thm)], [c177, sdef13, sdef26])).
% 22.19/3.41 cnf(c178, plain, barrel(sk1,sk3) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp178, plain, (spl14 | spl26), inference(avatar_split_clause, [status(thm)], [c178, sdef14, sdef26])).
% 22.19/3.41 cnf(c179, plain, barrel(sk1,sk3) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp179, plain, (spl15 | spl26), inference(avatar_split_clause, [status(thm)], [c179, sdef15, sdef26])).
% 22.19/3.41 cnf(c180, plain, down(sk1,sk2) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp180, plain, (spl1 | spl27), inference(avatar_split_clause, [status(thm)], [c180, sdef1, sdef27])).
% 22.19/3.41 cnf(c181, plain, down(sk1,sk2) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp181, plain, (spl2 | spl27), inference(avatar_split_clause, [status(thm)], [c181, sdef2, sdef27])).
% 22.19/3.41 cnf(c182, plain, down(sk1,sk2) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp182, plain, (spl3 | spl27), inference(avatar_split_clause, [status(thm)], [c182, sdef3, sdef27])).
% 22.19/3.41 cnf(c183, plain, down(sk1,sk2) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp183, plain, (spl4 | spl27), inference(avatar_split_clause, [status(thm)], [c183, sdef4, sdef27])).
% 22.19/3.41 cnf(c184, plain, down(sk1,sk2) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp184, plain, (spl5 | spl27), inference(avatar_split_clause, [status(thm)], [c184, sdef5, sdef27])).
% 22.19/3.41 cnf(c185, plain, down(sk1,sk2) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp185, plain, (spl6 | spl27), inference(avatar_split_clause, [status(thm)], [c185, sdef6, sdef27])).
% 22.19/3.41 cnf(c186, plain, down(sk1,sk2) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp186, plain, (spl7 | spl27), inference(avatar_split_clause, [status(thm)], [c186, sdef7, sdef27])).
% 22.19/3.41 cnf(c187, plain, down(sk1,sk2) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp187, plain, (spl8 | spl27), inference(avatar_split_clause, [status(thm)], [c187, sdef8, sdef27])).
% 22.19/3.41 cnf(c188, plain, down(sk1,sk2) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp188, plain, (spl9 | spl27), inference(avatar_split_clause, [status(thm)], [c188, sdef9, sdef27])).
% 22.19/3.41 cnf(c189, plain, down(sk1,sk2) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp189, plain, (spl10 | spl27), inference(avatar_split_clause, [status(thm)], [c189, sdef10, sdef27])).
% 22.19/3.41 cnf(c190, plain, down(sk1,sk2) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp190, plain, (spl11 | spl27), inference(avatar_split_clause, [status(thm)], [c190, sdef11, sdef27])).
% 22.19/3.41 cnf(c191, plain, down(sk1,sk2) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp191, plain, (spl12 | spl27), inference(avatar_split_clause, [status(thm)], [c191, sdef12, sdef27])).
% 22.19/3.41 cnf(c192, plain, down(sk1,sk2) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp192, plain, (spl13 | spl27), inference(avatar_split_clause, [status(thm)], [c192, sdef13, sdef27])).
% 22.19/3.41 cnf(c193, plain, down(sk1,sk2) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.41 cnf(ssp193, plain, (spl14 | spl27), inference(avatar_split_clause, [status(thm)], [c193, sdef14, sdef27])).
% 22.19/3.41 cnf(c194, plain, down(sk1,sk2) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp194, plain, (spl15 | spl27), inference(avatar_split_clause, [status(thm)], [c194, sdef15, sdef27])).
% 22.19/3.42 cnf(c195, plain, in(sk1,sk0) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp195, plain, (spl1 | spl28), inference(avatar_split_clause, [status(thm)], [c195, sdef1, sdef28])).
% 22.19/3.42 cnf(c196, plain, in(sk1,sk0) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp196, plain, (spl2 | spl28), inference(avatar_split_clause, [status(thm)], [c196, sdef2, sdef28])).
% 22.19/3.42 cnf(c197, plain, in(sk1,sk0) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp197, plain, (spl3 | spl28), inference(avatar_split_clause, [status(thm)], [c197, sdef3, sdef28])).
% 22.19/3.42 cnf(c198, plain, in(sk1,sk0) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp198, plain, (spl4 | spl28), inference(avatar_split_clause, [status(thm)], [c198, sdef4, sdef28])).
% 22.19/3.42 cnf(c199, plain, in(sk1,sk0) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp199, plain, (spl5 | spl28), inference(avatar_split_clause, [status(thm)], [c199, sdef5, sdef28])).
% 22.19/3.42 cnf(c200, plain, in(sk1,sk0) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp200, plain, (spl6 | spl28), inference(avatar_split_clause, [status(thm)], [c200, sdef6, sdef28])).
% 22.19/3.42 cnf(c201, plain, in(sk1,sk0) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp201, plain, (spl7 | spl28), inference(avatar_split_clause, [status(thm)], [c201, sdef7, sdef28])).
% 22.19/3.42 cnf(c202, plain, in(sk1,sk0) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp202, plain, (spl8 | spl28), inference(avatar_split_clause, [status(thm)], [c202, sdef8, sdef28])).
% 22.19/3.42 cnf(c203, plain, in(sk1,sk0) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp203, plain, (spl9 | spl28), inference(avatar_split_clause, [status(thm)], [c203, sdef9, sdef28])).
% 22.19/3.42 cnf(c204, plain, in(sk1,sk0) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp204, plain, (spl10 | spl28), inference(avatar_split_clause, [status(thm)], [c204, sdef10, sdef28])).
% 22.19/3.42 cnf(c205, plain, in(sk1,sk0) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp205, plain, (spl11 | spl28), inference(avatar_split_clause, [status(thm)], [c205, sdef11, sdef28])).
% 22.19/3.42 cnf(c206, plain, in(sk1,sk0) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp206, plain, (spl12 | spl28), inference(avatar_split_clause, [status(thm)], [c206, sdef12, sdef28])).
% 22.19/3.42 cnf(c207, plain, in(sk1,sk0) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp207, plain, (spl13 | spl28), inference(avatar_split_clause, [status(thm)], [c207, sdef13, sdef28])).
% 22.19/3.42 cnf(c208, plain, in(sk1,sk0) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp208, plain, (spl14 | spl28), inference(avatar_split_clause, [status(thm)], [c208, sdef14, sdef28])).
% 22.19/3.42 cnf(c209, plain, in(sk1,sk0) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp209, plain, (spl15 | spl28), inference(avatar_split_clause, [status(thm)], [c209, sdef15, sdef28])).
% 22.19/3.42 cnf(c210, plain, ~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) | hollywood(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 fof(sdef29, definition, (spl29 <=> (~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))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 22.19/3.42 cnf(ssp210, plain, (spl1 | spl29), inference(avatar_split_clause, [status(thm)], [c210, sdef1, sdef29])).
% 22.19/3.42 cnf(c211, plain, ~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) | city(sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp211, plain, (spl2 | spl29), inference(avatar_split_clause, [status(thm)], [c211, sdef2, sdef29])).
% 22.19/3.42 cnf(c212, plain, ~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) | event(sk5), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp212, plain, (spl3 | spl29), inference(avatar_split_clause, [status(thm)], [c212, sdef3, sdef29])).
% 22.19/3.42 cnf(c213, plain, ~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) | chevy(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp213, plain, (spl4 | spl29), inference(avatar_split_clause, [status(thm)], [c213, sdef4, sdef29])).
% 22.19/3.42 cnf(c214, plain, ~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) | car(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp214, plain, (spl5 | spl29), inference(avatar_split_clause, [status(thm)], [c214, sdef5, sdef29])).
% 22.19/3.42 cnf(c215, plain, ~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) | white(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp215, plain, (spl6 | spl29), inference(avatar_split_clause, [status(thm)], [c215, sdef6, sdef29])).
% 22.19/3.42 cnf(c216, plain, ~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) | dirty(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp216, plain, (spl7 | spl29), inference(avatar_split_clause, [status(thm)], [c216, sdef7, sdef29])).
% 22.19/3.42 cnf(c217, plain, ~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) | old(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp217, plain, (spl8 | spl29), inference(avatar_split_clause, [status(thm)], [c217, sdef8, sdef29])).
% 22.19/3.42 cnf(c218, plain, ~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) | street(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp218, plain, (spl9 | spl29), inference(avatar_split_clause, [status(thm)], [c218, sdef9, sdef29])).
% 22.19/3.42 cnf(c219, plain, ~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) | way(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp219, plain, (spl10 | spl29), inference(avatar_split_clause, [status(thm)], [c219, sdef10, sdef29])).
% 22.19/3.42 cnf(c220, plain, ~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) | lonely(sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp220, plain, (spl11 | spl29), inference(avatar_split_clause, [status(thm)], [c220, sdef11, sdef29])).
% 22.19/3.42 cnf(c221, plain, ~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) | barrel(sk5,sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp221, plain, (spl12 | spl29), inference(avatar_split_clause, [status(thm)], [c221, sdef12, sdef29])).
% 22.19/3.42 cnf(c222, plain, ~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) | down(sk5,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp222, plain, (spl13 | spl29), inference(avatar_split_clause, [status(thm)], [c222, sdef13, sdef29])).
% 22.19/3.42 cnf(c223, plain, ~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) | in(sk5,sk4), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp223, plain, (spl14 | spl29), inference(avatar_split_clause, [status(thm)], [c223, sdef14, sdef29])).
% 22.19/3.42 cnf(c224, plain, ~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) | ~hollywood(X12) | ~city(X12) | ~event(X13) | ~street(X14) | ~way(X14) | ~lonely(X14) | ~chevy(X15) | ~car(X15) | ~white(X15) | ~dirty(X15) | ~old(X15) | ~barrel(X13,X15) | ~down(X13,X14) | ~in(X13,X12), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 22.19/3.42 cnf(ssp224, plain, (spl15 | spl29), inference(avatar_split_clause, [status(thm)], [c224, sdef15, sdef29])).
% 22.19/3.42 cnf(p30, plain, (~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) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 22.19/3.42 cnf(p1, plain, (hollywood(sk0) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 22.19/3.42 cnf(p255, plain, (~city(sk0) | ~event(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~barrel(X0,X2) | ~down(X0,X1) | ~in(X0,sk0) | ~spl0 | ~spl15), inference(resolution, [status(thm)], [p30, p1])).
% 22.19/3.42 fof(sdef31, definition, (spl31 <=> (~event(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~barrel(X0,X2) | ~down(X0,X1) | ~in(X0,sk0))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 22.19/3.42 cnf(ssp225, plain, (~spl0 | ~spl15 | spl30 | spl31), inference(avatar_split_clause, [status(thm)], [p255, sdef30, sdef31])).
% 22.19/3.42 cnf(p2, plain, (hollywood(sk4) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 22.19/3.42 cnf(p258, plain, (~city(sk4) | ~event(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~barrel(X0,X2) | ~down(X0,X1) | ~in(X0,sk4) | ~spl1 | ~spl15), inference(resolution, [status(thm)], [p30, p2])).
% 22.19/3.42 fof(sdef33, definition, (spl33 <=> (~event(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~barrel(X0,X2) | ~down(X0,X1) | ~in(X0,sk4))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 22.19/3.42 cnf(ssp226, plain, (~spl1 | ~spl15 | spl32 | spl33), inference(avatar_split_clause, [status(thm)], [p258, sdef32, sdef33])).
% 22.19/3.42 cnf(p240, plain, (~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) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 22.19/3.42 cnf(p261, plain, (~city(sk0) | ~event(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~street(X2) | ~way(X2) | ~lonely(X2) | ~barrel(X0,X1) | ~down(X0,X2) | ~in(X0,sk0) | ~spl0 | ~spl29), inference(resolution, [status(thm)], [p240, p1])).
% 22.19/3.42 fof(sdef34, definition, (spl34 <=> (~event(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~street(X2) | ~way(X2) | ~lonely(X2) | ~barrel(X0,X1) | ~down(X0,X2) | ~in(X0,sk0))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 22.19/3.42 cnf(ssp227, plain, (~spl0 | ~spl29 | spl30 | spl34), inference(avatar_split_clause, [status(thm)], [p261, sdef30, sdef34])).
% 22.19/3.42 cnf(p263, plain, (~city(sk4) | ~event(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~street(X2) | ~way(X2) | ~lonely(X2) | ~barrel(X0,X1) | ~down(X0,X2) | ~in(X0,sk4) | ~spl1 | ~spl29), inference(resolution, [status(thm)], [p240, p2])).
% 22.19/3.42 fof(sdef35, definition, (spl35 <=> (~event(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~street(X2) | ~way(X2) | ~lonely(X2) | ~barrel(X0,X1) | ~down(X0,X2) | ~in(X0,sk4))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 22.19/3.42 cnf(ssp228, plain, (~spl1 | ~spl29 | spl32 | spl35), inference(avatar_split_clause, [status(thm)], [p263, sdef32, sdef35])).
% 22.19/3.42 cnf(p257, plain, (~event(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~barrel(X0,X2) | ~down(X0,X1) | ~in(X0,sk0) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 22.19/3.42 cnf(p6, plain, (event(sk5) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 22.19/3.42 cnf(p267, plain, (~street(X0) | ~way(X0) | ~lonely(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~barrel(sk5,X1) | ~down(sk5,X0) | ~in(sk5,sk0) | ~spl3 | ~spl31), inference(resolution, [status(thm)], [p257, p6])).
% 22.19/3.42 fof(sdef36, definition, (spl36 <=> (~street(X0) | ~way(X0) | ~lonely(X0) | ~down(sk5,X0))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 22.19/3.42 fof(sdef37, definition, (spl37 <=> (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sk5,X0))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 22.19/3.42 fof(sdef38, definition, (spl38 <=> (~in(sk5,sk0))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 22.19/3.42 cnf(ssp229, plain, (~spl3 | ~spl31 | spl36 | spl37 | spl38), inference(avatar_split_clause, [status(thm)], [p267, sdef36, sdef37, sdef38])).
% 22.19/3.42 cnf(p48, plain, (event(sk1) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 22.19/3.42 cnf(p271, plain, (~street(X0) | ~way(X0) | ~lonely(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~barrel(sk1,X1) | ~down(sk1,X0) | ~in(sk1,sk0) | ~spl17 | ~spl31), inference(resolution, [status(thm)], [p257, p48])).
% 22.19/3.42 fof(sdef39, definition, (spl39 <=> (~street(X0) | ~way(X0) | ~lonely(X0) | ~down(sk1,X0))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 22.19/3.42 fof(sdef40, definition, (spl40 <=> (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sk1,X0))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 22.19/3.42 cnf(ssp230, plain, (~spl17 | ~spl31 | spl39 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p271, sdef39, sdef40, sdef41])).
% 22.19/3.42 cnf(p260, plain, (~event(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~chevy(X2) | ~car(X2) | ~white(X2) | ~dirty(X2) | ~old(X2) | ~barrel(X0,X2) | ~down(X0,X1) | ~in(X0,sk4) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 22.19/3.42 cnf(p275, plain, (~street(X0) | ~way(X0) | ~lonely(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~barrel(sk5,X1) | ~down(sk5,X0) | ~in(sk5,sk4) | ~spl3 | ~spl33), inference(resolution, [status(thm)], [p260, p6])).
% 22.19/3.42 cnf(ssp231, plain, (~spl3 | ~spl33 | spl36 | spl37 | spl42), inference(avatar_split_clause, [status(thm)], [p275, sdef36, sdef37, sdef42])).
% 22.19/3.42 cnf(p277, plain, (~street(X0) | ~way(X0) | ~lonely(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~barrel(sk1,X1) | ~down(sk1,X0) | ~in(sk1,sk4) | ~spl17 | ~spl33), inference(resolution, [status(thm)], [p260, p48])).
% 22.19/3.42 fof(sdef43, definition, (spl43 <=> (~in(sk1,sk4))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 22.19/3.42 cnf(ssp232, plain, (~spl17 | ~spl33 | spl39 | spl40 | spl43), inference(avatar_split_clause, [status(thm)], [p277, sdef39, sdef40, sdef43])).
% 22.19/3.42 cnf(p268, plain, (~street(X0) | ~way(X0) | ~lonely(X0) | ~down(sk5,X0) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 22.19/3.42 cnf(p18, plain, (street(sk7) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 22.19/3.42 cnf(p281, plain, (~way(sk7) | ~lonely(sk7) | ~down(sk5,sk7) | ~spl9 | ~spl36), inference(resolution, [status(thm)], [p268, p18])).
% 22.19/3.42 cnf(ssp233, plain, (~spl9 | ~spl36 | spl44 | spl45 | spl46), inference(avatar_split_clause, [status(thm)], [p281, sdef44, sdef45, sdef46])).
% 22.19/3.42 cnf(p64, plain, (street(sk2) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 22.19/3.42 cnf(p285, plain, (~way(sk2) | ~lonely(sk2) | ~down(sk5,sk2) | ~spl18 | ~spl36), inference(resolution, [status(thm)], [p268, p64])).
% 22.19/3.42 fof(sdef49, definition, (spl49 <=> (~down(sk5,sk2))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 22.19/3.42 cnf(ssp234, plain, (~spl18 | ~spl36 | spl47 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p285, sdef47, sdef48, sdef49])).
% 22.19/3.42 cnf(p262, plain, (~event(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~street(X2) | ~way(X2) | ~lonely(X2) | ~barrel(X0,X1) | ~down(X0,X2) | ~in(X0,sk0) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 22.19/3.42 cnf(p289, plain, (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sk5,X0) | ~down(sk5,X1) | ~in(sk5,sk0) | ~spl3 | ~spl34), inference(resolution, [status(thm)], [p262, p6])).
% 22.19/3.42 cnf(ssp235, plain, (~spl3 | ~spl34 | spl36 | spl37 | spl38), inference(avatar_split_clause, [status(thm)], [p289, sdef36, sdef37, sdef38])).
% 22.19/3.42 cnf(p264, plain, (~event(X0) | ~chevy(X1) | ~car(X1) | ~white(X1) | ~dirty(X1) | ~old(X1) | ~street(X2) | ~way(X2) | ~lonely(X2) | ~barrel(X0,X1) | ~down(X0,X2) | ~in(X0,sk4) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 22.19/3.42 cnf(p294, plain, (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sk5,X0) | ~down(sk5,X1) | ~in(sk5,sk4) | ~spl3 | ~spl35), inference(resolution, [status(thm)], [p264, p6])).
% 22.19/3.42 cnf(ssp236, plain, (~spl3 | ~spl35 | spl36 | spl37 | spl42), inference(avatar_split_clause, [status(thm)], [p294, sdef36, sdef37, sdef42])).
% 22.19/3.42 cnf(p272, plain, (~street(X0) | ~way(X0) | ~lonely(X0) | ~down(sk1,X0) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 22.19/3.42 cnf(p296, plain, (~way(sk7) | ~lonely(sk7) | ~down(sk1,sk7) | ~spl9 | ~spl39), inference(resolution, [status(thm)], [p272, p18])).
% 22.19/3.42 fof(sdef50, definition, (spl50 <=> (~down(sk1,sk7))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 22.19/3.42 cnf(ssp237, plain, (~spl9 | ~spl39 | spl44 | spl45 | spl50), inference(avatar_split_clause, [status(thm)], [p296, sdef44, sdef45, sdef50])).
% 22.19/3.42 cnf(p298, plain, (~way(sk2) | ~lonely(sk2) | ~down(sk1,sk2) | ~spl18 | ~spl39), inference(resolution, [status(thm)], [p272, p64])).
% 22.19/3.42 cnf(ssp238, plain, (~spl18 | ~spl39 | spl47 | spl48 | spl51), inference(avatar_split_clause, [status(thm)], [p298, sdef47, sdef48, sdef51])).
% 22.19/3.42 cnf(p269, plain, (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sk5,X0) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 22.19/3.42 cnf(p8, plain, (chevy(sk6) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 22.19/3.42 cnf(p300, plain, (~car(sk6) | ~white(sk6) | ~dirty(sk6) | ~old(sk6) | ~barrel(sk5,sk6) | ~spl4 | ~spl37), inference(resolution, [status(thm)], [p269, p8])).
% 22.19/3.42 cnf(ssp239, plain, (~spl4 | ~spl37 | spl52 | spl53 | spl54 | spl55 | spl56), inference(avatar_split_clause, [status(thm)], [p300, sdef52, sdef53, sdef54, sdef55, sdef56])).
% 22.19/3.42 cnf(p112, plain, (chevy(sk3) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 22.19/3.42 cnf(p306, plain, (~car(sk3) | ~white(sk3) | ~dirty(sk3) | ~old(sk3) | ~barrel(sk5,sk3) | ~spl21 | ~spl37), inference(resolution, [status(thm)], [p269, p112])).
% 22.19/3.42 fof(sdef61, definition, (spl61 <=> (~barrel(sk5,sk3))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 22.19/3.42 cnf(ssp240, plain, (~spl21 | ~spl37 | spl57 | spl58 | spl59 | spl60 | spl61), inference(avatar_split_clause, [status(thm)], [p306, sdef57, sdef58, sdef59, sdef60, sdef61])).
% 22.19/3.42 cnf(p273, plain, (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~barrel(sk1,X0) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 22.19/3.42 cnf(p316, plain, (~car(sk6) | ~white(sk6) | ~dirty(sk6) | ~old(sk6) | ~barrel(sk1,sk6) | ~spl4 | ~spl40), inference(resolution, [status(thm)], [p273, p8])).
% 22.19/3.42 fof(sdef62, definition, (spl62 <=> (~barrel(sk1,sk6))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 22.19/3.42 cnf(ssp241, plain, (~spl4 | ~spl40 | spl52 | spl53 | spl54 | spl55 | spl62), inference(avatar_split_clause, [status(thm)], [p316, sdef52, sdef53, sdef54, sdef55, sdef62])).
% 22.19/3.42 cnf(p324, plain, (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sk1,X0) | ~down(sk1,X1) | ~in(sk1,sk0) | ~spl17 | ~spl34), inference(resolution, [status(thm)], [p48, p262])).
% 22.19/3.42 cnf(ssp242, plain, (~spl17 | ~spl34 | spl39 | spl40 | spl41), inference(avatar_split_clause, [status(thm)], [p324, sdef39, sdef40, sdef41])).
% 22.19/3.42 cnf(p325, plain, (~chevy(X0) | ~car(X0) | ~white(X0) | ~dirty(X0) | ~old(X0) | ~street(X1) | ~way(X1) | ~lonely(X1) | ~barrel(sk1,X0) | ~down(sk1,X1) | ~in(sk1,sk4) | ~spl17 | ~spl35), inference(resolution, [status(thm)], [p48, p264])).
% 22.19/3.42 cnf(ssp243, plain, (~spl17 | ~spl35 | spl39 | spl40 | spl43), inference(avatar_split_clause, [status(thm)], [p325, sdef39, sdef40, sdef43])).
% 22.19/3.42 cnf(p326, plain, (~car(sk3) | ~white(sk3) | ~dirty(sk3) | ~old(sk3) | ~barrel(sk1,sk3) | ~spl21 | ~spl40), inference(resolution, [status(thm)], [p112, p273])).
% 22.19/3.42 cnf(ssp244, plain, (~spl21 | ~spl40 | spl57 | spl58 | spl59 | spl60 | spl63), inference(avatar_split_clause, [status(thm)], [p326, sdef57, sdef58, sdef59, sdef60, sdef63])).
% 22.19/3.42 cnf(sat_ref, plain, $false, inference(avatar_sat_refutation, [status(thm)], [ssp0, ssp1, ssp2, ssp3, ssp4, ssp5, ssp6, ssp7, ssp8, ssp9, ssp10, ssp11, ssp12, ssp13, ssp14, ssp15, ssp16, ssp17, ssp18, ssp19, ssp20, ssp21, ssp22, ssp23, ssp24, ssp25, ssp26, ssp27, ssp28, ssp29, ssp30, ssp31, ssp32, ssp33, ssp34, ssp35, ssp36, ssp37, ssp38, ssp39, ssp40, ssp41, ssp42, ssp43, ssp44, ssp45, ssp46, ssp47, ssp48, ssp49, ssp50, ssp51, ssp52, ssp53, ssp54, ssp55, ssp56, ssp57, ssp58, ssp59, ssp60, ssp61, ssp62, ssp63, ssp64, ssp65, ssp66, ssp67, ssp68, ssp69, ssp70, ssp71, ssp72, ssp73, ssp74, ssp75, ssp76, ssp77, ssp78, ssp79, ssp80, ssp81, ssp82, ssp83, ssp84, ssp85, ssp86, ssp87, ssp88, ssp89, ssp90, ssp91, ssp92, ssp93, ssp94, ssp95, ssp96, ssp97, ssp98, ssp99, ssp100, ssp101, ssp102, ssp103, ssp104, ssp105, ssp106, ssp107, ssp108, ssp109, ssp110, ssp111, ssp112, ssp113, ssp114, ssp115, ssp116, ssp117, ssp118, ssp119, ssp120, ssp121, ssp122, ssp123, ssp124, ssp125, ssp126, ssp127, ssp128, ssp129, ssp130, ssp131, ssp132, ssp133, ssp134, ssp135, ssp136, ssp137, ssp138, ssp139, ssp140, ssp141, ssp142, ssp143, ssp144, ssp145, ssp146, ssp147, ssp148, ssp149, ssp150, ssp151, ssp152, ssp153, ssp154, ssp155, ssp156, ssp157, ssp158, ssp159, ssp160, ssp161, ssp162, ssp163, ssp164, ssp165, ssp166, ssp167, ssp168, ssp169, ssp170, ssp171, ssp172, ssp173, ssp174, ssp175, ssp176, ssp177, ssp178, ssp179, ssp180, ssp181, ssp182, ssp183, ssp184, ssp185, ssp186, ssp187, ssp188, ssp189, ssp190, ssp191, ssp192, ssp193, ssp194, ssp195, ssp196, ssp197, ssp198, ssp199, ssp200, ssp201, ssp202, ssp203, ssp204, ssp205, ssp206, ssp207, ssp208, ssp209, ssp210, ssp211, ssp212, ssp213, ssp214, ssp215, ssp216, ssp217, ssp218, ssp219, ssp220, ssp221, ssp222, ssp223, ssp224, ssp225, ssp226, ssp227, ssp228, ssp229, ssp230, ssp231, ssp232, ssp233, ssp234, ssp235, ssp236, ssp237, ssp238, ssp239, ssp240, ssp241, ssp242, ssp243, ssp244, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19])).
% 22.19/3.42 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------