%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : NLP117+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 : n011.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:44 PM UTC 2026
% Result : Theorem 15.06s 2.63s
% Output : Proof 15.06s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : NLP117+1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n011.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Thu Sep 24 02:02:27 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 15.06/2.63 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.06/2.63 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.06/2.63 fof(sdef36, definition, (spl36 <=> (~city(sk0,sk1))), introduced(definition, [new_symbols(naming, [spl36])], [avatar_definition])).
% 15.06/2.63 cnf(p363, plain, (~city(sk0,sk1) | ~spl36), inference(avatar_component_clause, [status(thm)], [sdef36])).
% 15.06/2.63 fof(sdef20, definition, (spl20 <=> (city(sk0,sk1))), introduced(definition, [new_symbols(naming, [spl20])], [avatar_definition])).
% 15.06/2.63 cnf(p57, plain, (city(sk0,sk1) | ~spl20), inference(avatar_component_clause, [status(thm)], [sdef20])).
% 15.06/2.63 cnf(p367, plain, ($false | ~spl20 | ~spl36), inference(resolution, [status(thm)], [p363, p57])).
% 15.06/2.63 cnf(sct0, plain, (~spl20 | ~spl36), inference(avatar_contradiction_clause, [status(thm)], [p367])).
% 15.06/2.63 fof(sdef37, definition, (spl37 <=> (~hollywood_placename(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl37])], [avatar_definition])).
% 15.06/2.63 cnf(p364, plain, (~hollywood_placename(sk0,sk2) | ~spl37), inference(avatar_component_clause, [status(thm)], [sdef37])).
% 15.06/2.63 fof(sdef21, definition, (spl21 <=> (hollywood_placename(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl21])], [avatar_definition])).
% 15.06/2.63 cnf(p76, plain, (hollywood_placename(sk0,sk2) | ~spl21), inference(avatar_component_clause, [status(thm)], [sdef21])).
% 15.06/2.63 cnf(p368, plain, ($false | ~spl21 | ~spl37), inference(resolution, [status(thm)], [p364, p76])).
% 15.06/2.63 cnf(sct1, plain, (~spl21 | ~spl37), inference(avatar_contradiction_clause, [status(thm)], [p368])).
% 15.06/2.63 fof(sdef38, definition, (spl38 <=> (~placename(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl38])], [avatar_definition])).
% 15.06/2.63 cnf(p365, plain, (~placename(sk0,sk2) | ~spl38), inference(avatar_component_clause, [status(thm)], [sdef38])).
% 15.06/2.63 fof(sdef22, definition, (spl22 <=> (placename(sk0,sk2))), introduced(definition, [new_symbols(naming, [spl22])], [avatar_definition])).
% 15.06/2.63 cnf(p95, plain, (placename(sk0,sk2) | ~spl22), inference(avatar_component_clause, [status(thm)], [sdef22])).
% 15.06/2.63 cnf(p369, plain, ($false | ~spl22 | ~spl38), inference(resolution, [status(thm)], [p365, p95])).
% 15.06/2.63 cnf(sct2, plain, (~spl22 | ~spl38), inference(avatar_contradiction_clause, [status(thm)], [p369])).
% 15.06/2.63 fof(sdef40, definition, (spl40 <=> (~white(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl40])], [avatar_definition])).
% 15.06/2.63 cnf(p373, plain, (~white(sk0,sk3) | ~spl40), inference(avatar_component_clause, [status(thm)], [sdef40])).
% 15.06/2.63 fof(sdef24, definition, (spl24 <=> (white(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl24])], [avatar_definition])).
% 15.06/2.63 cnf(p133, plain, (white(sk0,sk3) | ~spl24), inference(avatar_component_clause, [status(thm)], [sdef24])).
% 15.06/2.63 cnf(p377, plain, ($false | ~spl24 | ~spl40), inference(resolution, [status(thm)], [p373, p133])).
% 15.06/2.63 cnf(sct3, plain, (~spl24 | ~spl40), inference(avatar_contradiction_clause, [status(thm)], [p377])).
% 15.06/2.63 fof(sdef41, definition, (spl41 <=> (~dirty(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl41])], [avatar_definition])).
% 15.06/2.63 cnf(p374, plain, (~dirty(sk0,sk3) | ~spl41), inference(avatar_component_clause, [status(thm)], [sdef41])).
% 15.06/2.63 fof(sdef25, definition, (spl25 <=> (dirty(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl25])], [avatar_definition])).
% 15.06/2.63 cnf(p152, plain, (dirty(sk0,sk3) | ~spl25), inference(avatar_component_clause, [status(thm)], [sdef25])).
% 15.06/2.63 cnf(p378, plain, ($false | ~spl25 | ~spl41), inference(resolution, [status(thm)], [p374, p152])).
% 15.06/2.63 cnf(sct4, plain, (~spl25 | ~spl41), inference(avatar_contradiction_clause, [status(thm)], [p378])).
% 15.06/2.63 fof(sdef42, definition, (spl42 <=> (~old(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl42])], [avatar_definition])).
% 15.06/2.63 cnf(p375, plain, (~old(sk0,sk3) | ~spl42), inference(avatar_component_clause, [status(thm)], [sdef42])).
% 15.06/2.63 fof(sdef26, definition, (spl26 <=> (old(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl26])], [avatar_definition])).
% 15.06/2.63 cnf(p171, plain, (old(sk0,sk3) | ~spl26), inference(avatar_component_clause, [status(thm)], [sdef26])).
% 15.06/2.63 cnf(p379, plain, ($false | ~spl26 | ~spl42), inference(resolution, [status(thm)], [p375, p171])).
% 15.06/2.63 cnf(sct5, plain, (~spl26 | ~spl42), inference(avatar_contradiction_clause, [status(thm)], [p379])).
% 15.06/2.63 fof(sdef44, definition, (spl44 <=> (~city(sk6,sk7))), introduced(definition, [new_symbols(naming, [spl44])], [avatar_definition])).
% 15.06/2.63 cnf(p381, plain, (~city(sk6,sk7) | ~spl44), inference(avatar_component_clause, [status(thm)], [sdef44])).
% 15.06/2.63 fof(sdef3, definition, (spl3 <=> (city(sk6,sk7))), introduced(definition, [new_symbols(naming, [spl3])], [avatar_definition])).
% 15.06/2.63 cnf(p6, plain, (city(sk6,sk7) | ~spl3), inference(avatar_component_clause, [status(thm)], [sdef3])).
% 15.06/2.63 cnf(p385, plain, ($false | ~spl3 | ~spl44), inference(resolution, [status(thm)], [p381, p6])).
% 15.06/2.63 cnf(sct6, plain, (~spl3 | ~spl44), inference(avatar_contradiction_clause, [status(thm)], [p385])).
% 15.06/2.63 fof(sdef45, definition, (spl45 <=> (~hollywood_placename(sk6,sk8))), introduced(definition, [new_symbols(naming, [spl45])], [avatar_definition])).
% 15.06/2.63 cnf(p382, plain, (~hollywood_placename(sk6,sk8) | ~spl45), inference(avatar_component_clause, [status(thm)], [sdef45])).
% 15.06/2.63 fof(sdef4, definition, (spl4 <=> (hollywood_placename(sk6,sk8))), introduced(definition, [new_symbols(naming, [spl4])], [avatar_definition])).
% 15.06/2.63 cnf(p8, plain, (hollywood_placename(sk6,sk8) | ~spl4), inference(avatar_component_clause, [status(thm)], [sdef4])).
% 15.06/2.63 cnf(p386, plain, ($false | ~spl4 | ~spl45), inference(resolution, [status(thm)], [p382, p8])).
% 15.06/2.63 cnf(sct7, plain, (~spl4 | ~spl45), inference(avatar_contradiction_clause, [status(thm)], [p386])).
% 15.06/2.63 fof(sdef46, definition, (spl46 <=> (~placename(sk6,sk8))), introduced(definition, [new_symbols(naming, [spl46])], [avatar_definition])).
% 15.06/2.63 cnf(p383, plain, (~placename(sk6,sk8) | ~spl46), inference(avatar_component_clause, [status(thm)], [sdef46])).
% 15.06/2.63 fof(sdef5, definition, (spl5 <=> (placename(sk6,sk8))), introduced(definition, [new_symbols(naming, [spl5])], [avatar_definition])).
% 15.06/2.63 cnf(p10, plain, (placename(sk6,sk8) | ~spl5), inference(avatar_component_clause, [status(thm)], [sdef5])).
% 15.06/2.63 cnf(p387, plain, ($false | ~spl5 | ~spl46), inference(resolution, [status(thm)], [p383, p10])).
% 15.06/2.63 cnf(sct8, plain, (~spl5 | ~spl46), inference(avatar_contradiction_clause, [status(thm)], [p387])).
% 15.06/2.63 fof(sdef48, definition, (spl48 <=> (~lonely(sk0,sk4))), introduced(definition, [new_symbols(naming, [spl48])], [avatar_definition])).
% 15.06/2.63 cnf(p389, plain, (~lonely(sk0,sk4) | ~spl48), inference(avatar_component_clause, [status(thm)], [sdef48])).
% 15.06/2.63 fof(sdef28, definition, (spl28 <=> (lonely(sk0,sk4))), introduced(definition, [new_symbols(naming, [spl28])], [avatar_definition])).
% 15.06/2.63 cnf(p209, plain, (lonely(sk0,sk4) | ~spl28), inference(avatar_component_clause, [status(thm)], [sdef28])).
% 15.06/2.63 cnf(p391, plain, ($false | ~spl28 | ~spl48), inference(resolution, [status(thm)], [p389, p209])).
% 15.06/2.63 cnf(sct9, plain, (~spl28 | ~spl48), inference(avatar_contradiction_clause, [status(thm)], [p391])).
% 15.06/2.63 fof(sdef51, definition, (spl51 <=> (~present(sk0,sk5))), introduced(definition, [new_symbols(naming, [spl51])], [avatar_definition])).
% 15.06/2.63 cnf(p394, plain, (~present(sk0,sk5) | ~spl51), inference(avatar_component_clause, [status(thm)], [sdef51])).
% 15.06/2.63 fof(sdef31, definition, (spl31 <=> (present(sk0,sk5))), introduced(definition, [new_symbols(naming, [spl31])], [avatar_definition])).
% 15.06/2.63 cnf(p266, plain, (present(sk0,sk5) | ~spl31), inference(avatar_component_clause, [status(thm)], [sdef31])).
% 15.06/2.63 cnf(p398, plain, ($false | ~spl31 | ~spl51), inference(resolution, [status(thm)], [p394, p266])).
% 15.06/2.63 cnf(sct10, plain, (~spl31 | ~spl51), inference(avatar_contradiction_clause, [status(thm)], [p398])).
% 15.06/2.63 fof(sdef52, definition, (spl52 <=> (~barrel(sk0,sk5))), introduced(definition, [new_symbols(naming, [spl52])], [avatar_definition])).
% 15.06/2.63 cnf(p395, plain, (~barrel(sk0,sk5) | ~spl52), inference(avatar_component_clause, [status(thm)], [sdef52])).
% 15.06/2.63 fof(sdef32, definition, (spl32 <=> (barrel(sk0,sk5))), introduced(definition, [new_symbols(naming, [spl32])], [avatar_definition])).
% 15.06/2.63 cnf(p285, plain, (barrel(sk0,sk5) | ~spl32), inference(avatar_component_clause, [status(thm)], [sdef32])).
% 15.06/2.63 cnf(p399, plain, ($false | ~spl32 | ~spl52), inference(resolution, [status(thm)], [p395, p285])).
% 15.06/2.63 cnf(sct11, plain, (~spl32 | ~spl52), inference(avatar_contradiction_clause, [status(thm)], [p399])).
% 15.06/2.63 fof(sdef50, definition, (spl50 <=> (~agent(sk0,sk5,sk3))), introduced(definition, [new_symbols(naming, [spl50])], [avatar_definition])).
% 15.06/2.63 cnf(p393, plain, (~agent(sk0,sk5,sk3) | ~spl50), inference(avatar_component_clause, [status(thm)], [sdef50])).
% 15.06/2.63 fof(sdef30, definition, (spl30 <=> (agent(sk0,sk5,sk3))), introduced(definition, [new_symbols(naming, [spl30])], [avatar_definition])).
% 15.06/2.63 cnf(p247, plain, (agent(sk0,sk5,sk3) | ~spl30), inference(avatar_component_clause, [status(thm)], [sdef30])).
% 15.06/2.63 cnf(p402, plain, ($false | ~spl30 | ~spl50), inference(resolution, [status(thm)], [p393, p247])).
% 15.06/2.63 cnf(sct12, plain, (~spl30 | ~spl50), inference(avatar_contradiction_clause, [status(thm)], [p402])).
% 15.06/2.63 fof(sdef53, definition, (spl53 <=> (~down(sk0,sk5,sk4))), introduced(definition, [new_symbols(naming, [spl53])], [avatar_definition])).
% 15.06/2.63 cnf(p396, plain, (~down(sk0,sk5,sk4) | ~spl53), inference(avatar_component_clause, [status(thm)], [sdef53])).
% 15.06/2.63 fof(sdef33, definition, (spl33 <=> (down(sk0,sk5,sk4))), introduced(definition, [new_symbols(naming, [spl33])], [avatar_definition])).
% 15.06/2.63 cnf(p304, plain, (down(sk0,sk5,sk4) | ~spl33), inference(avatar_component_clause, [status(thm)], [sdef33])).
% 15.06/2.63 cnf(p403, plain, ($false | ~spl33 | ~spl53), inference(resolution, [status(thm)], [p396, p304])).
% 15.06/2.63 cnf(sct13, plain, (~spl33 | ~spl53), inference(avatar_contradiction_clause, [status(thm)], [p403])).
% 15.06/2.63 fof(sdef54, definition, (spl54 <=> (~in(sk0,sk5,sk1))), introduced(definition, [new_symbols(naming, [spl54])], [avatar_definition])).
% 15.06/2.63 cnf(p397, plain, (~in(sk0,sk5,sk1) | ~spl54), inference(avatar_component_clause, [status(thm)], [sdef54])).
% 15.06/2.63 fof(sdef34, definition, (spl34 <=> (in(sk0,sk5,sk1))), introduced(definition, [new_symbols(naming, [spl34])], [avatar_definition])).
% 15.06/2.63 cnf(p323, plain, (in(sk0,sk5,sk1) | ~spl34), inference(avatar_component_clause, [status(thm)], [sdef34])).
% 15.06/2.63 cnf(p404, plain, ($false | ~spl34 | ~spl54), inference(resolution, [status(thm)], [p397, p323])).
% 15.06/2.63 cnf(sct14, plain, (~spl34 | ~spl54), inference(avatar_contradiction_clause, [status(thm)], [p404])).
% 15.06/2.63 fof(sdef56, definition, (spl56 <=> (~white(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl56])], [avatar_definition])).
% 15.06/2.63 cnf(p406, plain, (~white(sk6,sk10) | ~spl56), inference(avatar_component_clause, [status(thm)], [sdef56])).
% 15.06/2.63 fof(sdef9, definition, (spl9 <=> (white(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl9])], [avatar_definition])).
% 15.06/2.63 cnf(p18, plain, (white(sk6,sk10) | ~spl9), inference(avatar_component_clause, [status(thm)], [sdef9])).
% 15.06/2.63 cnf(p413, plain, ($false | ~spl9 | ~spl56), inference(resolution, [status(thm)], [p406, p18])).
% 15.06/2.63 cnf(sct15, plain, (~spl9 | ~spl56), inference(avatar_contradiction_clause, [status(thm)], [p413])).
% 15.06/2.63 fof(sdef57, definition, (spl57 <=> (~dirty(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl57])], [avatar_definition])).
% 15.06/2.63 cnf(p407, plain, (~dirty(sk6,sk10) | ~spl57), inference(avatar_component_clause, [status(thm)], [sdef57])).
% 15.06/2.63 fof(sdef10, definition, (spl10 <=> (dirty(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl10])], [avatar_definition])).
% 15.06/2.63 cnf(p20, plain, (dirty(sk6,sk10) | ~spl10), inference(avatar_component_clause, [status(thm)], [sdef10])).
% 15.06/2.63 cnf(p414, plain, ($false | ~spl10 | ~spl57), inference(resolution, [status(thm)], [p407, p20])).
% 15.06/2.63 cnf(sct16, plain, (~spl10 | ~spl57), inference(avatar_contradiction_clause, [status(thm)], [p414])).
% 15.06/2.63 fof(sdef58, definition, (spl58 <=> (~old(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl58])], [avatar_definition])).
% 15.06/2.63 cnf(p408, plain, (~old(sk6,sk10) | ~spl58), inference(avatar_component_clause, [status(thm)], [sdef58])).
% 15.06/2.63 fof(sdef11, definition, (spl11 <=> (old(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl11])], [avatar_definition])).
% 15.06/2.63 cnf(p22, plain, (old(sk6,sk10) | ~spl11), inference(avatar_component_clause, [status(thm)], [sdef11])).
% 15.06/2.63 cnf(p415, plain, ($false | ~spl11 | ~spl58), inference(resolution, [status(thm)], [p408, p22])).
% 15.06/2.63 cnf(sct17, plain, (~spl11 | ~spl58), inference(avatar_contradiction_clause, [status(thm)], [p415])).
% 15.06/2.63 fof(sdef60, definition, (spl60 <=> (~lonely(sk6,sk9))), introduced(definition, [new_symbols(naming, [spl60])], [avatar_definition])).
% 15.06/2.63 cnf(p411, plain, (~lonely(sk6,sk9) | ~spl60), inference(avatar_component_clause, [status(thm)], [sdef60])).
% 15.06/2.63 fof(sdef7, definition, (spl7 <=> (lonely(sk6,sk9))), introduced(definition, [new_symbols(naming, [spl7])], [avatar_definition])).
% 15.06/2.63 cnf(p14, plain, (lonely(sk6,sk9) | ~spl7), inference(avatar_component_clause, [status(thm)], [sdef7])).
% 15.06/2.63 cnf(p416, plain, ($false | ~spl7 | ~spl60), inference(resolution, [status(thm)], [p411, p14])).
% 15.06/2.63 cnf(sct18, plain, (~spl7 | ~spl60), inference(avatar_contradiction_clause, [status(thm)], [p416])).
% 15.06/2.63 fof(sdef64, definition, (spl64 <=> (~present(sk6,sk11))), introduced(definition, [new_symbols(naming, [spl64])], [avatar_definition])).
% 15.06/2.63 cnf(p421, plain, (~present(sk6,sk11) | ~spl64), inference(avatar_component_clause, [status(thm)], [sdef64])).
% 15.06/2.63 fof(sdef14, definition, (spl14 <=> (present(sk6,sk11))), introduced(definition, [new_symbols(naming, [spl14])], [avatar_definition])).
% 15.06/2.63 cnf(p28, plain, (present(sk6,sk11) | ~spl14), inference(avatar_component_clause, [status(thm)], [sdef14])).
% 15.06/2.63 cnf(p425, plain, ($false | ~spl14 | ~spl64), inference(resolution, [status(thm)], [p421, p28])).
% 15.06/2.63 cnf(sct19, plain, (~spl14 | ~spl64), inference(avatar_contradiction_clause, [status(thm)], [p425])).
% 15.06/2.63 fof(sdef65, definition, (spl65 <=> (~barrel(sk6,sk11))), introduced(definition, [new_symbols(naming, [spl65])], [avatar_definition])).
% 15.06/2.63 cnf(p422, plain, (~barrel(sk6,sk11) | ~spl65), inference(avatar_component_clause, [status(thm)], [sdef65])).
% 15.06/2.63 fof(sdef15, definition, (spl15 <=> (barrel(sk6,sk11))), introduced(definition, [new_symbols(naming, [spl15])], [avatar_definition])).
% 15.06/2.63 cnf(p30, plain, (barrel(sk6,sk11) | ~spl15), inference(avatar_component_clause, [status(thm)], [sdef15])).
% 15.06/2.63 cnf(p426, plain, ($false | ~spl15 | ~spl65), inference(resolution, [status(thm)], [p422, p30])).
% 15.06/2.63 cnf(sct20, plain, (~spl15 | ~spl65), inference(avatar_contradiction_clause, [status(thm)], [p426])).
% 15.06/2.63 fof(sdef63, definition, (spl63 <=> (~agent(sk6,sk11,sk10))), introduced(definition, [new_symbols(naming, [spl63])], [avatar_definition])).
% 15.06/2.63 cnf(p420, plain, (~agent(sk6,sk11,sk10) | ~spl63), inference(avatar_component_clause, [status(thm)], [sdef63])).
% 15.06/2.63 fof(sdef13, definition, (spl13 <=> (agent(sk6,sk11,sk10))), introduced(definition, [new_symbols(naming, [spl13])], [avatar_definition])).
% 15.06/2.63 cnf(p26, plain, (agent(sk6,sk11,sk10) | ~spl13), inference(avatar_component_clause, [status(thm)], [sdef13])).
% 15.06/2.63 cnf(p427, plain, ($false | ~spl13 | ~spl63), inference(resolution, [status(thm)], [p420, p26])).
% 15.06/2.63 cnf(sct21, plain, (~spl13 | ~spl63), inference(avatar_contradiction_clause, [status(thm)], [p427])).
% 15.06/2.63 fof(sdef66, definition, (spl66 <=> (~down(sk6,sk11,sk9))), introduced(definition, [new_symbols(naming, [spl66])], [avatar_definition])).
% 15.06/2.63 cnf(p423, plain, (~down(sk6,sk11,sk9) | ~spl66), inference(avatar_component_clause, [status(thm)], [sdef66])).
% 15.06/2.63 fof(sdef16, definition, (spl16 <=> (down(sk6,sk11,sk9))), introduced(definition, [new_symbols(naming, [spl16])], [avatar_definition])).
% 15.06/2.63 cnf(p32, plain, (down(sk6,sk11,sk9) | ~spl16), inference(avatar_component_clause, [status(thm)], [sdef16])).
% 15.06/2.63 cnf(p429, plain, ($false | ~spl16 | ~spl66), inference(resolution, [status(thm)], [p423, p32])).
% 15.06/2.63 cnf(sct22, plain, (~spl16 | ~spl66), inference(avatar_contradiction_clause, [status(thm)], [p429])).
% 15.06/2.63 fof(sdef67, definition, (spl67 <=> (~in(sk6,sk11,sk7))), introduced(definition, [new_symbols(naming, [spl67])], [avatar_definition])).
% 15.06/2.63 cnf(p424, plain, (~in(sk6,sk11,sk7) | ~spl67), inference(avatar_component_clause, [status(thm)], [sdef67])).
% 15.06/2.63 fof(sdef17, definition, (spl17 <=> (in(sk6,sk11,sk7))), introduced(definition, [new_symbols(naming, [spl17])], [avatar_definition])).
% 15.06/2.63 cnf(p34, plain, (in(sk6,sk11,sk7) | ~spl17), inference(avatar_component_clause, [status(thm)], [sdef17])).
% 15.06/2.63 cnf(p430, plain, ($false | ~spl17 | ~spl67), inference(resolution, [status(thm)], [p424, p34])).
% 15.06/2.63 cnf(sct23, plain, (~spl17 | ~spl67), inference(avatar_contradiction_clause, [status(thm)], [p430])).
% 15.06/2.63 fof(f0, conjecture, ~ ~ ( ( ? [U] : ( actual_world(U) & ? [V,W,X,Y,Z] : ( of(U,W,V) & city(U,V) & hollywood_placename(U,W) & placename(U,W) & chevy(U,X) & white(U,X) & dirty(U,X) & old(U,X) & street(U,Y) & lonely(U,Y) & event(U,Z) & agent(U,Z,X) & present(U,Z) & barrel(U,Z) & down(U,Z,Y) & in(U,Z,V) ) ) => ? [X1] : ( actual_world(X1) & ? [X2,X3,X4,X5,X6] : ( of(X1,X3,X2) & city(X1,X2) & hollywood_placename(X1,X3) & placename(X1,X3) & street(X1,X4) & lonely(X1,X4) & chevy(X1,X5) & white(X1,X5) & dirty(X1,X5) & old(X1,X5) & event(X1,X6) & agent(X1,X6,X5) & present(X1,X6) & barrel(X1,X6) & down(X1,X6,X4) & in(X1,X6,X2) ) ) ) & ( ? [X1] : ( actual_world(X1) & ? [X2,X3,X4,X5,X6] : ( of(X1,X3,X2) & city(X1,X2) & hollywood_placename(X1,X3) & placename(X1,X3) & street(X1,X4) & lonely(X1,X4) & chevy(X1,X5) & white(X1,X5) & dirty(X1,X5) & old(X1,X5) & event(X1,X6) & agent(X1,X6,X5) & present(X1,X6) & barrel(X1,X6) & down(X1,X6,X4) & in(X1,X6,X2) ) ) => ? [U] : ( actual_world(U) & ? [V,W,X,Y,Z] : ( of(U,W,V) & city(U,V) & hollywood_placename(U,W) & placename(U,W) & chevy(U,X) & white(U,X) & dirty(U,X) & old(U,X) & street(U,Y) & lonely(U,Y) & event(U,Z) & agent(U,Z,X) & present(U,Z) & barrel(U,Z) & down(U,Z,Y) & in(U,Z,V) ) ) ) ), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', co1)).
% 15.06/2.63 fof(f0_neg, negated_conjecture, ~(~ ~ ( ( ? [U] : ( actual_world(U) & ? [V,W,X,Y,Z] : ( of(U,W,V) & city(U,V) & hollywood_placename(U,W) & placename(U,W) & chevy(U,X) & white(U,X) & dirty(U,X) & old(U,X) & street(U,Y) & lonely(U,Y) & event(U,Z) & agent(U,Z,X) & present(U,Z) & barrel(U,Z) & down(U,Z,Y) & in(U,Z,V) ) ) => ? [X1] : ( actual_world(X1) & ? [X2,X3,X4,X5,X6] : ( of(X1,X3,X2) & city(X1,X2) & hollywood_placename(X1,X3) & placename(X1,X3) & street(X1,X4) & lonely(X1,X4) & chevy(X1,X5) & white(X1,X5) & dirty(X1,X5) & old(X1,X5) & event(X1,X6) & agent(X1,X6,X5) & present(X1,X6) & barrel(X1,X6) & down(X1,X6,X4) & in(X1,X6,X2) ) ) ) & ( ? [X1] : ( actual_world(X1) & ? [X2,X3,X4,X5,X6] : ( of(X1,X3,X2) & city(X1,X2) & hollywood_placename(X1,X3) & placename(X1,X3) & street(X1,X4) & lonely(X1,X4) & chevy(X1,X5) & white(X1,X5) & dirty(X1,X5) & old(X1,X5) & event(X1,X6) & agent(X1,X6,X5) & present(X1,X6) & barrel(X1,X6) & down(X1,X6,X4) & in(X1,X6,X2) ) ) => ? [U] : ( actual_world(U) & ? [V,W,X,Y,Z] : ( of(U,W,V) & city(U,V) & hollywood_placename(U,W) & placename(U,W) & chevy(U,X) & white(U,X) & dirty(U,X) & old(U,X) & street(U,Y) & lonely(U,Y) & event(U,Z) & agent(U,Z,X) & present(U,Z) & barrel(U,Z) & down(U,Z,Y) & in(U,Z,V) ) ) ) )), inference(negated_conjecture, [status(cth)], [f0])).
% 15.06/2.63 fof(f0_nnf, plain, ((? [U] : ((actual_world(U) & ? [V,W,X,Y,Z] : ((((((((((((((((of(U,W,V) & city(U,V)) & hollywood_placename(U,W)) & placename(U,W)) & chevy(U,X)) & white(U,X)) & dirty(U,X)) & old(U,X)) & street(U,Y)) & lonely(U,Y)) & event(U,Z)) & agent(U,Z,X)) & present(U,Z)) & barrel(U,Z)) & down(U,Z,Y)) & in(U,Z,V))))) & ! [X1] : ((~(actual_world(X1)) | ! [X2,X3,X4,X5,X6] : ((((((((((((((((~(of(X1,X3,X2)) | ~(city(X1,X2))) | ~(hollywood_placename(X1,X3))) | ~(placename(X1,X3))) | ~(street(X1,X4))) | ~(lonely(X1,X4))) | ~(chevy(X1,X5))) | ~(white(X1,X5))) | ~(dirty(X1,X5))) | ~(old(X1,X5))) | ~(event(X1,X6))) | ~(agent(X1,X6,X5))) | ~(present(X1,X6))) | ~(barrel(X1,X6))) | ~(down(X1,X6,X4))) | ~(in(X1,X6,X2))))))) | (? [X1] : ((actual_world(X1) & ? [X2,X3,X4,X5,X6] : ((((((((((((((((of(X1,X3,X2) & city(X1,X2)) & hollywood_placename(X1,X3)) & placename(X1,X3)) & street(X1,X4)) & lonely(X1,X4)) & chevy(X1,X5)) & white(X1,X5)) & dirty(X1,X5)) & old(X1,X5)) & event(X1,X6)) & agent(X1,X6,X5)) & present(X1,X6)) & barrel(X1,X6)) & down(X1,X6,X4)) & in(X1,X6,X2))))) & ! [U] : ((~(actual_world(U)) | ! [V,W,X,Y,Z] : ((((((((((((((((~(of(U,W,V)) | ~(city(U,V))) | ~(hollywood_placename(U,W))) | ~(placename(U,W))) | ~(chevy(U,X))) | ~(white(U,X))) | ~(dirty(U,X))) | ~(old(U,X))) | ~(street(U,Y))) | ~(lonely(U,Y))) | ~(event(U,Z))) | ~(agent(U,Z,X))) | ~(present(U,Z))) | ~(barrel(U,Z))) | ~(down(U,Z,Y))) | ~(in(U,Z,V)))))))), inference(nnf_transformation, [status(thm)], [f0_neg])).
% 15.06/2.63 fof(f0_sk, plain, ! [X1,X3,X2,X4,X5,X6,U,W,V,X,Y,Z] : ((((actual_world(sk0) & (((((((((((((((of(sk0,sk2,sk1) & city(sk0,sk1)) & hollywood_placename(sk0,sk2)) & placename(sk0,sk2)) & chevy(sk0,sk3)) & white(sk0,sk3)) & dirty(sk0,sk3)) & old(sk0,sk3)) & street(sk0,sk4)) & lonely(sk0,sk4)) & event(sk0,sk5)) & agent(sk0,sk5,sk3)) & present(sk0,sk5)) & barrel(sk0,sk5)) & down(sk0,sk5,sk4)) & in(sk0,sk5,sk1))) & (~(actual_world(X1)) | (((((((((((((((~(of(X1,X3,X2)) | ~(city(X1,X2))) | ~(hollywood_placename(X1,X3))) | ~(placename(X1,X3))) | ~(street(X1,X4))) | ~(lonely(X1,X4))) | ~(chevy(X1,X5))) | ~(white(X1,X5))) | ~(dirty(X1,X5))) | ~(old(X1,X5))) | ~(event(X1,X6))) | ~(agent(X1,X6,X5))) | ~(present(X1,X6))) | ~(barrel(X1,X6))) | ~(down(X1,X6,X4))) | ~(in(X1,X6,X2))))) | ((actual_world(sk6) & (((((((((((((((of(sk6,sk8,sk7) & city(sk6,sk7)) & hollywood_placename(sk6,sk8)) & placename(sk6,sk8)) & street(sk6,sk9)) & lonely(sk6,sk9)) & chevy(sk6,sk10)) & white(sk6,sk10)) & dirty(sk6,sk10)) & old(sk6,sk10)) & event(sk6,sk11)) & agent(sk6,sk11,sk10)) & present(sk6,sk11)) & barrel(sk6,sk11)) & down(sk6,sk11,sk9)) & in(sk6,sk11,sk7))) & (~(actual_world(U)) | (((((((((((((((~(of(U,W,V)) | ~(city(U,V))) | ~(hollywood_placename(U,W))) | ~(placename(U,W))) | ~(chevy(U,X))) | ~(white(U,X))) | ~(dirty(U,X))) | ~(old(U,X))) | ~(street(U,Y))) | ~(lonely(U,Y))) | ~(event(U,Z))) | ~(agent(U,Z,X))) | ~(present(U,Z))) | ~(barrel(U,Z))) | ~(down(U,Z,Y))) | ~(in(U,Z,V))))))), inference(skolemisation, [status(esa), new_symbols(skolem, [sk0,sk1,sk2,sk3,sk4,sk5,sk6,sk7,sk8,sk9,sk10,sk11])], [f0_nnf])).
% 15.06/2.63 cnf(c0, plain, actual_world(sk0) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef0, definition, (spl0 <=> (actual_world(sk0))), introduced(definition, [new_symbols(naming, [spl0])], [avatar_definition])).
% 15.06/2.63 fof(sdef1, definition, (spl1 <=> (actual_world(sk6))), introduced(definition, [new_symbols(naming, [spl1])], [avatar_definition])).
% 15.06/2.63 cnf(ssp0, plain, (spl0 | spl1), inference(avatar_split_clause, [status(thm)], [c0, sdef0, sdef1])).
% 15.06/2.63 cnf(c1, plain, actual_world(sk0) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef2, definition, (spl2 <=> (of(sk6,sk8,sk7))), introduced(definition, [new_symbols(naming, [spl2])], [avatar_definition])).
% 15.06/2.63 cnf(ssp1, plain, (spl0 | spl2), inference(avatar_split_clause, [status(thm)], [c1, sdef0, sdef2])).
% 15.06/2.63 cnf(c2, plain, actual_world(sk0) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp2, plain, (spl0 | spl3), inference(avatar_split_clause, [status(thm)], [c2, sdef0, sdef3])).
% 15.06/2.63 cnf(c3, plain, actual_world(sk0) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp3, plain, (spl0 | spl4), inference(avatar_split_clause, [status(thm)], [c3, sdef0, sdef4])).
% 15.06/2.63 cnf(c4, plain, actual_world(sk0) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp4, plain, (spl0 | spl5), inference(avatar_split_clause, [status(thm)], [c4, sdef0, sdef5])).
% 15.06/2.63 cnf(c5, plain, actual_world(sk0) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef6, definition, (spl6 <=> (street(sk6,sk9))), introduced(definition, [new_symbols(naming, [spl6])], [avatar_definition])).
% 15.06/2.63 cnf(ssp5, plain, (spl0 | spl6), inference(avatar_split_clause, [status(thm)], [c5, sdef0, sdef6])).
% 15.06/2.63 cnf(c6, plain, actual_world(sk0) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp6, plain, (spl0 | spl7), inference(avatar_split_clause, [status(thm)], [c6, sdef0, sdef7])).
% 15.06/2.63 cnf(c7, plain, actual_world(sk0) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef8, definition, (spl8 <=> (chevy(sk6,sk10))), introduced(definition, [new_symbols(naming, [spl8])], [avatar_definition])).
% 15.06/2.63 cnf(ssp7, plain, (spl0 | spl8), inference(avatar_split_clause, [status(thm)], [c7, sdef0, sdef8])).
% 15.06/2.63 cnf(c8, plain, actual_world(sk0) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp8, plain, (spl0 | spl9), inference(avatar_split_clause, [status(thm)], [c8, sdef0, sdef9])).
% 15.06/2.63 cnf(c9, plain, actual_world(sk0) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp9, plain, (spl0 | spl10), inference(avatar_split_clause, [status(thm)], [c9, sdef0, sdef10])).
% 15.06/2.63 cnf(c10, plain, actual_world(sk0) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp10, plain, (spl0 | spl11), inference(avatar_split_clause, [status(thm)], [c10, sdef0, sdef11])).
% 15.06/2.63 cnf(c11, plain, actual_world(sk0) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef12, definition, (spl12 <=> (event(sk6,sk11))), introduced(definition, [new_symbols(naming, [spl12])], [avatar_definition])).
% 15.06/2.63 cnf(ssp11, plain, (spl0 | spl12), inference(avatar_split_clause, [status(thm)], [c11, sdef0, sdef12])).
% 15.06/2.63 cnf(c12, plain, actual_world(sk0) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp12, plain, (spl0 | spl13), inference(avatar_split_clause, [status(thm)], [c12, sdef0, sdef13])).
% 15.06/2.63 cnf(c13, plain, actual_world(sk0) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp13, plain, (spl0 | spl14), inference(avatar_split_clause, [status(thm)], [c13, sdef0, sdef14])).
% 15.06/2.63 cnf(c14, plain, actual_world(sk0) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp14, plain, (spl0 | spl15), inference(avatar_split_clause, [status(thm)], [c14, sdef0, sdef15])).
% 15.06/2.63 cnf(c15, plain, actual_world(sk0) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp15, plain, (spl0 | spl16), inference(avatar_split_clause, [status(thm)], [c15, sdef0, sdef16])).
% 15.06/2.63 cnf(c16, plain, actual_world(sk0) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp16, plain, (spl0 | spl17), inference(avatar_split_clause, [status(thm)], [c16, sdef0, sdef17])).
% 15.06/2.63 cnf(c17, plain, actual_world(sk0) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef18, definition, (spl18 <=> (~actual_world(X0) | ~of(X0,X1,X2) | ~city(X0,X2) | ~hollywood_placename(X0,X1) | ~placename(X0,X1) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X2))), introduced(definition, [new_symbols(naming, [spl18])], [avatar_definition])).
% 15.06/2.63 cnf(ssp17, plain, (spl0 | spl18), inference(avatar_split_clause, [status(thm)], [c17, sdef0, sdef18])).
% 15.06/2.63 cnf(c18, plain, of(sk0,sk2,sk1) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef19, definition, (spl19 <=> (of(sk0,sk2,sk1))), introduced(definition, [new_symbols(naming, [spl19])], [avatar_definition])).
% 15.06/2.63 cnf(ssp18, plain, (spl1 | spl19), inference(avatar_split_clause, [status(thm)], [c18, sdef1, sdef19])).
% 15.06/2.63 cnf(c19, plain, of(sk0,sk2,sk1) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp19, plain, (spl2 | spl19), inference(avatar_split_clause, [status(thm)], [c19, sdef2, sdef19])).
% 15.06/2.63 cnf(c20, plain, of(sk0,sk2,sk1) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp20, plain, (spl3 | spl19), inference(avatar_split_clause, [status(thm)], [c20, sdef3, sdef19])).
% 15.06/2.63 cnf(c21, plain, of(sk0,sk2,sk1) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp21, plain, (spl4 | spl19), inference(avatar_split_clause, [status(thm)], [c21, sdef4, sdef19])).
% 15.06/2.63 cnf(c22, plain, of(sk0,sk2,sk1) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp22, plain, (spl5 | spl19), inference(avatar_split_clause, [status(thm)], [c22, sdef5, sdef19])).
% 15.06/2.63 cnf(c23, plain, of(sk0,sk2,sk1) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp23, plain, (spl6 | spl19), inference(avatar_split_clause, [status(thm)], [c23, sdef6, sdef19])).
% 15.06/2.63 cnf(c24, plain, of(sk0,sk2,sk1) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp24, plain, (spl7 | spl19), inference(avatar_split_clause, [status(thm)], [c24, sdef7, sdef19])).
% 15.06/2.63 cnf(c25, plain, of(sk0,sk2,sk1) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp25, plain, (spl8 | spl19), inference(avatar_split_clause, [status(thm)], [c25, sdef8, sdef19])).
% 15.06/2.63 cnf(c26, plain, of(sk0,sk2,sk1) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp26, plain, (spl9 | spl19), inference(avatar_split_clause, [status(thm)], [c26, sdef9, sdef19])).
% 15.06/2.63 cnf(c27, plain, of(sk0,sk2,sk1) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp27, plain, (spl10 | spl19), inference(avatar_split_clause, [status(thm)], [c27, sdef10, sdef19])).
% 15.06/2.63 cnf(c28, plain, of(sk0,sk2,sk1) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp28, plain, (spl11 | spl19), inference(avatar_split_clause, [status(thm)], [c28, sdef11, sdef19])).
% 15.06/2.63 cnf(c29, plain, of(sk0,sk2,sk1) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp29, plain, (spl12 | spl19), inference(avatar_split_clause, [status(thm)], [c29, sdef12, sdef19])).
% 15.06/2.63 cnf(c30, plain, of(sk0,sk2,sk1) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp30, plain, (spl13 | spl19), inference(avatar_split_clause, [status(thm)], [c30, sdef13, sdef19])).
% 15.06/2.63 cnf(c31, plain, of(sk0,sk2,sk1) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp31, plain, (spl14 | spl19), inference(avatar_split_clause, [status(thm)], [c31, sdef14, sdef19])).
% 15.06/2.63 cnf(c32, plain, of(sk0,sk2,sk1) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp32, plain, (spl15 | spl19), inference(avatar_split_clause, [status(thm)], [c32, sdef15, sdef19])).
% 15.06/2.63 cnf(c33, plain, of(sk0,sk2,sk1) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp33, plain, (spl16 | spl19), inference(avatar_split_clause, [status(thm)], [c33, sdef16, sdef19])).
% 15.06/2.63 cnf(c34, plain, of(sk0,sk2,sk1) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp34, plain, (spl17 | spl19), inference(avatar_split_clause, [status(thm)], [c34, sdef17, sdef19])).
% 15.06/2.63 cnf(c35, plain, of(sk0,sk2,sk1) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp35, plain, (spl18 | spl19), inference(avatar_split_clause, [status(thm)], [c35, sdef18, sdef19])).
% 15.06/2.63 cnf(c36, plain, city(sk0,sk1) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp36, plain, (spl1 | spl20), inference(avatar_split_clause, [status(thm)], [c36, sdef1, sdef20])).
% 15.06/2.63 cnf(c37, plain, city(sk0,sk1) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp37, plain, (spl2 | spl20), inference(avatar_split_clause, [status(thm)], [c37, sdef2, sdef20])).
% 15.06/2.63 cnf(c38, plain, city(sk0,sk1) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp38, plain, (spl3 | spl20), inference(avatar_split_clause, [status(thm)], [c38, sdef3, sdef20])).
% 15.06/2.63 cnf(c39, plain, city(sk0,sk1) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp39, plain, (spl4 | spl20), inference(avatar_split_clause, [status(thm)], [c39, sdef4, sdef20])).
% 15.06/2.63 cnf(c40, plain, city(sk0,sk1) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp40, plain, (spl5 | spl20), inference(avatar_split_clause, [status(thm)], [c40, sdef5, sdef20])).
% 15.06/2.63 cnf(c41, plain, city(sk0,sk1) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp41, plain, (spl6 | spl20), inference(avatar_split_clause, [status(thm)], [c41, sdef6, sdef20])).
% 15.06/2.63 cnf(c42, plain, city(sk0,sk1) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp42, plain, (spl7 | spl20), inference(avatar_split_clause, [status(thm)], [c42, sdef7, sdef20])).
% 15.06/2.63 cnf(c43, plain, city(sk0,sk1) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp43, plain, (spl8 | spl20), inference(avatar_split_clause, [status(thm)], [c43, sdef8, sdef20])).
% 15.06/2.63 cnf(c44, plain, city(sk0,sk1) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp44, plain, (spl9 | spl20), inference(avatar_split_clause, [status(thm)], [c44, sdef9, sdef20])).
% 15.06/2.63 cnf(c45, plain, city(sk0,sk1) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp45, plain, (spl10 | spl20), inference(avatar_split_clause, [status(thm)], [c45, sdef10, sdef20])).
% 15.06/2.63 cnf(c46, plain, city(sk0,sk1) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp46, plain, (spl11 | spl20), inference(avatar_split_clause, [status(thm)], [c46, sdef11, sdef20])).
% 15.06/2.63 cnf(c47, plain, city(sk0,sk1) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp47, plain, (spl12 | spl20), inference(avatar_split_clause, [status(thm)], [c47, sdef12, sdef20])).
% 15.06/2.63 cnf(c48, plain, city(sk0,sk1) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp48, plain, (spl13 | spl20), inference(avatar_split_clause, [status(thm)], [c48, sdef13, sdef20])).
% 15.06/2.63 cnf(c49, plain, city(sk0,sk1) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp49, plain, (spl14 | spl20), inference(avatar_split_clause, [status(thm)], [c49, sdef14, sdef20])).
% 15.06/2.63 cnf(c50, plain, city(sk0,sk1) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp50, plain, (spl15 | spl20), inference(avatar_split_clause, [status(thm)], [c50, sdef15, sdef20])).
% 15.06/2.63 cnf(c51, plain, city(sk0,sk1) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp51, plain, (spl16 | spl20), inference(avatar_split_clause, [status(thm)], [c51, sdef16, sdef20])).
% 15.06/2.63 cnf(c52, plain, city(sk0,sk1) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp52, plain, (spl17 | spl20), inference(avatar_split_clause, [status(thm)], [c52, sdef17, sdef20])).
% 15.06/2.63 cnf(c53, plain, city(sk0,sk1) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp53, plain, (spl18 | spl20), inference(avatar_split_clause, [status(thm)], [c53, sdef18, sdef20])).
% 15.06/2.63 cnf(c54, plain, hollywood_placename(sk0,sk2) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp54, plain, (spl1 | spl21), inference(avatar_split_clause, [status(thm)], [c54, sdef1, sdef21])).
% 15.06/2.63 cnf(c55, plain, hollywood_placename(sk0,sk2) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp55, plain, (spl2 | spl21), inference(avatar_split_clause, [status(thm)], [c55, sdef2, sdef21])).
% 15.06/2.63 cnf(c56, plain, hollywood_placename(sk0,sk2) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp56, plain, (spl3 | spl21), inference(avatar_split_clause, [status(thm)], [c56, sdef3, sdef21])).
% 15.06/2.63 cnf(c57, plain, hollywood_placename(sk0,sk2) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp57, plain, (spl4 | spl21), inference(avatar_split_clause, [status(thm)], [c57, sdef4, sdef21])).
% 15.06/2.63 cnf(c58, plain, hollywood_placename(sk0,sk2) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp58, plain, (spl5 | spl21), inference(avatar_split_clause, [status(thm)], [c58, sdef5, sdef21])).
% 15.06/2.63 cnf(c59, plain, hollywood_placename(sk0,sk2) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp59, plain, (spl6 | spl21), inference(avatar_split_clause, [status(thm)], [c59, sdef6, sdef21])).
% 15.06/2.63 cnf(c60, plain, hollywood_placename(sk0,sk2) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp60, plain, (spl7 | spl21), inference(avatar_split_clause, [status(thm)], [c60, sdef7, sdef21])).
% 15.06/2.63 cnf(c61, plain, hollywood_placename(sk0,sk2) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp61, plain, (spl8 | spl21), inference(avatar_split_clause, [status(thm)], [c61, sdef8, sdef21])).
% 15.06/2.63 cnf(c62, plain, hollywood_placename(sk0,sk2) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp62, plain, (spl9 | spl21), inference(avatar_split_clause, [status(thm)], [c62, sdef9, sdef21])).
% 15.06/2.63 cnf(c63, plain, hollywood_placename(sk0,sk2) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp63, plain, (spl10 | spl21), inference(avatar_split_clause, [status(thm)], [c63, sdef10, sdef21])).
% 15.06/2.63 cnf(c64, plain, hollywood_placename(sk0,sk2) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp64, plain, (spl11 | spl21), inference(avatar_split_clause, [status(thm)], [c64, sdef11, sdef21])).
% 15.06/2.63 cnf(c65, plain, hollywood_placename(sk0,sk2) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp65, plain, (spl12 | spl21), inference(avatar_split_clause, [status(thm)], [c65, sdef12, sdef21])).
% 15.06/2.63 cnf(c66, plain, hollywood_placename(sk0,sk2) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp66, plain, (spl13 | spl21), inference(avatar_split_clause, [status(thm)], [c66, sdef13, sdef21])).
% 15.06/2.63 cnf(c67, plain, hollywood_placename(sk0,sk2) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp67, plain, (spl14 | spl21), inference(avatar_split_clause, [status(thm)], [c67, sdef14, sdef21])).
% 15.06/2.63 cnf(c68, plain, hollywood_placename(sk0,sk2) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp68, plain, (spl15 | spl21), inference(avatar_split_clause, [status(thm)], [c68, sdef15, sdef21])).
% 15.06/2.63 cnf(c69, plain, hollywood_placename(sk0,sk2) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp69, plain, (spl16 | spl21), inference(avatar_split_clause, [status(thm)], [c69, sdef16, sdef21])).
% 15.06/2.63 cnf(c70, plain, hollywood_placename(sk0,sk2) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp70, plain, (spl17 | spl21), inference(avatar_split_clause, [status(thm)], [c70, sdef17, sdef21])).
% 15.06/2.63 cnf(c71, plain, hollywood_placename(sk0,sk2) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp71, plain, (spl18 | spl21), inference(avatar_split_clause, [status(thm)], [c71, sdef18, sdef21])).
% 15.06/2.63 cnf(c72, plain, placename(sk0,sk2) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp72, plain, (spl1 | spl22), inference(avatar_split_clause, [status(thm)], [c72, sdef1, sdef22])).
% 15.06/2.63 cnf(c73, plain, placename(sk0,sk2) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp73, plain, (spl2 | spl22), inference(avatar_split_clause, [status(thm)], [c73, sdef2, sdef22])).
% 15.06/2.63 cnf(c74, plain, placename(sk0,sk2) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp74, plain, (spl3 | spl22), inference(avatar_split_clause, [status(thm)], [c74, sdef3, sdef22])).
% 15.06/2.63 cnf(c75, plain, placename(sk0,sk2) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp75, plain, (spl4 | spl22), inference(avatar_split_clause, [status(thm)], [c75, sdef4, sdef22])).
% 15.06/2.63 cnf(c76, plain, placename(sk0,sk2) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp76, plain, (spl5 | spl22), inference(avatar_split_clause, [status(thm)], [c76, sdef5, sdef22])).
% 15.06/2.63 cnf(c77, plain, placename(sk0,sk2) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp77, plain, (spl6 | spl22), inference(avatar_split_clause, [status(thm)], [c77, sdef6, sdef22])).
% 15.06/2.63 cnf(c78, plain, placename(sk0,sk2) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp78, plain, (spl7 | spl22), inference(avatar_split_clause, [status(thm)], [c78, sdef7, sdef22])).
% 15.06/2.63 cnf(c79, plain, placename(sk0,sk2) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp79, plain, (spl8 | spl22), inference(avatar_split_clause, [status(thm)], [c79, sdef8, sdef22])).
% 15.06/2.63 cnf(c80, plain, placename(sk0,sk2) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp80, plain, (spl9 | spl22), inference(avatar_split_clause, [status(thm)], [c80, sdef9, sdef22])).
% 15.06/2.63 cnf(c81, plain, placename(sk0,sk2) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp81, plain, (spl10 | spl22), inference(avatar_split_clause, [status(thm)], [c81, sdef10, sdef22])).
% 15.06/2.63 cnf(c82, plain, placename(sk0,sk2) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp82, plain, (spl11 | spl22), inference(avatar_split_clause, [status(thm)], [c82, sdef11, sdef22])).
% 15.06/2.63 cnf(c83, plain, placename(sk0,sk2) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp83, plain, (spl12 | spl22), inference(avatar_split_clause, [status(thm)], [c83, sdef12, sdef22])).
% 15.06/2.63 cnf(c84, plain, placename(sk0,sk2) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp84, plain, (spl13 | spl22), inference(avatar_split_clause, [status(thm)], [c84, sdef13, sdef22])).
% 15.06/2.63 cnf(c85, plain, placename(sk0,sk2) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp85, plain, (spl14 | spl22), inference(avatar_split_clause, [status(thm)], [c85, sdef14, sdef22])).
% 15.06/2.63 cnf(c86, plain, placename(sk0,sk2) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp86, plain, (spl15 | spl22), inference(avatar_split_clause, [status(thm)], [c86, sdef15, sdef22])).
% 15.06/2.63 cnf(c87, plain, placename(sk0,sk2) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp87, plain, (spl16 | spl22), inference(avatar_split_clause, [status(thm)], [c87, sdef16, sdef22])).
% 15.06/2.63 cnf(c88, plain, placename(sk0,sk2) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp88, plain, (spl17 | spl22), inference(avatar_split_clause, [status(thm)], [c88, sdef17, sdef22])).
% 15.06/2.63 cnf(c89, plain, placename(sk0,sk2) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp89, plain, (spl18 | spl22), inference(avatar_split_clause, [status(thm)], [c89, sdef18, sdef22])).
% 15.06/2.63 cnf(c90, plain, chevy(sk0,sk3) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef23, definition, (spl23 <=> (chevy(sk0,sk3))), introduced(definition, [new_symbols(naming, [spl23])], [avatar_definition])).
% 15.06/2.63 cnf(ssp90, plain, (spl1 | spl23), inference(avatar_split_clause, [status(thm)], [c90, sdef1, sdef23])).
% 15.06/2.63 cnf(c91, plain, chevy(sk0,sk3) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp91, plain, (spl2 | spl23), inference(avatar_split_clause, [status(thm)], [c91, sdef2, sdef23])).
% 15.06/2.63 cnf(c92, plain, chevy(sk0,sk3) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp92, plain, (spl3 | spl23), inference(avatar_split_clause, [status(thm)], [c92, sdef3, sdef23])).
% 15.06/2.63 cnf(c93, plain, chevy(sk0,sk3) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp93, plain, (spl4 | spl23), inference(avatar_split_clause, [status(thm)], [c93, sdef4, sdef23])).
% 15.06/2.63 cnf(c94, plain, chevy(sk0,sk3) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp94, plain, (spl5 | spl23), inference(avatar_split_clause, [status(thm)], [c94, sdef5, sdef23])).
% 15.06/2.63 cnf(c95, plain, chevy(sk0,sk3) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp95, plain, (spl6 | spl23), inference(avatar_split_clause, [status(thm)], [c95, sdef6, sdef23])).
% 15.06/2.63 cnf(c96, plain, chevy(sk0,sk3) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp96, plain, (spl7 | spl23), inference(avatar_split_clause, [status(thm)], [c96, sdef7, sdef23])).
% 15.06/2.63 cnf(c97, plain, chevy(sk0,sk3) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp97, plain, (spl8 | spl23), inference(avatar_split_clause, [status(thm)], [c97, sdef8, sdef23])).
% 15.06/2.63 cnf(c98, plain, chevy(sk0,sk3) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp98, plain, (spl9 | spl23), inference(avatar_split_clause, [status(thm)], [c98, sdef9, sdef23])).
% 15.06/2.63 cnf(c99, plain, chevy(sk0,sk3) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp99, plain, (spl10 | spl23), inference(avatar_split_clause, [status(thm)], [c99, sdef10, sdef23])).
% 15.06/2.63 cnf(c100, plain, chevy(sk0,sk3) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp100, plain, (spl11 | spl23), inference(avatar_split_clause, [status(thm)], [c100, sdef11, sdef23])).
% 15.06/2.63 cnf(c101, plain, chevy(sk0,sk3) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp101, plain, (spl12 | spl23), inference(avatar_split_clause, [status(thm)], [c101, sdef12, sdef23])).
% 15.06/2.63 cnf(c102, plain, chevy(sk0,sk3) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp102, plain, (spl13 | spl23), inference(avatar_split_clause, [status(thm)], [c102, sdef13, sdef23])).
% 15.06/2.63 cnf(c103, plain, chevy(sk0,sk3) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp103, plain, (spl14 | spl23), inference(avatar_split_clause, [status(thm)], [c103, sdef14, sdef23])).
% 15.06/2.63 cnf(c104, plain, chevy(sk0,sk3) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp104, plain, (spl15 | spl23), inference(avatar_split_clause, [status(thm)], [c104, sdef15, sdef23])).
% 15.06/2.63 cnf(c105, plain, chevy(sk0,sk3) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp105, plain, (spl16 | spl23), inference(avatar_split_clause, [status(thm)], [c105, sdef16, sdef23])).
% 15.06/2.63 cnf(c106, plain, chevy(sk0,sk3) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp106, plain, (spl17 | spl23), inference(avatar_split_clause, [status(thm)], [c106, sdef17, sdef23])).
% 15.06/2.63 cnf(c107, plain, chevy(sk0,sk3) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp107, plain, (spl18 | spl23), inference(avatar_split_clause, [status(thm)], [c107, sdef18, sdef23])).
% 15.06/2.63 cnf(c108, plain, white(sk0,sk3) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp108, plain, (spl1 | spl24), inference(avatar_split_clause, [status(thm)], [c108, sdef1, sdef24])).
% 15.06/2.63 cnf(c109, plain, white(sk0,sk3) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp109, plain, (spl2 | spl24), inference(avatar_split_clause, [status(thm)], [c109, sdef2, sdef24])).
% 15.06/2.63 cnf(c110, plain, white(sk0,sk3) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp110, plain, (spl3 | spl24), inference(avatar_split_clause, [status(thm)], [c110, sdef3, sdef24])).
% 15.06/2.63 cnf(c111, plain, white(sk0,sk3) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp111, plain, (spl4 | spl24), inference(avatar_split_clause, [status(thm)], [c111, sdef4, sdef24])).
% 15.06/2.63 cnf(c112, plain, white(sk0,sk3) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp112, plain, (spl5 | spl24), inference(avatar_split_clause, [status(thm)], [c112, sdef5, sdef24])).
% 15.06/2.63 cnf(c113, plain, white(sk0,sk3) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp113, plain, (spl6 | spl24), inference(avatar_split_clause, [status(thm)], [c113, sdef6, sdef24])).
% 15.06/2.63 cnf(c114, plain, white(sk0,sk3) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp114, plain, (spl7 | spl24), inference(avatar_split_clause, [status(thm)], [c114, sdef7, sdef24])).
% 15.06/2.63 cnf(c115, plain, white(sk0,sk3) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp115, plain, (spl8 | spl24), inference(avatar_split_clause, [status(thm)], [c115, sdef8, sdef24])).
% 15.06/2.63 cnf(c116, plain, white(sk0,sk3) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp116, plain, (spl9 | spl24), inference(avatar_split_clause, [status(thm)], [c116, sdef9, sdef24])).
% 15.06/2.63 cnf(c117, plain, white(sk0,sk3) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp117, plain, (spl10 | spl24), inference(avatar_split_clause, [status(thm)], [c117, sdef10, sdef24])).
% 15.06/2.63 cnf(c118, plain, white(sk0,sk3) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp118, plain, (spl11 | spl24), inference(avatar_split_clause, [status(thm)], [c118, sdef11, sdef24])).
% 15.06/2.63 cnf(c119, plain, white(sk0,sk3) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp119, plain, (spl12 | spl24), inference(avatar_split_clause, [status(thm)], [c119, sdef12, sdef24])).
% 15.06/2.63 cnf(c120, plain, white(sk0,sk3) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp120, plain, (spl13 | spl24), inference(avatar_split_clause, [status(thm)], [c120, sdef13, sdef24])).
% 15.06/2.63 cnf(c121, plain, white(sk0,sk3) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp121, plain, (spl14 | spl24), inference(avatar_split_clause, [status(thm)], [c121, sdef14, sdef24])).
% 15.06/2.63 cnf(c122, plain, white(sk0,sk3) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp122, plain, (spl15 | spl24), inference(avatar_split_clause, [status(thm)], [c122, sdef15, sdef24])).
% 15.06/2.63 cnf(c123, plain, white(sk0,sk3) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp123, plain, (spl16 | spl24), inference(avatar_split_clause, [status(thm)], [c123, sdef16, sdef24])).
% 15.06/2.63 cnf(c124, plain, white(sk0,sk3) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp124, plain, (spl17 | spl24), inference(avatar_split_clause, [status(thm)], [c124, sdef17, sdef24])).
% 15.06/2.63 cnf(c125, plain, white(sk0,sk3) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp125, plain, (spl18 | spl24), inference(avatar_split_clause, [status(thm)], [c125, sdef18, sdef24])).
% 15.06/2.63 cnf(c126, plain, dirty(sk0,sk3) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp126, plain, (spl1 | spl25), inference(avatar_split_clause, [status(thm)], [c126, sdef1, sdef25])).
% 15.06/2.63 cnf(c127, plain, dirty(sk0,sk3) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp127, plain, (spl2 | spl25), inference(avatar_split_clause, [status(thm)], [c127, sdef2, sdef25])).
% 15.06/2.63 cnf(c128, plain, dirty(sk0,sk3) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp128, plain, (spl3 | spl25), inference(avatar_split_clause, [status(thm)], [c128, sdef3, sdef25])).
% 15.06/2.63 cnf(c129, plain, dirty(sk0,sk3) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp129, plain, (spl4 | spl25), inference(avatar_split_clause, [status(thm)], [c129, sdef4, sdef25])).
% 15.06/2.63 cnf(c130, plain, dirty(sk0,sk3) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp130, plain, (spl5 | spl25), inference(avatar_split_clause, [status(thm)], [c130, sdef5, sdef25])).
% 15.06/2.63 cnf(c131, plain, dirty(sk0,sk3) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp131, plain, (spl6 | spl25), inference(avatar_split_clause, [status(thm)], [c131, sdef6, sdef25])).
% 15.06/2.63 cnf(c132, plain, dirty(sk0,sk3) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp132, plain, (spl7 | spl25), inference(avatar_split_clause, [status(thm)], [c132, sdef7, sdef25])).
% 15.06/2.63 cnf(c133, plain, dirty(sk0,sk3) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp133, plain, (spl8 | spl25), inference(avatar_split_clause, [status(thm)], [c133, sdef8, sdef25])).
% 15.06/2.63 cnf(c134, plain, dirty(sk0,sk3) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp134, plain, (spl9 | spl25), inference(avatar_split_clause, [status(thm)], [c134, sdef9, sdef25])).
% 15.06/2.63 cnf(c135, plain, dirty(sk0,sk3) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp135, plain, (spl10 | spl25), inference(avatar_split_clause, [status(thm)], [c135, sdef10, sdef25])).
% 15.06/2.63 cnf(c136, plain, dirty(sk0,sk3) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp136, plain, (spl11 | spl25), inference(avatar_split_clause, [status(thm)], [c136, sdef11, sdef25])).
% 15.06/2.63 cnf(c137, plain, dirty(sk0,sk3) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp137, plain, (spl12 | spl25), inference(avatar_split_clause, [status(thm)], [c137, sdef12, sdef25])).
% 15.06/2.63 cnf(c138, plain, dirty(sk0,sk3) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp138, plain, (spl13 | spl25), inference(avatar_split_clause, [status(thm)], [c138, sdef13, sdef25])).
% 15.06/2.63 cnf(c139, plain, dirty(sk0,sk3) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp139, plain, (spl14 | spl25), inference(avatar_split_clause, [status(thm)], [c139, sdef14, sdef25])).
% 15.06/2.63 cnf(c140, plain, dirty(sk0,sk3) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp140, plain, (spl15 | spl25), inference(avatar_split_clause, [status(thm)], [c140, sdef15, sdef25])).
% 15.06/2.63 cnf(c141, plain, dirty(sk0,sk3) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp141, plain, (spl16 | spl25), inference(avatar_split_clause, [status(thm)], [c141, sdef16, sdef25])).
% 15.06/2.63 cnf(c142, plain, dirty(sk0,sk3) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp142, plain, (spl17 | spl25), inference(avatar_split_clause, [status(thm)], [c142, sdef17, sdef25])).
% 15.06/2.63 cnf(c143, plain, dirty(sk0,sk3) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp143, plain, (spl18 | spl25), inference(avatar_split_clause, [status(thm)], [c143, sdef18, sdef25])).
% 15.06/2.63 cnf(c144, plain, old(sk0,sk3) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp144, plain, (spl1 | spl26), inference(avatar_split_clause, [status(thm)], [c144, sdef1, sdef26])).
% 15.06/2.63 cnf(c145, plain, old(sk0,sk3) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp145, plain, (spl2 | spl26), inference(avatar_split_clause, [status(thm)], [c145, sdef2, sdef26])).
% 15.06/2.63 cnf(c146, plain, old(sk0,sk3) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp146, plain, (spl3 | spl26), inference(avatar_split_clause, [status(thm)], [c146, sdef3, sdef26])).
% 15.06/2.63 cnf(c147, plain, old(sk0,sk3) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp147, plain, (spl4 | spl26), inference(avatar_split_clause, [status(thm)], [c147, sdef4, sdef26])).
% 15.06/2.63 cnf(c148, plain, old(sk0,sk3) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp148, plain, (spl5 | spl26), inference(avatar_split_clause, [status(thm)], [c148, sdef5, sdef26])).
% 15.06/2.63 cnf(c149, plain, old(sk0,sk3) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp149, plain, (spl6 | spl26), inference(avatar_split_clause, [status(thm)], [c149, sdef6, sdef26])).
% 15.06/2.63 cnf(c150, plain, old(sk0,sk3) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp150, plain, (spl7 | spl26), inference(avatar_split_clause, [status(thm)], [c150, sdef7, sdef26])).
% 15.06/2.63 cnf(c151, plain, old(sk0,sk3) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp151, plain, (spl8 | spl26), inference(avatar_split_clause, [status(thm)], [c151, sdef8, sdef26])).
% 15.06/2.63 cnf(c152, plain, old(sk0,sk3) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp152, plain, (spl9 | spl26), inference(avatar_split_clause, [status(thm)], [c152, sdef9, sdef26])).
% 15.06/2.63 cnf(c153, plain, old(sk0,sk3) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp153, plain, (spl10 | spl26), inference(avatar_split_clause, [status(thm)], [c153, sdef10, sdef26])).
% 15.06/2.63 cnf(c154, plain, old(sk0,sk3) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp154, plain, (spl11 | spl26), inference(avatar_split_clause, [status(thm)], [c154, sdef11, sdef26])).
% 15.06/2.63 cnf(c155, plain, old(sk0,sk3) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp155, plain, (spl12 | spl26), inference(avatar_split_clause, [status(thm)], [c155, sdef12, sdef26])).
% 15.06/2.63 cnf(c156, plain, old(sk0,sk3) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp156, plain, (spl13 | spl26), inference(avatar_split_clause, [status(thm)], [c156, sdef13, sdef26])).
% 15.06/2.63 cnf(c157, plain, old(sk0,sk3) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp157, plain, (spl14 | spl26), inference(avatar_split_clause, [status(thm)], [c157, sdef14, sdef26])).
% 15.06/2.63 cnf(c158, plain, old(sk0,sk3) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp158, plain, (spl15 | spl26), inference(avatar_split_clause, [status(thm)], [c158, sdef15, sdef26])).
% 15.06/2.63 cnf(c159, plain, old(sk0,sk3) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp159, plain, (spl16 | spl26), inference(avatar_split_clause, [status(thm)], [c159, sdef16, sdef26])).
% 15.06/2.63 cnf(c160, plain, old(sk0,sk3) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp160, plain, (spl17 | spl26), inference(avatar_split_clause, [status(thm)], [c160, sdef17, sdef26])).
% 15.06/2.63 cnf(c161, plain, old(sk0,sk3) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp161, plain, (spl18 | spl26), inference(avatar_split_clause, [status(thm)], [c161, sdef18, sdef26])).
% 15.06/2.63 cnf(c162, plain, street(sk0,sk4) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef27, definition, (spl27 <=> (street(sk0,sk4))), introduced(definition, [new_symbols(naming, [spl27])], [avatar_definition])).
% 15.06/2.63 cnf(ssp162, plain, (spl1 | spl27), inference(avatar_split_clause, [status(thm)], [c162, sdef1, sdef27])).
% 15.06/2.63 cnf(c163, plain, street(sk0,sk4) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp163, plain, (spl2 | spl27), inference(avatar_split_clause, [status(thm)], [c163, sdef2, sdef27])).
% 15.06/2.63 cnf(c164, plain, street(sk0,sk4) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp164, plain, (spl3 | spl27), inference(avatar_split_clause, [status(thm)], [c164, sdef3, sdef27])).
% 15.06/2.63 cnf(c165, plain, street(sk0,sk4) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp165, plain, (spl4 | spl27), inference(avatar_split_clause, [status(thm)], [c165, sdef4, sdef27])).
% 15.06/2.63 cnf(c166, plain, street(sk0,sk4) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp166, plain, (spl5 | spl27), inference(avatar_split_clause, [status(thm)], [c166, sdef5, sdef27])).
% 15.06/2.63 cnf(c167, plain, street(sk0,sk4) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp167, plain, (spl6 | spl27), inference(avatar_split_clause, [status(thm)], [c167, sdef6, sdef27])).
% 15.06/2.63 cnf(c168, plain, street(sk0,sk4) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp168, plain, (spl7 | spl27), inference(avatar_split_clause, [status(thm)], [c168, sdef7, sdef27])).
% 15.06/2.63 cnf(c169, plain, street(sk0,sk4) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp169, plain, (spl8 | spl27), inference(avatar_split_clause, [status(thm)], [c169, sdef8, sdef27])).
% 15.06/2.63 cnf(c170, plain, street(sk0,sk4) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp170, plain, (spl9 | spl27), inference(avatar_split_clause, [status(thm)], [c170, sdef9, sdef27])).
% 15.06/2.63 cnf(c171, plain, street(sk0,sk4) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp171, plain, (spl10 | spl27), inference(avatar_split_clause, [status(thm)], [c171, sdef10, sdef27])).
% 15.06/2.63 cnf(c172, plain, street(sk0,sk4) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp172, plain, (spl11 | spl27), inference(avatar_split_clause, [status(thm)], [c172, sdef11, sdef27])).
% 15.06/2.63 cnf(c173, plain, street(sk0,sk4) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp173, plain, (spl12 | spl27), inference(avatar_split_clause, [status(thm)], [c173, sdef12, sdef27])).
% 15.06/2.63 cnf(c174, plain, street(sk0,sk4) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp174, plain, (spl13 | spl27), inference(avatar_split_clause, [status(thm)], [c174, sdef13, sdef27])).
% 15.06/2.63 cnf(c175, plain, street(sk0,sk4) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp175, plain, (spl14 | spl27), inference(avatar_split_clause, [status(thm)], [c175, sdef14, sdef27])).
% 15.06/2.63 cnf(c176, plain, street(sk0,sk4) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp176, plain, (spl15 | spl27), inference(avatar_split_clause, [status(thm)], [c176, sdef15, sdef27])).
% 15.06/2.63 cnf(c177, plain, street(sk0,sk4) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp177, plain, (spl16 | spl27), inference(avatar_split_clause, [status(thm)], [c177, sdef16, sdef27])).
% 15.06/2.63 cnf(c178, plain, street(sk0,sk4) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp178, plain, (spl17 | spl27), inference(avatar_split_clause, [status(thm)], [c178, sdef17, sdef27])).
% 15.06/2.63 cnf(c179, plain, street(sk0,sk4) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp179, plain, (spl18 | spl27), inference(avatar_split_clause, [status(thm)], [c179, sdef18, sdef27])).
% 15.06/2.63 cnf(c180, plain, lonely(sk0,sk4) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp180, plain, (spl1 | spl28), inference(avatar_split_clause, [status(thm)], [c180, sdef1, sdef28])).
% 15.06/2.63 cnf(c181, plain, lonely(sk0,sk4) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp181, plain, (spl2 | spl28), inference(avatar_split_clause, [status(thm)], [c181, sdef2, sdef28])).
% 15.06/2.63 cnf(c182, plain, lonely(sk0,sk4) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp182, plain, (spl3 | spl28), inference(avatar_split_clause, [status(thm)], [c182, sdef3, sdef28])).
% 15.06/2.63 cnf(c183, plain, lonely(sk0,sk4) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp183, plain, (spl4 | spl28), inference(avatar_split_clause, [status(thm)], [c183, sdef4, sdef28])).
% 15.06/2.63 cnf(c184, plain, lonely(sk0,sk4) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp184, plain, (spl5 | spl28), inference(avatar_split_clause, [status(thm)], [c184, sdef5, sdef28])).
% 15.06/2.63 cnf(c185, plain, lonely(sk0,sk4) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp185, plain, (spl6 | spl28), inference(avatar_split_clause, [status(thm)], [c185, sdef6, sdef28])).
% 15.06/2.63 cnf(c186, plain, lonely(sk0,sk4) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp186, plain, (spl7 | spl28), inference(avatar_split_clause, [status(thm)], [c186, sdef7, sdef28])).
% 15.06/2.63 cnf(c187, plain, lonely(sk0,sk4) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp187, plain, (spl8 | spl28), inference(avatar_split_clause, [status(thm)], [c187, sdef8, sdef28])).
% 15.06/2.63 cnf(c188, plain, lonely(sk0,sk4) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp188, plain, (spl9 | spl28), inference(avatar_split_clause, [status(thm)], [c188, sdef9, sdef28])).
% 15.06/2.63 cnf(c189, plain, lonely(sk0,sk4) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp189, plain, (spl10 | spl28), inference(avatar_split_clause, [status(thm)], [c189, sdef10, sdef28])).
% 15.06/2.63 cnf(c190, plain, lonely(sk0,sk4) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp190, plain, (spl11 | spl28), inference(avatar_split_clause, [status(thm)], [c190, sdef11, sdef28])).
% 15.06/2.63 cnf(c191, plain, lonely(sk0,sk4) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp191, plain, (spl12 | spl28), inference(avatar_split_clause, [status(thm)], [c191, sdef12, sdef28])).
% 15.06/2.63 cnf(c192, plain, lonely(sk0,sk4) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp192, plain, (spl13 | spl28), inference(avatar_split_clause, [status(thm)], [c192, sdef13, sdef28])).
% 15.06/2.63 cnf(c193, plain, lonely(sk0,sk4) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp193, plain, (spl14 | spl28), inference(avatar_split_clause, [status(thm)], [c193, sdef14, sdef28])).
% 15.06/2.63 cnf(c194, plain, lonely(sk0,sk4) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp194, plain, (spl15 | spl28), inference(avatar_split_clause, [status(thm)], [c194, sdef15, sdef28])).
% 15.06/2.63 cnf(c195, plain, lonely(sk0,sk4) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp195, plain, (spl16 | spl28), inference(avatar_split_clause, [status(thm)], [c195, sdef16, sdef28])).
% 15.06/2.63 cnf(c196, plain, lonely(sk0,sk4) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp196, plain, (spl17 | spl28), inference(avatar_split_clause, [status(thm)], [c196, sdef17, sdef28])).
% 15.06/2.63 cnf(c197, plain, lonely(sk0,sk4) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp197, plain, (spl18 | spl28), inference(avatar_split_clause, [status(thm)], [c197, sdef18, sdef28])).
% 15.06/2.63 cnf(c198, plain, event(sk0,sk5) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef29, definition, (spl29 <=> (event(sk0,sk5))), introduced(definition, [new_symbols(naming, [spl29])], [avatar_definition])).
% 15.06/2.63 cnf(ssp198, plain, (spl1 | spl29), inference(avatar_split_clause, [status(thm)], [c198, sdef1, sdef29])).
% 15.06/2.63 cnf(c199, plain, event(sk0,sk5) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp199, plain, (spl2 | spl29), inference(avatar_split_clause, [status(thm)], [c199, sdef2, sdef29])).
% 15.06/2.63 cnf(c200, plain, event(sk0,sk5) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp200, plain, (spl3 | spl29), inference(avatar_split_clause, [status(thm)], [c200, sdef3, sdef29])).
% 15.06/2.63 cnf(c201, plain, event(sk0,sk5) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp201, plain, (spl4 | spl29), inference(avatar_split_clause, [status(thm)], [c201, sdef4, sdef29])).
% 15.06/2.63 cnf(c202, plain, event(sk0,sk5) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp202, plain, (spl5 | spl29), inference(avatar_split_clause, [status(thm)], [c202, sdef5, sdef29])).
% 15.06/2.63 cnf(c203, plain, event(sk0,sk5) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp203, plain, (spl6 | spl29), inference(avatar_split_clause, [status(thm)], [c203, sdef6, sdef29])).
% 15.06/2.63 cnf(c204, plain, event(sk0,sk5) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp204, plain, (spl7 | spl29), inference(avatar_split_clause, [status(thm)], [c204, sdef7, sdef29])).
% 15.06/2.63 cnf(c205, plain, event(sk0,sk5) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp205, plain, (spl8 | spl29), inference(avatar_split_clause, [status(thm)], [c205, sdef8, sdef29])).
% 15.06/2.63 cnf(c206, plain, event(sk0,sk5) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp206, plain, (spl9 | spl29), inference(avatar_split_clause, [status(thm)], [c206, sdef9, sdef29])).
% 15.06/2.63 cnf(c207, plain, event(sk0,sk5) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp207, plain, (spl10 | spl29), inference(avatar_split_clause, [status(thm)], [c207, sdef10, sdef29])).
% 15.06/2.63 cnf(c208, plain, event(sk0,sk5) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp208, plain, (spl11 | spl29), inference(avatar_split_clause, [status(thm)], [c208, sdef11, sdef29])).
% 15.06/2.63 cnf(c209, plain, event(sk0,sk5) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp209, plain, (spl12 | spl29), inference(avatar_split_clause, [status(thm)], [c209, sdef12, sdef29])).
% 15.06/2.63 cnf(c210, plain, event(sk0,sk5) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp210, plain, (spl13 | spl29), inference(avatar_split_clause, [status(thm)], [c210, sdef13, sdef29])).
% 15.06/2.63 cnf(c211, plain, event(sk0,sk5) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp211, plain, (spl14 | spl29), inference(avatar_split_clause, [status(thm)], [c211, sdef14, sdef29])).
% 15.06/2.63 cnf(c212, plain, event(sk0,sk5) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp212, plain, (spl15 | spl29), inference(avatar_split_clause, [status(thm)], [c212, sdef15, sdef29])).
% 15.06/2.63 cnf(c213, plain, event(sk0,sk5) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp213, plain, (spl16 | spl29), inference(avatar_split_clause, [status(thm)], [c213, sdef16, sdef29])).
% 15.06/2.63 cnf(c214, plain, event(sk0,sk5) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp214, plain, (spl17 | spl29), inference(avatar_split_clause, [status(thm)], [c214, sdef17, sdef29])).
% 15.06/2.63 cnf(c215, plain, event(sk0,sk5) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp215, plain, (spl18 | spl29), inference(avatar_split_clause, [status(thm)], [c215, sdef18, sdef29])).
% 15.06/2.63 cnf(c216, plain, agent(sk0,sk5,sk3) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp216, plain, (spl1 | spl30), inference(avatar_split_clause, [status(thm)], [c216, sdef1, sdef30])).
% 15.06/2.63 cnf(c217, plain, agent(sk0,sk5,sk3) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp217, plain, (spl2 | spl30), inference(avatar_split_clause, [status(thm)], [c217, sdef2, sdef30])).
% 15.06/2.63 cnf(c218, plain, agent(sk0,sk5,sk3) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp218, plain, (spl3 | spl30), inference(avatar_split_clause, [status(thm)], [c218, sdef3, sdef30])).
% 15.06/2.63 cnf(c219, plain, agent(sk0,sk5,sk3) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp219, plain, (spl4 | spl30), inference(avatar_split_clause, [status(thm)], [c219, sdef4, sdef30])).
% 15.06/2.63 cnf(c220, plain, agent(sk0,sk5,sk3) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp220, plain, (spl5 | spl30), inference(avatar_split_clause, [status(thm)], [c220, sdef5, sdef30])).
% 15.06/2.63 cnf(c221, plain, agent(sk0,sk5,sk3) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp221, plain, (spl6 | spl30), inference(avatar_split_clause, [status(thm)], [c221, sdef6, sdef30])).
% 15.06/2.63 cnf(c222, plain, agent(sk0,sk5,sk3) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp222, plain, (spl7 | spl30), inference(avatar_split_clause, [status(thm)], [c222, sdef7, sdef30])).
% 15.06/2.63 cnf(c223, plain, agent(sk0,sk5,sk3) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp223, plain, (spl8 | spl30), inference(avatar_split_clause, [status(thm)], [c223, sdef8, sdef30])).
% 15.06/2.63 cnf(c224, plain, agent(sk0,sk5,sk3) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp224, plain, (spl9 | spl30), inference(avatar_split_clause, [status(thm)], [c224, sdef9, sdef30])).
% 15.06/2.63 cnf(c225, plain, agent(sk0,sk5,sk3) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp225, plain, (spl10 | spl30), inference(avatar_split_clause, [status(thm)], [c225, sdef10, sdef30])).
% 15.06/2.63 cnf(c226, plain, agent(sk0,sk5,sk3) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp226, plain, (spl11 | spl30), inference(avatar_split_clause, [status(thm)], [c226, sdef11, sdef30])).
% 15.06/2.63 cnf(c227, plain, agent(sk0,sk5,sk3) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp227, plain, (spl12 | spl30), inference(avatar_split_clause, [status(thm)], [c227, sdef12, sdef30])).
% 15.06/2.63 cnf(c228, plain, agent(sk0,sk5,sk3) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp228, plain, (spl13 | spl30), inference(avatar_split_clause, [status(thm)], [c228, sdef13, sdef30])).
% 15.06/2.63 cnf(c229, plain, agent(sk0,sk5,sk3) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp229, plain, (spl14 | spl30), inference(avatar_split_clause, [status(thm)], [c229, sdef14, sdef30])).
% 15.06/2.63 cnf(c230, plain, agent(sk0,sk5,sk3) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp230, plain, (spl15 | spl30), inference(avatar_split_clause, [status(thm)], [c230, sdef15, sdef30])).
% 15.06/2.63 cnf(c231, plain, agent(sk0,sk5,sk3) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp231, plain, (spl16 | spl30), inference(avatar_split_clause, [status(thm)], [c231, sdef16, sdef30])).
% 15.06/2.63 cnf(c232, plain, agent(sk0,sk5,sk3) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp232, plain, (spl17 | spl30), inference(avatar_split_clause, [status(thm)], [c232, sdef17, sdef30])).
% 15.06/2.63 cnf(c233, plain, agent(sk0,sk5,sk3) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp233, plain, (spl18 | spl30), inference(avatar_split_clause, [status(thm)], [c233, sdef18, sdef30])).
% 15.06/2.63 cnf(c234, plain, present(sk0,sk5) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp234, plain, (spl1 | spl31), inference(avatar_split_clause, [status(thm)], [c234, sdef1, sdef31])).
% 15.06/2.63 cnf(c235, plain, present(sk0,sk5) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp235, plain, (spl2 | spl31), inference(avatar_split_clause, [status(thm)], [c235, sdef2, sdef31])).
% 15.06/2.63 cnf(c236, plain, present(sk0,sk5) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp236, plain, (spl3 | spl31), inference(avatar_split_clause, [status(thm)], [c236, sdef3, sdef31])).
% 15.06/2.63 cnf(c237, plain, present(sk0,sk5) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp237, plain, (spl4 | spl31), inference(avatar_split_clause, [status(thm)], [c237, sdef4, sdef31])).
% 15.06/2.63 cnf(c238, plain, present(sk0,sk5) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp238, plain, (spl5 | spl31), inference(avatar_split_clause, [status(thm)], [c238, sdef5, sdef31])).
% 15.06/2.63 cnf(c239, plain, present(sk0,sk5) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp239, plain, (spl6 | spl31), inference(avatar_split_clause, [status(thm)], [c239, sdef6, sdef31])).
% 15.06/2.63 cnf(c240, plain, present(sk0,sk5) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp240, plain, (spl7 | spl31), inference(avatar_split_clause, [status(thm)], [c240, sdef7, sdef31])).
% 15.06/2.63 cnf(c241, plain, present(sk0,sk5) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp241, plain, (spl8 | spl31), inference(avatar_split_clause, [status(thm)], [c241, sdef8, sdef31])).
% 15.06/2.63 cnf(c242, plain, present(sk0,sk5) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp242, plain, (spl9 | spl31), inference(avatar_split_clause, [status(thm)], [c242, sdef9, sdef31])).
% 15.06/2.63 cnf(c243, plain, present(sk0,sk5) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp243, plain, (spl10 | spl31), inference(avatar_split_clause, [status(thm)], [c243, sdef10, sdef31])).
% 15.06/2.63 cnf(c244, plain, present(sk0,sk5) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp244, plain, (spl11 | spl31), inference(avatar_split_clause, [status(thm)], [c244, sdef11, sdef31])).
% 15.06/2.63 cnf(c245, plain, present(sk0,sk5) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp245, plain, (spl12 | spl31), inference(avatar_split_clause, [status(thm)], [c245, sdef12, sdef31])).
% 15.06/2.63 cnf(c246, plain, present(sk0,sk5) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp246, plain, (spl13 | spl31), inference(avatar_split_clause, [status(thm)], [c246, sdef13, sdef31])).
% 15.06/2.63 cnf(c247, plain, present(sk0,sk5) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp247, plain, (spl14 | spl31), inference(avatar_split_clause, [status(thm)], [c247, sdef14, sdef31])).
% 15.06/2.63 cnf(c248, plain, present(sk0,sk5) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp248, plain, (spl15 | spl31), inference(avatar_split_clause, [status(thm)], [c248, sdef15, sdef31])).
% 15.06/2.63 cnf(c249, plain, present(sk0,sk5) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp249, plain, (spl16 | spl31), inference(avatar_split_clause, [status(thm)], [c249, sdef16, sdef31])).
% 15.06/2.63 cnf(c250, plain, present(sk0,sk5) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp250, plain, (spl17 | spl31), inference(avatar_split_clause, [status(thm)], [c250, sdef17, sdef31])).
% 15.06/2.63 cnf(c251, plain, present(sk0,sk5) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp251, plain, (spl18 | spl31), inference(avatar_split_clause, [status(thm)], [c251, sdef18, sdef31])).
% 15.06/2.63 cnf(c252, plain, barrel(sk0,sk5) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp252, plain, (spl1 | spl32), inference(avatar_split_clause, [status(thm)], [c252, sdef1, sdef32])).
% 15.06/2.63 cnf(c253, plain, barrel(sk0,sk5) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp253, plain, (spl2 | spl32), inference(avatar_split_clause, [status(thm)], [c253, sdef2, sdef32])).
% 15.06/2.63 cnf(c254, plain, barrel(sk0,sk5) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp254, plain, (spl3 | spl32), inference(avatar_split_clause, [status(thm)], [c254, sdef3, sdef32])).
% 15.06/2.63 cnf(c255, plain, barrel(sk0,sk5) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp255, plain, (spl4 | spl32), inference(avatar_split_clause, [status(thm)], [c255, sdef4, sdef32])).
% 15.06/2.63 cnf(c256, plain, barrel(sk0,sk5) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp256, plain, (spl5 | spl32), inference(avatar_split_clause, [status(thm)], [c256, sdef5, sdef32])).
% 15.06/2.63 cnf(c257, plain, barrel(sk0,sk5) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp257, plain, (spl6 | spl32), inference(avatar_split_clause, [status(thm)], [c257, sdef6, sdef32])).
% 15.06/2.63 cnf(c258, plain, barrel(sk0,sk5) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp258, plain, (spl7 | spl32), inference(avatar_split_clause, [status(thm)], [c258, sdef7, sdef32])).
% 15.06/2.63 cnf(c259, plain, barrel(sk0,sk5) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp259, plain, (spl8 | spl32), inference(avatar_split_clause, [status(thm)], [c259, sdef8, sdef32])).
% 15.06/2.63 cnf(c260, plain, barrel(sk0,sk5) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp260, plain, (spl9 | spl32), inference(avatar_split_clause, [status(thm)], [c260, sdef9, sdef32])).
% 15.06/2.63 cnf(c261, plain, barrel(sk0,sk5) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp261, plain, (spl10 | spl32), inference(avatar_split_clause, [status(thm)], [c261, sdef10, sdef32])).
% 15.06/2.63 cnf(c262, plain, barrel(sk0,sk5) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp262, plain, (spl11 | spl32), inference(avatar_split_clause, [status(thm)], [c262, sdef11, sdef32])).
% 15.06/2.63 cnf(c263, plain, barrel(sk0,sk5) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp263, plain, (spl12 | spl32), inference(avatar_split_clause, [status(thm)], [c263, sdef12, sdef32])).
% 15.06/2.63 cnf(c264, plain, barrel(sk0,sk5) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp264, plain, (spl13 | spl32), inference(avatar_split_clause, [status(thm)], [c264, sdef13, sdef32])).
% 15.06/2.63 cnf(c265, plain, barrel(sk0,sk5) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp265, plain, (spl14 | spl32), inference(avatar_split_clause, [status(thm)], [c265, sdef14, sdef32])).
% 15.06/2.63 cnf(c266, plain, barrel(sk0,sk5) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp266, plain, (spl15 | spl32), inference(avatar_split_clause, [status(thm)], [c266, sdef15, sdef32])).
% 15.06/2.63 cnf(c267, plain, barrel(sk0,sk5) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp267, plain, (spl16 | spl32), inference(avatar_split_clause, [status(thm)], [c267, sdef16, sdef32])).
% 15.06/2.63 cnf(c268, plain, barrel(sk0,sk5) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp268, plain, (spl17 | spl32), inference(avatar_split_clause, [status(thm)], [c268, sdef17, sdef32])).
% 15.06/2.63 cnf(c269, plain, barrel(sk0,sk5) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp269, plain, (spl18 | spl32), inference(avatar_split_clause, [status(thm)], [c269, sdef18, sdef32])).
% 15.06/2.63 cnf(c270, plain, down(sk0,sk5,sk4) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp270, plain, (spl1 | spl33), inference(avatar_split_clause, [status(thm)], [c270, sdef1, sdef33])).
% 15.06/2.63 cnf(c271, plain, down(sk0,sk5,sk4) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp271, plain, (spl2 | spl33), inference(avatar_split_clause, [status(thm)], [c271, sdef2, sdef33])).
% 15.06/2.63 cnf(c272, plain, down(sk0,sk5,sk4) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp272, plain, (spl3 | spl33), inference(avatar_split_clause, [status(thm)], [c272, sdef3, sdef33])).
% 15.06/2.63 cnf(c273, plain, down(sk0,sk5,sk4) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp273, plain, (spl4 | spl33), inference(avatar_split_clause, [status(thm)], [c273, sdef4, sdef33])).
% 15.06/2.63 cnf(c274, plain, down(sk0,sk5,sk4) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp274, plain, (spl5 | spl33), inference(avatar_split_clause, [status(thm)], [c274, sdef5, sdef33])).
% 15.06/2.63 cnf(c275, plain, down(sk0,sk5,sk4) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp275, plain, (spl6 | spl33), inference(avatar_split_clause, [status(thm)], [c275, sdef6, sdef33])).
% 15.06/2.63 cnf(c276, plain, down(sk0,sk5,sk4) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp276, plain, (spl7 | spl33), inference(avatar_split_clause, [status(thm)], [c276, sdef7, sdef33])).
% 15.06/2.63 cnf(c277, plain, down(sk0,sk5,sk4) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp277, plain, (spl8 | spl33), inference(avatar_split_clause, [status(thm)], [c277, sdef8, sdef33])).
% 15.06/2.63 cnf(c278, plain, down(sk0,sk5,sk4) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp278, plain, (spl9 | spl33), inference(avatar_split_clause, [status(thm)], [c278, sdef9, sdef33])).
% 15.06/2.63 cnf(c279, plain, down(sk0,sk5,sk4) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp279, plain, (spl10 | spl33), inference(avatar_split_clause, [status(thm)], [c279, sdef10, sdef33])).
% 15.06/2.63 cnf(c280, plain, down(sk0,sk5,sk4) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp280, plain, (spl11 | spl33), inference(avatar_split_clause, [status(thm)], [c280, sdef11, sdef33])).
% 15.06/2.63 cnf(c281, plain, down(sk0,sk5,sk4) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp281, plain, (spl12 | spl33), inference(avatar_split_clause, [status(thm)], [c281, sdef12, sdef33])).
% 15.06/2.63 cnf(c282, plain, down(sk0,sk5,sk4) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp282, plain, (spl13 | spl33), inference(avatar_split_clause, [status(thm)], [c282, sdef13, sdef33])).
% 15.06/2.63 cnf(c283, plain, down(sk0,sk5,sk4) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp283, plain, (spl14 | spl33), inference(avatar_split_clause, [status(thm)], [c283, sdef14, sdef33])).
% 15.06/2.63 cnf(c284, plain, down(sk0,sk5,sk4) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp284, plain, (spl15 | spl33), inference(avatar_split_clause, [status(thm)], [c284, sdef15, sdef33])).
% 15.06/2.63 cnf(c285, plain, down(sk0,sk5,sk4) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp285, plain, (spl16 | spl33), inference(avatar_split_clause, [status(thm)], [c285, sdef16, sdef33])).
% 15.06/2.63 cnf(c286, plain, down(sk0,sk5,sk4) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp286, plain, (spl17 | spl33), inference(avatar_split_clause, [status(thm)], [c286, sdef17, sdef33])).
% 15.06/2.63 cnf(c287, plain, down(sk0,sk5,sk4) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp287, plain, (spl18 | spl33), inference(avatar_split_clause, [status(thm)], [c287, sdef18, sdef33])).
% 15.06/2.63 cnf(c288, plain, in(sk0,sk5,sk1) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp288, plain, (spl1 | spl34), inference(avatar_split_clause, [status(thm)], [c288, sdef1, sdef34])).
% 15.06/2.63 cnf(c289, plain, in(sk0,sk5,sk1) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp289, plain, (spl2 | spl34), inference(avatar_split_clause, [status(thm)], [c289, sdef2, sdef34])).
% 15.06/2.63 cnf(c290, plain, in(sk0,sk5,sk1) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp290, plain, (spl3 | spl34), inference(avatar_split_clause, [status(thm)], [c290, sdef3, sdef34])).
% 15.06/2.63 cnf(c291, plain, in(sk0,sk5,sk1) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp291, plain, (spl4 | spl34), inference(avatar_split_clause, [status(thm)], [c291, sdef4, sdef34])).
% 15.06/2.63 cnf(c292, plain, in(sk0,sk5,sk1) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp292, plain, (spl5 | spl34), inference(avatar_split_clause, [status(thm)], [c292, sdef5, sdef34])).
% 15.06/2.63 cnf(c293, plain, in(sk0,sk5,sk1) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp293, plain, (spl6 | spl34), inference(avatar_split_clause, [status(thm)], [c293, sdef6, sdef34])).
% 15.06/2.63 cnf(c294, plain, in(sk0,sk5,sk1) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp294, plain, (spl7 | spl34), inference(avatar_split_clause, [status(thm)], [c294, sdef7, sdef34])).
% 15.06/2.63 cnf(c295, plain, in(sk0,sk5,sk1) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp295, plain, (spl8 | spl34), inference(avatar_split_clause, [status(thm)], [c295, sdef8, sdef34])).
% 15.06/2.63 cnf(c296, plain, in(sk0,sk5,sk1) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp296, plain, (spl9 | spl34), inference(avatar_split_clause, [status(thm)], [c296, sdef9, sdef34])).
% 15.06/2.63 cnf(c297, plain, in(sk0,sk5,sk1) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp297, plain, (spl10 | spl34), inference(avatar_split_clause, [status(thm)], [c297, sdef10, sdef34])).
% 15.06/2.63 cnf(c298, plain, in(sk0,sk5,sk1) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp298, plain, (spl11 | spl34), inference(avatar_split_clause, [status(thm)], [c298, sdef11, sdef34])).
% 15.06/2.63 cnf(c299, plain, in(sk0,sk5,sk1) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp299, plain, (spl12 | spl34), inference(avatar_split_clause, [status(thm)], [c299, sdef12, sdef34])).
% 15.06/2.63 cnf(c300, plain, in(sk0,sk5,sk1) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp300, plain, (spl13 | spl34), inference(avatar_split_clause, [status(thm)], [c300, sdef13, sdef34])).
% 15.06/2.63 cnf(c301, plain, in(sk0,sk5,sk1) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp301, plain, (spl14 | spl34), inference(avatar_split_clause, [status(thm)], [c301, sdef14, sdef34])).
% 15.06/2.63 cnf(c302, plain, in(sk0,sk5,sk1) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp302, plain, (spl15 | spl34), inference(avatar_split_clause, [status(thm)], [c302, sdef15, sdef34])).
% 15.06/2.63 cnf(c303, plain, in(sk0,sk5,sk1) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp303, plain, (spl16 | spl34), inference(avatar_split_clause, [status(thm)], [c303, sdef16, sdef34])).
% 15.06/2.63 cnf(c304, plain, in(sk0,sk5,sk1) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp304, plain, (spl17 | spl34), inference(avatar_split_clause, [status(thm)], [c304, sdef17, sdef34])).
% 15.06/2.63 cnf(c305, plain, in(sk0,sk5,sk1) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp305, plain, (spl18 | spl34), inference(avatar_split_clause, [status(thm)], [c305, sdef18, sdef34])).
% 15.06/2.63 cnf(c306, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | actual_world(sk6), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 fof(sdef35, definition, (spl35 <=> (~actual_world(X0) | ~of(X0,X1,X2) | ~city(X0,X2) | ~hollywood_placename(X0,X1) | ~placename(X0,X1) | ~street(X0,X3) | ~lonely(X0,X3) | ~chevy(X0,X4) | ~white(X0,X4) | ~dirty(X0,X4) | ~old(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X4) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X3) | ~in(X0,X5,X2))), introduced(definition, [new_symbols(naming, [spl35])], [avatar_definition])).
% 15.06/2.63 cnf(ssp306, plain, (spl1 | spl35), inference(avatar_split_clause, [status(thm)], [c306, sdef1, sdef35])).
% 15.06/2.63 cnf(c307, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | of(sk6,sk8,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp307, plain, (spl2 | spl35), inference(avatar_split_clause, [status(thm)], [c307, sdef2, sdef35])).
% 15.06/2.63 cnf(c308, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | city(sk6,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp308, plain, (spl3 | spl35), inference(avatar_split_clause, [status(thm)], [c308, sdef3, sdef35])).
% 15.06/2.63 cnf(c309, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | hollywood_placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp309, plain, (spl4 | spl35), inference(avatar_split_clause, [status(thm)], [c309, sdef4, sdef35])).
% 15.06/2.63 cnf(c310, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | placename(sk6,sk8), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp310, plain, (spl5 | spl35), inference(avatar_split_clause, [status(thm)], [c310, sdef5, sdef35])).
% 15.06/2.63 cnf(c311, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | street(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp311, plain, (spl6 | spl35), inference(avatar_split_clause, [status(thm)], [c311, sdef6, sdef35])).
% 15.06/2.63 cnf(c312, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | lonely(sk6,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp312, plain, (spl7 | spl35), inference(avatar_split_clause, [status(thm)], [c312, sdef7, sdef35])).
% 15.06/2.63 cnf(c313, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | chevy(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp313, plain, (spl8 | spl35), inference(avatar_split_clause, [status(thm)], [c313, sdef8, sdef35])).
% 15.06/2.63 cnf(c314, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | white(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp314, plain, (spl9 | spl35), inference(avatar_split_clause, [status(thm)], [c314, sdef9, sdef35])).
% 15.06/2.63 cnf(c315, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | dirty(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp315, plain, (spl10 | spl35), inference(avatar_split_clause, [status(thm)], [c315, sdef10, sdef35])).
% 15.06/2.63 cnf(c316, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | old(sk6,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp316, plain, (spl11 | spl35), inference(avatar_split_clause, [status(thm)], [c316, sdef11, sdef35])).
% 15.06/2.63 cnf(c317, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | event(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp317, plain, (spl12 | spl35), inference(avatar_split_clause, [status(thm)], [c317, sdef12, sdef35])).
% 15.06/2.63 cnf(c318, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | agent(sk6,sk11,sk10), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp318, plain, (spl13 | spl35), inference(avatar_split_clause, [status(thm)], [c318, sdef13, sdef35])).
% 15.06/2.63 cnf(c319, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | present(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp319, plain, (spl14 | spl35), inference(avatar_split_clause, [status(thm)], [c319, sdef14, sdef35])).
% 15.06/2.63 cnf(c320, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | barrel(sk6,sk11), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp320, plain, (spl15 | spl35), inference(avatar_split_clause, [status(thm)], [c320, sdef15, sdef35])).
% 15.06/2.63 cnf(c321, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | down(sk6,sk11,sk9), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp321, plain, (spl16 | spl35), inference(avatar_split_clause, [status(thm)], [c321, sdef16, sdef35])).
% 15.06/2.63 cnf(c322, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | in(sk6,sk11,sk7), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp322, plain, (spl17 | spl35), inference(avatar_split_clause, [status(thm)], [c322, sdef17, sdef35])).
% 15.06/2.63 cnf(c323, plain, ~actual_world(X6) | ~of(X6,X8,X7) | ~city(X6,X7) | ~hollywood_placename(X6,X8) | ~placename(X6,X8) | ~street(X6,X9) | ~lonely(X6,X9) | ~chevy(X6,X10) | ~white(X6,X10) | ~dirty(X6,X10) | ~old(X6,X10) | ~event(X6,X11) | ~agent(X6,X11,X10) | ~present(X6,X11) | ~barrel(X6,X11) | ~down(X6,X11,X9) | ~in(X6,X11,X7) | ~actual_world(X0) | ~of(X0,X2,X1) | ~city(X0,X1) | ~hollywood_placename(X0,X2) | ~placename(X0,X2) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X1), inference(cnf_transformation, [status(esa)], [f0_sk])).
% 15.06/2.63 cnf(ssp323, plain, (spl18 | spl35), inference(avatar_split_clause, [status(thm)], [c323, sdef18, sdef35])).
% 15.06/2.63 cnf(p36, plain, (~actual_world(X0) | ~of(X0,X1,X2) | ~city(X0,X2) | ~hollywood_placename(X0,X1) | ~placename(X0,X1) | ~chevy(X0,X3) | ~white(X0,X3) | ~dirty(X0,X3) | ~old(X0,X3) | ~street(X0,X4) | ~lonely(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X3) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X4) | ~in(X0,X5,X2) | ~spl18), inference(avatar_component_clause, [status(thm)], [sdef18])).
% 15.06/2.63 cnf(p1, plain, (actual_world(sk0) | ~spl0), inference(avatar_component_clause, [status(thm)], [sdef0])).
% 15.06/2.63 cnf(p360, plain, (~of(sk0,X0,X1) | ~city(sk0,X1) | ~hollywood_placename(sk0,X0) | ~placename(sk0,X0) | ~chevy(sk0,X2) | ~white(sk0,X2) | ~dirty(sk0,X2) | ~old(sk0,X2) | ~street(sk0,X3) | ~lonely(sk0,X3) | ~event(sk0,X4) | ~agent(sk0,X4,X2) | ~present(sk0,X4) | ~barrel(sk0,X4) | ~down(sk0,X4,X3) | ~in(sk0,X4,X1) | ~spl0 | ~spl18), inference(resolution, [status(thm)], [p36, p1])).
% 15.06/2.63 cnf(p38, plain, (of(sk0,sk2,sk1) | ~spl19), inference(avatar_component_clause, [status(thm)], [sdef19])).
% 15.06/2.63 cnf(p362, plain, (~city(sk0,sk1) | ~hollywood_placename(sk0,sk2) | ~placename(sk0,sk2) | ~chevy(sk0,X0) | ~white(sk0,X0) | ~dirty(sk0,X0) | ~old(sk0,X0) | ~street(sk0,X1) | ~lonely(sk0,X1) | ~event(sk0,X2) | ~agent(sk0,X2,X0) | ~present(sk0,X2) | ~barrel(sk0,X2) | ~down(sk0,X2,X1) | ~in(sk0,X2,sk1) | ~spl0 | ~spl18 | ~spl19), inference(resolution, [status(thm)], [p360, p38])).
% 15.06/2.63 fof(sdef39, definition, (spl39 <=> (~chevy(sk0,X0) | ~white(sk0,X0) | ~dirty(sk0,X0) | ~old(sk0,X0) | ~street(sk0,X1) | ~lonely(sk0,X1) | ~event(sk0,X2) | ~agent(sk0,X2,X0) | ~present(sk0,X2) | ~barrel(sk0,X2) | ~down(sk0,X2,X1) | ~in(sk0,X2,sk1))), introduced(definition, [new_symbols(naming, [spl39])], [avatar_definition])).
% 15.06/2.63 cnf(ssp324, plain, (~spl0 | ~spl18 | ~spl19 | spl36 | spl37 | spl38 | spl39), inference(avatar_split_clause, [status(thm)], [p362, sdef36, sdef37, sdef38, sdef39])).
% 15.06/2.63 cnf(p366, plain, (~chevy(sk0,X0) | ~white(sk0,X0) | ~dirty(sk0,X0) | ~old(sk0,X0) | ~street(sk0,X1) | ~lonely(sk0,X1) | ~event(sk0,X2) | ~agent(sk0,X2,X0) | ~present(sk0,X2) | ~barrel(sk0,X2) | ~down(sk0,X2,X1) | ~in(sk0,X2,sk1) | ~spl39), inference(avatar_component_clause, [status(thm)], [sdef39])).
% 15.06/2.63 cnf(p114, plain, (chevy(sk0,sk3) | ~spl23), inference(avatar_component_clause, [status(thm)], [sdef23])).
% 15.06/2.63 cnf(p372, plain, (~white(sk0,sk3) | ~dirty(sk0,sk3) | ~old(sk0,sk3) | ~street(sk0,X0) | ~lonely(sk0,X0) | ~event(sk0,X1) | ~agent(sk0,X1,sk3) | ~present(sk0,X1) | ~barrel(sk0,X1) | ~down(sk0,X1,X0) | ~in(sk0,X1,sk1) | ~spl23 | ~spl39), inference(resolution, [status(thm)], [p366, p114])).
% 15.06/2.63 fof(sdef43, definition, (spl43 <=> (~street(sk0,X0) | ~lonely(sk0,X0) | ~event(sk0,X1) | ~agent(sk0,X1,sk3) | ~present(sk0,X1) | ~barrel(sk0,X1) | ~down(sk0,X1,X0) | ~in(sk0,X1,sk1))), introduced(definition, [new_symbols(naming, [spl43])], [avatar_definition])).
% 15.06/2.63 cnf(ssp325, plain, (~spl23 | ~spl39 | spl40 | spl41 | spl42 | spl43), inference(avatar_split_clause, [status(thm)], [p372, sdef40, sdef41, sdef42, sdef43])).
% 15.06/2.63 cnf(p2, plain, (actual_world(sk6) | ~spl1), inference(avatar_component_clause, [status(thm)], [sdef1])).
% 15.06/2.63 cnf(p361, plain, (~of(sk6,X0,X1) | ~city(sk6,X1) | ~hollywood_placename(sk6,X0) | ~placename(sk6,X0) | ~chevy(sk6,X2) | ~white(sk6,X2) | ~dirty(sk6,X2) | ~old(sk6,X2) | ~street(sk6,X3) | ~lonely(sk6,X3) | ~event(sk6,X4) | ~agent(sk6,X4,X2) | ~present(sk6,X4) | ~barrel(sk6,X4) | ~down(sk6,X4,X3) | ~in(sk6,X4,X1) | ~spl1 | ~spl18), inference(resolution, [status(thm)], [p36, p2])).
% 15.06/2.63 cnf(p4, plain, (of(sk6,sk8,sk7) | ~spl2), inference(avatar_component_clause, [status(thm)], [sdef2])).
% 15.06/2.63 cnf(p380, plain, (~city(sk6,sk7) | ~hollywood_placename(sk6,sk8) | ~placename(sk6,sk8) | ~chevy(sk6,X0) | ~white(sk6,X0) | ~dirty(sk6,X0) | ~old(sk6,X0) | ~street(sk6,X1) | ~lonely(sk6,X1) | ~event(sk6,X2) | ~agent(sk6,X2,X0) | ~present(sk6,X2) | ~barrel(sk6,X2) | ~down(sk6,X2,X1) | ~in(sk6,X2,sk7) | ~spl1 | ~spl2 | ~spl18), inference(resolution, [status(thm)], [p361, p4])).
% 15.06/2.63 fof(sdef47, definition, (spl47 <=> (~chevy(sk6,X0) | ~white(sk6,X0) | ~dirty(sk6,X0) | ~old(sk6,X0) | ~street(sk6,X1) | ~lonely(sk6,X1) | ~event(sk6,X2) | ~agent(sk6,X2,X0) | ~present(sk6,X2) | ~barrel(sk6,X2) | ~down(sk6,X2,X1) | ~in(sk6,X2,sk7))), introduced(definition, [new_symbols(naming, [spl47])], [avatar_definition])).
% 15.06/2.63 cnf(ssp326, plain, (~spl1 | ~spl2 | ~spl18 | spl44 | spl45 | spl46 | spl47), inference(avatar_split_clause, [status(thm)], [p380, sdef44, sdef45, sdef46, sdef47])).
% 15.06/2.63 cnf(p376, plain, (~street(sk0,X0) | ~lonely(sk0,X0) | ~event(sk0,X1) | ~agent(sk0,X1,sk3) | ~present(sk0,X1) | ~barrel(sk0,X1) | ~down(sk0,X1,X0) | ~in(sk0,X1,sk1) | ~spl43), inference(avatar_component_clause, [status(thm)], [sdef43])).
% 15.06/2.63 cnf(p190, plain, (street(sk0,sk4) | ~spl27), inference(avatar_component_clause, [status(thm)], [sdef27])).
% 15.06/2.63 cnf(p388, plain, (~lonely(sk0,sk4) | ~event(sk0,X0) | ~agent(sk0,X0,sk3) | ~present(sk0,X0) | ~barrel(sk0,X0) | ~down(sk0,X0,sk4) | ~in(sk0,X0,sk1) | ~spl27 | ~spl43), inference(resolution, [status(thm)], [p376, p190])).
% 15.06/2.63 fof(sdef49, definition, (spl49 <=> (~event(sk0,X0) | ~agent(sk0,X0,sk3) | ~present(sk0,X0) | ~barrel(sk0,X0) | ~down(sk0,X0,sk4) | ~in(sk0,X0,sk1))), introduced(definition, [new_symbols(naming, [spl49])], [avatar_definition])).
% 15.06/2.63 cnf(ssp327, plain, (~spl27 | ~spl43 | spl48 | spl49), inference(avatar_split_clause, [status(thm)], [p388, sdef48, sdef49])).
% 15.06/2.63 cnf(p390, plain, (~event(sk0,X0) | ~agent(sk0,X0,sk3) | ~present(sk0,X0) | ~barrel(sk0,X0) | ~down(sk0,X0,sk4) | ~in(sk0,X0,sk1) | ~spl49), inference(avatar_component_clause, [status(thm)], [sdef49])).
% 15.06/2.63 cnf(p228, plain, (event(sk0,sk5) | ~spl29), inference(avatar_component_clause, [status(thm)], [sdef29])).
% 15.06/2.63 cnf(p392, plain, (~agent(sk0,sk5,sk3) | ~present(sk0,sk5) | ~barrel(sk0,sk5) | ~down(sk0,sk5,sk4) | ~in(sk0,sk5,sk1) | ~spl29 | ~spl49), inference(resolution, [status(thm)], [p390, p228])).
% 15.06/2.63 cnf(ssp328, plain, (~spl29 | ~spl49 | spl50 | spl51 | spl52 | spl53 | spl54), inference(avatar_split_clause, [status(thm)], [p392, sdef50, sdef51, sdef52, sdef53, sdef54])).
% 15.06/2.63 cnf(p342, plain, (~actual_world(X0) | ~of(X0,X1,X2) | ~city(X0,X2) | ~hollywood_placename(X0,X1) | ~placename(X0,X1) | ~street(X0,X3) | ~lonely(X0,X3) | ~chevy(X0,X4) | ~white(X0,X4) | ~dirty(X0,X4) | ~old(X0,X4) | ~event(X0,X5) | ~agent(X0,X5,X4) | ~present(X0,X5) | ~barrel(X0,X5) | ~down(X0,X5,X3) | ~in(X0,X5,X2) | ~spl35), inference(avatar_component_clause, [status(thm)], [sdef35])).
% 15.06/2.63 cnf(p371, plain, (~of(sk6,X0,X1) | ~city(sk6,X1) | ~hollywood_placename(sk6,X0) | ~placename(sk6,X0) | ~street(sk6,X2) | ~lonely(sk6,X2) | ~chevy(sk6,X3) | ~white(sk6,X3) | ~dirty(sk6,X3) | ~old(sk6,X3) | ~event(sk6,X4) | ~agent(sk6,X4,X3) | ~present(sk6,X4) | ~barrel(sk6,X4) | ~down(sk6,X4,X2) | ~in(sk6,X4,X1) | ~spl1 | ~spl35), inference(resolution, [status(thm)], [p342, p2])).
% 15.06/2.63 cnf(p400, plain, (~city(sk6,sk7) | ~hollywood_placename(sk6,sk8) | ~placename(sk6,sk8) | ~street(sk6,X0) | ~lonely(sk6,X0) | ~chevy(sk6,X1) | ~white(sk6,X1) | ~dirty(sk6,X1) | ~old(sk6,X1) | ~event(sk6,X2) | ~agent(sk6,X2,X1) | ~present(sk6,X2) | ~barrel(sk6,X2) | ~down(sk6,X2,X0) | ~in(sk6,X2,sk7) | ~spl1 | ~spl2 | ~spl35), inference(resolution, [status(thm)], [p371, p4])).
% 15.06/2.63 fof(sdef55, definition, (spl55 <=> (~street(sk6,X0) | ~lonely(sk6,X0) | ~chevy(sk6,X1) | ~white(sk6,X1) | ~dirty(sk6,X1) | ~old(sk6,X1) | ~event(sk6,X2) | ~agent(sk6,X2,X1) | ~present(sk6,X2) | ~barrel(sk6,X2) | ~down(sk6,X2,X0) | ~in(sk6,X2,sk7))), introduced(definition, [new_symbols(naming, [spl55])], [avatar_definition])).
% 15.06/2.63 cnf(ssp329, plain, (~spl1 | ~spl2 | ~spl35 | spl44 | spl45 | spl46 | spl55), inference(avatar_split_clause, [status(thm)], [p400, sdef44, sdef45, sdef46, sdef55])).
% 15.06/2.63 cnf(p384, plain, (~chevy(sk6,X0) | ~white(sk6,X0) | ~dirty(sk6,X0) | ~old(sk6,X0) | ~street(sk6,X1) | ~lonely(sk6,X1) | ~event(sk6,X2) | ~agent(sk6,X2,X0) | ~present(sk6,X2) | ~barrel(sk6,X2) | ~down(sk6,X2,X1) | ~in(sk6,X2,sk7) | ~spl47), inference(avatar_component_clause, [status(thm)], [sdef47])).
% 15.06/2.63 cnf(p16, plain, (chevy(sk6,sk10) | ~spl8), inference(avatar_component_clause, [status(thm)], [sdef8])).
% 15.06/2.63 cnf(p405, plain, (~white(sk6,sk10) | ~dirty(sk6,sk10) | ~old(sk6,sk10) | ~street(sk6,X0) | ~lonely(sk6,X0) | ~event(sk6,X1) | ~agent(sk6,X1,sk10) | ~present(sk6,X1) | ~barrel(sk6,X1) | ~down(sk6,X1,X0) | ~in(sk6,X1,sk7) | ~spl8 | ~spl47), inference(resolution, [status(thm)], [p384, p16])).
% 15.06/2.63 fof(sdef59, definition, (spl59 <=> (~street(sk6,X0) | ~lonely(sk6,X0) | ~event(sk6,X1) | ~agent(sk6,X1,sk10) | ~present(sk6,X1) | ~barrel(sk6,X1) | ~down(sk6,X1,X0) | ~in(sk6,X1,sk7))), introduced(definition, [new_symbols(naming, [spl59])], [avatar_definition])).
% 15.06/2.63 cnf(ssp330, plain, (~spl8 | ~spl47 | spl56 | spl57 | spl58 | spl59), inference(avatar_split_clause, [status(thm)], [p405, sdef56, sdef57, sdef58, sdef59])).
% 15.06/2.63 cnf(p401, plain, (~street(sk6,X0) | ~lonely(sk6,X0) | ~chevy(sk6,X1) | ~white(sk6,X1) | ~dirty(sk6,X1) | ~old(sk6,X1) | ~event(sk6,X2) | ~agent(sk6,X2,X1) | ~present(sk6,X2) | ~barrel(sk6,X2) | ~down(sk6,X2,X0) | ~in(sk6,X2,sk7) | ~spl55), inference(avatar_component_clause, [status(thm)], [sdef55])).
% 15.06/2.63 cnf(p12, plain, (street(sk6,sk9) | ~spl6), inference(avatar_component_clause, [status(thm)], [sdef6])).
% 15.06/2.63 cnf(p410, plain, (~lonely(sk6,sk9) | ~chevy(sk6,X0) | ~white(sk6,X0) | ~dirty(sk6,X0) | ~old(sk6,X0) | ~event(sk6,X1) | ~agent(sk6,X1,X0) | ~present(sk6,X1) | ~barrel(sk6,X1) | ~down(sk6,X1,sk9) | ~in(sk6,X1,sk7) | ~spl6 | ~spl55), inference(resolution, [status(thm)], [p401, p12])).
% 15.06/2.63 fof(sdef61, definition, (spl61 <=> (~chevy(sk6,X0) | ~white(sk6,X0) | ~dirty(sk6,X0) | ~old(sk6,X0) | ~event(sk6,X1) | ~agent(sk6,X1,X0) | ~present(sk6,X1) | ~barrel(sk6,X1) | ~down(sk6,X1,sk9) | ~in(sk6,X1,sk7))), introduced(definition, [new_symbols(naming, [spl61])], [avatar_definition])).
% 15.06/2.63 cnf(ssp331, plain, (~spl6 | ~spl55 | spl60 | spl61), inference(avatar_split_clause, [status(thm)], [p410, sdef60, sdef61])).
% 15.06/2.63 cnf(p409, plain, (~street(sk6,X0) | ~lonely(sk6,X0) | ~event(sk6,X1) | ~agent(sk6,X1,sk10) | ~present(sk6,X1) | ~barrel(sk6,X1) | ~down(sk6,X1,X0) | ~in(sk6,X1,sk7) | ~spl59), inference(avatar_component_clause, [status(thm)], [sdef59])).
% 15.06/2.63 cnf(p417, plain, (~lonely(sk6,sk9) | ~event(sk6,X0) | ~agent(sk6,X0,sk10) | ~present(sk6,X0) | ~barrel(sk6,X0) | ~down(sk6,X0,sk9) | ~in(sk6,X0,sk7) | ~spl6 | ~spl59), inference(resolution, [status(thm)], [p409, p12])).
% 15.06/2.63 fof(sdef62, definition, (spl62 <=> (~event(sk6,X0) | ~agent(sk6,X0,sk10) | ~present(sk6,X0) | ~barrel(sk6,X0) | ~down(sk6,X0,sk9) | ~in(sk6,X0,sk7))), introduced(definition, [new_symbols(naming, [spl62])], [avatar_definition])).
% 15.06/2.63 cnf(ssp332, plain, (~spl6 | ~spl59 | spl60 | spl62), inference(avatar_split_clause, [status(thm)], [p417, sdef60, sdef62])).
% 15.06/2.63 cnf(p418, plain, (~event(sk6,X0) | ~agent(sk6,X0,sk10) | ~present(sk6,X0) | ~barrel(sk6,X0) | ~down(sk6,X0,sk9) | ~in(sk6,X0,sk7) | ~spl62), inference(avatar_component_clause, [status(thm)], [sdef62])).
% 15.06/2.63 cnf(p24, plain, (event(sk6,sk11) | ~spl12), inference(avatar_component_clause, [status(thm)], [sdef12])).
% 15.06/2.63 cnf(p419, plain, (~agent(sk6,sk11,sk10) | ~present(sk6,sk11) | ~barrel(sk6,sk11) | ~down(sk6,sk11,sk9) | ~in(sk6,sk11,sk7) | ~spl12 | ~spl62), inference(resolution, [status(thm)], [p418, p24])).
% 15.06/2.63 cnf(ssp333, plain, (~spl12 | ~spl62 | spl63 | spl64 | spl65 | spl66 | spl67), inference(avatar_split_clause, [status(thm)], [p419, sdef63, sdef64, sdef65, sdef66, sdef67])).
% 15.06/2.63 cnf(p412, plain, (~chevy(sk6,X0) | ~white(sk6,X0) | ~dirty(sk6,X0) | ~old(sk6,X0) | ~event(sk6,X1) | ~agent(sk6,X1,X0) | ~present(sk6,X1) | ~barrel(sk6,X1) | ~down(sk6,X1,sk9) | ~in(sk6,X1,sk7) | ~spl61), inference(avatar_component_clause, [status(thm)], [sdef61])).
% 15.06/2.63 cnf(p428, plain, (~white(sk6,sk10) | ~dirty(sk6,sk10) | ~old(sk6,sk10) | ~event(sk6,X0) | ~agent(sk6,X0,sk10) | ~present(sk6,X0) | ~barrel(sk6,X0) | ~down(sk6,X0,sk9) | ~in(sk6,X0,sk7) | ~spl8 | ~spl61), inference(resolution, [status(thm)], [p412, p16])).
% 15.06/2.63 cnf(ssp334, plain, (~spl8 | ~spl61 | spl56 | spl57 | spl58 | spl62), inference(avatar_split_clause, [status(thm)], [p428, sdef56, sdef57, sdef58, sdef62])).
% 15.06/2.63 cnf(p370, plain, (~of(sk0,X0,X1) | ~city(sk0,X1) | ~hollywood_placename(sk0,X0) | ~placename(sk0,X0) | ~street(sk0,X2) | ~lonely(sk0,X2) | ~chevy(sk0,X3) | ~white(sk0,X3) | ~dirty(sk0,X3) | ~old(sk0,X3) | ~event(sk0,X4) | ~agent(sk0,X4,X3) | ~present(sk0,X4) | ~barrel(sk0,X4) | ~down(sk0,X4,X2) | ~in(sk0,X4,X1) | ~spl0 | ~spl35), inference(resolution, [status(thm)], [p342, p1])).
% 15.06/2.63 cnf(p431, plain, (~city(sk0,sk1) | ~hollywood_placename(sk0,sk2) | ~placename(sk0,sk2) | ~street(sk0,X0) | ~lonely(sk0,X0) | ~chevy(sk0,X1) | ~white(sk0,X1) | ~dirty(sk0,X1) | ~old(sk0,X1) | ~event(sk0,X2) | ~agent(sk0,X2,X1) | ~present(sk0,X2) | ~barrel(sk0,X2) | ~down(sk0,X2,X0) | ~in(sk0,X2,sk1) | ~spl0 | ~spl19 | ~spl35), inference(resolution, [status(thm)], [p38, p370])).
% 15.06/2.63 fof(sdef68, definition, (spl68 <=> (~street(sk0,X0) | ~lonely(sk0,X0) | ~chevy(sk0,X1) | ~white(sk0,X1) | ~dirty(sk0,X1) | ~old(sk0,X1) | ~event(sk0,X2) | ~agent(sk0,X2,X1) | ~present(sk0,X2) | ~barrel(sk0,X2) | ~down(sk0,X2,X0) | ~in(sk0,X2,sk1))), introduced(definition, [new_symbols(naming, [spl68])], [avatar_definition])).
% 15.06/2.63 cnf(ssp335, plain, (~spl0 | ~spl19 | ~spl35 | spl36 | spl37 | spl38 | spl68), inference(avatar_split_clause, [status(thm)], [p431, sdef36, sdef37, sdef38, sdef68])).
% 15.06/2.63 cnf(p432, plain, (~street(sk0,X0) | ~lonely(sk0,X0) | ~chevy(sk0,X1) | ~white(sk0,X1) | ~dirty(sk0,X1) | ~old(sk0,X1) | ~event(sk0,X2) | ~agent(sk0,X2,X1) | ~present(sk0,X2) | ~barrel(sk0,X2) | ~down(sk0,X2,X0) | ~in(sk0,X2,sk1) | ~spl68), inference(avatar_component_clause, [status(thm)], [sdef68])).
% 15.06/2.63 cnf(p433, plain, (~lonely(sk0,sk4) | ~chevy(sk0,X0) | ~white(sk0,X0) | ~dirty(sk0,X0) | ~old(sk0,X0) | ~event(sk0,X1) | ~agent(sk0,X1,X0) | ~present(sk0,X1) | ~barrel(sk0,X1) | ~down(sk0,X1,sk4) | ~in(sk0,X1,sk1) | ~spl27 | ~spl68), inference(resolution, [status(thm)], [p432, p190])).
% 15.06/2.63 fof(sdef69, definition, (spl69 <=> (~chevy(sk0,X0) | ~white(sk0,X0) | ~dirty(sk0,X0) | ~old(sk0,X0) | ~event(sk0,X1) | ~agent(sk0,X1,X0) | ~present(sk0,X1) | ~barrel(sk0,X1) | ~down(sk0,X1,sk4) | ~in(sk0,X1,sk1))), introduced(definition, [new_symbols(naming, [spl69])], [avatar_definition])).
% 15.06/2.63 cnf(ssp336, plain, (~spl27 | ~spl68 | spl48 | spl69), inference(avatar_split_clause, [status(thm)], [p433, sdef48, sdef69])).
% 15.06/2.63 cnf(p434, plain, (~chevy(sk0,X0) | ~white(sk0,X0) | ~dirty(sk0,X0) | ~old(sk0,X0) | ~event(sk0,X1) | ~agent(sk0,X1,X0) | ~present(sk0,X1) | ~barrel(sk0,X1) | ~down(sk0,X1,sk4) | ~in(sk0,X1,sk1) | ~spl69), inference(avatar_component_clause, [status(thm)], [sdef69])).
% 15.06/2.63 cnf(p435, plain, (~white(sk0,sk3) | ~dirty(sk0,sk3) | ~old(sk0,sk3) | ~event(sk0,X0) | ~agent(sk0,X0,sk3) | ~present(sk0,X0) | ~barrel(sk0,X0) | ~down(sk0,X0,sk4) | ~in(sk0,X0,sk1) | ~spl23 | ~spl69), inference(resolution, [status(thm)], [p434, p114])).
% 15.06/2.63 cnf(ssp337, plain, (~spl23 | ~spl69 | spl40 | spl41 | spl42 | spl49), inference(avatar_split_clause, [status(thm)], [p435, sdef40, sdef41, sdef42, sdef49])).
% 15.06/2.63 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, ssp245, ssp246, ssp247, ssp248, ssp249, ssp250, ssp251, ssp252, ssp253, ssp254, ssp255, ssp256, ssp257, ssp258, ssp259, ssp260, ssp261, ssp262, ssp263, ssp264, ssp265, ssp266, ssp267, ssp268, ssp269, ssp270, ssp271, ssp272, ssp273, ssp274, ssp275, ssp276, ssp277, ssp278, ssp279, ssp280, ssp281, ssp282, ssp283, ssp284, ssp285, ssp286, ssp287, ssp288, ssp289, ssp290, ssp291, ssp292, ssp293, ssp294, ssp295, ssp296, ssp297, ssp298, ssp299, ssp300, ssp301, ssp302, ssp303, ssp304, ssp305, ssp306, ssp307, ssp308, ssp309, ssp310, ssp311, ssp312, ssp313, ssp314, ssp315, ssp316, ssp317, ssp318, ssp319, ssp320, ssp321, ssp322, ssp323, ssp324, ssp325, ssp326, ssp327, ssp328, ssp329, ssp330, ssp331, ssp332, ssp333, ssp334, ssp335, ssp336, ssp337, sct0, sct1, sct2, sct3, sct4, sct5, sct6, sct7, sct8, sct9, sct10, sct11, sct12, sct13, sct14, sct15, sct16, sct17, sct18, sct19, sct20, sct21, sct22, sct23])).
% 15.06/2.63 % SZS output end Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------